descent
plain-language theorem explainer
On the 2D L1 diamond of any radius, every non-origin lattice vertex has a 4-neighbour strictly closer to the centre in L1 height. Cosmology and domain-coarsening proofs cite it to discharge the descent hypothesis of connectivity. The argument is finite case analysis on the signs of the coordinates, each step proved by omega.
Claim. Fix radius $t \in \mathbb{N}$. Let $V_t$ be the integer lattice points in the L1 ball $|x|+|y| \le t$, with 4-neighbour edges and height $h(x,y)=|x|+|y|$. For every $v \in V_t$ with $h(v) \ne 0$ there exists a neighbour $u$ (edge in either orientation) such that $h(u) < h(v)$.
background
The module proves the locked-domain bound: monochromatic components on a finite world are at most the number of bichromatic interface edges plus one. Connectivity of the ambient lattice is an input to that bound; it is discharged by a reusable descent criterion rather than by ad-hoc path constructions.
Vertices of the diamond are subtype points of the L1 ball of radius $t$. Adjacency is L1 distance exactly one (the 4-neighbour graph). Height is the L1 norm, the graph-distance potential to the origin. The edge list is every ordered adjacent pair inside the ball.
Upstream, connected_of_descent states that a finite world with a unique height-zero root and a strict descent edge from every other cell is path-connected through the root. The present lemma is the diamond instance of that descent hypothesis.
proof idea
Unpack the vertex as a pair $(x,y)$ in the ball and the nonzero-height hypothesis. Trichotomy on $x$:
- If $x < 0$, step to $(x+1,y)$: still in the ball, adjacent, height drops by 1.
- If $x > 0$, step to $(x-1,y)$ symmetrically.
- If $x = 0$, trichotomy on $y$: $y < 0$ steps to $(0,y+1)$; $y > 0$ steps to $(0,y-1)$; $y = 0$ contradicts height nonzero.
Each branch is discharged by rewriting membership and adjacency, then omega on the integer inequalities. No external lemmas beyond local mem_ball_iff, mem_edges, and adj.
why it matters
This is the lattice-specific half of descent connectivity on the exact 2D world the cosmogenesis engine runs on. It is fed directly into connected_of_descent (unique zero at the origin plus this descent implies the diamond is one component) and into mono_le_interface_succ, which specialises the dimension-free bound mono_components_le_bichromatic_succ to every radius.
Downstream, polarized birth-domain work (Fmono, polarized_components_le_three) reuses the same diamond edges and monochromatic filtering; the interface-plus-one ceiling is what turns numeric engine checks into a theorem. The module closes the open connected-graph fact left in the 2D/3D domain-coarsening scripts: locked domains $\le$ interface $+1$ on the live lattice, not merely on sampled fields.
Framework-wise this is graph connectivity read as the recognition pull toward the coarsest description (height descent to a unique root), supporting the cosmology side of the forcing chain rather than T5–T8 constants directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.