cert_mu
plain-language theorem explainer
cert_mu records the muon residue bounds as the interval from 14.03 to 14.04 in anchor units. Researchers auditing lepton masses on the Recognition Science ladder would cite this certificate when checking consistency with the integer-rung prediction near F(1332). The definition is a direct record construction that applies norm_num to confirm the interval is non-empty.
Claim. The muon residue certificate is the structure with fermion field equal to the muon, lower bound $1403/100$, upper bound $1404/100$, and the inequality $1403/100 ≤ 1404/100$.
background
ResidueCert is a structure that packages a fermion identifier with rational lower and upper bounds on its residue together with a proof that the lower bound does not exceed the upper bound. The scalar mu from the Ndim projector is the coefficient in the quadratic relation A² = μ A. This module supplies audit data derived from experimental masses transported to the anchor scale via RG flow, intended to verify the display_identity_at_anchor axiom from AnchorPolicy.
proof idea
The definition constructs the ResidueCert record by setting the fermion field to the muon, the bounds to 1403/100 and 1404/100, and discharging the inequality with the norm_num tactic.
why it matters
This certificate is included in the leptonCerts list that groups the electron, muon, and tau residues. It supports the module observation that lepton residues cluster near the theoretical gap F(1332) ≈ 13.95, consistent with the integer-rung model in the Recognition Science mass formula. The numerical values originate from Python RG transport of experimental data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.