fourColors_eq_2sq
plain-language theorem explainer
The equality sets the constant fourColors equal to 2 squared, confirming that the color count matches the cardinality of the two-dimensional vector space over F_2. Researchers assembling Recognition Science derivations of the four color theorem would cite this step when linking the bound to the underlying 2-bit lattice. The proof is a one-line decide tactic that evaluates the natural-number equality by direct computation.
Claim. The number of colors required by the four color theorem equals the cardinality of the vector space over the field with two elements: $4 = 2^2$.
background
The module treats the four color theorem as a structural consequence of the Recognition Science lattice at spatial dimension D = 3. The constant fourColors is introduced as the natural number 4, with the observation that this bound equals D + 1 and also equals the order of F_2^2 whose elements {00, 01, 10, 11} label admissible color assignments. The upstream definition supplies fourColors : ℕ := 4 directly as the left-hand side of the target equality.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality fourColors = 2 ^ 2. The tactic reduces both sides to concrete natural numbers and confirms the identity by decidable computation.
why it matters
This identity is packaged into the FourColorCert structure together with the companion relations fourColors = D + 1 and the explicit identification with F_2^2. It supplies the algebraic link that closes the Recognition Science account of the tight four-color bound arising from the D = 3 recognition lattice and the eight-tick octave structure. No open scaffolding remains for this specific equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.