kindRuleIndex
plain-language theorem explainer
Status index for Gap 2's kind-rule arc: letter-cost space admits equivariant failures of the kind-only clause both by counting and by incidence; countermodel exclusion is from the gauge-divisor measure formula, not dual-entry pinning; the kind rule is not forced here, and whether the dual-entry lattice forces the premise stays open. Downstream projections cite the two false flags. Pure structure inhabitant with boolean literals.
Claim. The kind-rule status index is the record with: counting failure true, incidence failure true, exclusion-not-from-pinning true, exclusion-is-measure-formula true, premise-yields-kind-totals true, premise-discriminates true, kind-rule-forced false, and lattice-forces-premise false.
background
Gap 2 asks whether a letter's cost must be a function of its kind alone, with the same three reals at every complex. The prior posting-cost derivation produced the measure from a posted kind-only cost normalized at the atoms, but left open whether the substrate forces that kind clause. This module works strictly in the letter-cost layer (a cost takes a complex and an alphabet letter, not a dual-entry state).
Two independent countermodels break kind-only charging while remaining gauge-equivariant: pairCost (vertex count as a vertex-letter charge; size-blind at totals) and incidenceCost t (charges $t$ on proper edge letters only; not size-blind). The structure KindRuleIndex packages the module's settled boolean verdicts so later theorems can project them by rfl rather than restate prose.
Upstream, kind_rule_fails_by_counting exhibits the counting witness and kind_rule_fails_by_incidence restates the incidence witness; both feed the true flags here. The cost type is silent on the dual-entry state space, so canonical-history pinning cannot be what excludes the countermodel weight.
proof idea
Definitional structure construction, not a tactic proof. Each field of KindRuleIndex is assigned a boolean literal matching the module's settled theorems and open questions: the two failure flags true (backed by the counting and incidence theorems), exclusion-not-from-pinning and exclusion-is-measure-formula true, premise flags true, and both kind_rule_forced and lattice_forces_premise false. No lemmas are applied at the definition site; the booleans are the index itself.
why it matters
Closes the bookkeeping for Gap 2's third arc inside the letter-cost space: the kind rule is exhibited to fail, exclusion is located in the gauge-divisor formula (class mass $\exp(-2t)/|\mathrm{Aut}|$, not $1/|\mathrm{Aut}|$), and the forced/open status is recorded explicitly. Downstream, index_kind_rule_not_forced and index_lattice_question_open are one-line rfl projections of the two false flags, giving stable citation points that the kind rule is not forced at this layer and that whether the dual-entry lattice forces the named premise remains the open successor.
Scope discipline matters for the gravity stack: an earlier framing asked whether the ledger forces the rule; the module header restricts to letter-cost space precisely because the lattice question is one layer below and is intentionally left open. This index is the machine-readable summary of that split verdict.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.