pos_cNeg_irrelevant
plain-language theorem explainer
For positive-sector signatures in the refined mass-ratio family, the unused negative-sector coefficient may be changed arbitrarily without changing the family output. Anyone assembling unique active coefficients $(c,\eta)$ for the positive sector cites this irrelevance lemma. The proof is a one-line simplification that unfolds the refined-family definition.
Claim. Fix reals $q_1,q_2,c,\eta,\kappa$ and positive naturals $s_{12},s_{23}$. The refined sub-leading mass family on coefficient triple $(q_1,c,\eta)$ with positive-sector signature $(s_{12},s_{23},\kappa)$ equals the same family on $(q_2,c,\eta)$ with that same signature. In particular the first coefficient is inert on the positive sector.
background
Item 8 of the Recognition mass program asks for a unified sub-leading correction to the phi-ladder mass ratios across lepton and quark sectors. This module builds the smallest precise target that would close that item: a sign-split refined family whose active coefficients $(c,\eta)$ are uniquely determined by residual data.
A residual signature carries a sector tag (positive or negative), generation steps $s_{12},s_{23}>0$, and a coupling $\kappa$. Coefficient triples are written $(q,c,\eta)$, where only one of the two sector-tied linear coefficients is live for a given tag. The refined family is the explicit algebraic map from those data to predicted residuals.
The module already records the dual fact for the negative sector: on a .neg signature the positive-sector coefficient is unused. The present statement is the matching positive-sector half. Together with solvability and uniqueness of the active pair $(c,\eta)$, it underwrites full sector closure ($\exists!$).
proof idea
One-line term-mode proof: simp [refinedFamily]. Unfolding the refined-family definition on a positive-sector signature drops the first coefficient field, so the two sides become definitionally equal once $c$, $\eta$, and the signature data agree. No algebraic cancellation or external lemma is required beyond the definitional expansion.
why it matters
This is the positive-sector twin of the helper used in refined_neg_sector_closure. The module summary states that full $\exists!$ for a negative sector combines solvability, uniqueness, and neg_cPos_irrelevant; the same pattern for the positive sector needs the present irrelevance fact so that arbitrary values of the dormant coefficient cannot spoil uniqueness of the active pair $(c,\eta)$.
In the broader Recognition chain this sits inside the verification layer for the mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), not inside the T0–T8 forcing spine. It does not invent new physics constants; it removes a spurious degree of freedom so that Item 8’s refined correction, once fitted, is a genuine prediction rather than a two-parameter family. Downstream sector-closure theorems (when assembled) will quote it exactly as the negative dual is quoted today. No used_by edges are recorded yet, so it is presently a proved building block awaiting the positive-sector closure package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.