The output tailored verifier of the introspection presentation, from its specification

The output tailored verifier at λ has seven's sampler and two programs, an answer-length calculator L and a linear-constraints processor P. At an index n they meet the specification IntroSpec when, at every question vectorEquiv x of the detyped presentation, L outputs the presented game's lengths and P its constraints. Then the output's n-th game extends the presented one along vectorEquiv (extends_presented), so it has its value and its perfect ZPC strategies.

On the other side, the detyped game the presentation is compared with is the reference verifier's game read along vectorEquiv (quantumValue_H), whose value is the value of seven's output (output_val_eq_reference). So the output's val* is at most the value of seven's output at the same index (valStar_output_le).

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.Intro.Output.Ref (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (U : Cost.ClockedUniversalMachine) (V : Verifier 7) : Verifier 5

The reference verifier at index n.

Equations

• MIPRE.Tailored.Intro.Output.Ref c hc he lam n U V = MIPRE.Introspection.DecisionCompiler.reference c hc he U (V.sampler.prog, V.decider.prog) lam n

theorem MIPRE.Tailored.Intro.Output.quantumValue_H (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (U : Cost.ClockedUniversalMachine) (V : Verifier 7) : quantumValue (Sound.H c hc he lam n U V) = quantumValue ((Ref c hc he lam n U V).game n (Introspection.DecisionCompiler.outerBound c lam n))

The detyped game is the reference verifier's game, read along vectorEquiv.

theorem MIPRE.Tailored.Intro.Output.valStar_presented_le_output {c : ℕ} {hc : 1 ≤ c} {he : Even c} {lam n : ℕ} {U : Cost.ClockedUniversalMachine} {V : Verifier 7} (T : TailoredVerifier 7) (hc2 : 2 ≤ c) {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} (hkg : KerGens (Introspection.SourceCompiler.registerBits c lam n) kg) (hacc : Typed.AcceptsAsInput T V n) (hV : V.IsBounded lam) (hl : 1 ≤ lam) (hn : 1 ≤ n) : (presented Introspection.DecisionCompiler.graph (Sound.H c hc he lam n U V) (Sound.tdata c hc he lam n T V hs kg)).valStar ≤ (Introspection.DecisionCompiler.output c hc he U (V.sampler.prog, V.decider.prog) lam).val ValueModel.tensor n (Introspection.DecisionCompiler.outerBound c lam n)

The presentation's value is at most that of seven's output, on the input's normal form verifier.

The output tailored verifier and its specification

noncomputable def MIPRE.Tailored.Intro.Output.outTV (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam : ℕ) (L P : Decider) : TailoredVerifier 5

The output tailored verifier with programs L and P: seven's sampler.

Equations

• MIPRE.Tailored.Intro.Output.outTV c hc he lam L P = { sampler := MIPRE.Introspection.PauliSampler.finalSampler c hc he 7 lam, len := L, lp := P }

noncomputable def MIPRE.Tailored.Intro.Output.qe (c : ℕ) (hc : 1 ≤ c) (he : Even c) {lam n : ℕ} (U : Cost.ClockedUniversalMachine) (V : Verifier 7) (hl : 1 ≤ lam) (hn : 1 ≤ n) : (CL.Detyping.Coord Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n)) → ZMod 2) ≃ (Fin ((Introspection.PauliSampler.finalSampler c hc he 7 lam).dim n) → CL.𝔽₂)

The detyped questions, as the output's questions.

Equations

• MIPRE.Tailored.Intro.Output.qe c hc he U V hl hn = (MIPRE.CL.Detyping.DeciderProgram.vectorEquiv (MIPRE.Introspection.PauliSampler.dimension c lam n)).trans (MIPRE.Verifier.dimensionEquiv ⋯)

structure MIPRE.Tailored.Intro.Output.IntroSpec (c : ℕ) (hc : 1 ≤ c) (he : Even c) {lam n : ℕ} (U : Cost.ClockedUniversalMachine) (V : Verifier 7) (hl : 1 ≤ lam) (hn : 1 ≤ n) (G : TailoredGame (CL.Detyping.Coord Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n)) → ZMod 2)) (L P : Decider) : Prop

The specification of the output's two programs at index n: at every detyped question the answer-length calculator outputs the presented game's lengths, and the linear-constraints processor its constraints.

• lenR_eq (x : CL.Detyping.Coord Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n)) → ZMod 2) : LenIs L n (CL.toBits ((qe c hc he U V hl hn) x)) false (G.lenR x)
• lenL_eq (x : CL.Detyping.Coord Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n)) → ZMod 2) : LenIs L n (CL.toBits ((qe c hc he U V hl hn) x)) true (G.lenL x)
• cons_eq (x y : CL.Detyping.Coord Introspection.DecisionKernel.Label (Fin (Introspection.PauliSampler.dimension c lam n)) → ZMod 2) (aR bR : Cost.BitStr) : LpIs P n (CL.toBits ((qe c hc he U V hl hn) x)) (CL.toBits ((qe c hc he U V hl hn) y)) aR bR (G.cons x y aR bR)

theorem MIPRE.Tailored.Intro.Output.lenOf_eq_of {ℓ : ℕ} {W : TailoredVerifier ℓ} {n : ℕ} {x : Cost.BitStr} {κ : Bool} {k : ℕ} (h : LenIs W.len n x κ k) : W.lenOf n x κ = k

theorem MIPRE.Tailored.Intro.Output.extends_presented {c : ℕ} {hc : 1 ≤ c} {he : Even c} {lam n : ℕ} {U : Cost.ClockedUniversalMachine} {V : Verifier 7} {hl : 1 ≤ lam} {hn : 1 ≤ n} {T : TailoredVerifier 7} {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} {L P : Decider} (h : IntroSpec c hc he U V hl hn (presented Introspection.DecisionCompiler.graph (Sound.H c hc he lam n U V) (Sound.tdata c hc he lam n T V hs kg)) L P) : ((outTV c hc he lam L P).tgame n).Extends (presented Introspection.DecisionCompiler.graph (Sound.H c hc he lam n U V) (Sound.tdata c hc he lam n T V hs kg)) (qe c hc he U V hl hn).toEmbedding

The output's game extends the presented game along the detyped questions.

Soundness

theorem MIPRE.Tailored.Intro.Output.valStar_outTV_le {c : ℕ} {hc : 1 ≤ c} {he : Even c} {lam n : ℕ} {U : Cost.ClockedUniversalMachine} {V : Verifier 7} {hl : 1 ≤ lam} {hn : 1 ≤ n} (T : TailoredVerifier 7) (hc2 : 2 ≤ c) {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} {L P : Decider} (hkg : KerGens (Introspection.SourceCompiler.registerBits c lam n) kg) (hacc : Typed.AcceptsAsInput T V n) (hV : V.IsBounded lam) (h : IntroSpec c hc he U V hl hn (presented Introspection.DecisionCompiler.graph (Sound.H c hc he lam n U V) (Sound.tdata c hc he lam n T V hs kg)) L P) : (outTV c hc he lam L P).valStar n ≤ (Introspection.DecisionCompiler.output c hc he U (V.sampler.prog, V.decider.prog) lam).val ValueModel.tensor n (Introspection.DecisionCompiler.outerBound c lam n)

The output's val* is at most the value of seven's output.

theorem MIPRE.Tailored.Intro.Output.soundness_seven {lam n : ℕ} {V : Verifier 7} {hl : 1 ≤ lam} {hn : 1 ≤ n} (T : TailoredVerifier 7) {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n) → CL.𝔽₂)} {L P : Decider} (hkg : KerGens (Introspection.SourceCompiler.registerBits Introspection.sevenConstant lam n) kg) (hacc : Typed.AcceptsAsInput T V n) (hV : V.IsBounded lam) (h : IntroSpec Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ Cost.selfClockedUniversal V hl hn (presented Introspection.DecisionCompiler.graph (Sound.H Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ lam n Cost.selfClockedUniversal V) (Sound.tdata Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ lam n T V hs kg)) L P) {ε : ℝ} (hε : 0 < ε) (hv : 1 - ε < (outTV Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ lam L P).valStar n) : 1 - Introspection.delta (Introspection.CompiledSoundness.coefficient Introspection.sevenConstant) Introspection.CompiledSoundness.exponent lam n ε ≤ V.val ValueModel.tensor (2 ^ n) ((2 ^ n) ^ lam)

Soundness of the output, through seven.

Completeness

theorem MIPRE.Tailored.Intro.Output.hasPerfectZPC_outTV {c : ℕ} {hc : 1 ≤ c} {he : Even c} {lam n : ℕ} {U : Cost.ClockedUniversalMachine} {V : Verifier 7} {hl : 1 ≤ lam} {hn : 1 ≤ n} (T : TailoredVerifier 7) (hc2 : 2 ≤ c) {hs : V.sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits c lam n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits c lam n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits c lam n) → CL.𝔽₂)} {L P : Decider} (hkg : KerGens (Introspection.SourceCompiler.registerBits c lam n) kg) (hacc : Typed.AcceptsAsInput T V n) (hV : V.IsBounded lam) (h : IntroSpec c hc he U V hl hn (presented Introspection.DecisionCompiler.graph (Sound.H c hc he lam n U V) (Sound.tdata c hc he lam n T V hs kg)) L P) (R : SyncStrategy (Introspection.DecisionCompiler.rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n).doubled) (hR : R.IsPCC) (hval : R.value = 1) (hsupp : ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n))) (a : Verifier.Answers (Introspection.DecisionCompiler.outerBound c lam n)), ¬Complete.okT T V c lam hs q.2 a → R.P.M q a = 0) (hperm : ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n))) (i : ℕ), IsSignedPerm (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT T V c lam hs q.2 a) i false))) (hdiag : ∀ (q : Bool × CL.Detyping.Question (Introspection.QuestionType QLD.Ty 7) (Fin ((Introspection.DecisionCompiler.extendedSampler c hc he lam).dim n))), ∀ i < (Sound.tdata c hc he lam n T V hs kg).lenR q.2.1, (pvmObs (R.P.M q) fun (a : Verifier.Answers ((Introspection.DecisionCompiler.constantCutoff (Introspection.DecisionCompiler.outerBound c lam n)).outer n)) => bitSign (List.getD (Complete.encT T V c lam hs q.2 a) i false)).IsDiag) : (outTV c hc he lam L P).HasPerfectZPC n

Completeness of the output: a perfect PCC strategy of the reference verifier's typed game meeting the three conditions of Complete.hasPerfectZPC_tpresented gives a perfect ZPC strategy of the output's n-th game.

The input's normal form verifier

theorem MIPRE.Tailored.Intro.Output.acceptsAsInput_ofTNFVT (T : TailoredVerifier 7) (U0 : Cost.UniversalMachine) (n : ℕ) : Typed.AcceptsAsInput T (T.ofTNFVT U0) n

The input's normal form verifier accepts as the input does.

The loss

theorem MIPRE.Tailored.Intro.Output.delta_mul_le {a b : ℝ} (ha : 1 ≤ a) (hb : 0 < b) {C lam n : ℕ} (hC : 1 ≤ C) (hl : 1 ≤ lam) (hn : 1 ≤ n) {ε : ℝ} (hε : 0 ≤ ε) : Introspection.delta a b (C * lam) n ε ≤ Introspection.delta (a * ↑C ^ a) b lam n ε

A larger parameter in the loss is absorbed by the coefficient: for C ≥ 1, a ≥ 1, δ(a, b, Cλ, n, ε) ≤ δ(a C^a, b, λ, n, ε) when λ n ≥ 1.

Soundness in the contract's form

theorem MIPRE.Tailored.Intro.Output.lenOf_le_of_isBounded {T : TailoredVerifier 7} {lam m : ℕ} (hT : T.IsBounded lam) (hm : 2 ≤ m) (x : Cost.BitStr) (κ : Bool) : T.lenOf m x κ ≤ m ^ lam

theorem MIPRE.Tailored.Intro.Output.maxLen_le_of_isBounded {T : TailoredVerifier 7} {lam m : ℕ} (hT : T.IsBounded lam) (hm : 2 ≤ m) : (T.tgame m).maxLen ≤ m ^ (lam + 1)

A λ-bounded tailored verifier's answers at index m ≥ 2 have at most m^(λ+1) bits.

theorem MIPRE.Tailored.Intro.Output.soundness_contract (T : TailoredVerifier 7) (U0 : Cost.UniversalMachine) {C lam n : ℕ} (hC : 2 ≤ C) (hl : 1 ≤ lam) (hn : 1 ≤ n) (hT : T.IsBounded lam) (hV : (T.ofTNFVT U0).IsBounded (C * lam)) {hs : (T.ofTNFVT U0).sampler.dim (2 ^ n) ≤ Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n} {kg : (S : Finset (Fin (Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n))) → CL.RegLinear CL.𝔽₂ S → List (Fin (Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n) → CL.𝔽₂)} {L P : Decider} (hkg : KerGens (Introspection.SourceCompiler.registerBits Introspection.sevenConstant (C * lam) n) kg) {hl' : 1 ≤ C * lam} (h : IntroSpec Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ Cost.selfClockedUniversal (T.ofTNFVT U0) hl' hn (presented Introspection.DecisionCompiler.graph (Sound.H Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ (C * lam) n Cost.selfClockedUniversal (T.ofTNFVT U0)) (Sound.tdata Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ (C * lam) n T (T.ofTNFVT U0) hs kg)) L P) {ε : ℝ} (hε : 0 < ε) (hv : 1 - ε < (outTV Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ (C * lam) L P).valStar n) : 1 - Introspection.delta (Introspection.CompiledSoundness.coefficient Introspection.sevenConstant * ↑C ^ Introspection.CompiledSoundness.coefficient Introspection.sevenConstant) Introspection.CompiledSoundness.exponent lam n ε ≤ T.valStar (2 ^ n)

Soundness of the output, in the contract's form: for a λ-bounded input whose normal form verifier is Cλ-bounded (C ≥ 2), when the output's programs meet the specification at Cλ, val* of the output above 1 - ε gives val* of the input at 2^n at least 1 - δ(a C^a, b, λ, n, ε), with seven's a and b.