One-prefix work-tape loop combinator — proof internals

This module proves exact body embedding, driver transitions, certified loop execution, and one-way-output preservation for TM.forWorkOnesTM.

def Complexity.TM.forWorkOnesBodyWrap {n : ℕ} (driverIdx : Fin n) (body : TM n) (cfg : Cfg n body.Q) : Cfg n (forWorkOnesTM driverIdx body).Q

Embed a body configuration in the body phase of forWorkOnesTM.

Equations

• Complexity.TM.forWorkOnesBodyWrap driverIdx body cfg = { state := Sum.inr cfg.state, input := cfg.input, work := cfg.work, output := cfg.output }

theorem Complexity.TM.forWorkOnesTM_body_step_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) {cfg next : Cfg n body.Q} (hstep : body.step cfg = some next) : (forWorkOnesTM driverIdx body).step (forWorkOnesBodyWrap driverIdx body cfg) = some (forWorkOnesBodyWrap driverIdx body next)

Every nonhalting body step is simulated exactly.

theorem Complexity.TM.forWorkOnesTM_body_reachesIn_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) {time : ℕ} {cfg next : Cfg n body.Q} (hreach : body.reachesIn time cfg next) : (forWorkOnesTM driverIdx body).reachesIn time (forWorkOnesBodyWrap driverIdx body cfg) (forWorkOnesBodyWrap driverIdx body next)

Exact body runs lift through the combined machine's body phase.

theorem Complexity.TM.forWorkOnesTM_step_scan_one_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) (cfg : Cfg n (forWorkOnesTM driverIdx body).Q) (hstate : cfg.state = Sum.inl ForWorkOnesPhase.scan) (hone : (cfg.work driverIdx).read = Γ.one) (hinput : cfg.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (cfg.work i).read ≠ Γ.start) (houtput : cfg.output.read ≠ Γ.start) : (forWorkOnesTM driverIdx body).step cfg = some { state := Sum.inr body.qstart, input := cfg.input, work := fun (i : Fin n) => if i = driverIdx then (cfg.work i).move Dir3.right else cfg.work i, output := cfg.output }

On a 1, the driver advances its selected work head and enters the body.

theorem Complexity.TM.forWorkOnesTM_step_scan_zero_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) (cfg : Cfg n (forWorkOnesTM driverIdx body).Q) (hstate : cfg.state = Sum.inl ForWorkOnesPhase.scan) (hzero : (cfg.work driverIdx).read = Γ.zero) (hinput : cfg.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (cfg.work i).read ≠ Γ.start) (houtput : cfg.output.read ≠ Γ.start) : (forWorkOnesTM driverIdx body).step cfg = some { state := Sum.inl ForWorkOnesPhase.done, input := cfg.input, work := cfg.work, output := cfg.output }

On the zero separator, the driver halts without consuming it.

theorem Complexity.TM.forWorkOnesTM_step_body_halt_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) (cfg : Cfg n body.Q) (hhalt : body.halted cfg) (hinput : cfg.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (cfg.work i).read ≠ Γ.start) (houtput : cfg.output.read ≠ Γ.start) : (forWorkOnesTM driverIdx body).step (forWorkOnesBodyWrap driverIdx body cfg) = some { state := Sum.inl ForWorkOnesPhase.scan, input := cfg.input, work := cfg.work, output := cfg.output }

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

theorem Complexity.TM.ForWorkOnesLoopSpec.reachesIn_internal {n : ℕ} {driverIdx : Fin n} {body : TM n} {bodyTime : ℕ → ℕ} {total : ℕ} (spec : ForWorkOnesLoopSpec driverIdx body bodyTime total) (count value : ℕ) : value + count = total → (forWorkOnesTM driverIdx body).reachesIn (forWorkOnesLoopTime bodyTime value count) (spec.scanCfg value) spec.doneCfg

A certified consecutive-one loop has its advertised exact remaining run.

theorem Complexity.TM.IsTransducer.forWorkOnesTM_internal {n : ℕ} {driverIdx : Fin n} {body : TM n} (hbody : body.IsTransducer) : (forWorkOnesTM driverIdx body).IsTransducer

Consecutive-one iteration preserves one-way output when the body does.