Cosmology Statistics Kernels Fermi Log Kernel Eq Log Partition

The Fermi log kernel from the partition function

In statistical mechanics, the Fermi pressure kernel is the function ln(1 + e^−t), with t a dimensionless ratio of energy to temperature. It appears in the pressure of a gas of fermions, particles that obey the Pauli exclusion principle, meaning at most one particle can occupy a given quantum state. The kernel is a standard ingredient in textbooks, usually introduced as a definition.

The machine-checked library of formal theorems in Recognition Science proves that this kernel is not a free input. The theorem fermiLogKernel_eq_log_partition establishes that ln(1 + e^−t) equals the natural logarithm of the partition function for a single mode at zero chemical potential. That partition function is the sum Z = 1 + e^−t, which arises from the two allowed occupancies, n = 0 and n = 1, each weighted by the Gibbs factor e^−n·t. The logarithm of this sum is exactly the pressure kernel.

This derivation starts from a single-mode grand partition function, Z_mode = Σ_n e^−n·E/T, where the sum runs over allowed occupancies. For fermions, the occupancy set is {0, 1}. The only inputs are the Gibbs weight e^−n·t and the Pauli exclusion principle, which restricts the occupancy set. From these, the framework derives the partition function, then the log kernel, then the occupation number 1/(e^t + 1), and then the energy kernel t/(e^t + 1) as t times the occupation number.

The framework also proves thermodynamic consistency. The derivative of the log kernel with respect to t gives minus the occupation number, and in physical variables the mean energy per mode equals −∂_β ln Z. The pressure and energy kernels are therefore derivative-related, exactly as the grand-canonical formalism demands. A capstone theorem shows the plasma pressure computed from the partition function matches the previously defined plasma pressure.

Within Recognition Science, this means the Fermi pressure kernel is a consequence of the partition function, not an independent assumption. The Gibbs weight itself and the occupancy set remain models, not theorems. The bridge from the framework's own exclusion principle, formalized as a J-cost statement, to the occupancy set {0, 1} used here remains open.

/-- **THEOREM: the Fermi pressure kernel is the log partition function.**
`ln(1+e^{−t}) = ln Z_F(t)`. -/
theorem fermiLogKernel_eq_log_partition (t : ℝ) :
    fermiLogKernel t = Real.log (fermiPartition t) := by
  rw [fermiPartition_eq]
  rfl

/-- **Fermi partition function** (two occupancy states):
`Z_F(t) = 1 + e^{−t}`, for every `t`. -/
theorem fermiPartition_eq (t : ℝ) :
    fermiPartition t = 1 + Real.exp (-t) := by
  unfold fermiPartition boltzmannWeight
  simp [Finset.sum_range_succ]

/-- **THEOREM (grand-canonical consistency, Fermi).**
`d/dt[ln(1+e^{−t})] = −⟨n⟩_F(t)`, for every `t`. -/
theorem fermiLogKernel_hasDerivAt (t : ℝ) :
    HasDerivAt fermiLogKernel (-(fermiOccupation 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).add h2
  have hpos : (0 : ℝ) < 1 + Real.exp (-t) := by positivity
  have h4 := h3.log (ne_of_gt hpos)
  have heq : (0 + Real.exp (-t) * (-1)) / (1 + Real.exp (-t))
      = -(fermiOccupation t) := by
    rw [fermiOccupation_eq]
    have hy0 : Real.exp t ≠ 0 := ne_of_gt (Real.exp_pos t)
    rw [Real.exp_neg]
    rw [Real.exp_neg] at hpos
    field_simp
    ring
  rw [← heq]
  exact h4

/-- **THEOREM (textbook form, Fermi).**  `−∂_β ln Z_F(βE) = E·⟨n⟩_F(βE)`. -/
theorem mode_energy_fermi (E : ℝ) {β : ℝ} :
    HasDerivAt (fun b => Real.log (fermiPartition (b * E)))
      (-(E * fermiOccupation (β * E))) β := by
  have h1 : HasDerivAt (fun b : ℝ => b * E) E β := by
    simpa using (hasDerivAt_id β).mul_const E
  have h2 := (fermiLogKernel_hasDerivAt (β * E)).comp β h1
  have h3 : HasDerivAt (fun b => fermiLogKernel (b * E))
      (-(E * fermiOccupation (β * E))) β := by
    convert h2 using 1
    ring
  apply h3.congr_of_eventuallyEq
  filter_upwards [Filter.univ_mem] with b _
  exact (fermiLogKernel_eq_log_partition (b * E)).symm

/-- **CAPSTONE (pressure).**  The plasma pressure of the η_B chain equals
the phase-space integral of `T·ln Z_mode(E/T)` — the grand-canonical
pressure `P = (T/V)·ln Z` — with `Z_B = Σ_{n∈ℕ} e^{−nE/T}` and
`Z_F = Σ_{n∈{0,1}} e^{−nE/T}`.  The log kernels are gone as inputs; only
the Gibbs weight and the occupancy sets remain. -/
theorem plasmaPressure_from_partitionFunction (gB gF : ℝ) {T : ℝ}
    (hT : 0 < T) :
    phaseSpaceDensity 3 gB T (fun t => Real.log (bosePartition t))
      + phaseSpaceDensity 3 gF T (fun t => Real.log (fermiPartition t))
      = GrandPotential.plasmaPressure gB gF T := by
  have hB := phaseSpaceDensity_congr_pos gB T hT
    (fun t => Real.log (bosePartition t)) boseLogKernel
    (fun t ht => (boseLogKernel_eq_log_partition ht).symm)
  have hF := phaseSpaceDensity_congr_pos gF T hT
    (fun t => Real.log (fermiPartition t)) fermiLogKernel
    (fun t _ => (fermiLogKernel_eq_log_partition t).symm)
  rw [hB, hF]
  exact PhaseSpaceReduction.plasmaPressure_from_phaseSpace gB gF hT

What this page does not claim

The Gibbs weight e^−βE itself is not derived, it is a model input. The occupancy set {0, 1} for fermions is not derived from the framework's exclusion principle, that bridge remains open. The theorem does not establish the Fermi pressure kernel for nonzero chemical potential.

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: