Streaming folds over binary indices

IndexFold.run calls a body at indices 0, …, n - 1, retaining only its binary index and accumulator. List.range occurs only in the correctness specification. The native certificate uses the existing binary-counted iterator, not a unary clock or a materialized range.

This is an enumeration building block for the local-assignment and measurement loops of [OAI26c], Lemma 3.2 and Proposition 3.4 (pp. 22–26). It does not yet decode indices into Boolean vectors or mixed-radix tuples. A callback may retain captured inputs in its accumulator; its certificate must cover the full index/accumulator encoding. Arbitrary callbacks need not have small outputs: the reachable-prefix size bound is an explicit hypothesis of the resource bound below. No polynomial-time claim is made for an exponentially long whole loop.

def Cslib.GenericRAM.IndexFold.step {β : Type} (body : ℕ × β → β) (p : ℕ × β) : ℕ × β

Advance the binary index after applying the body to the old index and accumulator.

def Cslib.GenericRAM.IndexFold.run {β : Type} (body : ℕ × β → β) (n : ℕ) (initial : β) : ℕ × β

A streaming prefix, including its next index. No list of visited indices is constructed.

@[simp]

theorem Cslib.GenericRAM.IndexFold.run_zero {β : Type} (body : ℕ × β → β) (initial : β) : run body 0 initial = (0, initial)

The empty prefix invokes no callback.

theorem Cslib.GenericRAM.IndexFold.run_succ {β : Type} (body : ℕ × β → β) (n : ℕ) (initial : β) : run body (n + 1) initial = step body (run body n initial)

A prefix is extended by exactly one callback at the current index.

@[simp]

theorem Cslib.GenericRAM.IndexFold.run_index {β : Type} (body : ℕ × β → β) (n : ℕ) (initial : β) : (run body n initial).1 = n

Every prefix has the expected next index, including the final prefix.

theorem Cslib.GenericRAM.IndexFold.run_accumulator {β : Type} (body : ℕ × β → β) (n : ℕ) (initial : β) : (run body n initial).2 = List.foldl (fun (acc : β) (i : ℕ) => body (i, acc)) initial (List.range n)

The accumulator agrees with the ordered range fold. The list is specification-only.

theorem Cslib.GenericRAM.IndexFold.run_eq {β : Type} (body : ℕ × β → β) (n : ℕ) (initial : β) : run body n initial = (n, List.foldl (fun (acc : β) (i : ℕ) => body (i, acc)) initial (List.range n))

The exact ordered state of every prefix. In particular, no index is skipped or repeated.

theorem Cslib.GenericRAM.IndexFold.length_run {β : Type} {encB : β ↪ List Bool} (body : ℕ × β → β) (n : ℕ) (initial : β) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) (run body n initial)).length = 2 * (Turing.MultiTapeTM.encNat n).length + 1 + (encB (run body n initial).2).length

The binary index adds only its encoded length to the live accumulator.

theorem Cslib.GenericRAM.IndexFold.length_run_le {β : Type} {encB : β ↪ List Bool} (body : ℕ × β → β) {n j B : ℕ} (initial : β) (hj : j ≤ n) (hB : (encB (run body j initial).2).length ≤ B) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) (run body j initial)).length ≤ 2 * (Turing.MultiTapeTM.encNat n).length + 1 + B

A common prefix accumulator bound gives a common full-state bound, without multiplying workspace by the number of visited indices.

def Cslib.GenericRAM.IndexFold.roundCertificate {β : Type} {encB : β ↪ List Bool} {body : ℕ × β → β} (cb : NativeCertificate body (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) encB) : NativeCertificate (step body) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB)

The native round is constructed from the existing binary successor and the actual callback certificate. Its input contains both the complete binary index and the complete accumulator.

noncomputable def Cslib.GenericRAM.IndexFold.certificate {β α : Type} {encB : β ↪ List Bool} {encIn : α ↪ List Bool} {count : α → ℕ} {initial : α → β} {body : ℕ × β → β} (cn : NativeCertificate count encIn Turing.MultiTapeTM.encNat) (ci : NativeCertificate initial encIn encB) (cb : NativeCertificate body (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) encB) : NativeCertificate (fun (a : α) => run body (count a) (initial a)) encIn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB)

One fixed native machine streams a runtime binary number of indices. Its bound is the existing iterator's trajectory-max bound; neither a finite state type nor a machine is selected separately for each runtime n.

theorem Cslib.GenericRAM.IndexFold.computableInO {β α : Type} {encB : β ↪ List Bool} {encIn : α ↪ List Bool} {count : α → ℕ} {initial : α → β} {body : ℕ × β → β} (cn : NativeCertificate count encIn Turing.MultiTapeTM.encNat) (ci : NativeCertificate initial encIn encB) (cb : NativeCertificate body (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) encB) (R Q B : α → ℕ) (hR : ∀ (a : α), ∀ j ≤ count a, cb.time (run body j (initial a)) ≤ R a) (hQ : ∀ (a : α), ∀ j ≤ count a, cb.space (run body j (initial a)) ≤ Q a) (hB : ∀ (a : α), ∀ j ≤ count a, (encB (run body j (initial a)).2).length ≤ B a) : Turing.MultiTapeTM.ComputableInO (fun (a : α) => run body (count a) (initial a)) encIn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat encB) (fun (a : α) => cn.time a + ((encIn a).length + ci.time a) + (count a + 1) * (2 * (Turing.MultiTapeTM.encNat (count a)).length + 1 + B a + ((Turing.MultiTapeTM.encNat (count a)).length + 1) ^ 2 + R a + (2 * (Turing.MultiTapeTM.encNat (count a)).length + 1 + B a) + ((Turing.MultiTapeTM.encNat (count a)).length + 1) ^ 2)) fun (a : α) => cn.space a + ((encIn a).length + ci.space a) + (2 * (Turing.MultiTapeTM.encNat (count a)).length + 1 + B a + ((Turing.MultiTapeTM.encNat (count a)).length + 1) + Q a) + (2 * (Turing.MultiTapeTM.encNat (count a)).length + 1 + B a) + (Turing.MultiTapeTM.encNat (count a)).length

Independent time/workspace bounds under explicit reachable-prefix callback and accumulator bounds. The runtime count stays binary. These are charged native O bounds, not exact clocks. R, Q, and B need not be polynomial; a polynomial live-state invariant can be supplied without asserting that the entire exponentially long computation is polynomial-time.