kind_rule_fails_by_counting
plain-language theorem explainer
The letter-cost space admits an equivariant, size-blind countermodel to the kind rule that never inspects incidence: the vertex-count charge pairCost. Anyone tracking Gap 2 (whether the substrate forces kind-only letter costs) cites this as the counting-side half of T1. The proof is a three-way constructor packaging the three already-proved properties of that witness.
Claim. The vertex-count letter charge is gauge-equivariant, is not kind-only, and is size-blind on totals: $\mathrm{Equivariant}(\mathrm{pairCost}) \land \lnot\mathrm{KindOnly}(\mathrm{pairCost}) \land \mathrm{CostSizeBlind}(\mathrm{pairCost})$.
background
Gap 2 asks whether the letter-cost layer forces the kind rule: a letter's cost depends only on its kind, with the same three reals at every complex. The prior arc derived the measure from a posted kind-only cost and left open whether the substrate itself forces that clause (incidence_silence_derived := false). Scope is deliberately the letter-cost space, not the dual-entry ledger one layer below.
Two independent countermodels live in that space. The incidence charge bills a fixed real for a proper edge letter and zero otherwise; it is equivariant and not kind-only, and its posted weight is not size-blind. Separately, the vertex-count charge (pairCost) reads only vertex-letter counts: it is equivariant, not kind-only, and size-blind on totals. The module stresses that this is one exhibited witness, not a comparison of countermodel sets; a constant size-function remains kind-only, so "every size charge fails" is false.
The present theorem packages the counting witness. Independence of "reads sizes" versus "reads incidence" is definitional (which fields of the complex a charge inspects), not a theorem here.
proof idea
Term-mode three-way product. The goal is the conjunction of equivariance, failure of kind-only, and cost-size-blindness for the vertex-count charge. Each conjunct is discharged by a sibling lemma already proved in the module: pairCost_equivariant, pairCost_not_kindOnly, and pairCost_costSizeBlind. No further rewriting or case analysis.
why it matters
This is T1's counting half in the Gap 2 third arc: the kind rule fails in the letter-cost space without any incidence data. Downstream, kind_rule_fails_twice conjoins it with the incidence countermodel to record two independent failures. The module's KindRuleIndex flags kind_rule_fails_by_counting := true as part of the settled ledger for the arc.
Together with the incidence failure and the silence theorems (letter cost cannot see dual-entry state; pinning is only a counting normalization), it closes what Lean can settle at this layer: the letter-cost space does not force the kind rule, and exclusion of countermodels, when it happens, lives in the measure formula rather than in canonical-state pinning. The open successor is whether the dual-entry lattice one layer below forces the rule; that is outside this module's scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.