No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
108theorem oganesson_full_shell : valenceElectrons 118 = periodLength 118 := by native_decide
proof body
Term-mode proof.
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 -/
depends on (9)
Lean names referenced from this declaration's body.
-
periodLength
in IndisputableMonolith.Chemistry.PeriodicTable
decl_use
-
valenceElectrons
in IndisputableMonolith.Chemistry.PeriodicTable
decl_use
-
radius
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
Z
in IndisputableMonolith.Masses.Anchor
decl_use
-
F
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
Z
in IndisputableMonolith.Physics.AnchorPolicyCertified
decl_use
-
F
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
F
in IndisputableMonolith.Pipelines
decl_use