Q3_face_pair_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the degree or the face count from first principles of graph theory.
- Does not extend the count to hypercubes of dimension other than three.
- Does not compute any eigenvalue multiplicities or spectral ratios.
- Does not address the automorphism group order or the explicit Laplacian spectrum.
formal statement (Lean)
80def Q3_face_pair_count : ℕ := 2 * Q3_degree ^ 2
proof body
Definition body.
81