MeasureDerivationIndex
plain-language theorem explainer
Record type that packages five boolean closure flags for Gap 2 measure derivation: gibbs class-mass gauge counting stated, C17/A1.7 gauge-counting route stated, premises certificate inhabited, C16 process discrimination packaged, and the measure flag moved after the 2026-07-30 review. Gravity auditors cite the inhabited witness that sets every flag true. Pure structure definition; no proof content.
Claim. A five-field boolean index recording whether (i) the closing theorem for the Gibbs-weight class mass is stated, (ii) the C17/A1.7 route to the gauge-counting principle is stated, (iii) the measure-derivation premises certificate is inhabited, (iv) C16 process discrimination is packaged, and (v) the measure flag has been moved (claimed 2026-07-30) so closings rest on C4+C17 theorems and the blocker equivalence, with C16 used only for process discrimination.
background
Gap 2 / A27 assembles the gauge-counting principle for the class mass of the Gibbs weight from substrate structure richer than bare automorphism counting. The module status is theorem-level assembly with the ledger flag deferred to hostile review; FullTheoryLedger is not imported here.
Load-bearing pieces are the C4 erasure Jacobian (the divisor appears as the Jacobian of label erasure, so Aut enters only in the conclusion), C17 unit-fugacity elimination (posted class mass equals $\mu$ on the A1.7 class), and the blocker equivalence $\mu = 1/|\mathrm{Aut},K|$ on representatives. C16 supplies an Aut-free LIFO process whose stationary class-mass ratio matches the directed inverse-Aut ratio at pre-registered witnesses; it is process discrimination, not a cited closing hypothesis.
Sibling premises package C4 bridges (pushforward_labeledWeight_eq_gauge_divisor, $\mu$ as Gibbs times erasure pushforward of one), C17 unit fugacity from surface and kind totals, C16 rate symmetry / cap uniformity / half-ratio under uniformity, labeled-weight framing, and the blocker iff. Jon's bookkeeping ruling assigns the base path-sum measure $\mu=1/|\mathrm{Aut},K|$ to flag 8 and the $J$-tilt continuum half to flag 9.
proof idea
No proof: this is a structure declaration. Five named Bool fields with doc-strings that act as a typed checklist for assembly status. Downstream, a single definitional witness fills every field with true. The mathematical content lives in the sibling inhabited-premises theorem and the C4/C17 closing lemmas those flags point at, not in this type.
why it matters
Gives Gap 2 a machine-checkable assembly index so flag-8 bookkeeping is explicit rather than prose-only. The sole downstream consumer is the concrete witness that sets all five flags true, recording that gibbs gauge counting, the A17 route, premises inhabitation, C16 discrimination packaging, and the post-review flag move are all claimed closed.
Under the 2026-07-30 gatekeeper ruling (MINOR, prose repaired), closings rest on C4+C17 theorems plus the blocker iff; C16 fields are discrimination only and are not cited by closing proof terms. That separates this path from the killed Aut-equivalent wrapper (semantic circularity). Framework role: discharges the typed obligation that the gauge-counting principle holds for $1/|\mathrm{Aut},K|$ from labeled weights, erasure pushforward, letter costs, and the LIFO process, without reintroducing Aut on the construction side. The $J$-tilt / continuum half remains flag 9.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.