imbalanceSq_loopPoint_native
plain-language theorem explainer
The squared vertex-imbalance total of the canonical loop-point complex is exactly zero. Gravity and ledger-cost workers cite this as the elementary witness that a one-loop-plus-isolated-vertex complex posts a balanced double-entry row at every vertex, hence pays no history cost. The proof is a one-line native decision of the finite integer sum.
Claim. For the bounded complex consisting of one loop at a vertex together with one isolated vertex, the squared-imbalance total $\sum_v (\mathrm{indeg}(v)-\mathrm{outdeg}(v))^2$ equals $0$.
background
Gap 2 (C14) freezes a pre-registered admissibility class for letter costs: a cost is ledger-generated when each letter is charged only from its own posting row (vertex imbalance for vertices; constants for edges and top-cells). The integer kernel of the recognition cost is the squared-imbalance total of a bounded complex: sum over vertices of (indegree minus outdegree) squared. That quantity is the integer part of $J$ and feeds history cost via $\mathrm{historyCost}=\mathrm{imbalanceSq}/(2\kappa)$.
The loop-point complex is the size-capped complex with two vertices, one edge, and no top-cells: a single loop at vertex $0$ plus an isolated vertex. Its count vector is $(2,1,0)$, identical to that of a proper edge, but every local posting balances, so the complex is the elementary zero-cost witness in the C15 enumeration harness.
proof idea
One-line wrapper: native_decide evaluates the finite sum defining the squared-imbalance total on the concrete loop-point complex and certifies equality with zero. No intermediate lemmas are invoked beyond the definitions of the complex and of the sum.
why it matters
Inside the LedgerGenerated fork gate, this identity separates isomorphism-class data from posting-row data: the loop-point complex shares the count vector of a proper edge yet contributes zero imbalance, so any cost that charges only local imbalances must treat them differently. That contrast is exactly what the pre-registered predicate uses when deciding whether $j\mathrm{Cost}$ is ledger-generated at small caps. The result sits in the Gap-2 measurement path that closes the escape class left by the bulk-cancelling fixed-kind-totals dichotomy (A1.7) and feeds the C15 diamond-rank / SJ-spectra tabulation. No downstream theorems currently depend on it in the graph; it is a certified atomic fact for the fork decision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.