DefectCollapse
plain-language theorem explainer
DefectCollapse(x) is the predicate requiring x positive and defect(x) equal to zero. It supplies the right-hand side of the Law of Existence biconditional. The definition is a direct conjunction using the local defect functional.
Claim. The predicate holds for $x$ precisely when $x > 0$ and $J(x) = 0$, where $J$ denotes the cost functional realized by the defect map.
background
The module states the Law of Existence as the biconditional that x exists if and only if defect(x) = 0. The defect map is defined by defect(x) := J(x) for real x. An upstream discrete Defect in CPM.LNALBridge returns 0 or 1 according to whether its string argument is structured, while the local defect replaces that toy version with the J-cost.
proof idea
One-line definition that directly forms the conjunction 0 < x ∧ defect x = 0. No lemmas or tactics are invoked.
why it matters
The predicate is the exact right-hand side of the law_of_existence theorem, which states Exists x ↔ DefectCollapse x. It therefore supports the downstream claim that 1 is the unique existent and the module's characterization that existence is equivalent to defect collapse at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.