has_phi_structure
plain-language theorem explainer
A ledger configuration of N positive real entries has phi-structure when at least one pair of entries stands in nonzero integer ratio phi^n. Researchers deriving the T6 closure step from T4 Recognition and the geometric scale sequence cite this predicate to express the forced departure from the uniform ground state. The definition is introduced directly as an existential statement on the ratio of two entries.
Claim. A configuration $c$ of $N$ positive real ledger entries has $phi$-structure if there exist indices $i,j$ and nonzero integer $n$ such that $c_i / c_j = phi^n$.
background
InitialCondition.Configuration is the structure of N positive real ledger entries with the positivity predicate on each. The StillnessGenerative module starts from the Law of Existence (T5) that the unique zero-defect state is the uniform configuration with all entries equal to 1. Upstream RecognitionForcing supplies the uniqueness of recognition as the extraction mechanism that requires distinguishable states, while PhiForcing supplies the self-similar fixed point phi satisfying phi^2 = phi + 1.
proof idea
The definition is introduced directly as the existential predicate on the configuration entries. It encodes the requirement that a non-trivial entry on a closed geometric scale sequence differs from the ground-state entry 1 by a nonzero power of phi.
why it matters
This predicate is the target of the T6 Closure Theorem in nontrivial_closed_has_phi_structure and of t6_derived, which combine T4 Recognition (non-triviality forced by recognition) with the geometric scale sequence to conclude that every physical configuration has phi-structure. It thereby closes the derivation from T0-T8 without external axioms and feeds the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.