pith. machine review for the scientific record. sign in
theorem proved term proof

conditional_separation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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. -/

depends on (8)

Lean names referenced from this declaration's body.