Canonical binary count-up loops — control proofs

This module supplies the local proof interface for TM.binaryForTM. It lifts runs of the composite body-plus-successor iteration through the outer control state and gives exact, full-frame transition lemmas for scanning, rewinding, entering an iteration, and returning from a completed iteration.

The canonical multi-step comparison run and loop induction are intentionally left to later proof layers.

def Complexity.TM.binaryForIterationWrap {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (c : Cfg n (body.binaryForIterationTM counterIdx).Q) : Cfg n (body.binaryForTM counterIdx limitIdx).Q

Embed a composite iteration configuration into the iteration phase of binaryForTM.

Equations

• body.binaryForIterationWrap counterIdx limitIdx c = { state := Sum.inr c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.binaryForTM_iteration_step_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) {c c' : Cfg n (body.binaryForIterationTM counterIdx).Q} (hstep : (body.binaryForIterationTM counterIdx).step c = some c') : (body.binaryForTM counterIdx limitIdx).step (body.binaryForIterationWrap counterIdx limitIdx c) = some (body.binaryForIterationWrap counterIdx limitIdx c')

Every nonhalting composite-iteration step is simulated exactly by one binaryForTM step.

theorem Complexity.TM.binaryForTM_iteration_reachesIn_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) {t : ℕ} {c c' : Cfg n (body.binaryForIterationTM counterIdx).Q} (hreach : (body.binaryForIterationTM counterIdx).reachesIn t c c') : (body.binaryForTM counterIdx limitIdx).reachesIn t (body.binaryForIterationWrap counterIdx limitIdx c) (body.binaryForIterationWrap counterIdx limitIdx c')

Exact runs of the composite iteration lift through the iteration phase of binaryForTM.

theorem Complexity.TM.binaryForTM_step_scan_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (equalSoFar : Bool) (c : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hstate : c.state = Sum.inl (BinaryForPhase.scan equalSoFar)) (hmore : ¬((c.work counterIdx).read = Γ.blank ∧ (c.work limitIdx).read = Γ.blank)) (hinput : c.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).step c = some { state := Sum.inl (BinaryForPhase.scan (equalSoFar && decide ((c.work counterIdx).read = (c.work limitIdx).read))), input := c.input, work := Function.update (Function.update c.work counterIdx ((c.work counterIdx).move Dir3.right)) limitIdx ((c.work limitIdx).move Dir3.right), output := c.output }

Away from the common terminating blank, one scanner step compares the current symbols and advances both designated tapes, preserving the full off-start frame.

theorem Complexity.TM.binaryForTM_step_scan_blank_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (equalSoFar : Bool) (c : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hstate : c.state = Sum.inl (BinaryForPhase.scan equalSoFar)) (hcounter : (c.work counterIdx).read = Γ.blank) (hlimit : (c.work limitIdx).read = Γ.blank) (hinput : c.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).step c = some { state := Sum.inl (BinaryForPhase.rewind equalSoFar), input := c.input, work := Function.update (Function.update c.work counterIdx ((c.work counterIdx).move Dir3.left)) limitIdx ((c.work limitIdx).move Dir3.left), output := c.output }

At the common terminating blank, one scanner step enters rewind and moves both designated tapes left, preserving the full off-start frame.

theorem Complexity.TM.binaryForTM_step_rewind_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (equalSoFar : Bool) (c : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hstate : c.state = Sum.inl (BinaryForPhase.rewind equalSoFar)) (hinput : c.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).step c = some { state := Sum.inl (BinaryForPhase.rewind equalSoFar), input := c.input, work := Function.update (Function.update c.work counterIdx ((c.work counterIdx).move Dir3.left)) limitIdx ((c.work limitIdx).move Dir3.left), output := c.output }

One ordinary rewind step moves both designated tapes left, preserving the full off-start frame.

theorem Complexity.TM.binaryForTM_step_rewind_equal_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (c : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hstate : c.state = Sum.inl (BinaryForPhase.rewind true)) (hcounter : (c.work counterIdx).read = Γ.start) (hlimit : (c.work limitIdx).read = Γ.start) (hcounterHead : (c.work counterIdx).head = 0) (hlimitHead : (c.work limitIdx).head = 0) (hinput : c.input.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).step c = some { state := Sum.inl BinaryForPhase.done, input := c.input, work := Function.update (Function.update c.work counterIdx ((c.work counterIdx).move Dir3.right)) limitIdx ((c.work limitIdx).move Dir3.right), output := c.output }

When an equal comparison rewinds to both left markers, one preserving step returns both designated heads to cell one and halts the loop.

theorem Complexity.TM.binaryForTM_step_rewind_unequal_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (hne : counterIdx ≠ limitIdx) (c : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hstate : c.state = Sum.inl (BinaryForPhase.rewind false)) (hcounter : (c.work counterIdx).read = Γ.start) (hlimit : (c.work limitIdx).read = Γ.start) (hcounterHead : (c.work counterIdx).head = 0) (hlimitHead : (c.work limitIdx).head = 0) (hinput : c.input.read ≠ Γ.start) (hother : ∀ (i : Fin n), i ≠ counterIdx → i ≠ limitIdx → (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).step c = some { state := Sum.inr (body.binaryForIterationTM counterIdx).qstart, input := c.input, work := Function.update (Function.update c.work counterIdx ((c.work counterIdx).move Dir3.right)) limitIdx ((c.work limitIdx).move Dir3.right), output := c.output }

When an unequal comparison rewinds to both left markers, one preserving step returns both designated heads to cell one and enters the composite iteration.

theorem Complexity.TM.binaryForTM_step_iteration_halt_internal {n : ℕ} (body : TM n) (counterIdx limitIdx : Fin n) (c : Cfg n (body.binaryForIterationTM counterIdx).Q) (hhalt : (body.binaryForIterationTM counterIdx).halted c) (hinput : c.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : (body.binaryForTM counterIdx limitIdx).step (body.binaryForIterationWrap counterIdx limitIdx c) = some { state := Sum.inl (BinaryForPhase.scan true), input := c.input, work := c.work, output := c.output }

A halted composite iteration takes one preserving outer seam step back to a fresh equality scan.