Alphabeta Math
CounterexampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The projected OGD bound does not cover infeasible comparators

Statement refuted

Refuted claim: For integers d,T≥1, let K⊆Rd be nonempty, closed, and convex with diameter at most a finite D>0. Let each ft:Rd→R be differentiable and convex on an open convex neighborhood of K, and suppose the projected online-gradient algorithm starts at x1∈K, uses ηt=D/(Gt) for finite G>0, and has ∥∇ft(xt)∥2≤G on every round. Assume Countable Choice for the metric projections. The refuted claim is that

∑t=1T(ft(xt)−ft(u))≤32DGT

holds for every comparator u∈Rd, including points outside K.

Facts & Assumptions

Given: The projected OGD algorithm, K=[0,1], diameter bound D=1, horizon T=2, losses ft:R→R defined by ft(x)=−x for t=1,2, initial point x1=0, gradient bound G=1, and infeasible comparator u=2.

[A1]

The Axiom of Countable Choice (ACω): Countable Choice is assumed for the nondegenerate projection updates.

[F1]

Projected online gradient descent: ηt=D/(Gt) and xt+1=PK(xt−ηtgt) when D,G>0.

[F5]

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: the gradient of a scalar-valued differentiable function on R is its ordinary derivative.

[F6]

Metric projection onto a closed convex set satisfies the variational inequality: p=PK(z) exactly when (z−p)(v−p)≤0 for every v∈K.

[F7]

Convex and strictly convex functions on Euclidean convex sets: a function is convex when it lies below the chord between any two points of its convex domain.

[F8]

Projection onto a nonempty closed convex set: under Countable Choice, the metric projection onto K exists and is unique.

Counterexample

technique · direct
1.1F2F3F4givenalgebra

The interval K=[0,1] is nonempty. For v,w∈K and λ∈[0,1], 0≤(1−λ)v+λw≤(1−λ)+λ=1, so [F3] makes it convex. Its complement is (−∞,0)∪(1,∞). If z<0, the ball of radius −z/2 about z lies in (−∞,0); if z>1, the ball of radius (z−1)/2 about z lies in (1,∞). Thus [F4] makes K closed. Its diameter is D=1 because ∣v−w∣≤1 for v,w∈[0,1] and the endpoints attain distance 1.

1.2F2F5F7givenalgebra

For each t and h≠0, (ft(x+h)−ft(x))/h=(−(x+h)+x)/h=−1, so the derivative is gt=−1 by [F5]; the affine identity ft((1−λ)x+λy)=(1−λ)ft(x)+λft(y) and [F7] show convexity. Also ∣gt∣=1=G.

2.1A1F1F6F8step 1.1step 1.2algebra

By [A1] and [F8], both metric projections exist uniquely. Since D=G=1, η1=1 and η2=1/2. The first unprojected point is x1−η1g1=1; for every v∈[0,1], (1−1)(v−1)=0, so [F6] gives x2=PK(1)=1. The next unprojected point is x2−η2g2=1+1/2>1; for every v∈[0,1], (1+1/2−1)(v−1)≤0, so [F6] gives x3=PK(1+1/2)=1.

3.1givenstep 1.1step 2.1algebra

The learner's two played losses sum to f1(x1)+f2(x2)=0−1=−1, whereas the infeasible comparator has ∑t=12ft(2)=−4. Its regret is therefore 3.

4.1givenstep 3.1algebra∎

The proposed right-hand side is 32⋅1⋅1⋅2=322<3, since 2<2. Thus the regret inequality fails for u=2∉K.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

57 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources