does
plain-language theorem explainer
At the letter-cost layer of Gap 2, the kind-only charging rule is not forced: well-formed equivariant costs can read incidence or vertex counts and still break kind-only posting. Gravity residual auditors after the posting-cost derivation cite this negative answer. The claim is the module headline assembled from explicit countermodels and type-level silence facts, not a ledger-level forcing theorem.
Claim. In the letter-cost space, the kind rule fails: there exist gauge-equivariant letter costs that are not functions of kind alone (with the same three reals at every complex). Neither incidence-blindness of the cost type nor canonical history pinning supplies that missing case; the residual kind clause is therefore not discharged at this layer.
background
Gap 2 left a residual after posting-cost derivation: the kind clause, that a letter's cost depends only on its kind, with one triple of reals reused at every complex. The prior module derived a kind-only posted measure from atoms without a gluing premise, and set incidence-silence as underived. This module asks only whether the letter-cost space forces that clause.
A LetterCost assigns a real to a complex and an alphabet letter. It does not see dual-entry ledger state. incidenceCost charges a proper edge letter by a parameter $t$ and charges nothing elsewhere; it is equivariant, not kind-only, and its posted weight is not size-blind. pairCost reads vertex count as a vertex-letter charge: equivariant, not kind-only, yet size-blind on totals. So both incidence-aware and counts-only witnesses break the kind rule inside the same type.
Upstream, posting-cost derivation already closed the escape that incidence cost fails gauge invariance (it does not). Class-pushforward and continuum-measure residual results separate weight normalizations from inequivalent-class sums. The dynamics kind-rule structure records what the dynamical layer still does not constrain. Scope is deliberately above the dual-entry lattice: whether that lattice forces the rule is the open successor.
proof idea
Empty extracted body; the mathematical content is the module's packaged negative answer, carried by named sibling witnesses rather than a fresh calculation.
Main steps in the arc: (1) exhibit incidenceCost as an equivariant, not-kind-only letter cost whose posting is not size-blind, so incidence alone kills the kind clause; (2) exhibit pairCost as an equivariant counts-only charge that is also not kind-only, so failure is not incidence-only; (3) record by definitional projection that letter cost (and the history cost at this layer) is silent on dual-entry state, so canonical history pinning cannot exclude those countermodels inside the present LetterCost type; (4) treat pinning as a counting normalization, not a kind-rule enforcer. Upstream Gap2PostingCostDerivation supplies that incidence remains gauge-legal; the dynamics kind-rule structure marks the unconstrained residue.
why it matters
Closes, at the only layer currently statable in Lean, the referee question left open by Gap 2 posting-cost derivation: does the letter-cost space force the kind rule? The answer is no, as three theorem-shaped parts (countermodels by incidence, countermodels by counting, silence of cost on state), not as interpretive gloss.
That keeps the Seven Gaps gravity residual honest: measure formulas and atom-normalized kind-only postings do not get to pretend the kind clause was forced by LetterCost. Parent consumers in the gap stack and any downstream argument that assumed kind-only costs must either add an extra axiom or move to a state-bearing cost carrier.
Framework contact is local to the gravity gap chain rather than T5–T8 forcing. The dual-entry ledger one layer below remains the open successor; this declaration explicitly refuses to answer that stronger question. Broad used_by edges on the short name are name-collision prone and should not be read as a dependency from action convexity or chemistry without module-qualified checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.