`recognition_lower_bound_sat`

proved

show as: view math explainer →

module: IndisputableMonolith.Complexity.BalancedParityHidden
domain: Complexity
line: 105 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.BalancedParityHidden on GitHub at line 105.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.