The finite Euclidean query programs evaluate to the literal source reports.

@[instance_reducible]

noncomputable def V7.Stage1E03.refinementPropDecidable (q : Prop) : Decidable q

Classical proposition decisions used locally in the program refinement proof.

Equations

• V7.Stage1E03.refinementPropDecidable q = Classical.propDecidable q

def V7.Stage1E03.prependReport {d : ℕ} (history : List (Observation d)) (guards : List (ObservableGuardCheck d)) (tail : TrialReport d) : TrialReport d

A report with earlier observations and checked guards prepended.

Equations

• V7.Stage1E03.prependReport history guards tail = { trace := history ++ tail.trace, checkedGuards := guards ++ tail.checkedGuards, outcome := tail.outcome }

noncomputable def V7.Stage1E03.sourceTerminalReport {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (U : Point d) : TrialReport d

The source terminal-query report, determined by the descent guard and gradient accuracy.

Equations

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

noncomputable def V7.Stage1E03.sourcePhaseBSuffix {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (U : Point d) : TrialReport d

The source phase-B suffix that checks interpolation before terminal descent.

Equations

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

noncomputable def V7.Stage1E03.sourcePhaseBReport {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (U : Point d) : TrialReport d

The source OGM-G report with its new observations and concluding checks.

Equations

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

noncomputable def V7.Stage1E03.sourcePhaseAReport {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) : ℕ → ℕ → TrialReport d

The recursively assembled source report for the remaining estimate phase and OGM-G.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage1E03.sourcePhaseAReport inst eps M n x✝ 0 = V7.Stage1E03.sourcePhaseBReport inst eps M n (V7.Stage1E03.sourceEstimateState inst.oracle M x0 n).accelerated

@[simp]

theorem V7.Stage1E03.ogmgStep_eq_source {d : ℕ} (n : ℕ) (oracle : PairOracle d) (M : ℝ) (U : Point d) (i : ℕ) : ogmgStep n M i (O3.ogmgState (O3.stage9ExecutionConfig n oracle M U) i) (O3.PairOracle.observe oracle (O3.ogmgState (O3.stage9ExecutionConfig n oracle M U) i).current) = O3.ogmgState (O3.stage9ExecutionConfig n oracle M U) (i + 1)

theorem V7.Stage1E03.allInterpolationChecks_eq_source {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (n : ℕ) (U : Point d) (obsAt : ℕ → Observation d) (hobs : ∀ i ≤ n, obsAt i = O3.PairOracle.observe inst.oracle (O3.ogmgState (O3.stage9ExecutionConfig n inst.oracle M U) i).current) : allInterpolationChecks n obsAt = allInterpolationChecks n fun (i : ℕ) => O3.PairOracle.observe inst.oracle (O3.ogmgState (O3.stage9ExecutionConfig n inst.oracle M U) i).current

theorem V7.Stage1E03.eval_terminal_eq_source {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (U : Point d) (obsAt : ℕ → Observation d) (history : List (Observation d)) (guards : List (ObservableGuardCheck d)) (hobs : obsAt n = O3.PairOracle.observe inst.oracle (O3.ogmgState (O3.stage9ExecutionConfig n inst.oracle M U) n).current) : Program.eval inst.oracle 1 (terminalProgram eps M n obsAt (O3.ogmgState (O3.stage9ExecutionConfig n inst.oracle M U) n) guards) history = prependReport history guards (sourceTerminalReport inst eps M n U)

theorem V7.Stage1E03.eval_phaseB_eq_source {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (U : Point d) (fuel i : ℕ) (exec : O3.OGMGExecutionState d) (obsAt : ℕ → Observation d) (history : List (Observation d)) (guards : List (ObservableGuardCheck d)) : i + fuel = n → exec = O3.ogmgState (O3.stage9ExecutionConfig n inst.oracle M U) i → (∀ j ≤ i, obsAt j = O3.PairOracle.observe inst.oracle (O3.ogmgState (O3.stage9ExecutionConfig n inst.oracle M U) j).current) → Program.eval inst.oracle (fuel + 1) (phaseBProgram eps M n i exec obsAt guards fuel) history = prependReport history guards (have cfg := O3.stage9ExecutionConfig n inst.oracle M U; have pre := List.map (fun (j : ℕ) => O3.PairOracle.observe inst.oracle (O3.ogmgState cfg (i + j + 1)).current) (List.range fuel); prependReport pre [] (sourcePhaseBSuffix inst eps M n U))

theorem V7.Stage1E03.eval_phaseA_eq_source {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n fuel k : ℕ) (last : Option (Observation d)) (history : List (Observation d)) (guards : List (ObservableGuardCheck d)) : k + fuel = n → (fuel = 0 → last = some (O3.PairOracle.observe inst.oracle (sourceEstimateState inst.oracle M x0 n).accelerated)) → Program.eval inst.oracle (phaseABudget n fuel) (phaseAProgram eps M x0 n k (sourceEstimateState inst.oracle M x0 k) last guards fuel) history = prependReport history guards (sourcePhaseAReport inst eps M n k fuel)

theorem V7.Stage1E03.eval_full_eq_source {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (hn : 0 < n) : Program.eval inst.oracle (phaseABudget n n) (phaseAProgram eps M x0 n 0 { accelerated := x0, cumulativeGradient := 0 } none [] n) [] = sourcePhaseAReport inst eps M n 0 n