Joining materialization and ordinary verification

The handoff carries a concrete stored certificate into the deterministic suffix. The time window is a finite maximum, so verifier bounds need not be monotone. The independent space window charges all intermediate ordinary storage.

def Complexity.WitnessTM.Verifier.suffixEntryFor (r k : ℕ) (x y : List Bool) (B : ℕ) : TapePred (tapes r k + 1)

Entry to the deterministic suffix for one fixed finite certificate.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.WitnessTM.Verifier.prefixPost_transition_for {r k : ℕ} {inp out : Tape} {work : Fin (tapes r k + 1) → Tape} {x : List Bool} {B : ℕ} (y : List Bool) (h : prefixPost r k x B inp work out) (hw : work (witnessIdx r k).castSucc = (Tape.init (List.map Γ.ofBool y)).move Dir3.right) : suffixEntryFor r k x y B (TM.transitionInput inp) (fun (i : Fin (tapes r k + 1)) => TM.transitionTape (work i)) (TM.transitionTape out)

Materialization's endpoint passes to the suffix with all charged heads bounded.

theorem Complexity.WitnessTM.Verifier.prefixPost_transition {r k : ℕ} {inp out : Tape} {work : Fin (tapes r k + 1) → Tape} {x : List Bool} {B : ℕ} (h : prefixPost r k x B inp work out) : ∃ (y : List Bool), y.length ≤ B ∧ suffixEntryFor r k x y B (TM.transitionInput inp) (fun (i : Fin (tapes r k + 1)) => TM.transitionTape (work i)) (TM.transitionTape out)

The existential stored witness is retained through the phase handoff.

theorem Complexity.WitnessTM.Verifier.window_bounds (bound resource : ℕ → ℕ) (x y : List Bool) (hy : y.length ≤ bound x.length) : resource (pair x y).length ≤ window bound resource x.length

The finite window bounds a resource on every permitted certificate length.

theorem Complexity.WitnessTM.Verifier.liftedSuffix_for {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) {L : Language} {T S : ℕ → ℕ} (hM : M.DecidesInTimeSpace L T S) (x y : List Bool) (hy : y.length ≤ bound x.length) : (ofDeterministic (suffix r M)).machine.HoareTime (suffixEntryFor r k x y (bound x.length)) (fun (x_1 : Tape) (x_2 : Fin (tapes r k + 1) → Tape) (out : Tape) => (pair x y ∈ L → out.cells 1 = Γ.one) ∧ (pair x y ∉ L → out.cells 1 = Γ.zero)) (TM.pairBuildTime x.length (bound x.length) + 1 + window bound T x.length) ∧ (ofDeterministic (suffix r M)).machine.HoareSafety (suffixEntryFor r k x y (bound x.length)) fun (inp : Tape) (work : Fin (tapes r k + 1) → Tape) (out : Tape) => { state := (), input := inp, work := fun (i : Fin (tapes r k)) => work i.castSucc, output := out }.WithinDecisionSpace x.length (space setup S x.length)

The lifted suffix retains its ordinary verifier bounds and final exact verdict.

theorem Complexity.WitnessTM.Verifier.suffixStage_contract {r : ℕ} {bound : ℕ → ℕ} {k : ℕ} (setup : WitnessBoundSetup r bound) (M : TM k) {L : Language} {T S : ℕ → ℕ} (hM : M.DecidesInTimeSpace L T S) (x : List Bool) : (ofDeterministic (suffix r M)).machine.HoareTime (fun (inp : Tape) (work : Fin (tapes r k + 1) → Tape) (out : Tape) => ∃ (y : List Bool), y.length ≤ bound x.length ∧ suffixEntryFor r k x y (bound x.length) inp work out) (fun (x_1 : Tape) (x_2 : Fin (tapes r k + 1) → Tape) (out : Tape) => ∃ (y : List Bool), y.length ≤ bound x.length ∧ (pair x y ∈ L → out.cells 1 = Γ.one) ∧ (pair x y ∉ L → out.cells 1 = Γ.zero)) (TM.pairBuildTime x.length (bound x.length) + 1 + window bound T x.length) ∧ (ofDeterministic (suffix r M)).machine.HoareSafety (fun (inp : Tape) (work : Fin (tapes r k + 1) → Tape) (out : Tape) => ∃ (y : List Bool), y.length ≤ bound x.length ∧ suffixEntryFor r k x y (bound x.length) inp work out) fun (inp : Tape) (work : Fin (tapes r k + 1) → Tape) (out : Tape) => { state := (), input := inp, work := fun (i : Fin (tapes r k)) => work i.castSucc, output := out }.WithinDecisionSpace x.length (space setup S x.length)

Uniform suffix contract after an existentially chosen bounded certificate.