theorem
proved
shellCapacity_4
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder on GitHub at line 41.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
38theorem shellCapacity_1 : shellCapacity 1 = 2 := by decide
39theorem shellCapacity_2 : shellCapacity 2 = 8 := by decide
40theorem shellCapacity_3 : shellCapacity 3 = 18 := by decide
41theorem shellCapacity_4 : shellCapacity 4 = 32 := by decide
42
43structure PeriodicTableCert where
44 five_blocks : Fintype.card ElectronBlock = 5
45 s1_cap : shellCapacity 1 = 2
46 s2_cap : shellCapacity 2 = 8
47 s3_cap : shellCapacity 3 = 18
48 s4_cap : shellCapacity 4 = 32
49
50def periodicTableCert : PeriodicTableCert where
51 five_blocks := electronBlockCount
52 s1_cap := shellCapacity_1
53 s2_cap := shellCapacity_2
54 s3_cap := shellCapacity_3
55 s4_cap := shellCapacity_4
56
57end IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder