quarkAbsoluteBridgeScoreCardCert_holds
The theorem asserts existence of a QuarkAbsoluteBridgeScoreCardCert by direct construction from row-level ratio agreements. A physicist deriving Recognition Science mass ladders cites it to confirm that structural predictions match anchor masses exactly for the u-c-t family ratios under phi powers. The proof is a term-mode assembly that populates the five fields of the certificate structure from six prior row theorems on ratios and residuals.
claimThere exists a certificate $C$ such that charm quark prediction over up quark prediction equals massAtAnchor of c over massAtAnchor of u, top over charm equals massAtAnchor of t over massAtAnchor of c, massAtAnchor of s over massAtAnchor of d equals phi to the 11, massAtAnchor of b over massAtAnchor of s equals phi to the 6, and the absolute bridge residual is named QuarkAbsoluteMassResidual.
background
The module deepens QuarkScoreCard by establishing exact agreement between the equal-Z anchor bridge and the structural rs_mass_MeV formula on within-family ratios for u/c/t quarks. massAtAnchor denotes the native RS expression with gap-corrected exponent r-8+gap(ZOf f) on the phi-ladder; phi is the self-similar fixed point from the forcing chain. The local setting is Phase 0 rows P0-Q01 to P0-Q06, where the absolute MeV bridge remains partial because Verification.rs_mass_MeV includes a 10^6 display divisor while RSBridge.massAtAnchor does not.
proof idea
The proof is a term-mode construction that directly supplies the five fields of QuarkAbsoluteBridgeScoreCardCert. It uses row_charm_up_structural_anchor_agree for the charm-up ratio, row_top_charm_structural_anchor_agree for the top-charm ratio, row_anchor_strange_down_ratio_rpow and row_anchor_bottom_strange_ratio_rpow for the down-sector phi-power anchors, and row_absolute_quark_bridge_residual_is_named for the residual identification.
why it matters in Recognition Science
This theorem certifies the P0-Q bridge rows in the quark mass sector, confirming that structural and anchor expressions agree on phi-power ratios for the up-charm-top family. It supports the Recognition Science mass formula yardstick times phi to the (rung-8+gap(Z)) and ties to T6 phi fixed point and T5 J-uniqueness via the underlying mass expressions. The absolute MeV bridge stays open pending a full SI/display mapping, as stated in the module doc; downstream use is limited because used_by_count is zero.
scope and limits
- Does not establish absolute MeV values for down-sector quarks.
- Does not close the full mass formula without the residual bridge.
- Does not address lepton or boson sectors.
- Does not provide numerical predictions beyond the listed ratio equalities.
formal statement (Lean)
160theorem quarkAbsoluteBridgeScoreCardCert_holds :
161 Nonempty QuarkAbsoluteBridgeScoreCardCert :=
proof body
Term-mode proof.
162 ⟨{ charm_up_ratio_agrees := row_charm_up_structural_anchor_agree
163 top_charm_ratio_agrees := row_top_charm_structural_anchor_agree
164 strange_down_anchor_ratio := row_anchor_strange_down_ratio_rpow
165 bottom_strange_anchor_ratio := row_anchor_bottom_strange_ratio_rpow
166 residual_named := row_absolute_quark_bridge_residual_is_named }⟩
167
168end
169
170end IndisputableMonolith.Masses.QuarkAbsoluteBridgeScoreCard