The below-two dual trajectory has the required dynamics and exact chronological observations.

@[simp]

theorem V7.Stage3BelowTwoS3F.dualQ_zero {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : dualQ p n oracle 0 = 0

@[simp]

theorem V7.Stage3BelowTwoS3F.dualR_zero {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : dualR p n oracle 0 = -coeffB n n n • oracle.gradient 0

theorem V7.Stage3BelowTwoS3F.dualQ_succ {d : ℕ} (p : ℝ) (n k : ℕ) (oracle : PairOracle d) : dualQ p n oracle (k + 1) = dualQ p n oracle k - increment n (n - 1 - k) • belowMirrorMap p (dualR p n oracle k)

theorem V7.Stage3BelowTwoS3F.dualR_succ {d : ℕ} (p : ℝ) (n k : ℕ) (oracle : PairOracle d) : dualR p n oracle (k + 1) = dualR p n oracle k - weightedSum (k + 2) (fun (i : ℕ) => coeffB n (n - i) (n - 1 - k)) fun (i : ℕ) => oracle.gradient (dualQ p n oracle i)

theorem V7.Stage3BelowTwoS3F.antiDiagonal_alpha {d : ℕ} (n k : ℕ) (hk : k < n) (Z : VectorSeq d) : weightedSum (k + 1) (fun (i : ℕ) => alpha n (n - i) (n - 1 - k)) Z = increment n (n - 1 - k) • Z k

noncomputable def V7.Stage3BelowTwoS3F.dualTrace {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : List (Observation d)

The exact observations at all normalized dual queries through the horizon.

Equations

• V7.Stage3BelowTwoS3F.dualTrace p n oracle = List.map (fun (k : ℕ) => O3.PairOracle.observe oracle (V7.Stage3BelowTwoS3F.dualQ p n oracle k)) (List.range (n + 1))

noncomputable def V7.Stage3BelowTwoS3F.dualData {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : BelowDualData p d n

The concrete dual trajectories and coefficients packaged as below-two phase data.

Equations

• One or more equations did not get rendered due to their size.

theorem V7.Stage3BelowTwoS3F.dual_dynamics {d : ℕ} (p : ℝ) (n : ℕ) (hn : 1 ≤ n) (oracle : PairOracle d) : BelowDualDynamics (dualData p n oracle)

theorem V7.Stage3BelowTwoS3F.dual_trace_exact {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : TraceExact oracle (dualTrace p n oracle)

theorem V7.Stage3BelowTwoS3F.dual_trace_length {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) : (dualTrace p n oracle).length = n + 1

theorem V7.Stage3BelowTwoS3F.dual_queried_at {d : ℕ} (p : ℝ) (n : ℕ) (oracle : PairOracle d) (k : ℕ) (hk : k ≤ n) : QueriedAt (dualTrace p n oracle) k (dualQ p n oracle k)