Theorem: Evaluation identity and the printed pairing

Assume {(UCP${}_W$)}. For every $\xi \in {\mathfrak{g}}_W$ and every $u=(\gamma ,\varphi ,b)\in {{\mathcal{C}}_{\mathrm{sol}}}^{\mathrm{bos}}$,

In particular ${\Delta }_{\xi }\mathcal{O}=0$ on ${{\mathcal{C}}_{\mathcal{W}}}^{\mathrm{bos}}$, and on the detecting tuple of Input statement input:XIIF, realized with ${\xi }_{\ast }\in {\mathfrak{g}}_W$ and a switch satisfying {(UCP${}_W$)}, ${\Delta }_{{\xi }_{\ast }}\mathcal{O}(u_{\ast })=-8I<0$.

Proof. Every term of $D{s}_{\xi }[\gamma ]$ is supported in $\mathrm{supp}\xi \subset W$, so $\mathrm{supp}(K{\rho }_{\xi })\subset J^{+}(\overline{W})\cap M_T$, and {(UCP${}_W$)} implies (CP) for every smooth $\gamma$; XII-D's causal plateau proposition then gives ${\mathcal{A}}_1(K{\rho }_{\xi };\varphi )=0$ for free $\varphi$. This is XIII-A's argument and yields (eq:eval) from (eq:ledger-input). On ${{\mathcal{C}}_{\mathcal{W}}}^{\mathrm{bos}}$ the compact tensor ${\mathcal{L}}_{\xi }{\beta }_{f,g}[\varphi ]$ is supported in $W$, where $D^{\ast }b=0$, and the second form of (eq:ledger-input) vanishes. The witness value is (eq:witness-input); XIII-A records that $W$ can be chosen to contain $\mathrm{supp}{\xi }_{\ast }$ and $g$ to satisfy {(UCP${}_W$)} within XII-F's admissible class.