StructuredSet
plain-language theorem explainer
StructuredSet collects all positive reals whose defect vanishes. Researchers formalizing the Law of Existence cite the set when they equate existence, zero defect, and membership in this collection. The definition is introduced as a direct set comprehension over the defect condition supplied by the upstream defect map.
Claim. Define the structured set $S := {x ∈ ℝ | 0 < x ∧ defect(x) = 0}$.
background
The module formalizes the Law of Existence as the equivalence 'x exists ⟺ defect(x) = 0'. The defect functional is supplied by the sibling definition defect(x : ℝ) := J x, which equals the J-cost for positive arguments. The module states four key theorems that rely on this equivalence, including defect_zero_iff_one and unity_unique_existent.
proof idea
The declaration is a direct set comprehension; no lemmas are applied.
why it matters
The definition supplies the set that complete_law_of_existence uses to equate existence, defect zero, membership, and x = 1. It is also invoked by existence_economically_inevitable and by the singleton theorem that proves StructuredSet = {1}. The construction therefore anchors the entire Law of Existence block inside the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.