Repeated tailored verifiers, from the specification of their programs

Paper II, thm:repetition (II:11103), at the level of tailored verifiers, in the direct form of the plan (planning/aldous-lyons-track.md, Phase 2). The repeated verifier repTV V λ τ L P has the repeated sampler of the existing pipeline (MIPRE.Repeat.repSampler, k(n) independent copies of V's sampler) and two programs L, P for the answer-length calculator and the linear-constraints processor. This file proves completeness, and the comparison of its games with the input's that soundness rests on, from a specification of L and P at the index n (RepSpec), which the programs of MIPRE.Background.Tailored.Repetition meet:

• at a question all of whose coordinates have their lengths defined, L outputs the sums of the coordinates' lengths, and it halts at no other question;
• at two such questions, with readable answers of the right lengths, P halts exactly when the input's processor halts on every coordinate, and then outputs the constraints of the tailored product (V.tgame n).repeat k (MIPRE.Tailored.TailoredGame.repeat).

The results:

• RepSpec.accepts_of_accepts: whatever the repeated verifier's game accepts at (x, y), the tailored product accepts at the tuples of coordinates; and conversely at questions whose coordinates all have their lengths (RepSpec.accepts_iff);
• RepSpec.hasPerfectZPC: completeness, a perfect ZPC strategy for 𝒱_n gives one for 𝒱^rep_n, the tensor power of MIPRE.Tailored.Repeat.Strategy pulled back along the blocks of the questions — the questions on an edge have all their lengths, because a perfect strategy is accepted somewhere on every edge (PermStrategy.exists_accepts);
• quantumValue_le_of_coarse, on ProjectiveMeasurement.mergeAt of MIPRE.Foundations.GameAdapt at the identity map of questions: a game whose accepted answers, read through a map of the answers that may depend on the question, are accepted by a second game on equivalent questions, has at most its value. Soundness (MIPRE.Background.Tailored.Repetition) applies it to the repeated verifier's game and the direct repetition of 𝒱_n.

Coarse-graining along a map of the answers that depends on the question

theorem MIPRE.TensorProductStrategy.value_le_mergeAt {X : Type u_1} {A : Type u_3} {A' : Type u_4} [Fintype X] [Fintype A] [Fintype A'] [DecidableEq A'] {G : Game X X A A} (S : TensorProductStrategy G) (H : Game X X A' A') (r : X → A → A') (hμ : ∀ (x y : X), H.μ x y = G.μ x y) (hD : ∀ (x y : X) (a b : A), G.D x y a b = true → H.D x y (r x a) (r y b) = true) : S.value ≤ { dA := S.dA, dB := S.dB, ψ := S.ψ, ψ_unit := ⋯, PA := S.PA.mergeAt id r, PB := S.PB.mergeAt id r }.value

Merging the answers of a strategy at each question can only raise its value, when every accepted tuple of the first game is accepted after merging.

theorem MIPRE.quantumValue_le_of_coarse {X : Type u_1} {Y : Type u_2} {A : Type u_3} {A' : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype A'] [DecidableEq A'] (G : Game X X A A) (H : Game Y Y A' A') (e : X ≃ Y) (r : X → A → A') (hμ : ∀ (x y : X), G.μ x y = H.μ (e x) (e y)) (hD : ∀ (x y : X) (a b : A), G.D x y a b = true → H.D (e x) (e y) (r x a) (r y b) = true) : quantumValue G ≤ quantumValue H

Coarse-graining with a relabeling of the questions: if every tuple G accepts at (x, y) is accepted by H at (e x, e y) after reading the answers through r x, r y, on matching distributions, then val*(G) ≤ val*(H).

Perfect strategies are accepted on every edge

theorem MIPRE.Tailored.PermStrategy.exists_accepts {X : Type u_1} [Fintype X] {G : TailoredGame X} (S : PermStrategy G) (hS : S.value = 1) {x y : X} (hxy : 0 < G.μ x y) : ∃ (a : Cost.BitStr) (b : Cost.BitStr), G.Accepts x y a b

A perfect permutation strategy is accepted on every edge: some pair of answers is.

theorem MIPRE.Tailored.TailoredGame.HasPerfectZPC.exists_accepts {X : Type u_1} [Fintype X] {G : TailoredGame X} (h : G.HasPerfectZPC) {x y : X} (hxy : 0 < G.μ x y) : ∃ (a : Cost.BitStr) (b : Cost.BitStr), G.Accepts x y a b

A game with a perfect ZPC strategy is accepted on every edge.

theorem MIPRE.Tailored.TailoredGame.not_accepts_of_reject_mem {X : Type u_1} [Fintype X] {G : TailoredGame X} {x y : X} {a b : Cost.BitStr} {d : ℕ} (h : rejectConstraint d ∈ G.cons x y (List.take (G.lenR x) a) (List.take (G.lenR y) b)) : ¬G.Accepts x y a b

A constraint list containing a rejecting constraint accepts nothing.

Repeated tailored verifiers

@[reducible, inline]

abbrev MIPRE.Tailored.TailoredVerifier.K (lam tau n : ℕ) : ℕ

The number of repetitions at index n.

Equations

• MIPRE.Tailored.TailoredVerifier.K lam tau n = MIPRE.Repetition.reps lam tau n

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.TailoredVerifier.qEquiv {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) : (Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂) ≃ (Fin (K lam tau n) → V.Questions n)

The questions of the repeated verifier are tuples of questions of V.

Equations

• V.qEquiv lam tau n = MIPRE.CL.blockEquiv finProdFinEquiv

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.TailoredVerifier.qc {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau n : ℕ) (x : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂) (i : Fin (K lam tau n)) : V.Questions n

The i-th coordinate of a question of the repeated verifier.

Equations

• V.qc lam tau n x i = (V.qEquiv lam tau n) x i

noncomputable def MIPRE.Tailored.TailoredVerifier.repTV {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau : ℕ) (L P : Decider) : TailoredVerifier ℓ

The repeated tailored verifier: the repeated sampler, and the programs L, P.

Equations

• V.repTV lam tau L P = { sampler := MIPRE.Repeat.repSampler V.sampler lam tau, len := L, lp := P }

structure MIPRE.Tailored.TailoredVerifier.RepSpec {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam tau : ℕ) (L P : Decider) (n : ℕ) : Prop

The specification of the repeated programs at index n. Write x⃗ = qEquiv x for the tuple of coordinates of a question x, and call x good when every coordinate has its lengths (V.LenDefined).

• len_eq (x : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂) : (∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) → ∀ (κ : Bool), LenIs L n (CL.toBits x) κ (∑ i : Fin (K lam tau n), V.lenOf n (CL.toBits (V.qc lam tau n x i)) κ)

  At a good question, L outputs the sums of the coordinates' lengths.

• good_of_len (x : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂) (κ : Bool) (m : ℕ) : LenIs L n (CL.toBits x) κ m → ∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))

  L halts at good questions only.

• lp_iff (x y : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂) (aR bR : Cost.BitStr) : (∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) → (∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n y i))) → List.length aR = (V.tgame n).lenRSum ((V.qEquiv lam tau n) x) → List.length bR = (V.tgame n).lenRSum ((V.qEquiv lam tau n) y) → ∀ (cs : List Cost.BitStr), LpIs P n (CL.toBits x) (CL.toBits y) aR bR cs ↔ (∀ (i : Fin (K lam tau n)), ∃ (c : List Cost.BitStr), LpIs V.lp n (CL.toBits (V.qc lam tau n x i)) (CL.toBits (V.qc lam tau n y i)) ((V.tgame n).coordR ((V.qEquiv lam tau n) x) aR i) ((V.tgame n).coordR ((V.qEquiv lam tau n) y) bR i) c) ∧ cs = ((V.tgame n).repeat (K lam tau n)).cons ((V.qEquiv lam tau n) x) ((V.qEquiv lam tau n) y) aR bR

  At good questions and readable answers of the right lengths, P halts exactly when the input's processor halts on every coordinate, and then outputs the product's constraints.

theorem MIPRE.Tailored.TailoredVerifier.repTV_μ {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (x y : (V.repTV lam tau L P).Questions n) : ((V.repTV lam tau L P).tgame n).μ x y = ((V.tgame n).repeat (K lam tau n)).μ ((V.qEquiv lam tau n) x) ((V.qEquiv lam tau n) y)

The distribution of the repeated verifier's game is the product's.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.lenOf_eq {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) {x : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂} (hx : ∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (κ : Bool) : (V.repTV lam tau L P).lenOf n (CL.toBits x) κ = ∑ i : Fin (K lam tau n), V.lenOf n (CL.toBits (V.qc lam tau n x i)) κ

At a good question, the repeated verifier's lengths are the product's.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.lenDefined {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) {x : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂} (hx : ∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) : (V.repTV lam tau L P).LenDefined n (CL.toBits x)

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.sameLens {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) {x : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂} (hx : ∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) : ((V.repTV lam tau L P).tgame n).lenR x = ((V.tgame n).repeat (K lam tau n)).lenR ((V.qEquiv lam tau n) x) ∧ ((V.repTV lam tau L P).tgame n).lenL x = ((V.tgame n).repeat (K lam tau n)).lenL ((V.qEquiv lam tau n) x)

At a good question, the repeated verifier's game has the product's lengths.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.good_of_repeat_accepts {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau n : ℕ} {x y : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂} {a b : Cost.BitStr} (hacc : ((V.tgame n).repeat (K lam tau n)).Accepts ((V.qEquiv lam tau n) x) ((V.qEquiv lam tau n) y) a b) (i : Fin (K lam tau n)) : V.LenDefined n (CL.toBits (V.qc lam tau n x i)) ∧ V.LenDefined n (CL.toBits (V.qc lam tau n y i))

Every coordinate of an accepted question pair of the product has its lengths.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.accepts_iff {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) {x y : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂} {a b : Cost.BitStr} (hx : ∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n x i))) (hy : ∀ (i : Fin (K lam tau n)), V.LenDefined n (CL.toBits (V.qc lam tau n y i))) : ((V.repTV lam tau L P).tgame n).Accepts x y a b ↔ ((V.tgame n).repeat (K lam tau n)).Accepts ((V.qEquiv lam tau n) x) ((V.qEquiv lam tau n) y) a b

At good questions the two games accept the same answers.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.accepts_of_accepts {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) {x y : Fin (K lam tau n * V.sampler.dim n) → CL.𝔽₂} {a b : Cost.BitStr} (hacc : ((V.repTV lam tau L P).tgame n).Accepts x y a b) : ((V.tgame n).repeat (K lam tau n)).Accepts ((V.qEquiv lam tau n) x) ((V.qEquiv lam tau n) y) a b

The repeated verifier accepts only what the product accepts.

theorem MIPRE.Tailored.TailoredVerifier.RepSpec.hasPerfectZPC {ℓ : ℕ} {V : TailoredVerifier ℓ} {lam tau : ℕ} {L P : Decider} {n : ℕ} (h : V.RepSpec lam tau L P n) (hV : V.HasPerfectZPC n) : (V.repTV lam tau L P).HasPerfectZPC n

Completeness of the repeated verifier.