middle_pair_unique_nonzero
plain-language theorem explainer
The theorem shows that the only distinct nonzero elements of the natural invariants at D=3 that sum to 17 are the pair 6 and 11 in either order. Mass-step enumeration work in Recognition Science cites this to confirm uniqueness of the lepton middle pair before handling endpoints. The proof is a term-mode wrapper that invokes middle_pairs_are_11_6 and discards the two zero cases by contradiction with the nonzero hypotheses.
Claim. Let $S$ denote the set of natural invariants at dimension 3 (the integers admitting direct combinatorial interpretation as cell counts or simple combinations on the 3-cube). For all $b,c$ in $S$ such that $b+c=17$, $b≠c$, $b≠0$ and $c≠0$, one has $(b=6∧c=11)∨(b=11∧c=6)$.
background
The module narrows the open forcing step left by SectorDependentTorsion by imposing partition constraints on the total N_3=55. The middle pair is required to sum to W=17. The set of natural invariants is defined explicitly as the list [1,6,7,8,11,12,13,14,15,17,18,20,25,26], each element corresponding to a Q_3 cell count or simple combination (V=8, F=6, E-A=11, etc.). This choice makes the modeling decision explicit rather than hidden.
proof idea
The term proof introduces b, c and the six hypotheses, obtains a four-way disjunction from the upstream lemma middle_pairs_are_11_6, returns the first two disjuncts directly as the desired pairs, and discharges the remaining two (the zero cases) by applying absurd to the nonzero hypotheses.
why it matters
The result is used by thirteen_natural_interpretations. It supplies the first of the two structural constraints enumerated in the module documentation (uniqueness of the lepton middle pair excluding zero). Within the Recognition framework it advances the enumeration of generation steps under the explicit D=3 natural invariants, thereby closing one modeling gap between combinatorial cell counts and the observed mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.