[proofplan]
We prove the conservativity claim directly from the acceptance invariant. Fix an arbitrary accepted surface theorem declaration and look at the kernel environment that existed before that declaration was accepted. The hypothesis says that acceptance supplies a closed core proof term of the claimed proposition, checked by the kernel in precisely that prior environment. Since kernel derivability of a proposition over an environment is exactly the existence of such a checked closed term, the claimed proposition was already derivable in the kernel theory with the previously accepted declarations.
[/proofplan]
[step:Fix an accepted surface theorem and its prior kernel environment]
Let $d$ be an accepted surface theorem declaration. Let $P$ denote the proposition claimed by $d$, and let $E$ denote the well-formed kernel environment consisting exactly of the declarations accepted before $d$ is processed. We must prove that $P$ is derivable in the kernel theory $\mathcal K$ extended by $E$.
The phrase "previously accepted declarations" is therefore interpreted relative to $d$: the environment $E$ excludes $d$ itself. This prevents the conclusion from using the theorem being accepted as one of its own assumptions.
[/step]
[step:Extract the checked core proof term from acceptance]
By the stated acceptance invariant, acceptance of the surface theorem declaration $d$ requires elaboration to produce an explicit core declaration $\widehat d$ checked by the kernel in the environment $E$. Since $d$ claims the proposition $P$, the theorem-specific part of the invariant gives a closed core term $p$ such that
\begin{align*}
E \vdash_{\mathcal K} p : P.
\end{align*}
Here $p$ is closed relative to the environment $E$: it has no free variables other than the constants and declarations already present in $E$. Any implicit arguments, coercions, tactic-generated terms, or searched-for witnesses used by the surface language have already been resolved into the explicit core term $p$ before the kernel judgment is accepted.
[guided]
We now use the only trusted fact about the elaborator. The elaborator may do substantial work before producing a term: it may infer omitted arguments, insert coercions, run automation, unfold notation, or synthesize intermediate expressions. None of those operations is itself treated as a proof of $P$. The proof object that matters is the final explicit core term.
For the accepted surface theorem declaration $d$, the hypothesis says that acceptance occurs only after the kernel checks the generated core declaration in the environment $E$. Because $d$ claims proposition $P$, the generated core theorem contains a closed core proof term $p$ whose type is the claimed proposition, as judged by the kernel:
\begin{align*}
E \vdash_{\mathcal K} p : P.
\end{align*}
The word "closed" is important here. It means that $p$ depends only on the constants and declarations already available in $E$, not on untrusted surface-language state and not on the theorem $d$ as a newly added assumption. If the elaborator chose a different candidate term, the kernel would check that different candidate. If elaboration failed to produce a candidate term, no accepted theorem declaration would result. Thus acceptance gives exactly the kernel judgment displayed above.
[/guided]
[/step]
[step:Translate the checked core judgment into kernel derivability]
By definition, a proposition $P$ is derivable in the kernel theory $\mathcal K$ extended by the environment $E$ when there exists a closed core term $p$ such that the kernel verifies
\begin{align*}
E \vdash_{\mathcal K} p : P.
\end{align*}
The previous step supplies exactly such a term $p$. Hence $P$ is derivable in $\mathcal K$ with the previously accepted declarations $E$.
[/step]
[step:Conclude conservativity for all accepted elaborated theorems]
The surface theorem declaration $d$ was arbitrary among accepted surface theorem declarations. Therefore every theorem proposition accepted through elaboration is already derivable by a kernel-checked closed core term over the environment of previously accepted declarations.
Thus elaboration affects how users construct candidate core terms, but it does not enlarge the set of theorem propositions accepted by the system beyond those derivable in the kernel theory with the prior accepted environment. This is precisely the conservativity of elaboration over kernel checking.
[/step]
