f2sq_card
plain-language theorem explainer
f2sq_card defines the cardinality of the vector space F₂² as four. Researchers deriving the four color theorem from Recognition Science cite this value when equating colors to the size of the 2-bit field at D=3. The definition is a direct power computation with no lemmas required.
Claim. The cardinality of the finite vector space $F_2^2$ equals 4.
background
The module derives the four color theorem from Recognition Science by identifying four colors with the elements of F₂², the two-dimensional vector space over the field with two elements. This space contains the pairs (0,0), (0,1), (1,0), (1,1). The module states that four equals D+1 at spatial dimension D=3 and also equals 2², with all equalities decided by computation.
proof idea
The declaration is a direct definition that evaluates 2 raised to the power 2.
why it matters
This supplies the explicit integer value used inside the FourColorCert structure and the theorem four_eq_F2sq. It completes the identification of four colors with 2², which the module links to the D=3 recognition lattice from the forcing chain T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.