136theorem normalized_bounded (M : ℕ → ℝ) (hpos : ∀ n, 0 < M n) : 137 ∀ n, normalized M n ≤ 1 :=
proof body
Term-mode proof.
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.