`second_shell_capacity`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.PauliExclusion
domain: QFT
line: 112 · 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 112.

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

formal source

 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
 140/-! ## Degeneracy Pressure -/
 141
 142/-- Fermi energy scale factor. For non-relativistic fermions,

papers checked against this theorem

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