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