loop1Complex
plain-language theorem explainer
The unique cap-1 complex with one vertex and one self-loop edge (no tetrahedra). Gravity and Gap-2 auditors cite it as the nontrivial seed in the C15 census at size 1 when testing whether recognition cost is ledger-generated. The body is a structure instance: census bounds by decide, edge map constantly (0,0), empty tet map.
Claim. Let $K$ be the bounded complex of cap $1$ with $n_V=1$, $n_E=1$, $n_T=0$, whose unique edge is the self-loop $(0,0)$ and whose tetrahedron map is empty. This is the cap-1 loop complex.
background
Gap 2 (C14) asks whether the canonical recognition letter cost $jCost$ is ledger-generated: charged only from each letter's own double-entry row (vertex imbalance $indeg-outdeg$ via a vertex charge $f_V$, plus constants $c_E,c_T$ on edges and top-cells). Forbidden inputs include orbit sums and global census data beyond the letter's row.
Bounded complexes package finite vertex/edge/tet censuses with explicit incidence maps. Cap $B$ restricts those counts. The C15 harness enumerates isomorphism classes at small caps; at cap 1 the nontrivial seed is a single self-loop.
Upstream census observables $n_V,n_E,n_T$ and incidence patterns (Freudenthal edge/tet tables, rung-descent edge vertices) supply the same shape of data this instance freezes for the loop.
proof idea
Definitional structure instance for BoundedComplex 1. Set $n_V=1$, $n_E=1$, $n_T=0$; discharge the three bound proofs by decide. Map the unique edge index to the pair $(0,0)$ (self-loop). The tet map is elim0 on the empty finite type. No lemmas beyond decidable arithmetic on the census bounds.
why it matters
Supplies the only nontrivial cap-1 seed for the LedgerGenerated fork. Downstream: imbalanceSq_loop1 (and native twin) prove squared imbalance is zero; historyCost_loop1 then gives history cost zero at $jCost,1$; historyCost_table_cap1 packages empty, point, and loop costs all zero. C27_not_armed_by_cap1_seeds records that cap-1 seeds alone do not arm C27 (ledger-generated and history zero). The aggregate LedgerGeneratedVerdict structure cites the cap-1 decision among the measured outcomes. In the RS gravity stack this is measurement infrastructure for the tilt fork behind flag 8, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.