cert_c
plain-language theorem explainer
This definition records the residue certificate for the charm quark, bounding its anchor-scale value between 13.95 and 13.96 in RS-native units and noting alignment with the lepton gap rather than the up-quark target. Researchers auditing the phi-ladder mass formula against experimental data would cite it when checking the display identity at the anchor. The construction is a direct record literal with a norm_num verification of the bound ordering.
Claim. The charm residue certificate is the record with fermion label $c$, lower bound $13.95$, upper bound $13.96$, and the inequality $13.95 ≤ 13.96$ holding by direct numerical normalization.
background
The module supplies audit payloads of numerical bounds on fermion residues at the anchor scale μ⋆. These bounds verify the display_identity_at_anchor axiom, which requires the integrated RG residue to equal the gap function F(Z) at that scale. The gap is defined as F(Z) = ln(1 + Z/φ) / ln(φ), where φ is the golden ratio fixed point; the module documentation states that charm bounds cluster near F(1332) ≈ 13.95 instead of the up-quark target near 10.7.
proof idea
This is a definition that constructs the ResidueCert record directly. It assigns the charm fermion to the f field, sets the lower bound to 13.95 and upper bound to 13.96, and applies the norm_num tactic to discharge the inequality between those bounds.
why it matters
The certificate is aggregated into the quarkCerts list that collects all quark residues for the full audit. It contributes to verifying the anchor policy for masses and highlights the charm anomaly noted in the module documentation, where the residue matches the lepton gap rather than the expected up-quark value. This touches the open question of Quarter-Ladder effects versus integer-rung structure on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.