Canonical certificate tape has a blank suffix
ProvedCookLevin.certificate_startConfig_blankSuffixblank-suffixcook-levintableau
In the canonical two-input start configuration, the Boolean certificate occupies an initial segment of tape 1 and every subsequent cell is blank.
This is the named no-interior-holes base invariant used by blank-suffix clause soundness.
Formal statement
import Definitions.Def_CookLevin_Reduction
open CookLevin
theorem CookLevin.certificate_startConfig_blankSuffix
{k G Q T : Nat} (hk : 2 ≤ k) (xs : List Symbol)
(w : List Bool) :
BlankSuffix ⟨k, G, Q, T⟩
(startConfig2 k xs (boolsToSymbols w)) 1 := by sorrySource
Existing blankSuffix_startConfig2 theorem in Def_CookLevin_Reduction; supports https://prove2.me/theorems/4ebfa3d8-d96a-46c2-b6c1-f73b21976657