Q3_trace
plain-language theorem explainer
The sum of the eight Laplacian eigenvalues of the three-dimensional hypercube equals its degree times its vertex count. Researchers working on spectral graph invariants in Recognition Science cite this identity to close the trace check inside the Q3 certificate. The proof is a one-line wrapper that unfolds the explicit eigenvalue list, the constant degree 3, and the vertex count 8, then lets native_decide confirm the arithmetic equality.
Claim. Let $Q_3$ be the three-dimensional hypercube with Laplacian eigenvalues listed as $0,2,2,2,4,4,4,6$. Then the sum of these eigenvalues equals $3$ times the number of vertices.
background
The CubeSpectrum module records the combinatorial and spectral data of the 3-cube $Q_3$, the unit cell of the integer lattice in three dimensions. It supplies the explicit list of Laplacian eigenvalues, the constant degree 3, and the vertex count 8. Upstream definitions in AlphaHigherOrder, LambdaRecDerivation, PlanckScaleMatching, and SpectralEmergence each record the same vertex count 8, sometimes as $2^3$ and sometimes as the order of the hyperoctahedral group in dimension 3.
proof idea
The proof is a one-line wrapper that unfolds Q3_laplacian_eigenvalues, Q3_degree, and Q3_vertices, then applies native_decide to verify the numerical identity between the summed list and the product of degree and vertex count.
why it matters
Q3_trace supplies the trace field of the q3Cert record that packages the basic invariants of the cube. It completes the spectral verification step required by the CubeSpectrum module, which underpins critical-exponent corrections inside the Recognition framework where the spatial dimension is fixed at 3. The parent certificate q3Cert is the immediate downstream consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.