def definition def or abbrev

`radiusProxy`

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

formal statement (Lean)

  48def radiusProxy (Z : ℕ) : ℝ :=

proof body

Definition body.

  49  shellRadiusProxy Z * screeningFactor Z
  50
  51/-- Normalized atomic radius (0 to 1 within period).
  52    0 = smallest in period, 1 = largest. -/

depends on (6)

Lean names referenced from this declaration's body.

period in IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS decl_use
screeningFactor in IndisputableMonolith.Chemistry.AtomicRadii decl_use
shellRadiusProxy in IndisputableMonolith.Chemistry.AtomicRadii decl_use
radius in IndisputableMonolith.Complexity.CellularAutomata decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use