Q3Cert
plain-language theorem explainer
The Q3Cert structure packages the vertex, edge, face, Euler, Laplacian-trace, automorphism-order and simplex-vertex counts for the three-cube graph. Lattice physicists and recognition theorists cite it when anchoring the D=3 case inside spectral corrections to scaling and the eta_1 term. It is realized as a record whose fields are populated directly by the module's constant definitions together with the already-established Euler and trace identities.
Claim. Let $Q_3$ be the graph of the three-dimensional hypercube. The structure asserts the equalities $V=8$, $E=12$, $F=6$, $V+F=E+2$, the sum of Laplacian eigenvalues equals degree times $V$, automorphism group order $48$, face-pair count $18$, and simplex vertex count $4$.
background
The module records combinatorial and spectral invariants of the 3-cube $Q_3$, the unit cell of the integer lattice $Z^3$. Its graph Laplacian has eigenvalues $[0,2,2,2,4,4,4,6]$ and its automorphism group has order $48$. The local setting is the Recognition Science treatment of cubic-lattice corrections, where these numbers enter the mass-ladder and RG-eigenvalue formulas.
proof idea
The declaration is a structure definition. Each field is filled by direct reference to the sibling constants (Q3_vertices, Q3_edges, Q3_faces, Q3_degree, Q3_aut_order, Q3_laplacian_eigenvalues) or by the already-proved Euler and trace theorems in the same file. No tactics beyond the record constructor are used.
why it matters
Q3Cert supplies the concrete D=3 data consumed by the downstream q3Cert instance that appears in AlphaHigherOrder and LambdaRecDerivation. It thereby closes the combinatorial side of the T8 step that forces three spatial dimensions and supplies the simplex vertex count 4 that enters the eta_1 correction. The structure therefore anchors the spectral-gap and symmetry inputs required by the Recognition Composition Law on the cubic lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.