theorem proved term proof

`twoLevel_gt_one`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 157theorem twoLevel_gt_one (epsilon : ℝ) (T : ℝ) (hT : T > 0) :
 158    twoLevelPartition epsilon T hT > 1 := by

proof body

Term-mode proof.

 159  unfold twoLevelPartition
 160  have h : exp (-beta T hT * epsilon) > 0 := exp_pos _
 161  linarith
 162
 163/-- At ε = 0, Z = 2 (two degenerate levels). -/

depends on (8)

Lean names referenced from this declaration's body.

T in IndisputableMonolith.Foundation.Breath1024 decl_use
T in IndisputableMonolith.Gap45.SyncMinimization decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use
beta in IndisputableMonolith.Relativity.ILG.PPN decl_use
beta in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use
twoLevelPartition in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use