theorem proved term proof

`RK_positive`

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

formal statement (Lean)

  71theorem RK_positive : 0 < von_klitzing_constant := by norm_num

proof body

Term-mode proof.

  72
  73/-! ## Landau Levels -/
  74
  75/-- **LANDAU QUANTIZATION**: E_n = ℏω_c(n + 1/2)
  76    The factor 1/2 is the zero-point energy of spin-1/2 fermions.
  77    In RS: the 1/2 comes from the 4-tick (half-period) fermionic phase. -/

depends on (20)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
period in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
von_klitzing_constant in IndisputableMonolith.Physics.QuantumHallEffect decl_use
half in IndisputableMonolith.QFT.SpinStatistics decl_use
half in IndisputableMonolith.RecogSpec.Core decl_use
half in IndisputableMonolith.Support.RungFractions decl_use