pairCost_chargesCountsOnly
plain-language theorem explainer
The vertex-count letter charge (pair cost) satisfies the counts-only premise: each letter's charge depends only on the three complex counts and its kind. Gravity and Gap-2 auditors cite it to show the named premise is inhabited by a real charge, not vacuous. The proof exhibits the three count-functions explicitly (nV-1 on vertices, 0 on edges and triangles) and discharges the equalities by simp and rfl.
Claim. The pair cost on letter-cost space is counts-only: there exist functions $f_V,f_E,f_T:\mathbb{N}^3\to\mathbb{R}$ such that for every bound $B$, every bounded complex $K$, and every letter, the charge equals $f_V(n_V,n_E,n_T)$ on vertices, $f_E(n_V,n_E,n_T)$ on edges, and $f_T(n_V,n_E,n_T)$ on triangles (independent of which particular letter of that kind is chosen).
background
Gap 2's third arc asks whether the letter-cost space forces the kind rule (a letter's cost depends only on its kind, with the same three reals at every complex). The residual after the posting-cost derivation is that kind clause; this module settles what Lean can settle inside LetterCost, not one layer below on the dual-entry ledger.
ChargesCountsOnly is the named premise: for each kind there is one function of the three counts $(n_V,n_E,n_T)$ assigning every letter of that kind its charge, the same functions at every complex. It is an authored restriction on letter costs, not forced by the alphabet (index-reading costs are excluded). It is recommended because it is stated purely in counts and kinds, the data needed for size-blind totals, and it excludes both exhibited kind-rule failures while still admitting the count charge.
Pair cost is the vertex-count read as a vertex-letter charge: it is gauge-equivariant, not kind-only, and size-blind at the level of totals. Together with incidence cost, it shows the kind rule fails in letter-cost space by counting as well as by incidence.
proof idea
Term-mode construction of the three existential witnesses in ChargesCountsOnly. Take $f_V(n_V,n_E,n_T)=(n_V:\mathbb{R})-1$, and take $f_E$ and $f_T$ constantly zero. The vertex branch reduces by simp only [pairCost]; the edge and triangle branches are rfl. No external lemmas are required beyond the definition of pair cost.
why it matters
Keeps the named premise honest inside Gap 2 T1: the premise does not claim letters are uncharged; it claims charges read the counts. Pair cost is the exhibited counts-only witness that is equivariant and size-blind yet not kind-only, so the kind rule fails by counting, not only by incidence. The module header stresses scope: this is the letter-cost layer; whether the dual-entry ledger forces the kind rule remains the open successor (incidence_silence_derived := false upstream). No downstream consumers are wired yet; the result stands as a local integrity check that the premise admits the count charge while still excluding the countermodels used against a global kind rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.