mp_forces_existence
plain-language theorem explainer
The assumption that defect diverges to infinity near zero forces existence of a stable configuration. Foundational work on the Meta-Principle in Recognition Science cites this to close the selection argument from cost structure. The proof is a one-line term that discards the hypothesis and directly supplies the known RSExists instance at 1.
Claim. If the defect function satisfies $C < defect(x)$ for all sufficiently small $x > 0$ and every real $C$, then there exists $x > 0$ such that $x$ is stable under the J-cost (i.e., defect vanishes).
background
RSExists x holds precisely when x > 0 and defect x = 0, making existence a derived outcome of cost minimization rather than a primitive. The module treats this as the operational ontology: configurations are selected by collapse of defect under coercive projection. The hypothesis encodes the Meta-Principle in cost language, stating that nothing (the zero configuration) is unbounded in defect and therefore not selectable.
proof idea
Term-mode proof. The intro discards the divergence hypothesis; exact then instantiates the pair (1, rs_exists_one) where rs_exists_one is the sibling lemma establishing RSExists at 1.
why it matters
The declaration converts the Meta-Principle into a concrete existence theorem inside the ontology predicates. It sits after the definitions of RSExists and rs_exists_one and before any uniqueness or uniqueness-at-one results. No downstream uses are recorded, indicating it functions as a foundational closure step rather than an intermediate lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.