refined_at_eta_zero
plain-language theorem explainer
At vanishing η, the refined residual family reduces exactly to the original sign-split ratio family on any residual signature. Citation target for anyone specializing the Item 8 sub-leading mass ansatz or checking that the η-extension is conservative. Proof is a one-line simp that unfolds both families and cancels the zero-η terms via ring identities.
Claim. For any real coefficients $c_N$, $c_P$ and any residual signature $\sigma$, the refined family at $(c_N, c_P, \eta=0)$ equals the sign-split ratio family at $(c_N, c_P)$ evaluated on $\sigma$.
background
Item 8 of the Recognition Science verification program concerns a unified sub-leading mass correction across lepton and quark sectors. The module builds the smallest precise theorem layer that would close that item and make the all-sector generalization falsifiable.
A residual signature packages the sector data needed for the correction law: a sign class (positive or negative $B$-power), two positive SDGT rung spacings step12 and step23 (cube-cell counts from the $Q_3$ decomposition), and a real coupling. The sign-split ratio family is the original two-coefficient ansatz in $(c_N, c_P)$. The refined family adds a third real parameter $\eta$ that absorbs the consistency obstruction forced by the ratio family (the rigidity gen12·s₁₂ + gen23·s₂₃ = 0, which PDG data violates).
This lemma records the specialization at $\eta = 0$: the refined law must recover the original ratio law, so the extension is conservative rather than a replacement.
proof idea
One-line wrapper. Unfold both refinedFamily and ratioFamily, then discharge the resulting arithmetic with simp only using zero_mul, add_zero, sub_zero, and mul_one. Every $\eta$-dependent summand vanishes or becomes the identity factor, leaving the two families identical as functions of the residual signature.
why it matters
Inside the Item 8 closure target, the refined family is the working ansatz that restores solvability and uniqueness of $(c, \eta)$ per sector after the ratio family is shown structurally rigid against data. This identity is the base-case sanity check: the refined law is a genuine one-parameter extension of the sign-split law, not an unrelated formula. It underwrites the narrative that $\eta$ is the unique continuous deformation parameter absorbing the consistency violation, and that setting $\eta = 0$ returns the original prediction surface. No downstream theorems currently depend on it in the graph, but it is the natural rewrite step whenever a proof specializes refined-family identities to the ratio-family regime (e.g., comparing consistency_of_ratioFamily with refined solvability/uniqueness).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.