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

theorem V7.Stage3BelowTwo.alpha_weighted_primal {d : ℕ} (n : ℕ) (u dw : ScalarSeq) (alpha c b : ScalarMatrix) (hcoeff : BelowCoefficientAssumptions 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.belowPointwiseResidualIdentity : BelowPointwiseResidualIdentityStatement