index_lattice_question_open
plain-language theorem explainer
The kind-rule status index marks the dual-entry lattice force question as unsettled: it does not claim that the ledger lattice forces the kind-only letter-cost premise. Gap-2 auditors cite this flag to keep letter-cost theorems separate from the deeper lattice layer. The proof is pure reflexivity on the index boolean.
Claim. On the compiled kind-rule status index, the boolean flag ``lattice forces premise'' equals $\mathrm{false}$: it is not asserted that the dual-entry ledger lattice forces the kind-only letter-cost rule.
background
Gap 2 asks whether a letter's cost must depend only on its kind (three shared reals at every complex). The prior posting-cost derivation settled the measure from a posted kind-only cost at the atoms, but left open whether the substrate forces that kind rule, and flagged incidence silence as underived.
This module works strictly in the letter-cost space. A referee required that scope: the ledger dual-entry lattice sits one layer below letter cost, and whether that lattice forces the kind rule is an open successor, not a claim settled here. Countermodels already show the letter-cost space admits equivariant charges that break kind-only behavior (incidence charging; non-constant vertex counts).
The upstream index packages five settled booleans (fails by counting, fails by incidence, exclusion not from pinning, exclusion is the measure formula, premise yields kind totals). The lattice-forces flag is the residual open bit on that same record.
proof idea
Term-mode reflexivity. The index structure is defined with lattice_forces_premise equal to false (explicitly or by default among the recorded fields), so rfl discharges equality to false. No lemmas are applied.
why it matters
Closes the bookkeeping half of Gap 2's third arc: what Lean can settle about kind-rule forcing is recorded as five true flags plus this explicit open on the lattice layer. Downstream readers (none wired yet in the graph) and paper prose can cite the index without conflating letter-cost countermodels with a lattice-forcing claim the framework has not made.
That separation matches the module header's referee correction: letter-cost results do not automatically lift to the dual-entry ledger. The open successor is whether a state-bearing cost on the lattice would force kind-only behavior; this flag keeps that question visible rather than silently assumed. No T0–T8 forcing step is discharged here; the result is local gravity/ledger hygiene inside the Seven Gaps program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.