probe_not_function_of_counts
plain-language theorem explainer
Two complexes share the census count vector (2,1,0) yet carry unequal history costs under unit J-cost. Gravity auditors cite this as a concrete witness that J is not a function of vertex, edge, and tet counts alone. The proof is a one-line specialization of the parent non-functionality theorem at kappa = 1.
Claim. The proper-edge complex and the loop-with-isolated-vertex complex satisfy $n_V = n_V'$, $n_E = n_E'$, and $n_T = n_T'$, yet their history costs under $J$-cost at $\kappa = 1$ with horizon $4$ are unequal.
background
Census observables on a bounded complex extract three real counts: vertices $n_V$, edges $n_E$, and free tet labels $n_T$. The history cost of a complex is the accumulated $J$-cost along a finite posting horizon; here the horizon is fixed at 4 and the cost kernel is $J$ at Casimir $\kappa = 1$.
Two hardcoded complexes realize the same count vector $(2,1,0)$: the proper edge (pays $1/\kappa$) and a single loop at one vertex plus an isolated vertex (every posting balances locally, so the cost is zero). The parent result already records that this pair separates cost from counts for any nonzero $\kappa$.
This module is an adversarial probe against the C15 J-diamond rank lattice. It edits nothing in the reviewed file; each failed attack is retained as positive evidence for the reviewed claim.
proof idea
One-line term wrapper. Instantiate the parent theorem jCost_not_a_function_of_counts at $\kappa = 1$, discharging $\kappa \neq 0$ by norm_num. No new arithmetic is performed here; the equalities of counts and the inequality of history costs are inherited verbatim from the parent.
why it matters
Closes the unit-Casimir instance of the count-vector conflict inside the hostile probe suite for Gap 2 (J-diamond rank). The parent doc states the lattice conflict precedes any gluing diamond: the same $(2,1,0)$ vector is carried by a paying edge and a free loop-point pair. Specializing at $\kappa = 1$ locks the witness to the concrete seed arithmetic used elsewhere in the probe (SJ costs 2 vs 0 on that vector).
No downstream consumers are wired yet; the declaration stands as review evidence rather than a production lemma. It supports the broader claim that $J$ cannot be reconstructed from census counts alone, which is a prerequisite for treating diamond rank as a genuine cost-lattice obstruction rather than a counting artifact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.