theorem
proved
determinism_resolution
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.Determinism on GitHub at line 128.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
125 - Reality IS deterministic (unique cost minimizer)
126 - Observations APPEAR random (projection through finite resolution)
127 - Both sides of the debate are correct, about different things -/
128theorem determinism_resolution :
129 (∀ x : ℝ, 0 < x → x ≠ 1 → 0 < LawOfExistence.defect x) ∧
130 (∃! x : ℝ, 0 < x ∧ LawOfExistence.defect x = 0) := by
131 constructor
132 · intro x hx hne
133 exact LawOfExistence.defect_pos_of_ne_one hx hne
134 · exact ⟨1, ⟨by norm_num, LawOfExistence.defect_one⟩,
135 fun y ⟨hy_pos, hy_zero⟩ =>
136 (LawOfExistence.defect_zero_iff_one hy_pos).mp hy_zero⟩
137
138end Determinism
139end Foundation
140end IndisputableMonolith