Pressure Decay

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.Step3.pressureDecay_algebra {κ C₁₂ C₁₃ α β δ lam δr : ℝ} (hκ : 0 < κ) (hκhalf : κ ≤ 1 / 2) (hC₁₂ : 0 ≤ C₁₂) (hC₁₃ : 0 ≤ C₁₃) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hδ : 0 ≤ δ) (hlam : 0 ≤ lam) : 0 ≤ δr → ∀ (hsq : δr ^ 2 ≤ C₁₂ * κ⁻¹ * α * β + C₁₂ * κ * α * β + C₁₂ * κ ^ (2 / 3) * δ ^ 2 + C₁₃ * κ * lam), δr ≤ √(2 * C₁₂) * κ ^ (-1 / 2) * √α * √β + √(2 * C₁₂) * κ ^ (1 / 3) * δ + √C₁₃ * κ ^ (1 / 2) * √lam

Take square roots in the three-group pressure estimate, with the constants used by eq:pressure-decay.

The source-level bridge keeps the two external pressure inputs visible as the names used in the paper. The annular shares are supplied through the conditional cylinder assemblers until their unconditional replacements land.