boundary_yneg
plain-language theorem explainer
On the 2D L1 diamond of radius t, exactly 2t+1 lattice cells have their downward neighbour outside the ball: one per vertical column. Cosmology edge-counting cites this as the −y face size in the volume-minus-boundary ledger. The proof is a Finset bijection from that filtered set onto the integer interval [−t,t].
Claim. Let $B_t=\{(x,y)\in\mathbb{Z}^2:\lvert x\rvert+\lvert y\rvert\le t\}$. Then $\bigl\lvert\{(x,y)\in B_t:(x,y-1)\notin B_t\}\bigr\rvert=2t+1$.
background
The module counts total ordered adjacencies of the coarsening world so that monochromatic (carried) edges can be split from bichromatic interface edges. In 2D the ambient set is the L1 diamond ball t: lattice points with $\lvert x\rvert+\lvert y\rvert\le t$, realized as a filtered bounding box. Membership is characterized by mem_ball_iff.
Ordered edges are pairs (cell, unit direction) with both endpoints in the ball. For fixed direction $d$, the cells whose $d$-step leaves the ball form a codimension-1 silhouette. The module doc states that in 2D this silhouette is one cell per transverse coordinate, hence size $2t+1$, matching $\mathrm{card}(\mathrm{Icc}(-t,t))$.
This declaration treats the downward direction $(0,-1)$. Sibling lemmas handle $+x$, $-x$, and $+y$; together they feed the per-direction interior-step count.
proof idea
Rewrite the target cardinality as $\mathrm{card}(\mathrm{Icc}(-t,t))$ via Int.card_Icc and omega. Build an explicit Finset.card_bij':
- forward map sends a filtered point $(x,y)$ to its first coordinate $x$;
- reverse map sends $x\in[-t,t]$ to the bottom-of-column point $(x,-(t-\lvert x\rvert))$.
Four obligations: forward lands in the interval (from mem_ball_iff plus the outside-neighbour filter, discharged by omega); reverse lands in the filtered set (same); left inverse recovers $y$ as the unique bottom height; right inverse is definitional rfl.
why it matters
Parent theorem step_card subtracts this $2t+1$ (and the three sibling face counts) from the diamond volume $2t^2+2t+1$ to get $2t^2$ interior steps per unit direction. Summing over the four directions yields Diamond.total_edge_card t = 8t^2, the closed total-adjacency law of the module.
That total minus the polarized interface count $8t-4$ is the monochromatic carried ledger $8t^2-8t+4$, the exact 2D form of "carry the bulk coarse, pay only for the interface." The same boundary size appears (scaled) in the 3D companion three_mul_step_card. No new axioms: pure finite-set combinatorics over the Phase-49 volume laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.