cert_t
plain-language theorem explainer
The definition supplies the residue certificate for the top quark with rational bounds 18.16 to 18.17. Researchers auditing the Recognition Science mass ladder would cite this datum to check consistency with the phi-ladder predictions at the anchor scale. The construction is a direct record literal with the inequality discharged by normalization.
Claim. The residue certificate for the top quark is the structure with fermion label the top quark, lower bound $1816/100$, upper bound $1817/100$, and the inequality $1816/100 ≤ 1817/100$.
background
A ResidueCert is a structure consisting of a fermion label, rational lower and upper bounds on the gap, and a proof that the lower bound does not exceed the upper bound. This module supplies audit data for fermion residues transported to the anchor scale via RG flow. The certificates are intended to verify the display_identity_at_anchor axiom from AnchorPolicy. Upstream, the ResidueCert structure is defined in both the Masses and RSBridge Anchor modules as a record with fields f, lo, hi, and lo_le_hi.
proof idea
The definition constructs the ResidueCert record directly by assigning the top quark to the fermion field, the rationals 1816/100 and 1817/100 to the bounds, and discharging the inequality lo ≤ hi via the norm_num tactic.
why it matters
This datum contributes to the list of quark certificates, which exhibit variation due to Quarter-Ladder effects as noted in the downstream quarkCerts definition. It forms part of the audit payload that checks the integer-rung model against experimental masses for the top quark, highlighting tension with the theoretical target. In the Recognition framework it supports the verification of the phi-ladder mass formula at the anchor scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.