cert_b
plain-language theorem explainer
The bottom-quark residue certificate supplies the interval 15.86 to 15.87 on gap(b) at the RS anchor scale. Particle physicists checking the phi-ladder mass formula against experimental bottom mass would cite this datum when testing consistency with the integer-rung prediction. The definition is a direct record literal whose only non-trivial field is discharged by a one-line norm_num tactic.
Claim. The residue certificate for the bottom quark is the record structure with fields $f = b$, $lo = 15.86$, $hi = 15.87$, and a witness that $lo ≤ hi$, where $b$ is the bottom-quark label and the bounds are expressed in RS-native units at the anchor scale.
background
This module supplies audit payloads of numerical bounds on fermion residues obtained by transporting experimental masses to the anchor scale via RG flow. ResidueCert is the record type that packages a fermion label, an interval [lo, hi] on the gap function, and a proof that lo ≤ hi. The module setting links these certificates to the display_identity_at_anchor axiom of AnchorPolicy, which requires the certified gap(Z) to match the theoretical F(Z) value at the canonical anchor.
proof idea
The definition constructs the ResidueCert record by direct field assignment: f set to the bottom label b, lo and hi set to the rationals 1586/100 and 1587/100, and the ordering field discharged by the norm_num tactic.
why it matters
This certificate is aggregated into the quarkCerts list that collects all fermion audit data. It quantifies the Quarter-Ladder deviation for the bottom quark, whose residue interval lies away from the lepton-cluster value near 13.95. In the Recognition framework it supplies the empirical gap(Z) input required by the mass formula yardstick · phi^(rung − 8 + gap(Z)) and supports the T5–T8 forcing chain by providing the numerical test points needed to confront the phi-ladder with observation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.