proj
plain-language theorem explainer
Canonical surjection from locked domains of a graph to locked domains after adjoining one edge. Cosmology component-count arguments cite it as the map that collapses at most one pair of classes. Built by lifting the identity on vertices through the quotient, with well-definedness from edge-list monotonicity of the connectivity closure.
Claim. For vertices $a,b$ and edge list $X$, there is a well-defined map $Q(X)\to Q((a,b)::X)$ from the quotient by connectivity closure of $X$ to the quotient after adjoining the edge $(a,b)$, sending the class of each vertex $v$ to its class under the coarser relation.
background
The module proves a dimension-free bound on locked domains in Recognition cosmogenesis: on any finite connected world, monochromatic components are at most the bichromatic interface size plus one. Vertices form a finite type $V$; an edge list $E$ is the ambient adjacency. Connectivity closure clos E is the equivalence generated by those edges; cs E packages it as a Setoid, and its quotient is the set of locked domains (components), counted by Nat.card without decidability on the closure.
Adding edges only merges domains. The atomic step is one new edge $(a,b)$ prepended to $X$: the finer quotient (fewer edges) maps onto the coarser one. Upstream, clos_mono_cons records that every prior connection survives: if clos X u v then clos ((a,b)::X) u v. That monotonicity is exactly what makes the identity on vertices descend to quotients.
proof idea
One-line Quotient.lift of the identity. On representatives, send $v$ to the class of $v$ in the coarser setoid cs ((a,b)::X). Well-definedness: if $u\sim v$ under clos X, then clos_mono_cons gives $u\sim v$ under clos ((a,b)::X), so Quotient.sound identifies the images. No further case analysis.
why it matters
This map is the structural core of the atomic merge bound comp_le_comp_cons: adding one edge lowers component count by at most one. That theorem builds an Option-valued injection on the finer quotient that is injective away from the single class the new edge can collapse into, and the comparison of classes is literally equality under this projection.
Iterating the atomic step over the bichromatic interface and using connectedness of the ambient world yields the headline mono_components_le_bichromatic_succ, closing the open connected-graph fact from the 2D/3D domain-coarsening scripts. In Recognition terms it is the combinatorial half of "locked domains are at most the interface plus one," the graph-theoretic reading of coarsening under the recognition law. Downstream quotient and Clifford uses of similarly named projections are separate; the local parent is the merge bound in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.