mem_ball_iff
plain-language theorem explainer
Membership of a lattice point (x,y) in the 2D diamond of radius t is exactly the L1 condition |x|+|y|≤t. Anyone building Diamond vertices, descent edges, or boundary counts cites this to drop the Finset filter packaging. The proof unfolds the bounding-box-plus-filter definition and recovers the box bounds by omega.
Claim. For every natural number $t$ and integers $x,y$, the point $(x,y)$ belongs to the finite 2D diamond of radius $t$ if and only if $|x|+|y|\le t$.
background
The ambient object is the 2D diamond of radius $t$: the integer L1 ball $|x|+|y|\le t$, packaged as a Finset by first taking the axis-aligned box $[-t,t]^2$ and then filtering by the L1 inequality. That packaging is what ball t is; the present lemma peels it back to the pure metric condition.
The module proves a dimension-free bound on locked domains: monochromatic components of a charge field are at most one more than the number of bichromatic (interface) edges, once the ambient world is connected. Connectivity of the concrete lattices the engine runs is discharged by a height-descent criterion: a unique zero plus a strict descent edge from every other cell implies one component. The 2D diamond instantiates that criterion with L1 height and the origin as zero, so a clean membership test for the diamond is infrastructure for the whole chain.
proof idea
Term/tactic hybrid. Unfold the diamond definition, then simplify membership through Finset.mem_filter, Finset.mem_Icc, and product order. The forward direction projects out the filter predicate. The reverse rebuilds box membership: four omega goals show $-t\le x,y\le t$ from $|x|+|y|\le t$, then reattach the L1 witness. No external lemmas beyond Mathlib Finset and omega.
why it matters
This is the membership API for every Diamond construction downstream. center uses it to place the origin in every ball (and thus obtain Nonempty vertices). descent rewrites membership to build the strict L1-lowering 4-neighbour step that feeds connected_of_descent. Lattice boundary counts (boundary_xneg, boundary_xpos, and siblings) rewrite through it when counting cells with an exterior neighbour.
Those pieces close the 2D half of the module headline: locked-domain count ≤ interface size + 1 on the diamond, discharging the connected-graph fact previously only numeric-checked in the cosmogenesis coarsening scripts. In the Recognition framework this is lattice infrastructure for domain coarsening, not a forcing-chain (T0–T8) step, but it makes the interface-plus-one bound a theorem rather than a runtime check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.