pith. sign in
module module moderate

IndisputableMonolith.Chemistry.PeriodicTableFromPhiLadder

show as:
view Lean formalization →

The module derives periodic table shell capacities from the phi-ladder in Recognition Science. It supplies the standard 2n² formula together with supporting definitions and a certification object. Physicists tracing chemistry to the J-uniqueness and eight-tick octave would cite the module. The module is built from sibling definitions and one certification theorem.

claimElectron shell capacities equal $2n^2$ for principal quantum number $n$, obtained from the phi-ladder.

background

Recognition Science obtains all structure from the forcing chain T0-T8, with T6 fixing phi as the self-similar point and T7 imposing the eight-tick octave. The module sits inside the Chemistry domain and introduces ElectronBlock, shellCapacity, and PeriodicTableCert. It imports only Mathlib and states the classical shell rule as its central object.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the chemical periodicity layer that PeriodicTableCert certifies and that later feeds mass-ladder and alpha-band results. It closes the link between the phi-ladder (T6) and observable shell structure.

scope and limits

declarations in this module (9)