`shellCapacity`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.PauliExclusion on GitHub at line 106.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 103
 104/-- Number of states in a shell with principal quantum number n.
 105    Formula: 2n² -/
 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 ∧

papers checked against this theorem

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