reasonTable_length
plain-language theorem explainer
The Gap-2 label-insertion necessary-reasons census is a finite table of exactly nine rows. Anyone packaging the composite certificate for insertion dynamics cites this length equality as the first conjunct. The proof is a one-shot decidable evaluation of a concrete list literal.
Claim. The necessary-reasons table for Gap-2 label-insertion dynamics has length exactly $9$.
background
Gap-2 in the gravity seven-gaps program asks for an explicit carrier-enlarging label-insertion and removal dynamics that forces InsertionStationarity (equivalently the GluingLaw), and thereby inverse factorials and the gauge-counting principle, without smuggling in unit fugacity or renaming the target.
This module runs a necessary-reasons census: every fact that would make that forcing unavoidable is listed, then marked THEOREM, OPEN, MODEL, or REFUTED. The table is a concrete Lean list whose rows are those reasons (status plus statement). Parent setting is the gluing-law stationarity development and the unit-fugacity selector; the method follows the Necessary Reasons Process plan.
Sibling material defines birth-death rates on carrier size, detailed balance (weight ratio equals rate ratio), equal-per-slot rates, and constant weight. Those feed later rows that show equal-per-slot balance forces constant weight and therefore fails InsertionStationarity, while size-blind birth with per-label death recovers the factorial world.
proof idea
The table is a closed list literal in the same module. The proof is a single decide step: Lean reduces List.length on that concrete value and checks equality to nine by decidable Nat equality. No lemmas about dynamics or stationarity are invoked.
why it matters
The composite certificate labelInsertionDynamics_certified opens with this length equality as its first conjunct, then packages detailed-balance facts, the failure of equal-per-slot rates against InsertionStationarity, and the success of size-blind birth with per-label death on the factorial weight. Parallel census modules (gauge-counting inevitable reasons, insertion-asymmetry inevitable reasons) use the same length-gate pattern with their own table sizes (18 and 17).
In the Recognition gravity stack this is bookkeeping for Gap-2, not a new dynamical law. It locks the census cardinality so downstream certificates cannot silently drop or add rows. It does not close the OPEN item in the module doc: deriving from recognition structure that birth is size-blind while death is per existing label. The measure flag gap2_measure_derived stays unmoved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.