J_arbitrarily_large_near_zero
plain-language theorem explainer
For any real bound M there exists ε > 0 such that J(x) > M for all x in (0, ε). Researchers deriving existence from cost axioms cite this to establish that states near zero incur arbitrarily high cost. The argument constructs ε = 1/(2(max(M,0)+2)) explicitly and applies reciprocal lower bounds together with the definition of J.
Claim. For every real number $M$, there exists $ε > 0$ such that $J(x) > M$ for all real $x$ with $0 < x < ε$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module CostAxioms encodes three primitive axioms for a cost functional: normalization at unity, the recognition composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), and calibration of the logarithmic second derivative. From these axioms J is the unique solution J(x) = (x + x^{-1})/2 - 1, which assigns to each positive ratio x the cost of deviating from perfect balance at x = 1. The module interprets J(0) → ∞ as the statement that non-existence is infinitely expensive, making existence an economic necessity rather than an additional postulate.
proof idea
The proof constructs ε = 1/(2M') with M' = max(M,0) + 2. It verifies 2M'x < 1 from the choice of ε, deduces 1/x > 2M', and obtains the chain J(x) ≥ (1/x)/2 - 1 > M' - 1 > M by direct comparison and linarith/nlinarith on the resulting inequalities.
why it matters
This supplies the uniform lower bound used by J_tendsto_atTop_as_x_to_zero to obtain the filter limit J(x) → +∞ as x → 0+, which in turn yields mp_from_cost (the meta-principle that nothing cannot recognize itself) and nothing_costs_infinity. It therefore converts the explicit algebraic form of J into the core economic claim of the Recognition Science framework that non-existence carries infinite cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.