same_signature_same_prediction
plain-language theorem explainer
Equal residual signatures produce identical predicted residual pairs under any fixed pair of global ratio-family coefficients. Citation target for anyone arguing that sector predictions carry no hidden knobs once the signature is fixed. The proof is pure substitution plus reflexivity: equality of inputs forces equality of the pure function outputs.
Claim. Fix any pair of global ratio-family coefficients $(c_{-}, c_{+})$. If two residual signatures $\sigma_1$ and $\sigma_2$ (each a sign class, two positive SDGT rung steps, and a coupling) are equal as structures, then the predicted residual pairs they induce under those coefficients coincide: $\widehat{R}(c_{-},c_{+};\sigma_1)=\widehat{R}(c_{-},c_{+};\sigma_2)$.
background
Item 8 is the open quark sub-leading mass correction in the Recognition Science ledger. This module builds the smallest precise target that would close it: a sign-split ratio family with only two global coefficients, applied to sector residual signatures, so that later lepton, genetic, and theta instantiations become out-of-sample tests rather than new fits.
A residual signature packages the structural data of one sector's sub-leading law: a $B_{\mathrm{pow}}$ sign class, the two SDGT rung spacings (cube-cell counts from the $Q_3$ decomposition) for generations $1\to 2$ and $2\to 3$, a real coupling, and positivity of the steps. Ratio-family coefficients are exactly the two globals $(c_{-},c_{+})$ allowed by the candidate family. Predicted residuals map those coefficients and a signature to the two generation residual corrections.
The surrounding proved results already give solvability and uniqueness of refined-family coefficients on each sign sector, plus a consistency identity that the plain sign-split family forces and that PDG data violates (hence the $\eta$ refinement).
proof idea
One-line congruence. Substitute the hypothesis that the two signatures are definitionally equal, then close by reflexivity of equality on the pure function predictedResiduals. No algebraic cancellation, no appeal to uniqueness or solvability lemmas; the claim is just that the prediction map is a well-defined function of its signature argument.
why it matters
Doc-comment frames this as the precise no-extra-knob property needed for later out-of-sample tests. Once Item 8 is closed by fixing both quark residual pairs inside one family and freezing $(c_{-},c_{+})$, every subsequent sector prediction must depend only on the structural signature; equal signatures must not be allowed to diverge by hidden parameters. This lemma records that functional dependence formally.
It sits beside the module's closure target proposition (exact up/down quark residual pairs inside one family) and the consistency / refined-family uniqueness chain. No downstream consumers are wired yet (used_by is empty), so it is infrastructure for the falsifiable all-sector generalization rather than a step already consumed by a parent theorem. Framework-wise it supports the mass-ladder story (yardstick times $\phi$ to a rung offset) by guaranteeing that sub-leading corrections are signature-determined once the two globals are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.