`Index`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.PeriodicTable on GitHub at line 247.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 244
 245/-! ## Minimal indexing scaffold -/
 246
 247structure Index where
 248  rail  : ℤ
 249  block : Block
 250  deriving Repr
 251
 252/- Placeholder indexer from atomic number (deterministic, no tuning). -/
 253def indexOf (Z : ℕ) : Index :=
 254  let period : ℕ := (Z - 1) / 8
 255  let pos    : ℕ := (Z - 1) % 8
 256  let b : Block :=
 257    match pos with
 258    | 0 | 1      => Block.s
 259    | 2 | 3 | 4  => Block.p
 260    | 5 | 6      => Block.d
 261    | _          => Block.f
 262  { rail := (period : ℤ), block := b }
 263
 264/- Dimensionless predicted band multiplier for atomic number `Z`. -/
 265def bandMultiplier (Z : ℕ) [BlockOffsets] : ℝ :=
 266  let idx := indexOf Z
 267  blockFactor idx.rail idx.block
 268
 269/-- Predicted (dimensionful) band energy for atomic number `Z`.
 270    This is a fit‑free display using the universal coherence tick. -/
 271def bandEnergy (Z : ℕ) [BlockOffsets] : ℝ :=
 272  IndisputableMonolith.Constants.E_coh * bandMultiplier Z
 273
 274/- Eight‑window neutrality predicate (rest if the sum is zero in aligned windows).
 275     In practice, the neutrality test is applied to a fit‑free valence‑cost proxy. -/
 276def neutralAt (f : ℕ → ℝ) (Z0 : ℕ) : Prop :=
 277  window8Sum f Z0 = 0

papers checked against this theorem

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