`refrigerator_one_statement`

proved

show as: view math explainer →

module: IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec
domain: Engineering
line: 88 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.IdentityTickRefrigeratorSpec on GitHub at line 88.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  85/-- **REFRIGERATOR ONE-STATEMENT.** Per-cycle cooling fraction
  86`J(φ) ∈ (0.11, 0.13)`; cumulative cooling additive in cycles, strictly
  87monotonic. -/
  88theorem refrigerator_one_statement :
  89    0 < coolingFraction ∧
  90    (0.11 : ℝ) < coolingFraction ∧ coolingFraction < 0.13 ∧
  91    (∀ {n m : ℕ}, n < m → cumulativeCooling n < cumulativeCooling m) :=
  92  ⟨coolingFraction_pos, coolingFraction_band.1, coolingFraction_band.2,
  93   @cumulativeCooling_strict_mono⟩
  94
  95end
  96
  97end IdentityTickRefrigeratorSpec
  98end Engineering
  99end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.