Completeness of intuitionistic logic over the paper's logical consequence relation

Let $\models$ be the logical-consequence relation defined in the paper's monotonic proof-theoretic semantics, and let $\texttt{IL}$ denote intuitionistic logic. Completeness over $\models$ means that whenever $\Gamma \models A$, the sequent $\Gamma \vdash_{\texttt{IL}} A$ is derivable. The completeness claim. The source states that $\texttt{IL}$ is complete over $\models$.

This claim is presented as the logical-consequence formulation corresponding to Prawitz's conjecture. The supplied text does not establish whether this formulation is proved or refuted; subsequent discussion instead concerns incompleteness phenomena and closure under substitutions.