BECParameters
plain-language theorem explainer
BECParameters is the record holding number density n, boson mass m and critical temperature T_c together with their positivity proofs. A researcher deriving quantum statistics from the even-phase ledger would cite this structure when stating the condition for macroscopic ground-state occupation. The declaration is a direct structure definition that packages the three positive reals required by the subsequent occupation theorem.
Claim. A structure consisting of positive real numbers $n>0$, $m>0$, $T_c>0$ where $n$ denotes particle number density, $m$ the boson mass, and $T_c$ the critical temperature satisfying $T_c = (2πℏ²/m k_B)(n/ζ(3/2))^{2/3}$ with ζ(3/2)≈2.612.
background
The module derives the Bose-Einstein distribution from Recognition Science's eight-tick even-phase ledger constraint: bosons carry integer spin so their phase factor is +1, wave functions are symmetric, and the minimum-J-cost state at fixed energy and particle number yields the distribution 1/(exp((E-μ)/kT)-1). Temperature is defined in the upstream BoltzmannDistribution module as the reciprocal of the Lagrange multiplier β, satisfying the thermodynamic relation dE/dS = T. The structure BECParameters simply collects the three positive scalars that enter the standard expression for T_c and that are required by the downstream occupation statement.
proof idea
This is a structure definition; no tactics or lemmas are applied. The three fields n, m, T_c are declared as ℝ and the three positivity hypotheses are attached directly as fields of the record.
why it matters
The record supplies the inputs to bec_ground_state_occupation, the theorem that asserts macroscopic ground-state occupation below T_c. It therefore closes the step from the even-phase ledger (MODULE_DOC) to the concrete prediction of Bose-Einstein condensation inside the Recognition Science derivation of quantum statistics. The construction sits inside the T7 eight-tick octave and the RCL functional equation that together force the symmetric statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.