middle_pair_unique_nonzero
plain-language theorem explainer
The theorem shows that among natural cube invariants at D=3 the only distinct nonzero pair summing to 17 is six and eleven in either order. Mass enumeration work in Recognition Science cites this to lock in the middle pair of the generation-step partition. The proof applies the inclusive enumeration of all pairs summing to 17 and then discards the zero cases by direct contradiction with the nonzero hypotheses.
Claim. Let $S$ be the set of natural invariants at dimension 3. For all $b,c$ in $S$, if $b+c=17$, $b≠c$, $b≠0$ and $c≠0$, then $(b=6∧c=11)∨(b=11∧c=6)$.
background
The module narrows the open forcing step for generation values by imposing partition constraints on pairs drawn from natural invariants at D=3. These invariants collect cell counts and simple combinations with direct Q₃-combinatorial meaning: vertex count 8, face count 6, passive edges 11 (=E-A), and derived values such as 13 (=V+F-C). The definition natural_invariants_D3 assembles them as the explicit list [1,6,7,8,11,12,13,14,15,17,18,20,25,26]. This theorem rests on the upstream result middle_pairs_are_11_6, whose docstring states it enumerates all pairs summing to 17 from the same list, including the zero-inclusive cases.
proof idea
The term proof introduces b and c under the stated hypotheses, invokes middle_pairs_are_11_6 to obtain one of four disjuncts, then performs case analysis: the first two disjuncts are returned directly as the desired conclusion, while the remaining two (the zero cases) are ruled out by applying absurd to the supplied nonzero assumptions.
why it matters
The result is used by thirteen_natural_interpretations, which records three equivalent natural-invariant readings of the value 13. It closes the structural half of the gap identified in the module docstring between proving Q₃ cell counts and deriving them as generation steps. Within the Recognition framework it supports the D=3 forcing (T8) and the uniqueness of the middle rung on the phi-ladder by fixing the lepton middle pair once zeros are excluded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.