ReasonStatus
plain-language theorem explainer
A three-field record that tags one entry in the Gap-2 necessary-reasons census: short id, human title, and a status string drawn from THEOREM, OPEN, MODEL, or REFUTED. Anyone reading the label-insertion dynamics audit cites it as the row type of the reason table. There is no proof body; it is a plain data structure.
Claim. A reason-status record is a triple $(i,t,s)$ of strings, where $i$ is a short identifier, $t$ is a human-readable title, and $s\in\{\texttt{THEOREM},\texttt{OPEN},\texttt{MODEL},\texttt{REFUTED}\}$ records the audit status of that reason in the Gap-2 label-insertion dynamics census.
background
The module audits Gap-2 label-insertion dynamics under the corrected target: a carrier-enlarging insert/remove process that forces InsertionStationarity (equivalently the GluingLaw), and thereby inverse factorials and the Gauge Counting Principle, without smuggling in $\mu$, Aut, unit fugacity, or stationarity under a new name.
Method is a necessary-reasons census: every fact that would make that forcing unavoidable is listed and classified. Status vocabulary is fixed by the field doc: THEOREM (proved), OPEN (missing derivation), MODEL (assumed dynamics), or REFUTED (fails as a selector). Parent setting is Gap2GluingLawStationarity and the unit-fugacity selector line.
This structure is only the row type for that census. Sibling modules (gauge-counting and insertion-asymmetry inevitable-reasons) reuse the same three-field shape so tables stay comparable across Gap-2 subclaims.
proof idea
No proof. The declaration is a structure definition with three String fields (id, title, status). The status field is documented to hold one of the four census tags. Instantiation is by structure literal or anonymous constructor when building reasonTable.
why it matters
It is the shared schema for the Gap-2 necessary-reasons tables. Downstream, reasonTable in this module fills rows D01–D05 (detailed balance, equal per-slot rates, size-blind birth plus per-label death, slot geometry, and the equal-rate refutation). Parallel ReasonStatus / reasonTable copies in GaugeCountingInevitableReasons and InsertionAsymmetryInevitableReasons keep the same audit language.
In the Recognition gravity stack this is bookkeeping for the Gap-2 forcing path toward InsertionStationarity and gauge counting, not a physics law itself. The module honesty block still leaves OPEN the recognition-structural derivation that birth is size-blind while death is per label (the rate asymmetry that yields $\mu_{n+1}=(n+1)\lambda_n$ without baking stationarity into the rates). The structure does not close that OPEN item; it only types the census that records it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.