LemmaStatement: 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.

Matrix-weights regret implies SDP threshold feasibility

Statement

Consider a nonempty normalized finite Hermitian SDP with $n, m \geq 1$ , $R > 0$ , $A_{1} = I$ , $b_{1} = R$ , $∥ A_{j} ∥, ∥ C ∥ \leq 1$ , and a dual optimum attained by a vector of $ℓ_{1}$ norm at most $r \geq 1$ . For the finite threshold construction require rationally encoded $b_{j}, R, r, e$ , with $0 < e < R / 4$ . Write $v$ for its common primal/dual optimum and set $w = r + 1$ , with $ℓ = \ln (\max (2, n)), θ = e / (24 R r), T = ⌈ 36 w^{2} R^{2} ℓ / e^{2} ⌉, η = \sqrt{ℓ / T} .$ For a rational threshold $α$ , use exact losses $M_{t} = (\sum_{j} y_{t, j} A_{j} - C) / w$ and ideal round densities $ρ_{t} \propto \exp (- η \sum_{s < t} M_{s})$ . Implement the round trace labels by the frozen flagged-trace construction and its controlled/inverse access from Flagged Gibbs trace estimation: errors, probability floors and charged access, including the bad-label/operator-hybrid budget required by Two-sparse estimated SDP oracle from coherent labels. On the joint good event, the finite threshold loop has exactly these alternatives:

A round returns EMPTY, which implies $α < v$ ; its HIGHER response is a threshold exclusion.
All $T$ rounds return two-sparse weights. Then $\overset{ˉ}{y} = (e / R) e_{1} + T^{- 1} \sum_{t} y_{t}$ is dual feasible, its matrix slack is at least $(e / (2 R)) I$ , and $b \cdot \overset{ˉ}{y} \leq α + e$ .

Exact rational returned weights and their finite average may be retained without coefficient rounding. If the predictable conditional bad-probability budgets of the actual adaptive calls sum to at most $δ$ , both implications hold simultaneously with probability at least $1 - δ$ . Unproved numerical failures or absent access implementations are not covered by this probability premise. Bounded-dual emptiness is used for threshold exclusion; it does not assert an unproved dense primal certificate.

Facts & Assumptions

Given: The normalized SDP, exact round updates, finite trace/score implementations and their supplied conditional guarantees.

[F1]

Normalized Hermitian inequality SDPs have equal primal and dual values identifies the two optimal values and puts them in $[- R, R]$ without strict primal feasibility.

[F2]

Two-sparse estimated SDP oracle from coherent labels gives a nonnegative two-sparse vector with $ℓ_{1}$ norm at most $r$ , objective at most $α$ , and true round trace slack at least $- 2 (r + 1) θ$ , or a good-event threshold exclusion.

[F3]

Matrix multiplicative-weights regret bound gives $\sum_{t} tr (M_{t} ρ_{t}) \leq λ_{\min} (\sum_{t} M_{t}) + η T + \ln n / η$ for the exact MMW densities and contractions.

[F4]

Estimated SDP polytopes and sound bounded-dual threshold exclusion proves the estimated-polytope inclusions, bounded-optimum contrapositive, and adaptive conditional union bound.

[F5]

Flagged Gibbs trace estimation: errors, probability floors and charged access gives $θ$ -good labels from fixed coherent flag samplers, with its explicit norm, confidence, work and access conditions.

Proof

1.1givenF1F2F4F5algebra

The rational input data give rational $θ = e / (24 R r)$ , so the scalar labels and round parameters satisfy [F2]'s rational-input requirements; $e / R$ and every returned finite average are rational as well. The ideal $η$ and Gibbs densities may be real, since their finite implementations carry the declared error budgets. On the supplied good event, [F5] and [F2] apply to every reached density. If the oracle reports EMPTY, [F2] and [F4] imply $α < v$ . Otherwise its exact finite weights have $y_{t} \geq 0$ , $∥ y_{t} ∥_{1} \leq r$ , and $b \cdot y_{t} \leq α$ ; their true trace residual is at least $- 2 w θ$ , hence $tr (M_{t} ρ_{t}) \geq - 2 θ$ . Also $∥ M_{t} ∥ \leq (\sum_{j} y_{t, j} + 1) / w \leq 1$ . If two selected labels have the same index, [F2] merges their weights and takes a good convex-averaged estimate; this leaves the same bounds.

2.1givenF3step 1.1algebra

The parameter choice gives $η \leq e / (6 w R) < 1$ and $\ln n / (η T) \leq ℓ / (η T) = η$ . Since $w / r \leq 2$ , $w (2 θ + η + \ln n / (η T)) \leq w e / (12 R r) + e / (3 R) \leq e / (2 R)$ . By [F3] and step 1.1, $λ_{\min} (T^{- 1} \sum_{t} M_{t}) \geq - 2 θ - η - \ln n / (η T)$ . Multiplying by $w$ makes the unshifted average dual slack at least $- (e / (2 R)) I$ . Adding $(e / R) e_{1}$ therefore gives matrix slack at least $(e / (2 R)) I$ and keeps all coordinates nonnegative. Its objective is $e + T^{- 1} \sum_{t} b \cdot y_{t} \leq α + e$ . This proves the precise no-failure dual alternative and its reserve margin.

3.1givenF4step 1.1step 2.1∎

Every reached input is determined by the prior finite history. Apply [F4]'s conditional union bound to the actual supplied call budgets; it needs no independence of adaptively chosen matrices or thresholds. Outside their union of bad events, steps 1.1–2.1 establish all claimed alternatives. A capped minimum may be wrong only within its proved budget; a timeout lacking such a contract remains a separate failure. The returned sparse rational list already has a finite encoding and does not require a dense spectral feasibility check or an unsupported rounding step.

Depends on

Used by

Dependency tree · two levels

39 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

van Apeldoorn et al., Quantum SDP-solvers, Lemma 6 and Meta-Algorithm 1 (standard reference, not scraped)