mass_ladder_holds
plain-language theorem explainer
The lemma shows that the charged-lepton mass ladder assumption directly yields the phi-based ladder matching imported PDG measurements within stated errors. Modelers of particle mass hierarchies via self-similar scaling would cite it for the surrogate construction. The proof is a direct one-line application of the hypothesis.
Claim. If every imported measurement $m$ satisfies $|m.value - phi^{rung(m)}| ≤ m.error$, then the same bound holds for the phi-ladder matching property under base $phi$.
background
Recognition Science places particle masses on a phi-ladder whose rungs are integer powers of the golden ratio phi, the self-similar fixed point forced by the J-uniqueness relation. The Masses.Basic module supplies a surrogate model restricted to charged leptons. The Constants structure from LawOfExistence bundles the framework parameters, including phi. The mass_ladder_assumption encodes the claim that imported data already lie within error of the phi-powered rung values. The mass_ladder_matches_pdg predicate states the identical bound for an arbitrary base.
proof idea
This is a one-line wrapper that applies the mass_ladder_assumption hypothesis directly.
why it matters
The lemma connects the imported-data assumption to the explicit matching predicate inside the masses module, thereby anchoring the phi-ladder surrogate for charged leptons. It supports the mass formula that assigns values via phi to the power of rung minus offset. No downstream results are recorded, so its role in extending the ladder to other families remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.