Lemma r.LeBron (lebron_step), conditional on Lemma U

lebron_step_of_lemmaU : LemmaUContract → LebronStepStatement β C₀.

• sup part: the step-down estimate (indystepdown), conjunct (i), with the iterate witness from RelativeError.exists_TIterates (classical solvability, AVenhance.classical_wellposed);
• Hölder-1/4 part: Lemma U for θ_m and θ_{m-1} with the uniform drift bound velBound β and the diffusivity window of kappaSeq_window;
• interpolation interpolate_holder with μ = δ/(8δ+4P), P = q(β+γ).

theorem AVenhance.Infra.FullTheorem.lebron_step_of_lemmaU (hU : LemmaUContract) (β C₀ : ℝ) : LebronStepStatement β C₀