interface_sq_le_total
plain-language theorem explainer
Discrete isoperimetric bound on the polarized diamond: for radius $t\ge 1$, the squared interface cardinality is at most eight times the total ordered adjacency count. Anyone tracking the birth-field cost ledger cites it to show forced distinctions form a codimension-1 surface, not a bulk term. Proof rewrites both sides via the closed forms $|B|=8t-4$ and $|E|=8t^2$, shifts $t=n+1$, and finishes by nonlinear arithmetic.
Claim. For every natural number $t\ge 1$, writing $B(t)$ for the bichromatic ordered edges of the polarized L1 diamond of radius $t$ and $E(t)$ for all ordered 4-neighbour adjacencies of that diamond, one has $|B(t)|^2\le 8\,|E(t)|$.
background
The module counts total ordered adjacencies of the coarsening world and splits them into monochromatic (carried) versus bichromatic (interface) edges. The L1 diamond $|x|+|y|\le t$ is the 2D ball; its 4-neighbour ordered edge set $E(t)$ is the Finset of adjacent vertex pairs, identical to the engine edge list of InterfaceComponentBound.
Upstream, total_edge_card proves $|E(t)|=8t^2$ by a bijection of ordered edges onto pairs (cell, unit direction) that stay inside the ball. Independently, PolarizedBirthInterfaceCount defines $B(t)$ as the bichromatic subset (adjacent pairs with unequal polarized charge) and proves $|B(t)|=8t-4$ for $t\ge 1$. Every adjacency is either carried or interface, so the monochromatic remainder is exactly $8t^2-(8t-4)$.
The local claim is the discrete surface law: interface squared is controlled by a constant times total adjacency, so the forced cost is sub-extensive and lives on a perimeter.
proof idea
Rewrite the left card by interface_card_eq (giving $8t-4$) and the right card by total_edge_card (giving $8t^2$), so the goal becomes $(8t-4)^2\le 8\cdot(8t^2)$. Write $t=n+1$ via omega (using $t\ge 1$). Simplify the linear factor $8(n+1)-4$ to $8n+4$ again by omega, then discharge the resulting quadratic inequality by nlinarith with the nonnegativity of $n$.
why it matters
This is the sharp discrete isoperimetric statement for the polarized birth field in 2D: interface grows only like the square root of bulk adjacency, so the engine's posted cost is localized to a codimension-1 surface. The module doc frames the north-star slogan "carry the bulk coarse, pay only for the interface"; the companion identity for carried edges is $8t^2-8t+4$, and the present inequality is the surface-law packaging of that split.
No downstream consumers are wired yet (used_by is empty), but the result sits next to carried and total_edge_card as the quantitative guarantee that the interface fraction $(8t-4)/(8t^2)\to 0$. In the broader Recognition ledger this matches the claim that distinction cost is perimeter-like rather than volumetric, consistent with the coarsening picture in which monochromatic domains are free and only bichromatic seams are posted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.