pith. machine review for the scientific record. sign in
theorem proved term proof

omega_n_queries

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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) :=

proof body

Term-mode proof.

  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. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.