The finite big Ramsey degrees of Henson graphs are provable in $\mathrm{ACA}_0$

Let $\mathbb{H}_{n+1}$ denote a computable copy of the $(n+1)$-clique free universal homogeneous Henson graph, $G$ denote a finite subgraph of $\mathbb{H}_{n+1}$, and $k(G,n)$ denote the big Ramsey degree of $G$ in $\mathbb{H}_{n+1}$.

We prove that for any computable coloring $\chi$ of the copies of $G$ in $\mathbb{H}_{n+1}$, there is a copy $\mathbb{H}'$ of $\mathbb{H}_{n+1}$ that is computable from $0^{(2\delta(G,n)-1)}$ in which $\chi$ takes no more than $k(G,n)$ colors, where $\delta(G,n)$ denotes the maximum number of levels of a diary for $G$ in $\mathbb{H}_{n+1}$ (this is a finite number).

It follows that the statement, ``Henson graphs have finite big Ramsey degrees," is provable in ACA$_0'$.

Combining this with a recent result of Cholak, Dobrinen, and McCoy \cite{CDM} yields the equivalence of the statement with ACA$_0'$ over RCA$_0$.