cert_tau
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the numerical bounds from raw experimental data.
- Does not prove that the interval contains the exact theoretical F(1332).
- Does not address the Quarter-Ladder tension observed in quark residues.
- Does not extend to higher-generation or composite states.
Lean usage
example : cert_tau ∈ leptonCerts := by simp [leptonCerts]formal statement (Lean)
76def cert_tau : ResidueCert := {
proof body
Definition body.
77 f := tau,
78 lo := 1389/100, -- 13.89
79 hi := 1390/100, -- 13.90
80 lo_le_hi := by norm_num
81}
82
83/-! ## Quark Certificates
84 Quarks show the Quarter-Ladder vs Integer-Rung tension.
85 Theoretical target: F(276) ≈ 10.71 (up) or F(24) ≈ 5.74 (down)
86-/
87