C27_trigger_armed_cap2
plain-language theorem explainer
At size cap 2, the canonical recognition letter cost jCost(1) is ledger-generated and its history cost is not identically zero. Gravity auditors cite this to arm the C27 trigger that feeds the Gap-2 ledger-generated fork gate. The proof is a two-field pair: the cap-2 ledger-generation theorem plus the single directed edge as a concrete nonzero-history witness.
Claim. The C27 trigger holds at cap $2$ for the recognition letter cost $c = \mathrm{jCost}(1)$: $c$ is ledger-generated at cap $2$, and there exist a bound $B$ and a bounded complex $K$ with $n_V(K), n_E(K), n_T(K) \le 2$ such that the history cost of $c$ on $K$ is nonzero.
background
Gap 2 / C14 freezes a pre-registered TRUE/FALSE gate that decides the tilt fork for flag 8. A letter cost $c$ is ledger-generated when each letter is charged only from its own double-entry posting row: vertices by a function of imbalance $\mathrm{indeg}-\mathrm{outdeg}$, edges and top-cells by constants. Global census data and orbit sums are forbidden inputs.
The recognition cost $\mathrm{jCost}(\kappa)$ charges a vertex by $(\mathrm{vertexImbalance})^2/(2\kappa)$ and charges edges and top-cells zero. History cost aggregates that letter cost over a bounded complex. The C27 trigger at a cap is the conjunction of ledger-generation at that cap with existence of some complex inside the cap whose history cost is nonzero.
Upstream, $\mathrm{jCost}$ is already ledger-generated for every $\kappa\ne 0$, hence at every finite cap; the proper edge complex (one directed edge $0\to 1$) sits inside cap 2 and has history cost $1$ under $\mathrm{jCost}(1)$.
proof idea
Term-mode pair construction for the C27 conjunction. The first conjunct is jCost_ledgerGenerated_cap2, itself the restriction of the global ledger-generation theorem for $\mathrm{jCost}(1)$ to cap 2. The second conjunct is witnessed by $B=4$ and the one-edge complex: the three size inequalities come from edgeComplex_fits_cap2 (native decide), and nonvanishing history cost is historyCost_not_identically_zero_cap2 (rewrite to the edge identity, then norm_num).
why it matters
Arms the C27 trigger at cap 2 inside the Gap-2 ledger-generated fork gate. Downstream, ledgerGeneratedVerdict packages the cap-1/2/3 decisions and the global ledger-generation fact; index_jCost_true records the measured TRUE bit for $\mathrm{jCost}$; the hostile probe probe_C27_shape_cap2 re-exports this theorem as a shape check. Together with the matching cap-1 and cap-3 arms, this closes the finite-cap side of the pre-registered measurement that A1.7 left open: whether nonzero history cost can still live inside the ledger-generated escape class. It is a gravity-side decision step, not a T0–T8 forcing landmark, but it certifies that the canonical $J$-cost remains ledger-local while still seeing imbalance on the simplest edge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.