defect_pos_of_ne_one
plain-language theorem explainer
For any positive real x different from 1, the defect functional is strictly positive. Researchers formalizing determinism and entropy in Recognition Science cite this to separate unity from all other states. The short proof obtains non-negativity from defect_nonneg, rules out equality to zero via defect_zero_iff_one, and concludes strict inequality with lt_of_le_of_ne.
Claim. If $x > 0$ and $x ≠ 1$, then defect$(x) > 0$, where defect$(x) := J(x)$ and $J(x) = (x + x^{-1})/2 - 1$.
background
The defect functional equals the J-cost: defect(x) := J(x) for x real and positive. The module formalizes the Law of Existence as x exists if and only if defect(x) = 0, with unity as the unique point of zero defect. Upstream results supply defect_nonneg (defect ≥ 0 for x > 0) and defect_zero_iff_one (defect(x) = 0 ↔ x = 1).
proof idea
Apply defect_nonneg to obtain defect(x) ≥ 0. Use defect_zero_iff_one to derive that defect(x) = 0 would force x = 1, contradicting the hypothesis x ≠ 1, so defect(x) ≠ 0. Combine the two facts with lt_of_le_of_ne to reach strict positivity.
why it matters
The result is invoked directly in determinism_resolution to establish that every non-unity state carries positive J-cost, yielding the unique minimizer at unity. It likewise feeds nonunity_positive_entropy and better_action_exists. The lemma closes the step that only unity collapses defect, consistent with J-uniqueness in the forcing chain and the claim that existence is equivalent to defect zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.