properEdgeCount_loopAndBridge
plain-language theorem explainer
On the three-vertex complex with one loop and one bridge edge, exactly one edge has distinct endpoints. Anyone deriving centered incidence charges for Gap 2's posting-cost story cites this count. The proof is a one-line decision-procedure check on the finite incidence data.
Claim. For the bounded complex with three vertices, two edges and no triangles (one loop edge and one bridge), the number of edges whose two endpoints differ equals $1$.
background
Gap 2 in the gravity seven-gaps program asks how premise (i) (size-blindness of a labeled weight) can be derived rather than assumed. This module attacks that via a posting-cost model: a complex is read as a posted history over a three-block alphabet (vertices, edges, triangles), a letter cost is summed to a history cost, and a Boltzmann factor over the alphabet gauge volume supplies the weight.
A proper edge is an edge whose two endpoints are distinct vertices. The proper-edge count is the cardinality of that subset of the edge set; it depends on incidence data, not merely on the three size parameters $(n_V,n_E,n_T)$. The test complex used here has $n_V=3$, $n_E=2$, $n_T=0$: the smallest complex whose two edge letters the centered cost must charge differently (one loop, one bridge).
That count enters the centered incidence letter cost, which shifts edge charges by a multiple of the proper-edge count so that same-kind letters can receive opposite signs on this complex.
proof idea
One-line wrapper: decide evaluates the finite filter-and-card expression defining the proper-edge count on the concrete incidence table of the loop-and-bridge complex and confirms the natural-number equality to $1$. No lemmas beyond the definitions of the complex and the count are required.
why it matters
The immediate parent is the charge computation on this complex: with proper-edge count $p=1$ and $n_E=2$, the centered incidence cost assigns $-t$ to the loop letter and $+t$ to the proper-edge letter. That opposite charging of two same-kind letters is the concrete witness that a kind-only letter cost still distinguishes loop from bridge, which is the posting-layer route toward premise (i) without an indistinguishability hypothesis.
In the module's larger arc, this is scaffolding arithmetic inside the numerator of the posted weight (history cost over gauge volume). It does not itself close Gap 2; it feeds the derivation that kind-only costs recover size-blindness of the labeled weight once the exponential Boltzmann reading is granted. Framework-wise it sits in the gravity side of Recognition Science, not in the T0–T8 forcing chain, but it supports the ledger-additive posting story used when gravity weights are built from recognition costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.