Consider the generative model $$ \begin{align} \theta &\sim \pi(\cdot \mid \phi),\\ y \mid \theta &\sim f(\cdot \mid \theta). \end{align} $$ Compute the posterior distribution $p(\theta \mid y) \propto f(y \mid \theta) \pi(\theta \mid \phi)$, and define $$ Q_{y,\phi}(x) = \frac{\int_{-\infty}^x f(y \mid t) \pi(t \mid \phi)\,dt}{\int_{-\infty}^\infty f(y \mid t) \pi(t \mid \phi)\,dt}, $$ as the posterior CDF. Now, for $0 < \gamma < 1$, take $I_{\phi, \gamma}(y) = \left(a(y), b(y)\right)$ such that $Q_{y, \phi}(b(y))-Q_{y, \phi}(a(y)) = \gamma$, i.e., $I_{\phi, \gamma}(y)$ is a $\gamma\%$ credibility interval* for $\theta$.
Question: Is it true that $$ \operatorname{Pr}(\theta \in I_{\phi, \gamma}(y) \mid \theta) \geq \gamma? $$ In other words, does the $\gamma\%$ credibility interval have $\gamma\%$ coverage when the data are generated according to the model above and the posterior is computed using the same prior $\pi(\cdot \mid \phi)$?
These related questions : q1 and q2 suggest this is true, but I could not for the life of me find a proof. It seems, for instance, that one can show that $$ \operatorname{Pr}(\theta \in I_{\phi, \gamma}(y) \mid \theta) = \gamma + \epsilon_n, $$ where $|\epsilon_n| < a/n$ for some $a$. See page 41 here. I suppose then that it remains to show that for the particular situation of interest here, $\epsilon_n=0$ for all $n$.
*- If you want, you can take the infimum over $b(y)-a(y)$ such that the condition is satisfied, just so that the interval is shortest.