lepton_mass_increasing
plain-language theorem explainer
The declaration establishes that the golden ratio raised to the 11th and 6th powers both exceed 1, confirming mass ratios increase across lepton generations on the phi-ladder. Researchers deriving fermion masses from the Recognition Science forcing chain cite this when verifying the geometric ordering of electron, muon, and tau. The proof is a direct term-mode construction applying the one_lt_zpow₀ lemma twice to the base fact 1 < phi.
Claim. The golden ratio satisfies $phi^{11} > 1$ and $phi^{6} > 1$.
background
The module formalizes P-002, the fermion mass hierarchy from the phi-ladder: each fermion occupies a rung n with mass proportional to phi^n. Because phi > 1 the hierarchy spans orders of magnitude, with phi^11 approximately 200 and phi^17 approximately 2200. The upstream lemma one_lt_phi states 1 < phi and is proved in Constants via the quadratic definition of the golden ratio, with equivalent statements appearing in PhiSupport and its Lemmas submodule.
proof idea
The term proof builds the conjunction as a pair of one_lt_zpow₀ applications. Each instance takes the known inequality 1 < phi together with a positive integer exponent (11 or 6) whose positivity is discharged by norm_num.
why it matters
This inequality anchors the lepton mass ordering inside the P-002 derivation and the broader phi-ladder construction of Recognition Science. It follows directly from the self-similar fixed point phi (T6) and the eight-tick octave structure, ensuring successive generations sit on higher rungs and therefore carry larger masses. No downstream theorems are recorded yet, but the result closes a prerequisite for any geometric mass progression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.