Q3_face_pair_count
plain-language theorem explainer
The definition sets the face-pair count for the three-dimensional hypercube graph to twice the square of its degree, which evaluates to 18 when the degree is 3. Researchers modeling critical-exponent corrections in Recognition Science cite this constant for the η₂ term. The definition is a direct algebraic substitution of the fixed degree value.
Claim. The face-pair count is defined by the expression $2D^2$, where $D$ is the degree of the graph of the three-dimensional hypercube $Q_3$.
background
The module establishes the combinatorial and spectral properties of the 3-cube $Q_3$, the unit cell of the integer lattice in three dimensions. It records that $Q_3$ possesses 8 vertices, 12 edges and 6 faces, together with Laplacian eigenvalues whose multiplicities are fixed by the automorphism group of order 48. The sibling definition Q3_degree fixes the numerical value 3 that enters every subsequent count in the module.
proof idea
The declaration is a one-line definition that directly substitutes the constant Q3_degree into the expression 2 * D^2.
why it matters
This definition supplies the integer 18 that is collected inside the Q3Cert structure and discharged by the companion equality theorem Q3_face_pair_count_eq. It furnishes the structural number required for the η₂ correction in the Recognition Science treatment of critical exponents on the cube spectrum. The parent structure Q3Cert assembles all such constants to certify the hypercube data used in the spectral-gap and trace identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.