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 208closure forces φ-structure. -/ 209 210/-- The 8-tick cycle requires visiting 8 distinct states. 211 This is the content of T7: period = 2^D = 8 for D = 3. -/
depends on (40)
Lean names referenced from this declaration's body.