Uniform shift room for the recursive packet estimates in the manuscript.

def EulerPacketShiftArithmetic.highShift (p : ℕ) : ℕ

High shift, given by 100*p-80.

Equations

• EulerPacketShiftArithmetic.highShift p = 100 * p - 80

def EulerPacketShiftArithmetic.meanShift (p : ℕ) : ℕ

Mean shift, given by 100*p-140.

def EulerPacketShiftArithmetic.highForceShift (p : ℕ) : ℕ

High force shift, given by highShift p-10.

Equations

• EulerPacketShiftArithmetic.highForceShift p = EulerPacketShiftArithmetic.highShift p - 10

def EulerPacketShiftArithmetic.meanForceShift (p : ℕ) : ℕ

Mean force shift, given by meanShift p-10.

Equations

• EulerPacketShiftArithmetic.meanForceShift p = EulerPacketShiftArithmetic.meanShift p - 10

theorem EulerPacketShiftArithmetic.primary_shift : highShift 1 = 20

theorem EulerPacketShiftArithmetic.slow_high_high_room (i j p : ℕ) (hi : 1 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : highShift i + highShift j + 2 + 8 ≤ meanForceShift p

theorem EulerPacketShiftArithmetic.slow_mean_high_room (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hp : i + j = p) : meanShift i + highShift j + 2 + 8 ≤ meanForceShift p

theorem EulerPacketShiftArithmetic.slow_mean_mean_room (i j p : ℕ) (hi : 2 ≤ i) (hj : 2 ≤ j) (hp : i + j = p) : meanShift i + meanShift j + 2 + 8 ≤ meanForceShift p

theorem EulerPacketShiftArithmetic.fast_mean_high_room (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) : meanShift i + highShift j + 2 + 8 ≤ highForceShift p

theorem EulerPacketShiftArithmetic.fast_corrector_high_room (i j p : ℕ) (hi : 2 ≤ i) (hj : 1 ≤ j) (hp : i + j = p + 1) : highShift (i - 1) + highShift j + 2 + 8 ≤ meanForceShift p

theorem EulerPacketShiftArithmetic.fast_corrector_corrector_room (i j p : ℕ) (hi : 2 ≤ i) (hj : 2 ≤ j) (hp : i + j = p + 1) : highShift (i - 1) + highShift (j - 1) + 2 + 8 ≤ meanForceShift p

theorem EulerPacketShiftArithmetic.previous_linear_room (p : ℕ) (hp : 2 ≤ p) : highShift (p - 1) + 2 + 8 ≤ meanForceShift p

theorem EulerPacketShiftArithmetic.mean_force_le_high_force (p : ℕ) : meanForceShift p ≤ highForceShift p

theorem EulerPacketShiftArithmetic.force_shift_dominates_grade (p : ℕ) (hp : 2 ≤ p) : 25 * p ≤ meanForceShift p ∧ 25 * p ≤ highForceShift p