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)
119theorem initial_state_minimum_entropy {N : ℕ} (hN : 0 < N) :
120 entropy (unity_config N hN) = 0 := unity_defect_zero hN
proof body
Term-mode proof.
121
122/-- **Theorem**: Any non-unity state has positive entropy. -/
depends on (6)
Lean names referenced from this declaration's body.
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
entropy
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
unity_config
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
unity_defect_zero
in IndisputableMonolith.Foundation.InitialCondition
decl_use
-
entropy
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
entropy
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use