The pointwise primal-dual residual identity for the above-two coefficient recurrences.

theorem V7.Stage4AboveTwoIdentity.alpha_weighted_primal {d : ℕ} (n : ℕ) (u dw : ScalarSeq) (alpha c b : ScalarMatrix) (hcoeff : AboveCoefficientAssumptions n u dw alpha c b) (A : VectorSeq d) (k : ℕ) (hk : k < n) : weightedSum (k + 1) (alpha (k + 1)) A = dw k • A k

theorem V7.abovePointwiseResidualIdentity : AbovePointwiseResidualIdentityStatement