`information_conserved_implies_no_distinct_zero_defect`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.InformationConservation
domain: Relativity
line: 57 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.InformationConservation on GitHub at line 57.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

  54  h
  55
  56/-- Conserved-information structure forbids two distinct zero-defect minimizers. -/
  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
  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

papers checked against this theorem

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