loopAndBridge
plain-language theorem explainer
A minimal 3-vertex complex with one self-loop and one proper edge (no tetrahedra). It is the smallest BoundedComplex 3 on which a centered letter cost must assign unequal charges to the two edge letters. Downstream Gap-2 arguments cite it as the witness complex for non-equivariance, fibre non-triviality, and injectivity of tilted numerators.
Claim. Define a bounded complex of bound $3$ with $n_V=3$ vertices, $n_E=2$ edges, and $n_T=0$ tetrahedra, with edge $0$ the loop $(0,0)$ and edge $1$ the proper edge $(1,2)$. Bound witnesses are reflexivity of $3\le 3$, $2\le 3$, and $0\le 3$; the empty tetrahedron map is vacuous.
background
Gap 2 works at the posting layer: a complex is read as a history of letters indexed by the three blocks Fin nV ⊕ Fin nE ⊕ Fin nT, and a LetterCost assigns a real charge to each letter. The history cost is the sum of those charges; the posted weight is the Boltzmann factor of that cost divided by the gauge volume (the reciprocal of the order of the three sort-respecting symmetric groups on the letter blocks).
A BoundedComplex B packages finite vertex/edge/tetrahedron counts at most $B$, together with incidence maps edgeVerts and tetVerts. The module derives premise (i) of the gluing argument from kind-only letter costs rather than from size-blindness indistinguishability premises.
The present object is the smallest complex whose two edge letters are geometrically unlike: one is a loop, one is a proper edge. That asymmetry is what forces a centered incidence cost to treat the two edge letters differently.
proof idea
Pure structure definition. Counts are hard-coded ($3,2,0$). Bound proofs are le_refl 3, norm_num for $2\le 3$, and Nat.zero_le 3. The edge map is a two-branch conditional: edge $0\mapsto(0,0)$, else $(1,2)$. The tetrahedron map is elim0 on the empty type Fin 0. No lemmas beyond reflexivity and zero-le are needed.
why it matters
This complex is the standard witness for Gap-2 posting-cost arguments. Downstream, the_letter_level_fibre_is_not_a_point evaluates a nonzero centered incidence cost on its second edge letter while proving the history cost vanishes on every complex, so impossibility must be stated at history cost, not letter cost. LetterCostDichotomyVerdict packages that dichotomy.
In the non-equivariant posting stream it anchors concrete evaluations: keyAt_loopAndBridge_zero/one, edgeSign_loopAndBridge, family_injective_at_loopAndBridge (tilted numerators separate continuously), and equivariance_is_load_bearing / nonequivariant_cost_posts_mu_with_nonunit_numerator, which show that dropping equivariance lets a cost post $\mu$ with non-unit numerator. It is scaffolding geometry for the posting-cost derivation of premise (i), not a forcing-chain landmark (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.