Jcost_nonneg
plain-language theorem explainer
The lemma establishes non-negativity of the J-cost function J(x) = (x + x^{-1})/2 - 1 for every positive real x. Researchers building path integrals, acoustic penalties, or aesthetic costs in Recognition Science cite it to guarantee that derived quantities remain non-negative. The proof rewrites J via the squared-ratio identity Jcost_eq_sq and applies non-negativity of squares together with positivity of the denominator.
Claim. For every real number $x > 0$, $J(x) := (x + x^{-1})/2 - 1$ satisfies $J(x) ≥ 0$.
background
The J-cost function is introduced in JcostCore as the basic recognition cost J(x) = (x + x^{-1})/2 - 1, which encodes the J-uniqueness property (T5) of the forcing chain and satisfies the Recognition Composition Law. Its algebraic form is supplied by the sibling lemma Jcost_eq_sq, which states J(x) = (x-1)^2/(2x) for x ≠ 0. The present module imports only Mathlib and focuses on core identities for this cost before it is lifted to ladders, actions, and acoustics.
proof idea
The tactic proof first obtains x ≠ 0 from the hypothesis 0 < x. It then invokes Jcost_eq_sq to replace Jcost x by the explicit fraction (x-1)^2/(2x). Non-negativity of the numerator follows from sq_nonneg, positivity of the denominator from mul_pos, and non-negativity of the quotient from div_nonneg; the final simpa substitutes the representation back into the goal.
why it matters
This non-negativity result is invoked by more than forty downstream declarations, including actionJ_nonneg in PathSpace, pitchCost_nonneg and srCost_nonneg in Acoustics, aestheticCost_nonneg, and yieldGapCost_nonneg. It supplies the positivity needed for J to serve as a defect distance on the phi-ladder and for the eight-tick octave structure, closing the basic requirement that costs derived from positive quantities cannot be negative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 3 of 3)
-
Threaded spindle and ring lock gauge-wheel spacing on planters
"The mechanism's core function (axial lock while permitting rotation) depends on sustained frictional preload from the washer/pressure ring."
-
Optimizers reduce to steepest descent under specific norms
"Proposition 1 (Steepest descent)... arg min Δw [gJΔw + λ/2 ||Δw||²] = -||g||*/λ · arg max ||t||=1 gJt"
-
Chunked prefills let decodes piggyback for up to 10x faster LLM decode
"SARATHI employs chunked-prefills, which splits a prefill request into equal sized chunks, and decode-maximal batching, which constructs a batch using a single prefill chunk and populates the remaining slots with decodes."