Cosmology Statistics Kernels Bose Energy Kernel Eq Occupation

The energy kernel

The Bose-Einstein distribution describes how many particles occupy a quantum state at a given temperature. For a state with energy E at temperature T, the average occupation number is 1/(e^E/T − 1). This is one of the foundational results of quantum statistics, derived by Satyendra Nath Bose and Albert Einstein in 1924.

The Recognition Science framework, a formal system for deriving physics from a ledger of recognition events, reconstructs this result from first principles. Its machine-checked library of formal theorems starts with a single quantum mode and the Gibbs weight e^−nE/T for each occupancy n. Summing over all allowed occupancies gives the partition function, and the average occupation follows as the ensemble mean. The framework proves that this average equals the Bose-Einstein form exactly.

In Recognition Science, the energy kernel t/(e^t − 1), where t = E/T, is not introduced as a separate assumption. The declaration boseEnergyKernel_eq_occupation proves that this kernel equals t times the average occupation number. In plain words: the energy kernel is just the average energy of a mode, written in dimensionless form. The proof is a theorem in the framework's library, checked by the Lean kernel, and it holds for any positive temperature.

This result also shows the energy kernel is not independent of the pressure kernel. The framework proves that the average occupation is the negative derivative of the log of the partition function, so the energy and pressure kernels are related by differentiation. This matches the grand-canonical formalism of statistical mechanics, where thermodynamic quantities derive from a single partition function.

What the declaration does not claim: it does not derive the Gibbs weight itself, which remains a model assumption. It does not explain why bosons allow unlimited occupancy; that bridge from the framework's exclusion principle to the occupancy set remains open. And it does not claim the Bose-Einstein distribution is unique to Recognition Science; the framework reproduces a known result of quantum statistics, which is a derivation, not a new discovery.

/-- **THEOREM: the Bose energy kernel is `t·⟨n⟩_B`.**  The integrand of
the plasma energy is (dimensionless energy) × (mean occupation). -/
theorem boseEnergyKernel_eq_occupation {t : ℝ} (ht : 0 < t) :
    boseEnergyKernel t = t * boseOccupation t := by
  rw [boseOccupation_eq ht]
  unfold PhaseSpaceReduction.boseEnergyKernel
  ring

/-- **THEOREM (Bose–Einstein distribution).**  The ensemble-mean
occupation of a bosonic mode is `⟨n⟩_B = 1/(eᵗ−1)`: the weighted
geometric series `Σ n·xⁿ = x/(1−x)²` divided by `Z_B = (1−x)⁻¹`. -/
theorem boseOccupation_eq {t : ℝ} (ht : 0 < t) :
    boseOccupation t = 1 / (Real.exp t - 1) := by
  unfold boseOccupation
  rw [bosePartition_eq ht]
  simp only [boltzmannWeight_pow]
  have hx0 : (0 : ℝ) ≤ Real.exp (-t) := le_of_lt (Real.exp_pos _)
  have hx1 : Real.exp (-t) < 1 := exp_neg_lt_one ht
  rw [tsum_coe_mul_geometric_of_norm_lt_one
    (by rw [Real.norm_of_nonneg hx0]; exact hx1)]
  have hy : 1 < Real.exp t := one_lt_exp ht
  have hy0 : Real.exp t ≠ 0 := ne_of_gt (Real.exp_pos t)
  have hy1 : Real.exp t - 1 ≠ 0 := by linarith
  have h1x : 1 - Real.exp (-t) ≠ 0 := by linarith
  rw [Real.exp_neg]
  rw [Real.exp_neg] at h1x
  field_simp

/-- **THEOREM (grand-canonical consistency, Bose).**  The mean occupation
is minus the derivative of the log partition function with respect to the
dimensionless energy: `d/dt[−ln(1−e^{−t})] = −⟨n⟩_B(t)`.  The pressure
and energy kernels are therefore *one* input, not two. -/
theorem boseLogKernel_hasDerivAt {t : ℝ} (ht : 0 < t) :
    HasDerivAt boseLogKernel (-(boseOccupation t)) t := by
  have h1 : HasDerivAt (fun s : ℝ => -s) (-1) t := (hasDerivAt_id t).neg
  have h2 : HasDerivAt (fun s : ℝ => Real.exp (-s))
      (Real.exp (-t) * (-1)) t := (Real.hasDerivAt_exp (-t)).comp t h1
  have h3 : HasDerivAt (fun s : ℝ => 1 - Real.exp (-s))
      (0 - Real.exp (-t) * (-1)) t := (hasDerivAt_const t 1).sub h2
  have hlt : Real.exp (-t) < 1 := exp_neg_lt_one ht
  have hne : 1 - Real.exp (-t) ≠ 0 := by linarith
  have h4 := (h3.log hne).neg
  have heq : -((0 - Real.exp (-t) * (-1)) / (1 - Real.exp (-t)))
      = -(boseOccupation t) := by
    rw [boseOccupation_eq ht]
    have hy0 : Real.exp t ≠ 0 := ne_of_gt (Real.exp_pos t)
    have hy1 : Real.exp t - 1 ≠ 0 := by
      have := one_lt_exp ht; linarith
    rw [Real.exp_neg]
    rw [Real.exp_neg] at hne
    field_simp
    ring
  rw [← heq]
  exact h4

What this page does not claim

The Gibbs weight is a model assumption, not a theorem. The framework does not derive the bosonic occupancy set from its exclusion principle. The Bose-Einstein distribution is a standard result reproduced by the framework, not a new prediction.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/StatisticsKernels.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: