Pressure Gradient Origin Budget

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

The clipped origin-carrier budget

At the clipped scale (1 - R₁) / 2, rescaling the one-sided Morrey bound leaves its small-cell budget unchanged and multiplies its whole-carrier budget by (R₁ / ((1 - R₁) / 2)) ^ θ. This file records the exact sufficient budget condition, the threshold where that factor is at most one, and the strict failure of the saturated established budget above that threshold.

theorem CKN.Core.Step4.clipped_scale_pos {R₁ : ℝ} (hR₁ : R₁ < 1) : 0 < (1 - R₁) / 2

The clipped radius is positive whenever the carrier radius is less than one.

theorem CKN.Core.Step4.clipped_scale_ratio_le_six {R₁ : ℝ} (hR₁ : R₁ < 3 / 4) : R₁ / ((1 - R₁) / 2) ≤ 6

For R₁ < 3 / 4, the clipped scale ratio is at most six.

theorem CKN.Core.Step4.clipped_scale_ratio_le_one_iff {R₁ : ℝ} (hR₁ : R₁ < 1) : R₁ / ((1 - R₁) / 2) ≤ 1 ↔ R₁ ≤ 1 / 3

The clipped scale ratio is at most one exactly up to the radius 1 / 3.

theorem CKN.Core.Step4.one_lt_clipped_scale_ratio {R₁ : ℝ} (hthird : 1 / 3 < R₁) (hR₁ : R₁ < 1) : 1 < R₁ / ((1 - R₁) / 2)

Above the threshold, the clipped scale ratio is strictly greater than one.

theorem CKN.Core.Step4.growth_exponent_mem_Icc {q τ : ℝ} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτ' : τ ≤ 25) : 59 / 25 ≤ 5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q) ∧ 5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q) ≤ 71 / 25

Under the admissible bounds on q and τ, the exponent in the clipped scale factor lies between 59 / 25 and 71 / 25.

theorem CKN.Core.Step4.clipped_factor_le_216 {R₁ θ : ℝ} (hR₁ : 0 < R₁) (hR₁' : R₁ < 3 / 4) (hθ : 0 ≤ θ) (hθ' : θ ≤ 3) : (R₁ / ((1 - R₁) / 2)) ^ θ ≤ 216

The clipped scale inflation factor has the uniform upper bound 216 on the admissible range.

theorem CKN.Core.Step4.clipped_factor_le_one {R₁ θ : ℝ} (hR₁ : 0 < R₁) (hR₁' : R₁ ≤ 1 / 3) (hθ : 0 ≤ θ) : (R₁ / ((1 - R₁) / 2)) ^ θ ≤ 1

On the lower-radius range, the clipped scale inflation factor is at most one.

theorem CKN.Core.Step4.one_lt_clipped_factor {R₁ θ : ℝ} (hthird : 1 / 3 < R₁) (hR₁ : R₁ < 1) (hθ : 0 < θ) : 1 < (R₁ / ((1 - R₁) / 2)) ^ θ

Above R₁ = 1 / 3, every positive clipped scale exponent makes the inflation factor strictly greater than one.

theorem CKN.Core.Step4.clipped_clause_of_inflated_budget {q τ C_CZ R₀ R₁ ε : ℝ} {KU KD A B : ENNReal} (hR₁ : 0 < R₁) (hR₁' : R₁ < 1) (hA : A ≤ 3 * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε)) (hB : B * ENNReal.ofReal ((R₁ / ((1 - R₁) / 2)) ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))) ≤ ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1)) : Endgame.oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((1 - R₁) / 2) A B ≤ oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD

If the whole-carrier bound includes the clipped scale inflation, it suffices for the one-sided Morrey bound at the clipped radius.

theorem CKN.Core.Step4.clipped_clause_of_global_bound {q τ C_CZ R₀ R₁ ε : ℝ} {KU KD A B : ENNReal} (hR₁ : 0 < R₁) (hR₁third : R₁ ≤ 1 / 3) (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτ' : τ ≤ 25) (hA : A ≤ 3 * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε)) (hB : B ≤ ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1)) : Endgame.oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((1 - R₁) / 2) A B ≤ oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD

When R₁ ≤ 1 / 3, the established whole-carrier budget alone suffices at the clipped radius.

theorem CKN.Core.Step4.clipped_saturated_budget_exceeds_KP {q τ C_CZ R₀ R₁ ε : ℝ} {KU KD : ENNReal} (hq : 5 / 2 < q) (hτ : 25 / 3 ≤ τ) (hτ' : τ ≤ 25) (hR₁third : 1 / 3 < R₁) (hR₁' : R₁ < 3 / 4) (hKU : KU < ⊤) (hKD : KD < ⊤) : oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD < Endgame.oneSidedMorreyBound (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) ((1 - R₁) / 2) (ENNReal.ofReal (|C_CZ| + 1) * (3 * (3 * KU * KD + Endgame.forceSourceMorreyBound q ε))) (ENNReal.ofReal (|C_CZ| + 1) * ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1))

At a saturated established budget, the clipped clause is strictly larger than the established constant whenever R₁ > 1 / 3. This is a failure of that budget to prove the clause, not a lower bound on the actual pressure-gradient integral.