Q3_edge_count
plain-language theorem explainer
The edge count in the 3-cube graph satisfies the handshaking relation for a 3-regular graph on 8 vertices. Researchers deriving flux quantities or passive-edge counts in Recognition Science cite this identity when connecting Q3 geometry to congruence primes. The proof is a one-line wrapper that unfolds the three constant definitions and applies arithmetic simplification via omega.
Claim. Let $E$ be the number of edges, $d$ the regular degree, and $V$ the number of vertices in the 3-cube graph $Q_3$. Then $E = d V / 2$.
background
The CubeSpectrum module formalizes combinatorial and spectral properties of the 3-cube $Q_3$, the unit cell of the integer lattice in Recognition Science. It records the standard counts: 8 vertices, degree 3, and 12 edges. Upstream results supply independent derivations of these counts, including $V 3 = 8$ and $E 3 = 12$ in SpectralEmergence together with the closed forms $2^3$ and $3*2^2$ in AlphaHigherOrder.
proof idea
The proof is a one-line wrapper that unfolds Q3_edges, Q3_degree, and Q3_vertices then invokes the omega tactic to discharge the resulting arithmetic equality.
why it matters
This identity is invoked by every downstream congruence theorem in the RamanujanBridge, including congruence_prime_11_is_passive_edges (which obtains 11 = edge count minus 1) and congruence_primes_sum_eq_flux (which equates the sum of primes 5+7+11+1 to the directed flux). It supplies the geometric link between the eight-tick octave (T7) realized by the 8 vertices and the three spatial dimensions (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.