ChargesCountsOnly
plain-language theorem explainer
A letter-cost is counts-only when each alphabet kind (vertex, edge, triangle) is charged by a single real-valued function of the three complex counts (nV, nE, nT), identical for every letter of that kind at every complex. Gravity Gap-2 authors cite it as the named premise that yields per-complex kind rates and excludes incidence-reading charges, without forcing the global fixed-kind rule. The body is a three-conjunct Prop of existentially quantified count functions.
Claim. A letter-cost $c$ is counts-only if 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 of each kind, the charge equals the corresponding function of $(n_V(K), n_E(K), n_T(K))$: vertices get $f_V$, edges $f_E$, triangles $f_T$.
background
Gap 2 asks whether the letter-cost space forces the kind rule: a letter's cost depends only on its kind, via three fixed reals shared by every complex. The prior arc derived a posted kind-only measure from atom normalizations but left open whether the substrate forces the kind clause (incidence_silence_derived := false). This module works strictly at the LetterCost layer (complex plus alphabet letter, no dual-entry state).
A LetterCost assigns a real charge to each letter of the posting alphabet of a bounded complex $K$, whose size data are the three counts $n_V$, $n_E$, $n_T$. The alphabet indexes letters, so index-reading costs are well-formed; incidence-reading costs (charge $t$ on proper edges, zero elsewhere) are equivariant yet not kind-only. The counts-only premise is an authored restriction: charge may depend on kind and the three counts, nothing else the alphabet carries.
The module doc stresses scope: whether the ledger's dual-entry lattice one layer below forces the rule is a successor question, not settled here.
proof idea
Definitional Prop, not a proved theorem. Three conjuncts, one per kind. Each asserts an existential count-function $f : \mathbb{N}^3 \to \mathbb{R}$ such that every letter of that kind, at every complex, receives $f(n_V,n_E,n_T)$. Vertex letters are the left summand; edges and triangles are nested right summands. No tactics or lemmas: the body is the predicate used by later exclusion and totals theorems.
why it matters
This is the named premise of the Gap-2 third arc. Downstream, chargesCountsOnly_kindTotals_perComplex shows it yields per-complex kind rates (block sum equals rate times count), which is weaker than FixedKindTotals (three global reals). chargesCountsOnly_excludes_incidence shows it rules out incidenceCost: a loop and a proper edge at sizes $(2,2,0)$ cannot share one edge-count function when charges are $0$ and $t \neq 0$. It does not rule out pairCost, which is counts-only with vertex rate $n_V-1$.
The three-layer no-go ledger_forces_countsOnly_at_no_layer (and the verdict certificate) packages $\neg$ counts-only for incidence cost, for the lattice-induced cost, and a non-counts-only schedule from dynamics. So the premise is recommended because it is statable in counts and kinds and excludes exhibited failures, yet the letter-cost space, lattice, and posting dynamics do not force it. The live residual is a physical schedule law (CountsOnlySchedule), not a forced ledger identity. No direct T0–T8 landmark; this is gravity Gap-2 scaffolding around kind-clause forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.