pith. machine review for the scientific record. sign in
theorem proved decidable or rfl high

blocks_holds

show as:
view Lean formalization →

The theorem states that the shell energy scale equals E_coh multiplied by block capacity for every natural number n. Chemists using phi-packing proxies for periodic table blocks would cite this identity when building shell-energy certificates. The proof is a single reflexivity step because the shell definition is literally the product.

claimFor every natural number $n$, the shell scale satisfies $s(n) = E_coh · c(n)$, where the block capacity is defined by $c(n) = φ^{2n}$.

background

The module supplies a dimensionless proxy for periodic-table block structure based on phi-packing of orbitals. It introduces block_capacity(n) as the real number φ raised to 2n and shell(n) as E_coh times that capacity, yielding an energy-like quantity for each shell. The Constants structure imported from LawOfExistence supplies the coherence energy E_coh and the golden-ratio base φ.

proof idea

The proof is a one-line reflexivity wrapper. Because the definition of shell n is exactly Constants.E_coh multiplied by block_capacity n, the equality is immediate by unfolding the definition.

why it matters in Recognition Science

The identity closes the basic relation between shell scale and capacity inside the phi-packing model. It supplies the algebraic fact required by any certificate or report that treats shell energies as proportional to orbital capacities. The construction sits inside the Recognition Science use of phi as the self-similar fixed point and the eight-tick octave structure for discrete shells.

scope and limits

formal statement (Lean)

  20@[simp] theorem blocks_holds (n : Nat) : shell n = Constants.E_coh * block_capacity n := by

proof body

Decided by rfl or decide.

  21  rfl
  22
  23end Chemistry
  24end IndisputableMonolith
  25
  26

depends on (3)

Lean names referenced from this declaration's body.