The parabolic-boundary bound for a scalar on the meridional half-disc

A scalar field g of class C¹ on the unit cylinder, read along the meridional embedding, is bounded on the parabolic boundary axisParabolicBoundary R_* t_η s of CIV.axisMaximumPrinciple by max (M_b, M_i): the lateral bound M_b on the half-circle {r² + z² = R_*²} for t_η < t ≤ s, the initial bound M_i on the open ball at t = t_η, and, at the corner where the two pieces meet, the initial bound again, carried to the boundary sphere by continuity along the radial segment c ↦ c·(r, z).

This is the scalar form of the swirl-profile boundary bound of CIV/Closure/SwirlBound.lean, stripped of the (−t)^η weight and of the component selection, so that the circulation instantiation of lem:aniso:axis can consume it directly.

theorem CIV.abs_scalar_boundary_corner_le (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hg1 : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (Rstar τ Mi : ℝ) (hRpos : 0 < Rstar) (hR1 : Rstar < 1) (hτ1 : -1 < τ) (hτ2 : τ < 0) (hinit : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, |g (x, τ)| ≤ Mi) (r z : ℝ) (hrz : r ^ 2 + z ^ 2 = Rstar ^ 2) : |g (meridional r z, τ)| ≤ Mi

At a corner point of the parabolic boundary — radius exactly R_*, time exactly the initial time τ — the initial bound M_i, which is hypothesised on the open ball only, still holds, by continuity of g (·, τ) along the radial segment.

theorem CIV.abs_scalar_meridional_le_boundary (g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hg1 : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => g z) unitCylinder) (Rstar tη : ℝ) (hRpos : 0 < Rstar) (hR1 : Rstar < 1) (htη1 : -1 < tη) (htη2 : tη < 0) (Mb Mi : ℝ) (hbdry : ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm x = Rstar → ∀ t ∈ Set.Ioo tη 0, |g (x, t)| ≤ Mb) (hinit : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, |g (x, tη)| ≤ Mi) (s : ℝ) (hs0 : s < 0) (p : (ℝ × ℝ) × ℝ) : p ∈ axisParabolicBoundary Rstar tη s → |g (meridional p.1.1 p.1.2, p.2)| ≤ max Mb Mi

The parabolic-boundary bound: on axisParabolicBoundary R_* t_η s, the meridional reading of g is bounded by max (M_b, M_i).