poly_circuit_poly_capacity

formal source

 164  circuit_bond_count_le c
 165
 166/-- Corollary: a poly-size circuit has poly-bounded Z-capacity. -/
 167theorem poly_circuit_poly_capacity {n : ℕ} (c : BooleanCircuit n)
 168    (h_poly : ∃ (k d : ℕ), c.gate_count ≤ k * n ^ d) :
 169    ∃ (k d : ℕ), CircuitZCapacity c ≤ k * n ^ d := by
 170  obtain ⟨k, d, hk⟩ := h_poly
 171  exact ⟨2 * k, d, by
 172    calc CircuitZCapacity c ≤ 2 * c.gate_count := circuit_capacity_bound c
 173      _ ≤ 2 * (k * n ^ d) := by linarith
 174      _ = 2 * k * n ^ d := by ring⟩
 175
 176/-! ## Part 3: The Defect Moat -/
 177
 178/-- The **Defect Moat** for a formula f: 0 if SAT, 1 if UNSAT. -/
 179noncomputable def DefectMoat {n : ℕ} (f : CNFFormula n) : ℕ :=
 180  haveI := Classical.propDecidable f.isSAT
 181  if f.isSAT then 0 else 1
 182
 183/-- **THEOREM (Moat Width for UNSAT).**
 184    For an UNSAT formula, every assignment has J-cost ≥ 1. -/
 185theorem moat_width_unsat {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
 186    ∀ a : Assignment n, satJCost f a ≥ 1 :=
 187  unsat_cost_lower_bound f h
 188
 189/-- **THEOREM (Moat Width for SAT).**
 190    For a SAT formula, there exists a zero-cost assignment. -/
 191theorem moat_zero_sat {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
 192    ∃ a : Assignment n, satJCost f a = 0 :=
 193  sat_reaches_zero f h
 194
 195/-- The moat value equals 0 iff the formula is satisfiable. -/
 196theorem defect_moat_zero_iff_sat {n : ℕ} (f : CNFFormula n) :
 197    DefectMoat f = 0 ↔ f.isSAT := by