q3Edges
plain-language theorem explainer
The declaration supplies the edge count of the three-cube graph Q3 as the constant 12. Researchers working on Recognition Science embeddings or Euler characteristic verifications cite this value when confirming that Q3 realizes the topological sphere with characteristic 2. The definition is a direct numerical assignment that matches the upstream algebraic form 3 * 2^(3-1).
Claim. The three-dimensional hypercube graph $Q_3$ has exactly 12 edges.
background
The module treats Q3 as the canonical recognition lattice for spatial dimension 3, listing 8 vertices, 12 edges, and 6 faces. Euler characteristic is defined as V - E + F and equals 2, reproducing the sphere topology. The upstream definition in GraphTheoryFromRS computes the same quantity via the closed form 3 * 2^(3-1), which evaluates to 12 and supplies the numerical anchor used here.
proof idea
This is a direct definition that assigns the constant 12. It aligns with the upstream expression 3 * 2^(3-1) without further reduction steps.
why it matters
The value feeds q3EulerChar, which computes the Euler characteristic 2, and populates the GraphTheoryCert structure that records the five canonical graph theorems for configDim D = 5. It thereby supports the Recognition Science claim that Q3 is the lattice realizing D = 3 with the eight-tick octave structure. No open scaffolding remains for this numerical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.