normalized_vorticity_bounded

formal source

 127/-! ## Properties of the Normalized Ancient Element -/
 128
 129/-- The normalized vorticity satisfies ‖ω̃ₙ‖ ≤ 1 for all n. -/
 130theorem normalized_vorticity_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) (n : ℕ) :
 131    normalized M n ≤ 1 :=
 132  normalized_le_one M n (hpos n)
 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