QuarkAbsoluteBridgeScoreCardCert
plain-language theorem explainer
QuarkAbsoluteBridgeScoreCardCert packages four exact ratio agreements between structural quark mass predictions and the Recognition Science anchor masses, plus the naming of the absolute bridge residual. A researcher verifying the phi-ladder mass formula against measured quark hierarchies would cite this certificate when checking within-family ratios for the up sector and down-sector power laws. The definition is a plain record that bundles the equalities without further computation.
Claim. The certificate structure asserts that the ratio of structural charm to up quark predictions equals the ratio of their anchor masses, the top to charm ratio matches the corresponding anchor ratio, the strange to down anchor mass ratio equals $phi^{11}$, the bottom to strange anchor ratio equals $phi^{6}$, and that the named absolute quark bridge residual coincides with the QuarkAbsoluteMassResidual proposition.
background
Recognition Science places quark masses on the phi-ladder via the anchor expression $M_0 exp((rung(f)-8+gap(ZOf f)) log phi)$. The structural predictions in Verification are explicit powers of phi divided by 2 million for MeV display. QuarkAbsoluteMassResidual is the proposition that these two expressions agree for up-sector fermions, as defined in the sibling module.
proof idea
This is a structure definition that simply declares the five fields as propositions. No tactics or lemmas are applied inside the definition itself; the equalities are asserted directly as part of the record type.
why it matters
This certificate is instantiated in quarkAbsoluteBridgeScoreCardCert_holds to witness that the scorecard rows hold. It fills the P0-Q01 to P0-Q06 rows of the physical derivation plan by confirming ratio agreement between the structural rs_mass_MeV formula and the gap-corrected massAtAnchor expression. It touches the open question of closing the absolute quark mass bridge to PDG values, as noted in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.