q3Edges_eq
plain-language theorem explainer
The equality q3Edges = 12 confirms that the recognition lattice Q₃ has exactly twelve edges under the formula 3 × 2^(D-1) at D=3. Researchers deriving graph properties from Recognition Science cite it when assembling the GraphTheoryCert record. The proof is a one-line decision procedure that evaluates the arithmetic expression directly.
Claim. The edge count of the recognition lattice Q₃ = {0,1}³ equals 12, i.e., |E(Q₃)| = 12.
background
The module defines the recognition lattice Q₃ = {0,1}³ as the prototypical graph with 8 vertices = 2^D and 12 edges = 3 × 2^(D-1), each of the three axes contributing four edges. The upstream definition q3Edges : ℕ := 3 * 2 ^ (3 - 1) supplies the expression whose concrete value is asserted here. The companion definition in GraphTheoryDepthFromRS simply hard-codes the same integer 12.
proof idea
This is a one-line wrapper that applies the decide tactic to evaluate the natural-number equality 3 * 2^(3-1) = 12.
why it matters
The result populates the edges_12 field of graphTheoryCert, which certifies the full set of Q₃ graph properties required by the Recognition Science derivation. It directly instantiates the T8 step that forces D = 3 spatial dimensions together with the eight-tick octave structure. No open scaffolding remains for this particular equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.