probe_same_count_vector
plain-language theorem explainer
The directed-edge complex and the loop-plus-isolated-vertex complex share the same census triple: two vertices, one edge, zero tets. Hostile-probe authors cite this to set up the count-vector collision that separates SJ cost 2 from SJ cost 0. The proof is pure definitional equality via three reflexivities.
Claim. Writing $n_V$, $n_E$, $n_T$ for the vertex-, edge-, and tet-count observables on a bounded complex, the one-edge complex and the loop-point complex satisfy $n_V(\mathrm{edge})=n_V(\mathrm{loop\text{-}point})$, $n_E(\mathrm{edge})=n_E(\mathrm{loop\text{-}point})$, and $n_T(\mathrm{edge})=n_T(\mathrm{loop\text{-}point})$.
background
This module is an adversarial probe against the C15 J-diamond rank lattice. It edits nothing in the reviewed source; every failed attack is evidence for the reviewed claim. The first attack class is witness arithmetic on seed diamonds and count vectors.
Census observables extract the triple $(n_V,n_E,n_T)$ from a bounded complex: $n_V$ is the vertex count, $n_E$ the edge count, and $n_T$ the free tet label. The one-edge complex is a single directed edge $0\to 1$. The loop-point complex is one loop at vertex $0$ together with one isolated vertex. Both are declared with the same numeric fields $(2,1,0)$.
The loop-point doc states the intended collision explicitly: its count vector is $(2,1,0)$, the same as the proper edge, yet every posting balances at its own vertex, so it pays nothing. That shared triple is the content of the present theorem.
proof idea
Term-mode proof by a triple of reflexivities. Both complexes hard-code $n_V=2$, $n_E=1$, $n_T=0$ in their structure fields, so each component equality is definitional and closes by rfl. No lemmas are invoked.
why it matters
Inside the hostile-probe checklist this is the count-vector half of the first witness: the pair of complexes that share $(2,1,0)$ but carry SJ costs $2$ versus $0$. Sibling probes then compare those SJ costs and the seed-defect arithmetic; the present fact is the pure census identity they rest on.
In the broader Seven Gaps gravity stack, the J-diamond rank lattice is the combinatorial skeleton behind the C15 gap. Establishing that two geometrically different complexes can be census-indistinguishable while differing in cost is the probe's way of stress-testing whether rank and cost are forced by counts alone. No downstream theorem currently depends on this declaration; it is local evidence inside the 2026-07-30 review package.
Framework landmarks are only indirect: the diamond and its J-unit defects sit downstream of the Recognition Composition Law and the T5 uniqueness of $J$, but this lemma itself is pure finite combinatorics of bounded complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.