theorem proved term proof

`noble_gas_ea_zero`

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

formal statement (Lean)

  62theorem noble_gas_ea_zero (Z : ℕ) (h : isNobleGas Z) : eaProxy Z = 0 := by

proof body

Term-mode proof.

  63  simp only [eaProxy, distToClosure]
  64  exact noble_gas_at_closure Z h
  65
  66/-- Halogens have EA proxy = 1 (one electron completes shell). -/

depends on (11)

Lean names referenced from this declaration's body.

distToClosure in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
eaProxy in IndisputableMonolith.Chemistry.ElectronAffinity decl_use
shell in IndisputableMonolith.Chemistry.PeriodicBlocks decl_use
isNobleGas in IndisputableMonolith.Chemistry.PeriodicTable decl_use
noble_gas_at_closure in IndisputableMonolith.Chemistry.PeriodicTable decl_use
one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use