The ordered guard evaluator records exactly the accepted prefix and first failure.

theorem V7.Stage1E03.checkHolds_exact_iff {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (kind : ObservableGuardKind) (x y : Point d) : CheckHolds p M (exactGuardCheck kind oracle x y) ↔ ¬GuardFails p M oracle (exactGuardCheck kind oracle x y).failure

theorem V7.Stage1E03.upperCheck_exact {d : ℕ} (oracle : PairOracle d) (x y : Point d) : upperCheck (O3.PairOracle.observe oracle x) (O3.PairOracle.observe oracle y) = exactGuardCheck ObservableGuardKind.upperModel oracle x y

theorem V7.Stage1E03.interpolationCheck_exact {d : ℕ} (oracle : PairOracle d) (x y : Point d) : interpolationCheck (O3.PairOracle.observe oracle x) (O3.PairOracle.observe oracle y) = exactGuardCheck ObservableGuardKind.interpolation oracle x y

theorem V7.Stage1E03.terminalCheck_exact {d : ℕ} (oracle : PairOracle d) (x y : Point d) : terminalCheck (O3.PairOracle.observe oracle x) (O3.PairOracle.observe oracle y) = exactGuardCheck ObservableGuardKind.terminalDescent oracle x y

theorem V7.Stage1E03.evaluateChecks_ok_iff {d : ℕ} (p M : ℝ) (checks passed : List (ObservableGuardCheck d)) : evaluateChecks p M checks = Except.ok passed ↔ passed = checks ∧ ∀ check ∈ checks, CheckHolds p M check

theorem V7.Stage1E03.evaluateChecks_error_characterization {d : ℕ} (p M : ℝ) (checks prior : List (ObservableGuardCheck d)) (failed : ObservableGuardCheck d) : evaluateChecks p M checks = Except.error (prior, failed) → prior <+: checks ∧ prior.getLast? = some failed ∧ (∀ check ∈ prior.dropLast, CheckHolds p M check) ∧ ¬CheckHolds p M failed

theorem V7.Stage1E03.evaluateChecks_error_prefix {d : ℕ} (p M : ℝ) {checks prior : List (ObservableGuardCheck d)} {failed : ObservableGuardCheck d} : evaluateChecks p M checks = Except.error (prior, failed) → prior <+: checks

theorem V7.Stage1E03.evaluateChecks_error_last {d : ℕ} (p M : ℝ) {checks prior : List (ObservableGuardCheck d)} {failed : ObservableGuardCheck d} : evaluateChecks p M checks = Except.error (prior, failed) → prior.getLast? = some failed

theorem V7.Stage1E03.evaluateChecks_error_prior_pass {d : ℕ} (p M : ℝ) {checks prior : List (ObservableGuardCheck d)} {failed : ObservableGuardCheck d} : evaluateChecks p M checks = Except.error (prior, failed) → ∀ check ∈ prior.dropLast, CheckHolds p M check

theorem V7.Stage1E03.evaluateChecks_error_failed {d : ℕ} (p M : ℝ) {checks prior : List (ObservableGuardCheck d)} {failed : ObservableGuardCheck d} : evaluateChecks p M checks = Except.error (prior, failed) → ¬CheckHolds p M failed