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

H_ThermodynamicsVerified

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)

  39def H_ThermodynamicsVerified : Prop :=

proof body

Definition body.

  40  ∀ (s : Thermodynamics.LedgerState), ∀ b ∈ s.active_bonds,
  41    let m := s.bond_multipliers b
  42    let u := Real.log m
  43    Cost.Jcost m ≥ u^2 / 2
  44
  45-- Legacy axiom eliminated. See Foundation.ConstantDerivations.
  46
  47end Information
  48end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.