Pressure gauge covariance on clipped origin cells

A spatial constant is removed from the harmonic remainder on each slice; its gradient, the divergence source, and the force potentials are unchanged. The pressure mean is taken on the fixed carrier ball vec3Ball 0 R₁, so all cells use one pressure normalization in the clipped carrier integral. The argument is slicewise and requires no temporal integrability of the gauge.

theorem CKN.Core.Step4.origin_fixed_gradient_slice_bound_gauge_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) (γ : ℝ → ℝ) {B : Set Foundation.Parabolic.Vec3} {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hball : euclideanBall z.1 (ρ / 2) ⊆ B) (hfield : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (k : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => Dp (x, s) k) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (k : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ originSliceGradientMajorant u Du (fun (w : Foundation.Parabolic.ParabolicPoint) => p w - γ w.2) f z hρ s

The same fixed weak pressure gradient obeys the slice bound with any spatially constant gauge removed from the pressure in the majorant. No time regularity of the gauge is needed for this almost-everywhere slice statement.

noncomputable def CKN.Core.Step4.originClauseGaugeMajorant (R₁ : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {ρ : ℝ} (hρ : 0 < ρ) (s : ℝ) : ENNReal

The explicit slice majorant with the pressure mean on the fixed origin carrier removed. The source and force terms keep their original values.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.originClauseGaugeCarrierCellIntegral_le_of_double_radius {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R₁ : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hR₁ : 0 ≤ R₁) (hR₁one : R₁ ≤ 1) (hI : Set.Icc (-1) 0 ⊆ I) {x : Foundation.Parabolic.Vec3} {t r : ℝ} (hr : 0 < r) (hsub : closure (Foundation.Parabolic.parabolicCylinder x t (2 * r)) ⊆ spaceTimeSet Ω I) {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {i : Fin 3} (hDmeas : AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) (hfield : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x t r ∩ Foundation.Parabolic.parabolicCylinder 0 0 R₁, ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t ∩ Set.Ioc (-R₁ ^ 2) 0, originClauseGaugeMajorant R₁ u Du p f (x, t) ⋯ s ^ (6 / 5)

The clipped carrier-cell integral bound with the pressure mean removed, obtained by applying the doubled-radius integral consumer to the slice estimate.

theorem CKN.Core.Step4.originClauseGauge_doubleRadius_subset_unit {R₁ r : ℝ} {z : Foundation.Parabolic.ParabolicPoint} (hR₁ : 0 < R₁) (hR₁one : R₁ < 1) (hr : 0 < r) (hmargin : r ≤ (1 - R₁) / 2) (hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁)) : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 (2 * r)) ⊆ closure (Foundation.Parabolic.parabolicCylinder 0 0 1)

The doubled source geometry is unchanged by pressure normalization.

theorem CKN.Core.Step4.originClauseGaugeCarrierCellIntegral_le_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R₁ : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR₁ : 0 < R₁) (hR₁one : R₁ < 1) {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {i : Fin 3} (hDmeas : AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) (hfield : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) {z : Foundation.Parabolic.ParabolicPoint} {r : ℝ} (hr : 0 < r) (hmargin : r ≤ 2 * ((1 - R₁) / 4)) (hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁)) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ Foundation.Parabolic.parabolicCylinder 0 0 R₁, ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, originClauseGaugeMajorant R₁ u Du p f z ⋯ s ^ (6 / 5)

Suitability supplies the doubled-radius slice estimate for a clipped origin cell with its fixed carrier pressure mean removed, while the fixed derivative is required only on the carrier ball.

theorem CKN.Core.Step4.originClauseGauge_exists_doubled_cell_bounds_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R₁ : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR₁ : 0 < R₁) (hR₁one : R₁ < 1) : ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) ∧ ∀ z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁), ∀ (r : ℝ) (hr : 0 < r), r ≤ 2 * ((1 - R₁) / 4) → ∀ (i : Fin 3), ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r ∩ Foundation.Parabolic.parabolicCylinder 0 0 R₁, ENNReal.ofReal |Dp w i| ^ (6 / 5) ≤ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, originClauseGaugeMajorant R₁ u Du p f z ⋯ s ^ (6 / 5)

One measurable carrier gradient, obtained from suitability, satisfies all mean-subtracted clipped cell estimates through twice the origin margin scale.