Finite certificate materialization: proof internals

The existing bounded NTM guess phase supplies its endpoint semantics. The choice-tape simulation transfers it to a composable deterministic phase, with separate projected resource accounting for the certificate that it stores.

theorem Complexity.NTM.choiceTM_reachesIn_source_internal {k : ℕ} (N : NTM k) (t : ℕ) (c c' : Cfg (k + 1) N.Q) : N.choiceTM.reachesIn t c c' → (c.work (Fin.last k)).StartInvariant → 1 ≤ (c.work (Fin.last k)).head → c'.work (Fin.last k) = { head := (c.work (Fin.last k)).head + t, cells := (c.work (Fin.last k)).cells }

An actual choice-machine run advances the source exactly once per step and leaves every source cell unchanged.

theorem Complexity.WitnessTM.storeBounded_hoareTime_internal {k : ℕ} (witness counter : Fin k) (hne : witness ≠ counter) (B : ℕ) (inp : Tape) (work : Fin k → Tape) (out source : Tape) (hwitness : work witness = (Tape.init []).move Dir3.right) (hcounter : (work counter).HasUnaryCounter B) (hinput : inp.read ≠ Γ.start) (houtput : out.read ≠ Γ.start) (hother : ∀ (i : Fin k), i ≠ witness → i ≠ counter → (work i).read ≠ Γ.start) (hsource : source.StartInvariant) (hhead : 1 ≤ source.head) : (storeBounded witness counter).machine.HoareTime (storeEntry inp work out source) (storePost witness counter B inp work out source) (NTM.guessBoundedTime B 0)

Every stream run stores a bounded canonical witness, with explicit frames.

theorem Complexity.WitnessTM.storeBounded_generates_internal {k : ℕ} (witness counter : Fin k) (hne : witness ≠ counter) (B : ℕ) (inp : Tape) (work : Fin k → Tape) (out : Tape) (hwitness : work witness = (Tape.init []).move Dir3.right) (hcounter : (work counter).HasUnaryCounter B) (y : List Bool) (hy : y.length ≤ B) : ∃ (g : ℕ → Bool) (c' : Cfg (k + 1) (storeBounded witness counter).machine.Q), ∃ t ≤ NTM.guessBoundedTime B 0, (storeBounded witness counter).machine.reachesIn t { state := (storeBounded witness counter).machine.qstart, input := inp, work := Fin.snoc work (NTM.loadTape g), output := out } c' ∧ (storeBounded witness counter).machine.halted c' ∧ c'.work witness.castSucc = (Tape.init (List.map Γ.ofBool y)).move Dir3.right

Every bounded finite certificate is generated by an external Boolean stream.

theorem Complexity.WitnessTM.storeBounded_hoareSafety_internal {k : ℕ} (witness counter : Fin k) (hne : witness ≠ counter) (B inputLength initialSpace : ℕ) (inp : Tape) (work : Fin k → Tape) (out source : Tape) (hwitness : work witness = (Tape.init []).move Dir3.right) (hcounter : (work counter).HasUnaryCounter B) (hinput : inp.read ≠ Γ.start) (houtput : out.read ≠ Γ.start) (hother : ∀ (i : Fin k), i ≠ witness → i ≠ counter → (work i).read ≠ Γ.start) (hsource : source.StartInvariant) (hhead : 1 ≤ source.head) (hspace : { state := (), input := inp, work := work, output := out }.WithinDecisionSpace inputLength initialSpace) : (storeBounded witness counter).machine.HoareSafety (storeEntry inp work out source) fun (i : Tape) (w : Fin (k + 1) → Tape) (o : Tape) => { state := (), input := i, work := fun (j : Fin k) => w j.castSucc, output := o }.WithinDecisionSpace inputLength (initialSpace + NTM.guessBoundedTime B 0)

The phase stores the certificate in charged space while leaving its source stream uncharged. The conservative bound depends on B, never verifier time.