middle_pairs_are_11_6
plain-language theorem explainer
The theorem establishes that among natural cube invariants at D=3, the only distinct pairs summing to 17 are the lepton middle pair {6,11} together with the trivial pairs involving zero. Researchers narrowing generation-step values on the Recognition Science mass ladder would cite this to confirm the middle rung constraint. The proof is a term-mode argument that unfolds list membership via simplification and discharges the resulting arithmetic cases with linear arithmetic.
Claim. Let $S$ be the set of natural invariants at dimension 3, given explicitly as the list of integers with direct $Q_3$-combinatorial interpretations: $S = [1,6,7,8,11,12,13,14,15,17,18,20,25,26]$. For all $b,c$ in $S$ such that $b+c=17$ and $b≠c$, either $(b=6∧c=11)$ or $(b=11∧c=6)$ or $(b=17∧c=0)$ or $(b=0∧c=17)$.
background
The module Step Value Enumeration narrows the open gap between proved $Q_3$ cell counts and their identification as generation steps. The key definition natural_invariants_D3 supplies the explicit list [1,6,7,8,11,12,13,14,15,17,18,20,25,26] consisting of vertex count V=8, face count F=6, passive edges E-A=11, and other simple combinations that admit direct combinatorial meaning in the 3-cube. The module documentation states that the four generation-step values {13,11,6,8} are already proved $Q_3$ invariants, while their appearance as steps remains identified from PDG data rather than derived.
proof idea
The term proof introduces b, c and the four hypotheses, then applies simp to unfold natural_invariants_D3 together with List.mem_cons. This reduces the statement to a finite collection of arithmetic equalities and inequalities, which the omega tactic solves directly.
why it matters
The result is used by the sibling theorem middle_pair_unique_nonzero, which adds the nonzero hypotheses to isolate the lepton middle pair {6,11}. It supplies the first structural constraint enumerated in the module, confirming uniqueness of the middle pair under the natural-invariant set. This step narrows Gap A in the Validation Program and supports the explicit modeling choice of the invariant list within the D=3 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.