Jcost_inv_eq
plain-language theorem explainer
The theorem establishes that the recognition cost satisfies J(1/x) = J(x) for every nonzero real x. Researchers formalizing the phi-ladder ultraviolet cutoff for Navier-Stokes regularity cite this reciprocal invariance when tracking dissipation across inverse scales. The proof is a one-line term reduction that unfolds the definition of Jcost, invokes inv_inv, and cancels via ring.
Claim. For every real $x$ with $x ≠ 0$, let $J(y) := (y + y^{-1})/2 - 1$. Then $J(x^{-1}) = J(x)$.
background
Jcost is defined by Jcost(x) := (x + x^{-1})/2 - 1 for real x > 0 and serves as the canonical recognition cost. The module develops its algebraic properties to support the claim that the phi-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. The local setting is the formalization of Navier-Stokes regularity via phi-ladder cutoff, whose main results include nonnegativity of Jcost, equivalence of zero cost with x = 1, and monotonicity of rung scales.
proof idea
The proof is a one-line term-mode reduction. It applies simp only on the definition of Jcost together with inv_inv, then closes with the ring tactic to obtain algebraic cancellation.
why it matters
This symmetry fills a basic algebraic step in the phi-ladder cutoff argument for Navier-Stokes regularity and aligns with the J-uniqueness property (T5) in the forcing chain, where J(x) = cosh(log x) - 1 is invariant under x to 1/x. It supports downstream module results such as Jcost_nonneg and cascadeDepth_mono even though no direct used_by edges are recorded. The result touches the normalization axiom J(1) = 0 and the discrete lattice structure underlying the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.