row_absolute_quark_bridge_residual
plain-language theorem explainer
This definition aliases the absolute mass residual for up-sector quarks to the equality between the structural rs_mass_MeV formula and the gap-corrected exponential massAtAnchor expression. Researchers verifying quark mass predictions within the Recognition Science framework would reference it when auditing the absolute MeV bridge. The construction is a direct one-line alias to the upstream QuarkAbsoluteMassResidual definition.
Claim. The absolute quark-mass bridge residual is the proposition that for every fermion $f$ in the up sector, the displayed mass $rs_mass_MeV(UpQuark, r)$ equals $M_0 exp((r - 8 + gap(Z(f))) log phi)$, where $r$ denotes the rung of $f$.
background
In the Quark Absolute Bridge Score Card module the focus is on Phase 0 rows P0-Q01 to P0-Q06 that deepen the QuarkScoreCard by showing agreement on within-family ratios for u/c/t quarks between the equal-Z anchor bridge and the structural rs_mass_MeV formula. The absolute MeV bridge remains a partial residual rather than a closed claim, with two anchors: Verification.rs_mass_MeV as a sector yardstick in MeV including the 10^6 divisor, and RSBridge.massAtAnchor as the native expression with gap-corrected exponent r - 8 + gap(ZOf f).
proof idea
The definition is a one-line wrapper that directly aliases row_absolute_quark_bridge_residual to the upstream QuarkAbsoluteMassResidual proposition.
why it matters
This definition supplies the named residual that feeds into the QuarkAbsoluteBridgeScoreCardCert structure, which certifies agreement on charm-up and top-charm ratios, and into the theorem row_absolute_quark_bridge_residual_is_named that equates it by reflexivity. It advances the absolute quark-mass row of the scorecard in the Recognition Science framework, where the phi-ladder and gap corrections determine masses via yardstick * phi^(rung - 8 + gap(Z)). The absolute MeV bridge remains open, with the falsifier being inability to map native anchor and MeV sector formulas to the same calibrated quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.