leptonCerts
plain-language theorem explainer
leptonCerts assembles the three individual lepton residue certificates into a single list for use in audit verification. A physicist checking consistency of experimental masses with the integer-rung phi-ladder model would reference this list when confirming the tight clustering around the theoretical gap F(1332) ≈ 13.95. The definition is a direct list construction that enumerates the precomputed cert_e, cert_mu, and cert_tau structures.
Claim. Define the list of lepton residue certificates as the collection containing the electron certificate (bounds $[13.95, 13.96]$), the muon certificate (bounds $[14.03, 14.04]$), and the tau certificate (bounds $[13.89, 13.90]$), where each certificate is a structure holding a fermion, rational lower and upper bounds, and the inequality proof between those bounds.
background
ResidueCert is the structure that records a fermion together with rational bounds lo and hi satisfying lo ≤ hi; these bounds represent the transported experimental residue gap(Z) at the anchor scale. The module supplies the audit payload that verifies the display_identity_at_anchor axiom from AnchorPolicy, with data obtained from RG transport of measured masses. For leptons the certificates are constructed to lie near the theoretical value F(1332) ≈ 13.95, confirming the integer-rung assignment on the phi-ladder.
proof idea
The definition is a direct enumeration that constructs the list by placing cert_e, cert_mu, and cert_tau in order. No lemmas or tactics are invoked beyond the sibling definitions of those three certificates.
why it matters
leptonCerts supplies the lepton half of the complete fermion list allCerts, which concatenates it with the quark certificates. It thereby completes the audit data section of the Residue Certificates module and supports the claim that lepton residues cluster around F(1332), consistent with the integer-rung model. In the Recognition framework this datum anchors the mass formula yardstick · phi^(rung-8 + gap(Z)) for the three leptons whose Z values are fixed at 1332.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.