Query routing for the detyped CL presentation #
The semantic specification of all branches of types.tex, def:detyped-sampler.
The level indices of factor and linear queries are zero based, as in CLFun.
These are equalities of the actual presentations' queries, not extra assumptions
on a future sampler program.
theorem
MIPRE.CL.CLFun.truncate_concat_add
{F : Type u_1}
{ι : Type u_2}
[Semiring F]
[DecidableEq ι]
{k ℓ : ℕ}
(L : CLFun F ι k)
(R : (ι → F) → CLFun F ι ℓ)
(j : ℕ)
:
Truncation after concatenation keeps the full first part and truncates the second.
theorem
MIPRE.CL.CLFun.truncate_concat_le
{F : Type u_1}
{ι : Type u_2}
[Semiring F]
[DecidableEq ι]
{k ℓ : ℕ}
(L : CLFun F ι k)
(R : (ι → F) → CLFun F ι ℓ)
(j : ℕ)
(hj : j ≤ k)
:
Truncation inside the first part never visits a concatenation's continuation.
theorem
MIPRE.CL.Detyping.content_proj_graph_compl
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
(S : Finset (Graph.Coord T))
(x : Coord T ι → ZMod 2)
:
theorem
MIPRE.CL.Detyping.graph_prefix
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
(S : Finset (Graph.Coord T))
(x : Coord T ι → ZMod 2)
:
pull Function.Embedding.inl
((proj (Finset.map Function.Embedding.inl S)) x + (proj (Finset.map Function.Embedding.inl Sᶜ)) ((proj (Finset.map Function.Embedding.inl S)ᶜ) x)) = pull Function.Embedding.inl x
theorem
MIPRE.CL.Detyping.presentation_cons
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
:
presentation E w P = CLFun.cons (Finset.map Function.Embedding.inl (Graph.own w))
(RegLinear.embed Function.Embedding.inl (RegLinear.id (Graph.own w))) fun (a : Coord T ι → ZMod 2) =>
CLFun.cons (Finset.map Function.Embedding.inl (Graph.own w)ᶜ)
(RegLinear.embed Function.Embedding.inl (Graph.second E w (pull Function.Embedding.inl a)))
fun (b : Coord T ι → ZMod 2) =>
CLFun.embed Function.Embedding.inr (selected P (select E w (pull Function.Embedding.inl (a + b))))
Expanding the first two levels exposes the exact prefix used for type selection.
theorem
MIPRE.CL.Detyping.marginal_graph
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(j : ℕ)
(hj : j ≤ 2)
(x : Coord T ι → ZMod 2)
:
(CLFun.truncate j (presentation E w P)).eval x = push Function.Embedding.inl ((CLFun.truncate j (Graph.presentation E w)).eval (pull Function.Embedding.inl x))
Marginals through level two are precisely graph marginals with zero content.
theorem
MIPRE.CL.Detyping.marginal_content
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(hP : ∀ (t : T), (P t).ExactlyOn Finset.univ)
(hℓ : 0 < ℓ)
(j : ℕ)
(x : Coord T ι → ZMod 2)
:
(CLFun.truncate (j + 2) (presentation E w P)).eval x = Sum.elim ((Graph.presentation E w).eval (pull Function.Embedding.inl x))
((CLFun.truncate j (selected P (select E w (pull Function.Embedding.inl x)))).eval (pull Function.Embedding.inr x))
Later marginals pair the full graph question with the selected content marginal.
theorem
MIPRE.CL.Detyping.factor_first
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(x : Coord T ι → ZMod 2)
:
The first factor is the player's own two graph blocks.
theorem
MIPRE.CL.Detyping.factor_second
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(x : Coord T ι → ZMod 2)
:
The second factor is the entire opposite pair of graph blocks.
theorem
MIPRE.CL.Detyping.factor_content
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(j : ℕ)
(x : Coord T ι → ZMod 2)
:
(presentation E w P).factorOfPrefix (j + 2) x = Finset.map Function.Embedding.inr
((selected P (select E w (pull Function.Embedding.inl x))).factorOfPrefix j (pull Function.Embedding.inr x))
Later factors are exactly the selected content factors, read from the content prefix.
theorem
MIPRE.CL.Detyping.linear_first
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(x y : Coord T ι → ZMod 2)
:
((presentation E w P).mapOfPrefix 0 x) y = push Function.Embedding.inl ((proj (Graph.own w)) (pull Function.Embedding.inl y))
The first linear query copies the player's own graph blocks.
theorem
MIPRE.CL.Detyping.linear_second
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(x y : Coord T ι → ZMod 2)
:
((presentation E w P).mapOfPrefix 1 x) y = push Function.Embedding.inl
((Graph.second E w ((proj (Graph.own w)) (pull Function.Embedding.inl x))) (pull Function.Embedding.inl y))
The second linear query keeps the neighbor bit selected by the graph prefix.
theorem
MIPRE.CL.Detyping.linear_content
{T : Type u_1}
{ι : Type u_2}
[Fintype T]
[DecidableEq T]
[Fintype ι]
[DecidableEq ι]
{ℓ : ℕ}
(E : T → T → Prop)
[DecidableRel E]
(w : Bool)
(P : T → CLFun (ZMod 2) ι ℓ)
(j : ℕ)
(x y : Coord T ι → ZMod 2)
:
((presentation E w P).mapOfPrefix (j + 2) x) y = push Function.Embedding.inr
(((selected P (select E w (pull Function.Embedding.inl x))).mapOfPrefix j (pull Function.Embedding.inr x))
(pull Function.Embedding.inr y))
Later linear queries are exactly the selected typed queries, with zero graph output.