coreMass
plain-language theorem explainer
Defines the core (sector-yardstick) quark mass law: sector amplitude times a power of φ whose exponent is the integer rung shifted by eight and the gap. Anyone comparing the integer-rung architecture to the residue/quarter coordinate cites this shape. The body is a one-line multiplicative definition via the core exponent.
Claim. For a sector yardstick $A_{\mathrm{sector}}\in\mathbb{R}$, integer rung $r\in\mathbb{Z}$, and gap parameter $g\in\mathbb{R}$, the core mass is $m_{\mathrm{core}}(A_{\mathrm{sector}},r,g)=A_{\mathrm{sector}}\,\varphi^{r-8+g}$, where $\varphi$ is the golden ratio fixed by the RS self-similarity condition.
background
Pass 2 of Quark Coordinate Unification equates two positive mass-law presentations on the φ-ladder. The core form is the integer-rung architecture $m=A_{\mathrm{sector}},\varphi^{r-8+\mathrm{gap}}$. The residue (quarter) form is $m=m_{\mathrm{ref}},\varphi^{R}$ once a reference mass is chosen. The explicit bridge is $R=\log_\varphi(A_{\mathrm{sector}}/m_{\mathrm{ref}})+(r-8+\mathrm{gap})$.
The golden ratio $\varphi$ is the RS self-similar fixed point (forcing chain T6). The gap term is the same structural offset that appears in the mass formula yardstick $\cdot,\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$. Sibling coreExponent packages the real exponent $r-8+\mathrm{gap}$; this definition only multiplies by the sector yardstick.
proof idea
Pure definition, not a theorem. The body is the product of the sector yardstick with $\varphi$ raised to coreExponent r gap, which is the real number $(r:\mathbb{R})-8+\mathrm{gap}$. No lemmas are applied; downstream proofs unfold this abbreviation together with residueMass and the coordinate maps.
why it matters
Anchors the core side of the coordinate dictionary. Downstream, core_eq_residue_of_positive shows core mass equals residue mass after the explicit transform residueFromCore; residue_eq_core is the inverse via yardstickFromResidue; and coordinate_systems_equivalent packages existence of a residue coordinate $R$ with equality of the two mass shapes for any positive yardstick and reference mass.
In the RS mass ladder this is the sector-yardstick presentation of $m=\mathrm{yardstick},\varphi^{(\mathrm{rung}-8+\mathrm{gap})}$. It does not invent a second law: the module's claim is that the quarter coordinate is only a reparameterization once $m_{\mathrm{ref}}$ is fixed. That structural fact is what Pass 2 verifies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.