rhat_is_non_natural

formal source

 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,
 200               Literal.satisfiedBy, ite_true]
 201  obtain ⟨g, hg⟩ := hforall φ hsat
 202  -- Two assignments: R₁ all-false, R₂ flips j to true
 203  let R₁ : Fin n → Bool := fun _ => false
 204  let R₂ : Fin n → Bool := fun i => i == j
 205  -- restrict R₁ M = restrict R₂ M (since j ∉ M, the only difference is invisible)
 206  have hrestr : BalancedParityHidden.restrict R₁ M = BalancedParityHidden.restrict R₂ M := by
 207    funext ⟨i, hi⟩
 208    simp only [BalancedParityHidden.restrict, R₁, R₂]