nothing_unbounded_defect
plain-language theorem explainer
The defect functional diverges to infinity as its argument approaches zero from above. Researchers studying the cost structure of Recognition Science cite this to establish that zero cannot be a stable configuration. The proof is a direct one-line application of the nothing_cannot_exist theorem from LawOfExistence.
Claim. $∀ C ∈ ℝ, ∃ ε > 0, ∀ x > 0, (x < ε → C < J(x))$ where $J$ is the cost function obeying the Recognition Composition Law.
background
The OntologyPredicates module defines RSExists x as the condition that defect(x) collapses to zero under coercive projection and aggregation, turning existence into a verifiable selection outcome. The defect functional is given by defect x := J x for positive x, with J the unique function satisfying J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This theorem restates the upstream nothing_cannot_exist result, whose doc-comment states: 'Nothing Cannot Exist: For any cost bound C, defect exceeds C near zero. This is the sharp statement that Nothing costs infinity.'
proof idea
The proof is a one-line wrapper that applies the nothing_cannot_exist theorem from the LawOfExistence module.
why it matters
This result feeds directly into nothing_not_rs_exists, whose doc-comment calls it the operational content of 'Nothing cannot recognize itself'. It supplies the cost-theoretic derivation of the Meta-Principle in the T0-T8 forcing chain, specifically supporting T5 J-uniqueness and the claim that zero is not selectable. The parent nothing_cannot_exist supplies the explicit ε construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.