ground_state_recognition_impossible

formal source

 174/-- **Ground State–T4 Incompatibility**: The uniform ground state
 175    cannot support recognition. Recognition requires distinguishable
 176    entries, but the unity config has all entries = 1. -/
 177theorem ground_state_recognition_impossible {N : ℕ} (hN : 0 < N) :
 178    ¬ T4_Recognition (InitialCondition.unity_config N hN) := by
 179  intro ⟨⟨i, hi⟩⟩
 180  simp only [InitialCondition.unity_config] at hi
 181  exact hi rfl
 182
 183/-- **Static Ground State Impossible**: No configuration can simultaneously
 184    have zero total defect (forcing all entries to 1) AND support
 185    recognition (forcing at least one entry ≠ 1). -/
 186theorem static_ground_state_impossible {N : ℕ} (hN : 0 < N)
 187    (c : InitialCondition.Configuration N)
 188    (hzero : InitialCondition.total_defect c = 0)
 189    (hT4 : T4_Recognition c) :
 190    False := by
 191  have h_all_one : ∀ i, c.entries i = 1 :=
 192    (InitialCondition.zero_defect_iff_unity hN c).mp hzero
 193  obtain ⟨i, hi⟩ := hT4.nontrivial
 194  exact hi (h_all_one i)
 195
 196/-! ## Part VI: 8-Tick Dynamics Forces Departure (Gap B)
 197
 198T7 (8-Tick): The fundamental dynamics has period 8 (from D = 3).
 199The 8-tick cycle visits 8 vertices of Q₃ via a Gray code Hamiltonian cycle.
 200Each vertex is a distinct 3-bit pattern.
 201
 202A uniform (all x = 1) configuration maps every vertex to the same state.
 203But a Gray code cycle requires adjacent vertices to differ in exactly one bit.
 204If the configuration is uniform, the "cycle" degenerates: all 8 steps are
 205identical, the period collapses from 8 to 1, violating T7.
 206
 207Therefore: T7 forces non-uniform configurations, which combined with T6