firstAttackBlock_length
plain-language theorem explainer
The first attack block in the Gap-2 label-insertion necessary-reasons census is a finite list of length exactly five. Census and certificate authors cite it to pin the block size before packaging the composite dynamics certificate. The proof is a one-shot `decide` on a concrete closed list.
Claim. The first attack block (the initial finite list of necessary-reason rows in the Gap-2 label-insertion dynamics census) has length $5$.
background
Gap-2 in this gravity stack concerns carrier-enlarging label insertion and removal. The module assumes the corrected target: an explicit 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 hypothesis.
The method is a necessary-reasons census: every fact that would make that forcing unavoidable is listed and marked proved, open, model, or refuted. Sibling material defines birth-death rates, detailed balance (weight ratio equals rate ratio), equal-per-slot rates (which force constant weight and therefore fail InsertionStationarity), and size-blind birth with per-label death (which can force stationarity once unit/atom data are fixed).
firstAttackBlock is the concrete initial block of that census list. List length here is ordinary finite-list cardinality (as in the primitive trace-length notion elsewhere in the stack), not a dynamical path length.
proof idea
One-line decidability proof. The block is a closed concrete list in the same module; decide evaluates the Nat equality length = 5 by computation. No lemmas about rates, balance, or geometry are invoked.
why it matters
The length pin is part of the composite certificate labelInsertionDynamics_certified, which asserts among other conjuncts that the full reason table has length 9, that equal-per-slot rates balance a constant weight yet fail InsertionStationarity, and that size-blind birth with per-label death balances the factorial-world weight and restores InsertionStationarity. Downstream, GaugeCountingInevitableReasons reuses the same length fact when assembling attack blocks toward gauge-counting inevitability.
In the Recognition gravity program this is bookkeeping for Gap-2 closure toward the Gauge Counting Principle, not a derivation of the physical rate asymmetry. The module honesty note still leaves open deriving, from recognition structure, that birth is size-blind while death is per existing label (or an equivalent asymmetry yielding $\mu_{n+1}=(n+1)\lambda_n$ without baking stationarity into the rates). The measure flag gap2_measure_derived remains unmoved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.