fourColors_eq_DplusOne
plain-language theorem explainer
Equating the four color count to the spatial dimension plus one connects the four color theorem to the three-dimensional structure in Recognition Science. Graph theorists and Recognition Science researchers would cite this when deriving coloring bounds from the recognition lattice. The proof consists of a direct computation verifying that both sides equal four.
Claim. Let $C$ denote the number of colors required by the four color theorem and $D$ the spatial dimension. Then $C = D + 1$.
background
The module places the four color theorem inside Recognition Science by observing that four colors suffice for any planar map and that this count equals the spatial dimension plus one. Colors correspond to the four elements of the field F_2 squared, which is also two squared and equals two to the power of D minus one at D equals three. The equality rests on the sibling definitions that set the color count to four and the spatial dimension plus one to three plus one.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality of the two constant natural number definitions.
why it matters
The result supplies the four_eq_Dp1 field of the FourColorCert record that certifies the four color theorem derivation from Recognition Science. It implements the structural observation that four equals D plus one when D equals three, consistent with the forcing chain step that fixes three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.