natural_invariants_D3
plain-language theorem explainer
The declaration enumerates the natural invariants at D=3 as the explicit finite list of integers with direct Q3-combinatorial interpretations. Mass generation researchers cite this set when constraining possible step values in the lepton sector and proving pair uniqueness. The definition consists of a direct listing drawn from vertex, edge, face, and cell counts together with their sums and differences.
Claim. Let $I_{D=3}$ denote the set of natural invariants at three spatial dimensions. Then $I_{D=3} = [1, 6, 7, 8, 11, 12, 13, 14, 15, 17, 18, 20, 25, 26]$, the integers arising as the 3-cube cell counts $V=8$, $E=12$, $F=6$, $C=1$ and their combinations such as $2V+1=17=W$ and $V+F-C=13$.
background
The module narrows the remaining gap between proved Q3 cube invariants and their use as generation steps. The natural invariants are the integers with direct combinatorial meaning at D=3: vertex count V=8, edge count E=12 (with E-A=11 for passive edges), face count F=6, cell count C=1, together with sums and differences such as V+F=14, V-C=7, V+F-C=13, 2V+1=17=W (wallpaper groups), V+E=20, E+F=18, V+E+F=26, and E-C=11. The module doc-comment states that these integers are enumerated to make explicit the modeling choice of the candidate set for step values.
proof idea
The definition is a direct listing of the integers identified in the doc-comment. No lemmas or tactics are applied; the body is the explicit finite list of natural numbers satisfying the listed Q3-combinatorial conditions.
why it matters
This definition supplies the explicit candidate pool referenced by the downstream theorems endpoint_pairs_not_unique, middle_pairs_are_11_6, and middle_pair_unique_nonzero. Those results establish that the middle pair summing to W=17 is uniquely {11,6} (excluding zero) while multiple endpoint pairs summing to 21 exist within the set. It fills the enumeration step in the module's program for narrowing the open forcing gap between proved cell counts and PDG-identified generation steps {13,11,6,8}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.