LedgerGenerated_implies_at
plain-language theorem explainer
If a letter cost is ledger-generated for every bounded complex, then it is ledger-generated at every finite size cap. Gap-2 auditors cite this when specializing a global certificate (e.g. for the recognition cost) down to the per-cap decision predicates. The proof is pure existential transport: unpack the witnessing vertex charge and edge/top constants, then re-package them under the restricted quantifiers.
Claim. If a letter cost $c$ is ledger-generated, meaning there exist a vertex charge $f_V:\mathbb{Z}\to\mathbb{R}$ and constants $c_E,c_T\in\mathbb{R}$ such that every letter is charged from its own double-entry posting row alone (edges and top-cells carrying constant null-row values), then for every natural number $\mathrm{cap}$ the same witnesses certify that $c$ is ledger-generated on all bounded complexes with vertex, edge, and top-cell counts at most $\mathrm{cap}$.
background
This module freezes the pre-registered model predicate for Gravity Gap 2 / C14: whether the canonical recognition cost is ledger-generated. Per the module doc, 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 on the letter's account), with edge and top-cell letters carrying constant null-row values. Forbidden inputs include orbit sums, isomorphism-class data, and any global census beyond the letter's own row.
The finite restriction asks the same existence only on complexes whose three counts are at most a given cap; that is the per-cap decision the gate measures. Upstream, the recognition cost of a letter charges a vertex by the square of its vertex imbalance over twice the Casimir, and charges edge and top-cell letters zero (they are not posting targets).
proof idea
Term-mode existential transport, no arithmetic. Destructure the global hypothesis into witnesses $f_V$, $c_E$, $c_T$ and the three universal charge equalities (vertices, edges, top-cells). Rebuild the finite-restriction package with those same witnesses, supplying a function of the complex that ignores the three size bounds and returns the unrestricted equalities. The global foralls immediately imply the cap-bounded ones.
why it matters
Direct parent of the three per-cap certificates at caps 1, 2, and 3: each is a one-line application of this lemma to the global recognition-cost certificate. Those caps are the measured TRUE outcomes of the Gap-2 fork gate against the C15 diamond-rank enumeration harness (437 classes at cap 4). Closing the ledger-generated side of the dichotomy supports the tilt-fork decision for flag 8 after A1.7 closed the bulk-cancelling fixed-kind-totals escape class. The gate is a model admissibility class, not a derived theorem; this lemma is the bridge from the global certificate to the finite measurements the harness reports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.