`NoetherTheoremDeepCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.NoetherTheoremDeep
domain: Foundation
line: 54 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.NoetherTheoremDeep on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  51/-- Energy = 0 at equilibrium (ground state). -/
  52theorem energy_zero_at_eq : energy_RS 1 = 0 := Jcost_unit0
  53
  54structure NoetherTheoremDeepCert where
  55  four_charges : noether_charge_count = 4
  56  energy_nonneg : ∀ r : ℝ, 0 < r → 0 ≤ energy_RS r
  57  energy_zero_at_eq : energy_RS 1 = 0
  58
  59noncomputable def noetherTheoremDeepCert : NoetherTheoremDeepCert where
  60  four_charges := four_charges
  61  energy_nonneg := energy_nonneg
  62  energy_zero_at_eq := energy_zero_at_eq
  63
  64theorem noetherTheoremDeepCert_inhabited : Nonempty NoetherTheoremDeepCert :=
  65  ⟨noetherTheoremDeepCert⟩
  66
  67end
  68end NoetherTheoremDeep
  69end Foundation
  70end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.