characterCost_kindOnly
plain-language theorem explainer
The three-parameter character letter cost (vertex/edge/tetrahedron charges equal to minus log of three reals) is kind-only: charge depends only on letter kind. Gap-2 countermodel and gluing/posting no-go theorems cite it as the structural half of the best-behaved non-unit-fugacity example. Proof is a four-field term packaging the three log-rates with the kind-rates identity.
Claim. For all real $u,v,w$, the letter cost that assigns $-\log u$ to every vertex letter, $-\log v$ to every edge letter, and $-\log w$ to every tetrahedron letter is kind-only: there exist three real rates such that the cost of a letter equals the rate of its kind alone.
background
Gap 2 asks whether the posting layer plus the carrier gluing law force unit sector fugacity in the path-sum measure. The gluing derivation reduces residual freedom to three positive constants (one fugacity per index type); unit fugacity is the extra normalization that sets those constants to one.
A letter cost is kind-only when its charge on each alphabet letter depends only on which of the three blocks (vertex, edge, tetrahedron) the letter occupies, not on finer labels. The character cost is the cleanest such family: constant charge $-\log u$, $-\log v$, $-\log w$ on the three blocks. Kind-only is the named structural premise that unlocks size-blind posted weight and the fixed-kind-totals package used throughout the posting layer.
Upstream, recognition costs are J-type functionals on ratios (observer forcing, multiplicative recognizers, rung coarsening). Here the cost is combinatorial on letters of a bounded complex, not a continuum J-cost; the link is only that both sit in the same ledger of recognition weights.
proof idea
Term-mode constructor for the KindOnly structure. Supply the three rates $-\log u$, $-\log v$, $-\log w$ as the kind charges, then discharge the defining equality by the sibling lemma that the character cost equals those rates on every letter (the kind-rates identity). No tactics, no case split: one structure value.
why it matters
This is the first conjunct of the packaged Gap-2 countermodel: for every positive triple the character cost is kind-only, gauge-equivariant, has size-blind posted weight equal to the three-constant character size function, and that size function glues everywhere, with fugacity unit iff $u=v=w=1$. The headline theorem then exists a kind-only equivariant cost whose posted weight is size-blind, whose size function satisfies carrier shuffle, and whose sector fugacity is non-unit whenever the triple is not $(1,1,1)$.
Direct consumers include the size-blindness of the posted character weight (one-line via this lemma), the continuum witness used in the hostile-probe module, and the index flag that unit fugacity is not shown underivable from posting+gluing alone. In the Recognition gravity stack this closes the negative half of Gap 2: gluing constrains fugacity shape (it must be a character) but not its value; unit fugacity needs an independent atom-normalization hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.