Repeated squaring of fortified projection tests

Lax323828.FortifiedSquaring · concepts/Lax323828/FortifiedSquaring.lean · lax-323828

proven

Loading review…

Natural Language Statement

Theorem

A projection test compares two locally valid answers after mapping them to a common alphabet B. Suppose its value is at most s, and every rectangular restriction has unnormalized winning probability at most v times the rectangle's probability plus eta. Two parallel copies then have value at most v*s + |B|*eta.

The error depends on the common projection alphabet, which remains fixed when tuple questions enlarge the prover-answer alphabet. This is the squaring step in the fortification approach to soundness amplification.

Concept map

2 concepts; 5 descendants hidden

100%

Proven claimThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

- thm✓Lax323828.FiniteProbability
→
thm✓Lax323828.FortifiedSquaring
⊢Lax323828Proofs.fortified_squaring_sound

Lean source view on GitHub

1	import Lax323828.FiniteProbability
2	import Mathlib.Data.Fintype.Prod
3
4	/-!
5	---
6	title: Repeated squaring of fortified projection tests
7	type: theorem
8	---
9	A projection test compares two locally valid answers after mapping them
10	to a common alphabet B. Suppose its value is at most s, and every
11	rectangular restriction has unnormalized winning probability at most
12	v times the rectangle's probability plus eta. Two parallel copies then
13	have value at most vs + \|B\|eta.
14
15	The error depends on the common projection alphabet, which remains fixed
16	when tuple questions enlarge the prover-answer alphabet. This is the
17	squaring step in the fortification approach to soundness amplification.
18	-/
19
20	namespace Lax323828.FortifiedSquaring
21
22	open FiniteProbability
23
24	structure Game (Z W A B : Type) where
25	left : Z → W
26	right : Z → W
27	validLeft : Z → A → Bool
28	validRight : Z → A → Bool
29	projectLeft : Z → A → B
30	projectRight : Z → A → B
31
32	namespace Game
33
34	variable {Z W A B : Type} (G : Game Z W A B)
35
36	def Test (z : Z) (a b : A) : Prop :=
37	G.validLeft z a = true ∧ G.validRight z b = true ∧
38	G.projectLeft z a = G.projectRight z b
39
40	def Wins (P Q : W → A) (z : Z) : Prop := G.Test z (P (G.left z)) (Q (G.right z))
41
42	def Sound [Fintype Z] (s : ℝ) : Prop :=
43	∀ P Q : W → A, probability (G.Wins P Q) ≤ s
44
45	def Fortified [Fintype Z] (v η : ℝ) : Prop :=
46	∀ (P Q : W → A) (S T : W → Prop),
47	probability (fun z ↦ G.Wins P Q z ∧ S (G.left z) ∧ T (G.right z)) ≤
48	v * probability (fun z ↦ S (G.left z) ∧ T (G.right z)) + η
49
50	def DoubleWins (P Q : W × W → A × A) (z : Z × Z) : Prop :=
51	let a := P (G.left z.1, G.left z.2)
52	let b := Q (G.right z.1, G.right z.2)
53	G.Test z.1 a.1 b.1 ∧ G.Test z.2 a.2 b.2
54
55	end Game
56
57	axiom soundness {Z W A B : Type} [Fintype Z] [Nonempty Z] [Fintype B]
58	(G : Game Z W A B) (s v η : ℝ) (hv : 0 ≤ v)
59	(hs : G.Sound s) (hfort : G.Fortified v η)
60	(P Q : W × W → A × A) :
61	probability (G.DoubleWins P Q) ≤ v * s + (Fintype.card B : ℝ) * η
62
63	end Lax323828.FortifiedSquaring
64