StandardModelMassPDGEmpiricalSurface
plain-language theorem explainer
Packages the PDG charged-lepton masses (electron 0.511 MeV, muon 105.66 MeV, tau 1776.9 MeV) and the mu/e ratio near 206.8 as an empirical Prop surface. Mass-ladder and T6-bridge authors cite it to keep laboratory inputs separate from theorem-grade forcing. The structure is pure data encoding: equalities and one absolute-value bound, no derivation.
Claim. A proposition asserting that the encoded PDG electron, muon, and tau masses equal $0.511$, $105.66$, and $1776.9$ MeV respectively, that the mu/e ratio is defined as the muon mass over the electron mass, and that this ratio satisfies $|\mu/e - 206.8| < 1$.
background
The Unified Forcing Chain module aims to show T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration, not as free postulates. Mass phenomenology sits downstream of T6 (φ forced as the self-similar fixed point): the canonical mass law is yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$ on the φ-ladder.
PDG lepton masses live in the SM verification layer as plain real constants: electron $0.511$ MeV, muon $105.66$ MeV, tau $1776.9$ MeV, with the mu/e ratio defined as their quotient. Those defs are laboratory bookkeeping, not consequences of the cost functional $J$.
This structure gathers those equalities (and a loose ratio bound) into one Prop so the forcing chain can name “empirical surface” without smuggling data into axioms. The module doc’s stronger claim is complete inevitability of the chain; empirical masses remain inputs against which the ladder is checked.
proof idea
No proof body: this is a structure of type Prop. Each field is a named hypothesis-shaped equality or inequality over the SM-verification PDG constants. Instantiation is by reflexivity on those defs plus a numeric check of the ratio bound, as in the companion theorem that builds an inhabitant by rfl on the four equalities.
why it matters
Keeps PDG lepton data explicitly empirical so the complete inevitability chain does not treat lab numbers as forcing axioms. The companion theorem states the encoded surface “is empirical data, not an extra forcing axiom,” and discharges the structure by reflexivity.
The T6-to-canonical-mass-ladder bridge consumes this surface: after T6 fixes φ, the bridge certifies the master formula rung - 8 + gap(Z), φ-scaling under rung shift, uniqueness under gap-equivalent assignments, and SM fermion masses routed through that formula. Without a clean empirical interface, ladder checks would blur data and derivation.
Framework landmarks: T6 φ-forcing and the mass formula on the φ-ladder. This declaration does not force masses; it walls off the PDG inputs the ladder is compared against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.