Read-only-input loop combinator — proof internals

This module supplies the exact body-simulation embedding and the structural one-way-output proof for TM.forInputTM.

def Complexity.TM.forInputBodyWrap {n : ℕ} (body : TM n) (c : Cfg n body.Q) : Cfg n body.forInputTM.Q

Embed a body configuration into the body phase of forInputTM.

Equations

• body.forInputBodyWrap c = { state := Sum.inr c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.forInputTM_body_step_internal {n : ℕ} (body : TM n) {c c' : Cfg n body.Q} (hstep : body.step c = some c') : body.forInputTM.step (body.forInputBodyWrap c) = some (body.forInputBodyWrap c')

Every nonhalting body step is simulated exactly by one forInputTM step.

theorem Complexity.TM.forInputTM_body_reachesIn_internal {n : ℕ} (body : TM n) {t : ℕ} {c c' : Cfg n body.Q} (hreach : body.reachesIn t c c') : body.forInputTM.reachesIn t (body.forInputBodyWrap c) (body.forInputBodyWrap c')

Exact body runs lift through the body phase of forInputTM.

theorem Complexity.TM.forInputTM_step_scan_bit_internal {n : ℕ} (body : TM n) (c : Cfg n body.forInputTM.Q) (hstate : c.state = Sum.inl ForInputPhase.scan) (hstart : c.input.read ≠ Γ.start) (hblank : c.input.read ≠ Γ.blank) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : body.forInputTM.step c = some { state := Sum.inr body.qstart, input := c.input.move Dir3.right, work := c.work, output := c.output }

On a Boolean input symbol, the driver advances the read-only input and enters the body while preserving every off-start work and output tape.

theorem Complexity.TM.forInputTM_step_scan_blank_internal {n : ℕ} (body : TM n) (c : Cfg n body.forInputTM.Q) (hstate : c.state = Sum.inl ForInputPhase.scan) (hblank : c.input.read = Γ.blank) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : body.forInputTM.step c = some { state := Sum.inl ForInputPhase.done, input := c.input, work := c.work, output := c.output }

At the first input blank, the driver halts while preserving all off-start tapes exactly.

theorem Complexity.TM.forInputTM_step_body_halt_internal {n : ℕ} (body : TM n) (c : Cfg n body.Q) (hhalt : body.halted c) (hinput : c.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (c.work i).read ≠ Γ.start) (houtput : c.output.read ≠ Γ.start) : body.forInputTM.step (body.forInputBodyWrap c) = some { state := Sum.inl ForInputPhase.scan, input := c.input, work := c.work, output := c.output }

A halted body takes one preserving seam step back to the input scanner.

theorem Complexity.TM.ForInputLoopSpec.reachesIn_internal {n : ℕ} {body : TM n} {bodyTime : ℕ → ℕ} {total : ℕ} (spec : body.ForInputLoopSpec bodyTime total) (count value : ℕ) : value + count = total → body.forInputTM.reachesIn (forInputLoopTime bodyTime value count) (spec.scanCfg value) spec.doneCfg

A certified input-driven loop has the advertised exact remaining run.

theorem Complexity.TM.ForInputLoopSpaceSpec.prefix_withinAuxSpace_internal {n : ℕ} {body : TM n} {bodyTime : ℕ → ℕ} {total inputLength spaceBound : ℕ} {spec : body.ForInputLoopSpec bodyTime total} (spaceSpec : ForInputLoopSpaceSpec spec inputLength spaceBound) (count value t : ℕ) (c : Cfg n body.forInputTM.Q) : value + count = total → body.forInputTM.reachesIn t (spec.scanCfg value) c → t ≤ forInputLoopTime bodyTime value count → c.WithinAuxSpace inputLength spaceBound

Every configuration reached no later than a certified loop's exact remaining runtime satisfies its auxiliary-space budget.

theorem Complexity.TM.IsTransducer.forInputTM_internal {n : ℕ} {body : TM n} (hbody : body.IsTransducer) : body.forInputTM.IsTransducer

A read-only-input loop preserves the body's one-way-output discipline.