tf_pinch_at_zero_node
plain-language theorem explainer
Navier-Stokes analysts cite this result to enforce that a strictly convex J-cost function with a zero in the positive domain must vanish only at the normalized scale x=1. It appears inside the running-max normalization to realize the topological frustration pinch, blocking simultaneous zeros in vorticity magnitude and direction. The argument is a direct contradiction that applies the positivity hypothesis to negate any other candidate zero.
Claim. Let $J:ℝ→ℝ$ be convex on $(0,∞)$, satisfy $J(1)=0$, and obey $J(x)>0$ for all $x>0$ with $x≠1$. Then $J(x)=0$ for $x>0$ forces $x=1$.
background
The module constructs running-max normalization for Navier-Stokes regularity: given a blowup sequence with $M_n=‖ω(·,t_n)‖∞→∞$, it defines the running supremum $M̃(t)$ and rescales fields so that the normalized vorticity satisfies $‖ω̃‖∞≤1$. The J-cost function enters via ledger factorization, where its strict convexity encodes topological frustration separating magnitude and direction zeros at interior nodes.
proof idea
The proof introduces a candidate zero x, assumes x≠1 by contradiction, and applies the positivity hypothesis to obtain J(x)>0, which directly negates the given zero. It is a one-line wrapper that invokes ne_of_gt on the strict positivity statement.
why it matters
This supplies the tf_pinch component of runningMaxCert, which assembles monotonicity, boundedness, and rigid-rotation exclusion to certify the normalized fields. It realizes T5 J-uniqueness from the forcing chain and closes Stage 5 of the NS paper argument: constant vorticity direction at the pinch is excluded by energy divergence. The parent runningMaxCert theorem quotes this directly to complete the normalization certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.