KindRuleIndex
plain-language theorem explainer
Navigation index of eight boolean status flags for Gap 2's kind-rule analysis in the letter-cost space. It records which claims are settled (failures by counting and incidence, exclusion via the measure formula, premise consequences) and which two are deliberately false or open (kind rule forced; lattice forces premise). Downstream code instantiates the concrete flag vector. Pure record type: no proof content.
Claim. A record type with eight boolean fields summarizing the kind-rule status in the letter-cost layer: the kind rule fails by counting alone and by incidence; exclusion of countermodels is not from canonical pinning but from the gauge-divisor measure formula; the named counts-only premise yields per-complex kind totals and discriminates countermodels; the kind rule is not forced in letter-cost space; whether the dual-entry lattice forces the premise remains open.
background
Gap 2 asks whether a letter's recognition cost depends only on its kind (vertex, edge, or triangle), 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 forces that kind clause. This module works strictly in the letter-cost space: a cost assigns a real to each alphabet letter of a bounded complex, with no dual-entry state in scope.
Two independent countermodels break kind-only charging: a vertex-count charge (pair cost) that is equivariant and size-blind at totals, and an incidence charge that prices proper edges only. The named premise (charges depend only on the three counts and the letter's kind) excludes both while admitting count charges and yielding per-complex kind rates. Letter cost is silent on the dual-entry state space, so canonical history pinning cannot be what excludes countermodels; exclusion lives in the gauge-divisor mass formula.
The module header stresses the scope: whether the ledger's dual-entry lattice one layer below forces the premise is the open successor, not settled here.
proof idea
No proof: this is a structure declaration. Each field is a bare Bool carrying a field docstring that states the corresponding claim or non-claim. Instantiation happens downstream by assigning concrete true/false values; the structure itself only fixes the flag schema.
why it matters
Closes the navigation layer of Gap 2's third arc: after theorems exhibit countermodels, silence of letter cost on state space, and the role of the named premise, this index packages the settled versus open status so a reader (or downstream Lean) can see the scoreboard at a glance. The sole consumer is the concrete instance that sets counting and incidence failures, measure-formula exclusion, and premise consequences to true, and sets kind-rule-forced and lattice-forces-premise to false.
In the Recognition gravity program this sits after posting-cost derivation of the measure from kind-only costs. It does not touch the forcing chain T0–T8, RCL, or the phi ladder directly; it polices a residual hypothesis about kind rates so the gravity measure arc does not overclaim what the letter-cost alphabet forces. The open flag on lattice forcing is the explicit handoff to dual-entry structure below.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.