r_charm
The definition assigns the natural number 15 as the RS rung index for the charm quark in the up-type second-generation sector formula. Researchers comparing structural mass predictions to PDG data cite this rung when anchoring the gap-corrected formula at the M_Z scale before two-loop QCD running. The assignment is a direct constant definition with no computation or lemmas.
claimThe RS rung index for the charm quark (up-type, generation 2) in the sector formula is the natural number 15.
background
In the Recognition Science framework the mass formula places a quark on the phi-ladder via yardstick times phi to the power (rung minus 8 plus gap(Z)). The CharmMSBarScoreCard module uses rung 15 for charm to state the structural prediction at the M_Z anchor, then applies two-loop alpha_s and mass anomalous dimension running to reach the m_c scale for comparison with the PDG value 1.27 GeV. Upstream, scale(k) is defined as phi^k, supplying the phi-power basis, while the canonical arithmetic object ensures the natural-number rung is realization-independent.
proof idea
This is a direct definition that assigns the literal natural number 15 to r_charm. No lemmas or tactics are applied; the value is supplied exactly as the RS rung for charm stated in the module documentation.
why it matters in Recognition Science
The definition supplies the rung_eq_15 field required by the CharmMSBarCert structure, which certifies that the RS-predicted charm mass after two-loop running lies inside the PDG band. It implements the sector rung step in the mass formula, consistent with the phi-ladder scaling and the eight-tick octave of the forcing chain. The specific choice of 15 places the gap-corrected prediction inside the empirical interval once the massAtAnchor derivation is evaluated at the canonical yardstick.
scope and limits
- Does not derive the rung value 15 from the J-uniqueness condition or Recognition Composition Law.
- Does not evaluate the gap correction or yardstick scaling for charm.
- Does not execute the two-loop alpha_s or mass anomalous dimension running.
- Does not address rungs for other quark flavors or generations.
- Does not claim the rung assignment holds in every possible realization.
Lean usage
import IndisputableMonolith.Physics.CharmMSBarScoreCard example : r_charm = 15 := rflformal statement (Lean)
47def r_charm : ℕ := 15
proof body
Definition body.
48
49/-- A reference RS-anchored charm mass at the M_Z scale, used as the input
50 `m_0` for two-loop mass running.
51
52 NOTE: this value is not derived in this module from first principles;
53 the structural derivation is in `Masses.RSBridge.Anchor.massAtAnchor`
54 via the gap-corrected formula. The numerical value here is the `massAtAnchor`
55 output evaluated at the canonical RS yardstick. -/