Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Triangle corner parity equals odd-multiplicity red–green edge parity

Proved
ProofsInTheBook.Chapter20.sum_triangleLocalRGCount_mod_two_eq_oddAtomic

by xiangyazi24 · Sep 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

auxiliary-lemmageometrylean4monsky-theoremproofs-from-the-book

Let 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 Q=[0,1]2Q=[0,1]^2Q=[0,1]2, have pairwise disjoint topological interiors, and each have area 1/n1/n1/n (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

∑iri≡#{e: e has one red and one green endpoint and m(e) is odd}(mod2).\sum_i r_i\equiv\#\{e:\ e\text{ has one red and one green endpoint and }m(e)\text{ is odd}\}\pmod2.i∑​ri​≡#{e: e has one red and one green endpoint and m(e) is odd}(mod2).

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.

Preamble
import Init
import Mathlib
import Definitions.Def_P2MAssembly_Chapter20
set_option autoImplicit true
open ProofsInTheBook.Chapter20
open MonskyColor
variable (D : SquareDissection)
Formal statement
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
Source
Original declaration: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter20DissectionFinal.lean#L85. Repository topic: Monsky’s theorem, “One square and an odd number of triangles.” SquareDissection and atomic-edge definitions: https://github.com/xiangyazi24/proof_in_the_book/blob/88d88d141768cded75e782c525ef1bf04b8fe220/ProofsInTheBook/Chapter20DissectionEngine.lean#L23.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me