pith. machine review for the scientific record. sign in
def definition def or abbrev

signedValenceCost

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 162def signedValenceCost (Z : ℕ) : ℤ :=

proof body

Definition body.

 163  let v := valenceElectrons Z
 164  let periodLen := periodLength Z
 165  if 2 * v ≤ periodLen then (v : ℤ) else (v : ℤ) - (periodLen : ℤ)
 166
 167/-- Predicate: Z is a noble gas (shell closure point). -/

depends on (10)

Lean names referenced from this declaration's body.