cert_tau
plain-language theorem explainer
cert_tau defines the ResidueCert for the tau lepton with rational bounds 13.89 to 13.90. Mass-spectrum auditors in Recognition Science cite it when checking lepton clustering against the integer-rung prediction near F(1332). The definition directly instantiates the ResidueCert record and applies norm_num to discharge the bound inequality.
Claim. The tau residue certificate is the structure with fermion component $f = $ tau lepton, lower bound $lo = 13.89$, upper bound $hi = 13.90$, and the inequality $lo ≤ hi$ proved by normalization.
background
ResidueCert is the structure with fields f : Fermion, lo : ℚ, hi : ℚ and lo_le_hi : lo ≤ hi. It packages numerical bounds on the gap function at the anchor scale. From AnchorPolicy, F(Z) := log(1 + Z/φ) / log(φ) is the display function that these certificates are designed to bound. The module supplies audit payloads obtained by RG transport of experimental masses; lepton certificates are expected to cluster near the theoretical value F(1332) ≈ 13.95.
proof idea
One-line record construction that supplies the fermion tau, the explicit rationals 1389/100 and 1390/100, and invokes the norm_num tactic to prove the inequality between them.
why it matters
cert_tau is collected into leptonCerts together with cert_e and cert_mu. That list verifies the integer-rung model for leptons against the anchor axiom in AnchorPolicy. Within the Recognition Science chain it supplies concrete data for the phi-ladder mass formula and the T5 J-uniqueness step that forces the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.