charm_to_up_ratio_structural
plain-language theorem explainer
Within a fixed sector and fixed charge-band correction, the ratio of two predicted masses equals φ to the power of the integer rung difference. Quark-ratio corollaries cite this to turn pure rung gaps into pure powers of φ with no residual yardstick or gap. The proof cancels the common prefactors and applies the real-power quotient identity.
Claim. For every sector $s$, integers $r_1,r_2$, and integer charge parameter $Z$, $$\frac{m(s,r_2,Z)}{m(s,r_1,Z)}=\varphi^{r_2-r_1},$$ where the forward mass is $m(s,r,Z)=A_s\,\varphi^{r-8+\mathrm{gap}(Z)}$ with sector yardstick $A_s$ and band correction $\mathrm{gap}(Z)$.
background
The Quark Forward Pipeline predicts all six quark masses from counting-layer integers, φ (forced at T5/T6), and α, with no PDG mass input. Convention A fixes a sector yardstick $A_s=2^{B_{\mathrm{pow}}(s)}E_{\mathrm{coh}}\varphi^{r_0(s)}$, an integer rung from generation torsion, and a charge-band gap $\mathrm{gap}(Z)$. The mass law is then $m=A_s,\varphi^{r-8+\mathrm{gap}(Z)}$.
Absolute masses still need a calibration seam; the module therefore works with dimensionless ratios. When two states share the same sector and the same $Z$, both $A_s$ and $\mathrm{gap}(Z)$ are identical, so they cancel in a mass ratio and only the rung difference remains. That is the structural content of this theorem: equal-$Z$ families live on a pure φ-ladder.
The same cancellation is the algebraic content of the general rung-scaling fact in the mass-law layer (adjacent rungs differ by exactly one factor of φ). Here it is stated for arbitrary integer rung pairs at fixed sector and $Z$.
proof idea
Introduce sector, the two rungs, and $Z$. Unfold the mass predictor and name the common gap and yardstick $Y$. Positivity of $Y$ follows from the product of three positive φ-powers (and the coherence energy), so $Y\neq 0$.
Cancel $Y$ from numerator and denominator by the left-multiplication form of division. The remaining quotient is $\varphi^{a}/\varphi^{b}$ with $a=r_2-8+\mathrm{gap}$ and $b=r_1-8+\mathrm{gap}$. Rewrite as a product via div_eq_iff, apply the real power-add law for base $\varphi>0$, and finish by ring on the exponents: the $-8$ and gap terms cancel, leaving $r_2-r_1$.
why it matters
This is the structural engine behind the module's equal-family quark ratios. Downstream, charm_to_up_eq_phi11 instantiates it on the up sector at the up/charm rungs and charge $Z=+2/3$ to obtain $m_c/m_u=\varphi^{11}$ (rung gap $15-4$). Likewise bottom_to_strange_eq_phi6 obtains $m_b/m_s=\varphi^{6}$ on the down sector (rung gap $21-15$).
In the Recognition chain those pure powers of φ are the testable content of the forward pipeline: once rungs are fixed by generation torsion and sectors by cube geometry, no free mass parameter remains inside an equal-$Z$ family. The result sits on the mass formula yardstick $\times\varphi^{r-8+\mathrm{gap}(Z)}$ and on φ as the T5/T6 self-similar fixed point. It does not by itself fix absolute GeV values; it certifies that equal-band ratios are seam-free φ-powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.