theorem
proved
entropy_monotone
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.ArrowOfTime on GitHub at line 95.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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 3 of 3)
-
Bulk viscosity locks curvature sign for baryogenesis
"Bulk viscosity guarantees positive entropy production, d/dt(a³s) = 9ζH²/T a³ ≥0. This monotonicity is the thermodynamic origin of sign locking"
-
Mutual information yields parameter-free SGS models
"we assume that the temporal variation of kTG is insensitive to the energy production and dissipation terms to obtain the local inter-scale equilibrium"
-
Next-token learning selects world-tracking encodings matching training ecologies
"under explicit heredity, variation, and selection assumptions... inter-model selection pushes toward lower ecological excess loss"