core_eq_residue_of_positive
plain-language theorem explainer
For positive sector yardstick and reference mass, the integer-rung core mass equals the residue-coordinate mass after the explicit log_φ reparameterization. Quark-mass pipeline authors cite this to treat core and quarter forms as the same law. The proof unfolds both mass maps, rewrites the yardstick ratio via rpow_logb, and collapses the exponents with rpow_add.
Claim. Let $A_{\mathrm{sector}}>0$ and $m_{\mathrm{ref}}>0$, and fix an integer rung $r$ and real gap. Then $$A_{\mathrm{sector}}\,\varphi^{r-8+\mathrm{gap}}=m_{\mathrm{ref}}\,\varphi^{R},$$ where $$R=\log_{\varphi}(A_{\mathrm{sector}}/m_{\mathrm{ref}})+(r-8+\mathrm{gap}).$$
background
Recognition Science places particle masses on a multiplicative $\varphi$-ladder. In RS-native units the mass law is a yardstick times $\varphi$ to a rung offset by the eight-tick baseline and a sector gap: $m=A,\varphi^{r-8+\mathrm{gap}}$. That is the core (integer-rung) convention.
A second bookkeeping convention fixes a positive reference mass $m_{\mathrm{ref}}$ and writes $m=m_{\mathrm{ref}},\varphi^{R}$ (quarter/residue form). The module shows these are not two physical laws: once $m_{\mathrm{ref}}$ is chosen, $R$ is the explicit change of coordinates $R=\log_{\varphi}(A/m_{\mathrm{ref}})+(r-8+\mathrm{gap})$.
The golden ratio $\varphi$ satisfies $\varphi>1$ (hence $\varphi\neq 1$), which legitimates $\log_{\varphi}$ and the identity $x=\varphi^{\log_{\varphi}x}$ for $x>0$. The eight in the exponent is the T7 eight-tick octave baseline from the forcing chain.
proof idea
Unfold the four local definitions (core mass, residue mass, residue-from-core map, and core exponent). Positivity of $A$ and $m_{\mathrm{ref}}$ gives $A/m_{\mathrm{ref}}>0$, so Real.rpow_logb with phi_pos and phi_ne_one yields $A/m_{\mathrm{ref}}=\varphi^{\log_{\varphi}(A/m_{\mathrm{ref}})}$.
A short calc then rewrites $A,\varphi^{r-8+\mathrm{gap}}$ as $m_{\mathrm{ref}}\cdot(A/m_{\mathrm{ref}})\cdot\varphi^{r-8+\mathrm{gap}}$ (field_simp), associates, substitutes the log identity, and merges powers by Real.rpow_add. The resulting exponent is exactly the residue coordinate.
why it matters
This is the algebraic heart of Quark Coordinate Unification (Pass 2): core and residue forms represent one positive mass law. Downstream, coordinate_systems_equivalent packages the claim as existence of an $R$ making the two masses equal, and pipeline_equals_residue_form applies it with the electron reference mass so the canonical forward quark pipeline matches Convention B coordinates.
In the broader framework this protects the mass formula yardstick $\cdot,\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$ on the $\varphi$-ladder: switching to a reference-mass residue coordinate does not invent a second law. It sits under the T6/T7 landmarks ($\varphi$ fixed, eight-tick baseline) rather than under J-uniqueness or the RCL directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.