reasonTable
plain-language theorem explainer
A nine-row census of necessary reasons for Gap-2 label-insertion dynamics: which birth-death facts force InsertionStationarity (hence inverse factorials and gauge counting) without smuggling in mu, Aut, or unit fugacity. Anyone auditing the Gap-2 forcing chain cites it as the scoreboard of proved, refuted, and still-open selectors. It is a literal list literal of status triples, not a derived theorem.
Claim. The Gap-2 label-insertion necessary-reasons table is the fixed list of nine status records $(D01\ldots D09)$, each a triple $(\mathrm{id},\ \mathrm{title},\ \mathrm{status})$ with status in $\{\mathrm{THEOREM},\ \mathrm{OPEN},\ \mathrm{MODEL},\ \mathrm{REFUTED}\}$. Rows cover detailed balance of weights versus rates, failure of equal per-slot rates to give insertion stationarity, size-blind birth with per-label death, inhabited $n+1$ slot geometry, decoy rate laws, and three open recognition-dynamics links.
background
Gap-2 asks for a carrier-enlarging label insertion/removal dynamics that forces InsertionStationarity (equivalently the gluing law), and thereby inverse factorials and the Gauge Counting Principle, without assuming $\mu$, $\mathrm{Aut}$, unit fugacity, or stationarity under another name.
InsertionStationarity on a weight $f:\mathbb{N}\to\mathbb{R}$ is the local law $f(0)=f(1)=1$ and $f(n+1)\cdot(n+1)=f(n)$: unit empty and singleton carriers, with $n+1$ interleaving slots when a new label is added. The weight class is label density (orbit size over sector relabeling count), stated without Aut or $\mu$.
This module runs the Necessary Reasons Process: every fact that would make that forcing unavoidable is listed and tagged THEOREM, OPEN, MODEL, or REFUTED. A failed reason does not automatically assert its opposite. Parent setting is Gap2GluingLawStationarity and the unit-fugacity selector line.
proof idea
Pure definition: a list literal of nine ReasonStatus structures. No tactics, no lemmas applied. Each row hard-codes an id string, a one-line title, and a status tag matching the honesty block in the module doc (D01–D05 and the positive half of D04 as THEOREM; D03 and D06 as REFUTED; D07–D09 as OPEN). Downstream length and certificate theorems simply read this table.
why it matters
This table is the Gap-2 dynamics scoreboard. The composite certificate labelInsertionDynamics_certified asserts reasonTable.length = 9 together with the proved balance and stationarity facts (detailed balance for constant weight under equal per-slot rates, failure of that weight under InsertionStationarity, and success under size-blind birth plus per-label death). Sibling modules GaugeCountingInevitableReasons and InsertionAsymmetryInevitableReasons mirror the same census pattern and re-use or extend these D-rows.
Framework role: closing D07–D09 would derive, from recognition structure alone, the birth/death asymmetry that yields $\mu_{n+1}=(n+1)\lambda_n$ without baking stationarity into the rates—the missing step before gap2_measure_derived can move. Until then the census banks what is already forced (detailed balance, geometry, decoy rejection) and isolates the open recognition-rate link. No Target Research job is required merely to hold this list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.