tf_pinch_at_zero_node
plain-language theorem explainer
A convex J-cost function on the positive reals that vanishes at 1 and is strictly positive elsewhere has its unique zero at 1. Navier-Stokes regularity arguments cite this when extracting constant vorticity direction from a zero node in the normalized blowup profile. The proof is a direct contradiction that invokes the positivity hypothesis on any candidate zero other than 1.
Claim. Let $J : (0,∞) → ℝ$ be convex, 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 formalizes running-max normalization for the Navier-Stokes regularity proof: given a hypothetical blowup sequence with sup-norms $M_n → ∞$, one constructs a monotone running maximum $M̃(t)$ and rescaled fields whose $L^∞$ norm is bounded by 1. The J-cost function appears in the TF (topological frustration) analysis; the doc-comment states that J is strictly convex with unique minimum at 1, so a zero node forces constant vorticity direction via the quadratic expansion $J ≈ ε²/2$ at that point. Upstream results supply auxiliary structures such as ledger factorization and integration-gap counts but are not invoked in this isolated convex-analysis fact.
proof idea
Term-mode proof by contradiction. Assume $x>0$, $x≠1$ with $J(x)=0$. The positivity hypothesis immediately yields $J(x)>0$, which is absurd. No lemmas beyond the supplied hypotheses are applied.
why it matters
The result is referenced inside runningMaxCert as the tf_pinch field of the RunningMaxCert structure, alongside monotonicity, boundedness, and rigid-rotation exclusions. It supplies the TF-pinch step in the NS paper §3 normalization argument, ensuring that a zero of the cost cannot occur away from the unit scale and thereby preventing simultaneous vanishing of vorticity magnitude and direction. This aligns with the Recognition Science J-uniqueness property (T5) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.