ledgerGeneratedIndex
plain-language theorem explainer
Frozen six-bit measurement index for the Gap-2 ledger-generated fork gate. It records that the recognition cost jCost is ledger-generated, that history cost vanishes only at size cap 1 (not 2 or 3), that the C27 hard-stop is armed, and that the measure flag is unmoved. Downstream reflexivity theorems and the hostile probe cite these bits. The body is a pure structure instance with six pre-registered booleans.
Claim. The ledger-generated measurement index is the record whose fields are: $jCost$ is ledger-generated ($\mathsf{true}$); history cost vanishes at size caps $1,2,3$ with values $\mathsf{true},\mathsf{false},\mathsf{false}$; the C27 hard-stop is armed ($\mathsf{true}$); the measure flag has not moved ($\mathsf{false}$).
background
Gap 2 (C14) is the ledger-generated fork gate for flag 8 (gap2_measure_derived). After A1.7 closed the bulk-cancelling fixed-kind-totals class, the remaining escape class is where a nonzero history cost can still live. This module asks whether the canonical recognition cost $jCost$ is ledger-generated under a pre-registered model predicate.
A letter cost $c$ is ledger-generated when there exist a vertex charge $f_V:\mathbb{Z}\to\mathbb{R}$ and constants $c_E,c_T$ such that every letter is charged from its own posting row alone: a vertex letter $v$ gets $f_V(\mathrm{indeg}-\mathrm{outdeg})$, every edge letter gets $c_E$, every top-cell letter gets $c_T$. Forbidden inputs include orbit sums, isomorphism-class data, and any global census beyond the letter's own row.
The structure LedgerGeneratedIndex packages the six boolean outcomes of that pre-registered measurement (and the related history-zero and hard-stop flags) into a single frozen record.
proof idea
Definitional structure instance, not a proof. Each of the six fields of LedgerGeneratedIndex is assigned a concrete boolean literal matching the pre-registered Gap-2 measurement table: $jCost$ ledger-generated true; history-zero only at cap 1; C27 hard-stop armed; measure flag unmoved. No lemmas are applied.
why it matters
This index is the single source of truth for the Gap-2 ledger-generated measurement bits. Downstream one-line theorems index_c27_armed, index_flag_unmoved, and index_jCost_true expose the three most-cited fields by reflexivity, and the hostile probe probe_flag_unmoved re-exports the unmoved-flag bit. Together they lock the tilt-fork decision for flag 8 and arm the C27 hard-stop path in the Seven Gaps gravity stack. The definition itself does not derive the physics; it freezes the measured outcomes so later forcing and gluing arguments can cite them without reopening the enumeration harness (C15 J-diamond rank spectra).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.