Physical estimates on the actual shortened parent state.

theorem EulerPacketInduction.Stage.restricted_gradient_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (t : ↑(Set.Icc 0 P.restrictedParent.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => P.restrictedState.evolution.velocity (↑t, y)) x‖ ≤ EulerPacketLowConstants.gradientConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n

theorem EulerPacketInduction.Stage.restricted_hessian_bound {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) (t : ↑(Set.Icc 0 P.restrictedParent.T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (P.restrictedState.evolution.force t) x‖ ≤ EulerPacketLowConstants.hessianConstant * EulerPacketSourceScaleSequence.previousShear S.J S.X n * EulerPacketSourceScaleSequence.olderShear S.J S.X n

theorem EulerPacketInduction.Stage.restricted_horizon_reciprocal {c B : ℝ} {S : EulerPacketInductionScales.Scales c B} {n : ℕ} (P : Stage S n) : P.restrictedParent.T⁻¹ ≤ 12 / EulerPacketBaseGuardScales.baseHorizon S.J S.X