q3Bipartite
plain-language theorem explainer
The declaration asserts that the chromatic number of the recognition lattice Q₃ equals 2. A researcher extracting discrete graph models from Recognition Science would cite this when confirming that Q₃ admits a 2-coloring consistent with even-odd parity. The proof is a one-line reflexivity that follows immediately from the definition of the chromatic number.
Claim. The chromatic number of the recognition lattice $Q_3$ equals 2.
background
The module develops graph-theoretic consequences of Recognition Science for the lattice $Q_3 = {0,1}^3$. This structure has 8 vertices ($2^D$ with $D=3$) and 12 edges ($D × 2^{D-1}$), and is bipartite by splitting vertices into even and odd parity classes. The upstream definition q3ChromaticNumber : ℕ := 2 directly encodes the chromatic number as 2, matching the bipartiteness property stated in the module documentation.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity (rfl) to the definition of q3ChromaticNumber.
why it matters
This result records that Q₃ is bipartite with chromatic number 2, a core property of the prototypical graph in the Recognition framework. It supports the eight-tick octave (T7) and the forcing of D=3 spatial dimensions (T8) by confirming the lattice admits a 2-coloring. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.