closedForm_or_empty
plain-language theorem explainer
Every bounded complex on the carrier is either vertex-bearing or fully empty (zero vertices, edges, and triangles). Anyone applying the closed-form size-blind weight to all complexes the carrier contains cites this dichotomy: the unit clause covers the empty case, and everything else has a vertex. The proof is a short case split on incidence counts, using vertex-of-incidence when edges or triangles appear.
Claim. Let $f:\mathbb{N}^3\to\mathbb{R}$ satisfy the carrier shuffle identities (positivity, unit weight on the empty size triple, and the dust/bouquet and dust/edge gluing identities). For every bounded complex $K$, either $n_V(K)\ge 1$, or $n_V(K)=n_E(K)=n_T(K)=0$.
background
Gap 2 aims to derive the gluing law rather than assume it. The prior gauge-volume module showed that a gluing law forces inverse factorials and hence the gauge-counting principle; this module supplies the missing disjoint-union structure on the carrier and reduces the premise to size-blindness plus gluing multiplicativity.
A size-blind weight $f(a,b,c)$ depends only on the three index sizes (vertices, edges, triangles). CarrierShuffle f packages the four gluing instances the carrier actually supplies as identities on those sizes: positivity, $f(0,0,0)=1$, and the dust-bouquet / dust-edge shuffle relations already transported through the interleaving factor.
A BoundedComplex B is a finite complex whose size triple $(n_V,n_E,n_T)$ is controlled by the bound $B$. The closed-form solutions of the three-variable shuffle are of the shape $f(a,b,c)=x^a y^b z^c/(a!b!c!)$; to apply that form to every complex the carrier contains, one needs a clean empty-versus-nonempty split.
proof idea
Case on whether $n_E+n_T>0$. If so, vertex_of_incidence immediately yields $n_V\ge 1$, giving the left disjunct. If not, case on $n_V$: a positive vertex count again gives the left disjunct; otherwise $n_V=0$ together with $n_E+n_T=0$ forces all three counts to zero by elementary arithmetic (omega), giving the right disjunct. No appeal to the shuffle identities beyond the ambient hypotheses is required.
why it matters
In the Gap 2 derivation, the closed form of a size-blind multiplicative weight is pinned down on nonempty size triples by the shuffle identity, while the empty triple is fixed by the unit clause $f(0,0,0)=1$. This lemma is the bookkeeping bridge: every complex the carrier can present falls into exactly one of those two regimes, so the closed form applies universally without a leftover "incidences but no vertices" ghost case.
The module's larger goal is to replace an assumed gluing law by two local premises (size-blindness and multiplicativity over disjoint union), recovering $f(a,b,c)=x^a y^b z^c/(a!b!c!)$ and thereby the inverse-factorial gauge volume. No downstream theorems currently depend on this declaration; it sits as an internal hygiene step next to the closed-form application and the later sector-fugacity material that measures the $1/|\mathrm{Aut}|$ factor rather than asserting it by headline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.