`four_charges`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.NoetherTheoremDeep on GitHub at line 42.

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

  39def noether_charge_count : ℕ := D + 1
  40
  41/-- `noether_charge_count = 4`. -/
  42theorem four_charges : noether_charge_count = 4 := by unfold noether_charge_count D; norm_num
  43
  44/-- Energy conservation: energy = recognition budget integral. -/
  45def energy_RS (r : ℝ) : ℝ := Jcost r
  46
  47/-- Energy ≥ 0. -/
  48theorem energy_nonneg (r : ℝ) (hr : 0 < r) : 0 ≤ energy_RS r :=
  49  Jcost_nonneg hr
  50
  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.