pith. machine review for the scientific record. sign in
theorem

determinism_resolution

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.Determinism
domain
Foundation
line
128 · github
papers citing
none yet

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

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

open explainer

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