C27_trigger_armed_cap3
plain-language theorem explainer
At size cap 3 the C27 trigger is armed for the canonical recognition cost jCost (κ=1): that cost is ledger-generated at the cap, and history cost is not identically zero there. Gap-2 auditors cite this when closing the LedgerGenerated fork gate for flag 8. The proof packs the cap-3 ledger-generated fact with a single directed-edge witness whose history cost equals 1.
Claim. At size cap $3$, the recognition letter cost $c$ given by $jCost$ at Casimir $\kappa=1$ is ledger-generated, and there exist a bound $B$ and a bounded complex $K$ with at most $3$ vertices, edges, and top-cells such that the history cost of $c$ on $K$ is nonzero.
background
Gap 2 (C14) is the LedgerGenerated fork gate for flag 8. A letter cost $c$ is ledger-generated when each letter is charged only from its own double-entry posting row: a vertex gets $f_V$ of its imbalance (indegree minus outdegree), while edges and top-cells get fixed constants. No orbit sums, isomorphism-class data, or global census of $K$ may enter. The module kernel-decides this model predicate on the canonical recognition cost $jCost$.
For $jCost(\kappa)$, a vertex letter is charged $(\mathrm{vertexImbalance})^2/(2\kappa)$; edge and top-cell letters carry zero charge. History cost is the sum of letter charges over a complex. The C27 trigger at a cap is the conjunction of ledger-generation at that cap with existence of some bounded complex inside the cap whose history cost is nonzero.
Upstream, $jCost$ is already ledger-generated for every $\kappa\neq 0$, hence at cap 3; the one-edge complex (two vertices, one directed edge, no top-cells) has history cost $1$ at $\kappa=1$ and fits inside cap 3.
proof idea
Term-mode packing of the two conjuncts of the trigger predicate. The first conjunct is the already-proved fact that $jCost$ at $\kappa=1$ is ledger-generated at cap 3 (restriction of the global ledger-generated theorem). The second conjunct is witnessed by $B=4$ and the one-edge complex: its vertex/edge/top counts are each $\le 3$ by a native decision, and its history cost is nonzero by the cap-2 nonvanishing lemma (history cost equals $1$ on that edge).
why it matters
Arms the C27 hard-stop boolean at cap 3 inside the Gap-2 LedgerGenerated measurement. Downstream, the ledger-generated verdict record and the true index bit for $jCost$ both depend on the cap-1/2/3 decisions; this theorem supplies the cap-3 arm of that package. Together with the matching cap-1 and cap-2 arms it certifies that the canonical recognition cost sits inside the admissibility class frozen before enumeration, while history cost still sees a nonzero edge, so the escape class of A1.7 is not empty at these caps. That is the measured TRUE side of the pre-registered fork that decides the tilt for flag 8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.