Proof-carrying binary routine control

This module exposes a canonical zero branch and a reusable count-up-loop adapter for BinaryRoutine. The loop accepts arbitrary starting counters, requests body obligations only along the reachable segment, and treats body times as upper bounds rather than falsely claiming exact runtimes.

Its auxiliary-space bound is width-sensitive: comparison space and every reachable body-plus-successor budget are maximized rather than accumulated. Thus many iterations can retain logarithmic auxiliary space.

Main results

• BinaryRoutine.Sound.branchZero verifies canonical zero/nonzero dispatch.
• BinaryRoutine.Sound.binaryFor verifies bounded count-up iteration.
• TM.BinaryForSegmentSpec.reachesIn composes a bounded reachable segment.
• TM.BinaryForSegmentSpaceSpec.prefix_withinAuxSpace covers all prefixes.

theorem Complexity.TM.BinaryForSegmentSpec.reachesIn {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {startValue limitValue : ℕ} (spec : body.BinaryForSegmentSpec counterIdx limitIdx bodyTime startValue limitValue) (count value : ℕ) (hstart : startValue ≤ value) (hlimit : value + count = limitValue) : ∃ time ≤ binaryForLoopTime bodyTime limitValue value count, (body.binaryForTM counterIdx limitIdx).reachesIn time (spec.scanCfg value) spec.doneCfg

A bounded reachable-segment certificate terminates within the standard recursive binary-loop bound.

theorem Complexity.TM.BinaryForSegmentSpaceSpec.prefix_withinAuxSpace {n : ℕ} {body : TM n} {counterIdx limitIdx : Fin n} {bodyTime : ℕ → ℕ} {startValue limitValue inputLength spaceBound : ℕ} {spec : body.BinaryForSegmentSpec counterIdx limitIdx bodyTime startValue limitValue} (spaceSpec : BinaryForSegmentSpaceSpec spec inputLength spaceBound) (count value time : ℕ) (cfg : Cfg n (body.binaryForTM counterIdx limitIdx).Q) (hstart : startValue ≤ value) (hlimit : value + count = limitValue) (hreach : (body.binaryForTM counterIdx limitIdx).reachesIn time (spec.scanCfg value) cfg) (htime : time ≤ binaryForLoopTime bodyTime limitValue value count) : cfg.WithinAuxSpace inputLength spaceBound

Phase-local segment bounds cover every reachable prefix of the whole count-up loop.

theorem Complexity.BinaryRoutine.Sound.branchZero {n : ℕ} {onZero onPositive : BinaryRoutine n} (hzero : onZero.Sound) (hpositive : onPositive.Sound) (idx : Fin n) : (BinaryRoutine.branchZero idx onZero onPositive).Sound

Canonical binary zero branching preserves routine soundness.

theorem Complexity.BinaryRoutine.Sound.binaryFor {n : ℕ} {body : BinaryRoutine n} (hbody : body.Sound) (counterIdx limitIdx : Fin n) : (body.binaryFor counterIdx limitIdx).Sound

A sound body yields a sound canonical count-up loop when the routine domain supplies the reachable body obligations and controller preservation.