The above-two dual trajectory satisfies the terminal row, query, and energy identities.

theorem V7.Stage4AboveTwoDualPhase.terminal_row {d : ℕ} (n : ℕ) (hn : 1 ≤ n) (u dw : ScalarSeq) (alpha c b : ScalarMatrix) (hcoeff : AboveCoefficientAssumptions n u dw alpha c b) (G r : VectorSeq d) (hr0 : r 0 = -b n n • G 0) (hr : ∀ k < n, r (k + 1) = r k - weightedSum (k + 2) (fun (i : ℕ) => b (n - i) (n - 1 - k)) G) : r n = G n

theorem V7.Stage4AboveTwoDualPhase.dualResidual_lower {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (hn : 1 ≤ n) (u dw : ScalarSeq) (alpha c b : ScalarMatrix) (hcoeff : AboveCoefficientAssumptions n u dw alpha c b) (C D : VectorSeq d) : (AboveDualResidual p n u alpha b C D fun (y : Point d) => aboveUniformConstant p * lpNorm p y ^ p) ≥ -aboveErrorSum p n u dw

theorem V7.Stage4AboveTwoDualPhase.terminalRowAndQuery {d : ℕ} (p : ℝ) (n : ℕ) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) : data.r n = data.G n ∧ QueriedAt data.trace n (data.q n) ∧ data.G n = data.oracle.gradient (data.q n)

theorem V7.Stage4AboveTwoDualPhase.dualTerminalEnergy {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) : aboveHstar p (data.oracle.gradient (data.q n)) ≤ (data.oracle.value (data.q 0) - sInf (Set.range data.oracle.value)) / data.u n + aboveErrorSum p n data.u data.dw

theorem V7.aboveDualTerminalRowAndQuery {d : ℕ} (p : ℝ) (n : ℕ) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) : data.r n = data.G n ∧ QueriedAt data.trace n (data.q n) ∧ data.G n = data.oracle.gradient (data.q n)

theorem V7.aboveDualTerminalEnergy {d : ℕ} (p : ℝ) (hp : 2 < p) (n : ℕ) (data : AboveDualPhaseData p d n) (hass : AboveDualPhaseAssumptions data) : aboveHstar p (data.oracle.gradient (data.q n)) ≤ (data.oracle.value (data.q 0) - sInf (Set.range data.oracle.value)) / data.u n + aboveErrorSum p n data.u data.dw