The deterministic strict method's exact transcript against the affine oracle.

def V7.Stage6StrictDeterministic.causalQuery (method : StrictLocalMethod) (t : ℕ) (trace : StrictTranscript) : StrictPoint

The query selected after a chronological prefix. At time zero the frozen strict model requires the supplied initial point.

Equations

• V7.Stage6StrictDeterministic.causalQuery method t trace = if t = 0 then method.x0 else method.nextQuery trace

noncomputable def V7.Stage6StrictDeterministic.affineTrace (method : StrictLocalMethod) (eps : ℝ) : ℕ → StrictTranscript

Chronological exact transcript generated against the affine oracle.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage6StrictDeterministic.affineTrace method eps 0 = []

@[simp]

theorem V7.Stage6StrictDeterministic.affineTrace_zero (method : StrictLocalMethod) (eps : ℝ) : affineTrace method eps 0 = []

theorem V7.Stage6StrictDeterministic.affineTrace_succ (method : StrictLocalMethod) (eps : ℝ) (n : ℕ) : affineTrace method eps (n + 1) = affineTrace method eps n ++ [O3.PairOracle.observe (strictAffineOracle eps method.x0) (causalQuery method n (affineTrace method eps n))]

@[simp]

theorem V7.Stage6StrictDeterministic.affineTrace_length (method : StrictLocalMethod) (eps : ℝ) (n : ℕ) : List.length (affineTrace method eps n) = n

theorem V7.Stage6StrictDeterministic.affineTrace_exact (method : StrictLocalMethod) (eps : ℝ) (n : ℕ) : StrictTranscriptExact (strictAffineOracle eps method.x0) (affineTrace method eps n)

theorem V7.Stage6StrictDeterministic.affineTrace_take (method : StrictLocalMethod) (eps : ℝ) {m n : ℕ} (hmn : m ≤ n) : List.take m (affineTrace method eps n) = affineTrace method eps m

theorem V7.Stage6StrictDeterministic.affineTrace_get (method : StrictLocalMethod) (eps : ℝ) (n t : ℕ) (ht : t < n) : List.get (affineTrace method eps n) ⟨t, ⋯⟩ = O3.PairOracle.observe (strictAffineOracle eps method.x0) (causalQuery method t (affineTrace method eps t))

theorem V7.Stage6StrictDeterministic.affineTrace_runConsistent (method : StrictLocalMethod) (eps : ℝ) (n : ℕ) : StrictRunConsistent method (strictAffineOracle eps method.x0) (affineTrace method eps n)