fourColorCert
plain-language theorem explainer
The fourColorCert definition assembles a structure certifying that the number of colors needed for planar maps equals the spatial dimension plus one, equals four, and equals the size of the two-bit field. Mathematicians deriving the four color theorem from Recognition Science foundations would reference this as the explicit witness. It is constructed by directly referencing three decide-based equality theorems.
Claim. Let $n$ be the minimal number of colors sufficient to color any planar map so that no two adjacent regions share a color. There exists a certificate $C$ satisfying $n = D + 1$, $n = 2^2$, and $n = |F_2^2|$, where $D$ denotes the number of spatial dimensions.
background
In the Recognition Science framework the four color theorem follows from the D=3 recognition lattice. The module states that four colors suffice and are tight, with colors identified with the four elements of the vector space F_2^2. The upstream theorems fourColors_eq_DplusOne, fourColors_eq_2sq and four_eq_F2sq each establish one of the required equalities by decision.
proof idea
The definition is a one-line wrapper that populates the FourColorCert structure by assigning the three fields directly to the corresponding decide-proved theorems: fourColors_eq_DplusOne supplies the dimension equality, fourColors_eq_2sq supplies the square equality, and four_eq_F2sq supplies the field-cardinality equality.
why it matters
This definition supplies the concrete certificate for the four color theorem in the RS mathematics module, linking the color count to the spatial dimension D=3 from the forcing chain T8. It completes the structural observation that 4 = D + 1 and 4 = 2^2. All supporting equalities are decided with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.