residueFromCore
plain-language theorem explainer
Defines the explicit change of coordinates that turns core-form quark mass parameters into a residue (quarter) exponent R on the phi-ladder. Anyone comparing the integer-rung architecture to reference-mass coordinates cites this map. The body is a one-line formula: base-phi log of the sector-to-reference ratio plus the core exponent.
Claim. Given a sector amplitude $A_{\mathrm{sector}}$, a positive reference mass $m_{\mathrm{ref}}$, an integer rung $r$, and a gap correction $\mathrm{gap}$, the residue coordinate is $$R = \log_\varphi\!\bigl(A_{\mathrm{sector}}/m_{\mathrm{ref}}\bigr) + (r - 8 + \mathrm{gap}).$$
background
The module unifies two conventions for positive quark masses on the Recognition Science $\varphi$-ladder. Core form writes $m = A_{\mathrm{sector}},\varphi^{r-8+\mathrm{gap}}$ (integer rung plus gap). Residue form writes $m = m_{\mathrm{ref}},\varphi^{R}$ once a reference mass is fixed.
The golden ratio $\varphi$ is the self-similar fixed point forced at T6. The mass yardstick and gap corrections (including the gap-45 derivation) supply the sector amplitude and the additive gap term that appear in the core exponent. The residue coordinate $R$ is not a second physical law; it is the unique real that makes the two multiplicative expressions agree when $A_{\mathrm{sector}}>0$ and $m_{\mathrm{ref}}>0$.
Sibling coreExponent packages the integer combination $r-8+\mathrm{gap}$. The present definition simply adjoins the base-$\varphi$ logarithm of the amplitude ratio.
proof idea
Pure definitional abbreviation. The body is the sum of Real.logb phi (A_sector / m_ref) and coreExponent r gap. No tactics, no lemmas, no positivity side conditions at the definition site; those appear only when the map is used to prove mass equality.
why it matters
This is the explicit reparameterization that makes the two quark mass coordinate systems interchangeable. Downstream, core_eq_residue_of_positive unfolds it to prove core mass equals residue mass under the transform, and coordinate_systems_equivalent packages the existence statement once $A_{\mathrm{sector}}>0$ and $m_{\mathrm{ref}}>0$. The forward pipeline uses it as residue_from_pipeline, measuring every sector relative to the electron anchor mass via the sector yardstick and gap correction.
In the broader RS mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), the definition shows that switching to a fixed reference mass is only a change of origin on the log-$\varphi$ line, not a new dynamical law. It closes the Pass-2 structural claim that quarter/residue coordinates are reparameterizations of the same ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.