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

block_capacity

show as:
view Lean formalization →

block_capacity supplies the dimensionless capacity of the n-th shell as phi to the power 2n in the periodic table proxy. Recognition Science chemists cite it when scaling shell energies via the E_coh factor. The implementation is a direct one-line power expression drawn from the imported Constants bundle.

claimThe capacity of the n-th shell is $C(n) = phi^{2n}$, where $phi$ is the self-similar fixed point supplied by the Constants structure.

background

The PeriodicBlocks module models periodic table block structure via phi-packing of orbitals. The module documentation states: 'We model a dimensionless capacity φ^(2n) for the n-th shell and an energy-like shell scale E_coh * φ^(2n), yielding a direct identity used by certificates and reports.' This depends on the Constants structure from LawOfExistence, an abstract bundle containing phi along with other CPM constants such as Knet.

proof idea

This is a one-line definition that directly assigns block_capacity n to Constants.phi raised to the power of 2 times n.

why it matters in Recognition Science

The definition supplies the capacity factor invoked by the shell definition and the blocks_holds theorem, which states shell n equals E_coh times block_capacity n. It realizes the phi-packing proxy for orbital capacities, linking to the self-similar fixed point phi from the unified forcing chain in the Recognition framework.

scope and limits

formal statement (Lean)

  15noncomputable def block_capacity (n : Nat) : ℝ := Constants.phi ^ (2 * n)

proof body

Definition body.

  16

used by (2)

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

depends on (1)

Lean names referenced from this declaration's body.