module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2FugacityPostingGluing`

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.GaugeCountingInevitableReasons module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2NonEquivariantPosting module_import

declarations in this module (40)

def UnitFugacity L126
theorem gibbsWeight_eq_gibbsSize L131
theorem classMass_sizeWeight_eq_mu_iff L141
theorem gibbsSize_eq_one_at_atom_sizes L155
theorem gibbsSize_unitFugacity L164
theorem unitFugacity_iff_mu_at_atoms L181
theorem unitFugacity_iff_normalizedAtTheAtoms L219
def characterCost L244
theorem characterCost_kindRates L250
theorem characterCost_kindOnly L255
theorem characterCost_equivariant L261
theorem historyCost_characterCost L265
theorem exp_log_mul_nat L272
theorem exp_neg_historyCost_characterCost L284
theorem postedWeight_characterCost L301
theorem postedWeight_characterCost_eq L307
theorem postedWeight_characterCost_sizeBlind L314
theorem characterSize_atom_vertex L320
theorem characterSize_atom_edge L324
theorem characterSize_atom_tet L328
theorem unitFugacity_characterSize_iff L334
theorem characterSize_gluesAt L350
theorem characterCost_countermodel L362
theorem gluing_and_posting_do_not_force_unit_fugacity L389
theorem characterCost_posts_mu_iff L410
theorem posts_mu_at_atoms_forces_unit_fugacity L437
theorem posts_mu_forces_gibbsSize L448
theorem gluing_hypothesis_is_idle L467
theorem postedWeight_tiltedCost_not_sizeWeight L488
theorem tiltedCost_classMass_eq_classMass_gibbsSize L499
theorem tiltedCost_classMass_glues_with_unit_fugacity L514
theorem no_posting_countermodel_with_nonunit_fugacity L534
theorem fugacity_posting_gluing_verdict L565
structure Index L591
def index L613
theorem index_premise_is_mu_at_atoms L623
theorem index_fugacity_free L624
theorem index_no_countermodel L625
theorem index_premise_not_derived L626
theorem index_not_shown_underivable L627