nontrivial_closed_has_phi_structure
plain-language theorem explainer
Non-trivial closed configurations on geometric scale sequences possess φ-structure, with a non-zero exponent relative to the ground state of 1. Researchers deriving the golden ratio ladder from Recognition Science T0-T8 would cite this to obtain φ-structure without new axioms. The tactic proof extracts witnesses for non-triviality and the ground state, rules out exponent zero by contradiction, and assembles the structure tuple directly.
Claim. Let $N$ be a natural number with $N ≥ 2$. Let $c$ be a configuration of $N$ positive real entries that is non-trivial, admits a ground-state entry equal to 1, and lies entirely on the geometric scale sequence (every entry equals $φ^n$ for some integer $n$). Then $c$ has $φ$-structure.
background
The module derives that the ground state $x=1$ is the generative source of all structure from T0-T8 with no added assumptions. A Configuration is a structure whose entries field maps each Fin N index to a positive real ratio; total defect sums the individual J-costs. Upstream T4_Recognition forces non-triviality because a uniform ledger carries zero information and cannot support recognition events. PhiForcingDerived.closed_ratio_is_phi establishes that any closed geometric scale sequence has ratio exactly φ.
proof idea
Tactic proof obtains the non-trivial witness i and ground-state witness j, extracts the integer exponent n for entry i, proves n ≠ 0 by showing that n=0 would force the entry to equal 1 and contradict non-triviality, then constructs the required φ-structure tuple from the ratio φ^n / 1.
why it matters
This realizes the T6 closure step inside StillnessGenerative, feeding directly into t6_derived which combines T4 recognition forcing with this result to conclude that every physical configuration has φ-structure. It closes the derivation chain from T2 discreteness and T6 closure to the φ-ladder without external axioms, supporting the eight-tick octave and D=3 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.