pith. machine review for the scientific record. sign in
def definition def or abbrev high

shell

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  17noncomputable def shell (n : Nat) : ℝ := Constants.E_coh * block_capacity n

proof body

Definition body.

  18
  19/-- Identity: shell scale equals `E_coh` times capacity at each n. -/

used by (30)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.