PhiLadder
plain-language theorem explainer
The φ-ladder is the set of all positive reals of the form φ^n where n ranges over the integers and φ denotes the golden ratio. Researchers deriving quantized spectra from J-cost minimization in self-similar systems cite this set when constructing discrete energy levels or mass gaps. The declaration is a direct set comprehension that encodes the fixed-point condition without invoking lemmas or additional hypotheses.
Claim. Let φ be the golden ratio. The φ-ladder is the set {φ^n | n ∈ ℤ}.
background
The φ-Emergence module derives the golden ratio from J-cost minimization under self-similarity. J-cost quantifies local deviation from minimality for a positive real position x, with stability requiring the ratio condition r² = r + 1 whose unique positive solution is φ. A position x > 0 is stable precisely when its J-cost attains a local minimum, which forces membership in the discrete spectrum generated by integer powers of φ.
proof idea
The declaration is a direct definition by set comprehension over integer exponents. No lemmas are applied; the body simply states the membership predicate. Separate sibling theorems later establish closure under multiplication and division by φ using the integer exponent addition rules.
why it matters
This definition supplies the discrete spectrum required by the hypothesis that stable positions coincide exactly with the φ-ladder. It is invoked in the spacetime emergence certificate to bound the mass gap and in Yang-Mills mass gap arguments to establish non-negativity of bond costs. Within the Recognition framework it realizes the step where φ is forced as the self-similar fixed point, enabling the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.