q3Cert
plain-language theorem explainer
q3Cert bundles the vertex, edge, face counts, Euler relation, Laplacian trace, automorphism order, face-pair count and simplex-vertex count for the three-dimensional hypercube into one structure. Recognition Science derivations of lattice corrections for D equals 3 cite this certificate when fixing the structural constants that enter the eta-one term. Construction proceeds by reflexivity on the direct combinatorial equalities together with delegation to the pre-proved Euler, trace and face-pair theorems.
Claim. The structure asserts that the 3-cube satisfies $V=8$, $E=12$, $F=6$, $V+F=E+2$, Laplacian trace equals degree times vertices, automorphism order equals 48, face-pair count equals 18, and simplex-vertex count equals 4.
background
The module records the combinatorial skeleton of the 3-cube Q3, the unit cell of the integer lattice Z^3, together with its graph-Laplacian invariants. Upstream, face_pairs from ParticleGenerations returns the number of opposite-face pairs on a D-cube, while aut_order from SpectralEmergence returns the order of the hyperoctahedral group B_D. The simplex-vertex count is defined locally as degree plus one, which equals four when D equals 3.
proof idea
The definition constructs the Q3Cert record by reflexivity on the vertex, edge, face, automorphism-order and simplex-vertex fields. The Euler characteristic is supplied directly by the theorem Q3_euler, the trace identity by Q3_trace, and the face-pair count by Q3_face_pair_count_eq.
why it matters
This certificate supplies the D=3 structural numbers required by the Recognition Science forcing chain at step T8, in particular the simplex-vertex count that appears in the eta-one correction. It closes the combinatorial prerequisites for the spectral-emergence calculations that adjust critical exponents on the lattice. The construction therefore anchors the eight-tick octave and three-dimensional spatial structure before any phi-ladder mass formulas are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.