Observable trial certification and amortized query bounds along the realized controller path.

structure V7.AnchorRunData (d : ℕ) : Type

The accepted index, trial estimates, points, and observations of the anchor search.

• acceptedIndex : ℕ

  The index of the first accepted anchor test.

• M : ℕ → ℝ

  The smoothness estimates examined by the anchor search.

• D : ℕ → ℝ

  The distances examined by the anchor search.

• y : ℕ → Point d

  The candidate anchor points.

• trace : List (Observation d)

  The chronological oracle observations of the anchor search.

noncomputable def V7.normingDirection {d : ℕ} (q : ℝ) (g : Point d) : Point d

The normalized signed power vector that attains the dual norm pairing.

Equations

• V7.normingDirection q g i = ↑(SignType.sign (g i)) * |g i| ^ (q - 1) / V7.lpNorm q g ^ (q - 1)

noncomputable def V7.NormingDirectionStatement : Prop

The norming direction has unit primal norm and attains the gradient's dual norm.

Equations

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

def V7.AnchorTest {d : ℕ} (oracle : PairOracle d) (x0 : Point d) (G D : ℝ) (y : Point d) : Prop

The candidate anchor achieves the required decrease from the initial point.

Equations

• V7.AnchorTest oracle x0 G D y = (oracle.value y ≤ oracle.value x0 - G * D / 2)

def V7.AnchorExecution {d : ℕ} (p : ℝ) (input : MethodInput d) (oracle : PairOracle d) (cached : CachedPair d) (run : AnchorRunData d) : Prop

The explicit dyadic ray search, including every rejected test and the first accepted test. These are algorithm-definition assumptions, not the named carrier's mathematical conclusions.

Equations

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

noncomputable def V7.AnchorStatement : Prop

U03/U13/U14/U19: source carrier for lem:anchor, keeping raw M0, accepted Ma, and Da distinct.

Equations

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

structure V7.ControllerVisit : Type

The smoothness and distance estimates at a controller visit.

• M : ℝ

  The smoothness estimate at this visit.

• D : ℝ

  The distance estimate at this visit.

def V7.VisitAt (visits : List ControllerVisit) (i : ℕ) (visit : ControllerVisit) : Prop

The specified visit occupies index i in the chronological controller path.

Equations

• V7.VisitAt visits i visit = ((List.drop i visits).head? = some visit)

def V7.ReportAt {d : ℕ} (reports : List (TrialReport d)) (i : ℕ) (report : TrialReport d) : Prop

The specified trial report occupies index i in the report list.

Equations

• V7.ReportAt reports i report = ((List.drop i reports).head? = some report)

def V7.ControllerPath {d : ℕ} (G Ma Da : ℝ) (visits : List ControllerVisit) (reports : List (TrialReport d)) : Prop

The initial visit and successive controller transitions agree with their trial reports.

Equations

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

def V7.RealizedPathGeometricallyDominated (eps G Ma R : ℝ) (visits : List ControllerVisit) : Prop

The realized visits form the permitted geometric sequence of scales and radii.

Equations

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

def V7.GuardAllowedInRegime (p : ℝ) (kind : ObservableGuardKind) : Prop

The observable guard kind is available in the selected exponent regime.

Equations

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

def V7.GuardLedgerComplete {d : ℕ} (p : ℝ) (report : TrialReport d) (schedule : List (ObservableGuardCheck d)) : Prop

The complete schedule belongs to the specified local routine. An early success or first failure consumes a prefix; Radius is legal only after the entire regime-appropriate schedule has been checked.

Equations

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

noncomputable def V7.TrialOutcomeCertificationStatement : Prop

U15--U22: source carrier for prop:certification. Correctness, visited bounds, reset behavior, and realized-path accounting are distinct conjuncts.

Equations

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

noncomputable def V7.localCostExponent (p : ℝ) : ℝ

The trial complexity exponent: one half below two, and p / (p + 2) above two.

Equations

• V7.localCostExponent p = if p ≤ 2 then 1 / 2 else p / (p + 2)

noncomputable def V7.GeometricTrialAmortizationStatement : Prop

G01--G02: source carrier for lem:amortization. Both geometric sums range over the realized path, never a rectangular product grid.

Equations

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