cert_c
plain-language theorem explainer
This definition supplies the numerical bounds for the charm quark residue at the anchor scale. A physicist auditing mass spectra against the Recognition gap function would cite it when checking the charm anomaly against lepton clustering. The definition is a direct record construction that hardcodes the interval derived from RG transport and proves the ordering by normalization.
Claim. The charm residue certificate is the record with particle identifier $c$, lower bound $13.95$, upper bound $13.96$, and the ordering $13.95 \le 13.96$ established by arithmetic normalization.
background
Residue certificates supply the audit payload of numerical bounds on residues obtained by transporting experimental masses to the anchor scale. The gap function is the closed-form expression $\mathcal{F}(Z) = rac{ ext{Real.log}(1 + Z/ ext{phi})}{ ext{Real.log}( ext{phi})}$, which the integrated RG residue is required to match at the anchor. The module stores these certificates to verify the display_identity_at_anchor axiom from AnchorPolicy.
The charm certificate is one of several sibling records (electron, muon, tau, up, down, etc.) that bound $ ext{gap}(Z)$ for each fermion. Upstream gap definitions appear in Masses.RSBridge.Anchor and Masses.AnchorPolicy; the Lepton inductive type enumerates the lepton species whose residues cluster near 13.95.
proof idea
This is a definition that constructs the ResidueCert record by direct field assignment: particle identifier set to charm, lower and upper bounds set to the decimal fractions 1395/100 and 1396/100, and the ordering proved by the norm_num tactic.
why it matters
The certificate is collected into the quarkCerts list that enumerates all fermion residues. It records the charm anomaly in which the measured residue matches the lepton gap $ ext{F}(1332) hickapprox 13.95$ rather than the up-quark target $ ext{F}(276) hickapprox 10.7$, thereby quantifying the tension between Quarter-Ladder and Integer-Rung models inside the Recognition mass formula. The datum feeds the broader audit that checks whether every fermion residue equals its theoretical gap at the anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.