mass_from_phi_ladder
plain-language theorem explainer
The declaration proves the golden ratio exceeds unity. This underpins exponential mass scaling across fermion generations in the three-generation structure derived from the 8-tick cycle in three dimensions. Researchers constructing phi-ladder mass hierarchies would reference the result to justify rung-dependent ratios. The proof is a one-line term application of linear arithmetic to the bound phi greater than 1.5.
Claim. $1 < phi$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The module derives exactly three fermion generations from the 8-tick cycle (period $2^3$) distributed across three spatial dimensions, with generations indexed by bit parity combinations. The phi-ladder places each generation on a distinct rung, producing exponential mass ratios via powers of phi; this requires phi > 1 for the hierarchy to increase with rung number. Upstream, phi_gt_onePointFive supplies the tighter bound (1.5 : R) < phi via the definition of phi and sqrt(5) > 2, while NucleosynthesisTiers.of structures physical quantities on discrete phi-tiers such as nuclear density scaling as phi to a nuclear exponent times Planck density.
proof idea
The proof is a term-mode one-liner that invokes linarith on the lemma phi_gt_onePointFive. This lemma asserts phi > 1.5; linear arithmetic then yields 1 < phi directly from the ordering 1 < 1.5.
why it matters
The inequality supports the mass hierarchy pattern and massRatio constructions in the three-generations module, enabling the exponential rung scaling in the Recognition Science mass formula (yardstick times phi to the power rung minus 8 plus gap(Z)). It aligns with framework landmarks T6 (phi as self-similar fixed point) and T7 (eight-tick octave), and with the module's derivation of three generations from 8 = 2^3 bits in D = 3 space. The result touches the open question of why precisely three generations arise, as stated in the module target of deriving the generation number from RS structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.