twoLoops_edges_loop
plain-language theorem explainer
Every edge of the two-loop complex is a genuine loop: its two recorded endpoints coincide. The fact is pure finite enumeration and is cited when showing that incidence cost is not kind-only, since loops contribute zero incidence charge while bridges of the same edge count do not. The proof is a one-line `decide` on the finite edge table.
Claim. For every edge $e$ of the two-loop complex, the two endpoints of $e$ are equal: no edge has distinct endpoints.
background
This module attacks Gap 2 premise (i) from a posting-cost side rather than from an indistinguishability premise. Complexes are read as posted histories over a three-block alphabet (vertices, edges, triangles). A letter cost assigns a real to each letter; history cost sums those charges; posted weight is the Boltzmann factor of that cost over the gauge volume $1/(nV!,nE!,nT!)$.
Among candidate letter costs is incidence cost, which charges an edge letter by a rate $t$ only when the edge joins distinct vertices. The complex twoLoops is the finite test object with two loop edges (each endpoint pair identical). The companion complex twoBridges has the same edge count but non-loop edges, so the same edge letter is charged differently under incidence cost.
Upstream edge-vertex infrastructure (edge lists, edgeVerts) supplies the endpoint projection used here; the present lemma only records the loop property of this particular complex.
proof idea
Finite decision procedure. The statement quantifies over Fin twoLoops.nE and compares the two components of edgeVerts e. Both the index type and the endpoint table are concrete finite data, so decide discharges the universal claim with no further lemmas.
why it matters
Feeds directly into incidenceCost_not_kindOnly, whose doc-comment states the point: two complexes at the same cap with the same number of edges charge the same edge letter differently (twoBridges charges $t$, twoLoops charges nothing), so no triple of kind-only rates can reproduce incidence cost.
That negative result is part of Gap 2's posting-cost derivation path: kind-only letter costs do give premise (i) and the measure, but incidence cost (a natural geometric charge) is not kind-only. The lemma is the small geometric fact that makes the twoLoops side of the counterexample hold. It sits inside the gravity SevenGaps stack rather than the T0–T8 forcing chain; its role is local to the Gap 2 premise inventory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.