Monsky’s theorem for finite equal-area dissections of the unit square

There is no dissection of the unit square $[0,1]^2$ into an odd finite number n of equal-area nondegenerate triangles. Precisely, let V be a finite vertex type with decidable equality and an injective coordinate map $v:V\to\mathbb R^2$, and let $(a_i,b_i,c_i)\in V^3$ be specified for each $i\in\{0,\ldots,n-1\}$. Put $T_i=\operatorname{conv}\{v(a_i),v(b_i),v(c_i)\}$. Assume each oriented double area is nonzero, $\bigcup_iT_i=[0,1]^2$, the ordinary topological interiors of distinct $T_i$ are disjoint, and

for every i, where the right-hand side is formally the rational quotient $1/n$ embedded into the reals. If n is odd, these data yield a contradiction.

The model permits a triangle corner to lie in the relative interior of another triangle's side. It assumes neither a face-to-face triangulation nor a supplied incidence or coloring certificate. The finite vertex type may also contain unused vertices; the structure does not require every vertex to occur as a triangle corner.