cert_s
The definition records the residue certificate for the strange quark with lower bound 13.96 and upper bound 13.97 on the anchor scale. Researchers auditing the phi-ladder mass predictions against experimental fermion data would cite this entry together with the lepton certificates. The construction directly populates the ResidueCert structure and applies norm_num to confirm the bound ordering.
claimThe strange quark residue certificate is the structure with fermion field $s$, lower bound $1396/100$, upper bound $1397/100$, and the inequality $1396/100 ≤ 1397/100$.
background
ResidueCert packages a fermion identifier with rational interval bounds and the ordering constraint lo ≤ hi. This module supplies the audit payload of numerical bounds obtained by transporting experimental masses to the anchor scale. The certificates verify the display_identity_at_anchor axiom from AnchorPolicy. Upstream result: structure ResidueCert where f : Fermion, lo : ℚ, hi : ℚ, lo_le_hi : lo ≤ hi.
proof idea
The definition is a direct instantiation of the ResidueCert structure. It assigns the strange quark to the fermion field, sets the rational bounds 1396/100 and 1397/100, and applies the norm_num tactic to discharge the inequality.
why it matters in Recognition Science
This certificate enters the quarkCerts collection that documents variation among up, charm, top, down, strange, and bottom quarks. It contributes to the audit verifying the mass formula against the phi-ladder and highlights the charm anomaly where the charm residue matches the lepton gap rather than the up-quark target. The entry supports verification of the display_identity_at_anchor axiom.
scope and limits
- Does not derive the numerical bounds from the Recognition Composition Law.
- Does not establish that the residue equals the theoretical gap function F(Z).
- Does not resolve the observed tension between up and top quark residues.
- Does not claim the bounds hold outside the anchor scale.
Lean usage
quarkCertsformal statement (Lean)
118def cert_s : ResidueCert := {
proof body
Definition body.
119 f := s,
120 lo := 1396/100, -- 13.96
121 hi := 1397/100,
122 lo_le_hi := by norm_num
123}
124