module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2KindRule`

Names ChargesCountsOnly, the premise Gap 2's posting-cost derivation needs: a letter's charge is a function of the three cell counts and the letter's kind. Supplies countermodels showing kind-only rules fail by counting and by incidence, and that pairCost is size-blind yet not kind-only. Downstream lattice work cites this as Gap 2's third arc. The argument is a cluster of equivariance lemmas and explicit countermodels, not a single uniqueness proof.

claimIsolates the predicate that a charge assignment $q$ on letters depends only on the three cell counts $(n_0,n_1,n_2)$ and the letter kind (ChargesCountsOnly), and exhibits countermodels showing that kind-only and size-blind weight rules are strictly weaker than this premise for the dual-entry posting cost $\mathrm{pairCost}$.

background

Gap 2 in the gravity seven-gaps program asks which premises make the gluing and posting-cost derivation go through. Upstream, Gap2PostingCostDerivation derives premise (i) from a posting cost and shows size-blindness of the labeled weight is not interchangeable with weaker blindness conditions: blindness to $X$ forces size-blindness for every weight exactly when $X$ resolves no more than the three counts.

The dual-entry enrichment setting (RecognitionDualEntryEnrichment4D) supplies the signed-source lattice on which letters and pairCost live. A letter carries a kind and sits on a complex whose three cell counts are the natural size data. pairCost is the dual-entry cost read at a transported letter; its vertex charge at a transported vertex letter equals the target's vertex count.

This module is the third arc: it names ChargesCountsOnly as the exact premise the posting-cost derivation needs, and separates it from weaker kind-only or silent-on-state-space alternatives.

proof idea

A cluster of lemmas and countermodels, not one theorem. Defines ChargesCountsOnly (charge is a function of the three counts and kind). Equivariance of pairCost under transport is stated directly for vertex letters so simp closes without a dependent match. Countermodels include pairCost_not_kindOnly, kind_rule_fails_by_counting, kind_rule_fails_by_incidence, and countermodel_weight_classMass_ne_mu. Separate lemmas show letter_cost and history_cost are silent on the state space, and that pinning is only a counting normalization. Net effect: pin ChargesCountsOnly as necessary rather than optional.

why it matters in Recognition Science

Feeds Gap2LatticeKindRule, the fourth arc, which asks whether the dual-entry lattice itself forces ChargesCountsOnly. Downstream doc: the third arc named the premise the posting-cost derivation needs (ChargesCountsOnly) and left open whether the lattice forces it, flagged lattice_forces_premise := false. Without this naming and the countermodels ruling out kind-only shortcuts, the lattice forcing question would be ill-posed. Sits in the Gravity domain, supporting the Gap 2 path toward the posting-cost derivation of gluing premise (i).

scope and limits

Does not prove the dual-entry lattice forces ChargesCountsOnly (deferred to Gap2LatticeKindRule).
Does not derive the full Gap 2 gluing theorem; only isolates its charge premise.
Does not claim pairCost is the unique cost satisfying the premise.
Does not address residual R3 enrichment beyond the imported dual-entry setting.
Does not equate size-blindness with ChargesCountsOnly; countermodels separate them.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2LatticeKindRule module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation module_import

declarations in this module (24)

theorem pairCost_equivariant L103
def oneVertex L120
theorem pairCost_not_kindOnly L135
theorem pairCost_costSizeBlind L157
theorem kind_rule_fails_by_counting L171
theorem kind_rule_fails_by_incidence L178
theorem letter_cost_is_silent_on_the_state_space L196
theorem history_cost_is_silent_on_the_state_space L204
theorem countermodel_weight_classMass_ne_mu L216
def pinning_is_a_counting_normalization L227
def ChargesCountsOnly L241
theorem does L253
theorem chargesCountsOnly_perComplex_kindRates L254
theorem chargesCountsOnly_kindTotals_perComplex L271
def indexCost L291
theorem indexCost_inl L296
theorem indexCost_not_chargesCountsOnly L301
theorem chargesCountsOnly_excludes_incidence L324
theorem pairCost_chargesCountsOnly L350
theorem kindOnly_of_constant_rates L367
structure KindRuleIndex L380
def kindRuleIndex L403
theorem index_kind_rule_not_forced L413
theorem index_lattice_question_open L415