The joint law of detyped questions

On an ordered edge the graph view depends only on the player's own type. Conditioning on the valid-edge event gives the uniform ordered-edge law and one shared uniform content seed, exactly as in types.tex, def:detyped-CL.

def MIPRE.CL.Detyping.view {T : Type u_1} [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (u : T) : Graph.Coord T → ZMod 2

The fixed valid graph question of one type, independent of the neighboring type.

Equations

• MIPRE.CL.Detyping.view E w u p = if p.1 = w then MIPRE.CL.Graph.encode E u p.2 else if p = (!w, true, u) then 1 else 0

theorem MIPRE.CL.Detyping.graph_output_of_select {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) {u : T} (h : select E w g = some u) : (Graph.presentation E w).eval g = view E w u

Every valid local sample is exactly the fixed graph question of its selected type.

theorem MIPRE.CL.Detyping.select_pairSeed {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (w : Bool) (uv : T × T) (huv : E uv.1 uv.2) : select E w (Graph.pairSeed E uv) = some (if w = true then uv.2 else uv.1)

On an adjacent seed the two players select exactly its two endpoint types.

theorem MIPRE.CL.Detyping.presentation_eval_valid {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 < ℓ) (g : Graph.Coord T → ZMod 2) (v : ι → ZMod 2) {u : T} (hu : select E w g = some u) : (presentation E w P).eval (Sum.elim g v) = Sum.elim (view E w u) ((P u).eval v)

On valid seeds the detyped question retains precisely the selected type's content.

theorem MIPRE.CL.Detyping.presentation_eval_invalid {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 < ℓ) (g : Graph.Coord T → ZMod 2) (v : ι → ZMod 2) (hg : ¬Graph.localValid E w g) : (presentation E w P).eval (Sum.elim g v) = Sum.elim ((Graph.presentation E w).eval g) 0

On invalid local seeds the entire content output is zero.

theorem MIPRE.CL.Detyping.sum_valid_questions {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {M : Type u_3} [AddCommMonoid M] (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (f : (Coord T ι → ZMod 2) → (Coord T ι → ZMod 2) → M) : ∑ g ∈ Graph.validSeeds E, ∑ v : ι → ZMod 2, f ((presentation E false (P false)).eval (Sum.elim g v)) ((presentation E true (P true)).eval (Sum.elim g v)) = ∑ uv ∈ Graph.edges E, ∑ v : ι → ZMod 2, f (Sum.elim (view E false uv.1) ((P false uv.1).eval v)) (Sum.elim (view E true uv.2) ((P true uv.2).eval v))

The joint valid-seed sum is exactly the typed edge-and-common-seed sum. In particular, no independence of the two content outputs is asserted or needed.

theorem MIPRE.CL.Detyping.conditional_average {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (f : (Coord T ι → ZMod 2) → (Coord T ι → ZMod 2) → ℝ) : (∑ g ∈ Graph.validSeeds E, ∑ v : ι → ZMod 2, f ((presentation E false (P false)).eval (Sum.elim g v)) ((presentation E true (P true)).eval (Sum.elim g v))) / (↑(Graph.validSeeds E).card * ↑(Fintype.card (ι → ZMod 2))) = (∑ uv ∈ Graph.edges E, ∑ v : ι → ZMod 2, f (Sum.elim (view E false uv.1) ((P false uv.1).eval v)) (Sum.elim (view E true uv.2) ((P true uv.2).eval v))) / (↑(Graph.edges E).card * ↑(Fintype.card (ι → ZMod 2)))

The conditional joint law is the uniform ordered-edge law with a shared uniform seed.