Streaming signed measurement values

The dimension is a runtime unary natural and the radius a runtime binary natural. The decoder uses the existing radix digits to produce ordinary signed integer lists. Count preparation and individual visits are polynomial in their full encoded input, even though the number of visits need not be. All coordinates remain present at radius zero; dimension zero has one empty tuple.

Only the current binary index, full parameters and captured accumulator persist. The decoder may use polynomial scratch (including a dimension-length range), but never constructs the whole measurement box. Index/box lists in the ordered-fold specification are not used by the native loop. The generic callback may grow its accumulator: polynomial whole-loop workspace requires an actual all-prefix accumulator invariant, not just a polynomial per-visit certificate.

This is the measurement-VALUE enumeration of [OAI26c], Lemma 3.2 and Proposition 3.4 (pp. 22–26). It is not formal mode-exponent enumeration, subset-pair traversal, rational coefficient accumulation or a complete runtime/ETH result.

def Cslib.GenericRAM.MeasurementFold.count (p : ℕ × ℕ) : ℕ

The actual number of signed measurement tuples in dimension c and radius D.

theorem Cslib.GenericRAM.MeasurementFold.count_polyTime : Turing.MultiTapeTM.ComputableInPolyTime count (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat

Prepare the visit count in binary, charging the unary dimension and binary radius.

noncomputable def Cslib.GenericRAM.MeasurementFold.clock : NativeCertificate count (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat

An actual fixed native count-preparation machine; no unary exponential count is produced.

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

Both preparation bounds are polynomial in the complete runtime pair encoding.

theorem Cslib.GenericRAM.MeasurementFold.length_count_le (c D : ℕ) : (Turing.MultiTapeTM.encNat (count (c, D))).length ≤ c * (D.size + 1) + 1

The binary count has polynomial bit length, rather than polynomial numeric value.

theorem Cslib.GenericRAM.MeasurementFold.decoder_polyTime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × ℕ) => Radix.measurementValues p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Decode the actual signed measurement values with unary dimension and binary radius/index. No fitting-index hypothesis is needed for this total polynomial-time decoder.

noncomputable def Cslib.GenericRAM.MeasurementFold.decoder : NativeCertificate (fun (p : (ℕ × ℕ) × ℕ) => Radix.measurementValues p.1.1 p.1.2 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

The fixed signed-tuple decoder has an actual polynomial native implementation.

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

The two selected decoder bounds are polynomial in its complete encoded runtime input.

theorem Cslib.GenericRAM.MeasurementFold.length_values_le (c D j : ℕ) : ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) (Radix.measurementValues c D j)).length ≤ c * (2 * (D.size + 1) + 1)

The tuple code is polynomial in dimension and binary radius length, not in radius value.

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

Decode the current index while retaining the full runtime parameters outside the user body.

def Cslib.GenericRAM.MeasurementFold.runPrefix {β : Type} (body : ((ℕ × ℕ) × List ℤ) × β → β) (p : ℕ × ℕ) (j : ℕ) (initial : β) : ℕ × (ℕ × ℕ) × β

A streaming prefix stores only the binary index, complete parameters and captured state.

def Cslib.GenericRAM.MeasurementFold.run {β : Type} (body : ((ℕ × ℕ) × List ℤ) × β → β) (p : ℕ × ℕ) (initial : β) : ℕ × (ℕ × ℕ) × β

Traverse the signed measurement-value box by increasing binary index.

@[simp]

theorem Cslib.GenericRAM.MeasurementFold.prefix_parameters {β : Type} (body : ((ℕ × ℕ) × List ℤ) × β → β) (p : ℕ × ℕ) (j : ℕ) (initial : β) : (runPrefix body p j initial).2.1 = p

Neither dimension nor radius can be overwritten by the callback.

theorem Cslib.GenericRAM.MeasurementFold.prefix_accumulator {β : Type} (body : ((ℕ × ℕ) × List ℤ) × β → β) (p : ℕ × ℕ) (j : ℕ) (initial : β) : (runPrefix body p j initial).2.2 = List.foldl (fun (acc : β) (i : ℕ) => body ((p, Radix.measurementValues p.1 p.2 i), acc)) initial (List.range j)

All prefixes follow the increasing-index order, with full parameters and captured state.

theorem Cslib.GenericRAM.MeasurementFold.run_accumulator {β : Type} (body : ((ℕ × ℕ) × List ℤ) × β → β) (p : ℕ × ℕ) (initial : β) : (run body p initial).2.2 = List.foldl (fun (acc : β) (word : List ℤ) => body ((p, word), acc)) initial (List.map (Radix.measurementValues p.1 p.2) (List.range (count p)))

Exact ordered-fold specification. With measurementValues_coverage, every fitting signed word is visited once. The materialized index/word lists occur only in this specification.

theorem Cslib.GenericRAM.MeasurementFold.length_prefix_le {β : Type} {encB : β ↪ List Bool} (body : ((ℕ × ℕ) × List ℤ) × β → β) (c D j B : ℕ) (initial : β) (hj : j ≤ count (c, D)) (hB : (encB (runPrefix body (c, D) j initial).2.2).length ≤ B) : ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) encB)) (runPrefix body (c, D) j initial)).length ≤ 2 * (c * (D.size + 1) + 1) + 4 * c + 2 * D.size + 4 + B

Full encoded persistent-state bound under the actual prefix accumulator bound. It includes both retained parameters and the final binary counter, including at base one/dimension zero.

theorem Cslib.GenericRAM.MeasurementFold.length_callback_input_le {β : Type} {encB : β ↪ List Bool} (c D j : ℕ) (acc : β) : ((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) encB) (((c, D), Radix.measurementValues c D j), acc)).length ≤ 4 * (2 * c + 1 + D.size) + 2 * (c * (2 * (D.size + 1) + 1)) + 3 + (encB acc).length

Preparing a callback charges both parameters, every signed coordinate and the full captured accumulator. This bound is about the encoded input, not uncharged machine scratch.

theorem Cslib.GenericRAM.MeasurementFold.prepare_polyTime {β : Type} {encB : β ↪ List Bool} : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × (ℕ × ℕ) × β) => ((p.2.1, Radix.measurementValues p.2.1.1 p.2.1.2 p.1), p.2.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) encB)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) encB)

Prepare the complete runtime parameter/tuple/captured-state input to the callback.

noncomputable def Cslib.GenericRAM.MeasurementFold.visitCertificate {β : Type} {encB : β ↪ List Bool} {body : ((ℕ × ℕ) × List ℤ) × β → β} (cb : NativeCertificate body (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) encB) encB) : NativeCertificate (visit body) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) encB)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) encB)

The actual captured callback uses the proved direct decoder, retaining both parameters.

theorem Cslib.GenericRAM.MeasurementFold.visitCertificate_isPolynomial {β : Type} {encB : β ↪ List Bool} {body : ((ℕ × ℕ) × List ℤ) × β → β} (cb : NativeCertificate body (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) encB) encB) (hcb : cb.IsPolynomial) : (visitCertificate cb).IsPolynomial

Polynomial per-visit bounds are derived from the actual callback and decoder machines.

noncomputable def Cslib.GenericRAM.MeasurementFold.certificate {β : Type} {encB : β ↪ List Bool} {α : Type} {encIn : α ↪ List Bool} {parameters : α → ℕ × ℕ} {initial : α → β} {body : ((ℕ × ℕ) × List ℤ) × β → β} (cp : NativeCertificate parameters encIn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat)) (ci : NativeCertificate initial encIn encB) (cb : NativeCertificate body (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) encB) encB) : NativeCertificate (fun (a : α) => run body (parameters a) (initial a)) encIn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encNat) encB))

One fixed native machine streams all measurement values. Count preparation is charged, time retains the visit-count factor, and workspace uses the existing all-prefix maxima. No whole-loop polynomial-time bound or polynomial accumulator invariant is assumed.