edgeComplex_fits_cap2
plain-language theorem explainer
The canonical one-edge complex has vertex, edge, and tet counts all at most 2. Gravity auditors cite it when arming the C27 trigger at size cap 2 in the Gap-2 ledger-generated fork. The proof is a one-line native decision on the frozen census values of that complex.
Claim. Let $K$ be the bounded complex consisting of a single directed edge $0\to 1$. Then its vertex count, edge count, and tet count each satisfy $n_V(K)\le 2$, $n_E(K)\le 2$, and $n_T(K)\le 2$.
background
Gap 2 (C14) is the LedgerGenerated fork gate: a pre-registered TRUE/FALSE measurement that decides whether the canonical recognition cost $jCost$ is ledger-generated. Ledger-generated means letter charges come 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.
The census observables $n_V$, $n_E$, $n_T$ extract vertex, edge, and tet counts from a bounded complex (or ensemble). The object edgeComplex is the minimal directed complex with one edge $0\to 1$: frozen counts $n_V=2$, $n_E=1$, $n_T=0$ inside BoundedComplex 4. Size caps restrict which complexes enter the finite decision LedgerGeneratedAt cap (jCost 1).
This lemma only certifies that the one-edge complex sits inside cap 2, so it is an admissible witness when the C27 trigger asks for a complex of size at most 2 with nonzero history cost.
proof idea
One-line wrapper: native_decide evaluates the three numeric inequalities on the concrete fields of edgeComplex ($n_V=2$, $n_E=1$, $n_T=0$). No lemmas are invoked beyond the definitional unfolding of those census projections.
why it matters
Parent use is C27_trigger_armed_cap2, which packages ledger-generation of $jCost$ at cap 2 together with a concrete nonzero-history-cost witness. The trigger refinement explicitly threads the three conjuncts of this theorem as the size bounds on edgeComplex, then pairs them with historyCost_not_identically_zero_cap2.
In the Gap-2 story, A1.7 closed the bulk-cancelling fixed-kind-totals class; the escape class is where nonzero history cost can still live. Arming C27 at cap 2 is a measured step toward deciding whether $jCost$ is ledger-generated on the C15 isomorphism classes. The result is local bookkeeping, not a forcing-chain landmark (T5–T8), but it is required scaffolding for the fork gate that feeds the gravity seven-gaps program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.