interface_subextensive
plain-language theorem explainer
For every radius t ≥ 1, the 2-D birth-field spine has exactly 2t+1 cells, and that cardinality times t is at most the diamond area 2t²+2t+1. Cosmologists citing sub-extensivity of the recognition-active interface use this bound: the interface support is O(t) inside a Θ(t²) world. The proof is a short term proof: spine cardinality plus the closed diamond volume formula, finished by linear arithmetic.
Claim. For every natural number $t \ge 1$, the spine (the vertical segment $x=0$, $|y|\le t$) has cardinality $2t+1$, and $(2t+1)\,t \le |\{|x|+|y|\le t\}|$. Equivalently, spine size times radius is at most the area of the 2-D $\ell^1$ diamond of radius $t$.
background
This module treats the recognition-active interface of the forced conjugate-birth field on the 2-D lattice diamond. Phase 50 already showed the carried side: the polarized field ($+1$ for $x>0$, $-1$ for $x<0$, $0$ on $x=0$) is held as exactly three locked domains at every radius, so carried state is $O(1)$ while the world is $\Theta(t^2)$. Here the complementary interface side is made exact.
The spine is the codimension-1 set $x=0$ inside the diamond; in 2-D it is the segment $|y|\le t$. The ambient world is the $\ell^1$ ball ${(x,y):|x|+|y|\le t}$, realized as a finite set by filtering the bounding box. Upstream, every bichromatic edge of the polarized field has an endpoint on the spine, so the entire recognition-active interface is spine-incident. Sub-extensivity then reduces to a pure cardinality comparison: spine size times radius versus diamond area.
The diamond volume is the closed formula $|B_t|=2t^2+2t+1$ from the lattice-ball volume development. The spine cardinality $2t+1$ is the 1-D ball of the same radius.
proof idea
Term-mode proof in two conjuncts. The first is exactly the already-proved spine cardinality lemma: $|\mathrm{spine}(t)|=2t+1$. For the inequality, rewrite both sides by that lemma and by the diamond ball-volume formula $|B_t|=2t^2+2t+1$, then discharge $(2t+1)t \le 2t^2+2t+1$ for $t\ge 1$ by nlinarith. No geometric enumeration of edges is required; only the two closed counts and arithmetic.
why it matters
This is the quantitative half of interface sub-extensivity for the birth field in 2-D. It feeds directly into the module capstone birth_field_subextensive, which packages three facts: (1) exactly three carried locked domains (Phase 50), (2) every bichromatic edge is spine-incident, and (3) spine times radius fits in the diamond area. Together those make both the carried-domain fraction and the interface support vanish inside the $\Theta(t^2)$ world, as a theorem rather than a numeric check.
In Recognition Science terms this is the North-Star rule made exact for the birth field: carry each region at the coarsest $\varphi$-rung its recognition allows. Cost localizes to a codimension-1 surface while volume grows one dimension higher. The module status is fully proved (zero sorry). It does not yet lift the same arithmetic to the 3-D spine (the 2-D diamond of card $2t^2+2t+1$), but the 2-D case already closes the Phase 50–51 interface picture on the plane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.