pith. machine review for the scientific record. sign in
def

entropyFromZ

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.ArrowOfTime
domain
Foundation
line
91 · github
papers citing
2 papers (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArrowOfTime on GitHub at line 91.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  88/-- Thermodynamic entropy as coarse-grained Z:
  89    entropy = log of the number of microstates with Z ≤ current Z.
  90    This is monotone in Z, giving the second law. -/
  91noncomputable def entropyFromZ (z : ℝ) (density : ℝ) : ℝ :=
  92  Real.log (1 + z * density)
  93
  94/-- Entropy is monotone in Z (second law from Berry phase). -/
  95theorem entropy_monotone (z₁ z₂ d : ℝ) (hd : 0 < d) (hz : 0 ≤ z₁) (h : z₁ < z₂) :
  96    entropyFromZ z₁ d < entropyFromZ z₂ d := by
  97  unfold entropyFromZ
  98  apply Real.log_lt_log (by nlinarith)
  99  nlinarith
 100
 101end
 102
 103end IndisputableMonolith.Foundation.ArrowOfTime

papers checked against this theorem (showing 2 of 2)