q3Edges_factored
plain-language theorem explainer
The equality confirms that the edge count of the recognition lattice Q3 equals twelve, which factors as three times four and matches the form D times two to the power of D minus one at D equals three. Researchers deriving lattice properties from Recognition Science would cite this to verify the twelve-edge count. The proof evaluates the equality by direct computation via the decide tactic.
Claim. The number of edges in the recognition lattice $Q_3$ equals $3$ times $4$, matching the expression $3$ times $2^{3-1}$ evaluated at spatial dimension $D=3$.
background
The module introduces the recognition lattice $Q_3 = {0,1}^3$ as the prototypical graph with eight vertices equal to $2^D$ and twelve edges equal to $3$ times $2^{D-1}$ for $D=3$. It is bipartite with chromatic number two. Upstream definitions supply the edge count once as the constant twelve and once as the expression $3$ times $2^{3-1}$.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the numerical equality between the two expressions for the edge count.
why it matters
This supplies the factored edge count to the graphTheoryCert certificate that collects vertex, edge, chromatic, and factored-edge facts for the recognition lattice. It aligns with the framework step that forces three spatial dimensions from the eight-tick octave. The certificate uses this fact to certify graph-theoretic consequences of the Recognition Science derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.