theorem
proved
no_information_sink
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Relativity.InformationConservation on GitHub at line 49.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
46
47/-- In LawOfExistence / LogicFromCost, the zero-defect state (x=1) is
48 the unique minimum. States evolve; they don't "disappear." -/
49theorem no_information_sink : ledger_conservative := information_conserved
50
51/-- Information-conservation structure implies no-information-sink structure. -/
52theorem information_conserved_implies_no_sink (h : ledger_conservative) :
53 ledger_conservative :=
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