signClass_collapse_to_refined
plain-language theorem explainer
When the two η slots of the sign-class residual family are set to the same value, that family coincides pointwise with the refined residual family that carries a single universal η. Item-8 workers closing the sub-leading mass law cite this as the bridge between the two coefficient presentations. The proof is a definitional collapse: unfold both families and case on the signature sign.
Claim. For real coefficients $c_N$, $c_P$, $\eta$ and any residual signature $\sigma$ (sign bit, positive rung steps $s_{12}, s_{23}$, and coupling), the sign-class residual family at coefficients $(c_N,\eta,c_P,\eta)$ equals the refined residual family at $(c_N,c_P,\eta)$.
background
Module Item8ClosureTarget builds the smallest precise theorem layer that would close Recognition Science Item 8: the open quark sub-leading mass correction, and make the all-sector generalization falsifiable against PDG residuals.
A ResidualSignature packages the sector data for that law: a sign bit (BpowSign), the sector-specific SDGT rung spacings step12 and step23 (cube-cell counts from the $Q_3$ decomposition), a real coupling, and positivity of the steps. Two generation residuals ($1\to 2$ and $2\to 3$) are the observables.
Two coefficient presentations appear. The sign-class family carries separate active coefficients and separate η slots for the two sign classes. The refined family uses a single universal η together with $(c_N,c_P)$. This lemma records the obvious specialization: equal η slots make the two presentations identical.
proof idea
Purely definitional. simp only unfolds signClassFamily and refinedFamily to their case-on-sign bodies. A cases on sig.sign splits into the negative and positive branches; each branch reduces by rfl because the two η arguments were already identical in the hypothesis, so the residual expressions match termwise. No arithmetic lemmas are required.
why it matters
Listed in the module summary as proved item 6 of the Item-8 closure stack. Upstream in the same file, consistency of the plain ratio family forces a linear relation that PDG data violates; the η-corrected refined family restores solvability and uniqueness (refinedFamily_*_solvable/unique, refined_neg_sector_closure). This collapse lemma licenses rewriting between the sign-class coefficient tuple (four slots, two η) and the refined triple $(c_N,c_P,\eta)$ whenever the two η values agree, so uniqueness and existence statements proved in the refined language transfer to the equal-η sign-class language without extra work.
No downstream consumers are wired yet (used_by empty); the intended landing is the concrete PDG+RS instantiation section that follows, and ultimately a single falsifiable all-sector residual law on the φ-ladder mass formula. It does not itself touch T5–T8 or the RCL; it is bookkeeping inside the mass-correction closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.