interface_cube_le_total_sq
plain-language theorem explainer
Discrete 3-D isoperimetric bound on the polarized birth octahedron: the cube of the forced-interface edge count is at most eight times the square of the total ordered-adjacency count, for every world radius t ≥ 1. Anyone arguing that the engine pays only a surface cost cites this. The proof substitutes the closed forms for interface and total adjacency, shifts t = n+1, and finishes by elementary polynomial comparison.
Claim. For every natural number $t \ge 1$, let $B(t)$ be the Finset of forced bichromatic (interface) edges of the polarized birth field on the 3-D $\ell_1$ ball of radius $t$, and let $E(t)$ be the Finset of all ordered 6-neighbour adjacencies of that ball. Then $|B(t)|^3 \le 8\,|E(t)|^2$.
background
The module counts total ordered adjacencies of the coarsening world and splits them into carried (monochromatic) versus forced interface (bichromatic) edges. In 3-D the world is the $\ell_1$ octahedron of radius $t$ with 6-neighbour adjacency. The total ordered edge set $E(t)$ has closed cardinality $8t^3 + 4t$ (volume-minus-boundary over the six unit directions). The interface set $B(t)$ is counted exactly in PolarizedBirthInterfaceCount as $8t^2 - 8t + 4$.
Module doc: the engine "pays only the vanishing interface fraction" while carrying the monochromatic bulk free. Upstream, total_edge_card bijects ordered edges onto admissible (cell, direction) pairs; the interface identity Octahedron.interface_card_eq supplies the $\Theta(t^2)$ surface count. Spatial dimension $D = 3$ is the forced value from the Recognition chain (T8/T9).
proof idea
Rewrite the goal by the two closed forms: PolarizedBirthInterface.Octahedron.interface_card_eq (interface $= 8t^2-8t+4$) and the local total_edge_card (total $= 8t^3+4t$). Shift variables via $t = n+1$ (valid by $t \ge 1$). Expand the interface polynomial to $8n^2+8n+4$. Bound that by $8(n+1)^2$ (nlinarith), and bound the bulk factor $8(n+1)^3$ by $8(n+1)^3+4(n+1)$ (Nat.le_add_right). A three-line calc then raises the interface bound to the third power, rewrites the cube as $8\cdot(8(n+1)^3)^2$ by ring, and multiplies the bulk inequality through on the square.
why it matters
This is the discrete surface law that certifies the interface is codimension-1 in three dimensions: interface $\Theta(t^2)$ versus total adjacency $\Theta(t^3)$, so interface scales as the $2/3$ power of bulk. It is the exact $\mathbb{N}$-level statement that the forced distinction set is a surface, not a volume, which the coarsening north star needs when it claims "carry the bulk coarse, pay only for the interface."
It sits next to carried_ge_interface (carried bulk overtakes interface for every $t \ge 1$) in the same octahedron section. Framework landmark: $D = 3$ from the forcing chain makes the $2/3$ exponent the physical one. No downstream users are wired yet (used_by empty); the natural parents are any global cost or carried-fraction theorems that need a uniform surface-to-volume comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.