`first_shell_capacity`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.PauliExclusion on GitHub at line 109.

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

 106def shellCapacity (n : ℕ) : ℕ := 2 * n^2
 107
 108/-- **THEOREM**: First shell (n=1) holds 2 electrons. -/
 109theorem first_shell_capacity : shellCapacity 1 = 2 := rfl
 110
 111/-- **THEOREM**: Second shell (n=2) holds 8 electrons. -/
 112theorem second_shell_capacity : shellCapacity 2 = 8 := rfl
 113
 114/-- **THEOREM**: Third shell (n=3) holds 18 electrons. -/
 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

papers checked against this theorem

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