secondAttackBlock
plain-language theorem explainer
Labels the second historical attack block on the residual Gap-2 selector after the R18 rebooking wall: three census rows (action-first ledger cost, U12, U13). Anyone tracking the necessary-reasons census for the gauge-counting principle cites it as the post-R18 plan. It is a literal three-string list; length is discharged by decide.
Claim. The second attack block is the ordered list of three census labels: action-first ledger-cost derivation, child row U12 (derive the gluing law), and child row U13 (justified asymmetry). All three were later resolved in the unit-fugacity selector census.
background
Gap-2 asks whether richer RecognitionLedger and posting-layer structure forces the gauge-counting principle for physical class mass (equivalently $\nu = 1/|\mathrm{Aut}|$). The module runs a necessary-reasons census: each candidate reason is theorem, open, model, or refuted.
R18 is the surviving selector target after many refutations. The R18 block shows that fugacity–action rebooking $(a,S)\mapsto(t\cdot a, S+\log t)$ preserves the Boltzmann product, and every product-visible prior is rebooking-invariant, so none forces unit fugacity $a\equiv 1$. The only priors outside that wall pin the action independently of the measure.
Upstream cost definitions (J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen total cost) supply the ledger-cost language the action-first residual needs. The module doc records the residual obligation as: derive the ledger cost the substrate posts, with fugacity booking then conventional and GCP given by the gauge-orbit-mass equivalence.
proof idea
Pure definition: a three-element string list literal. No tactics, no lemmas. The companion length theorem is a one-line decide on that literal.
why it matters
Closes the historical bookkeeping after R18 was scored REFUTED over rebooking-invariant priors. Downstream R18Status records that verdict; secondAttackBlock_length pins the block size at three. The doc-comment states the child census UnitFugacitySelector resolved all three rows (U12 theorem on ledger-counted global gluing, U13 scoped refutation that no product-visible cost prior selects unit fugacity). In the SevenGaps gravity program this marks the shift from measure-first selectors to action-first ledger cost, tying the residual to recognition cost (J-cost) rather than to a free fugacity gauge. It does not itself advance T0–T8; it organizes which Gap-2 obligations remain after the R18 wall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.