eta_absorbs_consistency
plain-language theorem explainer
The sum g₁₂ s₁₂ + g₂₃ s₂₃ equals η times the log-step L times the cross-difference g₁₂ s₁₂ − g₂₃ s₂₃, with η taken from the closed-form data formula. Anyone fitting the refined sub-leading mass family cites this as the exact absorption identity for the sign-split consistency violation. The proof unfolds the definition of η and clears the field under the two nondegeneracy hypotheses.
Claim. For real $g_{12}, g_{23}, s_{12}, s_{23}$ with $g_{12}s_{12}-g_{23}s_{23}\neq 0$ and $\log(s_{12}/s_{23})\neq 0$, writing $\eta=(g_{12}s_{12}+g_{23}s_{23})/(\log(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$ yields $g_{12}s_{12}+g_{23}s_{23}=\eta\cdot\log(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23})$.
background
Item 8 is the open quark sub-leading correction in the Recognition mass ladder. The module builds the smallest precise target that would close that item and make the all-sector generalization falsifiable.
The rigid sign-split ratio family forces the structural law $g_{12}s_{12}+g_{23}s_{23}=0$. PDG residual pairs violate that law. The closed-form parameter $\eta$ is defined from the four data numbers by dividing the sum by the product of the log-step $L=\log(s_{12}/s_{23})$ and the cross-difference $D=g_{12}s_{12}-g_{23}s_{23}$. The two nondegeneracy hypotheses keep $L$ and $D$ invertible.
Sibling identities then rewrite the refined-family components as $1+\eta L=2 g_{12}s_{12}/D$ and $1-\eta L=-2 g_{23}s_{23}/D$, which feed constructive existence and uniqueness for each sector.
proof idea
Term-mode, two steps. Unfold the definition of $\eta$ from data, which is exactly the quotient $(g_{12}s_{12}+g_{23}s_{23})/(L\cdot D)$. Then field_simp clears the common nonzero denominator under $D\neq 0$ and $L\neq 0$, recovering the claimed product form. No external lemmas are required beyond the definition and field arithmetic.
why it matters
This is the fundamental absorption equation for Item 8: the consistency violation of the sign-split family is exactly what $\eta$ soaks up. Module summary lists it with the closed-form $\eta$ package and the two component identities as the algebraic engine behind refined-family solvability.
Downstream, the constructive existence proofs for the refined negative and positive families build explicit coefficients from this $\eta$ and verify both residual components. Combined with uniqueness, that yields $\exists!$ per sector and the full negative-sector closure. Without this identity, the refined family would not systematically cancel the rigid-law obstruction that PDG data exhibits.
In the broader RS mass picture (phi-ladder yardstick with rung and gap corrections), this is the local algebraic hinge that turns a structural inconsistency into a single log-asymmetry parameter rather than an ad hoc sector patch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.