The two-level graph sampler

The graph may have loops. Its law is uniform on ordered adjacent pairs, so each loop is counted once. This file supplies the semantic CL presentations; compiling their finite graph table into an ambient sampler program is a separate obligation.

@[reducible, inline]

abbrev MIPRE.CL.Graph.Coord (T : Type u_2) : Type u_2

Four binary blocks: player, vertex/neighbor indicator, vertex.

Equations

• MIPRE.CL.Graph.Coord T = (Bool × Bool × T)

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

A vertex's one-hot indicator together with its neighbor indicator.

Equations

• MIPRE.CL.Graph.encode E u p = if p.1 = true then if E u p.2 then 1 else 0 else if p.2 = u then 1 else 0

theorem MIPRE.CL.Graph.encode_injective {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : Function.Injective (encode E)

The one-hot half makes the encoding injective, even for an isolated vertex.

noncomputable def MIPRE.CL.Graph.decode {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (x : Bool × T → ZMod 2) : Option T

Decode the finite graph table; malformed blocks have no decoded vertex.

Equations

• MIPRE.CL.Graph.decode E x = if h : ∃ (u : T), x = MIPRE.CL.Graph.encode E u then some h.choose else none

theorem MIPRE.CL.Graph.decode_eq_some_iff {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (x : Bool × T → ZMod 2) (u : T) : decode E x = some u ↔ x = encode E u

Successful decoding means equality with the whole vertex-and-neighbor encoding.

def MIPRE.CL.Graph.own {T : Type u_1} [Fintype T] (w : Bool) : Finset (Coord T)

The first factor consists of the two blocks belonging to one player.

Equations

• MIPRE.CL.Graph.own w = {p : MIPRE.CL.Graph.Coord T | p.1 = w}

@[simp]

theorem MIPRE.CL.Graph.mem_own {T : Type u_1} [Fintype T] [DecidableEq T] (w : Bool) (p : Coord T) : p ∈ own w ↔ p.1 = w

noncomputable def MIPRE.CL.Graph.mask {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (x : Coord T → ZMod 2) : Finset (Coord T)

The second stage keeps just the relevant opposite neighbor bit when decoding succeeds.

Equations

• MIPRE.CL.Graph.mask E w x = match MIPRE.CL.Graph.decode E fun (p : Bool × T) => x (w, p) with | some u => {(!w, true, u)} | none => ∅

theorem MIPRE.CL.Graph.mask_subset {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (x : Coord T → ZMod 2) : mask E w x ⊆ (own w)ᶜ

The second-stage mask is contained in the complement of the first factor.

noncomputable def MIPRE.CL.Graph.second {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (x : Coord T → ZMod 2) : RegLinear (ZMod 2) (own w)ᶜ

The graph sampler's second-stage linear map, on the entire remaining factor.

Equations

• MIPRE.CL.Graph.second E w x = { toLinearMap := MIPRE.CL.proj (MIPRE.CL.Graph.mask E w x), proj_comp_proj' := ⋯ }

noncomputable def MIPRE.CL.Graph.presentation {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) : CLFun (ZMod 2) (Coord T) 2

The actual two-level CL presentation: own blocks, then one opposite neighbor bit.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.CL.Graph.presentation_exactlyOn {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) : (presentation E w).ExactlyOn Finset.univ

Its two factors partition all four blocks on every prefix, valid or otherwise.

theorem MIPRE.CL.Graph.mask_proj_own {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (z : Coord T → ZMod 2) : mask E w ((proj (own w)) z) = mask E w z

Projecting onto one's own first-stage block does not affect decoding.

theorem MIPRE.CL.Graph.presentation_eval {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (z : Coord T → ZMod 2) : (presentation E w).eval z = (proj (own w)) z + (proj (mask E w z)) z

The semantic output is the own block plus the selected opposite neighbor bit.

theorem MIPRE.CL.Graph.presentation_eval_own {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (z : Coord T → ZMod 2) (p : Bool × T) : (presentation E w).eval z (w, p) = z (w, p)

A player sees its entire own block unchanged.

theorem MIPRE.CL.Graph.presentation_eval_bit {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (z : Coord T → ZMod 2) {u : T} (hu : (fun (p : Bool × T) => z (w, p)) = encode E u) : (presentation E w).eval z (!w, true, u) = z (!w, true, u)

On an encoded first-stage block, the selected opposite neighbor bit is visible unchanged.

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

The local valid-view predicate, stated on the seed before applying the graph sampler.

Equations

• MIPRE.CL.Graph.localValid E w z = ∃ (u : T), (fun (p : Bool × T) => z (w, p)) = MIPRE.CL.Graph.encode E u ∧ z (!w, true, u) = 1

theorem MIPRE.CL.Graph.localValid_output_iff {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (z : Coord T → ZMod 2) : localValid E w ((presentation E w).eval z) ↔ localValid E w z

Validity can be decided from the local sampled question, with no access to the seed.

theorem MIPRE.CL.Graph.opposite_output {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (z : Coord T → ZMod 2) : (proj (own w)ᶜ) ((presentation E w).eval z) = (proj (mask E w z)) z

The opposite part of the sampled question contains exactly the selected bit.

theorem MIPRE.CL.Graph.opposite_output_zero_of_invalid {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (z : Coord T → ZMod 2) (h : ¬localValid E w z) : (proj (own w)ᶜ) ((presentation E w).eval z) = 0

An invalid local view has zero opposite-neighbor block, as required for PCC detyping.

def MIPRE.CL.Graph.pairSeed {T : Type u_1} [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (uv : T × T) : Coord T → ZMod 2

A seed encoding a pair of types. Each ordered pair has precisely this one seed.

Equations

• MIPRE.CL.Graph.pairSeed E uv p = MIPRE.CL.Graph.encode E (if p.1 = true then uv.2 else uv.1) p.2

theorem MIPRE.CL.Graph.pairSeed_injective {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : Function.Injective (pairSeed E)

Encoding an ordered pair is injective.

theorem MIPRE.CL.Graph.localValid_both_iff {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (z : Coord T → ZMod 2) : localValid E false z ∧ localValid E true z ↔ ∃ (uv : T × T), E uv.1 uv.2 ∧ z = pairSeed E uv

Both local valid views are exactly the encodings of adjacent ordered pairs.

def MIPRE.CL.Graph.edges {T : Type u_1} [Fintype T] (E : T → T → Prop) [DecidableRel E] : Finset (T × T)

Ordered edges; a loop contributes once.

Equations

• MIPRE.CL.Graph.edges E = {p : T × T | E p.1 p.2}

def MIPRE.CL.Graph.validSeeds {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : Finset (Coord T → ZMod 2)

The valid seeds, expressed as an image so their exact number is transparent.

Equations

• MIPRE.CL.Graph.validSeeds E = Finset.image (MIPRE.CL.Graph.pairSeed E) (MIPRE.CL.Graph.edges E)

theorem MIPRE.CL.Graph.card_validSeeds {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : (validSeeds E).card = (edges E).card

The rejection event has exactly one seed per ordered edge.

theorem MIPRE.CL.Graph.mem_validSeeds_iff {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (z : Coord T → ZMod 2) : z ∈ validSeeds E ↔ localValid E false z ∧ localValid E true z

The rejection event is the event that both players have valid local views.

theorem MIPRE.CL.Graph.invalid_seed_locally_detected {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (z : Coord T → ZMod 2) : z ∉ validSeeds E ↔ ¬localValid E false ((presentation E false).eval z) ∨ ¬localValid E true ((presentation E true).eval z)

On every rejected seed, at least one player recognizes an invalid local question.

theorem MIPRE.CL.Graph.card_seeds {T : Type u_1} [Fintype T] [DecidableEq T] : Fintype.card (Coord T → ZMod 2) = 16 ^ Fintype.card T

The four binary blocks have 16 ^ |T| seeds.

theorem MIPRE.CL.Graph.sum_validSeeds {T : Type u_1} [Fintype T] [DecidableEq T] {M : Type u_2} [AddCommMonoid M] (E : T → T → Prop) [DecidableRel E] (f : (Coord T → ZMod 2) → M) : ∑ z ∈ validSeeds E, f z = ∑ uv ∈ edges E, f (pairSeed E uv)

Uniform averaging on valid seeds is uniform averaging on ordered edges, without multiplicity.

noncomputable def MIPRE.CL.Graph.validProbability {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : ℝ

The probability of the valid-edge event under the uniform binary seed.

Equations

• MIPRE.CL.Graph.validProbability E = ↑(MIPRE.CL.Graph.validSeeds E).card / ↑(Fintype.card (MIPRE.CL.Graph.Coord T → ZMod 2))

theorem MIPRE.CL.Graph.validProbability_eq {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] : validProbability E = ↑(edges E).card / 16 ^ Fintype.card T

Exact rejection probability, with loops counted once among the ordered edges.

theorem MIPRE.CL.Graph.inv_pow_le_validProbability {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (hne : (edges E).Nonempty) : (16 ^ Fintype.card T)⁻¹ ≤ validProbability E

A graph with an edge has acceptance probability at least 16 ^ (-|T|).

theorem MIPRE.CL.Graph.conditional_average {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (f : (Coord T → ZMod 2) → ℝ) : (∑ z ∈ validSeeds E, f z) / ↑(validSeeds E).card = (∑ uv ∈ edges E, f (pairSeed E uv)) / ↑(edges E).card

Conditioning uniform seeds on acceptance gives the uniform ordered-edge law.