max is the maximum value over (start_time, end_time].
@$pb.TagNumber(13) $core.double get max => $_getN(12);
@$pb.TagNumber(13) set max($core.double v) { $_setDouble(12, v); }