row_absolute_quark_bridge_residual_is_named
plain-language theorem explainer
The declaration equates the local definition of the absolute quark bridge residual to the named proposition from the QuarkScoreCard module. Researchers assembling the quark mass scorecard certification would cite it to confirm definitional identity before invoking the residual in larger constructions. The proof is a single reflexivity step confirming the two expressions are identical by definition.
Claim. The proposition asserting that the structural mass formula in MeV equals the gap-corrected native anchor mass expression for up-sector fermions is identical to the named residual that bridges those two formulas on a chosen quark sector.
background
The module develops the quark absolute bridge scorecard for phase 0 rows P0-Q01 to P0-Q06. It deepens the existing QuarkScoreCard by establishing agreement on within-family ratios for up-type quarks using the equal-Z anchor bridge and the structural rs_mass_MeV formula. The absolute MeV bridge remains a partial theorem expressed as a residual between two anchors: the sector yardstick rs_mass_MeV including the 10^6 divisor, and the native RSBridge.massAtAnchor with exponent r - 8 + gap(ZOf f).
proof idea
This is a one-line wrapper that applies reflexivity to confirm the local definition of the absolute quark bridge residual matches the imported QuarkAbsoluteMassResidual proposition.
why it matters
This declaration supports the construction of the QuarkAbsoluteBridgeScoreCardCert in the downstream theorem that collects agreements on charm-up and top-charm ratios along with down-sector anchors. It fills the naming step for the absolute mass residual in the quark scorecard, as described in the module statement on partial theorems for absolute MeV bridges. In the Recognition framework it touches the phi-ladder mass formula with gap corrections, but leaves the absolute calibration open pending a future SI/display bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.