Numerical absorption in the sharp gradient and Hessian bounds, and the common localized coercivity guard for all nested horizons.

theorem EulerPacketLowBoundPropagation.gradient_bound (CM hprev hchild g b e : ℝ) (hCM : 4 ≤ CM) (hp : 1 ≤ hprev) (hc : 1 ≤ hchild) (hscale : hprev ^ 2 ≤ hchild / 4) (hg : 4 * g ≤ CM) (hbad : hchild * b + e ≤ 1) : CM * hprev + hchild * (g + b) + e ≤ CM * hchild

theorem EulerPacketLowBoundPropagation.hessian_bound (CM CH hprev hold hchild g b e : ℝ) (hCH : 4 ≤ CH) (hp : 1 ≤ hprev) (hc : 1 ≤ hchild) (hhold : hold ≤ hprev) (hscale : hprev ^ 2 ≤ hchild / 4) (hg : 8 * CM * g ≤ CH) (hbad : 2 * CM * hprev * hchild * b + e ≤ 1) : CH * hprev * hold + 2 * CM * hprev * hchild * (g + b) + e ≤ CH * hchild * hprev

theorem EulerPacketLowBoundPropagation.localized_cost_le (J : ℕ) (X K Be Bc Kcap Becap CM Cboundary T : ℝ) (hK : 0 ≤ K) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hT : 0 ≤ T) (hC : 0 ≤ Cboundary) (hr : 0 ≤ EulerPacketBaseGuardScales.baseRadius X) (hKT : K ≤ Kcap) (hBeT : Be ≤ Becap) (hBcT : Bc ≤ CM * X ^ 1000 + 2) (hTS : T ≤ EulerPacketBaseGuardScales.baseHorizon J X) : K * (T ^ 2 / 2) + Be * T + Cboundary * Bc * EulerPacketBaseGuardScales.baseRadius X ^ 3 * T ≤ EulerPacketBaseGuardScales.baseGuardCost J Kcap Becap CM Cboundary X

theorem EulerPacketLowBoundPropagation.localized_guard (J : ℕ) (X K Be Bc Kcap Becap CM Cboundary T : ℝ) (hK : 0 ≤ K) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hT : 0 ≤ T) (hC : 0 ≤ Cboundary) (hr : 0 ≤ EulerPacketBaseGuardScales.baseRadius X) (hKT : K ≤ Kcap) (hBeT : Be ≤ Becap) (hBcT : Bc ≤ CM * X ^ 1000 + 2) (hTS : T ≤ EulerPacketBaseGuardScales.baseHorizon J X) (hbase : EulerPacketBaseGuardScales.baseGuardCost J Kcap Becap CM Cboundary X ≤ 1 / 2) : K * (T ^ 2 / 2) + Be * T + Cboundary * Bc * EulerPacketBaseGuardScales.baseRadius X ^ 3 * T ≤ 1 / 2