LinearDAG.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactFourier.Gate.map line 8
theorem OAI.ExactFourier.Gate.eval_map line 13
def OAI.ExactFourier.appendIndex line 16
def OAI.ExactFourier.keepIndex line 21
theorem OAI.ExactFourier.appendIndex_last line 24
theorem OAI.ExactFourier.appendIndex_castSucc line 34
theorem OAI.ExactFourier.keepIndex_succ line 40
theorem OAI.ExactFourier.keepIndex_zero line 43
theorem OAI.ExactFourier.appendIndex_zero line 46
def OAI.ExactFourier.Program.append line 51

theorem OAI.ExactFourier.Program.eval_append line 57

Source documentation

Literal semantics of DAG composition, including preservation of every existing value.

theorem Program.eval_append {n m k l : ℕ} (p : Program n k) (q : Program m l)
    (f : Fin (m + 1) → Fin (n + 1 + k)) (x : Fin n → ℂ) (y : Fin m → ℂ)
    (hf : ∀ (i : Fin (m + 1)), p.eval x (f i) = (Fin.snoc y 0 : Fin (m + 1) → ℂ) i) :
    (∀ j, (p.append f q).eval x (keepIndex j) = p.eval x j) ∧
    (∀ i, (p.append f q).eval x (appendIndex f i) = q.eval y i) := by
…

Mentions: OAI.ExactFourier.Program, OAI.ExactFourier.Program.eval, OAI.ExactFourier.keepIndex, OAI.ExactFourier.appendIndex

def OAI.ExactFourier.LinearDAG.comp line 86
Source documentation
Exact composition: all previous values can be reused without being consumed.
```
noncomputable def LinearDAG.comp {n a b : ℕ} (D : LinearDAG a b) (C : LinearDAG n a) :
    LinearDAG n b where
…
```
Mentions: OAI.ExactFourier.LinearDAG
theorem OAI.ExactFourier.Program.eval_zero line 92
theorem OAI.ExactFourier.Program.eval_input line 101
theorem OAI.ExactFourier.LinearDAG.eval_comp line 110
def OAI.ExactFourier.gateIndex line 129
Source documentation
Index of a newly emitted vector gate.
```
def gateIndex {n k a : ℕ} (i : Fin a) : Fin (n + 1 + (k + a)) :=
…
```
theorem OAI.ExactFourier.gateIndex_last line 132
theorem OAI.ExactFourier.gateIndex_castSucc line 137
def OAI.ExactFourier.Program.emit line 142
Source documentation
Emit independent scalar operations, one cost unit per coordinate, with original operands still available after the whole layer.
```
def Program.emit {n k : ℕ} (p : Program n k) :
    {a : ℕ} → (Fin a → Gate (n + 1 + k)) → Program n (k + a)
  | 0, _ => p
  | a + 1, g => .step (p.emit (g ∘ Fin.castSucc)) ((g (Fin.last a)).map keepIndex)
```
Mentions: OAI.ExactFourier.Program, OAI.ExactFourier.Gate, OAI.ExactFourier.keepIndex
theorem OAI.ExactFourier.Program.eval_emit line 147
def OAI.ExactFourier.LinearDAG.wires line 176
Source documentation
Read-only input relabeling and arbitrary fanout are genuinely free.
```
def LinearDAG.wires {n a : ℕ} (f : Fin a → Fin (n + 1)) : LinearDAG n a where
…
```
Mentions: OAI.ExactFourier.LinearDAG
theorem OAI.ExactFourier.LinearDAG.eval_wires line 181
def OAI.ExactFourier.LinearDAG.layer line 185
Source documentation
A rectangular vector layer still charges every scalar gate separately.
```
def LinearDAG.layer {n a : ℕ} (g : Fin a → Gate (n + 1)) : LinearDAG n a where
…
```
Mentions: OAI.ExactFourier.Gate, OAI.ExactFourier.LinearDAG
theorem OAI.ExactFourier.LinearDAG.size_layer line 190
theorem OAI.ExactFourier.LinearDAG.eval_layer line 193
def OAI.ExactFourier.LinearDAG.addColumn line 200
Source documentation
Append a scaled original input into each existing output accumulator. The two scalar operations per row are charged even for a zero scalar.
```
def LinearDAG.addColumn {n a : ℕ} (C : LinearDAG n a) (j : Fin n) (c : Fin a → ℂ) :
    LinearDAG n a where
…
```
Mentions: OAI.ExactFourier.LinearDAG
theorem OAI.ExactFourier.LinearDAG.eval_addColumn line 208
def OAI.ExactFourier.LinearDAG.matrix line 225
Source documentation
Direct multiplication: this construction will be used only for the fixed spatial matrices in the coefficient-boundary comparison, not as a purported FFT saving.
```
def LinearDAG.matrix (n a : ℕ) (G : Matrix (Fin a) (Fin n) ℂ) : LinearDAG n a :=
…
```
Mentions: OAI.ExactFourier.LinearDAG
theorem OAI.ExactFourier.foldColumns_size line 233
theorem OAI.ExactFourier.foldColumns_eval line 244
theorem OAI.ExactFourier.LinearDAG.size_matrix line 254
theorem OAI.ExactFourier.LinearDAG.eval_matrix line 258
theorem OAI.ExactFourier.MatrixPrice.twoWay_DAG_bound line 270
Source documentation
Quantitative version of the two-way pre-corner argument, with no hidden inverse oracle: D is an actual charged DAG computing the inverse map.
```
theorem MatrixPrice.twoWay_DAG_bound (p : MatrixPrice) {n : ℕ}
    (G : Matrix (Fin n) (Fin n) ℂ) (hG : IsUnit G) (C D : LinearDAG n n)
    (hC : ∀ x, C.eval x = G.mulVec x) (hD : ∀ x, D.eval x = G⁻¹.mulVec x) :
    p.value G ≤ 8 * C.size + 4 * D.size + 3 * n := by
…
```
Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.LinearDAG
theorem OAI.ExactFourier.MatrixPrice.quadratic_bound line 281
Source documentation
Uniform finite upper bound needed in the compactness branch. It does not assert that any price exists; it is a consequence of the standing price laws.
```
theorem MatrixPrice.quadratic_bound (p : MatrixPrice) {n : ℕ}
    (G : Matrix (Fin n) (Fin n) ℂ) (hG : IsUnit G) :
    p.value G ≤ 24 * (n : ℝ) ^ 2 + 3 * n := by
…
```
Mentions: OAI.ExactFourier.MatrixPrice