refinedPrediction
plain-language theorem explainer
Maps three global refined coefficients and a sector residual signature to the predicted gen12/gen23 sub-leading mass corrections. Citation target for Item 8 closure props that freeze coefficients on one sector and predict another. One-line alias of the refined family evaluator.
Claim. Given refined coefficients $(c_{-}, c_{+}, \eta)$ and a residual signature (sign class, rung steps $n_{12}, n_{23}$, coupling $\kappa$), return the predicted residual pair $(r_{12}, r_{23})$ under the refined sub-leading family.
background
Item 8 concerns the open quark sub-leading correction in the RS mass ladder. Residuals are the two generation steps $1\to 2$ and $2\to 3$ (a residual pair). Each sector carries a residual signature: a sign class for the $B$-power, positive SDGT rung spacings from the $Q_3$ cube-cell count, and a coupling.
The coarsest candidate was a pure sign-split family with two global amplitudes. PDG data break its rigidity identity. The refined family adds a universal log-asymmetry $\eta$ that modulates the gen12/gen23 ratio, with three global coefficients: $c_{-}$, $c_{+}$, and $\eta$.
This definition is the named evaluation map from those coefficients plus a signature to the predicted residual pair. At $\eta=0$ the refined family collapses to the original sign-split family.
proof idea
Definitional one-line wrapper: it returns exactly refinedFamily coeffs sig. No extra algebra. The body of the refined family selects $c_{-}$ or $c_{+}$ by signature sign, then builds the residual pair from coupling, rung steps, and the $\eta$-modulated log ratio.
why it matters
Naming layer for every Item 8 falsification and closure proposition in this module. Downstream: the refined Item 8 closure target asserts unique coefficients matching up- and down-quark exact residuals; the refined all-sector test asks whether three coefficients frozen on quarks also reproduce lepton residuals (six equations, three unknowns); lepton-anchored targets freeze $(c_{-},\eta)$ on leptons and predict anchor-scale quarks.
Sits inside the verification stack for the mass formula on the $\phi$-ladder (yardstick $\cdot \phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Closes the path from the failed sign-split consistency identity to a solvable, unique refined family per sector, making the all-sector generalization empirically falsifiable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.