theorem proved term proof

`zero_point_energy`

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

formal statement (Lean)

  89theorem zero_point_energy (ω_c : ℝ) :
  90    landau_energy 0 ω_c = ω_c / 2 := by

proof body

Term-mode proof.

  91  unfold landau_energy
  92  ring
  93
  94/-! ## FQHE - Fractional Quantum Hall Effect -/
  95
  96/-- The Jain sequence of allowed FQHE fractions:
  97    ν = p/(2mp ± 1) for positive integers p, m.
  98    The denominator must be ODD (from Fermi statistics). -/

depends on (8)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
landau_energy in IndisputableMonolith.Physics.QuantumHallEffect decl_use