ball
plain-language theorem explainer
The closed L1 ball of radius t on the integer lattice Z², realized as a Finset: all lattice points with |x|+|y|≤t. Cosmology and foam-topology arguments cite it as the exact 2D world the domain-coarsening engine runs on. Construction is the axis-aligned box Icc filtered by the L1 inequality.
Claim. For each natural number $t$, $\mathrm{ball}(t)$ is the finite set of lattice points $(x,y)\in\mathbb{Z}^2$ lying in the closed diamond $|x|+|y|\le t$ (equivalently, the $L^1$ ball of radius $t$ about the origin).
background
The module proves a dimension-free interface bound: on any finite connected world, the number of monochromatic (locked) domains is at most the number of bichromatic interface edges plus one. That closes an open connected-graph fact from the 2D/3D domain-coarsening engines.
In 2D the engine's world is the diamond lattice: 4-neighbour adjacency on the L1 ball. The ambient vertex set must be a Finset so that component counts via Nat.card of the monochromatic quotient are well-defined. The diamond is carved by taking the integer box $[-t,t]^2$ and retaining only points with taxicab norm at most $t$.
Downstream, height on this set is the L1 norm itself (graph distance to the origin), which supplies the descent potential used to prove the diamond is connected and therefore satisfies the interface bound for every radius and every charge field.
proof idea
Pure definition, no proof obligations. Form the closed integer square via Finset.Icc from $(-t,-t)$ to $(t,t)$, then filter by the predicate $p_1.\mathrm{natAbs}+p_2.\mathrm{natAbs}\le t$. The box guarantees finiteness; the filter enforces the diamond geometry.
why it matters
This is the concrete 2D lattice underlying Diamond.mono_le_interface_succ: for any charge colouring of the diamond, locked 4-connected domains are at most interface edges plus one. That is the engine-facing instance of the module headline mono_components_le_bichromatic_succ.
It feeds height (L1 potential), mem_ball_iff (membership characterization), Vtx (subtype of ball points), and the descent/connectivity package that discharges the connectedness hypothesis on the live 2D world. FoamTopology.eulerChar3D_oneVoid sits in the same cosmology stack (void/interface counting), though on the 3D side.
In Recognition terms this is the finite 2D stage on which locked domains versus recognition-active interface edges are counted; the bound is the discrete precursor to domain coarsening used in cosmogenesis scripts. No open sorry remains on this object: it is closed scaffolding for the proved interface inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.