Pressure Gradient Origin Clause Budget

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

Budget comparison for the one-sided pressure-gradient constant

The quantitative constant oneSidedPressureGradientKP is the one-sided Morrey constant of a selected pressure gradient, evaluated with the two numerical budgets fed to it by the local estimates. This module records the elementary comparison facts for that constant: monotonicity of the one-sided Morrey bound in its two integral budgets, and the resulting bound of the specialized constant by the general one with the budget factors made explicit. Both results are pure order arithmetic on ℝ≥0∞; no analytic hypothesis enters.

theorem CKN.Core.Step4.oneSidedMorreyBound_le_pressureGradientKP {q τ C_CZ R₀ R₁ ε : ℝ} {KU KD A B : ENNReal} (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) R₁ A B ≤ oneSidedPressureGradientKP q τ C_CZ R₀ R₁ ε KU KD

The one-sided Morrey bound taken with the raw budget data is dominated by the specialized constant oneSidedPressureGradientKP, whose budgets carry the explicit factor |C_CZ| + 1.