mass_summary
plain-language theorem explainer
Human-readable string summarizing Recognition Science lepton mass-ratio predictions against PDG values. It records the simple integer φ-ladder model (φ^11, φ^17) and the geometry-corrected steps that bring μ/e and τ/e into sub-percent agreement. Anyone auditing the quarantined MassComparison module cites it as the narrative status board. The body is pure string concatenation; there is no mathematical proof.
Claim. A fixed report string that states: under the simple integer model, $m_\mu/m_e \approx \varphi^{11}$ and $m_\tau/m_e \approx \varphi^{17}$; under the full model with geometry corrections $\mathrm{step}_{e\to\mu}=E_{\mathrm{passive}}+1/(4\pi)-\alpha^2$ and $\mathrm{step}_{\mu\to\tau}=\mathrm{Faces}-(2W+3)\alpha/2$, the predicted ratios match experiment to roughly $10^{-6}$ (muon) and $10^{-4}$ (tau).
background
The enclosing module compares Recognition Science mass predictions to PDG 2024 data and is explicitly quarantined from the certified surface: it imports experimental numbers and depends on the φ-ladder anchor system. The RS mass formula is $m(\mathrm{species})=\mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$, with yardstick built from coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers from cube geometry.
Electron mass in RS units sits on rung 2: $m_e=E_{\mathrm{coh}}\cdot\varphi^2$. Lepton generation structure and species tables (muon mass scale, DOF counts) supply the experimental anchors quoted in the summary. The integer rungs 11 and 17 are the cube-geometry baseline; the summary’s “full model” adds the spherical solid-angle term $1/(4\pi)$ and a one-loop fine-structure self-energy $-\alpha^2$.
proof idea
No proof. The declaration is a String definition assembled by successive ++ of fixed multiline literals. It hard-codes the numerical claims (φ^11 ≈ 199, corrected φ^11.0795 ≈ 206.768, etc.) as documentation text rather than evaluating Lean terms or citing theorems at runtime.
why it matters
Gives auditors a single narrative snapshot of how close the φ-ladder lepton ratios sit to experiment once geometry corrections are included. It sits in Verification.MassComparison, outside the certified kernel, so it does not feed proved theorems (no downstream uses). Framework landmarks it echoes: the mass formula on the φ-ladder, coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$, and the role of cube geometry in fixing integer rungs (linked to the eight-tick / D=3 forcing chain). It does not close any open Lean obligation; it only records the claimed numerical status of the full model (~0.0001% muon agreement).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.