chargesCountsOnly_perComplex_kindRates
plain-language theorem explainer
Under the counts-only premise on a letter cost, every letter of one kind inside a fixed complex carries the same real charge. The three kind rates may still depend on that complex's vertex, edge, and triangle counts. Gap-2 analysts cite this as the per-complex consequence of the named premise, distinct from the global kind rule. The proof unpacks the three existential witnesses in the premise and evaluates them at the complex's counts.
Claim. If a letter cost $c$ is counts-only (each kind's charge is given by a single function of the three counts), then for every bound $B$ and every bounded complex $K$ there exist reals $c_V,c_E,c_T$ such that every vertex letter of $K$ is charged $c_V$, every edge letter $c_E$, and every triangle letter $c_T$.
background
Gap 2 asks whether the letter-cost space forces the kind rule: a letter's cost depends only on its kind, via one triple of reals shared by every complex. The residual after the posting-cost derivation is exactly that clause. The present module works strictly inside LetterCost (complex plus alphabet letter, no dual-entry state) and separates what the space forces from what must be assumed.
The named premise ChargesCountsOnly is an authored restriction, not an alphabet consequence: for each kind there is a function of the three counts $(n_V,n_E,n_T)$ that assigns every letter of that kind its charge, the same function at every complex. It excludes index-reading and incidence-reading charges while still admitting count charges such as the vertex-count pair cost (vertex rate $n_V-1$).
Per-complex kind rates are weaker than the global kind rule. The latter is the special case in which the three count functions are constant across all complexes; the former only says that, inside one fixed complex, letters of a kind share one value.
proof idea
Term-mode unpacking. The hypothesis supplies three existential packages, one per kind: a count function $f_V$ (resp. $f_E$, $f_T$) together with a uniformity statement that every letter of that kind equals the function at the complex's counts. Instantiate each function at $(K.nV,K.nE,K.nT)$ to obtain the three reals, then discharge the three universal quantifiers by the corresponding uniformity hypotheses. No further lemmas are required.
why it matters
This is the first positive extraction from the counts-only premise in the Gap-2 third arc. It records that the premise already yields kind-uniform rates inside each complex, while deliberately stopping short of the global kind rule (one fixed triple for all complexes). The module doc stresses that difference: a counts-only charge may still vary its rates with the counts, as the pair cost does with vertex rate $n_V-1$, and the global rule is the constant special case later pinned to zero by atom normalizations.
No downstream theorems currently depend on it (used_by is empty); its role is local scaffolding for the totals-form companion and for the contrast with FixedKindTotals. It does not close the open successor question whether the dual-entry ledger below LetterCost forces the kind rule; the module header explicitly leaves that open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.