The executable detyped predicate agrees with the finite game #
The finite typed predicate retains the inner answer cutoff. On the outer bounded answer alphabet, the extra global cutoff disappears identically.
theorem
MIPRE.CL.Detyping.DeciderProgram.accepts_selected
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(E : T → T → Prop)
[DecidableRel E]
{ι : Type u_2}
{A : Type u_3}
{B : Type u_4}
[Fintype ι]
[DecidableEq ι]
(P : Question T ι → Question T ι → A → B → Bool)
(x y : Coord T ι → 𝔽₂)
(a : A)
(b : B)
:
accepts E P x y a b = match selectedEdge E (pull Function.Embedding.inl x) (pull Function.Embedding.inl y) with
| none => true
| some uv => P (uv.1, pull Function.Embedding.inr x) (uv.2, pull Function.Embedding.inr y) a b
theorem
MIPRE.CL.Detyping.DeciderProgram.graphOfBits_register
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(s : ℕ)
(x : Coord T (Fin s) → 𝔽₂)
:
theorem
MIPRE.CL.Detyping.DeciderProgram.drop_register
{T : Type u_1}
[Fintype T]
[DecidableEq T]
[Cost.SizedEncoding T]
(s : ℕ)
(x : Coord T (Fin s) → 𝔽₂)
:
List.drop (graphDim T) (toBits (push (registerEquiv s).toEmbedding x)) = toBits (pull Function.Embedding.inr x)
noncomputable def
MIPRE.CL.Detyping.DeciderProgram.typedPredicate
{T : Type u_1}
[Cost.SizedEncoding T]
{ℓ : ℕ}
(S : TypedSampler ℓ T)
(D : TypedDecider T)
(C : CutoffProgram)
(n : ℕ)
:
The source typed decision predicate with its entire-answer cutoff.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.CL.Detyping.DeciderProgram.bounded_acceptance
{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)
(hD : D.Total)
(n : ℕ)
(x y : Coord T (Fin (S.dim n)) → 𝔽₂)
(a b : Verifier.Answers (C.outer n))
:
decide
((decider E S D C).Accepts n (toBits (push (registerEquiv (S.dim n)).toEmbedding x))
(toBits (push (registerEquiv (S.dim n)).toEmbedding y)) ↑a ↑b) = accepts E (typedPredicate S D C n) x y a b
On the outer answer alphabet, the compiled predicate is exactly the already-formalized finite detyping predicate, on every pair of questions.
theorem
MIPRE.CL.Detyping.DeciderProgram.bounded_acceptance_edge
{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)
(hD : D.Total)
(n : ℕ)
(x y : Question T (Fin (S.dim n)))
(hE : E x.1 y.1)
(a b : Verifier.Answers (C.outer n))
:
decide
((decider E S D C).Accepts n (toBits (push (registerEquiv (S.dim n)).toEmbedding (question E false x)))
(toBits (push (registerEquiv (S.dim n)).toEmbedding (question E true y))) ↑a ↑b) = typedPredicate S D C n x y a b
In particular, a genuine edge preserves the source typed acceptance law and cutoff.
theorem
MIPRE.CL.Detyping.DeciderProgram.verifier_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 : ℕ)
(x y : Coord T (Fin (S.dim n)) → 𝔽₂)
(a b : Verifier.Answers (C.outer n))
:
((verifier E S D C hℓ hD).game n (C.outer n)).D (push (registerEquiv (S.dim n)).toEmbedding x)
(push (registerEquiv (S.dim n)).toEmbedding y) a b = accepts E (typedPredicate S D C n) x y a b
Predicate equality for the actual ambient verifier's finite game.