Canonical binary count-up loops

This module exposes an output-safe bounded loop whose counter and preserved limit use canonical little-endian binary work tapes. Under the certified invariant counter ≤ limit, every test scans the full limit width, so a comparison has the value-independent exact time 2 * limit.size + 2. A nonterminal test runs the supplied body, increments the counter, and returns to a fresh test; equality halts with both binary tapes rewound.

The generic certificates keep body-specific facts explicit. In particular, the loop driver does not assume that an arbitrary body preserves its counter, limit, or tape frames. Clients record those endpoint facts in BinaryForLoopSpec and the corresponding prefix-space facts in BinaryForLoopSpaceSpec.

Main results

• binaryForTM_compare_reachesIn_frame gives the exact framed comparison.
• BinaryForLoopSpec.reachesIn composes a certified loop exactly.
• BinaryForLoopSpaceSpec.prefix_withinAuxSpace covers every run prefix.
• IsTransducer.binaryForTM preserves one-way output safety.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame_of_eq {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hcounter : (work₀ counterIdx).HasBinaryNat value) (hlimit : (work₀ limitIdx).HasBinaryNat value) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime value) { state := Sum.inl (BinaryForPhase.scan true), input := inp₀, work := work₀, output := out₀ } { state := Sum.inl BinaryForPhase.done, input := inp₀, work := work₀, output := out₀ }

At equality, one full-width comparison preserves every tape and reaches the final driver configuration in exact time.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame_of_lt {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value limitValue : ℕ) (hlt : value < limitValue) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hcounter : (work₀ counterIdx).HasBinaryNat value) (hlimit : (work₀ limitIdx).HasBinaryNat limitValue) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime limitValue) { state := Sum.inl (BinaryForPhase.scan true), input := inp₀, work := work₀, output := out₀ } { state := Sum.inr (body.binaryForIterationTM counterIdx).qstart, input := inp₀, work := work₀, output := out₀ }

Strictly below the limit, one full-width comparison preserves every tape and reaches the composite iteration start in exact time.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (value limitValue : ℕ) (hle : value ≤ limitValue) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hcounter : (work₀ counterIdx).HasBinaryNat value) (hlimit : (work₀ limitIdx).HasBinaryNat limitValue) (hinp : inp₀.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (work₀ i).read ≠ Γ.start) (hout : out₀.read ≠ Γ.start) : ∃ (c' : Cfg n (body.binaryForTM counterIdx limitIdx).Q), (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForCompareTime limitValue) { state := Sum.inl (BinaryForPhase.scan true), input := inp₀, work := work₀, output := out₀ } c' ∧ c'.input = inp₀ ∧ c'.work = work₀ ∧ c'.output = out₀ ∧ (c'.state = Sum.inr (body.binaryForIterationTM counterIdx).qstart ↔ value < limitValue) ∧ (c'.state = Sum.inl BinaryForPhase.done ↔ value = limitValue)

A bounded canonical comparison has one exact, fully framed endpoint. It enters the composite iteration exactly below the limit and halts exactly at equality.

theorem Complexity.TM.BinaryForLoopSpec.reachesIn {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue : ℕ} (spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue) (count value : ℕ) (hlimit : value + count = limitValue) : (body.binaryForTM counterIdx limitIdx).reachesIn (binaryForLoopTime bodyTime limitValue value count) (spec.scanCfg value) spec.doneCfg

A certified count-up loop has its advertised exact remaining run.

theorem Complexity.TM.BinaryForLoopSpaceSpec.scanWithin {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue inputLength spaceBound value : ℕ} {spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue} (spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound) (hvalue : value ≤ limitValue) : (spec.scanCfg value).WithinAuxSpace inputLength spaceBound

Every canonical scanner configuration in a certified range satisfies the declared auxiliary-space budget.

theorem Complexity.TM.BinaryForLoopSpaceSpec.doneWithin {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue inputLength spaceBound : ℕ} {spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue} (spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound) : spec.doneCfg.WithinAuxSpace inputLength spaceBound

The final configuration of a space-certified loop satisfies its declared auxiliary-space budget.

theorem Complexity.TM.BinaryForLoopSpaceSpec.prefix_withinAuxSpace {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {limitValue inputLength spaceBound : ℕ} {spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue} (spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound) (count value t : ℕ) (c : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hlimit : value + count = limitValue) (hreach : (body.binaryForTM counterIdx limitIdx).reachesIn t (spec.scanCfg value) c) (htime : t ≤ binaryForLoopTime bodyTime limitValue value count) : c.WithinAuxSpace inputLength spaceBound

Every prefix of a certified binary count-up loop respects its declared auxiliary-space budget.

theorem Complexity.TM.IsTransducer.binaryForTM {n : ℕ} {body : TM n} (hbody : body.IsTransducer) (counterIdx limitIdx : Fin n) : (body.binaryForTM counterIdx limitIdx).IsTransducer

A binary count-up loop preserves the body's one-way-output discipline.