Documentation

MIPRE.Foundations.CL.DetypingCompleteSupport

The common measurement rule and support of detyping #

Both players use one decoder of graph views. It agrees with their own type selector on sampled questions, and otherwise selects a deterministic fallback. This is the player-independent rule in types.tex, lem:detyping-verifiers.

source
noncomputable def MIPRE.CL.Detyping.decodeView {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (g : Graph.Coord T → ZMod 2) :
Option (Bool × T)

The common decoder recognizes either player's full valid graph view.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.CL.Detyping.view_injective {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) :
    Function.Injective (view E w)

    Graph views uniquely determine the type within either pattern family.

    source
    theorem MIPRE.CL.Detyping.decodeView_view {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (u : T) :
    decodeView E (view E w u) = some (w, u)

    The common decoder recognizes every valid question with its original tag.

    source
    theorem MIPRE.CL.Detyping.graph_output_opposite_vertex {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) (u : T) :
    (Graph.presentation E w).eval g (!w, false, u) = 0

    The graph sampler always erases the other player's vertex block.

    source
    theorem MIPRE.CL.Detyping.graph_output_ne_opposite_view {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) (u : T) :
    (Graph.presentation E w).eval g ≠ view E (!w) u

    A sampled graph view cannot be a valid view of the opposite player.

    source
    theorem MIPRE.CL.Detyping.decodeView_output {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) :
    decodeView E ((Graph.presentation E w).eval g) = Option.map (fun (x : T) => (w, x)) (select E w g)

    On a sampled graph view, the common decoder is exactly the local selector.

    source
    noncomputable def MIPRE.CL.Detyping.decodeQuestion {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (q : Coord T ι → ZMod 2) :
    Option (Bool × Question T ι)

    Decode a full question, retaining its content register.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.CL.Detyping.decodeQuestion_question {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (w : Bool) (q : Question T ι) :
      decodeQuestion E (question E w q) = some (w, q)

      A fixed embedded typed question is decoded exactly.

      source
      theorem MIPRE.CL.Detyping.decodeQuestion_output {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) :
      decodeQuestion E ((presentation E w P).eval (Sum.elim g v)) = Option.map (fun (u : T) => (w, u, (P u).eval v)) (select E w g)

      On samples the decoder selects the original typed content, or the trivial branch.

      source
      theorem MIPRE.CL.Detyping.selects_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) (g : Graph.Coord T → ZMod 2) {u v : T} (hu : select E false g = some u) (hv : select E true g = some v) :
      E u v ∧ g = Graph.pairSeed E (u, v)

      Successful selection by both players identifies the common edge seed.