edgeComplex_fits_cap3
plain-language theorem explainer
The canonical one-edge complex sits inside every size cap of 3 or larger: two vertices, one edge, zero tets. Gravity/Gap-2 auditors cite it when arming the C27 ledger-generated trigger at cap 3, since the witness complex must fit the enumeration bound. The proof is a one-shot native decision on the three concrete inequalities.
Claim. Let $K$ be the bounded complex consisting of a single directed edge $0\to 1$ (so $n_V(K)=2$, $n_E(K)=1$, $n_T(K)=0$). Then $n_V(K)\le 3$, $n_E(K)\le 3$, and $n_T(K)\le 3$.
background
Gap 2 / C14 asks whether the recognition cost jCost is ledger-generated: charged only from each letter's own double-entry posting row (vertex imbalance for vertices; constants for edges and top-cells), with no orbit sums or global census inputs. Finite restrictions of that predicate are decided at size caps 1, 2, 3 against the C15 isomorphism classes.
The witness complex used here is the elementary directed edge $0\to 1$, frozen as a BoundedComplex 4 with vertex count 2, edge count 1, and tet count 0. The three observables $n_V$, $n_E$, $n_T$ are the census projections that extract those counts from an ensemble point; on this complex they are the literal structure fields.
Fitting a complex under a cap means all three counts are at most the cap. Cap-3 fitness of the edge complex is the size gate needed before its history cost can serve as a nonzero witness inside the C27 trigger.
proof idea
Pure computational discharge. The structure fields of the edge complex are definitionally $2$, $1$, and $0$; native_decide evaluates the three inequalities $2\le 3$, $1\le 3$, $0\le 3$ in the kernel and closes the conjunction. No lemmas are invoked beyond the definitional unfolding of those fields.
why it matters
Parent use is C27_trigger_armed_cap3, which packages ledger-generation of jCost at cap 3 together with a concrete complex whose history cost is not identically zero. The three conjuncts of this theorem supply the size bounds in that package:
refine ⟨4, edgeComplex, edgeComplex_fits_cap3.1,
edgeComplex_fits_cap3.2.1, edgeComplex_fits_cap3.2.2, ...⟩
Inside the Seven Gaps gravity stack this is bookkeeping, not physics derivation: it certifies that the simplest nonzero-history witness is admissible at the pre-registered cap-3 measurement. It does not itself decide the ledger-generated fork; it only clears the size gate so the C27 hard-stop can be armed when the cap-3 decision and the nonzero history-cost lemma are both in hand. Framework-wise it sits under Gap 2's escape-class analysis after A1.7 closed the bulk-cancelling fixed-kind-totals class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.