standard_model_mass_pdg_empirical_surface
plain-language theorem explainer
PDG lepton masses (electron, muon, tau) and the muon-to-electron ratio are packaged as an empirical surface certificate, not as forcing axioms. Anyone wiring the T6 mass ladder to Standard Model fermion checks cites this. The proof is a structure inhabitant: four fields by definitional equality, one by an existing numerical approximation lemma.
Claim. The encoded PDG surface holds: $m_e = 0.511\,\mathrm{MeV}$, $m_\mu = 105.66\,\mathrm{MeV}$, $m_\tau = 1776.9\,\mathrm{MeV}$, the ratio $m_\mu/m_e$ is defined as that quotient, and the ratio satisfies the stated numerical approximation. These equalities are empirical encodings, not extra axioms of the forcing chain.
background
The Unified Forcing Chain module shows T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T6 forces $\varphi$ as the self-similar fixed point of the discrete ledger; the mass ladder then uses the master exponent $\mathrm{rung}-8+\mathrm{gap}(Z)$ with $\varphi$-scaling under rung shift.
The structure certified here isolates PDG lepton numbers as empirical inputs. Its fields assert that the encoded electron, muon, and tau masses equal $0.511$, $105.66$, and $1776.9$ MeV, that the muon-to-electron ratio is their quotient, and that the ratio meets a fixed numerical check. Doc-comment: "PDG values are encoded as empirical inputs, separated from theorem-grade mass forcing."
In RS-native units mass is a real; the ladder formula is yardstick times $\varphi$ to the rung-gap exponent. This surface does not force those numbers from cost; it only records them so the bridge can route SM fermions through the same master formula without smuggling data into the axiom bundle.
proof idea
Term-mode inhabitant of the empirical-surface structure. Four fields (electron_value_encoded, muon_value_encoded, tau_value_encoded, mu_e_ratio_definition) are closed by rfl: they are definitional equalities against the encoded PDG constants and the ratio definition. The remaining field mu_e_ratio_approx is supplied by the existing lemma Masses.SMVerification.pdg_mu_e_ratio_approx. No tactic search and no new arithmetic; pure structure assembly.
why it matters
Feeds the parent theorem t6_to_canonical_mass_ladder_bridge_holds, whose doc states: "T6 supplies the canonical Mass Ladder bridge." That bridge packages $\varphi$-uniqueness from T6, the canonical mass-law formula, rung spacing by $\varphi$, uniqueness under gap-equivalent rung assignments, and SM fermion masses routed through the same master formula.
Without this certificate the bridge would either hard-code PDG numbers inside theorem-grade forcing or leave the SM surface unstated. The separation matches the module's stronger claim: constants and ladder structure are forced from RCL + normalization + calibration; measured lepton masses remain data. Landmark contact is T6 ($\varphi$ forced) and the mass formula yardstick $\cdot\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$. No open scaffold: claim status is proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.