not_two_generations
plain-language theorem explainer
The theorem shows that a three-dimensional cube has a number of opposite face pairs unequal to two. Researchers deriving fermion generation counts from spatial dimension in Recognition Science cite this to exclude two-generation models. The proof is a direct numerical reduction that unfolds the face_pairs definition and compares the resulting integer to 2.
Claim. In three spatial dimensions the cube geometry $Q_3$ has a number of opposite face pairs not equal to two.
background
The module formalizes P-001 on the origin of three fermion generations. It starts from the forced value D = 3 (from DimensionForcing) and the cube geometry Q_3. The local definition face_pairs D := D counts the D pairs of opposite faces; each such pair is identified with one generation in the ledger mode structure. The upstream face_pairs in SpectralEmergence instead uses the combinatorial count D(D-1)/2, but the present theorem relies on the simpler local version.
proof idea
The proof is a one-line wrapper that applies norm_num to the face_pairs definition, reducing face_pairs 3 to the numeral 3 and discharging the inequality with 2 by reflexivity.
why it matters
This declaration closes the two-generation case inside the three-generations argument of P-001. It sits downstream of the D = 3 forcing step (T8 in the unified chain) and upstream of the full three_generations_from_dimension claim. The result reinforces that the eight-tick octave and phi-ladder fix D = 3, after which the cube admits exactly three face-pairs and no other integer count is possible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.