`default`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.PeriodicTable
domain: Chemistry
line: 46 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Chemistry.PeriodicTable on GitHub at line 46.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  43
  44namespace BlockOffsets
  45/- Default φ‑packing offsets (audit subject to change): s=0, p=1, d=2, f=3. -/
  46def default : BlockOffsets :=
  47  { offset := fun b =>
  48      match b with
  49      | Block.s => 0
  50      | Block.p => 1
  51      | Block.d => 2
  52      | Block.f => 3 }
  53end BlockOffsets
  54
  55noncomputable section
  56
  57/-- Default instance: s=0, p=1, d=2, f=3 (no per‑element tuning). -/
  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))

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.