upquark_sector_params
plain-language theorem explainer
The declaration fixes the up-quark sector constants B_pow = -1 and r0 = 35 for use in the RS mass formula. Researchers comparing predicted quark masses to PDG data would reference this to anchor the up-type sector before rung calculations. It is established by a direct application of the two sector-specific equality theorems proved in the Anchor module.
Claim. In the Recognition Science mass model the up-quark sector satisfies $B_ {pow}(UpQuark) = -1$ and $r_0(UpQuark) = 35$.
background
The QuarkVerification module imports experimental PDG values solely for comparison; they are not derived inside RS. The up-quark mass formula is given as $m(UpQuark,r) = 2^{-1} phi^{-5} phi^{35} phi^r / 10^6$ MeV, which simplifies to $phi^{30+r}/(2 times 10^6)$ MeV once the sector parameters are inserted. B_pow is the function Sector to Z that records derived powers of two obtained from cube edge counting; r0 is the companion function that records phi-exponent offsets obtained from wallpaper groups plus cube geometry.
proof idea
The proof is a one-line wrapper that applies the lemmas B_pow_UpQuark_eq and r0_UpQuark_eq via the exact tactic to build the required conjunction.
why it matters
This theorem supplies the up-quark sector parameters to the construction of QuarkVerificationCert, which packages rung spacings, both sector parameter pairs, and the positivity check. It therefore occupies the parameter slot for up-type quarks (rungs 4, 15, 21) inside the phi-ladder mass formula. The numerical values themselves originate in the geometric derivations of the Anchor module and ultimately trace to the eight-tick octave and spatial dimension count of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.