Pith. sign in
module module high

IndisputableMonolith.Chemistry.PeriodicTable

show as:
view Lean formalization →

Defines the Recognition Science skeleton of the periodic table: shell rails scaled by φ^{2n}, fixed s/p/d/f block offsets, noble-gas Z closures, and period indexing. Downstream chemistry modules (ionization, radii, EN, EA, bonding) import these as the common Z-to-shell map. The module is definitional scaffolding plus small arithmetic lemmas, not a deep existence proof.

claimThe module fixes the RS periodic-table data: orbital blocks $s,p,d,f$ with default offsets $0,1,2,3$; dimensionless rail energies $E_n/E_{\mathrm{coh}}=\varphi^{2n}$; eight-tick window sums; noble-gas atomic numbers and cumulative shell capacities; and the map $Z\mapsto$ period and shell closure. No per-element free parameters.

background

Recognition Science ties atomic shell structure to the eight-tick octave (forcing chain T7) and the golden ratio $\varphi$ fixed at T6. Coherent energy sets the yardstick; shell rail $n$ carries a dimensionless multiplier $\varphi^{2n}$ so period trends are pure $\varphi$-ladder scalings rather than fitted Rydberg constants.

Blocks $s,p,d,f$ receive fixed packing offsets (default $0,1,2,3$) with no element-by-element tuning. Noble-gas $Z$ values and cumulative shell capacities encode the classical $2,8,18,32,\ldots$ closures as discrete ledger windows. Window neutrality (imported from Measurement.WindowNeutrality) supplies the eight-tick exactness that makes those closures privileged.

Constants supplies the RS-native $\varphi$ and tick structure used to write rail factors and energies without SI conversion at this layer.

proof idea

This is a definition module. It introduces inductive or enumerated types for blocks, a BlockOffsets structure with a default instance, and pure functions: rail and block factors, rail energy, window-8 sums, noble-gas $Z$ lists, shell capacity, cumulative closure, and periodOf. Supporting lemmas are arithmetic identities and table lookups, not analytic existence arguments. Downstream files consume the definitions directly.

why it matters in Recognition Science

Every listed chemistry derivation imports this module as the shared $Z$-to-shell geometry. IonizationEnergy (P0-A2) uses $\varphi^{2n}$ rails plus block offsets for the sawtooth $I_1(Z)$. ElectronAffinity (CH-006) and Electronegativity (CH-008) measure distance to the next noble-gas closure defined here. AtomicRadii (CH-007) reads period and block to get contraction and group trends. IonicBond (CH-010) and related bonding modules invoke eight-tick closure drive toward the noble-gas $Z$ table. Ferromagnetism, metallic bond, and van der Waals modules likewise sit on the same shell map. Without a single canonical periodic skeleton, those CH/CM claims would each re-encode shell arithmetic inconsistently.

scope and limits

used by (8)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (39)