Jcost_pos_of_ne_one
plain-language theorem explainer
The recognition cost J satisfies J(x) > 0 for every positive real x not equal to one. Researchers in acoustics, chemistry, and climate modeling invoke the result to establish that deviations from unit scale carry strictly positive penalties. The proof rewrites J via its squared algebraic form and confirms the fraction is positive by separate checks on numerator and denominator.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for real $x$. Then $J(x) > 0$ whenever $x > 0$ and $x ≠ 1$.
background
Jcost is the recognition cost function on the reals, defined by the expression (x + x inverse)/2 minus one. The sibling lemma Jcost_eq_sq supplies the algebraically equivalent squared form (x-1) squared over (2x) that holds for all nonzero x. This positivity statement belongs to the Cost module inside the Recognition Science development, where costs quantify deviations from the self-similar fixed point.
proof idea
The tactic proof first obtains x ≠ 0 from the given positivity hypothesis. It rewrites the goal with the squared-form lemma Jcost_eq_sq. Division positivity is then applied; the numerator square is shown positive by the hypothesis x ≠ 1, while the denominator 2x is positive by the standing assumption x > 0.
why it matters
The lemma supplies the basic positivity fact used by forty downstream results, including srCost_pos_off_threshold in acoustics and above_threshold_positive in chemistry. It directly supports the framework claim that recognition cost is strictly positive away from the unit fixed point, consistent with the J-uniqueness and phi-ladder structure. No open scaffolding remains for this elementary case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 5 of 5)
-
VLA models score 90 percent then 0 percent after small benchmark changes
"models persist in executing grasping actions when the target object is replaced with irrelevant items, and their outputs remain unchanged even when given corrupted instructions or even messy tokens"
-
Discrete text levels train LMMs to score visuals like humans
"Observing that human raters only learn and judge discrete text-defined levels in subjective studies, we propose to emulate this subjective process and teach LMMs with text-defined rating levels instead of scores."
-
Variance term stops collapse in self-supervised image learning
"a term that maintains the variance of each embedding dimension above a threshold... a term that decorrelates each pair of variables"
-
Human preferences train better flow-based video generators
"Experimental results indicate that VideoReward significantly outperforms existing reward models..."
-
K-sparse autoencoders scale cleanly to 16 million latents
"We propose using k-sparse autoencoders [Makhzani and Frey, 2013] to directly control sparsity, simplifying tuning and improving the reconstruction-sparsity frontier."