etaFromData
plain-language theorem explainer
Closed-form formula for the log-asymmetry parameter η that folds the sign-split family's consistency violation into a single correction. Cited by anyone closing Item 8 (quark sub-leading residuals) or running the refined all-sector test. Pure algebraic definition: weighted residual sum over log-step times cross-difference.
Claim. Given residual couplings $g_{12}, g_{23}$ and step sizes $s_{12}, s_{23}$, set $$\eta(g_{12},g_{23},s_{12},s_{23}) = \frac{g_{12}s_{12}+g_{23}s_{23}}{\ln(s_{12}/s_{23})\,(g_{12}s_{12}-g_{23}s_{23})}.$$ The expression is well-defined whenever $s_{12}\neq s_{23}$ and $g_{12}s_{12}\neq g_{23}s_{23}$.
background
Item 8 is the open quark sub-leading correction in the Recognition mass ladder. The module builds the smallest theorem package that would close it and make an all-sector generalization falsifiable.
The sign-split residual family is rigid: it forces $g_{12}s_{12}+g_{23}s_{23}=0$. PDG residual pairs violate that identity. The log-asymmetry parameter $\eta$ is introduced precisely to absorb the violation, turning the rigid family into a refined two-parameter family $(c,\eta)$ that can match data.
Here $g_{12},g_{23}$ are generation-step residual couplings and $s_{12},s_{23}$ are the corresponding rung steps (e.g. $11$ and $6$ for leptons, $6$ and $8$ for down quarks). $L=\ln(s_{12}/s_{23})$ is the log-step; $D=g_{12}s_{12}-g_{23}s_{23}$ is the cross-difference. Both must be nonzero for $\eta$ to be defined.
proof idea
Direct algebraic definition, not a proved statement. The body is the single quotient $(g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$. No lemmas are applied; downstream identities unfold this definition and cancel by ring arithmetic.
why it matters
This is the algebraic engine of the Item 8 closure package. Downstream, eta_absorbs_consistency shows that the consistency violation equals exactly $\eta\cdot L\cdot D$; the companion identities rewrite $1+\eta L=2g_{12}s_{12}/D$ and $1-\eta L=-2g_{23}s_{23}/D$, which close the gen-1→2 and gen-2→3 equations. Concrete sector values (leptonEta ≈ +0.065, downQuarkEta ≈ −0.88) are instances of this formula. Solvability and uniqueness of the refined family, and the refined all-sector test (three coefficients frozen by quarks must reproduce lepton residuals), all route through it. In the broader RS picture it sits under the mass-ladder yardstick $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, supplying the sub-leading correction that pure rung counting leaves open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.