Subcomplex
plain-language theorem explainer
A subcomplex of a bounded posting complex is an edge subset together with a vertex set closed under both endpoints of every selected edge. It is the basic region type for J-diamonds: pairs of proper subcomplexes whose union is the whole complex. Downstream defect and localization theorems quantify on this type. The declaration is pure data with two endpoint-closure axioms; no proof body.
Claim. Fix a bounded complex $K$ on a posting budget $B$. A subcomplex of $K$ consists of a finite vertex set $V'\subseteq V(K)$ and a finite edge set $E'\subseteq E(K)$ such that for every $e\in E'$, both the tail and the head of $e$ lie in $V'$.
background
Gap 2 / C15 studies the J-diamond rank lattice after the census-inversion route was ruled out: the recognition cost $J$ built from vertex-level ledger imbalance is not a valuation and its moment vector lies outside the census span. The successor test is rank and consistency of four-term inclusion-exclusion defects of $J$ on overlapping regions.
A bounded complex $K$ is a finite directed posting graph with fixed vertex and edge counts and an endpoint map sending each edge index to an ordered pair of vertices. The integer squared-imbalance total $SJ=2\kappa J$ is summed from per-vertex imbalance on chosen edge sets. A subcomplex packages a region on which those imbalance sums are well-defined: edges may be thinned, but every retained edge must keep both endpoints inside the chosen vertex set, so induced imbalance never refers to missing vertices.
The module treats a J-diamond as an unordered pair of proper subcomplexes whose edge-union recovers $K$; the interface is the vertex (and edge) overlap. That geometry is exactly what the present structure records.
proof idea
No proof: this is a structure declaration. Fields are a vertex Finset, an edge Finset, and two universal closure axioms (tail and head of every selected edge land in the vertex set). Downstream definitions build imbalance, charge, and diamond defect by projecting onto these fields; theorems such as the interface-coupling identity quantify over pairs of inhabitants of this type.
why it matters
Every object in the J-diamond calculus is typed by this structure: diamond defect, the localization theorem equating the four-term defect to minus twice the interface inner product of the two imbalance fields, the empty-interface exactness corollary, and the interface-balanced vanishing corollary. Concrete seed regions (out-star forks and spurs, path sides) are packaged as subcomplexes. The C15 verdict structure records the localization identity universally over subcomplex pairs on bounded complexes of budget 4. Without endpoint-closed regions, the inclusion-exclusion stand-off between two accumulation orders of the same complex is not even well-formed, so the non-valuation of $J$ and the support of its gluing asymmetry on boundary imbalance cannot be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.