Prices.lean`

31 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExactFourier.Shear.act_sumInl line 9
Source documentation
Lifting an in-place word to disjoint targets adds no auxiliary coordinates.
```
theorem Shear.act_sumInl {ι κ : Type*} (s : Shear ι) (v : ι → ℂ) (y : κ → ℂ) :
    Shear.act (s.sumInl κ) (Sum.elim v y) = Sum.elim (s.act v) y := by
…
```
Mentions: OAI.ExactFourier.Shear, OAI.ExactFourier.Shear.act
theorem OAI.ExactFourier.runShears_sumInl line 15
theorem OAI.ExactFourier.Program.memorySweep_exists line 23

theorem OAI.ExactFourier.broadcast_subset_exists line 42

Source documentation

The designated outputs are individual reads, not uncharged arbitrary linear maps.

theorem broadcast_subset_exists {ι κ : Type*} (S : Finset κ) (refs : κ → Option ι) :
    ∃ W : List (Shear (ι ⊕ κ)), W.length ≤ S.card ∧
      ∀ (v : ι → ℂ) (y : κ → ℂ),
        runShears W (Sum.elim v y) =
          Sum.elim v (fun j => y j + if j ∈ S then readCoord (refs j) v else 0) := by
…

Mentions: OAI.ExactFourier.Shear, OAI.ExactFourier.runShears, OAI.ExactFourier.readCoord

theorem OAI.ExactFourier.broadcast_exists line 76

theorem OAI.ExactFourier.broadcast_reverse line 84

Source documentation

Inverting the output-read word subtracts exactly the same reads.

theorem broadcast_reverse {ι κ : Type*} (W : List (Shear (ι ⊕ κ)))
    (R : (ι → ℂ) → κ → ℂ)
    (hW : ∀ v y, runShears W (Sum.elim v y) = Sum.elim v (fun j => y j + R v j))
    (v : ι → ℂ) (y : κ → ℂ) :
    runShears (reverseShears W) (Sum.elim v y) =
      Sum.elim v (fun j => y j - R v j) := by
…

Mentions: OAI.ExactFourier.Shear, OAI.ExactFourier.runShears, OAI.ExactFourier.reverseShears

theorem OAI.ExactFourier.replay_readout line 100

Source documentation

Forward/read/reverse on arbitrary memory. This is a word identity, not an assumption that dirty scratch starts at zero.

theorem replay_readout {ι κ : Type*} (W : List (Shear ι))
    (B : List (Shear (ι ⊕ κ))) (R : (ι → ℂ) → κ → ℂ)
    (hB : ∀ v y, runShears B (Sum.elim v y) = Sum.elim v (fun j => y j + R v j))
    (v : ι → ℂ) (y : κ → ℂ) :
    runShears ((W.map (fun s => s.sumInl κ)) ++ B ++
        reverseShears (W.map (fun s => s.sumInl κ))) (Sum.elim v y) =
      Sum.elim v (fun j => y j + R (runShears W v) j) := by
…

Mentions: OAI.ExactFourier.Shear, OAI.ExactFourier.runShears, OAI.ExactFourier.reverseShears

theorem OAI.ExactFourier.dirty_coordinate_replay_count line 113
theorem OAI.ExactFourier.Shear.act_eq_mulVec line 175
Source documentation
The operational shears above are the ordinary elementary matrices.
```
theorem Shear.act_eq_mulVec {ι : Type*} [Fintype ι] [DecidableEq ι]
    (s : Shear ι) (v : ι → ℂ) : s.act v = s.toMatrix.mulVec v := by
…
```
Mentions: OAI.ExactFourier.Shear
def OAI.ExactFourier.shearMatrix line 181
theorem OAI.ExactFourier.runShears_eq_mulVec line 184
theorem OAI.ExactFourier.shearMatrix_isUnit line 192
def OAI.ExactFourier.replayMatrix line 201
Source documentation
Jam the arbitrary dirty memory in an identity summand. The lower-left block is the designated rectangular map extended by zero on dirty scratch.
```
def replayMatrix {n a k : ℕ} (G : Matrix (Fin a) (Fin n) ℂ) :
    Matrix ((Fin n ⊕ Fin k) ⊕ Fin a) ((Fin n ⊕ Fin k) ⊕ Fin a) ℂ :=
…
```
theorem OAI.ExactFourier.replayMatrix_mulVec line 205

theorem OAI.ExactFourier.dirty_coordinate_replay_matrix line 214

Source documentation

Matrix endpoint of the dirty replay, necessary for the price and boundary laws.

theorem dirty_coordinate_replay_matrix {n a : ℕ} (C : LinearDAG n a)
    (G : Matrix (Fin a) (Fin n) ℂ) (hG : ∀ x, C.eval x = G.mulVec x) :
    ∃ W : List (Shear ((Fin n ⊕ Fin C.size) ⊕ Fin a)),
      W.length ≤ 8 * C.size + 2 * a ∧ shearMatrix W = replayMatrix G := by
…

Mentions: OAI.ExactFourier.LinearDAG, OAI.ExactFourier.Shear, OAI.ExactFourier.shearMatrix, OAI.ExactFourier.replayMatrix

def OAI.ExactFourier.MonomialMatrix line 234
Source documentation
Literal permutation-times-invertible-diagonal form on a finite index type.
```
def MonomialMatrix {ι : Type*} [DecidableEq ι] (A : Matrix ι ι ℂ) : Prop :=
…
```
structure OAI.ExactFourier.MatrixPrice line 238
theorem OAI.ExactFourier.MonomialMatrix.diagonal line 266
theorem OAI.ExactFourier.MonomialMatrix.one line 274
theorem OAI.ExactFourier.MatrixPrice.one line 281
theorem OAI.ExactFourier.MatrixPrice.identity_pad line 285
theorem OAI.ExactFourier.MatrixPrice.transvection_isUnit line 290
theorem OAI.ExactFourier.MatrixPrice.shear_two line 297
Source documentation
Diagonal conjugation varies the shear coefficient, including all complex values.
```
theorem shear_two (p : MatrixPrice) (c : ℂ) (hc : c ≠ 0) :
    p.value (Matrix.transvection (1 : Fin 2) 0 c) = 1 := by
…
```
Mentions: OAI.ExactFourier.MatrixPrice
def OAI.ExactFourier.MatrixPrice.pairComplement line 314
Source documentation
An ordered pair and its untouched complement, used for exact identity padding.
```
noncomputable def pairComplement {ι : Type*} (i j : ι) (hij : i ≠ j) :
    (Fin 2 ⊕ {t : ι // t ≠ i ∧ t ≠ j}) ≃ ι := by
…
```
theorem OAI.ExactFourier.MatrixPrice.pairComplement_left₀ line 334
theorem OAI.ExactFourier.MatrixPrice.pairComplement_left₁ line 337
theorem OAI.ExactFourier.MatrixPrice.pairComplement_right line 340
theorem OAI.ExactFourier.MatrixPrice.transvection_le_one line 344
Source documentation
Every coordinate shear is a single two-coordinate shear, with literal identity padding.
```
theorem transvection_le_one (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι]
    (i j : ι) (hij : i ≠ j) (c : ℂ) : p.value (Matrix.transvection i j c) ≤ 1 := by
…
```
Mentions: OAI.ExactFourier.MatrixPrice
theorem OAI.ExactFourier.MatrixPrice.transvection_list_isUnit line 363

theorem OAI.ExactFourier.MatrixPrice.transvection_list_le line 371

Source documentation

Every literal shear in an implementing word is charged.

theorem transvection_list_le (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι]
    (L : List (Matrix.TransvectionStruct ι ℂ)) :
    p.value (L.map Matrix.TransvectionStruct.toMatrix).prod ≤ L.length := by
…

Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.L

theorem OAI.ExactFourier.MatrixPrice.difference_le line 387

Source documentation

Inverse symmetry and subadditivity control a relative transformation in both directions.

theorem difference_le (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι]
    (A B : Matrix ι ι ℂ) (hA : IsUnit A) (hB : IsUnit B) :
    |p.value B - p.value A| ≤ p.value (A⁻¹ * B) := by
…

Mentions: OAI.ExactFourier.MatrixPrice