q3ChromaticNumber
plain-language theorem explainer
The definition assigns the chromatic number of the recognition lattice Q₃ to 2. Researchers deriving graph properties from Recognition Science cite this when confirming that the 3-cube graph is 2-colorable. The assignment is a direct constant definition that matches the bipartiteness property of the 8-vertex lattice.
Claim. The chromatic number of the recognition lattice $Q_3$ equals 2.
background
The module defines the recognition lattice $Q_3$ as the graph on vertex set {0,1}³. This graph has 8 vertices and 12 edges and is bipartite by parity of vertex weight. The chromatic number is the smallest number of colors such that no two adjacent vertices receive the same color. The upstream definition in GraphTheoryDepthFromRS states the same fact: Q₃ chromatic number: 2.
proof idea
This is a direct definition that sets the constant q3ChromaticNumber to the natural number 2. Equality theorems downstream apply reflexivity to this value.
why it matters
The definition supplies the chromatic_2 field required by the GraphTheoryCert structure, which records the core graph invariants of Q₃. It aligns with the framework landmark that Q₃ realizes the eight-tick octave for D = 3. Downstream results such as q3Chromatic_eq and q3Bipartite invoke this value to obtain the equality to 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.