tf_pinch_at_zero_node
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove convexity of J from first principles.
- Does not extend the pinch to non-convex cost functions.
- Does not quantify the positivity rate away from the minimum.
- Does not incorporate the time-dependent Navier-Stokes evolution.
formal statement (Lean)
152theorem tf_pinch_at_zero_node (J : ℝ → ℝ) (_hJ_convex : ConvexOn ℝ (Set.Ioi 0) J)
153 (_hJ_zero : J 1 = 0) (hJ_pos : ∀ x, x ∈ Set.Ioi 0 → x ≠ 1 → J x > 0) :
154 ∀ x, x ∈ Set.Ioi 0 → J x = 0 → x = 1 := by
proof body
Term-mode proof.
155 intro x hx hJx
156 by_contra h
157 exact absurd hJx (ne_of_gt (hJ_pos x hx h))
158
159/-! ## Rigid Rotation Identification -/
160
161/-- A 2D velocity field with constant vorticity is a rigid rotation.
162 If ω(x) = ω₀ (constant) and u is divergence-free, then
163 u(x) = (ω₀/2) × (x - x₀) for some center x₀.
164
165 This is the content of the 2D Biot-Savart law for constant vorticity.
166 It is the final step in Stage 5 of the NS paper: once we know the
167 blowup profile has constant vorticity direction and magnitude,
168 it must be a rigid rotation, which is excluded by the energy constraint. -/