allCerts
plain-language theorem explainer
This definition assembles the complete list of residue certificates for all fermions by concatenating the lepton subset with the quark subset. An auditor checking mass transport to the anchor scale would cite the resulting list when verifying the full set of gap bounds against the display_identity_at_anchor axiom. The construction is a direct list concatenation of two sibling definitions.
Claim. Let $allCerts$ denote the list obtained by concatenating the lepton residue certificates with the quark residue certificates, where each $ResidueCert$ is a structure containing a fermion identifier together with rational bounds $lo$ and $hi$ satisfying $lo ≤ hi$.
background
The Residue Certificates module supplies audit data for fermion masses transported to the anchor scale. Each $ResidueCert$ pairs a Fermion with rational lower and upper bounds on its gap value, satisfying the ordering condition $lo ≤ hi$. The module is designed to support verification of the display_identity_at_anchor axiom imported from AnchorPolicy, which requires that the transported gap(Z) lies within the supplied bounds at the anchor point.
proof idea
The definition is a one-line wrapper that concatenates the pre-defined leptonCerts list with the quarkCerts list using the standard append operator.
why it matters
This definition supplies the complete audit payload that feeds the AnchorPolicy verification step. It aggregates lepton certificates (clustering near F(1332) ≈ 13.95) and quark certificates (showing Quarter-Ladder variation) so the full experimental bounds can be checked against the phi-ladder predictions of the Recognition Science framework. The module documentation positions it as the single list needed to audit all fermions against the integer-rung model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.