twoCell_comp_nil
plain-language theorem explainer
On the two-vertex world, the empty monochromatic edge list has exactly two locked domains. This pins the base case of the two-cell interface bound (tight at 2 ≤ 1+1). The proof rewrites through the empty-graph component identity and evaluates the finite cardinality of the two-point vertex set.
Claim. Let $V$ be the two-point vertex set. The locked-domain count of the empty edge list equals two: $\mathrm{comp}([]: \mathrm{List}(V\times V)) = 2$.
background
The module proves a dimension-free interface bound: on any finite connected world, the number of locked domains (connected components of the monochromatic graph) is at most the number of bichromatic interface edges plus one. Component count is defined as comp E := Nat.card of the quotient by the equivalence closure of the edge relation on a finite vertex type $V$, so no decidability of the closure is required.
The empty edge list is the monochromatic graph of a fully charged-separated world: every vertex is its own locked domain. The upstream identity comp_nil states that for any finite $V$, comp [] = Nat.card V. Here $V$ is the two-cell set, so the empty monochromatic graph is the pure two-domain configuration against which a single opposite-charge interface edge is later measured.
Locally this is the minimal tight instance of the headline inequality (two domains, one interface edge).
proof idea
One-line tactic proof. Rewrite by the empty-list identity comp_nil, which replaces comp [] by Nat.card of the two-point vertex type. Then simp with Nat.card_eq_fintype_card evaluates that cardinality to 2.
why it matters
Closes the empty-graph base case for the two opposite-charge cells inside the interface-component module. The module discharges the connected-graph fact previously left open in the cosmogenesis domain-coarsening scripts and their 2D/3D Lean bridges: locked-domain count ≤ interface size + 1. The two-cell world is the elementary tight instance (2 ≤ 1 + 1), so this equality is the numerical anchor for that tightness claim.
No downstream dependents are recorded yet; the declaration sits as a named specialization of comp_nil rather than a link in the T0–T8 forcing chain. It supports the classical merge argument (each restored bichromatic edge collapses at most two components) at the smallest nontrivial scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.