residue_eq_core
plain-language theorem explainer
Residue-form quark mass equals core-form mass once the sector yardstick is recovered from the residue coordinate by the explicit inverse map. Anyone identifying the two RS mass conventions cites this algebraic identity. The proof unfolds both formulas and applies φ-power additivity in a short calc.
Claim. For reference mass $m_{\mathrm{ref}}\in\mathbb{R}$, residue coordinate $R\in\mathbb{R}$, integer rung $r\in\mathbb{Z}$, and gap $g\in\mathbb{R}$, the residue mass equals the core mass of the recovered yardstick: $m_{\mathrm{ref}}\,\varphi^{R}=A\,\varphi^{r-8+g}$, where $A=m_{\mathrm{ref}}\,\varphi^{R-(r-8+g)}$.
background
This module (Quark Coordinate Unification, Pass 2) shows that the two quark mass coordinate conventions are the same positive multiplicative law once a reference mass is fixed.
Core form is the integer-rung architecture $m=A_{\mathrm{sector}},\varphi^{r-8+g}$. Residue (quarter) form is the reference-mass coordinate $m=m_{\mathrm{ref}},\varphi^{R}$. The bridge is the explicit reparameterization $R=\log_{\varphi}(A_{\mathrm{sector}}/m_{\mathrm{ref}})+(r-8+g)$, so the residue coordinate is not a second physical law.
Local helpers: residue mass is $m_{\mathrm{ref}},\varphi^{R}$; core exponent is $r-8+g$; core mass is yardstick times $\varphi$ to that exponent; yardstick-from-residue inverts the map, sending $(m_{\mathrm{ref}},R,r,g)$ to $m_{\mathrm{ref}},\varphi^{R-(r-8+g)}$. The golden ratio $\varphi$ is the RS self-similar fixed point (forcing chain T6).
proof idea
Tactic proof by unfolding residue mass, core mass, yardstick-from-residue, and core exponent. Introduce $E:=(r:\mathbb{R})-8+g$. The only nontrivial step is $\varphi$-power additivity: $\varphi^{R}=\varphi^{R-E}\varphi^{E}$, from Real.rpow_add at positive base $\varphi$ together with the ring identity $(R-E)+E=R$. A three-line calc then reassociates $m_{\mathrm{ref}},\varphi^{R}$ into $(m_{\mathrm{ref}},\varphi^{R-E}),\varphi^{E}$ and substitutes the definition of $E$, matching the unfolded core mass of the recovered yardstick.
why it matters
Closes the residue-to-core direction of the Pass 2 unification: residue form equals core form under the explicit inverse transform (module claim). Together with the sibling core-equals-residue direction (under positivity), it underwrites full equivalence of the two coordinate systems and exact recovery of the residue coordinate from a residue-form mass.
In the RS mass law, physical masses sit on the $\varphi$-ladder as yardstick times $\varphi^{r-8+\mathrm{gap}(Z)}$. Showing that writing the same mass as $m_{\mathrm{ref}},\varphi^{R}$ is only a change of origin on that ladder keeps quark phenomenology from splitting into two inequivalent schemes. No external parent theorems are recorded on the used-by edge; the payload is internal to the unification siblings and the verification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.