Same-state soundness of finite-game detyping

Restricting to the fixed graph views gives a strategy for the typed game on literally the same state. The only loss is conditioning on the valid graph event. This proves the finite-game core of types.tex, lem:detyping-verifiers; the program's answer cutoff and runtime remain separate obligations.

theorem MIPRE.CL.Detyping.valid_average_le {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] (E : T → T → Prop) [DecidableRel E] (hne : (Graph.edges E).Nonempty) (f : (Graph.Coord T → ZMod 2) → (ι → ZMod 2) → ℝ) (hf : ∀ (g : Graph.Coord T → ZMod 2) (v : ι → ZMod 2), 0 ≤ f g v) : (∑ g ∈ Graph.validSeeds E, ∑ v : ι → ZMod 2, f g v) / (↑(Graph.validSeeds E).card * ↑(Fintype.card (ι → ZMod 2))) ≤ 16 ^ Fintype.card T * ((∑ g : Graph.Coord T → ZMod 2, ∑ v : ι → ZMod 2, f g v) / (16 ^ Fintype.card T * ↑(Fintype.card (ι → ZMod 2))))

Conditioning a nonnegative quantity on valid graph seeds costs at most 16 ^ |T|.

theorem MIPRE.CL.Detyping.restrict_failure_eq {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (game E P D)) : 1 - (restrict E hne P D S).value = (∑ g ∈ Graph.validSeeds E, ∑ v : ι → ZMod 2, S.failAt ((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)))

Exact identification of the restricted strategy's failure with conditional detyped failure.

theorem MIPRE.CL.Detyping.restrict_failure_le {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (game E P D)) : 1 - (restrict E hne P D S).value ≤ 16 ^ Fintype.card T * (1 - S.value)

The finite-game detyping reduction, with the source's explicit soundness factor.

theorem MIPRE.CL.Detyping.restrict_value_ge {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (hE : ∀ (u v : T), E u v → E v u) (hne : (Graph.edges E).Nonempty) (P : Bool → T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (w : Bool) (t : T), (P w t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (D : Question T ι → Question T ι → A → B → Bool) (S : TensorProductStrategy (game E P D)) {ε : ℝ} (hS : 1 - ε ≤ S.value) : 1 - 16 ^ Fintype.card T * ε ≤ (restrict E hne P D S).value

A near-perfect detyped strategy yields the claimed same-state typed strategy.