railFactor

formal source

  58instance : BlockOffsets := BlockOffsets.default
  59
  60/- Dimensionless shell rail multiplier (E_n/E_coh) at rail n: φ^{2n}. -/
  61def railFactor (n : ℤ) : ℝ :=
  62  Real.rpow IndisputableMonolith.Constants.phi ((2 : ℝ) * (n : ℝ))
  63
  64/- Predicted (dimensionless) band multiplier for block `b` on rail `n`.
  65     Uses fixed φ‑packing offsets from `BlockOffsets`. -/
  66def blockFactor (n : ℤ) (b : Block) [B : BlockOffsets] : ℝ :=
  67  let exp : ℝ := (2 : ℝ) * (n : ℝ) + (B.offset b : ℝ)
  68  Real.rpow IndisputableMonolith.Constants.phi exp
  69
  70/-- Rail energy (dimensionful): E_n = E_coh · φ^{2n}. -/
  71def railEnergy (n : ℤ) : ℝ :=
  72  IndisputableMonolith.Constants.E_coh * railFactor n
  73
  74/- Sliding 8‑window sum used for neutrality tests. -/
  75def window8Sum (f : ℕ → ℝ) (Z0 : ℕ) : ℝ :=
  76  (Finset.range 8).sum (fun k => f (Z0 + k))
  77
  78/-! ## Noble Gas Closure Infrastructure
  79
  80We define a valence proxy and prove that noble gases are exactly the
  818-window closure points.
  82-/
  83
  84/-- The canonical noble gas atomic numbers (first 6 periods + Oganesson). -/
  85def nobleGasZ : List ℕ := [2, 10, 18, 36, 54, 86]
  86
  87/-- Extended noble gas list including Oganesson (period 7). -/
  88def nobleGasZFull : List ℕ := [2, 10, 18, 36, 54, 86, 118]
  89
  90/-- Shell capacity sequence: {2, 8, 8, 18, 18, 32, 32, ...}
  91    Period n has capacity 2n² electrons, but fills in two sub-periods.