Canonical binary count-up loops — comparison internals

This module proves the exact full-width comparison run used by TM.binaryForTM. The scanner compares two canonical little-endian natural numbers without changing their contents, then rewinds both cursors. Under the loop invariant value ≤ limitValue, the run takes exactly binaryForCompareTime limitValue steps and branches to the composite iteration precisely below the limit, or to done precisely at equality.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame_of_eq_internal {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, the full-width comparison preserves every tape exactly and reaches the loop's done state in the advertised exact time.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame_of_lt_internal {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, the full-width comparison preserves every tape exactly and reaches the composite iteration start in the advertised time.

theorem Complexity.TM.binaryForTM_compare_reachesIn_frame_internal {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 complete canonical comparison has one exact, fully framed endpoint. The endpoint enters the composite iteration exactly below the limit and is the final done configuration exactly at equality.