IndisputableMonolith.Cosmology.LatticeBallEdges
Exact edge ledger for the 2D L1 lattice ball under the polarized birth field: every 4-neighbour adjacency is classified as monochromatic (carried) or bichromatic (interface), with closed cardinalities for each class and for the total. Cosmology proofs that weight recognition cost by edge type cite this module. The argument is combinatorial enumeration over the four unit directions and the four axial boundary faces.
claimOn the 2D $L^1$ ball (diamond) of radius $t$, the ordered 4-neighbour edge set decomposes as the disjoint union of monochromatic carried edges and bichromatic interface edges along the birth-field spine. The module supplies exact finite cardinalities for the direction set, each axial boundary, the carried class, the interface class, and the total edge count.
background
The scale-adaptive coarsening engine grows its world on an $L^1$ ball, one rung per recognition cycle. In 2D that ball is the diamond $|x|+|y|\le t$. Neighbours are the four unit steps $(\pm 1,0)$ and $(0,\pm 1)$. Upstream, LatticeBallVolume closed the cell counts; PolarizedBirthDomains showed the forced conjugate-birth field ($+1$ on $x>0$, $-1$ on $x<0$, $0$ on the spine) is held in exactly three locked domains; PolarizedBirthInterface and PolarizedBirthInterfaceCount confined recognition activity to the spine and counted interface edges exactly.
What remained open was the complementary bulk ledger: how many monochromatic adjacencies sit inside each half-plane, and how the total edge count splits as interface plus carried. This module introduces the direction set, the four axial boundary slices, and the global edge set $E$, then pins their cardinalities over $\mathbb{N}$.
proof idea
Definition-first combinatorial module. It fixes the four unit directions and proves their cardinality is 4. It defines the global ordered-edge set $E$ by ranging over ball cells and admissible steps that stay inside the ball, together with the four axial boundary faces (positive/negative $x$ and $y$). Cardinality lemmas then count each boundary slice by a one-dimensional step formula, assemble the domain-set count, and obtain the total edge cardinality as a closed polynomial in the radius. The interface-versus-carried split is inherited from the polarized field already fixed upstream; this module only finishes the arithmetic of the full adjacency list.
why it matters in Recognition Science
Phase 54 in the cosmogenesis chain. Downstream, PolarizedBirthInterfaceCost weights this ledger by the recognition cost $J(x)=(x+x^{-1})/2-1$ (unique by the Recognition Composition Law / T5) evaluated at the phi-rung charge gap: carried monochromatic edges cost nothing in the ledger, interface bichromatic edges are paid. Without exact total = interface + carried counts, the cost theorem cannot convert sub-extensive interface geometry into an $O(1)$-per-cycle recognition bill while the world is $\Theta(t^2)$. The module therefore closes the last purely combinatorial gap between the polarized birth geometry and the costed coarsening ledger.
scope and limits
- Does not treat the 3D octahedron or higher-dimensional $L^1$ balls.
- Does not assign recognition costs; only unweighted edge cardinalities.
- Does not re-prove interface confinement to the spine; that is upstream.
- Does not address non-polarized or arbitrary charge fields.
- Does not claim continuum or Euclidean edge measures.
used by (1)
depends on (5)
declarations in this module (22)
-
def
dirs -
theorem
dirs_card -
def
E -
def
Dset -
theorem
boundary_xpos -
theorem
boundary_xneg -
theorem
boundary_ypos -
theorem
boundary_yneg -
theorem
step_card -
theorem
Dset_card -
theorem
total_edge_card -
theorem
edges_length -
def
carried -
theorem
carried_edge_card -
theorem
interface_sq_le_total -
theorem
carried_ge_interface -
theorem
boundary_zpos -
theorem
boundary_zneg -
theorem
three_mul_step_card -
theorem
three_mul_Dset_card -
theorem
three_mul_total_edge_card -
theorem
interface_cube_le_total_sq