module module moderate

`IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivation`

Synthesizes the Gap-2 stationary measure on tet-free complexes from the C4 erasure Jacobian and C17 fugacity collapse, with an optional C16 Poisson-coarea reading. Gravity auditors cite it for the gauge-counting identity that turns class mass into a size-blind Gibbs weight times a unit fibre. The argument packages relabeling invariance, erasure transport, and unit-fugacity elimination into named premise bundles and two headline theorems.

claimUnder the Gap-2 measure-derivation premises (C4 erasure Jacobian plus C17 unit-fugacity collapse, with optional C16 process discrimination), the stationary class mass of a letter-cost weight equals the posted measure $\mu$ times a unit fibre factor. Equivalently, after erasure, any size-blind Gibbs weight whose class masses match $\mu$ at the three atoms forces unit fugacity, so the gauge-counting identity $m_{\mathrm{class}}(w)=w\cdot|\mathrm{fibre}|$ holds and admits a Jacobian reading of the Gap-2 measure.

background

Gap 2 in the Seven Gaps gravity stack asks for a unique stationary measure on serially named, tet-free bounded complexes once Aut-gauge is fixed. Two upstream lanes supply the analytic ingredients. Gap2FugacityElimination (A19 / lane C17) states that after the C4 erasure Jacobian, any letter cost whose posted class mass equals $\mu$ at the three atoms and is representable by a size-blind weight forces UnitFugacity, collapsing the three sector fugacities; on the gluing-residue family this is the character-size form.

Gap2PoissonCoarea (A20 / lane C16) supplies the process side: a raw LIFO Poissonized post/unpost process has symmetric legal rates and hence a uniform stationary law on each finite cap; at equal census $(4,2,0)$ the stationary class-mass ratio of two Aut-distinct complexes is exactly $1/2$ (directed Aut correction).

This module introduces the Gibbs weight, its letterwise relabeling invariance (serial-name permutations preserving sizes), class-mass identities relating Gibbs weights to unit fibres and to $\mu$ via erasure, and the bundled premises MeasureDerivationPremises that package C4+C17 (with C16 as a non-load-bearing reading).

proof idea

Definition-and-synthesis module, not a single proof. It first records letterwise relabeling invariance of the Gibbs weight in Aut-free form (serial-name permutations). Class-mass lemmas then factor a Gibbs class mass as the weight times a unit fibre, and transport that equality onto $\mu$ through the C4 erasure map. Gauge-counting theorems restate the same identity from surface data and kind totals. The headline results gap2_measure_from_c4_c17 and gap2_measure_jacobian_reading assemble those lemmas under the bundled premises; c16_process_discrimination is kept as an optional process reading rather than a load-bearing hypothesis. Inhabitation and an index structure witness that the premise bundle is non-empty and citable.

why it matters in Recognition Science

Closes the measure-derivation step of Gap 2 by turning C4 erasure and C17 fugacity elimination into a single citable gauge-counting identity for the stationary class mass. Downstream, Gap2MeasureDerivationHostileProbe imports the module as a flag-8 synthesis target and reports only a minor prose issue (C16 named as if load-bearing), later repaired; the probe verdict is MINOR with the flag flipped in-session. Within Recognition gravity this is the bridge from the erasure Jacobian and unit-fugacity collapse to a usable Gap-2 measure, so later gap closures can quote class mass equals $\mu$ times unit fibre without reopening fugacity bookkeeping. It does not itself finish the full Seven Gaps chain; it supplies the measure ingredient those later steps consume.

scope and limits

Does not prove C4 erasure or C17 fugacity elimination; those are imported upstream.
Does not treat C16 Poisson coarea as load-bearing for the headline measure identity.
Does not derive numerical gravity constants or the full RS forcing chain T0–T8.
Does not claim Aut-group computations beyond serial-name relabeling invariance.
Does not close remaining Seven Gaps beyond the Gap-2 measure synthesis.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivationHostileProbe module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2PoissonCoarea module_import

declarations in this module (20)

theorem gibbsWeight_relabelInvariant L84
theorem classMass_gibbs_eq_gibbs_mul_unitFibre L91
theorem classMass_gibbs_eq_mu_via_erasure L110
theorem gap2_gauge_counting_gibbsWeight L125
theorem gap2_gauge_counting_from_surface_and_kindTotals L136
theorem gap2_measure_from_c4_c17 L148
theorem gap2_measure_jacobian_reading L165
theorem c16_process_discrimination L185
structure MeasureDerivationPremises L205
def measureDerivationPremises L243
theorem measureDerivationPremises_inhabited L286
structure MeasureDerivationIndex L310
def measureDerivationIndex L325
theorem index_gibbs L332
theorem index_a17 L333
theorem index_premises L334
theorem index_c16 L335
theorem index_flag_moved L337
theorem construction_is_gibbsWeight L348
theorem closing_eq_mu_not_wrapper L355