Smoothing kernels, resisting oracle completions, and known-parameter lower-bound statements.

structure V7.DeterministicExactPairAlgorithm (d : ℕ) : Type

Causal deterministic exact-pair algorithm for the known-parameter lower bound. No inverse-gradient or unqueried-output channel is present.

• nextQuery : Point d → List (Observation d) → Point d

  The next query determined by the initial point and observation history.

• output : Point d → List (Observation d) → Point d

  The output determined by the initial point and observation history.

def V7.GeneratedBy {d : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (x0 : Point d) (trace : List (Observation d)) : Prop

Each trace point is the deterministic algorithm's query for the preceding history.

Equations

• V7.GeneratedBy algorithm x0 trace = ∀ (t : ℕ) (ht : t < trace.length), (trace.get ⟨t, ht⟩).point = if t = 0 then x0 else algorithm.nextQuery x0 (List.take t trace)

structure V7.SmoothingKernelData (p : ℝ) (d : ℕ) : Type

A smoothing potential, its derivatives, curvature bound, and induced oracle transformation.

• phi : Point d → ℝ

  The convex potential used to regularize the nonsmooth objective.

• gradPhi : Point d → Point d

  The coordinate gradient of the smoothing potential.

• hessian : Point d → Point d →L[ℝ] Point d

  The derivative of the kernel gradient, viewed as a continuous linear map.

• Mpd : ℝ

  The dimension- and exponent-dependent curvature bound for the kernel.

• smooth : ℝ → (Point d → ℝ) → PairOracle d

  The oracle obtained by smoothing an objective at a given scale.

noncomputable def V7.localSmoothingValue {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) (chi : ℝ) (ell : Point d → ℝ) (x : Point d) : ℝ

The infimal convolution of the objective with the rescaled smoothing potential.

Equations

• V7.localSmoothingValue kernel chi ell x = sInf {r : ℝ | ∃ (v : V7.Point d), r = ell (x + v) + chi * kernel.phi ((1 / chi) • v)}

def V7.IsOneLipschitz {d : ℕ} (p : ℝ) (f : Point d → ℝ) : Prop

The objective is one-Lipschitz with respect to the ℓp norm.

Equations

• V7.IsOneLipschitz p f = ∀ (x y : V7.Point d), |f x - f y| ≤ V7.lpNorm p (x - y)

def V7.SignedLpSymmetry {d : ℕ} (p : ℝ) (Q Qdual : Point d → Point d) : Prop

The primal and dual transformations preserve their norms and mutual pairing.

Equations

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

def V7.SmoothingKernelAssumptions {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) : Prop

The regularity, curvature, normalization, and smoothing properties required of a kernel.

Equations

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

noncomputable def V7.lowerKernelPhi {d : ℕ} (r0 theta : ℝ) (x : Point d) : ℝ

The signed-coordinate-invariant power kernel used in the lower-bound construction.

Equations

• V7.lowerKernelPhi r0 theta x = 2 * (∑ j : Fin d, |x j| ^ r0) ^ (2 * theta / r0)

noncomputable def V7.SmoothingKernelConstructionStatement : Prop

A smoothing kernel exists with the prescribed power formula and dimension-dependent bounds.

Equations

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

structure V7.LowerCompletionData (p : ℝ) (d T : ℕ) : Type

The adaptive partial objectives, queries, and final oracle in the resisting construction.

• algorithm : DeterministicExactPairAlgorithm d

  The deterministic algorithm against which the resisting oracle is constructed.

• x0 : Point d

  The initial query point.

• kernel : SmoothingKernelData p d

  The kernel used to smooth the resisting maxima.

• Delta : ℝ

  The main separation scale in the resisting construction.

• delta : ℝ

  The offset between successive affine pieces of the resisting maximum.

• chi : ℝ

  The smoothing scale of the partial objectives.

• beta : ℝ

  The coefficient of the added norm regularization.

• partialG : ℕ → Point d → ℝ

  The successive maxima of signed coordinate affine functions.

• partialH : ℕ → Point d → ℝ

  The successive regularized nonsmooth objectives.

• partialOracle : ℕ → PairOracle d

  The smooth oracle for each partial objective.

• completedOracle : PairOracle d

  The final oracle that preserves the earlier observations.

• queries : ℕ → Point d

  The queries generated against the successive partial oracles.

• sigma : ℕ → Fin d

  The coordinate selected at each resisting step.

• xi : ℕ → ℝ

  The sign selected for each resisting coordinate.

def V7.ResistingMaximumAt {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) (t : ℕ) : Prop

The partial objective is exactly the maximum of the affine pieces selected through t.

Equations

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

def V7.LowerCompletionAssumptions {p : ℝ} {d T : ℕ} (data : LowerCompletionData p d T) : Prop

The scales, fresh coordinates, oracle consistency, and adaptive queries of the resisting construction.

Equations

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

def V7.AboveLowerExactPairCompletionStatement : Prop

Source carrier for lem:above-lower-completion (L01--L04): both value and gradient agree at every chronological query.

Equations

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

structure V7.LowerObjectiveData (p : ℝ) (d T : ℕ) extends V7.LowerCompletionData p d T : Type

The completed resisting construction viewed as lower-bound objective data.

• algorithm : DeterministicExactPairAlgorithm d
• x0 : Point d
• kernel : SmoothingKernelData p d
• Delta : ℝ
• delta : ℝ
• chi : ℝ
• beta : ℝ
• partialG : ℕ → Point d → ℝ
• partialH : ℕ → Point d → ℝ
• partialOracle : ℕ → PairOracle d
• completedOracle : PairOracle d
• queries : ℕ → Point d
• sigma : ℕ → Fin d
• xi : ℕ → ℝ

def V7.IsCoerciveLp {d : ℕ} (p : ℝ) (f : Point d → ℝ) : Prop

The objective eventually exceeds every real bound outside a sufficiently large ℓp ball.

Equations

• V7.IsCoerciveLp p f = ∀ (B : ℝ), ∃ (radius : ℝ), 0 ≤ radius ∧ ∀ (x : V7.Point d), radius ≤ V7.lpNorm p x → B ≤ f x

def V7.LowerObjectiveAssumptions {p : ℝ} {d T : ℕ} (data : LowerObjectiveData p d T) : Prop

The completion conditions together with convexity and the exact coordinate gradient.

Equations

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

noncomputable def V7.AboveLowerQueryGapStatement : Prop

Source carrier for lem:above-lower-gap (L05).

Equations

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

noncomputable def V7.AboveLowerOutsideGradientStatement : Prop

Source carrier for lem:above-lower-outside (L06).

Equations

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

noncomputable def V7.AboveLowerBaseGradientStatement : Prop

Source carrier for prop:above-lower-base-gradient (L07).

Equations

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

noncomputable def V7.AboveLowerOptimizerRadiusStatement : Prop

Source carrier for lem:above-lower-radius (L08).

Equations

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

def V7.ChargedKnownParameterRun {d : ℕ} (algorithm : DeterministicExactPairAlgorithm d) (x0 : Point d) (oracle : PairOracle d) (trace : List (Observation d)) : Prop

An exact deterministic run with a nonempty trace charging its initial query.

Equations

• V7.ChargedKnownParameterRun algorithm x0 oracle trace = (V7.GeneratedBy algorithm x0 trace ∧ V7.TraceExact oracle trace ∧ trace ≠ [] ∧ Option.map O3.Observation.point trace.head? = some x0)

noncomputable def V7.KnownParameterAboveTwoUpperStatement : Prop

Upper half of the current known-parameter proposition. Cp occurs after p and before dimension and instance data.

Equations

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

noncomputable def V7.KnownParameterAboveTwoLowerStatement : Prop

Lower half of the current proposition: deterministic, exact-pair, every first-T query, T ≤ d, and explicit Mpd.

Equations

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

noncomputable def V7.KnownParameterAboveTwoOptimalityStatement : Prop

Source carrier for prop:pgtwo-optimality (U11--U12, A01--A13, L01--L09). The upper and lower halves remain separately inspectable.

Equations

• V7.KnownParameterAboveTwoOptimalityStatement = (V7.KnownParameterAboveTwoUpperStatement ∧ V7.KnownParameterAboveTwoLowerStatement)