module module high

`IndisputableMonolith.Chemistry.PeriodicTable`

The PeriodicTable module supplies RS-native definitions for chemical blocks, shell rails, and period structure using eight-tick neutrality and phi scaling. Chemists deriving ionization energies or electronegativities from the phi-ladder cite it as the shared foundation. It consists entirely of definitions and a default BlockOffsets instance with fixed s/p/d/f offsets and no per-element tuning.

claimBlockOffsets with default values $s=0$, $p=1$, $d=2$, $f=3$; rail multiplier at rail $n$ given by $\phi^{2n}$; periodOf and cumulativeShellClosure defined via nobleGasZ and shellCapacity.

background

The module sits inside the Chemistry domain and imports Constants (where $\tau_0=1$ tick) together with WindowNeutrality, whose doc-comment states that eight-tick neutrality constraints uniquely determine the gap weight $w_8$ appearing in the $\alpha^{-1}$ derivation. It introduces BlockOffsets as a type class whose default instance encodes the standard s/p/d/f packing offsets, railFactor as the dimensionless shell-rail multiplier $\phi^{2n}$, and auxiliary functions such as nobleGasZ, shellCapacity, and periodOf that locate elements on the phi-ladder.

These definitions rest on the eight-tick octave (T7) and the Recognition Composition Law, supplying the structural scaffolding that later modules use to predict sawtooth patterns in ionization energy and approach-to-closure behavior in electron affinity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the parent derivations in AtomicRadii (CH-007), IonizationEnergy (P0-A2), ElectronAffinity (CH-006), Electronegativity (CH-008), IonicBond (CH-010), Ferromagnetism (CM-010), MetallicBond, and VanDerWaals. Its BlockOffsets and railFactor definitions supply the fixed phi-packing offsets and $\phi^{2n}$ energy scaling that those modules invoke to obtain period and group trends without additional hypotheses.

scope and limits

Does not supply per-element tuning parameters beyond the default BlockOffsets instance.
Does not compute numerical radii or energies; those appear only in downstream modules.
Does not derive the eight-tick neutrality axiom itself; that is imported from WindowNeutrality.
Does not address relativistic corrections or fine-structure effects.

used by (8)

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

IndisputableMonolith.Chemistry.AtomicRadii module_import
IndisputableMonolith.Chemistry.ElectronAffinity module_import
IndisputableMonolith.Chemistry.Electronegativity module_import
IndisputableMonolith.Chemistry.Ferromagnetism module_import
IndisputableMonolith.Chemistry.IonicBond module_import
IndisputableMonolith.Chemistry.IonizationEnergy module_import
IndisputableMonolith.Chemistry.MetallicBond module_import
IndisputableMonolith.Chemistry.VanDerWaals module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Measurement.WindowNeutrality module_import

declarations in this module (39)

inductive Block L38
class BlockOffsets L41
def default L46
def railFactor L61
def blockFactor L66
def railEnergy L71
def window8Sum L75
def nobleGasZ L85
def nobleGasZFull L88
def shellCapacity L94
def cumulativeShellClosure L106
def periodOf L116
def prevClosure L126
def nextClosure L136
def distToNextClosure L147
def valenceElectrons L152
def periodLength L155
def signedValenceCost L162
def isNobleGas L168
theorem helium_is_noble L177
theorem neon_is_noble L180
theorem argon_is_noble L183
theorem krypton_is_noble L186
theorem xenon_is_noble L189
theorem radon_is_noble L192
theorem noble_gas_at_closure L195
theorem noble_gas_complete_shell L201
theorem cumulative_closure_eq_noble L208
theorem shell_sum_to_noble L213
def periodLengths L221
theorem period_lengths_from_noble_gaps L224
def blockElectronCount L229
theorem block_count_formula L236
structure Index L247
def indexOf L253
def bandMultiplier L265
def bandEnergy L271
def neutralAt L276
theorem neutralAt_const_zero L280