J_formula_nonneg
plain-language theorem explainer
The non-negativity of J-cost, given by J(x) = (x + 1/x)/2 - 1, holds for every positive real x. Researchers deriving bounds on recognition costs in the Recognition Science framework would cite this result when establishing lower bounds on event costs. The proof is a one-line wrapper that calls am_gm_reciprocal and finishes with linear arithmetic.
Claim. For every real number $x > 0$, $((x + 1/x)/2) - 1$ is nonnegative.
background
The Inequalities module collects basic lemmas that underwrite the Recognition Science monolith. J-cost is introduced in ObserverForcing as the cost of any recognition event and reappears in MultiplicativeRecognizerL4 as the derived cost of a comparator acting on positive ratios. The decisive upstream fact is am_gm_reciprocal, which asserts that x + 1/x ≥ 2 for all x > 0 and is described as the fundamental inequality forcing J-cost to be nonnegative.
proof idea
The proof applies am_gm_reciprocal to the hypothesis x > 0, obtaining x + 1/x ≥ 2, then invokes linarith to rearrange the target expression into the desired inequality.
why it matters
This lemma supplies the elementary non-negativity of J-cost that is presupposed whenever recognition costs are bounded below in the forcing chain. It directly implements the claim that every recognition event has nonnegative cost, a prerequisite for the T0-to-T8 development and for the Recognition Composition Law. No downstream theorems are recorded, leaving its use in later mass or alpha derivations implicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.