f2sq_card
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the four color theorem for planar maps.
- Does not specify adjacency conditions for regions.
- Does not invoke the Recognition Composition Law or J-cost.
formal statement (Lean)
33def f2sq_card : ℕ := 2 ^ 2