module module high

`IndisputableMonolith.Cosmology.InterfaceComponentBound`

Defines the graph-theoretic substrate for locked domains on lattice balls: adjacency from ordered edge lists, its equivalence closure, and the resulting component partition. Cosmology modules cite it to bound how many monochromatic domains a charge field can form. The development is pure finite-set combinatorics over Mathlib equivalence relations, with no physics axioms.

claimFrom a finite list of ordered pairs $E \subseteq V \times V$, form the base adjacency relation, take its equivalence closure $\sim_E$ (symmetrized transitive reflexive hull), and partition $V$ into connected components. The locked-domain count is the number of classes of $\sim_E$. Orientation of each pair is irrelevant once the closure is taken.

background

Recognition Science coarsening accumulates a discrete world on L1 balls (2D diamonds $|x|+|y|\le t$, 3D octahedra $|x|+|y|+|z|\le t$). A charge or birth field on the cells induces monochromatic regions separated by bichromatic edges. Those monochromatic regions are the locked domains the engine must carry; the bichromatic cut is the recognition-active interface it pays for.

This module supplies the pure combinatorial language for that split. An edge list of ordered pairs generates a base adjacency; the equivalence closure symmetrizes and transitively closes it, so undirected connectivity is recovered regardless of list orientation. Components of that relation are the candidate locked domains. Downstream phases specialize the vertex set to lattice balls and the edge set to nearest-neighbor pairs filtered by a field.

The module sits at Phase 48 of the cosmology stack: it proves, for arbitrary charge fields on the diamond and octahedron, that the number of locked domains is at most the interface size plus one.

proof idea

Definition-first development of finite relations. Generate the base relation from an edge list; form the equivalence closure via Mathlib's EqvGen; prove monotonicity under list extension and a merge lemma when a connecting edge is adjoined. Component count is the cardinality of the quotient. The interface-plus-one bound is obtained by induction on edges: each new bichromatic edge merges at most two classes, so components cannot exceed interface edges plus the initial connected pieces. No analytic estimates; only finite equivalence-relation algebra.

why it matters in Recognition Science

Parent substrate for the polarized-birth ledger. PolarizedBirthDomains quotes Phase 48 as having proved the locked-domain count is at most interface plus one for any charge field, then specializes to the forced conjugate-birth field and obtains exactly three domains (carried state $O(1)$ while the world is $\Theta(t^d)$). PolarizedBirthInterface and PolarizedBirthInterfaceCount close the complementary interface side (spine confinement and exact bichromatic edge counts $8t-4$ in 2D, $8t^2-8t+4$ in 3D). LatticeBallEdges and LatticeBallVolume import the same adjacency language to count total versus monochromatic edges and closed-form cell counts.

In the broader RS picture this is the combinatorial half of sub-extensivity: recognition cost lives on the interface, carried state stays bounded, consistent with eight-tick octave bookkeeping and scale-adaptive coarsening without extensive memory growth.

scope and limits

Does not fix a particular charge or birth field; the bound is field-agnostic.
Does not count edges or cells; only components of a given adjacency list.
Does not prove continuum or infinite-lattice limits.
Does not introduce physical constants, phi-ladder masses, or dynamical evolution.
Does not assert the bound is sharp for every field; sharpness is left to specializations.

used by (5)

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

IndisputableMonolith.Cosmology.LatticeBallEdges module_import
IndisputableMonolith.Cosmology.LatticeBallVolume module_import
IndisputableMonolith.Cosmology.PolarizedBirthDomains module_import
IndisputableMonolith.Cosmology.PolarizedBirthInterface module_import
IndisputableMonolith.Cosmology.PolarizedBirthInterfaceCount module_import

declarations in this module (37)

def gen L57
def clos L61
theorem clos_equiv L63
def cs L66
def comp L70
theorem eqvGen_le L74
theorem clos_mono_cons L85
def merged L93
theorem merged_equiv L96
theorem gen_cons_le_merged L120
theorem clos_cons_iff L131
def proj L147
theorem card_le_succ_of_merge L153
theorem comp_le_comp_cons L179
theorem comp_congr L193
theorem comp_le_comp_append L207
theorem clos_nil L226
theorem comp_nil L236
theorem comp_eq_one_of_connected L245
theorem mono_components_le_bichromatic_succ L258
theorem clos_root_of_descent L293
theorem connected_of_descent L318
theorem mono_le_interface_of_descent L331
theorem twoCell_connected L344
theorem twoCell_comp_nil L359
theorem twoCell_interface_bound L364
def ball L384
theorem mem_ball_iff L388
abbrev Vtx L397
def height L400
def center L403
def adj L408
def edges L413
theorem mem_edges L416
theorem hzero L422
theorem descent L432
theorem mono_le_interface_succ L463