Cosmology Statistics Kernels Bose Energy Kernel From Log Kernel

The energy kernel as a derivative

In statistical mechanics, a single quantum mode with energy E at temperature T is described by a partition function, a sum over all possible occupancies n of the mode weighted by the Gibbs factor e^−nE/T. For bosons, particles that may share a state, n runs over all nonnegative integers. The partition function for one bosonic mode is the geometric series Z = 1 + e^−t + e^−2t + ..., where t = E/T, which sums to Z = 1/(1 − e^−t).

The average occupancy of the mode, ⟨n⟩, is the ensemble mean (Σ n·e^−nt)/Z, and it evaluates to the Bose–Einstein distribution 1/(e^t − 1). The average energy of the mode is then t·⟨n⟩, because each quantum carries energy E = tT. This is the energy kernel, the function t/(e^t − 1) that appears inside momentum-space integrals for the energy density of a boson gas.

The framework's machine-checked library of formal theorems proves that this energy kernel is not an independent input. It establishes the identity boseEnergyKernel t = −t·d/dt[ln Z(t)], which says the average energy equals minus the derivative of the log-partition function with respect to t, scaled by t. In physical variables this is the standard thermodynamic relation ⟨E⟩ = −∂/∂β ln Z, where β = 1/T. The pressure kernel, −ln(1 − e^−t), and the energy kernel are therefore derivative-related, exactly as the grand-canonical formalism demands.

In Recognition Science, this theorem means the Bose energy kernel used in cosmological plasma calculations is derived from the single-mode partition function, not postulated separately. The derivation starts from the Gibbs weight e^−nE/T and the occupancy set n ∈ ℕ, and proceeds through the partition function, the occupation number, and the derivative identity. The same structure holds for fermions, with the occupancy set restricted to {0, 1} by Pauli exclusion, giving the Fermi–Dirac distribution 1/(e^t + 1) and the energy kernel t/(e^t + 1).

What the theorem does not claim is also precise. It does not derive the Gibbs weight itself, which remains a modeling choice for the canonical ensemble measure. It does not derive the Pauli exclusion principle from first principles; the bridge from the framework's cost-based exclusion certificate to the occupancy set {0, 1} remains open. And it does not establish any new physics beyond the standard grand-canonical formalism, which already contains this derivative relation. The theorem's contribution is formal: it shows the energy kernel follows from the partition function within a machine-checked proof system, closing a definitional gap in the framework's cosmology stack.

/-- The energy kernel is `−t` times the derivative of the pressure
kernel: `t/(eᵗ−1) = −t·(d/dt) ln Z_B`.  Pressure kernel in, energy kernel
out — no independent input. -/
theorem boseEnergyKernel_from_logKernel {t : ℝ} (ht : 0 < t) :
    boseEnergyKernel t = -t * deriv boseLogKernel t := by
  rw [(boseLogKernel_hasDerivAt ht).deriv, boseEnergyKernel_eq_occupation ht]
  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

/-- **Bose partition function** (geometric series): for `t > 0`,
`Z_B(t) = (1 − e^{−t})⁻¹`. -/
theorem bosePartition_eq {t : ℝ} (ht : 0 < t) :
    bosePartition t = (1 - Real.exp (-t))⁻¹ := by
  unfold bosePartition
  simp only [boltzmannWeight_pow]
  exact tsum_geometric_of_lt_one (le_of_lt (Real.exp_pos _))
    (exp_neg_lt_one ht)

/-- **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 e^−βE is derived, not assumed. The Pauli exclusion principle is derived from the framework's cost certificate in this module. The theorem introduces new physics beyond the standard grand-canonical formalism.

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: