allCerts
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the numerical bounds; they originate from external Python RG transport.
- Does not include certificates for bosons or other particles.
- Does not perform any verification or matching; it only assembles the data list.
- Does not specify the theoretical F(Z) values; those reside in upstream mass modules.
formal statement (Lean)
172def allCerts : List ResidueCert := leptonCerts ++ quarkCerts
proof body
Definition body.
173
174end RSBridge
175end IndisputableMonolith