Q3_face_pair_count_eq
plain-language theorem explainer
The equality Q3_face_pair_count = 18 holds by direct unfolding from the definition 2 * Q3_degree^2. Physicists modeling critical exponent corrections in Recognition Science cite this identity for the η₂ term when D = 3. The proof is a one-line wrapper that unfolds the two definitions and resolves the arithmetic via the omega tactic.
Claim. In the three-dimensional hypercube graph, the face-pair count satisfies $2D^2 = 18$ where $D = 3$.
background
The CubeSpectrum module formalizes combinatorial and spectral properties of the 3-dimensional hypercube Q₃ (unit cell of ℤ³), which has 8 vertices, 12 edges, 6 faces, and Laplacian eigenvalues {0, 2, 2, 2, 4, 4, 4, 6}. The face-pair count is defined as 2 * Q3_degree^2 and is identified as the structural number appearing in the η₂ correction. This sits inside the Recognition Science setting where D = 3 spatial dimensions are forced at step T8 of the unified forcing chain.
proof idea
The proof is a one-line wrapper that unfolds the definitions of Q3_face_pair_count and Q3_degree, then applies the omega tactic to discharge the resulting arithmetic equality.
why it matters
This identity supplies the combinatorial count required by the downstream q3Cert definition, which assembles the full certificate for Q3 vertices, edges, faces, Euler characteristic, and trace. It fills the η₂ structural number in the critical exponent corrections, consistent with the eight-tick octave and D = 3 forced in the Recognition Science chain. The parent q3Cert incorporates the equality to certify the cube spectrum for use in quantum channel and forcing calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.