KindOnly
plain-language theorem explainer
A letter cost is kind-only when three fixed reals charge every vertex, edge, and triangle letter the same way at every complex and size cap. Gap-2 posting-cost arguments cite this as the structural premise that makes history cost linear in the three cell counts. The declaration is a pure existence wrapper around KindRates; no proof content beyond that Prop.
Claim. A letter cost $c$ is kind-only if there exist three real rates $c_V,c_E,c_T$ such that, at every size cap and every bounded complex, $c$ assigns to each posting-alphabet letter a value depending only on whether the letter is a vertex, edge, or triangle letter, with those three fixed rates.
background
Gap 2 asks how premise (i) (size-blindness of the labeled weight in a form strong enough for the gluing derivation) can arise. The sibling module Gap2SizeBlindnessReach shows that indistinguishability premises weaker than the three counts cannot force it. This module attacks the same premise from a different layer: a posting cost on the alphabet rather than a blindness condition on weights.
A LetterCost is a real assigned to each letter of the posting alphabet Fin nV ⊕ Fin nE ⊕ Fin nT at every bounded complex and size cap. The history cost is the sum of those letter costs (ledger additivity over postings). The posted weight is the Boltzmann factor of that cost over the gauge volume nV! nE! nT!. Kind-only is the condition that the letter cost factors through the three blocks with three global rates, independent of which complex or cap is in view.
The module is explicit that "the substrate posts one letter per cell" and that the exponential map are modeling choices, not derived facts. Kind-only is a condition on the cost function itself, which is why it sits outside the size-blindness dichotomy.
proof idea
Pure definition: KindOnly c is the proposition that there exist three reals cV, cE, cT witnessing KindRates c cV cE cT. No tactics, no lemmas applied. Downstream proofs discharge it by exhibiting the three rates (e.g. -log u, -log v, -log w for a character cost).
why it matters
This is the structural premise of the posting-cost route to Gap 2 premise (i). Downstream, characterCost_kindOnly shows every character cost is kind-only; characterCost_countermodel and gluing_and_posting_do_not_force_unit_fugacity package kind-only + equivariance + size-blind posted weight into countermodels with non-unit sector fugacity. widening_blocked_without_naming_mu uses the same package to prove that elimination cannot drop the hypothesis that names mu at the atoms. kind_rule_fails_twice in the incidence-silence verdict also consumes it.
Together these feed the fugacity-posting-gluing verdict: unit sector fugacity is equivalent to posting mu at the atoms, and the structural posting conditions plus gluing do not force that unit. Kind-only is therefore the hinge that lets the module both derive premise (i) from a cost and exhibit the obstruction that keeps fugacity free without naming mu.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.