interface_increment_const
plain-language theorem explainer
Advancing the polarized 2-D diamond birth field by one cadence step increases the bichromatic ordered-edge interface by exactly eight edges, for every radius t ≥ 1. The increment is independent of world volume (which is Θ(t²)). Cosmologists and complexity auditors cite it as the Lean form of the compute-watch law: forced recognition activity per cycle is O(1). The proof is a two-line rewrite from the closed card formula 8t−4, finished by arithmetic.
Claim. For every natural number $t \ge 1$, if $B(t)$ denotes the finite set of ordered adjacent pairs of diamond vertices whose polarized charges differ, then $|B(t+1)| - |B(t)| = 8$.
background
The module counts the recognition-active interface of the forced conjugate-birth field on the 2-D diamond lattice. The polarized charge is $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$. The interface $B(t)$ is the Finset of ordered adjacent pairs whose charges differ; these are the forced distinctions the engine must post.
Phase 51 confined that interface to the codimension-1 spine and showed the spine is sub-extensive, but only bounded cells. This module upgrades the bound to an exact ordered-edge count. The key upstream identity is interface_card_eq: for $t\ge 1$, $|B(t)|=8t-4$, obtained by a bijection of bichromatic edges onto interior spine coordinates times side and orientation (each edge has one spine endpoint $(0,y)$ and one neighbour $(\pm 1,y)$ with $|y|\le t-1$).
The local setting is the 2-D diamond; the Octahedron namespace later lifts the same counting to the $D=3$ case forced by the chain, where the increment becomes linear in $t$ rather than constant.
proof idea
One-line algebraic reduction. Rewrite both cardinalities by the closed formula interface_card_eq: $|B(t+1)|=8(t+1)-4$ and $|B(t)|=8t-4$ (the hypothesis $t\ge 1$ supplies the side condition for the second application; $t+1\ge 1$ is immediate). The difference simplifies to $8$ by ordinary integer arithmetic (omega). No new bijection is built here; the work sits in the card formula.
why it matters
This is the headline corollary of the module: the literal Lean statement of the compute-watch principle. Recognition activity per cadence cycle is a pure constant, independent of world size, while volume grows as $\Theta(t^2)$. Cost therefore tracks the interface increment $O(1)$, never the bulk.
The module doc places it as the 2-D anchor before the $D=3$ lift. In three dimensions (the spatial dimension forced by the chain, T8/T9) the same construction yields a per-cycle increment $16t=\Theta(t)$, still sub-extensive against $\Theta(t^3)$ volume but no longer constant, because the active interface is a growing codimension-1 disk. Downstream, the total-growth identity over a run from radius $1$ to $T$ is the telescoping sum of these increments: $8(T-1)$ in 2-D, giving the closed-form compute-watch run total $\Theta(T^{D-1})$ forced distinctions rather than brute-force $\Theta(T^{D+1})$ spacetime cost.
No external used-by edges are recorded yet; the immediate consumer is the total-growth corollary in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.