CircuitSeparation

formal source

 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
 257
 258/-- **THEOREM**: The circuit separation structure is instantiable with
 259    all proved components. -/
 260theorem circuitSeparation : CircuitSeparation where
 261  rhat_polytime := fun n f h =>
 262    let ⟨steps, a, hle, ha⟩ := sat_recognition_time_bound f h
 263    ⟨steps, a, hle, ha⟩
 264  moat_exists := fun _n f h => moat_width_unsat f h
 265  circuit_blind := fun _n M hM decoder => no_sublinear_universal_decoder _n M hM decoder
 266  poly_circuit_bounded := fun _n c h => poly_circuit_poly_capacity c h
 267
 268/-! ## Part 6: The Open Gap — Spectral to Turing Bridge -/
 269