Binary work-tape loop combinator -- proof internals

This module proves exact body embedding, bit/blank scanner transitions, the advancing loopback seam, certified finite iteration, and transducer closure.

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

Embed a body configuration in the body phase of forBinaryWorkTM.

Equations

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

theorem Complexity.TM.forBinaryWorkTM_body_step_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) {cfg next : Cfg n body.Q} (hstep : body.step cfg = some next) : (forBinaryWorkTM driverIdx body).step (forBinaryWorkBodyWrap driverIdx body cfg) = some (forBinaryWorkBodyWrap driverIdx body next)

Every nonhalting body step is simulated exactly.

theorem Complexity.TM.forBinaryWorkTM_body_reachesIn_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) {time : ℕ} {cfg next : Cfg n body.Q} (hreach : body.reachesIn time cfg next) : (forBinaryWorkTM driverIdx body).reachesIn time (forBinaryWorkBodyWrap driverIdx body cfg) (forBinaryWorkBodyWrap driverIdx body next)

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

theorem Complexity.TM.forBinaryWorkTM_step_scan_bit_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) (bit : Bool) (cfg : Cfg n (forBinaryWorkTM driverIdx body).Q) (hstate : cfg.state = Sum.inl ForBinaryWorkPhase.scan) (hbit : (cfg.work driverIdx).read = Γ.ofBool bit) (hinput : cfg.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (cfg.work i).read ≠ Γ.start) (houtput : cfg.output.read ≠ Γ.start) : (forBinaryWorkTM driverIdx body).step cfg = some { state := Sum.inr body.qstart, input := cfg.input, work := cfg.work, output := cfg.output }

On either Boolean symbol, the scanner enters the body without moving or changing any tape.

theorem Complexity.TM.forBinaryWorkTM_step_scan_blank_internal {n : ℕ} (driverIdx : Fin n) (body : TM n) (cfg : Cfg n (forBinaryWorkTM driverIdx body).Q) (hstate : cfg.state = Sum.inl ForBinaryWorkPhase.scan) (hblank : (cfg.work driverIdx).read = Γ.blank) (hinput : cfg.input.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (cfg.work i).read ≠ Γ.start) (houtput : cfg.output.read ≠ Γ.start) : (forBinaryWorkTM driverIdx body).step cfg = some { state := Sum.inl ForBinaryWorkPhase.done, input := cfg.input, work := cfg.work, output := cfg.output }

On the first blank, the scanner halts without consuming it.

theorem Complexity.TM.forBinaryWorkTM_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) : (forBinaryWorkTM driverIdx body).step (forBinaryWorkBodyWrap driverIdx body cfg) = some { state := Sum.inl ForBinaryWorkPhase.scan, 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 }

A halted body takes one preserving seam step that advances only the selected driver head.

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

A certified bit-driven loop has its advertised exact remaining run.

theorem Complexity.TM.ForBinaryWorkLoopSpaceSpec.prefix_withinAuxSpace_internal {n : ℕ} {driverIdx : Fin n} {body : TM n} {bodyTime : ℕ → ℕ} {total inputLength spaceBound : ℕ} {spec : ForBinaryWorkLoopSpec driverIdx body bodyTime total} (spaceSpec : ForBinaryWorkLoopSpaceSpec spec inputLength spaceBound) (count value t : ℕ) (c : Cfg n (forBinaryWorkTM driverIdx body).Q) : value + count = total → (forBinaryWorkTM driverIdx body).reachesIn t (spec.scanCfg value) c → t ≤ forBinaryWorkLoopTime bodyTime value count → c.WithinAuxSpace inputLength spaceBound

Every prefix no longer than a certified loop's exact remaining runtime respects its auxiliary-space budget.

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

Bit-driven work iteration preserves one-way output when the body does.