def
definition
block_capacity
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Chemistry.PeriodicBlocks on GitHub at line 15.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
12namespace IndisputableMonolith
13namespace Chemistry
14
15noncomputable def block_capacity (n : Nat) : ℝ := Constants.phi ^ (2 * n)
16
17noncomputable def shell (n : Nat) : ℝ := Constants.E_coh * block_capacity n
18
19/-- Identity: shell scale equals `E_coh` times capacity at each n. -/
20@[simp] theorem blocks_holds (n : Nat) : shell n = Constants.E_coh * block_capacity n := by
21 rfl
22
23end Chemistry
24end IndisputableMonolith
25
26