IndisputableMonolith.Complexity.BalancedParityHidden

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Complexity
   5namespace BalancedParityHidden
   6
   7variable {n : ℕ} [DecidableEq (Fin n)]
   8
   9/-- Hidden mask encoder: bit b with mask R is `R` if b=false and `not ∘ R` if b=true. -/
  10def enc (b : Bool) (R : Fin n → Bool) : Fin n → Bool :=
  11  fun i => if b then ! (R i) else R i
  12
  13@[simp] lemma enc_false (R : Fin n → Bool) : enc (n:=n) false R = R := by
  14  funext i; simp [enc]
  15
  16@[simp] lemma enc_true (R : Fin n → Bool) : enc (n:=n) true R = (fun i => ! (R i)) := by
  17  funext i; simp [enc]
  18
  19/-- Restrict a full word to a queried index set `M`. -/
  20def restrict (f : Fin n → Bool) (M : Finset (Fin n)) : {i // i ∈ M} → Bool :=
  21  fun i => f i.val
  22
  23@[simp] lemma restrict_enc_false (R : Fin n → Bool) (M : Finset (Fin n)) :
  24  restrict (n:=n) (enc false R) M = restrict (n:=n) R M := by
  25  funext i; simp [restrict, enc]
  26
  27@[simp] lemma restrict_enc_true (R : Fin n → Bool) (M : Finset (Fin n)) :
  28  restrict (n:=n) (enc true R) M = (fun i => ! (restrict (n:=n) R M i)) := by
  29  funext i; simp [restrict, enc]
  30
  31/-- Extend a partial assignment on `M` to a full mask by defaulting to `false` off `M`. -/
  32def extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) : Fin n → Bool :=
  33  fun i => if h : i ∈ M then a ⟨i, h⟩ else false
  34
  35@[simp] lemma extendMask_in (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∈ M) :
  36  extendMask (n:=n) M a i = a ⟨i, h⟩ := by
  37  simp [extendMask, h]
  38
  39@[simp] lemma extendMask_notin (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∉ M) :
  40  extendMask (n:=n) M a i = false := by
  41  simp [extendMask, h]
  42
  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
  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. -/
  92theorem omega_n_queries
  93  (M : Finset (Fin n)) (g : (({i // i ∈ M} → Bool)) → Bool)
  94  (hMlt : M.card < n) :
  95  ¬ (∀ (b : Bool) (R : Fin n → Bool), g (restrict (n:=n) (enc b R) M) = b) :=
  96  no_universal_decoder (n:=n) M g
  97
  98end BalancedParityHidden
  99end Complexity
 100
 101namespace IndisputableMonolith
 102
 103/-- SAT recognition lower bound (dimensionless): any universally-correct fixed-view
 104    decoder over fewer than n queried indices is impossible. -/
 105theorem recognition_lower_bound_sat
 106  (n : ℕ) (M : Finset (Fin n))
 107  (g : (({i // i ∈ M} → Bool)) → Bool)
 108  (hMlt : M.card < n) :
 109  ¬ (∀ (b : Bool) (R : Fin n → Bool),
 110        g (Complexity.BalancedParityHidden.restrict
 111              (Complexity.BalancedParityHidden.enc b R) M) = b) := by
 112  classical
 113  simpa using
 114    (Complexity.BalancedParityHidden.omega_n_queries (n:=n) M g hMlt)
 115
 116end IndisputableMonolith
 117