module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure`

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 (2)

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

IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityElimination module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasureHostileProbe module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting module_import

declarations in this module (23)

abbrev labeledWeight L69
def rename L74
def RelabelInvariant L82
def erase L88
def erasePush L92
theorem rename_eq_push L98
theorem relabelInvariant_implies_classFun L104
theorem relabelInvariant_one L116
theorem relabelInvariant_exp_neg_history L120
theorem pushforward_labeledWeight_eq_gauge_divisor L133
theorem mu_eq_gibbs_mul_erasePush_one L161
theorem gibbsWeight_is_the_erasure_jacobian L176
theorem dust_twin_admissible L196
theorem autCard_dust_twin L203
theorem autCard_dust_twin_ne_square L210
def LocallyAdditive L221
theorem no_local_additive_cost_realizes_log_aut L228
theorem uniform_is_not_a_local_pushforward L253
structure LabelErasureIndex L289
def labelErasureIndex L297
theorem index_d1 L302
theorem index_d2 L303
theorem index_flag_unmoved L306