`QuantumState`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.PauliExclusion
domain: QFT
line: 64 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.PauliExclusion on GitHub at line 64.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  61/-! ## Quantum State Structure -/
  62
  63/-- A quantum state characterized by quantum numbers (n, l, m, ms). -/
  64structure QuantumState where
  65  /-- Principal quantum number (energy level). -/
  66  n : ℕ
  67  /-- Orbital angular momentum quantum number. -/
  68  l : ℕ
  69  /-- Magnetic quantum number. -/
  70  m : ℤ
  71  /-- Spin projection (±1 representing ±1/2). -/
  72  ms : Int
  73  /-- Validity: l < n. -/
  74  l_lt_n : l < n
  75  /-- Validity: |m| ≤ l. -/
  76  m_bound : m.natAbs ≤ l
  77  /-- Validity: ms = ±1. -/
  78  ms_valid : ms = 1 ∨ ms = -1
  79deriving DecidableEq
  80
  81/-! ## Atomic Shell Structure -/
  82
  83/-- Number of states in a subshell with angular momentum l.
  84    Formula: 2(2l+1) where factor 2 is for spin. -/
  85def subshellCapacity (l : ℕ) : ℕ := 2 * (2 * l + 1)
  86
  87/-- **THEOREM**: s-subshell (l=0) holds 2 electrons. -/
  88theorem s_subshell_capacity : subshellCapacity 0 = 2 := rfl
  89
  90/-- **THEOREM**: p-subshell (l=1) holds 6 electrons. -/
  91theorem p_subshell_capacity : subshellCapacity 1 = 6 := rfl
  92
  93/-- **THEOREM**: d-subshell (l=2) holds 10 electrons. -/
  94theorem d_subshell_capacity : subshellCapacity 2 = 10 := rfl

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.