center
plain-language theorem explainer
The origin (0,0) is a lattice vertex of every 2D L1 diamond of radius t. Cosmology and connectivity proofs cite it as the unique height-zero point that seeds the descent argument for diamond connectivity. The definition packages the membership proof via the ball characterization and omega arithmetic.
Claim. For every natural number $t$, the lattice point $(0,0)$ lies in the L1 ball of radius $t$, and is therefore a vertex of the diamond graph of that radius.
background
This module proves a dimension-free bound on locked domains: the number of monochromatic components is at most the number of bichromatic (interface) edges plus one, on any finite connected world. For the 2D engine lattice the ambient world is the diamond: integer points with $|x|+|y|\le t$, with 4-neighbour adjacency.
Vertices are the subtype Vtx t of lattice points in that ball. Membership is characterized by mem_ball_iff: $(x,y)$ is in the ball iff the sum of absolute values is at most $t$. The L1 norm doubles as a height function toward the origin, which later discharges connectivity via a unique zero and descent edges.
The origin is the natural basepoint of that height. Declaring it as a vertex is the first concrete inhabitant of Vtx t and underwrites the Nonempty instance used throughout the component-counting development.
proof idea
Definitional construction: pair the point $(0,0)$ with a membership proof. Rewrite membership by mem_ball_iff, then close $0+0\le t$ by omega. No further lemmas.
why it matters
Feeds the diamond connectivity path that closes the open component-count fact from the cosmogenesis domain-coarsening scripts. Immediately used by hzero (every height-zero vertex equals the centre) and by mono_le_interface_succ, which instantiates the headline bound mono_components_le_bichromatic_succ on the 2D diamond.
That bound is the 2D/3D weakening of the exact 1D identity runs = boundaries + 1: multiply-connected interfaces force an inequality. Connectivity of the ambient diamond is discharged by connected_of_descent with L1 height and this unique zero, matching the recognition law's pull toward the coarsest description read as graph connectivity.
Downstream cosmology and constants modules also touch the centre as a geometric basepoint (galaxy core profiles; solid-angle and passive-edge counts at D=3), so the definition is shared scaffolding rather than a one-off inhabitant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.