mp_from_cost
plain-language theorem explainer
The declaration establishes that the cost functional J diverges to positive infinity as its argument approaches zero from above. Researchers deriving physics from recognition axioms cite it to justify the meta-principle that Nothing cannot recognize itself. The proof is a one-line wrapper applying the prior unboundedness result for J near zero.
Claim. For every real number $M$ there exists an $ε > 0$ such that $J(x) > M$ for all $x$ satisfying $0 < x < ε$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module CostAxioms encodes the three primitive axioms of Recognition Science: normalization with $F(1) = 0$, the recognition composition law $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$, and calibration $F''_{log}(0) = 1$. From these the canonical cost functional is derived as the unique solution $J(x) = (x + x^{-1})/2 - 1$, which assigns zero cost to unity and infinite cost to the limit at zero. The upstream theorem J_arbitrarily_large_near_zero states that for any bound $M$ there exists $ε > 0$ such that $J(x) > M$ whenever $0 < x < ε$, proved by explicit choice of $ε = 1/(2(M + 2))$ and bounding the inverse term.
proof idea
The proof is a one-line wrapper that applies the theorem J_arbitrarily_large_near_zero from the same module.
why it matters
This declaration derives the meta-principle MP that Nothing cannot recognize itself, as stated in the module documentation, because recognition requires finite cost while $J(0) → ∞$. It occupies level 3 in the axiomatic hierarchy after uniqueness of J from the primitive axioms and supports the economic reading in which infinite cost blocks self-recognition of the empty state. The result aligns with the forcing chain at T5 uniqueness and the law of existence that $x$ exists precisely when $J(x) = 0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.