Jcost_eq_zero_iff
plain-language theorem explainer
For positive real x the recognition cost J(x) vanishes exactly at equilibrium x=1. Workers formalizing the Navier-Stokes regularity argument via the phi-ladder cutoff cite this equivalence to identify persistent states on the discrete lattice. The tactic proof splits the biconditional, unfolds the definition of Jcost, reduces the forward direction to (x-1)^2=0 by linear and nonlinear arithmetic, and dispatches the converse by substitution into the normalization Jcost 1=0.
Claim. For every real number $x>0$, $J(x)=0$ if and only if $x=1$, where the recognition cost is given by $J(x):=(x+x^{-1})/2-1$.
background
The module NavierStokes.PhiLadderCutoff supplies the algebraic and combinatorial core of the claim that the phi-ladder furnishes an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Its module documentation lists Jcost_eq_zero_iff among the principal results, together with nonnegativity of J, positivity and strict monotonicity of the phi-rung scales, and finiteness of rungs below any given scale. The canonical recognition cost is defined by Jcost x := (x + x^{-1})/2 - 1 and satisfies the normalization Jcost 1 = 0 by axiom A1.
proof idea
The proof is a direct tactic-mode equivalence. Constructor splits the biconditional. The forward direction unfolds Jcost, obtains x + x^{-1}=2 by linarith from the hypothesis, records x * x^{-1}=1, then applies nlinarith to reach (x-1)^2=0 and concludes x=1. The reverse direction rewrites the hypothesis x=1 and invokes the sibling lemma Jcost_one.
why it matters
Downstream results that invoke the equivalence include defectDist_no_global_quasi_triangle in CostAlgebra, Jcost_zero_iff_one in Cost, public_cost_layer in DimensionalConstraints.CostLayer, and the CoherentRecognition and persistent_state_unique statements in ObserverForcing. It supplies the equilibrium characterization required by the phi-ladder cutoff paper (papers/tex/NS_Regularity_Phi_Ladder_Cutoff.tex) and aligns with the T5 J-uniqueness step of the forcing chain. The result closes one of the algebraic prerequisites for showing that only the unity state persists under recognition forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.