226theorem no_sublinear_universal_decoder 227 (n : ℕ) (M : Finset (Fin n)) (hM : M.card < n) 228 (decoder : ({i // i ∈ M} → Bool) → Bool) : 229 ¬ ∀ (b : Bool) (R : Fin n → Bool), 230 decoder (restrict (enc b R) M) = b :=
proof body
Term-mode proof.
231 omega_n_queries M decoder hM 232 233/-! ## Part 5: The Circuit–R̂ Separation Structure -/ 234 235/-- The **circuit separation claim**: R̂ decides SAT in O(n) recognition steps, 236 while any circuit deciding SAT requires reading all n inputs. 237 238 Three proved components + one open gap. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.