determinism_resolution
plain-language theorem explainer
Determinism_resolution asserts that the defect functional is strictly positive for positive reals away from unity and possesses a unique positive root at x=1. Quantum foundations researchers cite it to ground the claim that J-cost dynamics are deterministic while observations appear random due to finite resolution. The proof splits the conjunction via constructor and directly applies the positivity and zero-characterization lemmas for defect.
Claim. Let $d(x) := J(x)$ for $x > 0$. Then $d(x) > 0$ whenever $x ≠ 1$, and there exists a unique $x > 0$ such that $d(x) = 0$.
background
The Foundation.Determinism module formalizes F-007 by establishing unique J-cost minimization at each ledger step. The defect functional is defined as defect(x) := J(x) for positive x, with upstream results showing defect(1) = 0, defect(x) > 0 for x > 0 and x ≠ 1, and the zero-characterization defect(x) = 0 ↔ x = 1. The module setting distinguishes deterministic underlying dynamics from coarse-grained projections that produce apparent randomness, with the Born rule emerging as the observer's view of the J-cost landscape.
proof idea
The term-mode proof opens with constructor to split the conjunction. The universal quantifier is discharged by applying defect_pos_of_ne_one to the assumptions 0 < x and x ≠ 1. The unique-existence conjunct is proved by exhibiting the witness x = 1 via defect_one and invoking defect_zero_iff_one to confirm no other positive root exists.
why it matters
This result supplies the unique-minimizer property used by information_conserved in Relativity.InformationConservation. It completes the F-007 registry item on determinism versus randomness, confirming that the J-cost function forces a single next state (T5 J-uniqueness). The theorem thereby supports the framework claim that apparent quantum randomness is an observer artifact rather than intrinsic to the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.