def definition def or abbrev

`distToClosure`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  35def distToClosure (Z : ℕ) : ℕ := distToNextClosure Z

proof body

Definition body.

  36
  37/-- Electron affinity proxy: higher when closer to closure.
  38    EA_proxy = periodLength - valenceElectrons = distToClosure
  39    Halogens (dist=1) have highest proxy, noble gases (dist=0) have lowest. -/

used by (7)

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

ea_decreases_within_period in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
eaProxy in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
halogen_ea_one in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
halogenZ in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
isHalogen in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
noble_gas_ea_zero in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
normalizedEA in IndisputableMonolith.Chemistry.ElectronAffinity decl_use

depends on (5)

Lean names referenced from this declaration's body.

distToNextClosure in IndisputableMonolith.Chemistry.PeriodicTable decl_use
periodLength in IndisputableMonolith.Chemistry.PeriodicTable decl_use
valenceElectrons in IndisputableMonolith.Chemistry.PeriodicTable decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use