nontrivial_closed_has_phi_structure

formal source

 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
 151/-- **The Derived T6 Requirement**: Combining T4 (recognition forces
 152    non-triviality) with T6 closure (non-trivial closed ledger has
 153    φ-structure), we derive that any physical configuration has
 154    φ-structure — WITHOUT introducing it as an axiom.
 155
 156    Premises (all from T0–T8):
 157    - T4: configuration is non-trivial (recognition requires distinguishing)
 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 :=