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

information_conserved_implies_no_distinct_zero_defect

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)

  57theorem information_conserved_implies_no_distinct_zero_defect
  58    (h : ledger_conservative) :
  59    ¬ ∃ x y : ℝ,
  60      x ≠ y ∧
  61      0 < x ∧
  62      0 < y ∧
  63      Foundation.LawOfExistence.defect x = 0 ∧
  64      Foundation.LawOfExistence.defect y = 0 := by

proof body

Term-mode proof.

  65  rcases h with ⟨x0, hx0, hx0_unique⟩
  66  intro hxy
  67  rcases hxy with ⟨x, y, hne, hxpos, hypos, hx, hy⟩
  68  have hx_eq : x = x0 := hx0_unique x ⟨hxpos, hx⟩
  69  have hy_eq : y = x0 := hx0_unique y ⟨hypos, hy⟩
  70  exact hne (hx_eq.trans hy_eq.symm)
  71
  72end InformationConservation
  73end Relativity
  74end IndisputableMonolith

depends on (2)

Lean names referenced from this declaration's body.