quarkCerts
plain-language theorem explainer
The definition assembles the six individual residue certificates for the up, charm, top, down, strange, and bottom quarks into one list. Researchers auditing mass spectra against the phi-ladder in the Recognition framework cite this when aggregating fermion data to check the display_identity_at_anchor condition. The construction is a direct enumeration of the six precomputed certificate structures.
Claim. Let $C_f$ denote the ResidueCert structure for quark flavor $f$, each consisting of a fermion label together with rational lower and upper bounds on the residue gap and a proof that the lower bound is at most the upper bound. The list of quark residue certificates is then defined as $[C_u, C_c, C_t, C_d, C_s, C_b]$.
background
ResidueCert is the structure type that pairs a fermion label with rational lower and upper bounds on its residue together with a proof that the lower bound does not exceed the upper bound. This module supplies the audit payload of numerical bounds obtained by transporting experimental masses to the anchor scale via RG flow. The module documentation notes that quark certificates exhibit more variation than leptons because of Quarter-Ladder effects, with charm matching the lepton gap near 13.95 rather than the up-quark target near 10.7.
proof idea
The definition is a direct list construction that enumerates the six quark certificates cert_u, cert_c, cert_t, cert_d, cert_s, and cert_b, each of which is itself a structure literal carrying explicit rational bounds and a norm_num proof of the inequality.
why it matters
This definition supplies the quark component of the allCerts aggregation that concatenates leptonCerts with the quark list to give complete fermion coverage. It records the observed tension between experimental residues and the theoretical F(Z) targets on the phi-ladder, including the charm anomaly and the spread between up and top values. In the Recognition framework the list supports verification of the display_identity_at_anchor axiom at the anchor scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.