normalized_bounded

formal source

 133
 134/-- The running maximum is the correct normalization: after normalizing,
 135    the sequence no longer diverges. -/
 136theorem normalized_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) :
 137    ∀ n, normalized M n ≤ 1 :=
 138  fun n => normalized_vorticity_bounded M hpos n
 139
 140/-! ## TF Pinch at Zero Node (Thm 5.5) -/
 141
 142/-- **TF Pinch at a zero node**: if the J-cost function J(x) has a zero at
 143    x₀ in the interior of the domain, then the vorticity direction is constant
 144    in a neighborhood of x₀.
 145
 146    This is pure convex analysis: J is strictly convex (J'' > 0), so
 147    J(x₀) = 0 implies x₀ = 1 (the unique minimum). At x = 1, the vorticity
 148    direction is determined by the leading-order quadratic expansion J ≈ ε²/2.
 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