The Pauli basis test from the low-individual-degree test in dyadic pairs

Phase 6 of planning/mipco-track.md. Introspection needs of the value model only that it be approached by projective strategies of models in which the Pauli basis test is sound (QLD.ApproxSoundIn), and the Pauli basis test is sound in a model as soon as the seeded low-individual-degree test is sound in every ancilla extension of it by a unit vector (QLD.soundIn_of_lidt). A dyadic pair has nonempty registers in every such extension, which is again a dyadic pair (BipartiteModel.IsDyadicPair.expand), so LIDT.Simul.SoundFin holds there (LIDT.Simul.SoundFin.expand); and ω_co dominates every model in a unit state (ValueModel.commuting_dominatesPOVM). So LIDT.Simul.SoundFin, with the approximation of ω_co in dyadic pairs, gives QLD.ApproxSoundIn for ω_co (lem:qld-approx-co-fin).

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

ω_co is approached in models where the Pauli basis test is sound, given that the seeded low-individual-degree test is sound in every dyadic pair and that ω_co is approached by projective strategies in dyadic pairs (lem:qld-approx-co-fin).