entropy_monotone
plain-language theorem explainer
The declaration establishes that the entropy function built from Z-complexity is strictly increasing for positive density. Researchers deriving the second law from Berry phase accumulation in the Recognition Science framework would cite this result. The proof is a direct algebraic verification that unfolds the definition and applies the strict monotonicity of the logarithm together with linear arithmetic.
Claim. For real numbers $z_1, z_2, d$ with $d > 0$, $z_1$ nonnegative and $z_1 < z_2$, the inequality $log(1 + z_1 d) < log(1 + z_2 d)$ holds.
background
The module derives the arrow of time from Berry phase monotonicity. R-hat steps preserve the ledger yet produce directed time because Z-complexity is monotonically non-decreasing, supplying an intrinsic before-after ordering without external thermodynamics. The upstream definition entropyFromZ sets entropy equal to the logarithm of one plus Z times density, which the module describes as thermodynamic entropy as coarse-grained Z: entropy equals the log of the number of microstates with Z at most the current value. This is monotone in Z, giving the second law.
proof idea
The proof is a term-mode verification. It unfolds the definition of entropyFromZ, applies the lemma Real.log_lt_log to the positive arguments obtained by nlinarith, and finishes with a second nlinarith step confirming the inequality.
why it matters
This supplies the monotonicity of entropy in Z that is required for the second law to emerge from Berry phase in the Recognition Science framework. It directly supports the module's listed results on forward accumulation, absolute Z immunity to reversal, and the emergence of thermodynamic entropy as coarse-grained Z. The result fills the chain step that defines temporal order via Z-complexity ordering and touches the open question of how topological asymmetry between forward and reverse steps enforces the arrow of time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 11 of 11)
-
Irreversibility equates four measures and picks low-entropy paths
"the system dynamics seeks those with the lowest entropy production rate ... emergent force ... minimizes the entropy production rate"
-
Entropy of heat diffusion rises monotonically on temporal networks
"we show that this quantity is monotone in time, yielding an information-theoretic analog of the second law of thermodynamics for inhomogeneous diffusion on temporal networks"
-
Excursions link currents to timing in double quantum dots
"thermo-kinetic uncertainty relations, showing how current precision ... is fundamentally constrained either by entropy production or by dynamical activity"
-
Abiotic uncertainties block clear biosignature detection on Enceladus
"racemization rate constants k(T) … D/L(t) evolution via Eq. 12"
-
Two-phase flow model adds bulk-surface coupling with thermodynamic consistency
"Sufficiently regular solutions of system (1.1) satisfy the energy-dissipation law (1.10)"
-
2D FrBD model preserves passivity in rolling friction
"the model preserves passivity under almost any parametrisation of practical interest"
-
Heat kernel isolates divergent action in nonlinear electrodynamics
"the strong-field causality condition … is necessary and sufficient for the convergence of the exact a1 and a2 contributions."
-
Plasmoid model matches FSRQ post-flare skewness shifts
"We further compute the ensemble Shannon entropy of the system and the skewness, where the entropy is found to decrease at a 3σ level in both the groups where skewness either increases or decreases, as a direct evidence of increase in order in the system caused by a flare."
-
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"