boundary_ypos
plain-language theorem explainer
On the 2D L1 diamond of radius t, the cells whose upward neighbour exits the ball number exactly 2t+1: one per vertical column. Cosmology edge-count arguments cite this as the +y face size in the volume-minus-boundary ledger. The proof is an explicit Finset bijection onto the integer interval Icc(-t,t), sending each boundary cell to its x-coordinate and recovering the unique top lattice point (x, t-|x|).
Claim. For every natural number $t$, the number of lattice points $p=(x,y)$ in the 2D $\ell_1$ ball of radius $t$ such that $(x,y+1)$ lies outside that ball equals $2t+1$.
background
The ambient set is the 2D diamond ball t: lattice points $(x,y)\in\mathbb{Z}^2$ with $|x|+|y|\le t$, realized as a Finset by filtering the axis-aligned box. Membership is characterized by mem_ball_iff: $(x,y)$ is in the ball iff the sum of absolute values is at most $t$.
This module sits in the cosmology ledger that splits every adjacency of the coarsening world into monochromatic (carried-for-free) edges versus bichromatic interface edges. The module doc states the strategy: ordered edges biject to pairs (cell, unit direction) with both endpoints in the ball; for fixed direction $d$, the cells whose $d$-neighbour leaves form a codimension-1 silhouette of size $2t+1$ in 2D (one cell per transverse coordinate in Icc(-t,t)).
The four cardinal boundary lemmas (including this top face) feed the per-direction bulk count, which then sums to the closed form for total ordered adjacencies of the diamond.
proof idea
Rewrite the target cardinality $2t+1$ as card(Icc(-(t:ℤ), t)) via Int.card_Icc and omega. Build a Finset bijection card_bij' between the filtered top-boundary set and that interval: forward map sends $(x,y)$ to its first coordinate $x$; reverse map sends $x$ to the unique top point $(x, t-|x|)$.
The four obligations are pure arithmetic under mem_ball_iff: (i) a filtered point has $x\in[-t,t]$; (ii) every such $x$ produces a point still in the ball whose $+y$ neighbour exits; (iii) the forward-then-reverse round-trip recovers $y$ because the top condition forces $y=t-|x|$; (iv) reverse-then-forward is the identity on $x$. All inequalities discharge by omega.
why it matters
Parent theorems step_card and (in the 3D analogue path) the direction cases feeding total edge counts use this face size directly: for each unit direction the in-ball steps equal bulk volume minus boundary, and step_card quotes the four boundary lemmas to obtain $2t^2$ survivors per direction. Summing over the four directions yields Diamond.total_edge_card t = 8t^2.
That closed form is the "total" side of the carried-versus-interface split. Subtracting the polarized interface count $8t-4$ gives the monochromatic carried edges $8t^2-8t+4$, so the carried fraction tends to 1. The module frames this as the exact statement of "carry the bulk coarse, pay only for the interface" in the coarsening north star. The argument is pure discrete geometry over $\mathbb{N}$; it does not invoke the forcing chain T0–T8, but it supplies the combinatorial substrate those cosmology claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.