module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureDerivation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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