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)
55def alternativeDefinitions : List String := [
proof body
Definition body.
56 "μ = (∂G/∂N)_{T,P}",
57 "μ = (∂U/∂N)_{S,V}",
58 "μ = -T(∂S/∂N)_{U,V}"
59]
60
61/-! ## Ideal Gas -/
62
63/-- Chemical potential of ideal gas:
64
65 μ = kT ln(n λ³)
66
67 Where:
68 n = N/V = number density
69 λ = h/√(2πmkT) = thermal wavelength
70
71 μ increases with concentration (more particles = higher cost). -/
depends on (20)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
G
in IndisputableMonolith.Constants
decl_use
-
G
in IndisputableMonolith.Constants.Codata
decl_use
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
G
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
T
in IndisputableMonolith.Foundation.Breath1024
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
T
in IndisputableMonolith.Gap45.SyncMinimization
decl_use
-
G
in IndisputableMonolith.Gravity.JCostInflaton
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
density
in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use
-
S
in IndisputableMonolith.Relativity.ILG.Action
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use