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 [OAI26c], 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.

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.lowBits_eq_word (n : ℕ) (j : Fin (2 ^ n)) : BitString.lowBits n ↑j = List.ofFn ((BitString.equivFin n).symm j)

Each valid binary index decodes to its word in the existing finite enumeration order.

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.

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) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary 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 : β) : ((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) 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)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary encB)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) 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 (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) encB) encB) : NativeCertificate (visit body) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary 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 (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) 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 (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) encB) encB) : NativeCertificate (fun (a : α) => run body (dimension a) (initial a)) encIn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary 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.