oganesson_full_shell

formal source

 105theorem krypton_full_shell : valenceElectrons 36 = periodLength 36 := by native_decide
 106theorem xenon_full_shell : valenceElectrons 54 = periodLength 54 := by native_decide
 107theorem radon_full_shell : valenceElectrons 86 = periodLength 86 := by native_decide
 108theorem oganesson_full_shell : valenceElectrons 118 = periodLength 118 := by native_decide
 109
 110/-! ## Ordering Lemmas -/
 111
 112/-- Li (Z=3) has larger radius than F (Z=9) in Period 2.
 113    Li: (1 - (3-2)/(10-2)) = 7/8
 114    F:  (1 - (9-2)/(10-2)) = 1/8 -/
 115theorem li_larger_than_f : normalizedRadius 3 > normalizedRadius 9 := by
 116  simp only [normalizedRadius, prevClosure, nextClosure]
 117  norm_num
 118
 119/-- Na (Z=11) has larger radius than Cl (Z=17) in Period 3.
 120    Na: (1 - (11-10)/(18-10)) = 7/8
 121    Cl: (1 - (17-10)/(18-10)) = 1/8 -/
 122theorem na_larger_than_cl : normalizedRadius 11 > normalizedRadius 17 := by
 123  simp only [normalizedRadius, prevClosure, nextClosure]
 124  norm_num
 125
 126/-- K (Z=19) has larger shell number than Li (Z=3) due to more shells. -/
 127theorem k_larger_shell_than_li : shellNumber 19 > shellNumber 3 := by
 128  native_decide
 129
 130/-! ## Falsification Criteria
 131
 132The atomic radii derivation is falsifiable:
 133
 1341. **Period trend violation**: If radius increases across a period (same shell).
 135
 1362. **Group trend violation**: If radius decreases going down a group.
 137
 1383. **Alkali not maximum**: If alkali metal does NOT have maximum radius in period.