pith. machine review for the scientific record. sign in
theorem proved term proof

rs_vacuum_stability_structural

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)

  37theorem rs_vacuum_stability_structural : uniqueness_implies_stability := by

proof body

Term-mode proof.

  38  intro cost huniq hdeg
  39  rcases huniq with ⟨x0, hx0, hxuniq⟩
  40  rcases hdeg with ⟨x, y, hxy, hx, hy⟩
  41  have hxeq : x = x0 := hxuniq x hx
  42  have hyeq : y = x0 := hxuniq y hy
  43  exact hxy (hxeq.trans hyeq.symm)
  44
  45/-! ## Ledger Vacuum -/
  46
  47/-- The ledger vacuum (all entries = 1) has zero total defect.
  48    This is the unique minimum from InitialCondition. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.