zero_point_energy
plain-language theorem explainer
Zero-point energy for the lowest Landau level equals half the cyclotron frequency in units with ħ set to one. Researchers deriving the integer quantum Hall spectrum from Recognition Science ledger topology would cite this identity when fixing the ground-state offset. The argument reduces to unfolding the energy definition and applying ring simplification to cancel all other terms.
Claim. The energy of the zeroth Landau level at cyclotron frequency $ω_c$ equals $ω_c/2$.
background
The module derives the quantum Hall effect from the Recognition Science topological ledger, where the integer quantum Hall conductance arises as a Chern number invariant of occupied Landau levels and the fractional case follows from composite fermions under eight-tick balance. Landau energy is defined in the sibling declaration landau_energy; the present theorem isolates the n=0 case. Upstream structures supply the J-cost calibration (PhiForcingDerived), the spectral emergence of SU(3)×SU(2)×U(1) content (SpectralEmergence), and the ledger factorization that fixes the half-period fermionic contribution.
proof idea
The proof is a one-line wrapper: unfold landau_energy followed by the ring tactic, which algebraically reduces the expression for the n=0 level to the required half-frequency term.
why it matters
This identity supplies the zero-point offset required for the Landau level ladder that underlies the module's quantized Hall conductance results. It draws on the eight-tick octave (T7) that enforces the fermionic half-period shift and feeds the Chern-number integer theorem listed in the module documentation. The companion paper RS_Quantum_Hall_Effect.tex uses the same offset to obtain σ_xy = n e²/h.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.