refined_neg_sector_closure
plain-language theorem explainer
For any negative B-power sector with nonzero first residual, nonzero coupling, distinct positive steps, and nondegenerate cross-difference, the refined residual family admits a unique active pair (amplitude c, log-asymmetry η) matching the data. Item-8 and lepton-sector verifiers cite this as the full existential-uniqueness package on the active coefficients. The proof glues constructive solvability to uniqueness after discarding the unused positive-sector amplitude.
Claim. Fix residuals $g_{12}, g_{23}\in\mathbb{R}$, steps $s_{12}, s_{23}\in\mathbb{N}_{>0}$, and coupling $\kappa\neq 0$. Assume $g_{12}\neq 0$, $g_{12}s_{12}-g_{23}s_{23}\neq 0$, and $\log(s_{12}/s_{23})\neq 0$. Then there exist unique active coefficients $c,\eta\in\mathbb{R}$ such that the refined family on the negative-sign residual signature with those steps and $\kappa$, evaluated at amplitude triple $(c,0,\eta)$, recovers $(g_{12},g_{23})$. Any other triple $(c',p',\eta')$ yielding the same residuals must satisfy $c'=c$ and $\eta'=\eta$ (the unused positive amplitude $p'$ is free).
background
Item 8 of the Recognition mass program asks for a precise, falsifiable sub-leading correction to the phi-ladder mass formula. This module builds the smallest theorem layer that would close that item: residual pairs $(g_{12},g_{23})$ are matched by a refined family whose free parameters are an amplitude $c$ and a log-asymmetry $\eta$, evaluated on a residual signature that records B-power sign, two positive integer steps, and a coupling $\kappa$.
A pure sign-split ratio family is too rigid: it forces $g_{12}s_{12}+g_{23}s_{23}=0$, which PDG data violate. The refined family absorbs the violation through $\eta$, with closed form $\eta=(g_{12}s_{12}+g_{23}s_{23})/(\ln(s_{12}/s_{23})\cdot(g_{12}s_{12}-g_{23}s_{23}))$ and the algebraic identities $1+\eta L=2g_{12}s_{12}/D$, $1-\eta L=-2g_{23}s_{23}/D$.
For the negative sign class the positive-sector amplitude is inert. Upstream work already supplies constructive solvability (refinedFamily_neg_solvable) and uniqueness of the active pair (refinedFamily_neg_unique); the present theorem packages both into a single sector-level $\exists!$ statement.
proof idea
Call the constructive solver refinedFamily_neg_solvable on the given residuals, steps, and coupling. It returns some triple $(c,c_p,\eta)$ that matches the data under the refined family on the negative signature.
Existence for the normalized triple $(c,0,\eta)$ follows by the helper neg_cPos_irrelevant: on a negative signature the positive amplitude does not enter the refined map, so swapping $c_p$ for $0$ preserves the residual pair.
Uniqueness: take any other triple $(c',p',\eta')$ that also matches. First show $c\neq 0$ from $g_{12}\neq 0$ by projecting the existence equation onto the first residual component and simplifying. Then apply refinedFamily_neg_unique to the two solutions (after equating their refined outputs) to conclude $c'=c$ and $\eta'=\eta$. The unused $p'$ is unconstrained.
why it matters
This is the full sector-level $\exists!$ for every negative B-power residual signature under the nondegeneracy hypotheses of Item 8. The module summary lists it as the combination of solvability and uniqueness with the inertness of the positive amplitude on .neg.
Downstream, leptonSectorClosure instantiates the theorem on the lepton signature at the candidate electromagnetic coupling $\kappa_{\mathrm{lep}}=1/(4\pi\cdot 11)$, freezing $(c_{\mathrm{Neg}},\eta)$ independently of quark data. The definition downQuarkEta sits in the same closure pipeline (mixed-scheme PDG $\eta\approx -0.88$), using the same refined-family language.
In the broader Recognition chain this is verification infrastructure rather than a T0–T8 forcing step: it makes the sub-leading mass correction (Item 8) mathematically closed and sector-falsifiable once concrete residuals and steps are plugged in. It does not yet force a universal $\eta$ across sign classes; the module notes that universal $\eta$ is ruled out by current data, motivating independent $\eta$ per sign class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.