Dependency-pure causal machine for the frozen V7 Euclidean trial.

@[instance_reducible]

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

Classical proposition decisions used locally to evaluate observable guards.

Equations

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

noncomputable def V7.Stage1E03.CheckHolds {d : ℕ} (p M : ℝ) (check : ObservableGuardCheck d) : Prop

The selected observable inequality evaluated solely from its recorded observations.

Equations

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

noncomputable def V7.Stage1E03.upperCheck {d : ℕ} (oy ox : Observation d) : ObservableGuardCheck d

An upper-model guard formed from the query and proposed next-point observations.

Equations

• V7.Stage1E03.upperCheck oy ox = { kind := V7.ObservableGuardKind.upperModel, xPair := oy, yPair := ox }

noncomputable def V7.Stage1E03.interpolationCheck {d : ℕ} (oi oj : Observation d) : ObservableGuardCheck d

A Euclidean interpolation guard formed from two observations.

Equations

• V7.Stage1E03.interpolationCheck oi oj = { kind := V7.ObservableGuardKind.interpolation, xPair := oi, yPair := oj }

noncomputable def V7.Stage1E03.terminalCheck {d : ℕ} (on ov : Observation d) : ObservableGuardCheck d

A terminal-descent guard formed from the final query and gradient-step observations.

Equations

• V7.Stage1E03.terminalCheck on ov = { kind := V7.ObservableGuardKind.terminalDescent, xPair := on, yPair := ov }

noncomputable def V7.Stage1E03.allInterpolationChecks {d : ℕ} (n : ℕ) (obsAt : ℕ → Observation d) : List (ObservableGuardCheck d)

The ordered list of interpolation checks for every pair through horizon n.

Equations

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

noncomputable def V7.Stage1E03.evaluateChecks {d : ℕ} (p M : ℝ) : List (ObservableGuardCheck d) → Except (List (ObservableGuardCheck d) × ObservableGuardCheck d) (List (ObservableGuardCheck d))

Pure inspection: the error branch is exactly the prefix through the first failed current-V7 point-carrying guard.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage1E03.evaluateChecks p M [] = Except.ok []

noncomputable def V7.Stage1E03.horizon (eps M D : ℝ) : ℕ

The ceiling of the Euclidean trial's accuracy-dependent iteration horizon.

Equations

• V7.Stage1E03.horizon eps M D = ⌈2 * √(M * D / eps)⌉₊

theorem V7.Stage1E03.horizon_real_ge (eps M D : ℝ) : 2 * √(M * D / eps) ≤ ↑(horizon eps M D)

theorem V7.Stage1E03.one_le_horizon {eps M D : ℝ} (hkappa : 1 ≤ M * D / eps) : 1 ≤ horizon eps M D

theorem V7.Stage1E03.horizon_gradient_budget {eps M D : ℝ} (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (hkappa : 1 ≤ M * D / eps) : have n := horizon eps M D; 2 * √2 * M * D / ((↑n + 1) * (↑n + 1)) ≤ eps

noncomputable def V7.Stage1E03.nextEstimateState {d : ℕ} (M : ℝ) (x0 : Point d) (k : ℕ) (state : O3.EuclideanEstimateState d) (oy : Observation d) : O3.EuclideanEstimateState d

The next accelerated estimate state after receiving a query observation.

Equations

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

noncomputable def V7.Stage1E03.estimateQuery {d : ℕ} (M : ℝ) (x0 : Point d) (k : ℕ) (state : O3.EuclideanEstimateState d) : Point d

The estimate-sequence query formed from the current accelerated point and quadratic minimizer.

Equations

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

noncomputable def V7.Stage1E03.ogmgStep {d : ℕ} (n : ℕ) (M : ℝ) (i : ℕ) (state : O3.OGMGExecutionState d) (oi : Observation d) : O3.OGMGExecutionState d

One OGM-G state update using the observed gradient and prescribed momentum coefficients.

Equations

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

noncomputable def V7.Stage1E03.terminalProgram {d : ℕ} (eps M : ℝ) (n : ℕ) (obsAt : ℕ → Observation d) (exec : O3.OGMGExecutionState d) (guards : List (ObservableGuardCheck d)) : Program d 1

The final one-query program checking descent and selecting the terminal outcome.

Equations

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

noncomputable def V7.Stage1E03.phaseBProgram {d : ℕ} (eps M : ℝ) (n i : ℕ) (exec : O3.OGMGExecutionState d) (obsAt : ℕ → Observation d) (guards : List (ObservableGuardCheck d)) (fuel : ℕ) : Program d (fuel + 1)

The finite OGM-G query program followed by interpolation and terminal-descent checks.

Equations

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

def V7.Stage1E03.phaseABudget (n : ℕ) : ℕ → ℕ

The query bound for the remaining estimate phase and the following OGM-G phase.

Equations

• V7.Stage1E03.phaseABudget n 0 = n + 1
• V7.Stage1E03.phaseABudget n fuel.succ = V7.Stage1E03.phaseABudget n fuel + 2

noncomputable def V7.Stage1E03.phaseAProgram {d : ℕ} (eps M : ℝ) (x0 : Point d) (n k : ℕ) (estimate : O3.EuclideanEstimateState d) (last : Option (Observation d)) (guards : List (ObservableGuardCheck d)) (fuel : ℕ) : Program d (phaseABudget n fuel)

The estimate-phase query program, which checks each upper model before continuing.

Equations

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

noncomputable def V7.Stage1E03.euclideanLocalTrial {d : ℕ} (eps : ℝ) (x0 : Point d) (n : ℕ) : LocalTrial d

The Euclidean local trial with a fixed planned horizon.

Equations

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