theorem proved term proof

`high_temp_value`

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

formal statement (Lean)

 266theorem high_temp_value (gap : ℝ) :
 267    groundStateProb gap 0 = 0.5 := by

proof body

Term-mode proof.

 268  unfold groundStateProb
 269  simp
 270  norm_num
 271
 272/-- **THEOREM**: At high temperature (small β), states are equally populated.
 273    Proof: groundStateProb is continuous and groundStateProb(0) = 0.5.
 274
 275    The rigorous proof uses continuity of the composition of continuous functions. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

high_temp_limit in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use
groundStateProb in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
temperature in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use