cert_d
plain-language theorem explainer
cert_d supplies the residue certificate for the down quark with rational bounds 18.75 to 18.76 at the anchor scale. Mass-ladder auditors cite the record when checking experimental data against the gap function in the integer-rung model. The definition is a direct record construction whose single inequality is discharged by normalization.
Claim. The down-quark residue certificate is the record with fermion label $d$, lower bound $1875/100$, upper bound $1876/100$, and proof that $1875/100 ≤ 1876/100$.
background
ResidueCert is the structure that records a fermion label together with rational bounds lo and hi on its gap value at the anchor, together with the proof that lo ≤ hi. The module supplies audit payloads obtained by transporting experimental masses to the anchor scale; each certificate is designed to verify the display_identity_at_anchor axiom from AnchorPolicy. Upstream, ResidueCert is defined as the structure with fields f : Fermion, lo : ℚ, hi : ℚ, lo_le_hi : lo ≤ hi.
proof idea
The definition constructs the record directly: the fermion field is set to d, the bounds are set to the shifted experimental values 18.75 and 18.76, and the ordering constraint is discharged by the norm_num tactic.
why it matters
The certificate is collected into the quarkCerts list that aggregates all quark residues. It contributes to the audit of Quarter-Ladder deviations from the integer-rung model and supports verification of the mass formula on the phi-ladder for D = 3. The entry helps quantify the observed tension between up, charm, and top residues against theoretical targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.