Q3_degree
plain-language theorem explainer
Q3_degree fixes the dimension parameter of the hypercube graph Q3 at the natural number 3. Lattice theorists and Recognition Science researchers cite it when deriving automorphism orders, edge counts, and spectral ratios for the unit cell of Z^3. The declaration is a direct constant assignment with no further computation.
Claim. Let $D$ denote the dimension of the hypercube graph $Q_3$. Then $D = 3$.
background
The module formalizes combinatorial and spectral properties of the 3-dimensional hypercube Q3, the unit cell of Z^3, which has 8 vertices, 12 edges, and 6 faces. Its Laplacian eigenvalues are {0, 2, 2, 2, 4, 4, 4, 6} with multiplicities {1, 3, 3, 1}, and its automorphism group is S4 times Z2^3 of order 48. Q3_degree supplies the fixed dimension D = 3 that parametrizes all counts and ratios in the module.
proof idea
Direct definition that assigns the constant 3 to Q3_degree in the natural numbers.
why it matters
This definition anchors the CubeSpectrum module by setting D = 3, matching the spatial dimension T8 of the Recognition Science forcing chain. It is referenced by Q3_aut_order_eq (which proves |Aut(Q3)| = D! * 2^D), Q3_edge_count (which derives edges = D * vertices / 2), Q3_face_pair_count (which yields 2D^2 = 18 for the eta2 correction), and Q3Cert (which certifies Euler and trace relations). It also supplies the simplex vertex count D + 1 = 4 used in the eta1 correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.