up_quark_pred
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.