The completed normalized resisting trace is exact, causal, and charges its initial query.

noncomputable def V7.Stage5AboveTwoLowerS5F.unitTrace (p : ℝ) (d T : ℕ) (algorithm : DeterministicExactPairAlgorithm d) (hT : 1 ≤ T) (hTd : T ≤ d) : List (Observation d)

The finite exact trace of the normalized completed resisting oracle.

Equations

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

theorem V7.Stage5AboveTwoLowerS5F.completed_partial_map_eq {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hp : 2 < p) (hd : 2 ≤ d) (hT : 1 ≤ T) (hTd : T ≤ d) {t : ℕ} (ht : t ≤ T) : List.map (fun (s : ℕ) => O3.PairOracle.observe (unitCompletionData p d T algorithm hT hTd).completedOracle ((unitCompletionData p d T algorithm hT hTd).queries s)) (List.range t) = List.map (fun (s : ℕ) => O3.PairOracle.observe ((unitCompletionData p d T algorithm hT hTd).partialOracle s) ((unitCompletionData p d T algorithm hT hTd).queries s)) (List.range t)

theorem V7.Stage5AboveTwoLowerS5F.unitTrace_take {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hT : 1 ≤ T) (hTd : T ≤ d) {t : ℕ} (ht : t ≤ T) : List.take t (unitTrace p d T algorithm hT hTd) = List.map (fun (s : ℕ) => O3.PairOracle.observe (unitCompletionData p d T algorithm hT hTd).completedOracle ((unitCompletionData p d T algorithm hT hTd).queries s)) (List.range t)

theorem V7.Stage5AboveTwoLowerS5F.unitTrace_generated {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hp : 2 < p) (hd : 2 ≤ d) (hT : 1 ≤ T) (hTd : T ≤ d) : GeneratedBy algorithm 0 (unitTrace p d T algorithm hT hTd)

theorem V7.Stage5AboveTwoLowerS5F.unitTrace_exact {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hT : 1 ≤ T) (hTd : T ≤ d) : TraceExact (unitCompletionData p d T algorithm hT hTd).completedOracle (unitTrace p d T algorithm hT hTd)

theorem V7.Stage5AboveTwoLowerS5F.unitTrace_head_point {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hT : 1 ≤ T) (hTd : T ≤ d) : Option.map O3.Observation.point (unitTrace p d T algorithm hT hTd).head? = some 0

theorem V7.Stage5AboveTwoLowerS5F.unitChargedRun {p : ℝ} {d T : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (hp : 2 < p) (hd : 2 ≤ d) (hT : 1 ≤ T) (hTd : T ≤ d) : ChargedKnownParameterRun algorithm 0 (unitCompletionData p d T algorithm hT hTd).completedOracle (unitTrace p d T algorithm hT hTd)