consistency_necessary
plain-language theorem explainer
If a sign-split ratio family reproduces an exact residual pair, that pair must obey the weighted cross identity gen12·step12 + gen23·step23 = 0. Mass-formula auditors cite it as the necessity half of the structural rigidity of the two-coefficient family. The proof rewrites by the match hypothesis and applies the already-proved family identity.
Claim. Let $c_\mathrm{neg}, c_\mathrm{pos}$ be the two global sign-class amplitudes, let $\sigma$ be a residual signature with positive rung steps $s_{12}, s_{23}$, and let $(g_{12}, g_{23})$ be an exact residual pair. If the sign-split family's predicted residuals equal $(g_{12}, g_{23})$, then $g_{12}\, s_{12} + g_{23}\, s_{23} = 0$.
background
Item 8 of the Recognition mass program asks for a unified sub-leading correction law on the phi-ladder for quarks (and, eventually, all sectors). Residuals are the generation $1\to 2$ and $2\to 3$ corrections $(g_{12}, g_{23})$; a residual signature packages the sector's $B_\mathrm{pow}$ sign, the SDGT rung spacings $s_{12}, s_{23}$ (cube-cell counts from the $Q_3$ decomposition), and a coupling.
The smallest candidate is the sign-split ratio family: two global amplitudes $(c_\mathrm{neg}, c_\mathrm{pos})$ feed a fixed functional form predictedResiduals. Upstream in this module, consistency_of_ratioFamily already shows that every output of that form is forced onto the hyperplane $g_{12} s_{12} + g_{23} s_{23} = 0$. The present statement is the matching necessity: any exact pair the family can hit must lie on that same hyperplane.
Module context: this rigidity is known to be violated by PDG data, which is why the file next introduces a single universal log-asymmetry $\eta$ that softens the ratio $g_{12}/g_{23} = -s_{23}/s_{12}$.
proof idea
One short tactic chain. Rewrite the goal residual pair by the hypothesis that it equals predictedResiduals coeffs sig, unfold that definition, and discharge with the sibling theorem consistency_of_ratioFamily coeffs sig, which already proves the weighted sum vanishes for every coefficient pair and signature. No new algebra is performed here.
why it matters
This is the contrapositive gate for the sign-split family inside the Item 8 closure target: if PDG (or any other) residuals fail $g_{12} s_{12} + g_{23} s_{23} = 0$, no choice of $(c_\mathrm{neg}, c_\mathrm{pos})$ can fit. The module summary lists consistency_of_ratioFamily as the first sorry-free result and records that PDG data violates the constraint; the present lemma packages that fact as a matching necessity usable in later uniqueness or non-existence arguments.
It sits on the mass side of the Recognition ladder (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), where sub-leading generation corrections are the remaining open item. Downstream the file builds the refined $\eta$-family with constructive $\exists!$ per sector; this necessity explains why the rigid two-parameter family is abandoned before that refinement. No used_by edges are recorded yet, so its role is local scaffolding for the Item 8 falsifiability story rather than a leaf of a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.