eulerChar2D_filledBox
plain-language theorem explainer
A filled lattice rectangle with (a+1)×(b+1) vertices has cubical Euler characteristic exactly 1 for every integer side lengths a, b. Foam-topology and cosmogenesis readers cite it as the 2-D contractible normalization: size cannot fake topology. The proof is pure ring cancellation on the cell counts N0, N1, N2.
Claim. For all integers $a,b$, $$(a+1)(b+1) - \bigl(a(b+1)+(a+1)b\bigr) + ab = 1.$$ Interpreting $(a+1)(b+1)$ as vertices, $a(b+1)+(a+1)b$ as unit edges, and $ab$ as unit squares, the 2-D Euler characteristic of a filled axis-aligned lattice rectangle is identically one, independent of $a$ and $b$.
background
In the Recognition foam module (Phase 18), the cubical Euler characteristic of a digital region is the alternating cell count $\chi = N_0 - N_1 + N_2 - N_3$ (occupied vertices, unit edges, unit squares, unit cubes). The module supplies the parameter-free topological readout of the many-domain foam assembled in Phase 15 and frozen in Phase 17: the recognition analogue of the cosmic-web genus statistic.
The first structural fact is contractible normalization. A filled $d$-box must read $\chi = 1$ independent of side lengths. That size-independence is the signature of a topological invariant: a solid region, however large, has the Euler characteristic of a point. Any later deviation of $\chi$ from 1 therefore measures genuine topology (extra components, tunnels $b_1$, enclosed voids $b_2$), never mere volume. The 2-D identity proved here is $N_0 - N_1 + N_2 = 1$ with the cell counts above; 1-D and 3-D siblings expand the same idea.
A second fact, proved alongside, is the inclusion-exclusion valuation $\chi(A\cup B)+\chi(A\cap B)=\chi(A)+\chi(B)$, so $\chi$ is additive over disjoint locked domains and $k$ solid components read $\chi = k$.
proof idea
One-line ring proof. Expand $(a+1)(b+1) - [a(b+1)+(a+1)b] + ab$ in the commutative ring $\mathbb{Z}$. All quadratic and linear terms cancel, leaving the constant $1$. No external lemmas are invoked beyond the ring structure; the tactic ring discharges the identity.
why it matters
This is the 2-D half of the module's §1 contractible-normalization block. Together with the 1-D and 3-D filled-box identities and the inclusion-exclusion valuation, it underwrites the claim that numeric foam readouts never confuse size with topology. Classically, the polar birth law assembles a single contractible domain ($\chi = 1$), while the Thue-Morse foam fragments into simply-connected dust whose $\chi$ equals its component count $b_0$ (so $b_1 = b_2 = 0$). The Euler curve $\chi(R)$ as the world grows is then a topological signature separating the laws, and Phase-17 freeze-out lowers the curve in a controlled way.
In the broader RS chain the ambient spatial setting is $D = 3$ (T8), but this 2-D identity is the planar calibration step for the cubical complex before the full 3-D foam statistic. No Lean used_by edges are wired yet; the declaration is infrastructure for that classical comparison and for any later Lean consumer that needs $\chi(\text{filled box}) = 1$ as a base case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.