no_sublinear_universal_decoder

formal source

 223/-- **THEOREM (Sublinear Circuit Cannot Universally Decode).**
 224    No circuit querying fewer than n inputs can universally decode
 225    the balanced-parity encoding. -/
 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 :=
 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. -/
 239structure CircuitSeparation where
 240  /-- PROVED: R̂ reaches zero cost in ≤ n steps for SAT formulas -/
 241  rhat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT →
 242    ∃ (steps : ℕ) (a : Assignment n),
 243      steps ≤ n ∧ satJCost f a = 0
 244  /-- PROVED: UNSAT formulas have a defect moat of width ≥ 1 -/
 245  moat_exists : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
 246    ∀ a : Assignment n, satJCost f a ≥ 1
 247  /-- PROVED: no fixed-view decoder over fewer than n variables can
 248      universally certify the moat -/
 249  circuit_blind : ∀ n : ℕ, ∀ M : Finset (Fin n), M.card < n →
 250    ∀ decoder : ({i // i ∈ M} → Bool) → Bool,
 251      ¬ ∀ (b : Bool) (R : Fin n → Bool),
 252          decoder (restrict (enc b R) M) = b
 253  /-- PROVED: poly-size circuits have poly-bounded Z-capacity -/
 254  poly_circuit_bounded : ∀ n : ℕ, ∀ c : BooleanCircuit n,
 255    (∃ k d : ℕ, c.gate_count ≤ k * n ^ d) →
 256    ∃ k d : ℕ, CircuitZCapacity c ≤ k * n ^ d