Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Exact central points have barrier gap m/t or nu/t

Statement

For the smooth convex inequality problem of Log-barrier central paths and primal-dual Newton residuals, suppose a strict feasible exact minimizer xt of the barrier objective exists, the primal value p∗ is finite, and the equality multiplier is included. Use the sign convention L(x,λ,ν)=f0(x)+λTg(x)+νT(Ax−b), and define qD(λ,ν)=inf⁡x∈DL(x,λ,ν) on the common open domain D. Then the Lagrangian dual pair generated by λi=−1/(tgi(xt)) has value qD(λ,ν)=f0(xt)−m/t, so 0≤f0(xt)−p∗≤m/t. For the conic model of Conic, LP, and convex QP primal-dual models, suppose xt is an exact barrier minimizer and F is a ν-log-homogeneous barrier. Its barrier multiplier zt=−∇F(st)/t and equality multiplier give a dual feasible pair with gap ν/t, and hence 0≤cTxt−p∗≤ν/t. No primal attainment or strong-duality assumption is used; existence of the exact barrier minimizer and finiteness of p∗ are required.

Facts & Assumptions

Given: The smooth and conic barrier objectives, their strict feasibility and exact minimizers, and a finite primal value.

[F1]

The smooth inequality convention is gi≤0, with multiplier λi≥0 (Inequality constrained programs, tangent cones, constraint qualifications, and KKT).

[F2]

For differentiable convex L on an open convex domain, L(y)≥L(x)+∇L(x)T(y−x) (Differentiable convex functions are characterized by the gradient inequality).

[F3]

The barrier identity is DF(s)[s]=−ν and −∇F(s)∈K∗ (The negative gradient of a log-homogeneous cone barrier is dual feasible).

Proof

1.1F1F2algebra

In the smooth case, differentiating Ψt at its affine-constrained minimizer gives t∇f0(xt)+Dg(xt)T(−1/g(xt))+ATw=0. Since gi(xt)<0, λi=−1/(tgi(xt))>0, and ν=w/t make this ∇f0+DgTλ+ATν=0. Also λigi(xt)=−1/t for every i. Thus ∇xL(xt,λ,ν)=0 and L(⋅,λ,ν) is convex; [F2] proves that xt globally minimizes this Lagrangian on D. Therefore qD(λ,ν)=L(xt,λ,ν)=f0(xt)−m/t.

2.1F1step 1.1algebra

For every primal feasible x∈D, [F1] gives λi≥0 and gi(x)≤0, hence L(x,λ,ν)=f0(x)+λTg(x)≤f0(x). Thus qD(λ,ν)≤f0(x) for every feasible x, so qD(λ,ν)≤p∗. Since xt is feasible, p∗≤f0(xt). Combining this with step 1.1 yields 0≤f0(xt)−p∗≤m/t.

3.1F3step 2.1algebra∎

In the conic case set zt=−∇F(st)/t∈K∗ by [F3] and yt=−w/t. The stationarity equation in Log-barrier central paths and primal-dual Newton residuals gives ATyt−G∗zt=c, so the pair is dual feasible. The conic gap identity in Conic, LP, and convex QP primal-dual models gives cTxt−(bTyt−⟨h,zt⟩)=⟨zt,st⟩=−DF(st)[st]/t=ν/t. For every primal feasible x, the same identity and zt∈K∗ make its objective at least the dual value, so bTyt−⟨h,zt⟩≤p∗. Since xt is primal feasible, p∗≤cTxt; combining these inequalities with the exact gap gives 0≤cTxt−p∗≤ν/t.

Depends on

Used by

Dependency tree · two levels

16 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