Verifier transport at a single index

Wrappers may change a sampler at exceptional indices. Equality of its dimension and CL presentations at the index in question suffices to preserve both quantum value and perfect PCC strategies; the programs need not agree elsewhere.

Stated in a value model (Phase 4 of planning/mipco-track.md): the two games are related by equivalences of their alphabets, so they have the same value in every value model (val_congr_at, through ValueModel.eq_of_equiv); the quantum-value statement valStar_congr_at is its instance at ValueModel.tensor.

def MIPRE.Verifier.dimensionEquiv {s t : ℕ} (h : s = t) : (Fin s → CL.𝔽₂) ≃ (Fin t → CL.𝔽₂)

Numbered vectors transported along an equality of their dimensions.

Equations

• MIPRE.Verifier.dimensionEquiv h = h ▸ Equiv.refl (Fin s → MIPRE.CL.𝔽₂)

theorem MIPRE.Verifier.toBits_dimensionEquiv {s t : ℕ} (h : s = t) (x : Fin s → CL.𝔽₂) : CL.toBits ((dimensionEquiv h) x) = CL.toBits x

theorem MIPRE.Verifier.clDist_dimensionEquiv {s t ℓ : ℕ} (h : s = t) (L R : CL.CLFun CL.𝔽₂ (Fin s) ℓ) (L' R' : CL.CLFun CL.𝔽₂ (Fin t) ℓ) (hL : L ≍ L') (hR : R ≍ R') (x y : Fin s → CL.𝔽₂) : CL.clDist L'.eval R'.eval ((dimensionEquiv h) x) ((dimensionEquiv h) y) = CL.clDist L.eval R.eval x y

structure MIPRE.Verifier.SamplerAgreement {ℓ : ℕ} (V W : Verifier ℓ) (n : ℕ) : Prop

Only the sampler data used at this index are compared.

• dimension : V.sampler.dim n = W.sampler.dim n
• presentation (w : Player) : V.sampler.cl n w ≍ W.sampler.cl n w

theorem MIPRE.Verifier.SamplerAgreement.symm {ℓ : ℕ} {V W : Verifier ℓ} {n : ℕ} (h : V.SamplerAgreement W n) : W.SamplerAgreement V n

theorem MIPRE.Verifier.game_mu_dimensionEquiv {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (h : V.SamplerAgreement W n) (x y : V.Questions n) : (W.game n T).μ ((dimensionEquiv ⋯) x) ((dimensionEquiv ⋯) y) = (V.game n T).μ x y

theorem MIPRE.Verifier.game_D_dimensionEquiv {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (h : V.SamplerAgreement W n) (hD : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) (x y : V.Questions n) (a b : Answers T) : (W.game n T).D ((dimensionEquiv ⋯) x) ((dimensionEquiv ⋯) y) a b = (V.game n T).D x y a b

theorem MIPRE.Verifier.val_congr_at {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (ω : ValueModel) (h : V.SamplerAgreement W n) (hD : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) : V.val ω n T = W.val ω n T

Changing programs away from the current index preserves the value, in every value model.

theorem MIPRE.Verifier.valStar_congr_at {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (h : V.SamplerAgreement W n) (hD : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) : V.valStar n T = W.valStar n T

Changing programs away from the current index preserves quantum value.

theorem MIPRE.Verifier.hasPerfectPCC_of_congr_at {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (h : V.SamplerAgreement W n) (hD : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) (hV : V.HasPerfectPCC n T) : W.HasPerfectPCC n T

Perfect PCC strategies also depend only on the game at the current index.

theorem MIPRE.Verifier.hasPerfectPCC_congr_at {ℓ : ℕ} {V W : Verifier ℓ} {n T : ℕ} (h : V.SamplerAgreement W n) (hD : ∀ (x y a b : Cost.BitStr), V.decider.Accepts n x y a b ↔ W.decider.Accepts n x y a b) : V.HasPerfectPCC n T ↔ W.HasPerfectPCC n T