pith. machine review for the scientific record. sign in
def definition def or abbrev

identityTickRefrigeratorCert

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

formal statement (Lean)

  77def identityTickRefrigeratorCert : IdentityTickRefrigeratorCert where
  78  fraction_pos := coolingFraction_pos

proof body

Definition body.

  79  fraction_band := coolingFraction_band
  80  cumulative_zero := cumulativeCooling_zero
  81  cumulative_succ := cumulativeCooling_succ
  82  cumulative_pos := @cumulativeCooling_pos
  83  cumulative_strict_mono := @cumulativeCooling_strict_mono
  84
  85/-- **REFRIGERATOR ONE-STATEMENT.** Per-cycle cooling fraction
  86`J(φ) ∈ (0.11, 0.13)`; cumulative cooling additive in cycles, strictly
  87monotonic. -/

depends on (7)

Lean names referenced from this declaration's body.