FourColorCert
plain-language theorem explainer
FourColorCert packages three equalities showing that the color count for planar maps equals both the spatial dimension plus one and the cardinality of the two-bit field. Researchers deriving the four color theorem from Recognition Science would cite this certificate when confirming the numerical identities that follow from D equals 3. The definition is realized as a structure that directly bundles the constant definitions without additional computation or lemmas.
Claim. A certificate structure asserting the identities $4 = 3 + 1$, $4 = 2^2$, and $4 = |F_2^2|$ for the number of colors sufficient to color any planar map.
background
In this module the constant fourColors is defined as the natural number 4. The quantity spatial dimension plus one is defined as 3 plus 1. The cardinality f2sq_card is defined as 2 raised to the power 2, which counts the elements of the vector space F₂². These definitions are supplied by the upstream declarations in the same module. The local theoretical setting is the Recognition Science claim that the four color theorem follows from the D equals 3 recognition lattice structure, where colors correspond to the four elements of F₂² and the bound 4 equals both D plus 1 and 2 squared.
proof idea
The declaration is a structure definition that bundles the three equalities between the color count, the spatial dimension plus one, two squared, and the cardinality of the two-bit field. It is a direct one-line wrapper around the constant definitions supplied by the upstream results; no tactics or further lemmas are invoked.
why it matters
This certificate is consumed by the downstream fourColorCert definition to record the numerical matches required for the Recognition Science derivation of the four color theorem. It implements the module's structural observation that 4 equals D plus 1 and 2 squared, which rests on the T8 step of the unified forcing chain that forces three spatial dimensions. The module notes that four colors is the tight bound while five colors would be trivially sufficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.