probe_loopPoint_counts
plain-language theorem explainer
The loop-point complex has census counts (vertices, edges, tets) equal to (2, 1, 0). Hostile-probe authors cite this to lock the shared count vector against the proper-edge complex before comparing SJ costs. The proof is pure definitional equality: three reflexivity steps on the structure fields.
Claim. For the loop-point complex (one loop at a vertex plus one isolated vertex), the census observables satisfy $n_V = 2$, $n_E = 1$, and $n_T = 0$.
background
The ambient module is an adversarial probe of the C15 J-diamond rank lattice. It never edits the reviewed Gap2JDiamondRank development; failed attacks are treated as evidence for the reviewed claims. One headline attack is a count-vector collision: two complexes share the same $(n_V, n_E, n_T)$ yet carry different SJ costs.
Census observables $n_V$, $n_E$, $n_T$ extract the vertex, edge, and tet (free-label) components of a bounded complex ensemble. The loop-point complex is defined as one loop at vertex $0$ together with one isolated vertex; its doc-comment states that its count vector is $(2,1,0)$, matching a proper edge, while every posting balances locally so the complex pays nothing.
That shared vector is the setup for later probes that contrast SJ cost $2$ (edge) against SJ cost $0$ (loop-point).
proof idea
One-line term proof. The structure loopPointComplex is defined with literal fields nV := 2, nE := 1, nT := 0, so the three equalities are rfl. Pack them as a triple of proofs of equality.
why it matters
This is witness arithmetic for the hostile probe of Gap 2 (J-diamond rank). The module doc lists a count-vector conflict on $(2,1,0)$ with SJ costs $2$ versus $0$ as a primary attack surface. Pinning the loop-point side of that vector is the first half of the collision; sibling probes handle the edge side and the SJ-cost comparison.
No downstream theorem currently depends on this declaration (used-by is empty). Its role is local certification inside the adversarial suite: if the reviewed lattice treats count vectors as the only input to cost, the loop-point versus edge pair is a concrete counterexample shape. The probe records that the inconsistency theorems quantify over rational rate triples, not library LetterCost, as a scope note rather than a false claim.
Framework context is gravity-side Gap 2 scaffolding around diamond rank and SJ defect bookkeeping, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.