def definition def or abbrev

`screeningFactor`

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

formal statement (Lean)

  42def screeningFactor (Z : ℕ) : ℝ :=

proof body

Definition body.

  43  if periodLength Z = 0 then 1
  44  else 1 - (valenceElectrons Z : ℝ) / (2 * periodLength Z : ℝ)
  45
  46/-- Atomic radius proxy: combines shell and screening effects.
  47    radius = shellRadius * screeningFactor -/

used by (1)

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

radiusProxy in IndisputableMonolith.Chemistry.AtomicRadii decl_use

depends on (8)

Lean names referenced from this declaration's body.

shell in IndisputableMonolith.Chemistry.PeriodicBlocks decl_use
periodLength in IndisputableMonolith.Chemistry.PeriodicTable decl_use
valenceElectrons in IndisputableMonolith.Chemistry.PeriodicTable decl_use
shellRadius in IndisputableMonolith.Chemistry.SolvationShellsFromConfigDim decl_use
radius in IndisputableMonolith.Complexity.CellularAutomata decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use