rs_adversarial_lower_bound

formal source

 166    any fixed-view decoder on a proper subset of variables can be fooled.
 167    This is the RS version of the natural proof barrier: no local property
 168    of the formula can certify unsatisfiability. -/
 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 :=
 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. -/
 178theorem rhat_is_non_natural (n : ℕ) :
 179    ¬ ∃ (M : Finset (Fin n)),
 180      (M.card < n) ∧
 181      ∀ (f : CNFFormula n) (_ : f.isSAT),
 182        ∃ g : ({i // i ∈ M} → Bool) → Bool,
 183          ∀ R : Fin n → Bool,
 184            g (BalancedParityHidden.restrict R M) = (f.clauses.any
 185              (fun c => c.satisfiedBy (fun i => R i))).not.not := by
 186  intro ⟨M, hcard, hforall⟩
 187  -- Since |M| < n, there exists j ∉ M
 188  have ⟨j, hj⟩ : ∃ j : Fin n, j ∉ M := by
 189    by_contra hall; push_neg at hall
 190    have hsub : Finset.univ ⊆ M := fun x _ => hall x
 191    exact absurd (Finset.card_le_card hsub) (by simp [Finset.card_fin]; omega)
 192  -- Construct a single-clause formula depending only on variable j
 193  let clause_j : Clause n := ⟨[(j, true)], by simp⟩
 194  let φ : CNFFormula n := ⟨[clause_j], n, rfl⟩
 195  -- φ is SAT: the all-true assignment satisfies it
 196  have hsat : φ.isSAT := by
 197    refine ⟨fun _ => true, ?_⟩
 198    simp only [CNFFormula.satisfiedBy, φ, List.all_cons, List.all_nil, Bool.and_true,
 199               Clause.satisfiedBy, clause_j, List.any_cons, List.any_nil, Bool.or_false,