V7 statement-layer foundations

This module contains transparent data carriers only. It deliberately does not import any historical O3 result or concrete O3 dispatcher.

@[reducible, inline]

abbrev V7.Point (d : ℕ) : Type

The finite-dimensional real vector space used by the parameter-free method.

Equations

• V7.Point = O3.Point

@[reducible, inline]

abbrev V7.PairOracle (d : ℕ) : Type

An oracle supplying objective values and gradients at query points.

Equations

• V7.PairOracle = O3.PairOracle

@[reducible, inline]

abbrev V7.Observation (d : ℕ) : Type

A query point together with its observed value and gradient.

Equations

• V7.Observation = O3.Observation

@[reducible, inline]

abbrev V7.pairing {d : ℕ} (x y : Point d) : ℝ

The coordinatewise real pairing of two vectors.

Equations

• V7.pairing x y = O3.pairing x y

@[reducible, inline]

noncomputable abbrev V7.lpNorm (p : ℝ) {d : ℕ} (x : Point d) : ℝ

The finite-dimensional real ℓp norm used in the method's bounds.

Equations

• V7.lpNorm p x = O3.lpNorm p x

@[reducible, inline]

noncomputable abbrev V7.conjugateExponent (p : ℝ) : ℝ

The Hölder-conjugate exponent p / (p - 1).

Equations

• V7.conjugateExponent p = O3.conjugateExponent p

structure V7.MethodInput (d : ℕ) : Type

The primitive numerical input of the positive secant model.

• p : ℝ

  The exponent of the norm used by the method.

• eps : ℝ

  The requested gradient accuracy.

• x0 : Point d

  The initial optimization point.

• z0 : Point d

  The second point of the supplied nondegenerate secant pair.

• M0 : ℝ

  The initial smoothness estimate.

structure V7.PairRunResult (d : ℕ) : Type

Chronological post-initialization result data.

• returned : Point d

  The point returned after the method finishes.

• trace : List (Observation d)

  The chronological observations made after initialization.

def V7.PairRunResult.postInitializationCallCount {d : ℕ} (run : PairRunResult d) : ℕ

The number of oracle calls recorded after initialization.

Equations

• run.postInitializationCallCount = run.trace.length

def V7.TraceExact {d : ℕ} (oracle : PairOracle d) (trace : List (Observation d)) : Prop

Every trace entry equals the exact oracle observation at its recorded point.

Equations

• V7.TraceExact oracle trace = ∀ obs ∈ trace, obs = O3.PairOracle.observe oracle obs.point

def V7.WasQueried {d : ℕ} (trace : List (Observation d)) (x : Point d) : Prop

The point occurs among the recorded oracle queries.

Equations

• V7.WasQueried trace x = ∃ obs ∈ trace, obs.point = x

def V7.QueriedAt {d : ℕ} (trace : List (Observation d)) (k : ℕ) (x : Point d) : Prop

The point was queried at the specified chronological trace index.

Equations

• V7.QueriedAt trace k x = ∃ (obs : V7.Observation d), (List.drop k trace).head? = some obs ∧ obs.point = x

def V7.PairRunResult.returnedWasQueried {d : ℕ} (run : PairRunResult d) : Prop

The returned point occurs in the run's query trace.

Equations

• run.returnedWasQueried = V7.WasQueried run.trace run.returned

def V7.MethodInput.toO3 {d : ℕ} (input : MethodInput d) : O3.MethodInput d

The numerical input viewed in the underlying causal machine interface.

Equations

• input.toO3 = { p := input.p, eps := input.eps, x0 := input.x0, z0 := input.z0, M0 := input.M0 }

@[reducible, inline]

abbrev V7.RuntimeMethodFamily : Type 1

A single causal machine family selected before p, dimension, or instance data. Objective information reaches it only through query.

Equations

• V7.RuntimeMethodFamily = ((d : ℕ) → O3.FirstOrderMethod d)

def V7.Executes {d : ℕ} (method : O3.FirstOrderMethod d) (input : MethodInput d) (oracle : PairOracle d) (run : PairRunResult d) : Prop

A finite-fuel execution of the underlying method produces the specified result and trace.

Equations

• V7.Executes method input oracle run = ∃ (fuel : ℕ) (oldRun : O3.RunResult d), method.run oracle input.toO3 fuel = some oldRun ∧ run.returned = oldRun.returned ∧ run.trace = oldRun.queries

def V7.SecantInitialization {d : ℕ} (input : MethodInput d) (oracle : PairOracle d) : Prop

A supplied nondegenerate secant relation; discovery is outside the count.

Equations

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