CorrectedMeasurePremise
plain-language theorem explainer
Packages three propositions that encode Gap-2's surviving measure obligation: a named prior selects the Gibbs numerator a≡1, is stronger than label indifference, and forces the Gauge Counting Principle on physical class mass. Downstream code cites it as the AssumedRequired target and as the corrected floor after the R18 booking-gauge wall. Pure structure definition; no proof content.
Claim. A corrected measure premise is a triple of propositions $(P_{\mathrm{sel}}, P_{>}, P_{\mathrm{GCP}})$ where $P_{\mathrm{sel}}$ asserts that a named prior forces the Boltzmann numerator $a \equiv 1$ (equivalently selects the Gibbs weight among size-dependent indifference weights), $P_{>}$ asserts that this prior is strictly stronger than mere relabeling invariance / label indifference, and $P_{\mathrm{GCP}}$ asserts that the prior entails the Gauge Counting Principle for the physical class mass (equivalently $\nu = 1/|\mathrm{Aut}|$).
background
Gap-2 asks whether richer RecognitionLedger / posting-layer structure forces the Gauge Counting Principle (GCP) for physical class mass, i.e. the orbit measure $\nu = 1/|\mathrm{Aut}|$. The module runs a necessary-reasons census: every candidate fact that would make GCP unavoidable is proved, left open, recorded as MODEL, or refuted. Failed reasons do not flip to their opposites; they force a corrected floor plan.
Among the indifference family of size-dependent weights, the Gibbs choice is the one with Boltzmann numerator $a \equiv 1$. The audit shows mere label indifference does not select that numerator. The R18 block strengthens the wall: the fugacity–action rebooking $(a,S)\mapsto(t\cdot a, S+\log t)$ preserves the Boltzmann product pointwise, so no rebooking-invariant (or product-visible) prior can force $a\equiv 1$.
This structure is the typed residual after that census: not an inhabitant, but the shape of what a genuine selector would have to supply.
proof idea
Definition only: three bare Prop fields with no constructors, instances, or proofs. The structure is a target package. Downstream AssumedRequired wraps it as an existential conjunction of the three fields; no lemma is applied here.
why it matters
Closes the honesty contract of the gauge-counting census. After R07–R17-style refutations (invariant enrichment, equivariant costs, bare-posting gluing, size-blindness, site-symmetry counts, label indifference) and the scoped R18 wall (no product-visible prior selects $a\equiv 1$), the module must still name what would count as success. This structure is that name.
AssumedRequired is literally $\exists p:\texttt{CorrectedMeasurePremise}$ with all three fields true; the module explicitly does not claim an inhabitant. correctedFloorPlans banks the redirected research paths (derive Gibbs from a prior principle, not from invariant enrichment). R17/R18 refutations clear false routes into this residual.
In the broader RS gravity stack this sits under Gap-2 measure uniqueness: GCP is the counting law that would pin class mass once a genuine selector exists. The open residual flagged by the module is an action-first prior that pins $S$ independently of the measure, outside the rebooking wall.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.