four_eq_F2sq
plain-language theorem explainer
The equality asserts that the number of colors required by the four color theorem equals the cardinality of the two-dimensional vector space over the field with two elements. Researchers working on Recognition Science derivations of the four color theorem would cite this equality to link the color count directly to the F₂² structure. The proof is a one-line decision procedure that reduces the numerical equality 4 = 2².
Claim. The number of colors required by the four color theorem equals the cardinality of the two-dimensional vector space over the field with two elements, i.e., $4 = |F_2^2|$.
background
The module derives the four color theorem from the Recognition Science lattice at D=3, where 4 equals D+1 and also equals 2². The definition fourColors sets the color count to 4. The definition f2sq_card sets the cardinality to 2^2, described in its doc-comment as '4 colors = |F₂²| (2-bit space)'.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality of the two constant definitions.
why it matters
This equality is packaged inside the fourColorCert record alongside fourColors_eq_DplusOne and fourColors_eq_2sq. It supplies the direct identification of the color count with the F₂² structure required by the RS derivation, consistent with the forcing chain step that fixes D=3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.