R18Status
plain-language theorem explainer
Status tag for census row R18 in the Gap-2 gauge-counting necessary-reasons table. It records the scoped verdict that no prior seeing only the physical Boltzmann product can force unit fugacity (Gibbs numerator a ≡ 1), because rebooking-invariant priors always admit non-unit representatives. Downstream block certification quotes this exact string. The body is a one-line string constant.
Claim. The R18 row verdict string is fixed as $\texttt{REFUTED\_OVER\_REBOOKING\_INVARIANT\_PRIORS}$, i.e. the selector claim that a prior forces the Gibbs numerator $a \equiv 1$ is recorded as refuted for every prior invariant under the fugacity–action rebooking $(a,S)\mapsto(t\cdot a,\,S+\log t)$.
background
The module runs a necessary-reasons census for Gap-2: if richer RecognitionLedger / posting-layer structure is to force the Gauge Counting Principle (physical class mass $\nu = 1/|\mathrm{Aut}|$), every candidate reason is banked as proved, open, model, or refuted. A failed reason does not flip to its opposite; it forces a corrected floor plan.
R18 is the surviving selector target: the proposition AssumedRequired that some prior forces unit fugacity $a \equiv 1$ in the Gibbs weight. The module header records the R18 block as theorem-level: the rebooking gauge $(a,S)\mapsto(t\cdot a,,S+\log t)$ preserves the Boltzmann product pointwise; every satisfiable rebooking-invariant prior admits a non-unit-fugacity representative; every product-visible prior (one that sees only the physical weight) is rebooking-invariant. Hence no such prior selects $a \equiv 1$.
The literal assumed Prop remains vacuously inhabitable (a decoy scored by the vacuity guard); the honest discharge is the wall, not the inhabitant. Residual open route: an action-first prior that pins $S$ independently of the measure.
proof idea
Definitional constant: the body is the string literal "REFUTED_OVER_REBOOKING_INVARIANT_PRIORS". No tactics, no lemmas. The adjacent doc note marks the first attack block as historical; R18 closed as a scoped wall, superseded by secondAttackBlock.
why it matters
Bookkeeping anchor for the R18 honesty package. Parent theorem R18_block_certified asserts the conjunction of the wall theorem, the vacuity guard (literal target still inhabitable), corrected floor-plan length 5, empty next-attack block, and exact equality of this status string with the refuted-over-rebooking tag.
In the Gap-2 program this closes one false derivation path to GCP from richer structure: product-visible / rebooking-invariant priors cannot force the Gibbs numerator. It sits among the other REFUTED rows (invariant enrichment, equivariant posting cost, bare-posting gluing, size-blindness, ledger-cost readout, label indifference as selector). Framework role is census hygiene for the measure-substrate blocker, not a new dynamical law; the open residual remains action-first selection of $S$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.