Finite causal query programs implementing the below-two primal and dual phases.

@[instance_reducible]

noncomputable def V7.Stage3BelowTwoS3F.machinePropDecidable (q : Prop) : Decidable q

Classical proposition decisions used locally by the below-two trial machine.

Equations

• V7.Stage3BelowTwoS3F.machinePropDecidable q = Classical.propDecidable q

noncomputable def V7.Stage3BelowTwoS3F.normalizedGradient {d : ℕ} (M D : ℝ) (obs : Observation d) : Point d

The observed physical gradient rescaled into normalized trial coordinates.

Equations

• V7.Stage3BelowTwoS3F.normalizedGradient M D obs = (1 / (M * D)) • obs.gradient

noncomputable def V7.Stage3BelowTwoS3F.cocoCheck {d : ℕ} (before after : Observation d) : ObservableGuardCheck d

The cocoercivity guard formed from consecutive observations.

Equations

• V7.Stage3BelowTwoS3F.cocoCheck before after = { kind := V7.ObservableGuardKind.cocoercivity, xPair := before, yPair := after }

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

The cocoercivity inequality reconstructed from a guard's two recorded observations.

Equations

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

noncomputable def V7.Stage3BelowTwoS3F.cocoPairHolds {d : ℕ} (p M : ℝ) (before after : Observation d) : Prop

The form actually evaluated by the machine, written directly from the two returned exact pairs.

Equations

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

noncomputable def V7.Stage3BelowTwoS3F.dualProgram {d : ℕ} (p eps M D : ℝ) (n k : ℕ) (center q r : Point d) (G : VectorSeq d) (previous : Observation d) (guards : List (ObservableGuardCheck d)) (fuel : ℕ) : Program d fuel

The below-two dual query program with early accuracy or guard-failure termination.

Equations

• One or more equations did not get rendered due to their size.
• V7.Stage3BelowTwoS3F.dualProgram p eps M D n k center q r G previous guards 0 = V7.CausalProgram.Program.finish guards (V7.TrialOutcome.radius previous)

def V7.Stage3BelowTwoS3F.phaseOneBudget (n : ℕ) : ℕ → ℕ

The remaining primal query budget plus the complete dual query budget.

Equations

• V7.Stage3BelowTwoS3F.phaseOneBudget n 0 = n
• V7.Stage3BelowTwoS3F.phaseOneBudget n fuel.succ = V7.Stage3BelowTwoS3F.phaseOneBudget n fuel + 1

noncomputable def V7.Stage3BelowTwoS3F.phaseOneProgram {d : ℕ} (p eps M D : ℝ) (x0 : Point d) (n k : ℕ) (state : PrimalState d) (previous : Observation d) (guards : List (ObservableGuardCheck d)) (fuel : ℕ) : Program d (phaseOneBudget n fuel)

The below-two primal query program that passes its endpoint to the dual phase.

Equations

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

noncomputable def V7.Stage3BelowTwoS3F.belowLocalTrial {d : ℕ} (p eps : ℝ) (x0 : Point d) (n : ℕ) : LocalTrial d

The complete below-two local trial initialized with the cached starting observation.

Equations

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