StabilityCert
plain-language theorem explainer
StabilityCert packages a valid ResidueCert for a given fermion together with a matching proof. Mass-spectrum analysts in Recognition Science cite it when transporting experimental fermion masses to the anchor scale and checking consistency with the integer-rung gap formula. The declaration is a plain structure definition whose three fields directly enforce the required equality and validity conditions.
Claim. For a fermion $f$, a stability certificate consists of a residue certificate $c$ such that $c.f = f$ and $c$ satisfies the validity predicate.
background
The module supplies audit data that bounds the residues of fermions after RG transport to the canonical anchor. Fermion is the inductive type enumerating the twelve standard-model fermions. ResidueCert is the structure holding a fermion label together with rational interval bounds and the proof that the lower bound does not exceed the upper bound. AnchorPolicy supplies the pair $(λ, κ) = (ln φ, φ)$ at which the stationarity axiom display_identity_at_anchor is required to hold. The upstream canonical arithmetic object and Beat synchronization supply the invariant arithmetic and eight-tick structure used to define the anchor scale.
proof idea
The declaration is a structure definition. It introduces the three fields cert, cert_matches and cert_valid with no lemmas, tactics or reduction steps.
why it matters
StabilityCert supplies the concrete audit payload that verifies the display_identity_at_anchor axiom of AnchorPolicy for each fermion. It therefore supports the numerical checks of the mass formula yardstick · φ^(rung-8+gap(Z)) against experimental data inside the RSBridge layer. The module documentation records that the lepton residues cluster near the predicted F(1332) ≈ 13.95 while the charm residue deviates from the up-quark target, leaving an open tension between the quarter-ladder and integer-rung pictures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.