interface_increment_linear
plain-language theorem explainer
Advancing the 3-D polarized octahedron birth field by one cadence cycle adds exactly 16t ordered interface edges. Anyone citing the D=3 compute-watch law (cost tracks recognition activity, not volume) needs this increment. The proof rewrites both cardinalities by the closed-form interface count and finishes by elementary algebra on the quadratic.
Claim. For every natural number $t \ge 1$, if $B(t)$ denotes the finite set of ordered bichromatic adjacency edges of the polarized octahedron birth field at radius $t$, then $|B(t+1)| - |B(t)| = 16t$.
background
The module closes the exact interface-edge count for the forced conjugate-birth field. Phase 51 confined recognition activity to a codimension-1 spine and proved sub-extensivity of spine cells; this file counts ordered bichromatic edges exactly.
In the Octahedron namespace (the D=3 lift selected by the forcing chain), the polarized charge is $+1$ on the fine half, $-1$ on the coarse half, and $0$ on the spine disk $x=0$. The interface $B(t)$ is the Finset of ordered adjacent pairs whose polarized charges differ. Upstream, the exact count is $|B(t)| = 8t^2 - 8t + 4$ for $t \ge 1$: a bijection with interior spine points times side and orientation, four times the Phase-49 diamond area law.
The 2-D sibling has constant per-cycle growth of 8 ordered edges. In three dimensions the active interface is a growing 2-D disk, so the increment must be linear in the radius.
proof idea
One short tactic proof. Rewrite both $|B(t+1)|$ and $|B(t)|$ by the closed-form interface_card_eq (the 3-D quadratic $8r^2-8r+4$). Expand $(t+1)^2 = t^2+2t+1$ by ring, record the elementary inequality $t \le t^2$ (from $t \ge 1$) via nlinarith, substitute, and discharge the resulting integer identity with omega. No bijection work is redone here; all combinatorial content sits in the cardinality formula.
why it matters
This is the honest 3-D form of the compute-watch principle: cost per cadence cycle still tracks recognition activity, but in $D=3$ that activity is $\Theta(t)$, not $O(1)$, because the recognition-active interface is a growing codim-1 disk. The module doc states the contrast with the 2-D constant increment of 8 and ties the setting to the forcing-chain dimension $D=3$ (T8).
The sibling total-growth theorem records the net over a full run $1\to T$ as $8T(T-1)=\Theta(T^2)$, strictly sub-extensive against brute-force spacetime cost $\Theta(T^4)$ (volume times ticks). No downstream Lean dependents are wired yet; the declaration stands as the per-cycle primitive those run-totals and any engine cost bounds would cite. It does not touch mass ladders, $\alpha$, or J-uniqueness directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.