Exact Fourier circuits: slot assembly

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/SlotAssembly.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.Inventory {τ : Type} (k : τ → ℕ) : Type

The collection of copies of each species in an inventory.

Equations

• Complexity.ExactFourier.Packing.Inventory k = ((t : τ) × Fin (k t))

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.ActiveSpace {τ : Type} (D : τ → Type) (k : τ → ℕ) : Type

The dependent coordinate space of all active species copies.

Equations

• Complexity.ExactFourier.Packing.ActiveSpace D k = ((i : Complexity.ExactFourier.Packing.Inventory k) × D i.fst)

def Complexity.ExactFourier.Packing.inventoryMatrix {τ : Type} [DecidableEq τ] {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} (k : τ → ℕ) : Matrix (ActiveSpace D k) (ActiveSpace D k) ℂ

The block diagonal action of every matrix copy in the active inventory.

Equations

• Complexity.ExactFourier.Packing.inventoryMatrix k = Matrix.blockDiagonal' fun (i : Complexity.ExactFourier.Packing.Inventory k) => A i.fst

theorem Complexity.ExactFourier.Packing.layer_decompose {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [Fintype π] [DecidableEq π] {β : π → Type} [(p : π) → Fintype (β p)] [(p : π) → DecidableEq (β p)] (S : (p : π) → Step D A (β p)) : (Matrix.blockDiagonal' fun (p : π) => (S p).matrix) = (Matrix.blockDiagonal' fun (p : π) => (S p).monoPart) * Embedded.matrix (Embedded.sigmaEmbed fun (p : π) => (S p).activeTuple) (Matrix.blockDiagonal' fun (p : π) => optionalMatrix A (S p).kind)

theorem Complexity.ExactFourier.Packing.gather_active {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [Fintype π] [DecidableEq π] {β : π → Type} [(p : π) → Fintype (β p)] [(p : π) → DecidableEq (β p)] (k : τ → ℕ) (S : (p : π) → Step D A (β p)) (hc : ∀ (t : τ), Fintype.card { p : π // (S p).kind = some t } = k t) : ∃ (e : ActiveSpace D k ↪ (p : π) × β p), Embedded.matrix e (inventoryMatrix k) = Embedded.matrix (Embedded.sigmaEmbed fun (p : π) => (S p).activeTuple) (Matrix.blockDiagonal' fun (p : π) => optionalMatrix A (S p).kind)

def Complexity.ExactFourier.Packing.inventoryWithIdentity {τ : Type} [DecidableEq τ] {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} {ν : Type} [DecidableEq ν] (k : τ → ℕ) : Matrix (ActiveSpace D k ⊕ ν) (ActiveSpace D k ⊕ ν) ℂ

Extend the active inventory matrix by an identity block of spare coordinates.

Equations

• Complexity.ExactFourier.Packing.inventoryWithIdentity k = Matrix.fromBlocks (Complexity.ExactFourier.Packing.inventoryMatrix k) 0 0 1

theorem Complexity.ExactFourier.Packing.embedded_inl {α γ : Type} [DecidableEq α] [DecidableEq γ] (M : Matrix α α ℂ) : Embedded.matrix Function.Embedding.inl M = Matrix.fromBlocks M 0 0 1

theorem Complexity.ExactFourier.Packing.assemble_slot {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [Fintype π] [DecidableEq π] {β : π → Type} [(p : π) → Fintype (β p)] [(p : π) → DecidableEq (β p)] {ν : Type} [Fintype ν] [DecidableEq ν] (k : τ → ℕ) (S : (p : π) → Step D A (β p)) (hc : ∀ (t : τ), Fintype.card { p : π // (S p).kind = some t } = k t) (hw : Fintype.card (ActiveSpace D k ⊕ ν) ≤ Fintype.card ((p : π) × β p)) : ∃ (M : Matrix ((p : π) × β p) ((p : π) × β p) ℂ) (e : ActiveSpace D k ⊕ ν ↪ (p : π) × β p), MonomialMatrix M ∧ (Matrix.blockDiagonal' fun (p : π) => (S p).matrix) = M * Embedded.matrix e (inventoryWithIdentity k)

One full slot, with spectators carrying arbitrary data, is exactly one J call.

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.SpeciesDomain {τ : Type} (D : τ → Type) : Option τ → Type

A species' coordinate type, with a singleton for the identity species.

Equations

• Complexity.ExactFourier.Packing.SpeciesDomain D none = Unit
• Complexity.ExactFourier.Packing.SpeciesDomain D (some t) = D t

@[instance_reducible]

instance Complexity.ExactFourier.Packing.speciesDomainFintype {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] (s : Option τ) : Fintype (SpeciesDomain D s)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Complexity.ExactFourier.Packing.speciesDomainDecidableEq {τ : Type} {D : τ → Type} [(t : τ) → DecidableEq (D t)] (s : Option τ) : DecidableEq (SpeciesDomain D s)

Equations

• One or more equations did not get rendered due to their size.

def Complexity.ExactFourier.Packing.speciesMatrix {τ : Type} {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} (s : Option τ) : Matrix (SpeciesDomain D s) (SpeciesDomain D s) ℂ

The species matrix, using a one-coordinate identity for the absent species.

Equations

• Complexity.ExactFourier.Packing.speciesMatrix none = 1
• Complexity.ExactFourier.Packing.speciesMatrix (some t) = A t

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.speciesCopies {τ : Type} (k : τ → ℕ) (I : ℕ) : Option τ → ℕ

The number of copies of an active species or of the identity species.

Equations

• Complexity.ExactFourier.Packing.speciesCopies k I none = I
• Complexity.ExactFourier.Packing.speciesCopies k I (some t) = k t

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.SpeciesSpace {τ : Type} (D : τ → Type) (k : τ → ℕ) (I : ℕ) : Type

Coordinates grouped by species, copy index, and coordinate within a copy.

Equations

• Complexity.ExactFourier.Packing.SpeciesSpace D k I = ((s : Option τ) × Fin (Complexity.ExactFourier.Packing.speciesCopies k I s) × Complexity.ExactFourier.Packing.SpeciesDomain D s)

def Complexity.ExactFourier.Packing.speciesCoordinates {τ : Type} {D : τ → Type} (k : τ → ℕ) (I : ℕ) : ActiveSpace D k ⊕ Fin I ≃ SpeciesSpace D k I

Regroup active inventory and spare coordinates by their optional species.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.ExactFourier.Packing.speciesCoordinates_matrix {τ : Type} [DecidableEq τ] {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} (k : τ → ℕ) (I : ℕ) : (Matrix.reindex (speciesCoordinates k I) (speciesCoordinates k I)) (inventoryWithIdentity k) = speciesInventory (speciesCopies k I) speciesMatrix

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.LivePair (τ : Type) : Type

A pair of optional species with at least one active member.

Equations

• Complexity.ExactFourier.Packing.LivePair τ = { p : Option τ × Option τ // p ≠ (none, none) }

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.PairDomain {τ : Type} (D : τ → Type) (p : LivePair τ) : Type

The product coordinate type for a live pair of species.

Equations

• Complexity.ExactFourier.Packing.PairDomain D p = (Complexity.ExactFourier.Packing.SpeciesDomain D (↑p).1 × Complexity.ExactFourier.Packing.SpeciesDomain D (↑p).2)

def Complexity.ExactFourier.Packing.pairMatrix {τ : Type} {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} (p : LivePair τ) : Matrix (PairDomain D p) (PairDomain D p) ℂ

The tensor product of the two matrices of a live species pair.

Equations

• Complexity.ExactFourier.Packing.pairMatrix p = (Complexity.ExactFourier.Packing.speciesMatrix (↑p).1).kronecker (Complexity.ExactFourier.Packing.speciesMatrix (↑p).2)

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.LiveSpace {τ : Type} (D : τ → Type) (k : τ → ℕ) (I : ℕ) : Type

All copies of live pair coordinates in the tensor-square inventory.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.ExactFourier.Packing.liveCoordinates {τ : Type} {D : τ → Type} (k : τ → ℕ) (I : ℕ) : LiveSpace D k I ⊕ Fin I × Fin I ≃ SpeciesSpace D k I × SpeciesSpace D k I

Separate live pair coordinates from the identity-only tensor-square coordinates.

Equations

• One or more equations did not get rendered due to their size.

structure Complexity.ExactFourier.Packing.Frame {τ : Type} (D : τ → Type) [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] (α : Type) [Fintype α] [DecidableEq α] : Type

A monomial factor followed in matrix-product order by one embedded species call.

• mono : Matrix α α ℂ

  The monomial matrix factor attached to the call.

• monomial : MonomialMatrix self.mono
• type : τ

  The species called by this frame.

• tuple : D self.type ↪ α

  The ambient coordinates occupied by the species call.

noncomputable def Complexity.ExactFourier.Packing.Frame.matrix {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (f : Frame D α) : Matrix α α ℂ

The product of the frame's monomial factor and its embedded species matrix.

Equations

• f.matrix = f.mono * Complexity.ExactFourier.Embedded.matrix f.tuple (A f.type)

def Complexity.ExactFourier.Packing.Frame.pre {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) (f : Frame D α) : Frame D α

Multiply an additional monomial factor into the front of a frame.

Equations

• Complexity.ExactFourier.Packing.Frame.pre M hm f = { mono := M * f.mono, monomial := ⋯, type := f.type, tuple := f.tuple }

structure Complexity.ExactFourier.Packing.FramedWord {τ : Type} (D : τ → Type) [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] (α : Type) [Fintype α] [DecidableEq α] : Type

A list of species-call frames together with a final monomial factor.

• frames : List (Frame D α)

  The ordered list of monomial-and-call frames.

• tail : Matrix α α ℂ

  The final monomial matrix in the word's product.

• tail_monomial : MonomialMatrix self.tail

noncomputable def Complexity.ExactFourier.Packing.FramedWord.matrix {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (W : FramedWord D α) : Matrix α α ℂ

Multiply all frame matrices in order and then the final monomial factor.

Equations

• W.matrix = (List.map Complexity.ExactFourier.Packing.Frame.matrix W.frames).prod * W.tail

def Complexity.ExactFourier.Packing.FramedWord.types {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {α : Type} [Fintype α] [DecidableEq α] (W : FramedWord D α) : List τ

The ordered sequence of species called by the frames.

Equations

• W.types = List.map Complexity.ExactFourier.Packing.Frame.type W.frames

def Complexity.ExactFourier.Packing.FramedWord.pre {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) (W : FramedWord D α) : FramedWord D α

Absorb a leading monomial factor into the first frame or the final tail.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.ExactFourier.Packing.FramedWord.matrix_pre {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) (W : FramedWord D α) : (pre M hm W).matrix = M * W.matrix

@[simp]

theorem Complexity.ExactFourier.Packing.FramedWord.types_pre {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) (W : FramedWord D α) : (pre M hm W).types = W.types

def Complexity.ExactFourier.Packing.Word.framed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] : Word D A α → FramedWord D α

Collect monomial steps into adjacent call frames and a final monomial tail.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Packing.Word.framed [] = { frames := [], tail := 1, tail_monomial := ⋯ }

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_framed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (W : Word D A α) : W.framed.matrix = W.matrix

@[simp]

theorem Complexity.ExactFourier.Packing.Word.types_framed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (W : Word D A α) : W.framed.types = W.calls

def Complexity.ExactFourier.Packing.Frame.word {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (f : Frame D α) : Word D A α

Expand one frame into its monomial step and embedded species call.

Equations

• f.word = [Complexity.ExactFourier.Packing.Step.mono f.mono ⋯, Complexity.ExactFourier.Packing.Step.call f.type f.tuple]

@[simp]

theorem Complexity.ExactFourier.Packing.Frame.matrix_word {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (f : Frame D α) : f.word.matrix = f.matrix

def Complexity.ExactFourier.Packing.speciesWord {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (s : Option τ) : Word D A (SpeciesDomain D s)

The identity word or one full-coordinate call to the selected species.

Equations

• Complexity.ExactFourier.Packing.speciesWord none = []
• Complexity.ExactFourier.Packing.speciesWord (some t) = Complexity.ExactFourier.Packing.callWord t (Function.Embedding.refl (D t))

@[simp]

theorem Complexity.ExactFourier.Packing.speciesWord_matrix {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (s : Option τ) : (speciesWord s).matrix = speciesMatrix s

noncomputable def Complexity.ExactFourier.Packing.standardPair {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (p : LivePair τ) : Word D A (PairDomain D p)

Realize a live pair by the standard tensor product of its species words.

Equations

• Complexity.ExactFourier.Packing.standardPair p = (Complexity.ExactFourier.Packing.speciesWord (↑p).1).kronecker (Complexity.ExactFourier.Packing.speciesWord (↑p).2)

@[simp]

theorem Complexity.ExactFourier.Packing.standardPair_matrix {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (p : LivePair τ) : (standardPair p).matrix = pairMatrix p

def Complexity.ExactFourier.Packing.pairBaseline {τ : Type} [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] (p : LivePair τ) (t : τ) : ℕ

The number of calls to each species in the standard pair realization.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.ExactFourier.Packing.speciesWord_count {τ : Type} [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (s : Option τ) (t : τ) : (speciesWord s).count t = if s = some t then 1 else 0

@[simp]

theorem Complexity.ExactFourier.Packing.standardPair_count {τ : Type} [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (p : LivePair τ) (t : τ) : (standardPair p).count t = pairBaseline p t

structure Complexity.ExactFourier.Packing.PairComparison {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} : Type

Exact two-factor comparison; identity factors have width one and zero price.

• pair : LivePair τ

  The live pair being realized by the comparison word.

• word : Word D A (PairDomain D self.pair)

  The alternative word realizing the same live pair matrix.

• correct : self.word.matrix = pairMatrix self.pair

def Complexity.ExactFourier.Packing.PairComparison.delta {τ : Type} [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (c : PairComparison) (t : τ) : ℤ

The signed call savings relative to the standard pair realization.

Equations

• c.delta t = ↑(Complexity.ExactFourier.Packing.pairBaseline c.pair t) - ↑(c.word.count t)

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.speciesPrice {τ : Type} (p : τ → ℝ) : Option τ → ℝ

Extend species prices by assigning zero to the identity species.

Equations

• Complexity.ExactFourier.Packing.speciesPrice p none = 0
• Complexity.ExactFourier.Packing.speciesPrice p (some t) = p t

def Complexity.ExactFourier.Packing.pairPrice {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] (p : τ → ℝ) (s : LivePair τ) : ℝ

The standard tensor-product price of a live pair, weighted by coordinate dimensions.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.ExactFourier.Packing.pair_baseline_price {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] (p : τ → ℝ) (s : LivePair τ) : ∑ t : τ, p t * ↑(pairBaseline s t) = pairPrice p s

theorem Complexity.ExactFourier.Packing.comparison_ineq {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (p : τ → ℝ) (c : PairComparison) : ∑ t : τ, p t * ↑(c.delta t) ≤ 0 ↔ pairPrice p c.pair ≤ Word.weight p c.word

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.singlePair {τ : Type} (t : τ) : LivePair τ

The live pair consisting of one active species and the identity species.

Equations

• Complexity.ExactFourier.Packing.singlePair t = ⟨(some t, none), ⋯⟩

def Complexity.ExactFourier.Packing.singleCoordinates (α : Type) : α ≃ α × Unit

Adjoin a singleton coordinate factor without changing the coordinate space.

Equations

• Complexity.ExactFourier.Packing.singleCoordinates α = { toFun := fun (a : α) => (a, ()), invFun := Prod.fst, left_inv := ⋯, right_inv := ⋯ }

noncomputable def Complexity.ExactFourier.Packing.singleComparison {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (t : τ) (W : Word D A (D t)) (hW : W.matrix = A t) : PairComparison

Regard any realization of one species as a comparison for its singleton pair.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.ExactFourier.Packing.singleComparison_price {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (p : τ → ℝ) (t : τ) (W : Word D A (D t)) (hW : W.matrix = A t) : pairPrice p (singleComparison t W hW).pair = p t

@[simp]

theorem Complexity.ExactFourier.Packing.singleComparison_weight {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (p : τ → ℝ) (t : τ) (W : Word D A (D t)) (hW : W.matrix = A t) : Word.weight p (singleComparison t W hW).word = Word.weight p W