defect_nonneg
plain-language theorem explainer
Defect(x) is non-negative for every positive real x. Researchers citing the discreteness forcing principle or economic inevitability theorems in Recognition Science invoke this result to establish the cost lower bound. The proof unfolds the defect definition, rewrites the expression as a scaled square term via field simplification, and concludes non-negativity by direct positivity.
Claim. $J(x) = J(x) = 0$ for all $x > 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
Defect is the J-cost functional restricted to positive reals, with upstream definition defect x := J x where J(x) = (x + x^{-1})/2 - 1. The module formalizes the Law of Existence as the equivalence between existence and zero defect, with key results including defect zero iff x equals one and the unique minimizer at unity. The and theorem from CirclePhaseLift supplies angular bounds in related contexts but is not required for this non-negativity step.
proof idea
The tactic proof first simplifies defect and J by definition, introduces the auxiliary fact that x is nonzero, establishes non-negativity of (x-1)^2 / x by positivity, then applies a calc block to equate the original expression to half that term and finishes with positivity.
why it matters
This supplies the non-negativity clause required by the discreteness forcing principle, which uses it to show J forces discrete ontology through its unique minimum at x=1. It is also invoked directly in economic_inevitability, total_defect_nonneg, zero_defect_iff_unity, and nonunity_positive_entropy. The result anchors the J-uniqueness step (T5) in the forcing chain and the cost non-negativity that drives the eight-tick octave and D=3 emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.