C27TriggerAt
plain-language theorem explainer
The C27 trigger at a size cap holds for a letter cost when that cost is ledger-generated up to the cap and the history cost is not identically zero on complexes fitting the cap. Gap-2 gravity auditors cite it as the armed-gate predicate for the LedgerGenerated fork (C14 / flag 8). It is a pure definitional conjunction of the finite ledger-generation restriction with an existential nonzero-history witness.
Claim. For a natural number size bound $N$ and a letter cost $c$, the C27 trigger holds at $N$ when $c$ is ledger-generated at cap $N$, and there exist a bound $B$ and a bounded complex $K$ (of ambient size at most $B$) whose vertex, edge, and top-cell counts are each at most $N$, such that the history cost of $c$ on $(B,K)$ is nonzero.
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, then measures finite restrictions against the C15 enumeration harness.
Ledger-generated (the model admissibility class) 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 from its own double-entry posting row alone. A vertex letter pays $f_V$ of its imbalance (indegree minus outdegree); edge and top-cell letters have empty rows, so they pay constants. Forbidden inputs include orbit sums, isomorphism-class data, and any global census beyond the letter's own row.
The finite restriction at cap $N$ only demands the ledger identity on complexes whose vertex, edge, and top-cell counts are $\le N$. History cost is the residual imbalance-squared posting cost (at $\kappa=1$, half the squared imbalance); the trigger asks that this residual not vanish on every complex inside the cap.
proof idea
Definitional expansion, not a proved theorem. The predicate is the conjunction of two clauses: (i) the finite ledger-generation restriction of $c$ at the given cap, and (ii) an existential witness: some ambient bound $B$ and bounded complex $K$ with $n_V,n_E,n_T\le$ cap on which the history cost of $c$ is nonzero. No tactics or lemmas fire at the definition site; downstream arming theorems supply the concrete witnesses.
why it matters
This is the C27 armed-gate shape for the C14 LedgerGenerated fork. Downstream, the cap-2 and cap-3 arming theorems instantiate it at the unit recognition cost by pairing the finite ledger-generation decisions with an explicit edge-complex witness whose history cost is nonzero. The hostile-probe module re-exports the cap-2 arming as a shape check. The fork verdict structure packages the global ledger-generation claim for nonzero $\kappa$ together with the cap-1/2/3 finite decisions; the trigger sits one layer below that verdict as the "not identically zero history" half of the escape-class test.
In the broader Recognition stack this is measurement infrastructure for Gap 2, not a forcing-chain landmark (T5–T8). It freezes what "ledger-generated plus live history residual" means before enumeration, so the TRUE/FALSE outcome on the recognition cost is a pre-registered observation rather than a post-hoc fit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.