theorem
proved
term proof
rs_adversarial_lower_bound
show as:
view Lean formalization →
formal statement (Lean)
169theorem rs_adversarial_lower_bound (n : ℕ) (M : Finset (Fin n))
170 (g : ({i // i ∈ M} → Bool) → Bool) :
171 ∃ (b : Bool) (R : Fin n → Bool),
172 g (BalancedParityHidden.restrict (BalancedParityHidden.enc b R) M) ≠ b :=
proof body
Term-mode proof.
173 BalancedParityHidden.adversarial_failure M g
174
175/-- The R̂ certifier is "non-natural" in the sense that it uses the entire
176 assignment at once (global, not local). The adversarial failure shows
177 that any LOCAL certifier fails, while R̂'s global evaluation succeeds. -/