t6_derived

formal source

 158    - T2: entries live on a geometric scale sequence (discreteness)
 159    - T6: the sequence is closed with ratio φ (closure)
 160    - Past Theorem: x = 1 is in the configuration (ground state exists) -/
 161theorem t6_derived {N : ℕ} (hN : 2 ≤ N)
 162    (c : InitialCondition.Configuration N)
 163    (h_T4 : T4_Recognition c)
 164    (h_ground : ∃ j : Fin N, c.entries j = 1)
 165    (h_on_ladder : ∀ i : Fin N, ∃ n : ℤ, c.entries i = PhiForcing.φ ^ n) :
 166    has_phi_structure c :=
 167  nontrivial_closed_has_phi_structure hN c h_T4.nontrivial h_ground h_on_ladder
 168
 169/-! ## Part V: Ground State Instability (now fully derived)
 170
 171The incompatibility between x = 1 (all entries uniform) and T4 (recognition
 172forces non-triviality) is now a THEOREM, not an assumption. -/
 173
 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 :=