IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount
Exact Finset count of bichromatic ordered edges for the polarized birth field on the growing L1 ball. Those forced-distinction edges number $8t-4$ in 2D and $8t^2-8t+4$ in 3D: the recognition cost the coarsening engine posts. Cosmology proofs that split carried versus interface cost cite this module. The argument indexes spine-neighbor adjacencies and reduces cardinality by explicit Finset bijections.
claimOn the L1 ball of radius $t$, the polarized birth field ($+1$ on $x>0$, $-1$ on $x<0$, $0$ on the spine $x=0$) has bichromatic ordered-edge set of cardinality $8t-4$ in two dimensions and $8t^{2}-8t+4$ in three dimensions.
background
The scale-adaptive coarsening engine accumulates its world on an L1 ball that grows one rung per recognition cycle: the 2D diamond $|x|+|y|\le t$ and the 3D octahedron $|x|+|y|+|z|\le t$. LatticeBallVolume supplies the closed cell counts ($2t^2+2t+1$ in 2D; centered octahedral numbers in 3D).
The polarized birth field is the forced conjugate configuration used as the model charge: $+1$ on the positive half-space, $-1$ on the negative half-space, and $0$ on the coordinate spine $x=0$. PolarizedBirthDomains already showed the carried side is $O(1)$: exactly three locked domains at every radius, while the world is $\Theta(t^d)$.
PolarizedBirthInterface proved the complementary geometric fact that recognition activity (bichromatic edges) lives on the spine. This module turns that geometry into an exact Finset and a closed cardinality: the interface is the set of ordered edges whose endpoints carry opposite nonzero signs, i.e. the forced distinctions the engine must post.
proof idea
The module builds an explicit Finset model of the bichromatic ordered-edge set of the polarized field on the L1 ball. Spine and neighbor membership predicates carve the active locus; an edge-index map (and its inverse) gives a bijection between that Finset and a concrete index set whose cardinality is elementary in $t$.
Cardinalities are then read off by counting the index set, yielding the closed forms $8t-4$ (2D) and $8t^2-8t+4$ (3D). Companion lemmas equate interface length to that cardinality and record the constant per-rung increment, so later modules can differentiate the cost without re-enumerating edges.
why it matters in Recognition Science
LatticeBallEdges imports this module to finish the adjacency ledger: total ordered edges of the L1 ball minus the interface count equals the monochromatic (carried-internal) edges the engine keeps for free. Downstream doc states the split explicitly: interface cost is exactly the formulas proved here; the remainder is free carriage.
Together with PolarizedBirthDomains (carried state $O(1)$) and InterfaceComponentBound (locked domains $\le$ interface $+1$), the module closes the cost side of the polarized-birth story on the diamond and octahedron. It is the quantitative interface half of the Phase-50/51 coarsening chain that turns the numeric domain-coarsening scripts into sorry-free Lean theorems over $\mathbb{N}$.
scope and limits
- Does not count monochromatic (same-sign) adjacencies; that is LatticeBallEdges.
- Does not treat non-polarized or arbitrary charge fields, only the forced birth polarization.
- Does not re-prove locked-domain bounds; those live in InterfaceComponentBound.
- Restricted to L1 balls (2D diamond, 3D octahedron), not Euclidean or other norms.
- Gives ordered-edge cardinalities, not undirected geometric edge lengths.
used by (1)
depends on (4)
declarations in this module (14)
-
def
B -
theorem
interface_length_eq_card -
theorem
edge_structure -
def
idx -
theorem
idx_card -
theorem
memSpine -
theorem
memNbr -
def
edgeIndex -
def
edgeFromIndex -
theorem
interface_card_eq -
theorem
interface_length_eq -
theorem
interface_increment_const -
theorem
interface_total_growth -
theorem
interface_increment_linear