RefinedCoeffs
plain-language theorem explainer
Packages the three global real parameters of the refined residual family: negative-sign amplitude, positive-sign amplitude, and a universal log-asymmetry η that tilts the gen12/gen23 balance. Anyone writing Item-8 closure, lepton-anchored transport, or the all-sector falsification test cites this carrier. It is a plain structure definition with no proof content.
Claim. A refined coefficient package is a triple $(c_{-}, c_{+}, \eta) \in \mathbb{R}^{3}$, where $c_{-}$ (resp. $c_{+}$) is the amplitude for the negative (resp. positive) sign class and $\eta$ is a universal log-asymmetry modulating the gen12/gen23 residual ratio.
background
Item 8 asks for a unified sub-leading correction to the RS mass ladder across quark and lepton sectors. The plain sign-split ratio family is too rigid: it forces $\mathrm{gen}{12}\cdot s{12}+\mathrm{gen}{23}\cdot s{23}=0$, which PDG residuals violate. The refined family repairs that by inserting a single global log-asymmetry $\eta$ into the two-generation residual map.
The three fields here are exactly the free parameters of that map. Sign-class amplitudes $c_{-}$ and $c_{+}$ multiply the appropriate branch of a residual signature; $\eta$ multiplies a log-step factor $L=\ln(s_{12}/s_{23})$ so that the effective weights become $1\pm\eta L$. Closed-form recovery of $\eta$ from data is already proved in-module via etaFromData and the identities $1+\eta L=2 g_{12}s_{12}/D$, $1-\eta L=-2 g_{23}s_{23}/D$.
The name eta collides with unrelated unit-map and Minkowski-metric symbols elsewhere in the monolith; in this module it means only the residual log-asymmetry coefficient.
proof idea
No proof: this is a structure declaration. Three real fields are introduced with no invariants, defaults, or constructors beyond Lean’s automatic ones. Downstream code builds concrete packages (e.g. lepton-anchored triples) and feeds them to refinedFamily.
why it matters
This is the parameter type for every refined Item-8 object in the module. refinedFamily reads $(c_{-},c_{+},\eta)$ and returns a residual pair; solvability and uniqueness theorems (refinedFamily_neg_solvable, refinedFamily_pos_solvable, and the matching uniqueness results) establish $\exists!$ active $(c,\eta)$ per sector. The all-sector falsifier refinedAllSectorTest quantifies over one such triple fitting up, down, and lepton residuals simultaneously (6 equations, 3 unknowns). Lepton-anchored transport builds a concrete package with $c_{+}=0$ and lepton-derived $\eta$, then asks whether the same coefficients predict anchor-scale quark residuals (leptonAnchoredTarget, refinedItem8ClosureTarget).
In the broader RS picture this is the minimal coefficient space that can absorb the consistency obstruction of the plain ratio family while remaining rigid enough to be globally falsifiable. It does not itself invoke T5–T8 or the RCL; it sits at the verification layer above the $\phi$-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.