Canonical binary count-up loops — proof internals #
This module turns the wrapper-free loop certificates from BinaryFor.Defs
into exact executions and all-prefix auxiliary-space bounds. It also proves
that the binary loop driver preserves the one-way-output discipline of its
body.
theorem
Complexity.TM.BinaryForLoopSpec.reachesIn_internal
{n : ℕ}
{body : TM n}
{counterIdx limitIdx : Fin n}
{bodyTime : ℕ → ℕ}
{limitValue : ℕ}
(spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue)
(count value : ℕ)
:
value + count = limitValue →
(body.binaryForTM counterIdx limitIdx).reachesIn (binaryForLoopTime bodyTime limitValue value count)
(spec.scanCfg value) spec.doneCfg
A certified canonical binary count-up loop has its advertised exact remaining run.
theorem
Complexity.TM.BinaryForLoopSpaceSpec.scanWithin_internal
{n : ℕ}
{body : TM n}
{counterIdx limitIdx : Fin n}
{bodyTime : ℕ → ℕ}
{limitValue inputLength spaceBound value : ℕ}
{spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue}
(spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound)
(hvalue : value ≤ limitValue)
:
(spec.scanCfg value).WithinAuxSpace inputLength spaceBound
Scanner bounds are the reflexive prefixes of the comparison obligation.
theorem
Complexity.TM.BinaryForLoopSpaceSpec.doneWithin_internal
{n : ℕ}
{body : TM n}
{counterIdx limitIdx : Fin n}
{bodyTime : ℕ → ℕ}
{limitValue inputLength spaceBound : ℕ}
{spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue}
(spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound)
:
spec.doneCfg.WithinAuxSpace inputLength spaceBound
The final-state bound is the complete final comparison prefix.
theorem
Complexity.TM.BinaryForLoopSpaceSpec.prefix_withinAuxSpace_internal
{n : ℕ}
{body : TM n}
{counterIdx limitIdx : Fin n}
{bodyTime : ℕ → ℕ}
{limitValue inputLength spaceBound : ℕ}
{spec : body.BinaryForLoopSpec counterIdx limitIdx bodyTime limitValue}
(spaceSpec : BinaryForLoopSpaceSpec spec inputLength spaceBound)
(count value t : ℕ)
(c : Cfg n (body.binaryForTM counterIdx limitIdx).Q)
:
value + count = limitValue →
(body.binaryForTM counterIdx limitIdx).reachesIn t (spec.scanCfg value) c →
t ≤ binaryForLoopTime bodyTime limitValue value count → c.WithinAuxSpace inputLength spaceBound
Every configuration reached no later than a certified binary loop's exact remaining runtime satisfies its auxiliary-space budget.
theorem
Complexity.TM.IsTransducer.binaryForTM_internal
{n : ℕ}
{body : TM n}
(hbody : body.IsTransducer)
(counterIdx limitIdx : Fin n)
:
(body.binaryForTM counterIdx limitIdx).IsTransducer
A canonical binary count-up loop preserves the body's one-way-output discipline.