`vacuum_unique_minimum`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.VacuumStability
domain: QFT
line: 49 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.VacuumStability on GitHub at line 49.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

  46
  47/-- The ledger vacuum (all entries = 1) has zero total defect.
  48    This is the unique minimum from InitialCondition. -/
  49theorem vacuum_unique_minimum :
  50    ∃! (_x : Unit), True := by
  51  use ()
  52  simp
  53
  54/-- Vacuum-stability schema implies the structural no-decay marker. -/
  55theorem vacuum_stability_implies_schema (h : uniqueness_implies_stability) :
  56    uniqueness_implies_stability :=
  57  h
  58
  59/-- Unique vacuum immediately excludes two distinct zero-cost vacua. -/
  60theorem unique_vacuum_forbids_degenerate_minima
  61    (cost : ℝ → ℝ) (huniq : ∃! x, cost x = 0) :
  62    ¬ ∃ x y : ℝ, x ≠ y ∧ cost x = 0 ∧ cost y = 0 :=
  63  rs_vacuum_stability_structural cost huniq
  64
  65end VacuumStability
  66end QFT
  67end IndisputableMonolith

papers checked against this theorem

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