Streaming local Boolean assignments

The runtime dimension is unary and the current index is binary. The existing lowBits decoder returns exactly that many bits, padding or truncating on arbitrary indices. Its certificate below is derived from direct native list/bit primitives; no legacy polynomial-time bridge is used. The assignment list in the correctness specification is not constructed by the streaming loop.

This is the local Boolean-vector component of the enumeration in [OAI26f], Lemma 3.2 and Proposition 3.4, pp. 22–26. It is not a mixed-radix or subset-pair enumerator, and gives no polynomial-time bound for a whole loop with exponentially many rounds. certificate_bounds gives the loop's explicit bounds instead: when the components are polynomial and every prefix keeps its accumulator polynomially bounded, the workspace is polynomial and the time is 2 ^ n + 1 times a polynomial.

theorem Cslib.GenericRAM.BooleanFold.decoder_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ) => BitString.lowBits p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits

The fixed decoder reads its runtime width in unary and its runtime index in binary. The actual machine has polynomial time and charged workspace in their complete pair encoding.

noncomputable def Cslib.GenericRAM.BooleanFold.decoder : NativeCertificate (fun (p : ℕ × ℕ) => BitString.lowBits p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBits

Bounds selected from the direct fixed decoder machine; the machine is uniform in both runtime width and index. This is not a separate finite machine for every width.

theorem Cslib.GenericRAM.BooleanFold.decoder_isPolynomial : decoder.IsPolynomial

Both selected decoder resource bounds are polynomial in the full encoded input length.

theorem Cslib.GenericRAM.BooleanFold.decoded_range_eq_enumList (n : ℕ) : List.map (BitString.lowBits n) (List.range (2 ^ n)) = BitString.enumList n

The conceptual sequence of decoded indices is exactly the old materializing enumeration. Only this specification uses the list of all indices.

theorem Cslib.GenericRAM.BooleanFold.decoder_injective (n : ℕ) : Function.Injective fun (j : Fin (2 ^ n)) => BitString.lowBits n ↑j

Distinct valid indices decode to distinct runtime words.

theorem Cslib.GenericRAM.BooleanFold.decoder_coverage (n : ℕ) (word : List Bool) (hw : word.length = n) : ∃! j : Fin (2 ^ n), BitString.lowBits n ↑j = word

Every runtime word of the declared length is decoded by exactly one valid index.

def Cslib.GenericRAM.BooleanFold.clock : NativeCertificate (fun (n : ℕ) => 2 ^ n) Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat

Construct the exponential visit count in binary, in linear time in the unary dimension. Only n + 1 output bits are produced; no unary representation of 2 ^ n is constructed.

theorem Cslib.GenericRAM.BooleanFold.length_clock (n : ℕ) : (Turing.MultiTapeTM.encNat (2 ^ n)).length = n + 1

The binary visit count has exactly one more bit than the dimension.

def Cslib.GenericRAM.BooleanFold.visit {β : Type} (body : (ℕ × List Bool) × β → β) (p : ℕ × ℕ × β) : ℕ × β

Decode the current index, retain the runtime dimension and invoke the full captured body.

def Cslib.GenericRAM.BooleanFold.runPrefix {β : Type} (body : (ℕ × List Bool) × β → β) (n j : ℕ) (initial : β) : ℕ × ℕ × β

A prefix of the streaming assignment traversal, retaining width and captured accumulator.

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

The whole traversal, including its completed index and retained dimension.

@[simp]

theorem Cslib.GenericRAM.BooleanFold.prefix_width {β : Type} (body : (ℕ × List Bool) × β → β) (n j : ℕ) (initial : β) : (runPrefix body n j initial).2.1 = n

The dimension is preserved at every prefix, independent of the body.

theorem Cslib.GenericRAM.BooleanFold.prefix_accumulator {β : Type} (body : (ℕ × List Bool) × β → β) (n j : ℕ) (initial : β) : (runPrefix body n j initial).2.2 = List.foldl (fun (acc : β) (i : ℕ) => body ((n, BitString.lowBits n i), acc)) initial (List.range j)

Every prefix visits the decoded words in increasing index order.

theorem Cslib.GenericRAM.BooleanFold.run_accumulator {β : Type} (body : (ℕ × List Bool) × β → β) (n : ℕ) (initial : β) : (run body n initial).2.2 = List.foldl (fun (acc : β) (word : List Bool) => body ((n, word), acc)) initial (BitString.enumList n)

The streaming traversal agrees with the existing enumeration, hence covers every runtime word of length n exactly once in that enumeration's order. The right side is specification-only.

@[reducible, inline]

abbrev Cslib.GenericRAM.BooleanFold.encStreamState {β : Type} (encB : β ↪ List Bool) : ℕ × ℕ × β ↪ List Bool

Streaming state (j, (n, acc)) of runPrefix: the current index j in binary, then the width n in unary, then the captured accumulator under encB. The index and the width are framed; the accumulator is not.

@[reducible, inline]

abbrev Cslib.GenericRAM.BooleanFold.encCallbackInput {β : Type} (encB : β ↪ List Bool) : (ℕ × List Bool) × β ↪ List Bool

Input ((n, word), acc) of one callback: the width n in unary and the decoded word as a bit word, then the captured accumulator under encB. The pair (n, word) is framed, and so is n inside it; the word and the accumulator are not.

theorem Cslib.GenericRAM.BooleanFold.length_prefix_le {β : Type} {encB : β ↪ List Bool} (body : (ℕ × List Bool) × β → β) (n j B : ℕ) (initial : β) (hj : j ≤ 2 ^ n) (hB : (encB (runPrefix body n j initial).2.2).length ≤ B) : ((encStreamState encB) (runPrefix body n j initial)).length ≤ 4 * n + 4 + B

The full live state contains the binary index, retained unary width and accumulator. No word list or exponential history contributes to this prefix bound.

theorem Cslib.GenericRAM.BooleanFold.length_callback_input {β : Type} {encB : β ↪ List Bool} (n j : ℕ) (acc : β) : ((encCallbackInput encB) ((n, BitString.lowBits n j), acc)).length = 6 * n + 3 + (encB acc).length

The decoded word itself always has the declared runtime dimension, even on arbitrary indices. This bounds temporary callback input as well as the persistent state.

theorem Cslib.GenericRAM.BooleanFold.prepare_polyTime {β : Type} {encB : β ↪ List Bool} : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × ℕ × β) => ((p.2.1, BitString.lowBits p.2.1 p.1), p.2.2)) (encStreamState encB) (encCallbackInput encB)

Prepare the complete runtime width/word/captured-accumulator input for one callback.

noncomputable def Cslib.GenericRAM.BooleanFold.visitCertificate {β : Type} {encB : β ↪ List Bool} {body : (ℕ × List Bool) × β → β} (cb : NativeCertificate body (encCallbackInput encB) encB) : NativeCertificate (visit body) (encStreamState encB) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encB)

Construct the actual native captured callback, retaining width outside the user body. Only the supplied body's certificate is assumed; decoder/preparation efficiency is proved here.

theorem Cslib.GenericRAM.BooleanFold.visitCertificate_isPolynomial {β : Type} {encB : β ↪ List Bool} {body : (ℕ × List Bool) × β → β} (cb : NativeCertificate body (encCallbackInput encB) encB) (hcb : cb.IsPolynomial) : (visitCertificate cb).IsPolynomial

A polynomial native body gives a polynomial native visit, in the COMPLETE encoded index/width/captured-state input. This is a per-visit result, not a whole-loop bound.

noncomputable def Cslib.GenericRAM.BooleanFold.certificate {β : Type} {encB : β ↪ List Bool} {α : Type} {encIn : α ↪ List Bool} {dimension : α → ℕ} {initial : α → β} {body : (ℕ × List Bool) × β → β} (cn : NativeCertificate dimension encIn Turing.MultiTapeTM.encUnary) (ci : NativeCertificate initial encIn encB) (cb : NativeCertificate body (encCallbackInput encB) encB) : NativeCertificate (fun (a : α) => run body (dimension a) (initial a)) encIn (encStreamState encB)

A single native machine handles all runtime dimensions. Count construction, initialization, decoding and captured callback costs are included. The inherited IndexFold bounds retain maximum live-state/workspace and linear-in-visit-count time; no exponential whole-loop PT claim is made.

theorem Cslib.GenericRAM.BooleanFold.clock_isPolynomial : clock.IsPolynomial

The clock is linear in the unary dimension.

theorem Cslib.GenericRAM.BooleanFold.certificate_bounds {β : Type} {encB : β ↪ List Bool} {α : Type} {encIn : α ↪ List Bool} {dimension : α → ℕ} {initial : α → β} {body : (ℕ × List Bool) × β → β} {cn : NativeCertificate dimension encIn Turing.MultiTapeTM.encUnary} {ci : NativeCertificate initial encIn encB} {cb : NativeCertificate body (encCallbackInput encB) encB} (hcn : cn.IsPolynomial) (hci : ci.IsPolynomial) (hcb : cb.IsPolynomial) {B : α → ℕ} (hB : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) B) (hstate : ∀ (a : α), ∀ j ≤ 2 ^ dimension a, (encB (runPrefix body (dimension a) j (initial a)).2.2).length ≤ B a) : Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) (certificate cn ci cb).space ∧ ∃ (T : α → ℕ), Turing.MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) T ∧ ∀ (a : α), (certificate cn ci cb).time a ≤ (2 ^ dimension a + 1) * T a

Explicit bounds of a streaming traversal. Suppose the dimension, the initial state and the body have polynomial certificates, and every prefix keeps its accumulator within a polynomial bound B in the encoded input length. Then the traversal of all 2 ^ n words, for n the dimension, uses polynomial workspace, and its time is 2 ^ n + 1 times a polynomial. The traversal count enters only the time.