defect_at_one
plain-language theorem explainer
The theorem establishes that the defect functional vanishes at the unit value. Researchers formalizing the Law of Existence would cite this when verifying that unity meets the zero-cost existence condition. The proof is a direct simplification that reduces the claim using the definitions of defect and the J-cost functional.
Claim. $J(1) = 0$, where the canonical cost functional is $J(x) = (x + x^{-1})/2 - 1$ and the defect functional coincides with $J$ for positive real arguments.
background
The defect functional is defined by defect(x) := J(x) for x > 0, with J the canonical cost functional J(x) = (x + x^{-1})/2 - 1. This module supplies a literal formalization of the Law of Existence as the equivalence between existence of x and defect(x) = 0. The upstream definition of defect as equal to J supplies the algebraic content used here.
proof idea
The proof is a one-line wrapper that applies the simp tactic with the definitions of defect and J, reducing the statement directly to the algebraic identity at unity.
why it matters
This base case feeds the complete Law of Existence theorem, the uniqueness of the existent, and the economic inevitability result that unity is the unique minimizer. It supplies the zero-defect anchor for the equivalence Exists x ↔ defect(x) = 0 ↔ x = 1. The result aligns with the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.