neg_cPos_irrelevant
plain-language theorem explainer
For negative residual signatures, the refined sub-leading mass family ignores the unused positive-sector coefficient: swapping that field leaves the prediction unchanged. Cited by the unique $(c,\eta)$ closure for the negative sector. Proof is a one-line simplification of the refined-family definition.
Claim. Fix reals $c,q_1,q_2,\eta$, steps $s_{12},s_{23}\in\mathbb{N}_{>0}$, and coupling $\kappa$. On a negative signature with those steps and coupling, the refined family with active coefficient $c$, unused positive coefficient $q_1$, and $\eta$ equals the same evaluation with unused coefficient $q_2$ instead of $q_1$.
background
Item 8 is the open quark sub-leading mass correction in the Recognition mass ladder. This module builds a minimal theorem layer that would close it: a sign-split refined family whose active coefficient $c$ and mixing parameter $\eta$ are to be matched to residual data per sector.
A residual signature carries a sign class (positive or negative), generation steps $s_{12},s_{23}$, and a coupling $\kappa$. Coefficient triples are written $(c_{\mathrm{neg}}, c_{\mathrm{pos}}, \eta)$; only one of $c_{\mathrm{neg}},c_{\mathrm{pos}}$ is active for a given sign. The refined family maps a coefficient triple and a signature to a predicted residual pair.
The module already proves solvability and uniqueness of the active pair $(c,\eta)$ on each sign class (under nonzero gen12, nondegenerate cross-difference, distinct steps, nonzero $\kappa$). The present lemma isolates the unused-field freedom on the negative class.
proof idea
One-line term proof: unfold the refined-family definition by simp. On a negative signature the formula depends only on the active (negative) coefficient, $\eta$, the steps, and $\kappa$; the positive coefficient does not appear, so the two sides reduce to identical expressions.
why it matters
Feeds refined_neg_sector_closure, the full $\exists!$ statement for any negative sector: unique active $(c,\eta)$ matching the data, with arbitrary unused positive coefficient. The module summary lists this helper explicitly as the bridge from solvability plus uniqueness to sector closure (item 5 of the proved list).
Without unused-field irrelevance, uniqueness would be stated only up to a fixed dummy coefficient; the closure theorem needs free variation of that dummy so the existential quantifier ranges over genuine physical parameters alone. That is the last algebraic bookkeeping step before the negative-sector Item 8 target is closed in Lean. The twin statement for positive signatures (unused negative coefficient free) plays the same role on the other sign class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.