LedgerGeneratedIndex
plain-language theorem explainer
A six-flag boolean record that packages the pre-registered Gap-2 ledger-generation measurement outcomes for the recognition cost jCost. Gravity and quantum-gravity workers cite it as the typed carrier of the C14 fork-gate results (ledger-generated status, history-cost vanishing at caps 1–3, C27 hard-stop arming, and the measure-flag move). As a structure definition it has no proof body; the concrete assignment lives in the companion value ledgerGeneratedIndex.
Claim. A record type with six boolean fields: whether the canonical recognition cost $j$ is ledger-generated; whether history cost vanishes at size caps $1$, $2$, and $3$; whether the C27 hard-stop is armed; and whether the measure flag has been moved. No mathematical claim is asserted by the type itself.
background
Gap 2 (C14) is the LedgerGenerated fork gate in the Seven Gaps gravity program. After A1.7 closed the bulk-cancelling fixed-kind-totals class, the remaining escape class is where a nonzero history cost can still live. The module asks whether the canonical recognition cost $j$ (the J-cost of Recognition Science, forced unique by T5) is ledger-generated in a frozen model sense.
Ledger-generated means: there exist a vertex charge $f_V:\mathbb{Z}\to\mathbb{R}$ and constants $c_E,c_T$ such that every letter is charged only from its own double-entry posting row (vertex imbalance $\mathrm{indeg}-\mathrm{outdeg}$ for vertices; constant charges for edges and top-cells). Forbidden inputs include orbit sums, isomorphism-class data, and any global census beyond the letter's own row. This is an admissibility class (model choice), not a derived theorem.
The enumeration harness and SJ spectra come from C15 (J-diamond rank): 437 classes at cap 4. Kernel decisions at caps 1–3 and the full $j$-cost ledger-generation check are measured against that frozen predicate and tabulated here as booleans.
proof idea
No proof: this is a structure declaration (six Bool fields). It only names the measurement slots. The companion definition ledgerGeneratedIndex supplies the concrete TRUE/FALSE assignment measured by the Gap-2 harness. Downstream code pattern-matches or projects these fields rather than proving anything about the type.
why it matters
This record is the typed interface for the C14 pre-registered TRUE/FALSE measurement that decides the tilt fork for flag 8 (gap2_measure_derived). Its sole direct consumer is ledgerGeneratedIndex, which freezes the measured outcomes: $j$ is ledger-generated, history cost vanishes at cap 1 but not at caps 2 or 3, and the C27 hard-stop is armed.
In the Recognition framework the J-cost is the unique cost forced by T5 and the Recognition Composition Law. Asking whether that cost is ledger-generated (chargeable from local double-entry rows alone) separates local ledger accounting from residual history cost that could tilt the gravity fork. The structure therefore sits on the path from the eight-tick/octave and D=3 forcing chain into the concrete gravity gap closures, without itself asserting any of those physical claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.