IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount
Exact count of bichromatic ordered edges of the polarized birth field on the L1 ball: the recognition interface the coarsening engine must post. In 2D the count is $8t-4$; in 3D it is $8t^2-8t+4$. Cosmologists tracking carried-versus-interface cost cite this. The argument indexes spine-crossing adjacencies and equates Finset cardinality to a closed form.
claimOn the L1 ball of radius $t$, for the polarized birth field ($+1$ on $x>0$, $-1$ on $x<0$, $0$ on the spine $x=0$), the Finset of ordered bichromatic edges (the recognition interface) has cardinality $8t-4$ in 2D and $8t^2-8t+4$ in 3D. Interface length equals that cardinality, and the per-rung increment is constant.
background
The scale-adaptive coarsening engine grows an L1 world: 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). InterfaceComponentBound already bounds locked domains by interface size plus one.
PolarizedBirthDomains treats the forced conjugate-birth field itself: charge $+1$ on $x>0$, $-1$ on $x<0$, $0$ on the spine. That field collapses to exactly three locked domains at every radius, so carried state is $O(1)$ while the world is $\Theta(t^d)$. PolarizedBirthInterface shows the complementary fact: recognition activity (bichromatic edges) lives on the spine.
This module packages that interface as an explicit Finset of ordered edges and computes its size. Sibling definitions build the edge index, membership on spine and neighbors, and the equality between interface length and Finset card.
proof idea
The module constructs the bichromatic ordered-edge Finset $B$ by indexing spine-adjacent pairs via an edge index map (edgeIndex / edgeFromIndex) with proven cardinality. Membership lemmas (memSpine, memNbr) pin which lattice adjacencies cross charge. interface_card_eq and interface_length_eq identify Finset card with interface length; interface_increment_const shows the count grows by a fixed amount per rung. The closed forms $8t-4$ (2D) and $8t^2-8t+4$ (3D) follow by summing the constant increment against the spine geometry already fixed upstream.
why it matters in Recognition Science
LatticeBallEdges imports this module as the interface half of the ledger: "PolarizedBirthInterfaceCount counts the interface exactly... That is the cost the engine pays." The parent then counts total ordered adjacencies and monochromatic (carried-internal) edges carried for free, giving the exact carried-versus-interface split on the L1 ball.
In the Recognition cosmology chain this closes the cost side of polarized birth after PolarizedBirthDomains closed the carried side. Together with InterfaceComponentBound and LatticeBallVolume, it turns the numeric coarsening reports (domain counts, diamond/octahedron growth) into theorem-level accounting: interface cost linear in $t$ (2D) or quadratic (3D), while locked domains stay $O(1)$. No forcing-chain landmark (T5–T8) is restated here; the module is pure discrete geometry feeding the cosmogenesis cost ledger.
scope and limits
- Does not bound or count monochromatic (same-charge) edges; that is LatticeBallEdges.
- Does not treat arbitrary charge fields; only the forced polarized birth field.
- Does not re-prove locked-domain $O(1)$ bounds; those live in PolarizedBirthDomains.
- Does not address continuum limits, curvature, or physical units beyond lattice combinatorics.
- Does not claim the count for non-L1 balls or non-integer radii.
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