`fourth_shell_capacity`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.PauliExclusion on GitHub at line 118.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 115theorem third_shell_capacity : shellCapacity 3 = 18 := rfl
 116
 117/-- **THEOREM**: Fourth shell (n=4) holds 32 electrons. -/
 118theorem fourth_shell_capacity : shellCapacity 4 = 32 := rfl
 119
 120/-! ## Noble Gas Configurations -/
 121
 122/-- Noble gas electron counts (cumulative filled shells). -/
 123def nobleGasElectrons : List ℕ := [2, 10, 18, 36, 54, 86]
 124
 125/-- **THEOREM**: Helium has 2 electrons (1s²). -/
 126theorem helium_electrons : nobleGasElectrons[0]! = 2 := rfl
 127
 128/-- **THEOREM**: Neon has 10 electrons (1s² 2s² 2p⁶). -/
 129theorem neon_electrons : nobleGasElectrons[1]! = 10 := rfl
 130
 131/-- **THEOREM**: Argon has 18 electrons. -/
 132theorem argon_electrons : nobleGasElectrons[2]! = 18 := rfl
 133
 134/-- **THEOREM**: Shell filling follows 2n² pattern. -/
 135theorem shell_filling_pattern :
 136    shellCapacity 1 + shellCapacity 2 = 10 ∧
 137    shellCapacity 1 + shellCapacity 2 + shellCapacity 3 = 28 := by
 138  constructor <;> rfl
 139
 140/-! ## Degeneracy Pressure -/
 141
 142/-- Fermi energy scale factor. For non-relativistic fermions,
 143    E_F ∝ n^(2/3) where n is number density. -/
 144def fermiEnergyExponent : ℚ := 2/3
 145
 146/-- Degeneracy pressure exponent. P ∝ n^(5/3) for non-relativistic. -/
 147def degeneracyPressureExponent : ℚ := 5/3
 148

papers checked against this theorem

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