measureDerivationIndex
plain-language theorem explainer
Five-bit certificate that Gap 2 flag 8's measure-derivation assembly is complete: Gibbs class-mass gauge counting, the A1.7 route, inhabited premises, C16 process discrimination, and the 2026-07-30 flag move are all marked true. Gravity auditors cite it when checking that GaugeCountingPrinciple for gibbsWeight class mass was discharged without Aut on the construction side. The body is a pure structure instance with every field set to true.
Claim. The measure-derivation index is the Boolean record asserting that (i) the closing theorem for Gibbs-weight class mass is stated, (ii) the C17 A1.7 route to the gauge-counting principle is stated, (iii) the premises certificate is inhabited, (iv) C16 process discrimination is packaged, and (v) the measure-derived flag has been moved.
background
Gap 2 (A27) assembles the gauge-counting principle for the class mass of the Gibbs weight from three substrate pieces: the C4 erasure Jacobian (Aut appears only as the Jacobian denominator in the conclusion), C17 unit-fugacity elimination (so posted class mass equals $\mu$ on the A1.7 class), and C16 LIFO process discrimination (Aut-free stationary class-mass ratios matching the directed inverse-Aut ratio at pre-registered witnesses).
Under the bookkeeping ruling, the base path-sum measure is $\mu = 1/|\mathrm{Aut}, K|$; the $J$-tilt $e^{-SJ}$ is routed to flag 9, not flag 8. The index structure packages five Boolean status bits for that assembly. Its sibling premises certificate asserts that the C4 Jacobian and Gibbs-factor theorems, C17 unit fugacity, and C16 rate-symmetry and uniformity premises are all inhabited (or tagged DERIVED-UNFORMALIZED for the named uniformity premise).
FullTheoryLedger is deliberately not imported here; the flag flip is a separate gatekeeper-signed bookkeeping step.
proof idea
Pure definitional structure instance. Each of the five fields of MeasureDerivationIndex is set to the Boolean literal true. No lemmas are applied; no tactics run. Downstream rfl theorems read the fields back.
why it matters
Bookkeeping anchor for flag 8 of the Seven Gaps gravity stack. Downstream one-liners index_gibbs, index_a17, index_premises, index_c16, and index_flag_moved expose each bit as a theorem; the hostile-probe module re-exports flag_moved so external review can assert the 2026-07-30 gatekeeper flip without opening the assembly file.
Closes the typed obligation to derive GaugeCountingPrinciple exactly for $1/|\mathrm{Aut}, K|$ from substrate richer than bare counting, without reintroducing Aut on the construction side (the 2026-07-26 Aut-wrapper discharge was killed as G1 circular). Does not touch the continuum/$J$-tilt half, which remains flag 9 (gap2_geometric_continuum_limit). Sits inside the gravity domain of the Recognition forcing chain rather than the T0–T8 foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.