consistency_of_ratioFamily
plain-language theorem explainer
The sign-split ratio family always returns residual pairs orthogonal to the sector step vector: g₁₂ s₁₂ + g₂₃ s₂₃ = 0. Anyone testing whether Item 8 can close under a two-coefficient family cites this rigidity. The proof destructures the signature, unfolds the family, and finishes by field simplification and ring for both sign cases.
Claim. For any global coefficients $(c_-, c_+)$ and any residual signature with positive rung steps $s_{12}, s_{23}$ (and any coupling), the residual pair $(g_{12}, g_{23})$ produced by the sign-split ratio family satisfies $g_{12}\, s_{12} + g_{23}\, s_{23} = 0$.
background
Item 8 is the open quark sub-leading mass correction in the Recognition mass ladder. This module isolates the smallest precise target that would close it: fix both up and down quark residual pairs inside one closed two-coefficient family, freezing the globals so later lepton, genetic, and theta checks become out-of-sample tests.
A residual signature packages the sector's B-power sign, the two SDGT rung spacings $s_{12}, s_{23}$ (cube-cell counts from the $Q_3$ decomposition, both required positive), and a coupling. A residual pair is just the two generation corrections $(g_{12}, g_{23})$. The candidate family is the sign-split ratio family driven by two globals $(c_-, c_+)$.
The module documents that this family is algebraically rigid: every output pair must obey the cross-product identity above. Numerically, lepton pole masses nearly satisfy it (~3.9% violation); PDG quark ratios violate it more strongly (down ~25%, up ~45%), partly from mixed renormalization scales.
proof idea
Destructure the signature into sign, steps $s_{12}, s_{23}$, coupling, and the two positivity witnesses. Unfold the ratio-family definition and project to the two residual components.
First prove $s_{12}+s_{23}\neq 0$ over $\mathbb{R}$: both casts are strictly positive by Nat.cast_pos on the signature hypotheses, then linarith. Case-split on the B-power sign; in each branch field_simp clears the common nonzero denominator and ring cancels to zero. No external lemmas beyond arithmetic are required.
why it matters
This is the structural obstruction for the smallest sign-split candidate that would close Item 8. Downstream, consistency_necessary is the one-line rewrite: if the family ever matches an exact residual pair, that pair must obey the same cross-product identity; contrapositively, any pair that fails the identity cannot be fit by any coefficients.
The module summary lists this as the first sorry-free result: the family forces $g_{12}s_{12}+g_{23}s_{23}=0$, a rigidity PDG data violates. That obstruction motivates the refined family with an $\eta$ correction that absorbs the violation, for which the module later proves sectorwise existence and uniqueness. In the broader RS chain this sits under the mass-ladder / sub-leading correction program rather than T5–T8 forcing, but it is the gate that decides whether a pure two-coefficient sign-split law can freeze the quark residuals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.