refinedFamily_neg_unique
plain-language theorem explainer
On a fixed negative-sign residual signature, equal refined-family outputs force the active coefficient c and the tilt η to coincide. Mass-ladder and Item-8 auditors cite this for single-sector uniqueness of sub-leading corrections. The proof cancels common κ-weighted step factors from the two generation components, adds to kill η, then cancels the nonzero log ratio.
Claim. Fix positive integers $s_{12}, s_{23}$ and $\kappa \neq 0$ with $\log(s_{12}/s_{23}) \neq 0$. If two triples $(c_1,p_1,\eta_1)$ and $(c_2,p_2,\eta_2)$ with $c_1 \neq 0$ yield the same refined-family residual pair on the negative-sign signature $(s_{12},s_{23},\kappa)$, then $c_1 = c_2$ and $\eta_1 = \eta_2$.
background
Item 8 is the open quark sub-leading mass correction in the Recognition Science ladder. This module builds the smallest precise target that would close it: a refined residual family that absorbs the consistency violation of the plain sign-split ratio family.
A residual signature carries a sign class (here negative), two positive generation steps $s_{12}, s_{23}$, and a nonzero coupling $\kappa$. Coefficient data are a triple $(c, p, \eta)$; on the negative sector the active scale is $c$ (the unused opposite-sign slot is irrelevant). The refined family maps those data to a residual pair $(\mathrm{gen}{12}, \mathrm{gen}{23})$ whose components are $\kappa$-weighted fractions of the total step times factors $1 \pm \eta \log(s_{12}/s_{23})$.
Upstream solvability already constructs explicit $(c,\eta)$ matching any admissible residual pair. Uniqueness of those active parameters is the complementary half needed for sector-level $\exists!$.
proof idea
From equality of residual pairs, project to the $\mathrm{gen}{12}$ and $\mathrm{gen}{23}$ components and unfold the refined-family definition. The $\mathrm{gen}_{23}$ equation carries a global minus; strip it by injectivity of negation.
Each component still multiplies by a nonzero common factor $\kappa \cdot s_i / (s_{12}+s_{23})$. Cancel those factors with mul_right_cancel₀ after a short calc/ring reassociation, obtaining
$c_1(1+\eta_1 L)=c_2(1+\eta_2 L)$ and $c_1(1-\eta_1 L)=c_2(1-\eta_2 L)$ with $L=\log(s_{12}/s_{23})$.
Add the two identities: the $\eta$ terms cancel and linarith yields $c_1=c_2$. Substitute back, cancel $c_1\neq 0$ on the left, then cancel $L\neq 0$ on the right to get $\eta_1=\eta_2$.
why it matters
Together with the constructive solvability theorem for the negative sector, this supplies the uniqueness half of full sector closure: unique active $(c,\eta)$ matching any admissible residual data. The parent refined_neg_sector_closure packages exactly that $\exists!$, and notes that any solution with arbitrary opposite-sign coefficient still shares the same active pair.
In the Item-8 program this is the algebraic lock that makes the refined sub-leading formula falsifiable rather than underdetermined: once PDG-style residuals and rung steps are fixed, the correction coefficients cannot drift. It sits inside the mass-ladder story (yardstick times $\varphi$ powers with sector gaps) as the uniqueness statement for the continuous tilt that repairs the rigid sign-split identity $\mathrm{gen}{12}s{12}+\mathrm{gen}{23}s{23}=0$, which plain PDG data violate.
The symmetric positive-sector uniqueness and the irrelevance lemmas for the unused coefficient complete the two-sector picture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.