becTemperature
plain-language theorem explainer
The becTemperature definition supplies the critical temperature below which Bose-Einstein condensation sets in for an ideal gas of density n and mass m. Quantum statisticians and Recognition Science modelers cite it when locating the point at which chemical potential vanishes and ground-state occupation becomes macroscopic. It is realized as a direct arithmetic expression that inserts the RS-native hbar and the SI Boltzmann constant into the standard formula with numerical factor 2.612.
Claim. The Bose-Einstein condensation temperature is the real number $T_c(n,m) = (2π ħ² / (m k_B)) (n / 2.612)^{2/3}$, where ħ is the reduced Planck constant and k_B is Boltzmann's constant.
background
The Thermodynamics.ChemicalPotential module treats chemical potential as the J-cost gradient μ = ∂J_total/∂N. J_total is the sum of mass and light contributions defined in Astrophysics.ObservabilityLimits, while the underlying cost functions come from MultiplicativeRecognizerL4 and ObserverForcing. In this setting particles flow to minimize total J-cost, and μ controls ledger occupation in the Bose or Fermi distributions.
proof idea
One-line definition that directly transcribes the textbook BEC temperature formula, substituting the imported constants hbar (from Constants and Codata) and kB_SI (from ExternalAnchors).
why it matters
This definition supplies the temperature scale that closes the Bose-Einstein regime inside the J-cost derivation of chemical potential. It supports the module target that μ = ∂J_total/∂N and the statement that particles pile into the ground state for T < T_c. No downstream uses are recorded yet; the entry therefore remains a self-contained anchor for later thermodynamic lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.