SectorAlgorithm.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Sector algorithm.

def OAI.PowerSaving.RAM.upholstery line 15
Source comment
prepare data structure pack (stamped fields plus x entries). Also need original chips tape.
```
def upholstery (n : ℕ) (f : ℕ→Shard) :=
…
```
abbrev OAI.PowerSaving.RAM.ragTy line 18
def OAI.PowerSaving.RAM.rag line 20
def OAI.PowerSaving.RAM.rolls line 23

theorem OAI.PowerSaving.RAM.Bench.gleamT line 32

Source comment

cost-sensitive use of binary kernel, when input generated within budget

theorem gleamT (hw : ∀ i,n i=2^k i) (hg : ∀ i,k i≤l i) (hn : b.Nick n) (hk : b.Nick k)
    (hI : b.Moves (fun _ => 0) sc fun _ => Complex.I)
    (hx : b.Moves n (a (c cl)) fun i => Tape.tab (n i) (x i)) :
    b.Moves (fun i => n i*hills (l i)) (a (c cl)) fun i =>
      Tape.tab (n i) (gleam (k i) (x i)) := by
…

Mentions: OAI.PowerSaving.RAM.sc, OAI.PowerSaving.Tape.tab, OAI.PowerSaving.hills

structure OAI.PowerSaving.RAM.Bench.Matting line 58
lemma OAI.PowerSaving.RAM.Bench.Matting.transfer line 66
lemma OAI.PowerSaving.RAM.Bench.Matting.kitOf line 71
lemma OAI.PowerSaving.RAM.Bench.Matting.packT line 77
Source documentation
pack via linear scatter, along with all sector tags
```
lemma packT (h : b.Matting n l f)
    (hx : b.Moves (fun _ => 0) (a (c cl)) fun i => Tape.tab (n i) (x i)) :
    b.Moves n (a (ragTy cl)) fun i => Tape.tab (n i) (rag (n i) (f i) (x i)) := by
…
```
Mentions: OAI.PowerSaving.Tape.tab, OAI.PowerSaving.RAM.ragTy, OAI.PowerSaving.RAM.rag
structure OAI.PowerSaving.RAM.Bench.Weft line 93
lemma OAI.PowerSaving.RAM.Bench.Weft.transfer line 102
lemma OAI.PowerSaving.RAM.Bench.Weft.kitOf line 107
lemma OAI.PowerSaving.RAM.Bench.Weft.stowOf line 111

lemma OAI.PowerSaving.RAM.Bench.Weft.shine line 116

Source comment

rolls at a sector start.

lemma shine (h : b.Weft cl n l f x) (hj : b.Nick j) (hg : ∀ i,j i<n i)
    (hz : ∀ i,(patch (n i) (f i) (j i)).seat=0) :
    b.Moves (fun i => seatfare (n i) (f i) (j i) * hills (l i)) (a (c cl))
      fun i => rolls (n i) (f i) (x i) (j i) := by
…

Mentions: OAI.PowerSaving.hills, OAI.PowerSaving.RAM.rolls

lemma OAI.PowerSaving.RAM.Bench.Weft.arrays line 140
lemma OAI.PowerSaving.RAM.Bench.Weft.woven line 174
lemma OAI.PowerSaving.RAM.Bench.Matting.cardT line 207