T4_Recognition

formal source

 117    This is a direct consequence of T4 in the forcing chain. We formalize
 118    it as: for N ≥ 2 (the minimum for any comparison), if recognition is
 119    possible then the configuration is non-trivial. -/
 120structure T4_Recognition {N : ℕ} (c : InitialCondition.Configuration N) : Prop where
 121  nontrivial : is_nontrivial c
 122
 123/-- **T6 Closure Theorem**: A non-trivial configuration on a closed
 124    geometric scale sequence has φ-structure.
 125
 126    From PhiForcingDerived: any closed geometric scale sequence has
 127    ratio = φ. A non-trivial entry on such a sequence sits at some
 128    rung φ^n with n ≠ 0. The ratio between that entry and a ground-state
 129    entry (x = 1) is φ^n / 1 = φ^n.
 130
 131    Derivation chain:
 132      T2 (discreteness) → geometric scale sequence
 133      T6 (closure: 1 + r = r²) → ratio = φ  [PhiForcingDerived.closed_ratio_is_phi]
 134      non-trivial entry → n ≠ 0
 135      → has_phi_structure -/
 136theorem nontrivial_closed_has_phi_structure {N : ℕ} (_hN : 2 ≤ N)
 137    (c : InitialCondition.Configuration N)
 138    (h_nontrivial : is_nontrivial c)
 139    (h_ground : ∃ j : Fin N, c.entries j = 1)
 140    (h_on_ladder : ∀ i : Fin N, ∃ n : ℤ, c.entries i = PhiForcing.φ ^ n) :
 141    has_phi_structure c := by
 142  obtain ⟨i, hi⟩ := h_nontrivial
 143  obtain ⟨j, hj⟩ := h_ground
 144  obtain ⟨n, hn_eq⟩ := h_on_ladder i
 145  have hn_ne : n ≠ 0 := by
 146    intro h_zero
 147    rw [h_zero, zpow_zero] at hn_eq
 148    exact hi hn_eq
 149  exact ⟨i, j, n, hn_ne, by rw [hn_eq, hj, div_one]⟩
 150