q3Edges
plain-language theorem explainer
The definition computes the edge count of the recognition lattice Q₃ as 3 times 2 to the power of 2. Researchers verifying graph properties derived from Recognition Science cite this when confirming that the 3-dimensional hypercube has exactly 12 edges. The definition is a direct arithmetic expression that evaluates to the constant required by the eight-tick structure.
Claim. The number of edges in the recognition lattice $Q_3 = {0,1}^3$ is given by $3 × 2^{3-1}$.
background
The module derives graph-theoretic properties of the recognition lattice Q₃, the prototypical graph {0,1}³. Module documentation states that Q₃ has 8 vertices equal to 2^D and 12 edges equal to 3 × 2^(D-1) for D = 3, and is bipartite with chromatic number 2. The upstream definition in GraphTheoryDepthFromRS supplies the constant value 12 that this expression must match.
proof idea
This is a direct definition via the arithmetic expression 3 * 2 ^ (3 - 1). No lemmas or tactics are applied; the value is fixed at definition time and used verbatim in downstream certificates.
why it matters
This definition supplies the edge count that populates the GraphTheoryCert structure certifying vertices_8, edges_12, chromatic_2, and the factored form 3 * 4. It supports the framework claim that Q₃ has 12 edges via D × 2^(D-1) with D = 3, linking to the eight-tick octave and spatial dimensions. The result is referenced by q3Edges_eq, q3Edges_factored, and q3EulerChar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.