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
proof body
Tactic-mode proof.
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) -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.