QuarkAbsoluteMassResidual
plain-language theorem explainer
QuarkAbsoluteMassResidual defines the proposition that equates the Recognition Science mass formula in MeV for up-sector fermions to the gap-corrected exponential form M0 * phi^(rung(f)-8+gap(Z(f))). Researchers closing absolute quark-mass predictions in the Recognition Science scorecard would cite this named residual. The definition is a direct universal quantification over up-sector fermions of the two mass expressions.
Claim. For every fermion $f$ in the up sector, the mass in MeV computed by the Recognition Science verification formula at the up-quark anchor and rung of $f$ equals the base mass $M_0$ times the exponential of $(rung(f)-8+gap(Z(f)))log phi$, where $phi$ is the golden ratio, rung assigns the discrete level, $Z(f)$ is the effective charge number, and gap is the integration-gap function.
background
The Quark Score Card module records theorem-grade facts for Phase 0 quark-mass rows P0-Q01..P0-Q06 and flags open items. It states that the rs_mass_MeV formula lacks the gap(ZOf f) correction present in the massAtAnchor formula, making the bridge equivalence the missing piece for absolute mass matches to PDG bands. Upstream results supply the rung assignment to fermions, the golden-ratio constant phi, and the integration gap A=1 whose phi-power balance identity holds at D=3.
proof idea
As a definition the body is the explicit universal quantification over fermions f with sector equal to up of the equality between the verification mass expression and the exponential form involving rung, gap, and log phi. No lemmas or tactics are invoked; the declaration simply names the quantified statement.
why it matters
This definition names the residual that appears directly in the QuarkAbsoluteBridgeScoreCardCert structure and in the row_absolute_quark_bridge_residual alias. It fills the open absolute-mass bridge item noted in the module documentation. Within the Recognition Science framework it connects the structural mass formula to the phi-ladder expression yardstick * phi^(rung-8+gap(Z)) from the T6 fixed-point and T8 three-dimensional setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.