imbalance_loopPoint_zero
plain-language theorem explainer
The loop-point complex (one self-loop at a vertex plus an isolated vertex) has vanishing ledger imbalance at the looped vertex. Anyone evaluating recognition history cost on this zero-cost witness needs the fact. The proof is a one-line finite decision on the incidence table.
Claim. Let $K$ be the bounded complex with two vertices and one edge that is a self-loop at vertex $0$ (plus an isolated vertex). The net recognition imbalance of vertex $0$ in $K$, namely in-degree minus out-degree, equals $0$.
background
In the Gap-2 / C15 setting, recognition cost $J$ is built from vertex-level ledger imbalance on posting graphs (bounded complexes). The imbalance of a vertex is the integer difference of its in-degree and out-degree, read from the ordered edge incidence of the complex; the squared-imbalance total is the integer part of $J$.
The loop-point complex is the two-vertex, one-edge witness with a self-loop at vertex $0$ and one isolated vertex. Its census count vector is $(2,1,0)$, matching a proper edge, but every posting balances at its own vertex, so the complex is intended to pay nothing.
This module studies J-diamonds (four-term inclusion-exclusion defects of $J$ on overlapping subcomplexes) after the census-inversion route was ruled out. Zero imbalance on the loop-point witness is a basic incidence fact used when history cost is evaluated on that complex.
proof idea
One-line kernel proof: decide discharges equality of two concrete integers computed from the finite incidence data of loopPointComplex at vertex $0$. No lemmas are invoked beyond the definitions of the complex and of vertex imbalance (in-degree minus out-degree).
why it matters
Feeds historyCost_loopPoint, which shows that the recognition history cost of the loop-point complex vanishes for any positive scale $\kappa$. That zero-cost witness separates census type from actual $J$-payment: the count vector matches a proper edge, yet imbalance (hence $J$) is zero at both vertices.
In the broader Gap-2 program this supports the claim that $J$ is not a valuation on complexes and that cost localizes on imbalance rather than on bare edge counts. It is a small but necessary incidence lemma on the path from diamond-defect localization to the rank test on J-diamonds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.