LedgerGenerated
plain-language theorem explainer
A letter cost is ledger-generated when each vertex charge depends only on that vertex's own imbalance (indegree minus outdegree), while edges and top-cells carry fixed null-row constants. Gap-2 / C14 workers cite this as the pre-registered admissibility class for the tilt-fork gate on flag 8. It is a pure existential Prop (model choice), not a derived theorem: no orbit sums, isomorphism-class data, or global census may enter the charge.
Claim. A letter cost $c$ is ledger-generated if there exist a vertex charge $f_V:\mathbb{Z}\to\mathbb{R}$ and constants $c_E,c_T\in\mathbb{R}$ such that, for every size bound $B$, every bounded complex $K$, and every letter of $K$: each vertex $v$ is charged $f_V(\mathrm{imbalance}_K(v))$ with $\mathrm{imbalance}_K(v)=\mathrm{indeg}_K(v)-\mathrm{outdeg}_K(v)$; every edge is charged the constant $c_E$; every top-cell is charged the constant $c_T$.
background
Gap 2 / C14 is the LedgerGenerated fork gate: a pre-registered TRUE/FALSE measurement that decides the tilt fork 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 (the J-cost letter charge at Casimir $\kappa$) sits inside a frozen admissibility class.
A letter cost assigns a real charge to every letter of a bounded complex $K$ (vertices, edges, top-cells). The imbalance of a vertex is its double-entry posting row: indegree minus outdegree. Edge and top-cell letters are not accounts; their posting row is empty, so any ledger-style charge on them must be a constant (the null-row value).
The definition is a MODEL choice: the gate's admissibility class, not a derived theorem. Forbidden inputs are orbit sums, isomorphism-class data, and any global census of $K$ beyond the letter's own row. Finite restrictions to complexes with counts at most a cap supply the per-cap decisions the gate asks for; the C15 enumeration harness (437 classes at cap 4) is the measurement substrate.
proof idea
Pure definition: the body is an existential Prop. A letter cost $c$ satisfies the predicate when witnesses $f_V:\mathbb{Z}\to\mathbb{R}$ and constants $c_E,c_T$ exist such that three universal equalities hold for every size bound $B$ and every bounded complex $K$: vertex letters equal $f_V$ of their imbalance; edge letters equal $c_E$; top-cell letters equal $c_T$. No tactics, no lemmas, no reduction.
why it matters
This is the frozen C14 predicate against which the kernel decides the tilt fork. Downstream, jCost_ledgerGenerated certifies that the canonical recognition cost at any nonzero Casimir is ledger-generated, with vertex charge $m\mapsto m^2/(2\kappa)$ and null-row values zero. The finite restrictions at caps 1--3 and the implication from the global predicate to each cap feed LedgerGeneratedVerdict, the C14 fork verdict structure.
The predicate also discriminates: censusVertexCost_not_ledgerGenerated shows a global-census charge fails it (point vs two-point dust both have imbalance zero yet charge 1 and 2). Cap-1 seed facts (C27_not_armed_by_cap1_seeds) and hostile-probe modules use the same class to keep decoys out. In the Recognition gravity stack this closes the model side of Gap 2 before history-cost spectra on the J-diamond rank classes are read as measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.