cert_u
plain-language theorem explainer
cert_u supplies the residue bounds 11.70 to 11.71 for the up quark at the anchor scale. Researchers auditing Recognition Science mass predictions cite it when comparing quarter-ladder residues to experimental data. The definition is a direct record literal whose only obligation is discharged by a single norm_num call.
Claim. The up-quark residue certificate is the record with fermion field $u$, lower bound $11.70$, upper bound $11.71$, and the inequality $11.70 ≤ 11.71$.
background
ResidueCert is the structure that pairs a fermion with rational bounds on its gap value together with a proof that the lower bound does not exceed the upper bound. The module assembles these certificates from RG-transported experimental masses to test the integer-rung model for leptons and the quarter-ladder model for quarks. Upstream, the same ResidueCert structure is declared in both the Masses.RSBridge.Anchor and RSBridge.Anchor modules.
proof idea
The definition builds the ResidueCert record by direct field assignment for the up fermion and the two rational bounds; the single proof obligation on the inequality is discharged by the norm_num tactic.
why it matters
cert_u is collected into the quarkCerts list that documents the spread among up, charm and top residues. The module uses this spread to highlight quarter-ladder effects that are absent in the lepton certificates. The bounds sit inside the Recognition Science mass formula that places each fermion on the phi-ladder according to its Z value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.