OAI/Computability/FourierCircuit/Shears.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactFourier.Program.dirtyEval line 10

   Source documentation

   Each internal gate starts at an arbitrary dirty value, and its computed linear combination is added to that value. The literal zero remains literal zero.

   def Program.dirtyEval {n : ℕ} : {k : ℕ} → Program n k →
       (Fin n → ℂ) → (Fin k → ℂ) → (Fin (n + 1 + k) → ℂ)
     | 0, .nil, x, _ => Fin.snoc x 0
     | k + 1, .step p g, x, z =>
         let v := p.dirtyEval x (Fin.init z)
   …

   Mentions: OAI.ExactFourier.Program

2. theorem OAI.ExactFourier.Gate.eval_add line 17
3. theorem OAI.ExactFourier.snoc_add line 21
4. theorem OAI.ExactFourier.Program.dirtyEval_add line 27
5. theorem OAI.ExactFourier.Program.dirtyEval_clean line 41
6. theorem OAI.ExactFourier.Program.dirtyEval_split line 51

   Source documentation

   Exact identity behind the two replays (fft:dirty-forward, fft:dirty-output).

   theorem Program.dirtyEval_split {n k : ℕ} (p : Program n k)
       (x : Fin n → ℂ) (z : Fin k → ℂ) :
       p.dirtyEval x z = p.eval x + p.dirtyEval 0 z := by
   …

   Mentions: OAI.ExactFourier.Program

7. structure OAI.ExactFourier.LinearDAG line 57
8. def OAI.ExactFourier.LinearDAG.eval line 62
9. abbrev OAI.ExactFourier.Shear line 69
10. def OAI.ExactFourier.Shear.act line 71
11. def OAI.ExactFourier.runShears line 75
12. theorem OAI.ExactFourier.runShears_nil line 78
13. theorem OAI.ExactFourier.runShears_cons line 79
14. theorem OAI.ExactFourier.runShears_append line 81
15. theorem OAI.ExactFourier.Shear.act_self line 84
16. theorem OAI.ExactFourier.Shear.act_other line 87
17. theorem OAI.ExactFourier.Shear.act_source line 90
18. theorem OAI.ExactFourier.Shear.inv_act_act line 93
19. def OAI.ExactFourier.reverseShears line 102
20. theorem OAI.ExactFourier.reverseShears_length line 105
21. theorem OAI.ExactFourier.runShears_reverse line 108
22. def OAI.ExactFourier.readCoord line 119

    Source documentation

    none is the literal input zero, not a physical workspace coordinate.

    def readCoord {ι : Type*} (r : Option ι) (v : ι → ℂ) : ℂ := r.elim 0 v

23. theorem OAI.ExactFourier.readCoord_congr_except line 121
24. theorem OAI.ExactFourier.add_reference line 129

    Source documentation

    Adding one permitted reference uses at most one elementary coordinate shear.

    theorem add_reference {ι : Type*} (d : ι) (r : Option ι) (c : ℂ)
        (h : ∀ i, r = some i → d ≠ i) :
        ∃ W : List (Shear ι), W.length ≤ 1 ∧ ∀ v : ι → ℂ,
          runShears W v d = v d + c * readCoord r v ∧
          ∀ i, i ≠ d → runShears W v i = v i := by
    …

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

25. theorem OAI.ExactFourier.add_gate line 149

    Source documentation

    A gate's two (or one) distinct-from-destination reads, with repeated operands allowed.

    theorem add_gate {ι : Type*} {w : ℕ} (d : ι) (refs : Fin w → Option ι)
        (h : ∀ a j, refs a = some j → d ≠ j) (g : Gate w) :
        ∃ W : List (Shear ι), W.length ≤ 2 ∧ ∀ v : ι → ℂ,
          runShears W v d = v d + g.eval (fun a => readCoord (refs a) v) ∧
          ∀ i, i ≠ d → runShears W v i = v i := by
    …

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

26. def OAI.ExactFourier.available line 190
27. def OAI.ExactFourier.Program.dirtyScratch line 193
28. theorem OAI.ExactFourier.Program.dirtyEval_input line 197
29. theorem OAI.ExactFourier.Program.dirtyEval_available line 207
30. theorem OAI.ExactFourier.Program.dirtyScratch_step_cast line 215
31. theorem OAI.ExactFourier.Program.dirtyScratch_step_last line 223
32. def OAI.ExactFourier.replayInputs line 231
33. def OAI.ExactFourier.referenceMap line 234
34. theorem OAI.ExactFourier.read_referenceMap line 239
35. theorem OAI.ExactFourier.referenceMap_avoids line 250
36. theorem OAI.ExactFourier.Program.dirtySweep_exists line 263

    Source documentation

    The full forward-sweep construction, with one coordinate per gate and NO zero register. Its exact semantic statement is uniform in arbitrary dirty initial values.

    theorem Program.dirtySweep_exists {ι : Type*} {n k : ℕ} (p : Program n k)
        (enabled : Bool) (xs : Fin n → ι) (zs : Fin k → ι)
        (hz : Function.Injective zs) (hxz : ∀ i j, xs i ≠ zs j) :
        ∃ W : List (Shear ι), W.length ≤ 2 * k ∧ ∀ v : ι → ℂ,
          (∀ j, runShears W v (zs j) =
            p.dirtyScratch (replayInputs enabled xs v) (v ∘ zs) j) ∧
          (∀ r, (∀ j, r ≠ zs j) → runShears W v r = v r) := by
    …

    Mentions: OAI.ExactFourier.Program, OAI.ExactFourier.Shear, OAI.ExactFourier.runShears, OAI.ExactFourier.replayInputs