q3Chromatic_eq
plain-language theorem explainer
The equality asserts that the chromatic number of the recognition lattice Q₃ equals 2. Researchers extracting graph invariants from Recognition Science cite it to confirm bipartiteness of the 3-cube. The proof is a direct reflexivity step on the constant definition of the chromatic number.
Claim. The chromatic number of the graph $Q_3$ satisfies $χ(Q_3)=2$.
background
The module defines the recognition lattice Q₃ as the graph on vertex set {0,1}³. This graph carries 8 vertices and 12 edges and splits into two independent sets of size 4 by parity. The sibling definition q3ChromaticNumber sets the chromatic number directly to the constant 2, matching the bipartition property stated in the module documentation.
proof idea
The proof is a one-line reflexivity that equates the defined value of q3ChromaticNumber to the numeral 2.
why it matters
This equality populates the chromatic_2 field inside the graphTheoryCert bundle that collects the core invariants of Q₃. It anchors the eight-tick octave (T7) and the emergence of D=3 in the forcing chain by confirming that the prototypical graph is 2-colorable without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.