structure definition def or abbrev

`T4_Recognition`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 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 -/