Pith. sign in
module module high

IndisputableMonolith.Cosmology.PolarizedBirthInterface

show as:
view Lean formalization →

On the polarized diamond birth field, every charge-flipping adjacency has an endpoint on the spine x=0. The module identifies that spine, proves the active interface lives only there, and shows both spine and interface are sub-extensive in the ball radius. Cosmology proofs that bound recognition cost of conjugate birth cite it. The core step is pure sign case analysis plus a 1D image cardinality.

claimFor the polarized charge field $\mathrm{sign}(x)$ on the 2D L1 ball $|x|+|y|\le t$, every unit-distance edge joining opposite charges has at least one endpoint on the spine $\{x=0\}$. That spine equals the image of a 1D lattice segment; its cell count and the bichromatic interface it supports are both $O(t)$ (sub-extensive) in the radius $t$.

background

The scale-adaptive coarsening engine grows its world as an L1 ball: the diamond $|x|+|y|\le t$ in 2D (and the octahedron in 3D). Upstream, LatticeBallVolume supplies closed-form cell counts ($2t^2+2t+1$ in 2D). InterfaceComponentBound proved that locked-domain count is at most the interface size plus one for any charge field. PolarizedBirthDomains specialized to the forced conjugate-birth (polarized) field and showed its carried state is already sub-extensive.

This module isolates where recognition is actually active for that polarized field. Charge is $\mathrm{sign}(x)$, so flips occur only between columns $x\in{-1,0,1}$. The spine is the codimension-1 slice $x=0$ inside the diamond; bichromatic (opposite-charge) adjacencies are the interface the engine must pay for.

proof idea

The lead lemma is pure case analysis: split on $\mathrm{sign}$ at each endpoint of a unit-distance edge; opposite signs force the step in $x$ to cross $0$, so one endpoint lies on the spine. From that, the interface is contained in the spine neighborhood. The spine is identified with the image of a 1D lattice segment, giving an exact cardinality linear in $t$. Sub-extensivity of the interface and of the birth-field carried state then follow by comparing that $O(t)$ spine size to the quadratic ball volume.

why it matters in Recognition Science

Downstream, PolarizedBirthInterfaceCount upgrades the spine-cell bound to an exact bichromatic edge count ($8t-4$ ordered edges in 2D, $8t^2-8t+4$ in 3D) and constant recognition activity per cycle; its doc-comment states that this module "proved the recognition-active interface ... is confined to the codimension-1 spine and that the spine is sub-extensive, but it bounded only the spine cells." LatticeBallEdges then splits total adjacencies into that paid interface versus monochromatic edges carried for free. In the phase sequence this is the bridge from domain-count and volume laws to the exact cost ledger of polarized birth.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (7)