massRatiosDefault
plain-language theorem explainer
Canonical lepton mass ratios at the RecogSpec level are the triple $(\varphi,\,\varphi^{-2},\,\varphi^{-1})$ for $\mu/e$, $\tau/e$, and $\tau/\mu$. Spec and exclusivity authors cite this when packing dimensionless observables or asserting that mass ratios are $\varphi$-closed. The body is a one-line structure constructor, marked simp, and is flagged as a legacy placeholder.
Claim. For any real $\varphi$, the default lepton-sector mass-ratio payload is $\mu/e=\varphi$, $\tau/e=\varphi^{-2}$, and $\tau/\mu=\varphi^{-1}$.
background
RecogSpec packages dimensionless observables that a recognition ledger and bridge are expected to match. Among them is a lepton-sector payload: three real numbers for the inter-generation mass ratios $\mu/e$, $\tau/e$, and $\tau/\mu$.
The upstream structure LeptonMassRatios is exactly that triple of reals, with no further constraints in the type. The golden ratio $\varphi$ (forced as the self-similar fixed point in the T6 step of the forcing chain) is the natural scale for RS mass ladders: masses sit on a $\varphi$-power yardstick of the form yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$.
This definition supplies the canonical, spec-level choice of those three ratios as pure $\varphi$-powers. The module doc marks it CERT(definitional) and a legacy placeholder, so it is a fixed packing convention rather than a derived mass-spectrum theorem.
proof idea
Pure definition: the structure is inhabited by the triple constructor $\langle\varphi,,1/\varphi^{2},,1/\varphi\rangle$. No lemmas are applied. The @[simp] attribute makes the three field projections reduce definitionally in later packs and certificates.
why it matters
This is the mass-ratio slot inside the explicit universal dimensionless pack and the matching witness: both dimlessPack_explicit and UD_explicit set their mass-ratio fields to this default. Downstream exclusivity structure DerivesObservables hard-codes the first component as a mass-prediction clause ($\mu/e=\varphi$ for every $\varphi$), and HonestClosureCert treats $\varphi$-closed algebraic observables as Part A of honest framing.
In the broader RS picture it is the lightweight stand-in for lepton ratios on the $\varphi$-ladder (primer mass formula), not a substitute for the full rung-and-gap derivation. It lets verification and exclusivity layers talk about mass ratios before the detailed spectrum theorems are wired in. Open question it leaves: replacing the legacy powers with the actual rung/gap predictions while keeping the same payload type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.