Same-state soundness for the actual detyped verifier

The actual sampler's numbered CL presentations have precisely the finite detyping distribution after the coordinate permutation. Together with the proved executable predicate law, this transports the existing finite-game restriction to strategies for the compiled ambient verifier.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): a projective strategy (BipartiteModel.ProjStrat) of the compiled verifier's game in a model is read in the unnumbered finite game by relabelling its questions along the coordinate numbering (toFinite, through ProjStrat.relabel), and restricted to the valid typed graph views by asking its measurements at the embedded typed questions (restrictAmbient, through ProjStrat.restrict), in the same model. The failure bound, with the factor 16^{|T|}, is the model form of finite-game detyping (CL.Detyping.restrict_failure_le_povm). The statements that the shared state is unchanged (toFinite_state, restrictAmbient_state) have no counterpart: the model is the state. The completeness transport, for synchronous strategies, is unchanged.

noncomputable def MIPRE.CL.Detyping.DeciderProgram.vectorEquiv {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) : (Coord T (Fin s) → 𝔽₂) ≃ (Fin (graphDim T + s) → 𝔽₂)

The coordinate numbering is an equivalence of the complete question spaces.

Equations

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

def MIPRE.CL.Detyping.DeciderProgram.sourceFamily {T : Type u_1} [Cost.SizedEncoding T] {ℓ : ℕ} (S : TypedSampler ℓ T) (n : ℕ) (w : Bool) : T → CLFun 𝔽₂ (Fin (S.dim n)) ℓ

Equations

• MIPRE.CL.Detyping.DeciderProgram.sourceFamily S n w = S.cl n (MIPRE.Player.ofBool w)

theorem MIPRE.CL.Detyping.DeciderProgram.numbered_clDist {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (n : ℕ) (x y : Coord T (Fin (S.dim n)) → 𝔽₂) : clDist (numbered E Player.alice (S.cl n Player.alice)).eval (numbered E Player.bob (S.cl n Player.bob)).eval ((vectorEquiv (S.dim n)) x) ((vectorEquiv (S.dim n)) y) = clDist (presentation E false (sourceFamily S n false)).eval (presentation E true (sourceFamily S n true)).eval x y

The exact finite distribution obtained by numbering the detyped registers.

theorem MIPRE.CL.Detyping.DeciderProgram.verifier_game_mu {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (x y : Coord T (Fin (S.dim n)) → 𝔽₂) : ((verifier E S D C hℓ hD).game n (C.outer n)).μ ((vectorEquiv (S.dim n)) x) ((vectorEquiv (S.dim n)) y) = (game E (sourceFamily S n) (typedPredicate S D C n)).μ x y

The actual ambient game and the finite game have identical question weights.

noncomputable def MIPRE.CL.Detyping.DeciderProgram.toFinite {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : M.ProjStrat ((verifier E S D C hℓ hD).game n (C.outer n))) : M.ProjStrat (game E (sourceFamily S n) (typedPredicate S D C n))

Read the actual compiled-verifier strategy in the unnumbered finite game, in the same model: the same measurements, asked along the coordinate numbering.

Equations

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

theorem MIPRE.CL.Detyping.DeciderProgram.toFinite_value {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : M.ProjStrat ((verifier E S D C hℓ hD).game n (C.outer n))) : (toFinite E S D C hℓ hD n R).value = R.value

noncomputable def MIPRE.CL.Detyping.DeciderProgram.restrictAmbient {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hne : (Graph.edges E).Nonempty) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : M.ProjStrat ((verifier E S D C hℓ hD).game n (C.outer n))) : M.ProjStrat (typedGame E hne (sourceFamily S n) (typedPredicate S D C n))

Restrict an actual compiled-verifier strategy to valid typed graph views, in the same model: the finite-game measurements, asked at the embedded typed questions.

Equations

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

theorem MIPRE.CL.Detyping.DeciderProgram.restrictAmbient_failure_le {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : M.ProjStrat ((verifier E S D C hℓ hD).game n (C.outer n))) : 1 - (restrictAmbient E S D C hne hℓ hD n R).value ≤ 16 ^ Fintype.card T * (1 - R.value)

The source detyping soundness factor now applies to the actual program-defined game.

theorem MIPRE.CL.Detyping.DeciderProgram.restrictAmbient_value_ge {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) {𝒞 : Type u_2} {𝒜 : Type u_3} {ℬ : Type u_4} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : M.ProjStrat ((verifier E S D C hℓ hD).game n (C.outer n))) {ε : ℝ} (hR : 1 - ε ≤ R.value) : 1 - 16 ^ Fintype.card T * ε ≤ (restrictAmbient E S D C hne hℓ hD n R).value

noncomputable def MIPRE.CL.Detyping.DeciderProgram.doubledVectorEquiv {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) : Bool × (Fin (graphDim T + s) → 𝔽₂) ≃ Bool × (Coord T (Fin s) → 𝔽₂)

Undo coordinate numbering while preserving the doubling tag.

Equations

• MIPRE.CL.Detyping.DeciderProgram.doubledVectorEquiv s = (Equiv.refl Bool).prodCongr (MIPRE.CL.Detyping.DeciderProgram.vectorEquiv s).symm

theorem MIPRE.CL.Detyping.DeciderProgram.doubled_game_mu {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (p q : Bool × (Fin (graphDim T + S.dim n) → 𝔽₂)) : ((verifier E S D C hℓ hD).game n (C.outer n)).doubled.μ p q = (game E (sourceFamily S n) (typedPredicate S D C n)).doubled.μ ((doubledVectorEquiv (S.dim n)) p) ((doubledVectorEquiv (S.dim n)) q)

theorem MIPRE.CL.Detyping.DeciderProgram.doubled_game_D {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (p q : Bool × (Fin (graphDim T + S.dim n) → 𝔽₂)) (a b : Verifier.Answers (C.outer n)) : ((verifier E S D C hℓ hD).game n (C.outer n)).doubled.D p q a b = (game E (sourceFamily S n) (typedPredicate S D C n)).doubled.D ((doubledVectorEquiv (S.dim n)) p) ((doubledVectorEquiv (S.dim n)) q) a b

noncomputable def MIPRE.CL.Detyping.DeciderProgram.fromFiniteSync {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : SyncStrategy (game E (sourceFamily S n) (typedPredicate S D C n)).doubled) : SyncStrategy ((verifier E S D C hℓ hD).game n (C.outer n)).doubled

Transport a synchronous finite-game strategy to the actual compiled verifier.

Equations

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

theorem MIPRE.CL.Detyping.DeciderProgram.fromFiniteSync_value {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : SyncStrategy (game E (sourceFamily S n) (typedPredicate S D C n)).doubled) : (fromFiniteSync E S D C hℓ hD n R).value = R.value

theorem MIPRE.CL.Detyping.DeciderProgram.fromFiniteSync_isPCC {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : SyncStrategy (game E (sourceFamily S n) (typedPredicate S D C n)).doubled) (hR : R.IsPCC) : (fromFiniteSync E S D C hℓ hD n R).IsPCC

theorem MIPRE.CL.Detyping.DeciderProgram.exists_ambientPerfectPCC {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : SyncStrategy (typedGame E hne (sourceFamily S n) (typedPredicate S D C n)).doubled) (hR : R.IsPCC) (hval : R.value = 1) : ∃ (Q : SyncStrategy ((verifier E S D C hℓ hD).game n (C.outer n)).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = R.d

Perfect PCC completeness for the actual program-defined game, on the same outer answer alphabet with the source typed cutoff included in the premise.

theorem MIPRE.CL.Detyping.DeciderProgram.verifier_hasPerfectPCC {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) (R : SyncStrategy (typedGame E hne (sourceFamily S n) (typedPredicate S D C n)).doubled) (hR : R.IsPCC) (hval : R.value = 1) : (verifier E S D C hℓ hD).HasPerfectPCC n (C.outer n)

Completeness in the ambient verifier API, with the source typed cutoff already present in the finite typed game on the same outer alphabet.