Proof-carrying binary routine control -- proof internals #
theorem
Complexity.TM.BinaryForSegmentSpec.reachesIn_internal
{n : ℕ}
{body : TM n}
{counterIdx limitIdx : Fin n}
{bodyTime : ℕ → ℕ}
{startValue limitValue : ℕ}
(spec : body.BinaryForSegmentSpec counterIdx limitIdx bodyTime startValue limitValue)
(count value : ℕ)
:
startValue ≤ value →
value + count = limitValue →
∃ time ≤ binaryForLoopTime bodyTime limitValue value count,
(body.binaryForTM counterIdx limitIdx).reachesIn time (spec.scanCfg value) spec.doneCfg
A bounded segment certificate supplies a terminating run within the standard recursive count-up-loop bound.
theorem
Complexity.TM.BinaryForSegmentSpaceSpec.prefix_withinAuxSpace_internal
{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)
:
startValue ≤ value →
value + count = limitValue →
(body.binaryForTM counterIdx limitIdx).reachesIn time (spec.scanCfg value) cfg →
time ≤ binaryForLoopTime bodyTime limitValue value count → cfg.WithinAuxSpace inputLength spaceBound
Phase-local space obligations cover every prefix of a bounded loop segment, even when an iteration terminates strictly before its time bound.
theorem
Complexity.BinaryRoutine.Sound.branchZero_internal
{n : ℕ}
{onZero onPositive : BinaryRoutine n}
(hzeroSound : onZero.Sound)
(hpositiveSound : onPositive.Sound)
(idx : Fin n)
:
(branchZero idx onZero onPositive).Sound
theorem
Complexity.BinaryRoutine.Sound.binaryFor_internal
{n : ℕ}
{body : BinaryRoutine n}
(hbodySound : body.Sound)
(counterIdx limitIdx : Fin n)
: