Canonical two-input configuration satisfies reductionInit
ProvedCookLevin.startConfig2_satisfies_reductionInitcook-levininitial-configurationtableau
The canonical two-input start configuration, with the instance on tape 0 and a Boolean certificate on tape 1, satisfies the Cook-Levin reduction's initial-row constraints whenever the machine dimensions, alphabet, witness length, and tableau width obey their stated bounds.
This packages the semantic completeness invariant for the initial-clause emitter.
Formal statement
import Definitions.Def_CookLevin_Reduction
open CookLevin
theorem CookLevin.startConfig2_satisfies_reductionInit
{k G Q T m : Nat} {xs : List Symbol} {w : List Bool}
(hk : 2 ≤ k) (hG : 4 ≤ G)
(hxs : ∀ s ∈ xs, s < G)
(hw : w.length ≤ m)
(hxT : xs.length ≤ T) (hmT : m ≤ T) :
StartOK ⟨k, G, Q, T⟩ (reductionInit xs m)
(startConfig2 k xs (boolsToSymbols w)) := by sorrySource
Existing startOK_startConfig2 theorem in Def_CookLevin_Reduction; supports https://prove2.me/theorems/98af19bb-6149-4bb6-8b62-937c00cfffef