Positivity of the constants and scales used by the above-two phases.

theorem V7.Stage4AboveTwo.uniformConstant_pos {p : ℝ} (hp : 2 < p) : 0 < aboveUniformConstant p

theorem V7.Stage4AboveTwo.errorPower_gt_one {p : ℝ} (hp : 2 < p) : 1 < aboveErrorPower p

theorem V7.Stage4AboveTwo.errorConstant_pos {p : ℝ} (hp : 2 < p) : 0 < aboveErrorConstant p

theorem V7.Stage4AboveTwo.budgetConstant_pos {p : ℝ} (hp : 2 < p) : 0 < aboveBudgetConstant p

theorem V7.Stage4AboveTwo.budgetExponent_pos {p : ℝ} (hp : 2 < p) : 0 < aboveBudgetExponent p

theorem V7.Stage4AboveTwo.budgetExponent_lt_one {p : ℝ} (hp : 2 < p) : aboveBudgetExponent p < 1

theorem V7.Stage4AboveTwo.errorPower_mul_budgetExponent {p : ℝ} (hp : 2 < p) : aboveErrorPower p * aboveBudgetExponent p = 1

theorem V7.Stage4AboveTwo.growthConstant_pos {p : ℝ} (hp : 2 < p) : 0 < aboveGrowthConstant p

theorem V7.Stage4AboveTwo.hpConstant_pos {p : ℝ} (hp : 2 < p) : 0 < aboveHp p

theorem V7.Stage4AboveTwo.conjugate_pos {p : ℝ} (hp : 2 < p) : 0 < conjugateExponent p

theorem V7.Stage4AboveTwo.jpConstant_pos {p : ℝ} (hp : 2 < p) : 0 < aboveJp p

theorem V7.Stage4AboveTwo.gamma_pos {p eta : ℝ} {n : ℕ} (hp : 2 < p) (heta : 0 < eta) (hn : 1 ≤ n) : 0 < aboveGamma p eta n