Uniform interior Morrey decay near the top boundary #
The heart of the uniform interior route to CIV.timeZeroSingularSetNull: from top-cylinder gradient
smallness at the top time slice above an interior point x (uniform in the base scale up to
r₀), together with the global energy class and a C^2-bounded force, there are a radius
r₅, a Morrey constant M₁ and a time window (-σ, 0), all independent of the interior time
s, such that the three scale-invariant quantities α, β, δ² decay like r^{2/5} at every
point (x, s) with s in that window and every scale r ≤ r₅.
The proof follows the order fixed by the route review: the absolute decay constant C₂₇ (and
the paired C₂₈) are obtained once from the CKN manuscript's one-step theta-decay inequality
and threaded through both the finite descent and the below-r₅ iteration; a scale r₄ is
fixed so small that the force term is controlled at both thresholds; the uniform crude bound
Θ_bar at r₄ is combined with a finite, entrance-controlled descent (the entrance holds only
while the base time is within ρ² of the top, which is exactly what bounds the number of
descent steps) to reach r₅ := κ^N r₄ with θ ≤ η; and the CKN manuscript's iteration
proposition, which needs no further gradient smallness, supplies the Morrey decay below r₅.
The iteration phase is discharged through the general-purpose engine CKN.iteration_of_thetaDecay
rather than the convenience wrapper CKN.iteration_of_sws_absolute: the wrapper re-derives its
own existential witness for C₂₇ internally, which cannot be forced to coincide with the C₂₇
already fixed from the raw one-step decay used by the descent phase. Feeding the same C₂₇,
C₂₈ and the same raw decay fact to CKN.iteration_of_thetaDecay directly is the only way to
honor the "thread the same C₂₇" requirement of the route review; it is also exactly what the
wrapper's own proof does internally.
Helper A: local reproof of the private gradient-comparison bound #
The spatial-gradient integrand of the energy class is finite over the unit cylinder,
via the pointwise comparison with the enorm gradient and the energy class's own finite
H¹ conjunct.
The entrance step: an off-centre cylinder Q_ρ(x,s) whose base time s is no more than
ρ² below the top boundary sits inside the top-cylinder gradient-smallness hypothesis at the
enlarged radius √2 ρ, and the β-scale quantity there is bounded by ε_*.
Helper D: a small radius with a cubic force bound #
Helper E: the step count from the descent contraction #
A pure real-number existence lemma, via the descent contraction of the CKN
manuscript's iteration proposition: given a nonnegative crude bound Θ_bar at the initial
scale and a sufficiently small forcing budget, there is a step count N after which the
geometric bound, together with its residual forcing slack, sits below η.
The finite descent, extracted as its own declaration for elaboration budget #
The finite descent from the crude bound Θ_bar at scale r₄ to scale κ^N r₄, valid on the
time window forced by N itself. Extracted from the main proof so that its induction gets an
independent elaboration budget.
The crude uniform bound at the fixed scale r₄, extracted for elaboration budget #
The uniform crude bound Θ_bar on θ at the fixed scale r₄, valid for every qualifying
time s, built from the three uniform crude bounds of CIV.Regularity.UniformCrudeBounds.
The Morrey decay below r₅, extracted for elaboration budget #
Once the descent has produced r₅ with θ(x,s;r₅) ≤ η for every qualifying s, the
iteration proposition of the CKN manuscript (needing no further gradient smallness) gives the
Morrey decay for every scale r ≤ r₅.