Exact Fourier circuits: packed schedule

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

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

theorem Complexity.ExactFourier.Packing.pack_list {α γ : Type} [Fintype α] [Fintype γ] [DecidableEq α] [DecidableEq γ] (J : Matrix γ γ ℂ) (L : List (Matrix α α ℂ)) (hL : ∀ B ∈ L, ∃ (M : Matrix α α ℂ) (e : γ ↪ α), MonomialMatrix M ∧ B = M * Embedded.matrix e J) : ∃ (W : Word (fun (x : Unit) => γ) (fun (x : Unit) => J) α), W.matrix = L.prod ∧ W.calls.length = L.length

Convert exact slot factorizations to a literal word, retaining the precise call count.

theorem Complexity.ExactFourier.Packing.packed_schedule {τ : 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 : τ → ℕ) (W : (p : π) → FramedWord D (β p)) {T : ℕ} (time : (p : π) → Fin (W p).frames.length → Fin T) (ht : ∀ (p : π), StrictMono (time p)) (hc : ∀ (s : Fin T) (t : τ), Fintype.card { p : π // (slotCall (framedSlot (W p) (time p) s)).kind = some t } = k t) (hw : Fintype.card (ActiveSpace D k ⊕ ν) ≤ Fintype.card ((p : π) × β p)) : ∃ (V : Word (fun (x : Unit) => ActiveSpace D k ⊕ ν) (fun (x : Unit) => inventoryWithIdentity k) ((p : π) × β p)), (V.matrix = Matrix.blockDiagonal' fun (p : π) => (W p).matrix) ∧ V.calls.length = T

def Complexity.ExactFourier.Packing.cyclicStart (F : ℕ) {m : ℕ} (j : Fin m) : ℕ

Sectors with identical programs start cyclically at the F possible starts.

Equations

• Complexity.ExactFourier.Packing.cyclicStart F j = ↑j % F

theorem Complexity.ExactFourier.Packing.same_remainder_card {m F : ℕ} (S : Finset (Fin m)) (hS : ∀ i ∈ S, ∀ j ∈ S, ↑i % F = ↑j % F) : S.card ≤ m / F + 1

Within any one residue class, division by F is an injective label.

theorem Complexity.ExactFourier.Packing.occurrence_card {m F o t : ℕ} : {j : Fin m | cyclicStart F j + o = t}.card ≤ m / F + 1

Every occurrence of a fixed program has at most floor(m/F)+1 copies in a slot.

theorem Complexity.ExactFourier.Packing.occurrence_card_real {m F o t : ℕ} (hF : 0 < F) : ↑{j : Fin m | cyclicStart F j + o = t}.card ≤ ↑m / ↑F + 1

def Complexity.ExactFourier.Packing.occurrences {τ : Type u_2} [DecidableEq τ] (P : List τ) (i : τ) : Finset (Fin P.length)

Positions of calls of type i within a fixed sector program.

Equations

• Complexity.ExactFourier.Packing.occurrences P i = {o : Fin P.length | P.get o = i}

def Complexity.ExactFourier.Packing.scheduledLoad {π : Type u_1} {τ : Type u_2} [Fintype π] [DecidableEq τ] (P : π → List τ) (m : π → ℕ) (F : ℕ) (i : τ) (t : ℕ) : ℕ

Exact number of calls of a given type at a given time in the cyclic schedule.

Equations

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

def Complexity.ExactFourier.Packing.totalCalls {π : Type u_1} {τ : Type u_2} [Fintype π] [DecidableEq τ] (P : π → List τ) (m : π → ℕ) (i : τ) : ℕ

Total calls of a type before scheduling.

Equations

• Complexity.ExactFourier.Packing.totalCalls P m i = ∑ p : π, m p * (Complexity.ExactFourier.Packing.occurrences (P p) i).card

theorem Complexity.ExactFourier.Packing.scheduledLoad_bound {π : Type u_1} {τ : Type u_2} [Fintype π] [DecidableEq τ] (P : π → List τ) (m : π → ℕ) (F : ℕ) (hF : 0 < F) (i : τ) (t : ℕ) : ↑(scheduledLoad P m F i t) ≤ ↑(totalCalls P m i) / ↑F + ∑ p : π, ↑(P p).length

The additive discrepancy is a constant depending only on the fixed program family, not on sector multiplicities or on the number of slots.

theorem Complexity.ExactFourier.Packing.schedule_strict {F m : ℕ} (j : Fin m) : StrictMono fun (o : ℕ) => cyclicStart F j + o

Chronological order is strict inside every sector, including repeated types.

theorem Complexity.ExactFourier.Packing.schedule_in_range {F L m : ℕ} (hF : 0 < F) (j : Fin m) (o : Fin L) : cyclicStart F j + ↑o < F + L - 1

No occurrence is placed outside the allocated F+L-1 slots.

theorem Complexity.ExactFourier.Packing.scheduledLoad_capacity {π : Type u_1} {τ : Type u_2} [Fintype π] [DecidableEq τ] (P : π → List τ) (m : π → ℕ) (F : ℕ) (hF : 0 < F) (capacity : τ → ℕ) (hmargin : ∀ (i : τ), ↑(totalCalls P m i) / ↑F + ∑ p : π, ↑(P p).length ≤ ↑(capacity i)) (i : τ) (t : ℕ) : scheduledLoad P m F i t ≤ capacity i

theorem Complexity.ExactFourier.Packing.framedSlot_type {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (W : FramedWord D α) {T : ℕ} (time : Fin W.frames.length → Fin T) (ht : Function.Injective time) (s : Fin T) (t : τ) : (slotCall (framedSlot W time s)).kind = some t ↔ ∃ (i : Fin W.frames.length), time i = s ∧ (W.frames.get i).type = t

def Complexity.ExactFourier.Packing.subtypeSigmaAll {π : Type} {β : π → Type} (P : (p : π) → β p → Prop) : { x : (p : π) × β p // P x.fst x.snd } ≃ (p : π) × { x : β p // P p x }

Move a dependent predicate from a sigma type into each individual summand.

Equations

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

theorem Complexity.ExactFourier.Packing.card_subtype_sigma {π : Type} [Fintype π] {β : π → Type} [(p : π) → Fintype (β p)] (P : (p : π) → β p → Prop) [(p : π) → DecidablePred (P p)] : Fintype.card { x : (p : π) × β p // P x.fst x.snd } = ∑ p : π, Fintype.card { x : β p // P p x }

theorem Complexity.ExactFourier.Packing.slot_card {τ : Type} [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [Fintype π] {β : π → Type} [(p : π) → Fintype (β p)] [(p : π) → DecidableEq (β p)] (W : (p : π) → FramedWord D (β p)) {T : ℕ} (time : (p : π) → Fin (W p).frames.length → Fin T) (ht : ∀ (p : π), Function.Injective (time p)) (s : Fin T) (t : τ) : Fintype.card { p : π // (slotCall (framedSlot (W p) (time p) s)).kind = some t } = Fintype.card { v : (p : π) × Fin (W p).frames.length // time v.fst v.snd = s ∧ ((W v.fst).frames.get v.snd).type = t }

theorem Complexity.ExactFourier.Packing.monotone_fiber_gap {n T d : ℕ} (f : Fin n → Fin T) (hm : Monotone f) (hc : ∀ (t : Fin T), Fintype.card { i : Fin n // f i = t } < d) {a b : Fin n} (hab : ↑a + d ≤ ↑b) : f a < f b

A monotone chronological listing cannot repeat a time after more than its capacity.

def Complexity.ExactFourier.Packing.sigmaFiberEquiv {ι : Type} {β : ι → Type} (t : ι) : { x : (i : ι) × β i // x.fst = t } ≃ β t

Identify a sigma type's fiber over one index with that index's coordinate type.

Equations

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

theorem Complexity.ExactFourier.Packing.vacancy_listing {T n : ℕ} (c : Fin T → ℕ) (hn : ∑ t : Fin T, c t = n) : ∃ (f : Fin n → Fin T), Monotone f ∧ ∀ (t : Fin T), Fintype.card { i : Fin n // f i = t } = c t

theorem Complexity.ExactFourier.Packing.exists_dummy_schedule {T d h k : ℕ} (c : Fin T → ℕ) (hc : ∀ (t : Fin T), c t ≤ k) (hkd : k < d) (hsum : ∑ t : Fin T, c t = d * h) : ∃ (time : Fin d → Fin h → Fin T), (∀ (j : Fin d), StrictMono (time j)) ∧ ∀ (t : Fin T), Fintype.card { v : Fin d × Fin h // time v.1 v.2 = t } = c t

Cyclic vacancy allocation; no distribution assumption on the clustering of vacancies.

theorem Complexity.ExactFourier.Packing.exists_dummy_framed {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (W : (t : τ) → FramedWord D (D t)) (hW : ∀ (t : τ) (o : Fin (W t).frames.length), ((W t).frames.get o).type = t) {T : ℕ} (c : τ → Fin T → ℕ) (k d : τ → ℕ) (hc : ∀ (t : τ) (s : Fin T), c t s ≤ k t) (hkd : ∀ (t : τ), k t < d t) (hsum : ∀ (t : τ), ∑ s : Fin T, c t s = d t * (W t).frames.length) : ∃ (time : (v : (t : τ) × Fin (d t)) → Fin (W v.fst).frames.length → Fin T), (∀ (v : (t : τ) × Fin (d t)), StrictMono (time v)) ∧ ∀ (s : Fin T) (t : τ), Fintype.card { v : (t : τ) × Fin (d t) // (slotCall (framedSlot (W v.fst) (time v) s)).kind = some t } = c t s