shell
plain-language theorem explainer
shell(n) multiplies the coherence energy constant by the phi-powered block capacity at level n. Chemists using Recognition Science models cite this when scaling atomic radii or electron affinities from the phi-ladder. The definition is a direct algebraic composition with the block_capacity function and requires no lemmas.
Claim. Let $E_{coh}$ be the coherence energy. The shell scale at level $n$ is $s(n) := E_{coh} · ϕ^{2n}$.
background
The PeriodicBlocks module models the periodic table via phi-packing of orbitals. block_capacity sets the dimensionless capacity of the n-th shell to phi raised to 2n. shell then scales this capacity by the coherence energy drawn from the Constants structure in LawOfExistence, which bundles Knet, Cproj, Ceng, Cdisp and related nonnegativity conditions.
proof idea
The declaration is a direct definition that multiplies Constants.E_coh by the result of block_capacity n. It is a one-line wrapper that applies the block_capacity definition with no tactics or additional lemmas.
why it matters
This supplies the shell scale used by shellNumber, screeningFactor, and normalizedRadius in AtomicRadii plus eaProxy and distToClosure in ElectronAffinity. It fills the energy-scale slot in the phi-based periodic table proxy, consistent with the T7 eight-tick octave and the phi-ladder mass formula. It closes part of the scaffolding for chemical predictions inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.