cert_c
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the theoretical gap value from the phi-ladder formula.
- Does not supply certificates for leptons or other sectors.
- Does not resolve the physical origin of the charm anomaly.
- Does not incorporate experimental error bars or RG flow details.
formal statement (Lean)
95def cert_c : ResidueCert := {
proof body
Definition body.
96 f := c,
97 -- NOTE: Charm matches Lepton gap (13.95), not Up gap (10.71)!
98 -- This suggests Charm has special structure or the Quarter-Ladder applies.
99 lo := 1395/100,
100 hi := 1396/100,
101 lo_le_hi := by norm_num
102}
103