Deterministic finite-verifier suffix

Compose the framed pair builder and placed verifier without charging verifier time as space. All ordinary scratch remains charged; the actual output stays on the output tape throughout.

theorem Complexity.WitnessTM.Verifier.suffix_hoareTimeSafety_decide {k : ℕ} (r : ℕ) (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTimeSpace L T S) (x y : List Bool) (extras : Fin (tapes r k) → Tape) (hextraSI : ∀ (i : Fin (tapes r k)), i ≠ witnessIdx r k → i ≠ pairIdx r k → (extras i).StartInvariant) (hextraPos : ∀ (i : Fin (tapes r k)), i ≠ witnessIdx r k → i ≠ pairIdx r k → 1 ≤ (extras i).head) (hblank : ∀ (i : Fin (tapes r k)), r + 1 ≤ ↑i → ↑i < r + 1 + k → extras i = TM.parkedBlank) {initialSpace H : ℕ} (hinit : 1 ≤ initialSpace) (hextraH : ∀ (i : Fin (tapes r k)), i ≠ witnessIdx r k → i ≠ pairIdx r k → (extras i).head ≤ initialSpace) (hpairH : initialSpace + TM.pairBuildTime x.length y.length ≤ H) (hverifyH : (pair x y).length + S (pair x y).length + 1 ≤ H) : (suffix r M).HoareTime (TM.PairBuildFramePre (witnessIdx r k) (pairIdx r k) x y extras TM.parkedBlank) (fun (x_1 : Tape) (x_2 : Fin (tapes r k) → Tape) (out : Tape) => (pair x y ∈ L → out.cells 1 = Γ.one) ∧ (pair x y ∉ L → out.cells 1 = Γ.zero)) (TM.pairBuildTime x.length y.length + 1 + T (pair x y).length) ∧ (suffix r M).HoareSafety (TM.PairBuildFramePre (witnessIdx r k) (pairIdx r k) x y extras TM.parkedBlank) fun (inp : Tape) (work : Fin (tapes r k) → Tape) (out : Tape) => { state := (), input := inp, work := work, output := out }.WithinDecisionSpace x.length H

Once a concrete finite certificate is stored, the deterministic suffix builds the pair and produces the verifier's exact verdict within its original time/space contract. Setup scratch is retained as ordinary charged work.