quark_verification_cert_exists
plain-language theorem explainer
Existence of a QuarkVerificationCert is established by direct construction, bundling verified rung spacings for up and down quark generations, sector parameters for the mass formulas, and positivity of all computed masses. A researcher auditing the RS quark mass ladder against PDG data would cite this to confirm the certificate is inhabited. The proof proceeds by term construction, assembling the structure from four upstream theorems on spacings and parameters.
Claim. There exists a certificate $C$ such that $r_ {up}(c) - r_{up}(u) = 11$ and $r_{up}(t) - r_{up}(u) = 17$, $r_{down}(s) - r_{down}(d) = 11$ and $r_{down}(b) - r_{down}(d) = 17$, $B_{pow}(UpQuark) = -1$ and $r_0(UpQuark) = 35$, $B_{pow}(DownQuark) = 23$ and $r_0(DownQuark) = -5$, and $0 < m(s,r)$ for all sectors $s$ and rungs $r$, where $m$ denotes the RS mass in MeV.
background
The module formalizes RS quark mass predictions against PDG values, with experimental inputs treated as quarantined constants. QuarkVerificationCert is the structure that packages rung spacings (generation differences of 11 and 17), sector parameters $B_{pow}$ and $r_0$ for the two sectors, and the global positivity condition on $rs_mass_MeV$. The up-sector formula is $m = 2^{-1} phi^{-5} phi^{35} phi^r / 10^6$ MeV; the down-sector formula is $m = 2^{23} phi^{-10+r} / 10^6$ MeV, with rungs taken from Anchor (u,c,t at 4,15,21 and d,s,b at 4,15,21). Upstream results supply the concrete spacing theorems (proved by decide in QuarkScoreCard and by omega on anchor edges in this module) together with the sector-parameter equalities and the positivity theorem obtained by unfolding $rs_mass_MeV$ and applying positivity of multiplication and division.
proof idea
The proof is a one-line term construction that builds the QuarkVerificationCert record by substituting the four upstream theorems up_generation_spacing, down_generation_spacing, upquark_sector_params, downquark_sector_params, and quark_mass_positive into the respective fields of the structure.
why it matters
The theorem certifies that the structural constraints required for the quark mass verification certificate are satisfied inside the Recognition Science framework. It closes the local check that the phi-ladder rung assignments and sector parameters produce strictly positive masses, consistent with the T5 J-uniqueness and T6 phi fixed-point steps that fix the mass yardstick. With no downstream uses recorded, the result functions as a terminal verification artifact for the quark sector, leaving open the question of how the specific rung integers and $B_{pow}$ values are ultimately derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.