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)
128noncomputable def becTemperature (n m : ℝ) : ℝ :=
proof body
Definition body.
129 (2 * pi * hbar^2 / (m * kB_SI)) * (n / 2.612)^(2/3)
130
131/-! ## J-Cost Interpretation -/
132
133/-- In RS, chemical potential is J-cost gradient:
134
135 μ = ∂J_total/∂N
136
137 Adding a particle increases total J-cost by μ.
138
139 Particles flow from high μ to low μ to minimize J_total. -/
depends on (17)
Lean names referenced from this declaration's body.
-
J_total
in IndisputableMonolith.Astrophysics.ObservabilityLimits
decl_use
-
hbar
in IndisputableMonolith.Constants
decl_use
-
hbar
in IndisputableMonolith.Constants.Codata
decl_use
-
kB_SI
in IndisputableMonolith.Constants.ExternalAnchors
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
hbar
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use
-
hbar
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
gradient
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use