firstAttackBlock
plain-language theorem explainer
Names the five reason codes that form the first attack block in the Gap-2 label-insertion dynamics census: D07, D04, D03, D06, D08. Anyone auditing the necessary-reasons table for InsertionStationarity cites this list as the ordered attack set. The body is a literal five-string list; length is discharged by decide downstream.
Claim. The first attack block is the ordered list of reason identifiers $[\mathrm{D07},\mathrm{D04},\mathrm{D03},\mathrm{D06},\mathrm{D08}]$ in the Gap-2 label-insertion dynamics necessary-reasons census.
background
Gap-2 asks for an explicit carrier-enlarging label-insertion/removal dynamics that forces InsertionStationarity (equivalently the GluingLaw), and thereby inverse factorials and the Gauge Counting Principle, without smuggling in $\mu$, Aut, unit fugacity, or a renamed stationarity axiom.
The module runs a necessary-reasons census: each candidate fact is THEOREM, OPEN, MODEL, or REFUTED. The D-codes live in the insertion-asymmetry sibling. D03 is equal-per-slot detailed balance with constant weight failing InsertionStationarity. D04 is the claim that size-blind birth with per-label death, plus unit/atom normalizations $f(0)=f(1)=1$, yields InsertionStationarity. D06 flags baking the target weight into the rates as a decoy. D07 records that fixed-carrier posting does not supply insertion stationarity. D08 says bare invariance axioms admit distinct measures.
A parallel historical firstAttackBlock in the gauge-counting census used R-codes and is superseded; this list is the dynamics-side counterpart.
proof idea
Pure definition: the value is the concrete list of five strings "D07", "D04", "D03", "D06", "D08". No lemmas or tactics. Downstream firstAttackBlock_length closes |firstAttackBlock| = 5 by decide.
why it matters
Gives the ordered attack surface for the label-insertion dynamics census that the composite certificate labelInsertionDynamics_certified packages (nine-row reason table, equal-per-slot counterexample, asymmetric-counting success under unit/atom, geometry inhabited, decoys and fixed-carrier routes ruled out). Parent length theorem and the gauge-counting module's own firstAttackBlock/length pair treat this list as the shared census handle.
In the Recognition Gravity Gap-2 program this is bookkeeping for the forcing path to GluingLaw/GCP, not a derivation of the missing physical rate asymmetry (size-blind birth vs per-label death), which the module doc leaves OPEN. It does not move gap2_measure_derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.