lemma
proved
tactic proof
restrict_extendMask
show as:
view Lean formalization →
formal statement (Lean)
43@[simp] lemma restrict_extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) :
44 restrict (n:=n) (extendMask (n:=n) M a) M = a := by
proof body
Tactic-mode proof.
45 funext i
46 simp [restrict, extendMask]
47
48/-- Any fixed-view decoder on a set `M` of queried indices can be fooled by a suitable `(b,R)`. -/
49 theorem adversarial_failure (M : Finset (Fin n))
50 (g : (({i // i ∈ M} → Bool)) → Bool) :
51 ∃ (b : Bool) (R : Fin n → Bool),
52 g (restrict (n:=n) (enc b R) M) ≠ b := by
53 classical
54 -- Pick an arbitrary local view `a` and force the decoder to predict `b' := g a`.
55 let a : {i // i ∈ M} → Bool := fun _ => false
56 let b' : Bool := g a
57 -- Choose the true bit to be the opposite of the decoder's prediction.
58 let b : Bool := ! b'
59 -- Choose the mask so that the restricted encoding equals `a`.
60 let R : Fin n → Bool :=
61 if b then extendMask M (fun i => ! (a i)) else extendMask M a
62 have hRestr : restrict (n:=n) (enc b R) M = a := by
63 funext i
64 dsimp [restrict, enc, R, extendMask]
65 by_cases hb : b
66 · -- b = true
67 simp [hb, dif_pos i.property]
68 · -- b = false
69 simp [hb, dif_pos i.property]
70 refine ⟨b, R, ?_⟩
71 have hval' : g (restrict (n:=n) (enc b R) M) = g a := by
72 simpa [hRestr]
73 have hval : g (restrict (n:=n) (enc b R) M) = b' := by
74 simpa [b'] using hval'
75 have hbrel : b = ! b' := rfl
76 have ne : b' ≠ ! b' := by cases b' <;> decide
77 have : g (restrict (n:=n) (enc b R) M) ≠ ! b' := by simpa [hval]
78 simpa [hbrel]
79
80/-- If a decoder is correct for all `(b,R)` while querying only `M`, contradiction. -/
81 theorem no_universal_decoder (M : Finset (Fin n))
82 (g : (({i // i ∈ M} → Bool)) → Bool) :
83 ¬ (∀ (b : Bool) (R : Fin n → Bool), g (restrict (n:=n) (enc b R) M) = b) := by
84 classical
85 intro h
86 rcases adversarial_failure (n:=n) M g with ⟨b, R, hw⟩
87 have := h b R
88 exact hw this
89
90/-- Query lower bound (worst-case, adversarial): any universally-correct decoder
91 must inspect all `n` indices. -/