WorkingCompiler.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Synchronized Fourier at working length given preparation access to local roots (including all algorithms for scalars and schedules not already explicitly inputs).

def OAI.PowerSaving.RAM.Bench.halos line 18
Source comment
choose dyadic root canonical always
```
def halos : Line := fun i => root (2^i)
```
Mentions: OAI.PowerSaving.Line, OAI.PowerSaving.root
lemma OAI.PowerSaving.RAM.Bench.haloSprings line 20
abbrev OAI.PowerSaving.RAM.Bench.forgeTy line 23
def OAI.PowerSaving.RAM.Bench.forge line 27
Source documentation
local root and dimension table.
```
def forge (l e : ℕ) (r : Axes) (z : ℂ) : T forgeTy :=
…
```
Mentions: OAI.PowerSaving.RAM.Bench.forgeTy
def OAI.PowerSaving.RAM.Bench.teams line 31
abbrev OAI.PowerSaving.RAM.Bench.kilnTy line 34
def OAI.PowerSaving.RAM.Bench.kiln line 35
structure OAI.PowerSaving.RAM.Bench.Foundry line 39
Source comment
readiness via explicit finite tables
```
structure Foundry (b : Bench m ι) (r : ι→Axes) (l e : ι→ℕ) (z : ι→ℂ) : Prop where
…
```
Mentions: OAI.PowerSaving.RAM.Bench
lemma OAI.PowerSaving.RAM.Bench.Foundry.transfer line 49
lemma OAI.PowerSaving.RAM.Bench.Foundry.nickL line 56
lemma OAI.PowerSaving.RAM.Bench.Foundry.archE line 58
lemma OAI.PowerSaving.RAM.Bench.Foundry.nickR line 63
lemma OAI.PowerSaving.RAM.Bench.Foundry.unitM line 70
lemma OAI.PowerSaving.RAM.Bench.Foundry.digitT line 73
lemma OAI.PowerSaving.RAM.Bench.Foundry.kilnD line 77
lemma OAI.PowerSaving.RAM.Bench.Foundry.table line 104

theorem OAI.PowerSaving.RAM.Bench.effuse line 113

Source comment

combine once after change of base; computation includes preliminary forge print

theorem effuse (h : ∀ i, Isles (r i) (l i)) (hl : ∀ i, ∀ j<l i, r i j≤2^e i)
    (hz : ∀ i, IsPrimitiveRoot (z i) (extent (r i) (l i)))
    (h1 : Small S l) (h2 : Small S fun i => 2^e i)
    (h3 : Small b.size S) (h4 : Small b.size fun i => extent (r i) (l i))
    (hp : PolyCan m b.size S b.tray forgeTy b.env fun i => forge (l i) (e i) (r i) (z i))
    (hx : b.Moves (fun _ => 0) (a (c cl)) fun i => Tape.tab (extent (r i) (l i)) (x i)) :
    ∃ d : ℕ,
    b.Moves (fun i => (score (e i)+1)*(extent (r i) (l i)*hills (l i)) + (S i+2)^d)
      (a (c cl)) fun i => Tape.tab (extent (r i) (l i))
        (freq (extent (r i) (l i)) (z i) (x i)) := by
…

Mentions: OAI.PowerSaving.RAM.Small, OAI.PowerSaving.RAM.PolyCan, OAI.PowerSaving.RAM.Bench.forgeTy, OAI.PowerSaving.RAM.Bench.forge, OAI.PowerSaving.Tape.tab, OAI.PowerSaving.hills