The low-individual-degree test in dyadic pairs, and values approached in sound models

Phase 6 of planning/mipco-track.md takes as its target, in place of LIDT.Simul.SoundCo, the soundness of the seeded CL test in every dyadic pair (SoundFin, def:lidt-sound-fin): the finite pairs, whose two algebras are each other's commutants and both carry a faithful tracial state (MIPRE.BipartiteModel.IsFinitePair, reports/lidt-co-audit.md, §3.4), whose two algebras moreover have unital dyadic matrix units (MIPRE.BipartiteModel.IsDyadicPair), with an arbitrary vector state. SoundFin and SoundCo are incomparable as statements; what SoundFin buys is a trace on both algebras and, through the matrix units, no abelian projections in either (reports/c6b-paper-proofs.md, §3). Like SoundCo (SoundCo.expand), it holds in every ancilla extension by a unit vector of a model in its class (SoundFin.expand), the class being closed under them.

The answer-reduction analysis applies the hypothesis inside the model of one near-optimal projective strategy, so what it needs of a value model ω is that ω be approached by projective strategies of models in which the test is sound and which ω dominates (ApproxSoundIn ω). val* has it through the tensor-product models of tensor-product strategies (approxSoundIn_tensor). Both hypotheses give it for ω_co: SoundCo through the commuting-operator models (approxSoundIn_commuting), and SoundFin through dyadic pairs, given that ω_co is approached in dyadic pairs (approxSoundIn_commuting_of_fin; the approximation is MIPRE.Repetition.commutingFinitePairApprox, from Lin's tracial density and an amplification by the twisted Pauli algebra).

def MIPRE.LIDT.Simul.SoundFin : Prop

The seeded CL test is sound in every dyadic pair (def:lidt-sound-fin): SoundIn M for every bipartite model M on a Hilbert space of Type whose two algebras are each other's commutants, carry faithful tracial states and have unital dyadic matrix units (BipartiteModel.IsDyadicPair). The target of Phase 6 of planning/mipco-track.md.

Equations

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

theorem MIPRE.LIDT.Simul.SoundFin.expand (h : SoundFin) {𝒞 𝒜 ℬ : Type} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarModule ℂ 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [StarProper ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hM : M.IsDyadicPair) {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α × β → ℂ) (he : ‖evec e‖ = 1) : SoundIn (M.expand e)

The seeded CL test is sound in every extension of a dyadic pair by a unit vector, when it is sound in every dyadic pair: the registers of a unit vector are nonempty (nonempty_of_norm_evec_eq_one), and the extension is again a dyadic pair (BipartiteModel.IsDyadicPair.expand). The Pauli basis analysis applies the test there (QLD.soundIn_of_lidt).

def MIPRE.LIDT.Simul.ApproxSoundIn (ω : ValueModel) : Prop

The value model is approached by projective strategies of models in which the seeded test is sound and which it dominates: below the value of a game, and above 0, lies the value of such a strategy, on a Hilbert space of Type. Answer reduction applies the test inside the model of such a strategy (AnswerReduction.arVerifier_soundness_of_approx).

Equations

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

theorem MIPRE.LIDT.Simul.approxSoundIn_tensor : ApproxSoundIn ValueModel.tensor

val* is approached in tensor-product models, where the test is sound (soundIn_tensor) and which val* dominates (ValueModel.tensor_dominates): a tensor-product strategy near the supremum is a projective strategy of its model, of the same value.

theorem MIPRE.LIDT.Simul.approxSoundIn_commuting (h : SoundCo) : ApproxSoundIn ValueModel.commuting

ω_co is approached in the models of commuting-operator strategies (exists_projStrat_lt_commutingOperatorValue), where the test is sound if SoundCo holds.

theorem MIPRE.LIDT.Simul.approxSoundIn_commuting_of_fin (hV : CommutingFinitePairApprox) (h : SoundFin) : ApproxSoundIn ValueModel.commuting

ω_co is approached in dyadic pairs, where the test is sound if SoundFin holds, as soon as ω_co is approached by projective strategies in dyadic pairs (CommutingFinitePairApprox, proved as MIPRE.Repetition.commutingFinitePairApprox).