loopPointComplex
plain-language theorem explainer
The loop-point complex is a two-vertex, one-edge, zero-tet posting graph whose single edge is a self-loop at vertex 0 and whose second vertex is isolated. Its census triple is (2,1,0), identical to the proper edge, yet every vertex imbalance vanishes so the history cost of J is zero. Downstream proofs cite it as the free witness that J is not a function of the three counts, before any diamond gluing is considered.
Claim. The loop-point complex is the bounded complex on capacity $4$ with $n_V=2$, $n_E=1$, $n_T=0$, whose unique edge is the self-loop $(0,0)$ and whose tetrahedron incidence is empty (vacuous on $\mathrm{Fin}\,0$).
background
Gap 2 / C15 studies the J-diamond rank lattice after the census-inversion route was ruled out. Recognition cost $J$ is built from vertex-level ledger imbalance on a posting graph; the squared-imbalance total $SJ=2\kappa J$ is the integer charge used in diamond defects. A bounded complex packages finite vertex, edge, and tet counts together with incidence maps edgeVerts and tetVerts.
The three census observables $(n_V,n_E,n_T)$ are the only kind totals available to a putative rate formula. The proper edge complex already realizes the count vector $(2,1,0)$ and pays a positive history cost $1/\kappa$. The loop-point complex is the matching-count counterexample: same triple, different geometry.
Module context: subcomplexes, interface imbalance coupling, and the localization identity $D=-2\sum_v m_A(v)m_B(v)$ on edge-partitions. This definition sits upstream of those diamond facts; it is pure witness data for the count conflict.
proof idea
Pure structure definition. Counts are set to $2,1,0$; the three bound certificates are discharged by decide. The single edge is hard-coded as the self-loop $(0,0)$; the tet map is the empty elimination on Fin 0. No lemmas are invoked.
why it matters
Supplies the zero-cost side of the count conflict that precedes diamond analysis. jCost_not_a_function_of_counts pairs it with the proper edge: identical $(n_V,n_E,n_T)$ yet unequal history costs under $J$. Supporting facts imbalance_loopPoint_zero, imbalance_loopPoint_one, imbalanceSq_loopPoint, and historyCost_loopPoint compute the vanishing ledger explicitly.
Those facts feed JDiamondRankVerdict (the C15 lattice verdict) and the hostile probes that stress-test count-only formulae. In the Recognition gravity stack this closes the claim that per-kind rates cannot be read off census totals alone; the asymmetry of $J$ is geometric, not combinatorial. No forcing-chain landmark (T5–T8) is touched directly; the object is local to Gap 2 / A15 successor work on diamond rank.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.