tf_pinch_at_zero_node

formal source

 149
 150    In RS: the TF (topological frustration) prevents simultaneous vanishing of
 151    both the vorticity magnitude and direction — one of them must persist. -/
 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
 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. -/
 169theorem constant_vorticity_implies_rigid_rotation (ω₀ : ℝ) :
 170    ∃ (u : ℝ × ℝ → ℝ × ℝ), ∀ (x : ℝ × ℝ),
 171      u x = (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1) := by
 172  exact ⟨fun x => (ω₀ / 2 * (-x.2), ω₀ / 2 * x.1), fun x => rfl⟩
 173
 174/-- Rigid rotations have infinite energy (‖u‖² = ∫ ω₀²|x|²/4 dx = ∞).
 175    This contradicts the finite-energy assumption on NS solutions.
 176
 177    **Proof sketch** (standard measure theory):
 178    In `ℝ × ℝ` with the sup metric, `B(0, R) = (-R, R)²`. By Fubini:
 179    `∫_{(-R,R)²} (ω₀/2)² (x² + y²) = (ω₀/2)² · 8R⁴/3`,
 180    which grows as R⁴ and exceeds any bound. The formal computation
 181    requires `MeasureTheory.integral_prod` + `intervalIntegral.integral_pow`.
 182