module module high

`IndisputableMonolith.Chemistry.PeriodicTable`

This module supplies the Recognition Science periodic table scaffolding via phi-ladder rails and eight-tick shell closures. It defines block offsets, rail multipliers, shell capacities, and noble-gas Z values that anchor all downstream chemistry predictions. The module is purely definitional and contains no theorems. Researchers deriving ionization energies, atomic radii, or electronegativities from RS cite these objects to fix the phi-based period and block structure.

claimThe module defines block offsets $B(s)=0$, $B(p)=1$, $B(d)=2$, $B(f)=3$ together with the rail multiplier $E_n/E_0 = φ^{2n}$ for shell rail $n$, shell capacities, cumulative closures, and noble-gas atomic numbers $Z$ derived from the eight-tick window.

background

Recognition Science places chemical structure on the phi-ladder of energy rails whose spacing is fixed by the eight-tick octave (T7) and the window-neutrality constraint. The module imports the base time quantum τ₀ = 1 tick from Constants and the eight-tick neutrality axiom from Measurement.WindowNeutrality, which states that the window-8 neutrality constraints uniquely determine the gap weight w₈. Key objects are BlockOffsets (default instance with s=0, p=1, d=2, f=3 and no per-element tuning) and railFactor (dimensionless multiplier φ^{2n} at rail n).

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds AtomicRadii (CH-007), ElectronAffinity (CH-006), Electronegativity (CH-008), IonizationEnergy (P0-A2), IonicBond (CH-010), and the remaining chemistry modules by supplying the shared phi-ladder and block structure. It realizes the eight-tick octave and closure-driven sawtooth patterns required for RS chemical predictions.

scope and limits

Does not incorporate per-element empirical tuning beyond the default block offsets.
Does not compute numerical values for any chemical observable.
Does not address relativistic corrections or explicit wavefunctions.
Does not derive molecular geometries or bonding energies.

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