jcost_arbitrarily_small_positive
plain-language theorem explainer
For every positive tolerance ε there is a ratio strictly above 1 whose recognition cost J is positive yet smaller than ε. Cosmogenesis and T-3 cite this to kill any positive demand threshold: a forced posting can sit just under any ε. The proof picks x = 1 + min(1,ε) and reduces J to a quadratic over a linear denominator, then finishes by elementary inequalities.
Claim. For every real $\varepsilon > 0$ there exists a real $x > 1$ such that $0 < J(x) < \varepsilon$, where $J(x) = \frac{x + x^{-1}}{2} - 1$ is the Recognition Science cost of a positive ratio.
background
Module T-3 fixes the cosmogenesis refinement trigger as law-derived: descend a block exactly when it carries a forced internal posting, so the threshold is structurally zero. The naive alternative (descend when demand exceeds a tuned $\varepsilon$) is forbidden by the north star; this lemma is the analytic reason no positive $\varepsilon$ works.
The cost is the standard RS functional $J(x) = (x + x^{-1})/2 - 1$, also written $\cosh(\log x) - 1$ (T5 J-uniqueness). Sibling jcost_pos already records that any genuine distinction ($x > 0$, $x \neq 1$) has strictly positive cost, via the identity $J(x) = (x-1)^2/(2x)$. Demand on a block is the sum of $J$ over that block's internal postings (demand, built from RungCoarsen.cost).
The local claim is purely about $J$ near the identity: ratios slightly above one produce arbitrarily small positive cost, so a forced distinction can hide under any positive cutoff.
proof idea
Fix $\varepsilon > 0$ and set $\delta := \min(1,\varepsilon) > 0$. Take the witness $x := 1 + \delta$. Then $x > 1$ and $x > 0$, so jcost_pos gives $J(x) > 0$. Unfold $J$ and simplify to the closed form $J(1+\delta) = \delta^2 / (2(1+\delta))$. Clearing the positive denominator reduces the target $J(x) < \varepsilon$ to $\delta^2 < 2\varepsilon(1+\delta)$, which follows from $\delta \le 1$, $\delta \le \varepsilon$, and nonnegativity of $\delta(1-\delta)$ by a short nlinarith chase. No external lemmas beyond jcost_pos and field algebra.
why it matters
This is the analytic half of T-3's "no positive threshold is safe" clause in the scale-adaptive Cosmogenesis spine (build_spine.T3_law_derived_refinement). Downstream epsilon_unsafe consumes it directly: pick a single internal Event with the small-cost ratio, form demand under the two-site block map b01, and show the rule "descend iff demand $> \varepsilon$" skips that active block, so reconstruction is lossy.
Together with lossless_iff, lossless_law, and descendLaw_necessary, it forces the unique law-given rule: descend iff recognition demand is positive. The threshold is zero, read off the ledger; there is no free $\varepsilon$. The cost functional is the same $J$ fixed by T5 in the forcing chain, so the argument sits on the RS composition law rather than an ad hoc metric. Closes the knob-risk gap that the Python numerical discharge already observed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.