Charged finite certificate materialization

The bounded guess phase produces every certificate of length at most a stored unary bound and no longer certificate. It preserves unrelated tapes, consumes its read-only external stream, and accounts for its reusable certificate tape with an explicit projected all-prefix space bound.

theorem Complexity.WitnessTM.storeBounded_hoareTime {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 {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 {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.