QuarkVerificationCert
plain-language theorem explainer
QuarkVerificationCert assembles rung spacings of 11 and 17, sector constants B_pow and r0, and mass positivity into a single record for the RS quark spectrum. Researchers comparing Recognition Science mass predictions to PDG data would cite the record when confirming generation structure on the phi-ladder. The declaration is a direct structure definition that records values supplied by the Anchor module.
Claim. A structure certifying quark mass verification consisting of: rung_spacing_up asserting $r_ {up}(c) - r_{up}(u) = 11$ and $r_{up}(t) - r_{up}(u) = 17$, rung_spacing_down with the analogous conditions for down-type quarks, sector_params_up requiring $B_{pow}(UpQuark) = -1$ and $r_0(UpQuark) = 35$, sector_params_down with $B_{pow}(DownQuark) = 23$ and $r_0(DownQuark) = -5$, and all_masses_positive asserting that rs_mass_MeV$(s,r) > 0$ for all sectors and rungs.
background
In Recognition Science, quark masses sit on the phi-ladder via the formula $m = 2^{B_{pow}} phi^{-5} phi^{r_0 + r} / 10^6$ MeV. The Anchor module derives the sector constants from cube edge counting and wallpaper geometry: B_pow(UpQuark) = -1 with r0(UpQuark) = 35, and B_pow(DownQuark) = 23 with r0(DownQuark) = -5. Rung assignments are u,d at rung 4, c,s at 4 + tau(1) = 15, t,b at 4 + tau(2) = 21, where tau increments are 11 and 17. The module treats PDG 2024 values as external constants and quarantines the comparison.
proof idea
The declaration is a structure definition that directly records the five fields. No tactics or lemmas are applied; the fields are populated by the sibling definitions up_generation_spacing, down_generation_spacing, upquark_sector_params, downquark_sector_params, and quark_mass_positive.
why it matters
The structure supplies the concrete data record consumed by the existence theorem quark_verification_cert_exists, which constructs a Nonempty instance to certify that the RS mass ladder reproduces the observed quark generation pattern. It closes the verification loop for the mass formula in the quark sectors, linking the phi-ladder rung assignments to the numerical predictions. The open question it touches is the precise mapping of experimental uncertainties onto the RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.