interface_total_growth
plain-language theorem explainer
Over a full forward run of the polarized birth field from radius 1 to radius T, the net growth in ordered interface edges is exactly 8(T-1). Anyone citing the compute-watch run-total in 2-D cosmology would use this closed form. The proof rewrites both endpoint cardinalities by the exact interface count and finishes by integer arithmetic.
Claim. For every natural number $T \ge 1$, if $B(t)$ is the Finset of ordered bichromatic (interface) edges of the polarized diamond field at radius $t$, then $|B(T)| - |B(1)| = 8T - 8$.
background
On the 2-D diamond lattice the polarized birth field assigns a forced conjugate-birth charge: $+1$ on the fine half $x>0$, $-1$ on the coarse half $x<0$, and $0$ on the spine $x=0$. The interface is the Finset of ordered adjacent pairs whose charges differ; those pairs are the forced distinctions the recognition engine posts each cycle.
This module finishes the Phase-51 program by counting those ordered bichromatic edges exactly. The key upstream fact is the exact cardinality at fixed radius: $|B(t)|=8t-4$ for $t\ge 1$, obtained by a bijection with interior spine cells times side and orientation. The module setting is the compute-watch principle: cost should track recognition activity (interface growth), not bulk volume.
proof idea
Two-line tactic proof. Rewrite $(B,T).\mathrm{card}$ and $(B,1).\mathrm{card}$ by the exact interface count $|B(t)|=8t-4$ (applied at $T$ with the given hypothesis, and at $1$ via reflexivity of $\le$). The goal collapses to the integer identity $(8T-4)-(8-4)=8T-8$, discharged by omega.
why it matters
This is the closed-form 2-D compute-watch run-total: a full forward run from radius 1 to $T$ posts exactly $8(T-1)=\Theta(T)$ net forced distinctions, strictly sub-extensive against brute-force spacetime cost $\Theta(T^3)$ (volume $\Theta(T^2)$ times $T$ cycles). The module pairs it with the 3-D octahedron analogue $8T(T-1)$, which is $\Theta(T^{D-1})$ against $\Theta(T^{D+1})$, matching the forcing-chain selection $D=3$. Together with the constant per-cycle increment of 8 ordered edges, it makes precise that recognition activity stays sub-extensive in 2-D. No downstream dependents are recorded yet; it stands as a headline corollary of the exact edge count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.