Radius exponents for the pressure term of a slice majorant

The pressure-gradient slice estimate of ss:step3 carries, on a cell of radius r and at doubled spatial radius ρ = 2 r, the positive term ρ⁻¹/² ‖p(·,s)‖_{L^{3/2}(B_ρ)}. Raising it to the power 6/5 and integrating over the backward window (t - r², t] produces a power of r that has to dominate the power 5 - 6/κ demanded by membership of the gradient in the parabolic Morrey class M^{6/5,κ} of def:parabolic-morrey.

This file records the two exponent balances involved, in the normalisation 5 * (1 - (6/5)/κ) = 5 - 6/κ:

• the cell-centred route, in which the pressure is replaced by the cell-mean-subtracted pressure and controlled in a parabolic Morrey class M^{3/2,χ} on the doubled cell. Hölder in time and the Morrey growth then give the radius power 19/5 - 6/χ, so the route closes exactly when 1/χ ≤ 1/κ - 1/5. The gradient exponent in eq:pressure-gradient-morrey lies between 25/11 and 25/9; the required pressure exponent ranges from 25/6 to 25/4 at those endpoints. Thus χ ≥ 25/4 suffices uniformly over the admissible range.
• the fixed-scale route, in which the pressure enters only through a majorant that is bounded in space on a fixed carrier and lies in L^{3/2} in time, as for the fixed-carrier remainder in the proof of lem:pressure-gradient-morrey. The spatial measure of the cell then contributes and the radius power is 17/5, which dominates the requirement for every admissible κ with room to spare.

theorem CKN.Core.Step4.five_mul_one_sub_six_fifths_div {κ : ℝ} (hκ : κ ≠ 0) : 5 * (1 - 6 / 5 / κ) = 5 - 6 / κ

The Morrey growth power in the normalisation used by the cell clauses.

theorem CKN.Core.Step4.cellCentred_pressure_exponent_le_iff (χ κ : ℝ) : 5 - 6 / κ ≤ 19 / 5 - 6 / χ ↔ 1 / χ ≤ 1 / κ - 1 / 5

The cell-centred balance: the radius power produced by a pressure Morrey exponent χ dominates the power required by the gradient Morrey exponent κ exactly when 1/χ ≤ 1/κ - 1/5.

theorem CKN.Core.Step4.cellCentred_pressure_exponent_at_min_kappa : 19 / 5 - 6 / (25 / 6) = 5 - 6 / (25 / 11)

At the smallest admissible gradient Morrey exponent the cell-centred route needs pressure Morrey exponent exactly 25/6; both sides equal 59/25.

theorem CKN.Core.Step4.cellCentred_pressure_exponent_at_max_kappa : 19 / 5 - 6 / (25 / 4) = 5 - 6 / (25 / 9)

At the largest admissible gradient Morrey exponent the cell-centred route needs pressure Morrey exponent exactly 25/4; both sides equal 71/25.

theorem CKN.Core.Step4.endgame_kappa_le {τ q : ℝ} (hτ : 0 < τ) (hτ25 : τ ≤ 25) : min (1 / τ + 8 / 25)⁻¹ q ≤ 25 / 9

The gradient Morrey exponent of thm:endgame never exceeds 25/9.

theorem CKN.Core.Step4.endgame_kappa_ge {τ q : ℝ} (hτ : 25 / 3 ≤ τ) (hq : 5 / 2 < q) : 25 / 11 ≤ min (1 / τ + 8 / 25)⁻¹ q

The gradient Morrey exponent of thm:endgame is never below 25/11.

theorem CKN.Core.Step4.cellCentred_pressure_exponent_quarter_suffices {κ : ℝ} (hκ : 0 < κ) (hκle : κ ≤ 25 / 9) : 5 - 6 / κ ≤ 19 / 5 - 6 / (25 / 4)

Pressure Morrey exponent 25/4 closes the cell-centred balance for every gradient Morrey exponent admissible in thm:endgame.

theorem CKN.Core.Step4.cellCentred_pressure_exponent_deficit {κ : ℝ} (hκ : 25 / 11 ≤ κ) : 19 / 5 - 6 / (25 / 8) < 5 - 6 / κ

The pressure Morrey exponent available from the decay estimate, 25/8, does not close the cell-centred balance for any admissible gradient Morrey exponent: the produced radius power 47/25 stays strictly below the required one, which is at least 59/25.

theorem CKN.Core.Step4.fixedScale_pressure_exponent_suffices {κ : ℝ} (hκ : κ ≤ 25 / 9) (hκpos : 0 < κ) : 5 - 6 / κ ≤ 17 / 5

The fixed-scale balance: the radius power 17/5 produced by a spatially bounded, L^{3/2}-in-time pressure majorant dominates the requirement for every admissible gradient Morrey exponent, with the strict margin 14/25 already at the top of the range.