MeasureDerivationPremises
plain-language theorem explainer
Named premises certificate for Gap-2 flag-8 measure derivation: nine propositional fields bundling C4 erasure-Jacobian facts, C17 unit-fugacity forcing, C16 LIFO process discrimination (Cap-3 measured, Cap-4 open-strength), the labeled-weight framing model, and blocker equivalence to class mass μ. Auditors of the GaugeCountingPrinciple assembly cite this so weaker tiers cannot be silently promoted. Structure definition only, not a proved theorem.
Claim. A record of nine propositional premises for deriving gauge-counting on class mass of the Gibbs weight: letterwise relabel-invariant labeled weight pushes forward to weight times the gauge divisor; Gibbs weight is the size-only Jacobian factor; fixed kind totals plus surface-pure dilate history force unit fugacity with posted class mass $\mu$; LIFO reverse-pair rate symmetry yields uniform detailed balance; Cap-3 tet-free LIFO law is uniform $1/910$ (measured); Cap-4 uniformity by the same argument (unformalized); under uniformity the $\pi$-weighted class-mass ratio at $(4,2,0)$ equals $1/2$; path-sum measure is erasure pushforward of a letterwise-invariant labeled weight; gauge-counting for $\nu$ holds iff $\nu$ on representatives equals $\mu$.
background
Gap 2 (A27) asks for a substrate derivation of the gauge-counting principle on class mass of the Gibbs weight, without putting the automorphism group on the construction side. The module assembles that obligation from three strands: C4 (erasure Jacobian), C17 (fugacity elimination), and C16 (LIFO process discrimination). FullTheoryLedger is not imported; the flag flip is deferred to hostile review.
Under the bookkeeping ruling, the base path-sum measure is $\mu = 1/|\mathrm{Aut},K|$, with Aut appearing only as C4's Jacobian denominator. The J-tilt $e^{-SJ}$ is routed to flag 9 (continuum half), not flag 8. Construction cites labeled weights, erasure pushforward, letter costs, and the LIFO process only.
Each field of this structure carries an honest tier in its docstring (THEOREM, MEASURED, DERIVED-UNFORMALIZED, MODEL). Below-theorem premises are named explicitly so they cannot be silently promoted when the assembly is later discharged.
proof idea
No proof body: this is a structure whose fields are bare Prop slots. Each field is a named hypothesis interface fixed by its docstring (C4 pushforward identity, Gibbs-as-Jacobian factor, C17 unit-fugacity forcing, C16 rate-symmetry balance, Cap-3 measured uniformity $1/910$, Cap-4 derived-unformalized uniformity, half-ratio under uniformity, labeled-weight framing model, and blocker equivalence to $\mu$ on representatives). Inhabitation is supplied downstream by the certificate value, which fills each slot with a cited source fact or a named open-strength premise (Cap-4 via UniformNamedPremise at the witness ambient, not a kernel solve).
why it matters
This is the typed obligation surface for flag-8 assembly of the gauge-counting principle. Downstream, the inhabited certificate fills the slots from source facts; the hostile-probe uniqueness result uses the same substrate to show that among invariant labeled weights, only the Gibbs weight induces the principle.
Per the module ruling, load-bearing for the base close are the blocker-iff-$\mu$ equivalence and the C4 bridge; for the no-tilt close, C17 unit-fugacity plus the blocker equivalence; the labeled-weight/erasure-pushforward carrier is definitionally load-bearing (MODEL). C16 fields are process discrimination only. The assembly is deliberately not an Aut-equivalent wrapper (the 2026-07-26 circularity kill). Cap-4 uniformity remains the named open-strength premise inside the certificate, keeping the honesty boundary visible for review.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.