module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting`

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

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

IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityPostingGluing module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPostingHostileProbe module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2PostingLayerFloor module_import

declarations in this module (68)

def sgnLt L148
theorem sgnLt_swap L152
theorem sgnLt_cases L158
theorem classMass_zero L162
theorem classMass_add L168
theorem classMass_neg L175
theorem classMass_one L187
theorem there L199
def numeratorMass L206
class mass L210
theorem classMass_postedWeight L214
theorem mu_eq_orbitCard_mul_gibbsWeight L231
theorem posts_mu_iff_numeratorMass_eq_orbitCard L248
theorem orbitMeanOne_forces_one_of_invariant L270
def swap01 L301
theorem swap01_involutive L304
theorem swap01_trans_self L313
theorem swap01_apply_zero L316
theorem swap01_apply_one L321
def edgeRelabel L328
def twist L339
theorem twist_nE L341
theorem twist_edgeVerts L343
theorem twist_twist L348
def twistEquiv L354
theorem twistEquiv_apply L360
def twistRel L365
theorem twist_equivalent L374
theorem twist_class L376
theorem classMass_comp_twist L387
theorem classMass_of_twistOdd L398
def keyAt L417
theorem keyAt_of_lt L420
theorem keyAt_twist L426
theorem keyAt_twist_zero L439
theorem keyAt_twist_one L444
def edgeSign L452
theorem edgeSign_cases L455
theorem edgeSign_eq_zero_of_nE_le_one L467
theorem edgeSign_twist L474
def tiltedNumer L491
theorem tiltedNumer_pos L493
theorem tiltedNumer_twist L500
theorem tiltedNumer_eq_one_of_nE_le_one L506
def tiltedCost L514
theorem historyCost_tiltedCost L521
theorem exp_neg_historyCost_tiltedCost L534
theorem postedWeight_tiltedCost L538
theorem numeratorMass_tiltedCost L547
theorem tiltedCost_posts_mu L570
theorem keyAt_loopAndBridge_zero L581
theorem keyAt_loopAndBridge_one L583
theorem edgeSign_loopAndBridge L585
theorem tiltedNumer_loopAndBridge L592
theorem numerator_ne_one_at_loopAndBridge L598
theorem tiltedCost_not_equivariant L612
theorem postedWeight_tiltedCost_not_invariant L629
theorem normalizedAtTheAtoms_tiltedCost L646
theorem nonequivariant_cost_posts_mu_with_nonunit_numerator L661
theorem equivariance_is_load_bearing L680
theorem nonequivariant_posting_family L699
theorem family_injective_at_loopAndBridge L709
theorem nonequivariant_case_verdict L725
structure Index L758
def index L776
theorem index_nonequivariant_settled L785
theorem index_cost_layer_does_not_determine L787
theorem index_premise_still_open L790