LedgerGeneratedAt
plain-language theorem explainer
Finite-cap restriction of the ledger-generated admissibility class for letter costs: vertex charges may depend only on each vertex's own imbalance (indegree minus outdegree), while edge and top-cell charges are fixed constants, required only on complexes with all three counts at most the cap. The Gap 2 / C14 fork gate and the C27 trigger cite this as the per-cap decision predicate. Pure definitional Prop (existential over a vertex charge and two constants).
Claim. A letter cost $c$ is ledger-generated at cap $N$ when 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 bounded complex $K$ with $n_V(K),n_E(K),n_T(K)\le N$, each vertex letter is charged $f_V(\mathrm{imbalance}(v))$, every edge letter is charged $c_E$, and every top-cell letter is charged $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 is ledger-generated in a frozen model sense.
The unrestricted predicate says a letter cost is ledger-generated when each letter's charge is a fixed function of that letter's own double-entry posting row (debits minus credits), with edge and top-cell letters carrying constant null-row values. Forbidden inputs: orbit sums, isomorphism-class data, and any global census beyond the letter's own row. Vertex imbalance is exactly indegree minus outdegree on that account.
The present definition is the finite restriction of that model to complexes whose three census counts (vertices, edges, top-cells) are at most a given cap. The enumeration harness and SJ spectra come from the C15 diamond-rank census (437 classes at cap 4).
proof idea
Definitional Prop, not a proved theorem. The body is an existential over a vertex charge map $f_V:\mathbb{Z}\to\mathbb{R}$ and two real constants $c_E,c_T$, followed by a universal quantifier over size bounds $B$ and bounded complexes $K$, restricted by the three inequalities $n_V,n_E,n_T\le\mathrm{cap}$. Under those bounds the cost must match $f_V$ on vertex letters and the two constants on edge and top-cell letters. No tactics or lemmas; the shape is the unrestricted ledger-generated predicate with the cap guards inserted.
why it matters
This is the per-cap decision the C14 gate actually asks for. Downstream, the implication from the unrestricted predicate yields the three kernel decisions that $j$-cost (at $\kappa=1$) is ledger-generated at caps 1, 2, and 3. Those feed the C27 trigger predicate (ledger-generated at the cap, and history cost not identically zero there) and the negative arming result that cap-1 seeds alone do not arm C27 (ledger-generated with vanishing history on the empty, point, and loop-1 complexes).
In the Recognition gravity stack this freezes the admissibility class against which history-cost spectra are measured, separating model choice from the measured TRUE/FALSE outcomes at small caps. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is infrastructure for the Gap 2 ledger fork inside the seven-gaps gravity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.