defect_one
plain-language theorem explainer
The declaration establishes that the defect functional vanishes at unity. Researchers formalizing the Law of Existence cite it to anchor the equivalence between existence and zero defect. The proof is a direct term reference to the already-established defect_at_one result.
Claim. defect(1) = 0, where defect(x) := J(x) for x > 0.
background
In the Law of Existence module the defect functional is introduced by the definition defect(x) := J(x). The module states the core equivalence x exists iff defect(x) = 0 and lists the supporting theorems defect_zero_iff_one, law_of_existence, and unity_unique_existent. Upstream defect_at_one supplies the direct evaluation defect(1) = 0 by simplification against the definition of J.
proof idea
One-line wrapper that applies defect_at_one.
why it matters
The result feeds determinism_resolution, which asserts a unique J-cost minimizer at each step, and zero_defect_iff_unity, which equates total defect zero with the all-ones configuration. It supplies the base case for the Law of Existence formalization and aligns with the J-uniqueness step (T5) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.