nothing_costs_infinity
plain-language theorem explainer
The cost functional J is unbounded above on the positive reals, so no finite C bounds J(x) for all x > 0. Researchers deriving physics from Recognition Science cost axioms cite this to formalize that no finite-cost state can approach the null configuration. The argument negates the existential claim and invokes the auxiliary result that J exceeds any bound in a neighborhood of zero.
Claim. There is no real number $C$ such that $J(x) ≤ C$ for every positive real $x$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module encodes the three primitive axioms: Normalization (F(1) = 0), the Recognition Composition Law requiring F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y) for positive x and y, and Calibration (second log-derivative at zero equals one). J is defined by J(x) = (x + x^{-1})/2 - 1 and is the unique solution to these axioms. The Composition class encodes the d'Alembert equation in multiplicative form, while the upstream lemma J_arbitrarily_large_near_zero states that for any M there exists ε > 0 such that J(x) > M for all 0 < x < ε.
proof idea
The term-mode proof applies push_neg to the negated statement. It introduces an arbitrary bound C, invokes J_arbitrarily_large_near_zero to obtain ε > 0 with J(x) > C for 0 < x < ε, then selects the witness ε/2. The conditions 0 < ε/2 and ε/2 < ε are discharged by linarith, after which the lemma supplies the required inequality.
why it matters
This theorem realizes the Level 3 meta-principle that nothing cannot recognize itself because J approaches infinity at zero. It supports the economic reading that contradiction carries infinite cost while consistency is cost-free, and it feeds the uniqueness result T5 together with the forcing chain that yields three spatial dimensions. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.