Iteration.lean`

22 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Superstring.BitCode.RunsInPolyTime.pair line 12
Source documentation
Compute two values from the same explicitly coded input, then concatenate their self-delimiting encodings. Duplication and concatenation are charged bitwise.
```
theorem pair (hf : RunsInPolyTime ea eb f) (hg : RunsInPolyTime ea ec g) :
    RunsInPolyTime ea (fun p : β × γ => eb p.1 ++ ec p.2) (fun a => (f a, g a)) := by
…
```
Mentions: OAI.Superstring.BitCode.RunsInPolyTime
def OAI.Superstring.BitCode.natCode line 78
Source documentation
Unary natural numbers have an explicit end marker, so prefix parsing never relies on an uncharged register-length operation.
```
def natCode : ℕ → List Bool
  | 0 => [true]
  | n + 1 => false :: natCode n
```
theorem OAI.Superstring.BitCode.length_natCode line 82
theorem OAI.Superstring.BitCode.natCode_eq line 87
theorem OAI.Superstring.BitCode.natCode_reverse line 92
theorem OAI.Superstring.BitCode.Parses.nat line 100
theorem OAI.Superstring.BitCode.RunsInPolyTime.inPlace line 112
Source documentation
Normalize any clean routine to the same input and output register. The linear bit-order-preserving relocation is included in its polynomial clock.
```
theorem inPlace (hf : RunsInPolyTime ea eb f) :
    ∃ (K : Type) (_ : DecidableEq K) (i : K) (b : Block K) (P : Polynomial ℕ),
      ∀ a, ∃ n ≤ P.eval (ea a).length, b.Exec (single i (ea a)) (single i (eb (f a))) n := by
…
```
Mentions: OAI.Superstring.BitCode.RunsInPolyTime, OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.single

theorem OAI.Superstring.BitCode.Block.iterate_exec line 140

Source documentation

Iterate a clean in-place routine once per explicitly stored counter bit. The hypothesis is a STATE SIZE invariant, not an assumed time or computation oracle. The only computation premise is an actual bit-program execution.

theorem iterate_exec (b : Block K) (i : K) (P : Polynomial ℕ)
    (hb : ∀ a, ∃ n ≤ P.eval (e a).length, b.Exec (single i (e a)) (single i (e (f a))) n)
    (n M : ℕ) (a : α) (hsize : ∀ j < n, (e (f^[j] a)).length ≤ M) :
    ∃ t ≤ n * (P.eval M + 2) + 1,
      (Block.loop (Sum.inr () : K ⊕ Unit) (.seq (.pop (.inr ())) (b.rename Sum.inl))).Exec
        (Sum.elim (single i (e a)) (fun _ : Unit => List.replicate n false))
        (Sum.elim (single i (e (f^[n] a))) (fun _ : Unit => [])) t := by
…

Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.single, OAI.Superstring.BitCode.Block.Exec

def OAI.Superstring.BitCode.parserEmbedding line 183
Source documentation
Place the parser's input in an existing work bank, its private storage in a fresh bank, and its output in a fresh counter register.
```
def parserEmbedding {K L : Type} (i : K) : Ports L → (K ⊕ L) ⊕ Unit
  | .inl false => .inl (.inl i)
  | .inl true => .inr ()
  | .inr k => .inl (.inr k)
```
Mentions: OAI.Superstring.BitCode.Ports
theorem OAI.Superstring.BitCode.parserEmbedding_injective line 188
theorem OAI.Superstring.BitCode.Block.Exec.parseAt line 199
theorem OAI.Superstring.BitCode.RunsInPolyTime.iterate line 231
Source documentation
Bounded iteration of an actual polynomial bit routine is polynomial. The bound is on encoded intermediate DATA, and the counter is explicitly unary. This closure rule does not assume a polynomial-time evaluator or a time oracle.
```
theorem iterate {α : Type} {e : α → List Bool} {f : α → α}
    (hf : RunsInPolyTime e e f) (R : Polynomial ℕ)
    (hsize : ∀ n a j, j < n → (e (f^[j] a)).length ≤
      R.eval (natCode n ++ e a).length) :
    RunsInPolyTime (fun p : ℕ × α => natCode p.1 ++ e p.2) e
      (fun p => f^[p.1] p.2) := by
…
```
Mentions: OAI.Superstring.BitCode.RunsInPolyTime, OAI.Superstring.BitCode.natCode
abbrev OAI.Superstring.BitCode.Workspace line 290
abbrev OAI.Superstring.BitCode.workPort line 291
def OAI.Superstring.BitCode.workStore line 292
theorem OAI.Superstring.BitCode.workStore_single line 295
def OAI.Superstring.BitCode.workEmbedding line 302
theorem OAI.Superstring.BitCode.workEmbedding_injective line 305
theorem OAI.Superstring.BitCode.Block.Exec.inWorkspace line 316
theorem OAI.Superstring.BitCode.Block.Exec.workspace line 335
Source documentation
Two in-place workspaces may share their data register, with all their private registers disjoint. Everything outside the active workspace is framed.
```
theorem Exec.workspace {K L : Type} [DecidableEq K] [DecidableEq L]
    {b : Block (Workspace K)} {w v : List Bool} {n : ℕ}
    (h : b.Exec (workStore w (fun _ : K => [])) (workStore v (fun _ : K => [])) n)
    (f : K → L) (hf : Function.Injective f) (z : Store L) (hz : ∀ k, z (f k) = []) :
    (b.rename (Sum.map _root_.id f)).Exec (workStore w z) (workStore v z) n := by
…
```
Mentions: OAI.Superstring.BitCode.Block, OAI.Superstring.BitCode.Workspace, OAI.Superstring.BitCode.workStore, OAI.Superstring.BitCode.Store, OAI.Superstring.BitCode.Block.Exec
theorem OAI.Superstring.BitCode.RunsInPolyTime.canonical line 358

theorem OAI.Superstring.BitCode.RunsInPolyTime.boolCase line 371

Source documentation

Branch on an explicitly encoded Boolean, charging the branch and removal of its bit. No unbounded predicate acts as a primitive instruction.

theorem boolCase {α β : Type} {ea : α → List Bool} {eb : β → List Bool}
    {f g : α → β} (hf : RunsInPolyTime ea eb f) (hg : RunsInPolyTime ea eb g) :
    RunsInPolyTime (fun p : Bool × α => p.1 :: ea p.2) eb
      (fun p => if p.1 then f p.2 else g p.2) := by
…

Mentions: OAI.Superstring.BitCode.RunsInPolyTime