refinedFamily_pos_unique
plain-language theorem explainer
On a fixed positive-sign residual signature, equal refined-family outputs force the active coupling coefficient and the sub-leading slope η to agree. Anyone closing Item 8 (quark sub-leading mass corrections) cites this for the uniqueness half of sector-wise existence-uniqueness. The proof cancels shared nonzero scale factors from the two residual channels, then recovers c by linear arithmetic and η by cancellation against a nonzero log-step ratio.
Claim. Let $s_{12}, s_{23} \in \mathbb{N}_{>0}$, $\kappa \neq 0$, and $L = \log(s_{12}/s_{23}) \neq 0$. Fix the positive sign class. If two coefficient triples $(n_1,c_1,\eta_1)$ and $(n_2,c_2,\eta_2)$ with $c_1 \neq 0$ produce the same refined residual pair under this signature, then $c_1 = c_2$ and $\eta_1 = \eta_2$.
background
Item 8 concerns the unified sub-leading mass formula for quark sectors in Recognition Science. This module builds the smallest precise theorem package that would close that open correction item and make the all-sector generalization falsifiable.
A residual signature packages a sign class (positive or negative), two positive natural steps $s_{12}, s_{23}$, and a nonzero coupling $\kappa$. Coefficient data are triples $(n, c, \eta)$: an offset, an active scale $c$, and a logarithmic slope $\eta$. The refined family maps such data to a residual pair $(\mathrm{gen}{12}, \mathrm{gen}{23})$ whose channels are weighted by $\kappa$ and the step fractions, with factors $1 \pm \eta L$ where $L = \log(s_{12}/s_{23})$.
Companion solvability results construct coefficients matching any admissible residual pair. Uniqueness of the active pair $(c, \eta)$ is the other half of sector-wise $\exists!$. The module summary states the proof shape: cancel common factors, then recover $c$ and $\eta$ by linear arithmetic and multiplicative cancellation.
proof idea
Project the assumed equality of refined residual pairs onto the two generators. After unfolding the refined-family definition and applying sign-injectivity on the second channel, both sides share nonzero prefactors $\kappa \cdot s_{23}/(s_{12}+s_{23})$ and $\kappa \cdot s_{12}/(s_{12}+s_{23})$ (nonzero because $\kappa \neq 0$ and the steps are positive).
Cancel those prefactors with right-multiplication cancellation after ring rewrites, 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)$.
Adding via linarith yields $c_1=c_2$. Substitute, cancel $c_1 \neq 0$ on the left, then cancel $L \neq 0$ on the right to recover $\eta_1=\eta_2$.
why it matters
Together with the matching solvability theorem for the positive sign class, this supplies uniqueness of $(c,\eta)$ on each positive sector, completing the $\exists!$ package announced in the module summary (items 3–4). The negative-sign twin and the full negative-sector closure already combine solvability with uniqueness; this is the positive counterpart.
Item 8 is the open quark sub-leading correction on the mass ladder (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Closing it needs a unique, data-matched refined family per sector so the all-sector generalization becomes falsifiable against PDG residuals. The plain ratio family is structurally rigid (gen12·s12 + gen23·s23 = 0), which PDG data violate; the refined family absorbs that via $\eta$. Downstream the module aims at sign-class collapse and full sector closures; used-by edges are empty, so this lemma is infrastructure awaiting positive-sector closure assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.