The resisting prefix states synchronize their stored coordinates, signs, and observations.

theorem V7.Stage5AboveTwoLowerS5F.obsPrefix_succ {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : (prefixState P (t + 1)).obsPrefix = (prefixState P t).obsPrefix ++ [O3.PairOracle.observe (partialOracle P t) (query P t)]

theorem V7.Stage5AboveTwoLowerS5F.obsPrefix_eq_map_range {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : (prefixState P t).obsPrefix = List.map (fun (s : ℕ) => O3.PairOracle.observe (partialOracle P s) (query P s)) (List.range t)

The load-bearing causal invariant: the stored prefix is exactly the list of chronological partial-oracle observations appearing in the frozen carrier.

theorem V7.Stage5AboveTwoLowerS5F.query_chronology {p : ℝ} {d T : ℕ} (P : PrefixParameters p d T) (t : ℕ) : query P t = if t = 0 then 0 else P.algorithm.nextQuery 0 (List.map (fun (s : ℕ) => O3.PairOracle.observe (partialOracle P s) (query P s)) (List.range t))

theorem V7.Stage5AboveTwoLowerS5F.obsPrefix_take {p : ℝ} {d T : ℕ} {P : PrefixParameters p d T} {t u : ℕ} (htu : t ≤ u) : List.take t (prefixState P u).obsPrefix = (prefixState P t).obsPrefix

theorem V7.Stage5AboveTwoLowerS5F.obsPrefix_getElemOption {p : ℝ} {d T : ℕ} {P : PrefixParameters p d T} {s t : ℕ} (hst : s < t) : (prefixState P t).obsPrefix[s]? = some (O3.PairOracle.observe (partialOracle P s) (query P s))

theorem V7.Stage5AboveTwoLowerS5F.obsPrefix_ne_nil {p : ℝ} {d T : ℕ} {P : PrefixParameters p d T} {t : ℕ} (ht : 0 < t) : (prefixState P t).obsPrefix ≠ []