Approximating the quantum value from below

Groundwork for lem:value-lower-approx, the MIP* ⊆ RE direction: a machine that, given a game G and a rational t, halts if and only if val*(G) > t. It enumerates candidate strategies with Gaussian-rational entries, computes their values exactly, and halts on a certificate; val* is by definition a supremum over finite-dimensional tensor-product strategies (MIPRE.quantumValue), so no infinite-dimensional truncation and no semidefinite programming enter.

The decomposition followed here is the one validated in the adversarial campaign recorded in vidick/mipre-proof (ledger nodes 1.1.7.2.1 to 1.1.7.2.6); see planning/ledger-informed-plan.md. This file carries the part of node 1.1.7.2.1 that makes the candidate set decidable: an operator-norm constraint on a Hermitian matrix is equivalent to two positive-semidefiniteness tests, and positive semidefiniteness of a Gaussian-rational Hermitian matrix is decidable.

Everything is stated through the quadratic form ⟨x| M |x⟩ rather than a matrix norm. That is faithful — for Hermitian M the operator norm is the supremum of |⟨x| M |x⟩| over unit x — and it keeps the statements independent of which of Mathlib's several matrix-norm instances is in scope.

theorem MIPRE.ValueApprox.isHermitian_realSmul_one_add {d : Type u_1} [DecidableEq d] {M : Matrix d d ℂ} (hM : M.IsHermitian) (c : ℝ) : (↑c • 1 + M).IsHermitian

Shifting by a real multiple of the identity keeps a matrix Hermitian.

theorem MIPRE.ValueApprox.isHermitian_realSmul_one_sub {d : Type u_1} [DecidableEq d] {M : Matrix d d ℂ} (hM : M.IsHermitian) (c : ℝ) : (↑c • 1 - M).IsHermitian

Likewise for the reflected shift.

theorem MIPRE.ValueApprox.dotProduct_realSmul_one_add {d : Type u_1} [Fintype d] [DecidableEq d] (c : ℂ) (M : Matrix d d ℂ) (x : d → ℂ) : star x ⬝ᵥ (c • 1 + M).mulVec x = c * star x ⬝ᵥ x + star x ⬝ᵥ M.mulVec x

The quadratic form of a shifted matrix splits.

theorem MIPRE.ValueApprox.dotProduct_realSmul_one_sub {d : Type u_1} [Fintype d] [DecidableEq d] (c : ℂ) (M : Matrix d d ℂ) (x : d → ℂ) : star x ⬝ᵥ (c • 1 - M).mulVec x = c * star x ⬝ᵥ x - star x ⬝ᵥ M.mulVec x

The quadratic form of the reflected shift splits.

theorem MIPRE.ValueApprox.posSemidef_realSmul_one_add_and_sub_iff {d : Type u_1} [Fintype d] [DecidableEq d] {M : Matrix d d ℂ} (hM : M.IsHermitian) (c : ℝ) : (↑c • 1 + M).PosSemidef ∧ (↑c • 1 - M).PosSemidef ↔ ∀ (x : d → ℂ), -(↑c * star x ⬝ᵥ x) ≤ star x ⬝ᵥ M.mulVec x ∧ star x ⬝ᵥ M.mulVec x ≤ ↑c * star x ⬝ᵥ x

Ledger node 1.1.7.2.1, the norm constraint. For a Hermitian M and a real c, the two positive-semidefiniteness tests on c·1 + M and c·1 - M hold exactly when the quadratic form of M is sandwiched by ±c⟨x|x⟩ — which for a Hermitian matrix says ‖M‖ ≤ c. This is what the enumeration of node 1.1.7.2.2 needs: its constraint ‖∑ a A^x_a - 1‖ ≤ |A|η is two psd tests, and psd of a Gaussian-rational Hermitian matrix is decidable, so membership in the candidate set is decidable.

Perturbing a candidate

Nodes 1.1.7.2.3 (stability) and 1.1.7.2.4 (density) both compare the value of an approximate candidate with the value of an exact strategy nearby, and both do it by the same algebra: split the difference of two Born expectations into a part where only the operators moved and a part where only the state moved. The identities below are that split, exactly and with no estimates in them; the analytic bounds of those two nodes are obtained by bounding each term separately.

theorem MIPRE.ValueApprox.kronecker_sub_kronecker {dA : Type u_2} {dB : Type u_3} (A A' : Matrix dA dA ℂ) (B B' : Matrix dB dB ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A' B' = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (A - A') B + Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A' (B - B')

A difference of Kronecker products splits over the two factors. This is what lets the two players' operators be perturbed one at a time.

theorem MIPRE.ValueApprox.dotProduct_mulVec_perturb {d : Type u_1} [Fintype d] (M N : Matrix d d ℂ) (ψ φ : d → ℂ) : star ψ ⬝ᵥ M.mulVec ψ - star φ ⬝ᵥ N.mulVec φ = star ψ ⬝ᵥ (M - N).mulVec ψ + star (ψ - φ) ⬝ᵥ N.mulVec ψ + star φ ⬝ᵥ N.mulVec (ψ - φ)

The perturbation split. The difference of the Born expectations of (M, ψ) and (N, φ) is an operator term, in which only M - N appears, plus two state terms, in which only ψ - φ appears. Exact: no norms and no estimates.

theorem MIPRE.ValueApprox.dotProduct_kronecker_perturb {dA : Type u_2} {dB : Type u_3} [Fintype dA] [Fintype dB] (A A' : Matrix dA dA ℂ) (B B' : Matrix dB dB ℂ) (ψ φ : dA × dB → ℂ) : star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).mulVec ψ - star φ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A' B').mulVec φ = star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (A - A') B).mulVec ψ + star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A' (B - B')).mulVec ψ + star (ψ - φ) ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A' B').mulVec ψ + star φ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A' B').mulVec (ψ - φ)

The split a candidate strategy actually needs: a bipartite Born expectation with both players' operators and the state perturbed at once decomposes into four terms, each moving exactly one of A, B and ψ. Combining kronecker_sub_kronecker with dotProduct_mulVec_perturb.