oneVertex
plain-language theorem explainer
The one-vertex complex is the atom with sizes (1,0,0): one vertex, no edges, no tetrahedra. It is the minimal BoundedComplex used as a comparison point when testing whether a letter charge can be kind-only. Construction fills the structure fields with reflexive size bounds and empty edge/tet vertex maps via elim0.
Claim. Let $K_1$ be the bounded complex of size bound $1$ with $n_V=1$, $n_E=0$, $n_T=0$. Edge and tetrahedron vertex maps are empty (vacuous on the empty finite types). This is the one-vertex atom in the letter-cost state space.
background
Gap 2 asks whether the letter-cost space forces the kind rule: a letter's cost depends only on its kind (vertex, edge, or tet), with the same three reals at every complex. The residual after Gap2PostingCostDerivation is exactly that clause; this module exhibits equivariant letter costs that break it.
A BoundedComplex n packages finite counts $n_V,n_E,n_T \le n$ together with maps assigning vertices to each edge and tet. The one-vertex complex is the atom with sizes $(1,0,0)$. Its counterpart is the two-vertex complex used in the same countermodel arguments.
Upstream arithmetic supplies le_refl and zero_le for the size inequalities; empty-index elimination (elim0) discharges the edge and tet vertex maps when those index types are empty.
proof idea
Structure construction, not a proof. Set $n_V=1$, $n_E=0$, $n_T=0$. Discharge the three size bounds by le_refl 1 and Nat.zero_le 1. Define edgeVerts and tetVerts by elim0 on the empty edge and tet index types, so there are no vertices to assign.
why it matters
Parent use is pairCost_not_kindOnly: the vertex-count charge $\uparrow n_V-1$ equals $0$ on this atom and $1$ on the two-vertex complex, so no single vertex rate works for every complex. That theorem is T1 of the module: the kind rule fails in the letter-cost space not only by incidence (incidenceCost) but also by a counts-only equivariant charge (pairCost).
The module scope is deliberately the letter-cost layer, not the dual-entry ledger below it. Whether the ledger forces the kind rule remains the open successor; this atom only supplies the size-varying witness needed to separate kind-only from count-dependent charging inside LetterCost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.