module module

`IndisputableMonolith.Cosmology.RefineTrigger`

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.Cosmology.RecognitionEquilibrium module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.RungCoarsen module_import

declarations in this module (17)

def reconstructUnder L60
theorem lossless_iff L69
def descendLaw L87
theorem lossless_law L92
theorem descendLaw_necessary L100
def Jcost L111
theorem jcost_pos L114
theorem jcost_arbitrarily_small_positive L128
def demand L145
def b01 L151
theorem b01_zero L153
theorem b01_one L154
theorem cost_singleton L156
theorem epsilon_unsafe L163
structure LawGivenTrigger L206
theorem lawGivenTrigger L214
theorem t3_law_derived_refinement L227