conditional_separation

formal source

 304/-- **CONDITIONAL THEOREM**: Given SpectralTuringBridgeHypothesis,
 305    the TM time for SAT is Ω(n²), while R̂ needs only O(n) steps.
 306    For n ≥ 4, the TM lower bound exceeds the R̂ upper bound. -/
 307theorem conditional_separation
 308    (bridge : SpectralTuringBridgeHypothesis)
 309    (_sep : CircuitSeparation) :
 310    ∀ n : ℕ, ∃ (T_TM T_R : ℕ),
 311      T_TM ≥ n * (n / 2) ∧ T_R ≤ n + 1 := by
 312  intro n
 313  obtain ⟨T_TM, hTM⟩ := bridge.tm_time_lower_bound n
 314  obtain ⟨T_R, hTR⟩ := bridge.rhat_convergence n
 315  exact ⟨T_TM, T_R, hTM, hTR⟩
 316
 317/-! ## Certificate -/
 318
 319/-- **CircuitLedgerCert**: bundles all proved results in this module. -/
 320structure CircuitLedgerCert where
 321  /-- A poly-size circuit has poly-bounded Z-capacity -/
 322  capacity_bound : ∀ n : ℕ, ∀ c : BooleanCircuit n,
 323    CircuitZCapacity c ≤ 2 * c.gate_count
 324  /-- UNSAT formulas have a defect moat of width ≥ 1 -/
 325  moat_width : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →
 326    ∀ a : Assignment n, satJCost f a ≥ 1
 327  /-- No fixed-view decoder over <n variables is universal -/
 328  blind_decoder : ∀ n : ℕ, ∀ M : Finset (Fin n), M.card < n →
 329    ∀ g : ({i // i ∈ M} → Bool) → Bool,
 330      ∃ (b : Bool) (R : Fin n → Bool),
 331        g (restrict (enc b R) M) ≠ b
 332  /-- The full separation structure holds -/
 333  separation : CircuitSeparation
 334  /-- The open gap is identified -/
 335  open_gap : SpectralTuringBridgeHypothesis
 336
 337def circuitLedgerCert : CircuitLedgerCert where