Triangle corner parity equals odd-multiplicity red–green edge parity
ProvedProofsInTheBook.Chapter20.sum_triangleLocalRGCount_mod_two_eq_oddAtomicLet D be a SquareDissection: a natural number n, a finite vertex type with decidable equality and injective real-plane coordinates, and n nondegenerate vertex triples whose closed convex hulls cover exactly , have pairwise disjoint topological interiors, and each have area (the rational quotient embedded in the reals). Area is half the absolute determinant. Triangle sides are subdivided at all vertices lying strictly between their endpoints, ordered by affine parameter. Consecutive vertices form unordered atomic edges; multiplicity counts occurrences across the triangle boundary lists. T-junctions and unused vertices are permitted. No oddness assumption on n is made here.
Color each vertex by its coordinates using the chosen real 2-adic Monsky coloring. For triangle i let r_i be the number of red–green pairs among its three corner pairs. For an unordered vertex pair e let m(e) be its atomic multiplicity. Then
The set on the right ranges over all unordered pairs of D-vertices, including the diagonal convention; pairs of zero multiplicity do not contribute. This is a parity equality and does not itself assert oddness of either side.
import Init import Mathlib import Definitions.Def_P2MAssembly_Chapter20 set_option autoImplicit true open ProofsInTheBook.Chapter20 open MonskyColor variable (D : SquareDissection)
theorem ProofsInTheBook.Chapter20.sum_triangleLocalRGCount_mod_two_eq_oddAtomic :
(∑ i : Fin D.n, triangleLocalRGCount
(realTwoAdicColor (D.coord (D.tri i).1),
realTwoAdicColor (D.coord (D.tri i).2.1),
realTwoAdicColor (D.coord (D.tri i).2.2))) % 2 =
(Finset.univ.filter fun e : Sym2 D.vtx =>
edgeRGIndicator (realTwoAdicColor ∘ D.coord) e = 1 ∧
Odd (atomicMult D e)).card % 2 := by sorry