downquark_sector_params
plain-language theorem explainer
The theorem fixes the down-quark sector parameters at B_pow equal to 23 and r0 equal to -5 for the Recognition Science mass formula. Researchers matching predicted quark masses to PDG values would cite this choice when constructing verification certificates. The proof is a one-line term that directly pairs the two sector-specific equalities already established in the Anchor module.
Claim. $B_ {pow}(DownQuark) = 23$ and $r_0(DownQuark) = -5$, where these parameters enter the down-quark mass expression $m = 2^{23} phi^{-10 + r} / 10^6$ MeV for rung integer $r$.
background
In the QuarkVerification module each quark mass is expressed as a phi-power divided by a sector-dependent scale, with the formulas fixed by cube geometry and containing no free parameters. For the down sector the mass formula reads $m(DownQuark, r) = 2^{23} phi^{-10 + r} / 10^6$ MeV; the constants B_pow and r0 supply the 2-power and the base rung offset respectively. The Quark inductive type distinguishes the six flavors, while the Mass type is simply the reals; upstream lemmas from Anchor supply the concrete equalities B_pow_DownQuark_eq and r0_DownQuark_eq.
proof idea
The proof is the one-line term exact ⟨B_pow_DownQuark_eq, r0_DownQuark_eq⟩. It constructs the required conjunction by direct appeal to the two defining equalities already proved for the down-quark case in the Anchor module; no additional tactics or reductions are applied.
why it matters
This declaration supplies the down-sector parameters to the parent theorem quark_verification_cert_exists, which packages rung spacing, both sector parameter pairs, and mass positivity into a single verification certificate. It completes the structural half of the phi-ladder mass formula for down-type quarks, consistent with the eight-tick octave and D = 3 geometry of the Recognition framework. The result touches the T5 J-uniqueness step by fixing the concrete exponents that appear in the mass expression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.