module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2KindRule`

Third arc of Gap 2: names the premise ChargesCountsOnly that the posting-cost derivation needs, namely that a letter's charge depends only on the three cell counts and the letter's kind. Establishes countermodels and silence results showing pure kind-only and size-blind rules fail, and records that pairCost is equivariant and size-blind yet not kind-only. Downstream lattice work imports this naming. Argument is a mix of counting lemmas, incidence counterexamples, and equivariance facts.

claimGap 2, third arc: the posting-cost derivation of premise (i) requires that charge is a function of the three cell counts $(n_0,n_1,n_2)$ and letter kind only ("charges count only"). Pure kind-only rules fail by counting and by incidence; $pairCost$ is equivariant under transport and size-blind, yet not kind-only. Letter-cost and history-cost are silent on the dual-entry state space; a countermodel weight separates class-mass from $\mu$.

background

Gap 2 sits in the gravity seven-gaps program. The posting-cost derivation (Gap2PostingCostDerivation) obtains premise (i) of the gluing argument from a labeled weight, but only after assuming size-blindness of that weight. Upstream analysis shows no weaker "blindness to $X$" premise supplies size-blindness unless $X$ resolves at most the three cell counts.

This module works one layer up from the dual-entry signed-source enrichment (Wave B residual R3): letters carry charges on a 4D dual-entry lattice, and costs such as $pairCost$ read vertex or cell data after transport. The named target premise is ChargesCountsOnly: charge of a letter is determined by the triple of cell counts together with the letter's kind.

Sibling facts record what fails without that premise. Kind-only rules are defeated by counting and by incidence. $pairCost$ is transport-equivariant and cost-size-blind, yet not kind-only. Letter-cost and history-cost contribute nothing on the dual-entry state space; pinning is only a counting normalization.

proof idea

Module-level argument, not a single theorem. Equivariance of $pairCost$ under letter transport is stated directly (transport of a vertex letter remains a vertex letter; cost reads the target vertex count), avoiding a dependent cases match that blocks simp. Separate lemmas show $pairCost$ is size-blind but not kind-only. Kind-rule failure is proved two ways: by pure counting of cells, and by incidence configurations. Silence lemmas show letter-cost and history-cost ignore the dual-entry state. A countermodel weight separates class-mass from $\mu$. ChargesCountsOnly is introduced as the interface hypothesis the posting-cost arc actually needs; the module flags that the lattice itself is not yet shown to force it.

why it matters in Recognition Science

Names the exact premise the Gap 2 posting-cost derivation depends on, so later arcs can discharge or refute it rather than re-derive it. Downstream Gap2LatticeKindRule imports this module and answers the open flag lattice_forces_premise := false: whether the dual-entry lattice one layer below LetterCost forces ChargesCountsOnly. Without this naming, the gluing derivation's size-blindness assumption stays an unexplained black box. Ties into the broader QG Wave B residual program (signed-source enrichment, no xRatio) and the seven-gaps gravity stack that feeds Recognition dual-entry structure toward continuum limits. Does not itself close the lattice-forcing question; that is the fourth arc.

scope and limits

Does not prove the dual-entry lattice forces ChargesCountsOnly (left to Gap2LatticeKindRule).
Does not derive premise (i) of gluing; only names the charge hypothesis posting-cost needs.
Does not claim pairCost equals any physical mass or Newtonian potential.
Does not establish uniqueness of the three-count charge among all possible weights.
Does not address continuum or large-scale gravity limits beyond the discrete letter model.

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