up_quark_pred
The declaration defines the structural mass prediction for the up quark as phi^34 divided by 2 million in MeV. Researchers verifying Recognition Science quark mass ladders against PDG data cite this value when checking structural ratios such as charm to up. The definition is a direct encoding of the rung-4 assignment from the fermion anchor map with zero gap correction.
claimThe structural mass of the up quark is $m_u = phi^{34}/2000000$ MeV, where $phi$ is the golden ratio and the exponent follows from rung 4 in the UpQuark sector with zero gap correction.
background
In the Masses.Verification module, structural mass predictions follow the phi-ladder formula using sector-specific rungs drawn from RSBridge.Anchor. The rung map assigns 4 to the up quark (and 15 to the charm quark), as stated in the upstream RSBridge.Anchor.rung definition. The module quarantines experimental PDG values as imported constants while computing RS-derived predictions directly from phi.
proof idea
One-line definition that applies Constants.phi raised to the natural number 34 and divides by the fixed normalization 2000000. It depends on the imported phi constant and the rung assignment for the up quark sector.
why it matters in Recognition Science
This supplies the up-quark term used in QuarkScoreCardCert to certify ZOf values and charm-up ratios, and in row_charm_up_ratio to establish the structural ratio equals phi^11. It closes the absolute quark-mass row of the scorecard and links to the phi-ladder mass formula in the Recognition Science framework.
scope and limits
- Does not incorporate experimental mass measurements from PDG.
- Does not apply nonzero gap corrections for Z.
- Does not extend to top or down quark sectors.
- Does not derive the exponent 34 from first principles.
formal statement (Lean)
353noncomputable def up_quark_pred : ℝ :=
proof body
Definition body.
354 Constants.phi ^ (34 : ℕ) / 2000000
355
356/-- The charm-quark structural mass (UpQuark sector, rung 15). -/