Jcost_pos
plain-language theorem explainer
The recognition cost J(x) is strictly positive for every positive real x not equal to 1. Workers on the φ-ladder ultraviolet cutoff for Navier-Stokes regularity cite this to guarantee dissipation away from equilibrium. The short proof applies non-negativity of J together with the characterization of its zero set to reach a contradiction.
Claim. For all real $x > 0$ with $x ≠ 1$, the recognition cost $J(x) > 0$, where $J(x) := (x + x^{-1})/2 - 1$.
background
The recognition cost is defined by Jcost x := (x + x^{-1})/2 - 1 for x > 0, normalized so that J(1) = 0 by the axiom that equilibrium carries zero cost. This module develops the algebraic core of the argument that the φ-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Upstream results establish that J(x) ≥ 0 for x > 0 by the AM-GM inequality and that J(x) = 0 if and only if x = 1.
proof idea
The proof first invokes Jcost_nonneg to obtain 0 ≤ Jcost x. It then splits into cases via lt_or_eq_of_le. The strict inequality case is immediate. The equality case is ruled out by applying Jcost_eq_zero_iff, which forces x = 1 and contradicts the hypothesis x ≠ 1.
why it matters
This result is one of the main algebraic facts listed in the module for Navier-Stokes regularity from the φ-ladder cutoff. It ensures that the cost is positive away from equilibrium, supporting the decay estimates in the energy cascade. It aligns with the J-uniqueness property in the Recognition Science forcing chain and feeds the subsequent positivity and monotonicity statements for φ-rung scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.