% !TEX program = pdflatex
%=====================================================================
% IX-D-ST.tex
%
% Self-contained source file for pdfLaTeX.
% Four ordered local stages are retained:
%   I.   IX-D-ST
%   II.  IX-E-ST
%   III. IX-E-2-ST
%   IV.  IX-E-3-ST
%
% The mathematical release is an interface/conditional-bridge release.
% A sharp time-ordered product is NOT constructed.
%
% Suggested build:
%   pdflatex -interaction=nonstopmode -halt-on-error IX-D-ST.tex
%   pdflatex -interaction=nonstopmode -halt-on-error IX-D-ST.tex
%
% No successful compilation or independent execution is asserted.
%=====================================================================

\documentclass[11pt]{article}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools,mathrsfs}
\usepackage{array,booktabs,tabularx,longtable}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage[hidelinks]{hyperref}

\hypersetup{
  pdftitle={IX-D-ST: Causal interfaces and a conditional support bridge},
  pdfauthor={},
  pdfsubject={Supported adaptations of IX-D through IX-E-3}
}

\setlength{\emergencystretch}{3em}
\setlist{itemsep=3pt,topsep=5pt}
\setcounter{tocdepth}{1}
\numberwithin{equation}{section}
\allowdisplaybreaks
\urlstyle{same}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{assumption}[theorem]{Assumption}
\newtheorem{requirement}[theorem]{Requirement}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\RR}{\mathbb R}
\newcommand{\CC}{\mathbb C}
\newcommand{\DD}{\mathcal D}
\newcommand{\EE}{\mathcal E}
\newcommand{\HH}{\mathcal H}
\newcommand{\AA}{\mathcal A}
\newcommand{\Padm}{\mathscr P_\Sigma}
\newcommand{\Pmc}{\mathscr P_{\mathrm{mc}}}
\newcommand{\taus}{\tau_\Sigma}
\newcommand{\Bspace}{\mathscr B}
\newcommand{\Wspace}{\mathscr W}
\newcommand{\Lspace}{\mathscr L}
\newcommand{\Rspace}{\mathscr R}
\newcommand{\Ddecl}{D_{\mathrm{decl}}}
\newcommand{\Dold}{D_{\mathrm{old}}}
\newcommand{\Dfirst}{D_{\mathrm{first}}}
\newcommand{\Dsecond}{D_{\mathrm{second}}}
\newcommand{\Dnew}{D_{\mathrm{new}}}
\newcommand{\Dcmp}{D_{\mathrm{cmp}}}
\newcommand{\Dtwo}{D_2}
\newcommand{\Dthree}{D_3}
\newcommand{\Otwo}{O_2}
\newcommand{\Oact}{O_{\mathrm{act}}}
\newcommand{\Rthree}{\CC[\hbar]/(\hbar^4)}
\newcommand{\Rtwo}{\CC[\hbar]/(\hbar^3)}
\newcommand{\Vthree}{\Padm\otimes_{\CC}\Rthree}
\newcommand{\Vtwo}{\Padm\otimes_{\CC}\Rtwo}
\newcommand{\TO}{\mathsf{TO}_2}
\newcommand{\Ttwo}{\mathsf T_2}
\newcommand{\Tbar}{\overline{\mathsf T}_2}
\newcommand{\Rhat}{\widehat{\mathsf{Ret}}_1}
\newcommand{\Ezero}{\mathsf E_0}
\newcommand{\Eflat}{\mathsf E_{\mathrm{fl}}}
\newcommand{\Ddir}{\mathrm D}
\newcommand{\btrace}{\mathfrak b}
\newcommand{\Bsurf}{\mathcal B}
\newcommand{\dd}{\mathrm d}
\newcommand{\fsupp}{\operatorname{supp}_{\mathrm{fun}}}
\newcommand{\hsupp}{\operatorname{supp}_{h}}
\newcommand{\psupp}{\operatorname{supp}_{\phi}}
\newcommand{\pair}[2]{\left\langle #1,#2\right\rangle}
\newcommand{\norm}[1]{\left\lVert #1\right\rVert}
\newcommand{\abs}[1]{\left\lvert #1\right\rvert}
\newcommand{\ket}[1]{\lvert #1\rangle}
\newcommand{\bra}[1]{\langle #1\rvert}
\newcommand{\kb}[2]{\ket{#1}\bra{#2}}
\newcommand{\proj}[1]{\kb{#1}{#1}}
\newcommand{\loc}[1]{\texttt{\detokenize{#1}}}
\newcommand{\ddia}{d_\diamond}
\newcommand{\dtr}{d_{\mathrm{tr}}}

\DeclareMathOperator{\supp}{supp}
\DeclareMathOperator{\WF}{WF}
\DeclareMathOperator{\Tr}{Tr}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\Span}{span}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\RePart}{Re}
\DeclareMathOperator{\ImPart}{Im}

\newcommand{\scopebox}[2]{%
  \par\medskip\noindent
  \fbox{\begin{minipage}{%
  \dimexpr\linewidth-2\fboxsep-2\fboxrule\relax}
  \textbf{#1}\par\smallskip #2
  \end{minipage}}
  \par\medskip
}

\title{\textbf{IX-D-ST: Causal interfaces and a conditional\\
functional-support bridge on a prescribed cone}\\[5pt]
\large Ordered local Grade S adaptations of\\
IX-D, IX-E, IX-E-2, and IX-E-3}
\author{Ngo Cheung}
\date{}

\begin{document}
\maketitle

\begin{abstract}
We organize the causal-interface programme following the
constructed sharp free partial product as four ordered,
supported stages on the regular part of the prescribed
I-B conical spacetime. The adapted IX-A-ST carrier and the
IX-Free-2 coefficient assignment are explicit inherited
inputs; neither is reinterpreted as time ordering.

The principal analytical result is a complete
common-regulator evaluation of the imaginary part of the
locked mixed kernel. A direct null-cone distribution is
accompanied by a nonzero observation-spacelike contribution
between the direct and reflected cones; the two cosine
tails cancel beyond the reflected cone. Consequently the
commutator vanishes on the entire strongly separated
two-way class, while a nonzero observation-spacelike
control is not, by itself, a causal obstruction.

We prove exact functional support for the quadratic slot
and show that a boundary-trace certificate implies a
null-sphere lower-support theorem for the sharp insertion.
Those spheres suffice for the full retained two-way
commutator bridge; a solid-ball lower-support assertion is
unnecessary and is false in the specified flat realization.
We also prove the scalar non-lift, an actual-tensor
algebraic consistency criterion, conditional causal
subtraction, and the one-order loss under normalization.

The potential usefulness is methodological: the results
separate a genuine fixed-domain obstruction from an
uncertified support inference and identify a precise
operator certificate for the next analytical step.
The underlying algebraic and kernel findings are attributed
to the cited Cheung manuscripts; the present contribution
is their supported conical organization, explicit
hypothesis audit, and finite certificate interface.
Verification of the trace certificate for an otherwise
unspecified inherited adjoint remains open.
No sharp time-ordered product, normalized retarded product,
interacting quantum coefficient, or spacetime-emergence
theorem is constructed.
\end{abstract}

\scopebox{One file, four ordered releases}{%
The requested one-file delivery is followed. The four
parts retain distinct stage boundaries and do not assert
that registry entries have been installed.

``Complete'' means complete proofs of the stated interface,
kernel, algebraic, and conditional support results.
It does not mean a solution of the explicitly retained
time-ordering problem. The final causal-product verdict is
\textbf{Unresolved}. No proof of universal nonexistence is
claimed.}

\tableofcontents

%=====================================================================
\section{Background, attribution, and proof boundary}
\label{sec:background}
%=====================================================================

The programme begins after the construction of one free
partial product, not before it.
IX-D separates that product from causal interfaces;
IX-E formulates the binary extension problem;
IX-E-2 evaluates the missing kernel difference; and
IX-E-3 identifies the functional-support certificate
needed to use that evaluation on all retained two-way
pairs \cite{IXD,IXE,IXE2,IXE3}.

The finite operational background is Enter's separation
between a consumed quantum input name, a classical record,
and an unmeasured residual. Its operational
characterization has its own structural assumptions
\cite{EnterArticle,EnterI}. We adopt finite Born
instruments and prove the complete channel identities
needed here; we do not re-prove that characterization.

The philosophical background is a discipline of
non-identification: destructive readout is not quantum
recovery, a channel is not a thermodynamic machine, and
an operational analogy does not supply a geometric
dictionary \cite{EnterPhil}.
In I-B, geometry, locations, operational permissions,
and clock calibration are supplied separately.
The finite clock is not the geometric time axis
\cite{IB}.

\begin{definition}[Local Grade S in this manuscript]
\label{def:grade}
A local Grade S package consists of:
\begin{enumerate}[label=\textup{(S\arabic*)}]
\item a prescribed host and a supported regular laboratory;
\item mathematical objects with explicit domains and inputs;
\item complete finite channels, including untouched references;
\item one finite destructive-clock factor with stated calibration;
\item computational dependency bounds, distinguished from
physical causal containment;
\item a nonempty regular transport realization with durations
and resource counts.
\end{enumerate}
These clauses do not assert emergence of the metric.
Grade E is not constructed.
\end{definition}

\paragraph{Attribution and novelty.}
The source-level mathematical findings are attributed to
N.~Cheung. No priority claim over
\cite{IXD,IXE,IXE2,IXE3} is made.
The supported adaptation and its hypothesis audit are
different from an independent verification of the whole
source corpus.

\paragraph{Two kinds of missing result.}
Failure to construct a map is not proof that every such
map is impossible. Conversely, a conditional theorem is
a proved implication, not a discharge of its hypothesis.
Both distinctions are maintained in every release below.

%=====================================================================
\section{Shared host contract}
\label{sec:host}
%=====================================================================

Fix \(0<\delta_{\mathrm c}<2\pi\),
\(\alpha=1-\delta_{\mathrm c}/(2\pi)\), and
\(c_{\mathrm{light}}>0\). The prescribed regular host is
\begin{equation}
 M^\circ_{\delta_{\mathrm c}}
 =\RR_T\times C^\circ_{\delta_{\mathrm c}}\times\RR_z,
 \qquad
 g=-c_{\mathrm{light}}^2\dd T^2+
       \dd r^2+\alpha^2r^2\dd\varphi^2+\dd z^2,
 \qquad r>0.
 \label{eq:host}
\end{equation}
Its stipulated completion has defect
\[
 \mathcal W=\RR_T\times\{o\}\times\RR_z.
\]
Thus the defect is a worldsheet.

\begin{proposition}[The regular product is not globally hyperbolic]
\label{prop:nonGH}
The spacetime \eqref{eq:host} has a noncompact causal diamond.
\end{proposition}

\begin{proof}
Choose a regular spatial point of radius \(r_*>0\), and
two events there separated by more than
\(2r_*/c_{\mathrm{light}}\).
At an intermediate time, points on the same radial ray
with radii tending to zero lie in their causal diamond.
They have no convergent subsequence in the regular product.
\end{proof}

Choose a product-adapted developing chart
\[
 \iota:U=(-\epsilon_0,H)\times B_R
                  \longrightarrow M^\circ_{\delta_{\mathrm c}},
 \qquad t=c_{\mathrm{light}}(T-T_\Sigma),
\]
whose closure over the retained laboratory stays off
\(\mathcal W\).
The developed metric is \(-\dd t^2+\dd\mathbf x^2\).
For analytical comparison formulae use
\[
 \eta=\operatorname{diag}(1,-1,-1,-1),
 \qquad P=\partial_t^2-\Delta_{\mathbf x}.
\]
Changing the overall signature convention does not
change the causal relation.

Fix
\[
 V=(0,T_0)\times B_{r_0},\qquad
 R>r_0+T_0,\qquad H>T_0,
\]
and retain the entire compact shadow
\[
 K_*=[0,T_0]\times\overline B_{r_0+T_0}\Subset U.
\]
All observation tests used for the free sector are in
\(\mathcal D(V;\CC)\).
Their complete truncated chart pasts, including their
initial sphere points, lie in the retained laboratory.

\begin{definition}[Chart causal relation]
\label{def:chartcausal}
For developed points in the laboratory,
\[
 (v,\mathbf z)\in J^-_{\mathrm{ch}}(t,\mathbf x)
 \quad\Longleftrightarrow\quad
 v\le t,\quad |\mathbf z-\mathbf x|\le t-v.
\]
Both null boundaries and coincidence are included.
All occurrences of \(J^\pm\) below mean these chart sets.
They are not assertions about all causal curves of the
global conical host.
For a compact observation set \(F\), put
\[
 P_F=J^-_{\mathrm{ch}}(F)\cap\{t\ge0\}.
\]
\end{definition}

Every \(P_F\) used here is compact and retained in \(K_*\).
No finite-propagation assertion crosses the worldsheet.

\begin{assumption}[Supported carrier input]
\label{ass:carrier}
The carrier is IX-A-ST's adapted
\((\Padm,\taus)\), with the following explicitly used
properties \cite{IXAST}.
\begin{enumerate}[label=\textup{(A\arabic*)}]
\item Elements are actual off-shell polynomial functionals
with compact distributional configuration kernels.
Equality means equality on all smooth configurations,
not equality modulo equations of motion.
\item Smooth configurations and compactly supported smooth
variations are unrestricted in the retained chart.
\item Classical pointwise multiplication, conjugation, and
fixed smooth directional differentiation preserve the carrier.
Multiplication by a fixed classical factor is continuous.
\item Every coefficient must satisfy the inherited metric
admission condition
\[
 (\Ddir_{\boldsymbol\eta}F)'_h(\Psi)
       \in\mathscr S_1=\mathscr M_1+\mathscr Q_\Sigma
\]
for every configuration and required finite direction list.
Existence of a distributional pairing alone is not admission.
\item The supplied local response \(L=\Ezero C\) has the
retained support property: a metric variation outside
\(P_F\) cannot change \(Lh\) on \(F\).
The IX-A-ST saturation statement makes its retained
response independent of auxiliary extensions.
No global conical inverse is supplied.
\item The sharp metric adjoint, on its supplied source domain,
retains the actual identity
\begin{equation}
 L^*a=\theta(t)C^*b+
       \delta(t)\Bsurf(b|_\Sigma),
 \qquad b=\Ezero^*a.
 \label{eq:sharpadjoint}
\end{equation}
The source domain and the actual adjoint must be matched
before a formula for \(b|_\Sigma\) is imported.
\item Unchanged regular approximants do not converge:
\[
 B_{f,\varepsilon}\not\longrightarrow B_f
 \quad\text{in }\taus
 \qquad(0\ne f\text{ real}).
\]
\end{enumerate}
The boundary-trace certificate (TC) of Part IV is not
included in this assumption.
\end{assumption}

\begin{remark}[What saturation does not say]
Saturation is a local response-independence statement,
not a global Green-operator theorem.
In a fully specified flat zero-Cauchy realization, an
adjoint trace can be proved by transposition. Part IV
does this for that realization.
The weak inherited interface above does not silently
identify its complete adjoint source domain with that
realization.
Global Green-operator results require their own
hypotheses \cite{BGP}.
\end{remark}

\begin{proposition}[Description changes do not evolve the host]
\label{prop:fixedhost}
Changing the parent parameter, regulator description,
stage tag, or a proposed time-ordering token leaves
\eqref{eq:host}, \(\Sigma\), and \(\mathcal W\) unchanged.
\end{proposition}

\begin{proof}
They are description-register entries. No metric update
is in the command's output type.
\end{proof}

%=====================================================================
\section{Inherited free sector and locked comparison kernel}
\label{sec:free}
%=====================================================================

Configurations are \(\Psi=(h,\phi)\). Set
\begin{equation}
 B_f[h,\phi]=-\int f(x)(Lh)^\mu(x)
                         \partial_\mu\phi(x)\,\dd^4x,
 \qquad
 W_g[h]=\int g(y)h_{00}(y)^2\,\dd^4y.
 \label{eq:generators}
\end{equation}
Pairings are complex linear in their tests.

Use \(x=(t,\mathbf x)\), \(y=(s,\mathbf y)\),
\(x'=(t',\mathbf x')\), and
\[
 \tau=t-s,\qquad u=t+s,\qquad
 \mathbf z=\mathbf x-\mathbf y,\qquad R=|\mathbf z|.
\]
The locked mixed comparison kernel is
\begin{equation}
 \begin{split}
 K(x,y)=\int_{\RR^3}\frac{\dd^3p}{(2\pi)^3}
 e^{ip\cdot(\mathbf x-\mathbf y)}
 \left[
 \left(-\frac{t}{4|p|}+\frac{i}{8|p|^2}\right)
                              e^{-i|p|(t-s)}
 -\frac{i}{8|p|^2}e^{i|p|(t+s)}
 \right].
 \end{split}
 \label{eq:K}
\end{equation}
It is a chart comparison formula, not a covariance
derived from the conical host.

The first stages are locked as
\begin{align}
 B_f\star_cW_g&=B_fW_g+\hbar Q_{f,g},
 &Q_{f,g}
   &=-2\pair{fgK}{\partial_t\phi(x)h_{00}(y)},\nonumber\\
 W_g\star_cB_f&=W_gB_f+\hbar Q^R_{g,f},
 &Q^R_{g,f}
   &=-2\pair{fg\overline K}{\partial_t\phi(x)h_{00}(y)}.
 \label{eq:firststages}
\end{align}
The minus sign and the factor \(2\) are fixed.

For later support bookkeeping write
\[
 w=Lh,\qquad
 S_{\mu\nu}(x,x')
   =\partial_{x^\mu}\partial_{x'^\nu}
                         \Delta_m^+(x-x'),
\]
\[
 T_{f,f'}=
   \pair{f(x)f'(x')S_{\mu\nu}(x,x')}
                         {w^\mu(x)w^\nu(x')}.
\]
Define
\[
 G_{12}=Q_{f,g}B_{f'},\quad
 G_{23}=B_fQ^R_{g,f'},\quad
 G_{13}=T_{f,f'}W_g.
\]
The inherited two-edge values have residual forms
\begin{align}
 G_{12,23}
 &=2\pair{f(x)g(y)f'(x')K(x,y)\overline{K(x',y)}}
             {\partial_t\phi(x)\partial_{t'}\phi(x')},
 \nonumber\\
 G_{12,13}
 &=2\pair{f(x)g(y)f'(x')K(x,y)S_{0\nu}(x,x')}
                                  {h_{00}(y)w^\nu(x')},
 \label{eq:trees}\\
 G_{13,23}
 &=2\pair{f(x)g(y)f'(x')S_{\mu0}(x,x')
                              \overline{K(x',y)}}
                                  {w^\mu(x)h_{00}(y)}.
 \nonumber
\end{align}

\begin{assumption}[Constructed free partial product]
\label{ass:free2}
The IX-Free-2 record, or the supported IX-C-ST predecessor
when accepted with its stated inputs, supplies
\cite{IXFreeTwo,IXCST}:
\begin{enumerate}[label=\textup{(F\arabic*)}]
\item The displayed free coefficients exist in \(\Padm\),
including required directional descendants.
\item With
\[
 \Bspace=\{B_f\},\quad \Wspace=\{W_g\},\quad
 \Lspace=\Span\{B_fW_g,Q_{f,g}\},\quad
 \Rspace=\Span\{W_gB_f,Q^R_{g,f}\},
\]
the actual algebraic tensor domains are
\[
 \Dfirst=(\Bspace\otimes\Wspace)+(\Wspace\otimes\Bspace),
\]
\[
 \Dsecond=(\Lspace\otimes\Bspace)+(\Bspace\otimes\Rspace),
 \quad
 \Dnew=\Dfirst+\Dsecond,
\]
\[
 \Dold=\Pmc\otimes\Pmc,\qquad
 \Ddecl=\Dnew+\Dold,\qquad
 \Dnew\cap\Dold=0.
\]
The old free coefficients are unchanged.
\item There is one linear coefficient assignment
\[
 S=\star_c:\Ddecl\longrightarrow\Vthree.
\]
It is extended linearly to formal tensors. No arbitrary
intermediate closure is supplied.
\item Both degree-two presentation maps and both degree-four
presentation maps are injective. In particular,
\(Q^R_{g,f}\ne0\) for nonzero \(g\otimes f\).
\item For one common real parent \(c\),
\begin{equation}
 \begin{split}
 A_c(f,g,f')={}&
 (B_f\star_cW_g)\star_cB_{f'}
 =B_f\star_c(W_g\star_cB_{f'})\\
 ={}&B_fW_gB_{f'}
  +\hbar(G_{12}+G_{13}+G_{23})\\
 &+\hbar^2(G_{12,23}+G_{12,13}+G_{13,23})
  +\hbar^3\mathcal N_c(f,g,f')1
                         \pmod{\hbar^4}.
 \end{split}
 \label{eq:word}
\end{equation}
\item If \(\sigma(F\otimes G)=G\otimes F\) and
\(\gamma(F\otimes G)=F^*\otimes G^*\), then
\[
 d^\dagger=\sigma\gamma d,\qquad
 \Ddecl^\dagger=\Ddecl,\qquad
 S(d)^*=S(d^\dagger).
\]
Conjugation fixes formal \(\hbar\).
\item Fixed-support continuity holds on the named generating
families, denoted F9a. Actual-stage continuity F9b and
quantum hypocontinuity are not supplied.
\end{enumerate}
\end{assumption}

No conclusion below reopens degree-four free descent.

\begin{assumption}[Parent calibration, not re-proved]
\label{ass:parent}
The scalar in \eqref{eq:word} is
\[
 \mathcal N_c(f,g,f')
   =\pair{U_c}{f\otimes g\otimes f'},\qquad
 U_c=u_\mu^\rho+cr,
\]
with the source-locked VII-D/IX-B normalization
\[
 u_\mu^\rho=U_m+(\kappa_\rho+\log\mu)r.
\]
Its supplied strong numerical estimate is
\[
 \left|\pair{
 T_\varepsilon^\rho-\log((\mu\varepsilon)^{-1})r-u_\mu^\rho
 }{\Phi}\right|
 \le C_A\varepsilon(1+|\log\varepsilon|)p_{A,64}(\Phi)
\]
on arbitrary joint tests in a fixed retained compact set.
The parent conversion class is \(\RR r\), not an evaluated
binary time-ordering ambiguity class
\cite{VIID,IXB}.
\end{assumption}

The numerical facts
\(\mathcal C_{\mathrm{desc}}=
 \mathcal C_{\mathrm{glue}}=\RR\)
are inherited free-sector facts. They impose no causal
normalization and do not run the host curvature.

%=====================================================================
\part{IX-D-ST: causal interfaces after the free product}
%=====================================================================

\section{Functional support and separate causal interfaces}
\label{sec:interfaces}
%=====================================================================

\begin{definition}[Functional support and ordering]
\label{def:fsupp}
A point belongs to \(\fsupp F\) if every neighbourhood
admits a compactly supported smooth perturbation that
changes \(F\) at some smooth configuration.
For formal polynomials, support means the union of the
supports of their finitely many coefficients.
Species supports \(\hsupp F,\psupp F\) use only the
corresponding variations.

Define
\begin{equation}
 F\gtrsim G
 \quad\Longleftrightarrow\quad
 \fsupp F\cap J^-_{\mathrm{ch}}(\fsupp G)=\varnothing.
 \label{eq:ordering}
\end{equation}
\end{definition}

\begin{lemma}[Derivative characterization]
\label{lem:derivativesupport}
On the unrestricted affine configuration space,
\(\fsupp F\) is the closure of the union of the supports
of all first functional derivatives, over all smooth
configurations and species.
\end{lemma}

\begin{proof}
If every derivative vanishes on perturbations in an open
set, integration along
\(\Psi+\lambda k\), \(0\le\lambda\le1\), shows that every
such perturbation leaves \(F\) unchanged.
Conversely, if a derivative pairs nontrivially with a
variation, the directional function has nonzero derivative
and is not locally constant.
Taking all configurations, local variations, and closures
gives the assertion.
\end{proof}

\begin{lemma}[A comparison domain for both free orderings]
\label{lem:comparison}
The domain
\[
 \Dcmp=\Ddecl\cap\sigma(\Ddecl)
\]
is stable under \(\sigma,\gamma,\dagger\).
It contains \(\Dfirst\).
\end{lemma}

\begin{proof}
Flip stability is immediate. Dagger stability of
\(\Ddecl\) gives
\(\gamma(\Ddecl)=\sigma(\Ddecl)\).
Thus
\[
 \gamma(\Dcmp)
  =\sigma(\Ddecl)\cap\Ddecl=\Dcmp.
\]
The first-stage domain contains both orderings, so is
contained in \(\Dcmp\).
\end{proof}

\begin{requirement}[Time-ordered interface
\(\mathcal I_{\mathrm{TO}}\)]
\label{req:TO}
A proposed bosonic causal construction must provide:
\begin{enumerate}[label=\textup{(TO\arabic*)}]
\item actual tensor domains \(\Dtwo\), and any required
\(\Dthree\), with all necessary flips, conjugates, and
intermediate domains specified;
\item a symmetric linear map
\[
 \Ttwo:\Dtwo\longrightarrow\Vthree,
 \qquad T_0(F,G)=FG,\qquad T_1^{\mathrm{arity}}(F)=F;
\]
the last normalization concerns arity one, not
\(\hbar\)-order one;
\item admitted coefficients and all required descendants,
with actual-presentation independence;
\item causal factorization on every retained comparison pair:
\[
 \Ttwo(F,G)=S(F\otimes G)\quad\text{if }F\gtrsim G;
\]
\item exact values on every separately supplied old
time-ordered overlap, and a specified admissible
contact class;
\item anti-time ordering and involution:
\begin{equation}
 \Tbar(d)=S(d)+S(\sigma d)-\Ttwo(d),
 \qquad
 \Ttwo(d)^*=\Tbar(\gamma d);
 \label{eq:antitime}
\end{equation}
\item a continuity theorem on named domains at a specified
strength.
\end{enumerate}
Outside \(\Dcmp\), every additional free comparator must
be independently constructed.
Higher causal factorization must name every product it uses.
\end{requirement}

In particular, symmetry does not mean
\(\Ttwo(F,G)^*=\Ttwo(F^*,G^*)\).
The anti-time-ordered map in \eqref{eq:antitime} is essential.

\begin{requirement}[Retarded interface
\(\mathcal I_{\mathrm{ret}}\)]
\label{req:ret}
A retarded construction must specify its actual argument
domain, normalization convention, admitted coefficients
and descendants, old retarded overlaps, and a named
continuity statement.

For independently unsmeared source or observation slots,
a distributional retarded-support assertion additionally
requires a specified multilinear distribution and a proof
of its support in the declared causal relation.
Vanishing for one functional-support ordering is not
that slot-support theorem.

A second retarded order requires higher time ordering
and all intermediate products in its defining identity.
None is supplied by writing an arity-two subtraction.
\end{requirement}

\begin{theorem}[The free release does not supply either causal interface]
\label{thm:interfaces}
Assumption~\ref{ass:free2} supplies neither a system satisfying
\(\mathcal I_{\mathrm{TO}}\) nor one satisfying
\(\mathcal I_{\mathrm{ret}}\).
In particular, \eqref{eq:word} is not causal factorization.
\end{theorem}

\begin{proof}
The free assignment has a specified free tensor domain
and coefficient values. The time-ordered maps,
ordered restrictions, anti-time-ordering equations,
old time-ordered overlaps, and retarded slot
distributions in the requirements are additional objects.
They are not among its outputs.
The explicit nonimplication witness in
Lemma~\ref{lem:separation} below shows that even adjoining
a symmetric admitted auxiliary multiplication does not
supply the missing causal axiom.
\end{proof}

%=====================================================================
\section{Laboratory-local support of the inherited outputs}
\label{sec:support}
%=====================================================================

\begin{theorem}[Configuration-support inclusions]
\label{thm:support}
Let \(F=\supp f\), \(G=\supp g\), and \(F'=\supp f'\).
The inherited outputs have the following bounds:
\begin{center}
\small
\renewcommand{\arraystretch}{1.15}
\begin{tabularx}{\linewidth}{@{}p{.24\linewidth}XX@{}}
\toprule
Functional & Metric support bound & Scalar support bound\\
\midrule
\(B_f\) & \(P_F\) & \(F\)\\
\(W_g\) & \(G\) & \(\varnothing\)\\
\(Q_{f,g}\) & \(G\) & \(F\)\\
\(Q^R_{g,f'}\) & \(G\) & \(F'\)\\
\(T_{f,f'}\) & \(P_F\cup P_{F'}\) & \(\varnothing\)\\
\(G_{12}\) & \(G\cup P_{F'}\) & \(F\cup F'\)\\
\(G_{23}\) & \(P_F\cup G\) & \(F\cup F'\)\\
\(G_{13}\) & \(P_F\cup P_{F'}\cup G\) & \(\varnothing\)\\
\(G_{12,23}\) & \(\varnothing\) & \(F\cup F'\)\\
\(G_{12,13}\) & \(G\cup P_{F'}\) & \(\varnothing\)\\
\(G_{13,23}\) & \(P_F\cup G\) & \(\varnothing\)\\
\(B_fW_gB_{f'}\) & \(P_F\cup G\cup P_{F'}\) & \(F\cup F'\)\\
\(\mathcal N_c(f,g,f')1\) & \(\varnothing\) & \(\varnothing\)\\
\bottomrule
\end{tabularx}
\end{center}
All inclusions are relative to the supported laboratory.
\end{theorem}

\begin{proof}
The supplied response-support property gives the metric
bound for \(B_f\); its scalar slot is integrated only on
\(F\). The assertion for \(W_g\) is immediate.

The kernels in the displayed free outputs are fixed
comparison distributions, not varying configurations.
Only their residual fields contribute configuration
dependence. Each residual \(w\)-slot on an observation
set contributes its corresponding \(P_F\); each local
\(h_{00}\)-slot contributes \(G\); each scalar derivative
slot contributes its observation support.
A classical product depends only on the union of its
factors' dependence sets.
These observations prove every row directly.
\end{proof}

These are the supported versions of IX-D's support ledger
\cite[{\loc{thm:support}}]{IXD}.
They do not assert support of an unconstructed retarded
argument-slot distribution.

%=====================================================================
\section{Scalar non-lift and an explicit causal separation}
\label{sec:nonlift}
%=====================================================================

Let \(\operatorname{ev}_0F=F[0,0]\), coefficientwise.
Define
\[
 \Pi_{3,0}(A)=[\hbar^3]\operatorname{ev}_0A.
\]

\begin{theorem}[The calibrated scalar is a projection, not a lift]
\label{thm:nonlift}
The constructed free word satisfies
\[
 \operatorname{ev}_0 A_c
       =\hbar^3\mathcal N_c(f,g,f')1,\qquad
 \Pi_{3,0}A_c=\mathcal N_c(f,g,f').
\]
Neither projection defines \(\TO\), \(\Ttwo\),
\(\mathsf{Ret}_1\), or a higher retarded map.
\end{theorem}

\begin{proof}
Every nonconstant term in \eqref{eq:word} has positive
field degree and vanishes at zero configuration.
The displayed identities follow.

The projection has a large kernel:
\(\Pi_{3,0}(\hbar F)=0\) for every \(\hbar\)-independent
\(F\), and
\(\operatorname{ev}_0(\hbar^jF)=0\) whenever \(F[0,0]=0\).
It loses nonconstant coefficient information and has
no supplied rule assigning missing binary coefficients,
ordered restrictions, or old causal overlaps.
A change in a nonconstant coefficient may leave the
projection unchanged. This is information loss, not
permission to change any locked free coefficient.
\end{proof}

\begin{lemma}[Free coherence does not imply causal factorization]
\label{lem:separation}
The inherited free coherence is compatible with the
symmetric, admitted auxiliary map \(M_2(F,G)=FG\),
although that map fails causal factorization on a
retained ordered first-stage pair.
\end{lemma}

\begin{proof}
Choose nonzero tests with
\[
 \supp f\subset\{0<t<a\},\qquad
 \supp g\subset\{t>b\},\qquad b>a.
\]
The support bounds imply \(W_g\gtrsim B_f\).
Both free orderings belong to the first-stage domain.

Classical closure makes \(M_2\) admitted and symmetric.
It changes none of the inherited free data.
But
\[
 S(W_g\otimes B_f)=W_gB_f+\hbar Q^R_{g,f},
 \qquad Q^R_{g,f}\ne0
\]
by the inherited injective presentation map.
Thus \(M_2(W_g,B_f)\ne S(W_g\otimes B_f)\).
\end{proof}

The slabs prove the displayed ordering, not necessarily
its uniqueness: different time slabs may still be
spacelike separated.
The lemma excludes the classical candidate, not every
causal extension.

%=====================================================================
\section{Conditional source contacts, subtraction, and order audit}
\label{sec:conditional}
%=====================================================================

\begin{assumption}[Simultaneous source prescription]
\label{ass:source}
For this subsection only, let \(P_{\mathrm f}\) be a
specified formally self-adjoint field operator and
\(H_{\mathrm F}\) a specified fundamental solution with
\[
 (P_{\mathrm f})_xH_{\mathrm F}
                    =c_{\mathrm F}\delta,\qquad c_{\mathrm F}\ne0.
\]
The actual source presentation is \(j=P_{\mathrm f}h\).
Differential compatibility requires
\(H^{\mathrm{TO}}_{jh}=(P_{\mathrm f})_xH_{\mathrm F}\).
The declared test domain detects the diagonal contact.
\end{assumption}

\begin{proposition}[Conditional source-contact incompatibility]
\label{prop:contact}
Under Assumption~\ref{ass:source}, the additional prescription
\(H^{\mathrm{TO}}_{jh}=0\) is inconsistent.
\end{proposition}

\begin{proof}
Compatibility forces \(H^{\mathrm{TO}}_{jh}
=c_{\mathrm F}\delta\).
A nonzero real compact test \(q\) gives
\[
 \pair{c_{\mathrm F}\delta}{q\otimes q}
       =c_{\mathrm F}\int q^2\ne0.
\]
For a bundle-valued identity select a nonzero diagonal
component and matching bundle tests.
\end{proof}

The statement excludes only those simultaneous assumptions.
An independent central source need not be identified with
\(P_{\mathrm f}h\). A free bisolution equation
\(P_{\mathrm f}H=0\) is a different input.
The two-slot contact is not the three-observation residue
\(r\), and cannot be absorbed merely by changing \(c\)
\cite[{\loc{prop:contact}}]{IXD}.

\begin{assumption}[Future time-ordered lift]
\label{ass:future}
For the implication below only, suppose:
\begin{enumerate}[label=\textup{(T\arabic*)}]
\item a symmetric actual map
\(\Ttwo:\Dtwo\to\Vthree\) is constructed, with
\(\sigma,\gamma\)-stable comparison domain
\(E_2=\Dtwo\cap\Dcmp\);
\item all its coefficients and required descendants are
admitted, and actual-presentation descent holds;
\item its classical coefficient is multiplication, and
\(\Ttwo(F,G)=S(F\otimes G)\) whenever \(F\gtrsim G\);
\item \eqref{eq:antitime} holds;
\item all claimed old time-ordered and retarded overlaps
are supplied and agree exactly, with old unnormalized
retarded convention \(i(\Ttwo-S)\);
\item any claimed continuity is proved on the same named
comparison interfaces.
\end{enumerate}
None of these new time-ordering hypotheses is discharged
by this assumption's declaration.
\end{assumption}

\begin{theorem}[Conditional unnormalized causal subtraction]
\label{thm:conditionalret}
Under Assumption~\ref{ass:future},
\[
 \Rhat(d)=i\bigl(\Ttwo(d)-S(d)\bigr),\qquad d\in E_2,
 \label{eq:Rhat}
\]
has admitted coefficients and descendants, zero classical
coefficient, and exact supplied old unnormalized overlaps.
It satisfies
\[
 \Rhat(V,O)=0
 \quad\text{if}\quad
 \fsupp O\cap J^+_{\mathrm{ch}}(\fsupp V)=\varnothing,
\]
and
\[
 \Rhat(d)^*=\Rhat(\gamma d).
\]
A common named fixed-support continuity property passes
to this difference.
\end{theorem}

\begin{proof}
Admission, descendant admission, and old overlap follow
by linear subtraction. The order-zero coefficients cancel.

The support condition is \(V\gtrsim O\), so factorization
makes the two terms equal.
For involution use free reversal and \eqref{eq:antitime}:
\[
\begin{split}
 \Rhat(d)^*
 &=-i\bigl(\Ttwo(d)^*-S(d)^*\bigr)\\
 &=-i\bigl(S(\gamma d)+S(\sigma\gamma d)
                -\Ttwo(\gamma d)-S(\sigma\gamma d)\bigr)\\
 &=i\bigl(\Ttwo(\gamma d)-S(\gamma d)\bigr).
\end{split}
\]
Continuity follows from continuity of addition and scalar
multiplication in the named locally convex range.
\end{proof}

The vanishing is an ordered-functional-pair assertion,
not an independently unsmeared slot-support theorem.

\begin{lemma}[One-order loss]
\label{lem:hbaraudit}
There is a well-defined coefficient shift
\[
 \mathcal L:\hbar\Vthree\longrightarrow\Vtwo,\qquad
 \mathcal L(\hbar A_1+\hbar^2A_2+\hbar^3A_3)
                =A_1+\hbar A_2+\hbar^2A_3.
\]
Numerator data through order \(\hbar^3\) determine a
normalized quotient only through order \(\hbar^2\).
\end{lemma}

\begin{proof}
The coefficient expansion gives the shift uniquely.
In \(\Vthree\), multiplication by \(\hbar\) annihilates
every \(\hbar^3C\). Hence that final coefficient of a
putative quotient is undetermined.
Equivalently, \(\hbar\) is not invertible in \(\Rthree\).
\end{proof}

Since \(\Ttwo\) is not constructed, no normalized
\(R_1=\mathcal L(\Rhat)\) is released, even at the
lower determined order. Neither \(R_2\) nor
\(\mathsf T_3\) is defined.

\begin{proposition}[The switch witness is a separate gate]
\label{prop:switch}
Retain the copied first-order witness, on its original
hypotheses,
\[
 B_f[h+\mathsf K\xi,\phi]-B_f[h,\phi]
     =-\int f\,X_\xi\phi\ne0,\qquad g\,\mathsf K\xi=0.
\]
In a coupling expansion, a correction beginning at
\(\kappa^2\) cannot cancel this nonzero order-\(\kappa\)
variation.
\end{proposition}

\begin{proof}
The order-\(\kappa\) coefficient of a correction divisible
by \(\kappa^2\) is zero. The copied nonzero coefficient
therefore remains unchanged.
\end{proof}

This preserves the witness conditionally; it does not
construct its switched successor, a new gauge action,
or G2.

\begin{theorem}[IX-D-ST stage release]
\label{thm:Drelease}
Part I proves the causal-interface specification,
laboratory-local configuration-support bounds, scalar
non-lift, free/causal separation, conditional source-contact
incompatibility, conditional subtraction, and normalization
audit.

The sharp causal-product release remains
\textbf{Unresolved}. No sharp \(\TO\), \(\Ttwo\),
normalized \(R_1\), or \(R_2\) is constructed.
\end{theorem}

\begin{proof}
The preceding results establish the stated claims.
The future time-ordered hypotheses have not been supplied
as a construction, so the subtraction implication cannot
be instantiated as an unconditional causal product.
\end{proof}

%=====================================================================
\part{IX-E-ST: binary consistency on a fixed actual domain}
%=====================================================================

\section{Domain, ordering geometry, and the commutator}
\label{sec:Egeometry}
%=====================================================================

No nonzero old time-ordered seed is supplied by the input.
Set
\[
 \Otwo=\{0\},
 \qquad
 \Dtwo=
 \Span_\CC\{\sigma^a\gamma^bd:
      d\in\Dfirst+\Otwo,\ a,b\in\{0,1\}\}.
 \label{eq:Dtwo}
\]
This target retains every first-stage tensor, its flip,
and its conjugates.

\begin{proposition}[Domain stability]
\label{prop:domain}
The domain \eqref{eq:Dtwo} is contained in \(\Dcmp\) and
is stable under \(\sigma,\gamma,\dagger\).
An old time-ordered map on a nonzero comparison space is
not supplied by declaring \(\Otwo=0\).
\end{proposition}

\begin{proof}
Lemma~\ref{lem:comparison} puts every generator in
\(\Dcmp\). The involutions permute the generators and
preserve their complex span. The zero seed defines only
the zero map on the zero space.
\end{proof}

Write
\[
 \Oact=\Dtwo\cap\Dold.
\]
No old time-ordered value is inferred merely from the
existence of the old free product. Under additional
conjugation-stability information the intersection may
be evaluated, but that requires its own proof.
No retained tensor is deleted after a failed test.

\begin{proposition}[Double ordering]
\label{prop:geometry}
Both \(F\gtrsim G\) and \(G\gtrsim F\) hold exactly when
their actual functional supports have no causally related
pair in either direction. In particular those supports
are disjoint, with neither null relation nor coincidence.
\end{proposition}

\begin{proof}
The two equations respectively exclude
\(a\in J^-(b)\) and \(b\in J^-(a)\) for support points.
Reflexivity excludes coincidence.
\end{proof}

A null-related support pair is outside at least one
ordered region. A limit from ordered pairs does not
define its missing value without a separately proved
topology and extension.

\begin{lemma}[A strongly separated comparison class]
\label{lem:spacelike}
Suppose \(f,g\) have times in \([0,T]\) and spatial
supports in \(B(\mathbf x_0,r)\) and
\(B(\mathbf y_0,s_0)\). If
\begin{equation}
 |\mathbf x_0-\mathbf y_0|>2T+r+s_0,
 \label{eq:strong}
\end{equation}
and all retained shadows fit in the laboratory, then
both actual orderings hold.
\end{lemma}

\begin{proof}
A point of \(P_F\cup F\) has time in \([0,T]\) and
spatial distance at most \(T+r\) from \(\mathbf x_0\).
Its distance from any point of \(G\) is therefore
greater than \(T\), while their time difference is
at most \(T\). The upper support sets are strictly
spacelike, and actual supports are their subsets.
\end{proof}

This constructs chart comparison regions, not a Lorentz
cone from operational data.

\begin{proposition}[Locked first-stage commutator]
\label{prop:commutator}
On the first-stage sector,
\begin{equation}
\begin{split}
 B_f\star_cW_g-W_g\star_cB_f
   &=\hbar\mathcal C_{f,g},\\
 \mathcal C_{f,g}
   &=-2\pair{fg(K-\overline K)}
                    {\partial_t\phi(x)h_{00}(y)}\\
   &=-4i\pair{fg\,\ImPart K}
                    {\partial_t\phi(x)h_{00}(y)}.
\end{split}
\label{eq:commutator}
\end{equation}
\end{proposition}

\begin{proof}
Subtract \eqref{eq:firststages}.
Their classical terms coincide.
Only smooth configuration factors are reordered.
Distributional linearity and
\(K-\overline K=2i\ImPart K\) give the result.
\end{proof}

Neither full support of \(K\) nor injectivity of either
presentation map computes this difference. A real
distribution may have full support.

\begin{lemma}[Compact detection]
\label{lem:detection}
If \(fg(K-\overline K)\) is a nonzero compact distribution
in the interior observation chart, then
\(\mathcal C_{f,g}\ne0\) as an actual functional.
\end{lemma}

\begin{proof}
Density of finite sums of product tests gives smooth
compact \(a(x),b(y)\) with a nonzero pairing.
Choose a smooth scalar with
\[
 \partial_t\phi(t,\mathbf x)=a(t,\mathbf x),
 \qquad
 \phi(t,\mathbf x)=\int_{t_*}^ta(v,\mathbf x)\,\dd v,
\]
and choose \(h_{00}=b\), all other components zero.
These are allowed off-shell configurations.
For real-only configurations, real and imaginary
decomposition supplies a real detecting pair.
\end{proof}

\begin{theorem}[Fixed-domain obstruction]
\label{thm:obstruction}
If a retained pair satisfies both actual orderings and
\(\mathcal C_{f,g}\ne0\), no symmetric causally factorizing
map \(\Ttwo\) exists on the fixed \(\Dtwo\).
\end{theorem}

\begin{proof}
Factorization and symmetry would force
\[
 B_f\star_cW_g
 =\Ttwo(B_f,W_g)
 =\Ttwo(W_g,B_f)
 =W_g\star_cB_f,
\]
contradicting the nonzero order-\(\hbar\) coefficient.
Higher orders or a contact added to the proposed
time-ordered value cannot satisfy two unequal prescribed
equalities.
\end{proof}

The quantifier covers every extension on this fixed
domain that retains the specified free values.
Without a certified nonzero two-way pair, it is a
conditional obstruction criterion, not an evaluated
no-go theorem \cite{IXE}.

%=====================================================================
\section{Actual-relation consistency and analytical obligations}
\label{sec:algebraic}
%=====================================================================

On \(\Dtwo\), both free orders exist. Define
\[
 A(d)=\frac12\bigl(S(d)+S(\sigma d)\bigr).
\]
It has classical coefficient multiplication and obeys
\[
 A(\sigma d)=A(d),\qquad A(\gamma d)=A(d)^*.
\]

Let \((d_i,t_i)\), \(i\in I\), be all forced ordered values
and any separately supplied old time-ordered values.
Set
\[
 x_i=t_i-A(d_i)\in\hbar\Vthree,\qquad
 Q=\Dtwo/\operatorname{im}(\id-\sigma).
\]
The index set need not be finite.

\begin{theorem}[Algebraic extension criterion]
\label{thm:algebraic}
A complex-linear map on \(\Dtwo\) satisfying the prescribed
values, symmetry, classical multiplication, and
\eqref{eq:antitime} exists algebraically if and only if,
for every finite relation,
\begin{equation}
 \sum_i a_i[d_i]+\sum_i b_i[\gamma d_i]=0
 \quad\Longrightarrow\quad
 \sum_i a_ix_i-\sum_i b_ix_i^*=0.
 \label{eq:relationtest}
\end{equation}
This conclusion includes no sharp distributional
construction or continuity theorem.
\end{theorem}

\begin{proof}
Write \(\Ttwo=A+X\).
Symmetry requires \(X\) to descend to \(Q\);
\eqref{eq:antitime} requires
\(X(\gamma q)=-X(q)^*\).
Thus its forced values are
\(X([d_i])=x_i\) and
\(X([\gamma d_i])=-x_i^*\), giving necessity.

Conversely, \eqref{eq:relationtest} defines such a map
on the conjugation-stable span of these classes.
Multiplying its range by \(i\) makes it
conjugation-equivariant.
Extend the resulting real-linear map from the real
fixed-point subspace to a real complement in \(Q\),
then complexify and multiply by \(-i\).
Pull back to \(\Dtwo\) and add \(A\).
The extension takes values in \(\hbar\Vthree\), so
does not change the classical coefficient.
All values are finite linear combinations of admitted
elements. No continuity of the chosen complement is implied.
\end{proof}

This is the actual-tensor criterion of IX-E
\cite[{\loc{thm:algebraic}}]{IXE}.
It tests finite relations among any number of prescribed
tensors, not only pairwise double-ordering consistency.

\begin{requirement}[Analytical completion of the binary target]
\label{req:analytic}
A construction realizing the criterion analytically must
add all of the following:
\begin{enumerate}[label=\textup{(E\arabic*)}]
\item Complete consistency of forced ordered values and
all actual tensor relations.
\item Exact proposed replacement kernels, their source
and differentiation conventions, ordered restrictions,
singular sets, and residual configuration functionals.
\item Distributional existence, compact configuration
kernels, carrier admission, and every required
directional descendant.
\item A specified admissible contact family and simultaneous
solution of ordered-restriction, old-overlap, admission,
symmetry, and anti-time-ordering equations.
\item A named continuity theorem. One possible weak target
uses seminorms
\[
 F\longmapsto
 |\Ddir_{\eta_1}\cdots\Ddir_{\eta_r}F(\Psi)|
\]
on fixed-support generating families.
This is not actual-stage hypocontinuity.
\end{enumerate}
\end{requirement}

Observation-time ordering alone is insufficient for
\eqref{req:analytic}: the sharp insertion has nonlocal
configuration dependence. One cannot silently commute
time ordering with differentiation, the Cauchy response,
or its sharp adjoint.

The regular-functional time-ordering formula and a
renormalized singular extension are different operations
\cite{FR}. Extension principles require proved hypotheses
at the actual extension locus \cite{BF}.
Those references are documentary comparisons here, not
existence theorems for this sharp sector.
No scaling degree or ambiguity class for its unresolved
binary extension is evaluated.

\begin{theorem}[Conditional binary subtraction]
\label{thm:subtraction}
If Requirement~\ref{req:analytic} and the stated
time-ordering identities are discharged on \(\Dtwo\),
Theorem~\ref{thm:conditionalret} gives an unnormalized
binary retarded difference through \(\hbar^3\).
Its normalized coefficient shift is determined only
through \(\hbar^2\).
\end{theorem}

\begin{proof}
Apply Theorem~\ref{thm:conditionalret} on the fixed
comparison domain and then Lemma~\ref{lem:hbaraudit}.
\end{proof}

\begin{theorem}[IX-E-ST stage release]
\label{thm:Erelease}
Part II proves the double-ordering geometry, a nonempty
strong-separation criterion, the commutator identity,
fixed-domain obstruction criterion, and algebraic
extension criterion.
Its subtraction theorem is conditional.

At this stage the necessary restriction of
\(K-\overline K\) has not been evaluated on the intended
two-way sector, no nonzero old time-ordered map is
supplied, and no sharp analytical extension is
constructed. The release is \textbf{Unresolved},
not a universal obstruction.
\end{theorem}

\begin{proof}
The positive statements are proved above.
Neither an analytical candidate nor a certified
violating two-way pair has been produced in Part II.
These are distinct missing discharges.
\end{proof}

%=====================================================================
\part{IX-E-2-ST: exact imaginary part and witness-class vanishing}
%=====================================================================

\section{Common-regulator evaluation}
\label{sec:imaginary}
%=====================================================================

Introduce one Abel parameter \(\epsilon>0\), multiplying
every momentum term in \eqref{eq:K} by
\(e^{-\epsilon|p|}\).
This represents the existing kernel. It is not the
VII-C smoothing profile and does not define a new product.

\begin{lemma}[Fourier existence]
\label{lem:Fourier}
The locked formula defines a tempered distribution in
\((t,s,\mathbf z)\), smooth in \(t,s\) with values in
\(\mathcal S'(\RR^3)\).
The common-Abel family converges to it distributionally.
\end{lemma}

\begin{proof}
After spatial Fourier transformation of a joint test,
the multiplier is bounded on compact time sets by
\(C(|p|^{-1}+|p|^{-2})\).
Both powers are locally integrable with three-dimensional
momentum measure. At infinity the transformed test is
rapidly decreasing. Dominated convergence proves the
pairing and the Abel limit.
Temporal derivatives introduce only polynomial factors
in momenta and times, handled by the same estimates.
Temporal Schwartz weights absorb the explicit factor
\(t\), giving temperedness.
\end{proof}

Define
\[
 D(v,\mathbf z)=
   \int\frac{\dd^3p}{(2\pi)^3}
       e^{ip\cdot\mathbf z}\frac{\sin(|p|v)}{|p|},
 \qquad
 H(v,\mathbf z)=
   \int\frac{\dd^3p}{(2\pi)^3}
       e^{ip\cdot\mathbf z}\frac{\cos(|p|v)}{|p|^2}.
\]
Both have the same common-Abel interpretation.
The changes \(v=t-s\) and \(v=t+s\) are submersion
pullbacks, equivalently tensor products followed by
invertible linear coordinate changes.

\begin{proposition}[Exact direct-plus-reflected subtraction]
\label{prop:subtractionkernel}
One has
\begin{equation}
 K-\overline K
 =\frac{it}{2}D(\tau,\mathbf z)
     +\frac{i}{4}\bigl(H(\tau,\mathbf z)-H(u,\mathbf z)\bigr),
 \label{eq:Kdifference}
\end{equation}
and therefore
\begin{equation}
 \ImPart K
 =\frac{t}{4}D(\tau,\mathbf z)
     +\frac18\bigl(H(\tau,\mathbf z)-H(u,\mathbf z)\bigr).
 \label{eq:imagdecomp}
\end{equation}
\end{proposition}

\begin{proof}
Conjugate at fixed \(x,y\) and replace \(p\) by \(-p\).
For \(q=|p|\), the direct difference is
\[
 -\frac{t}{4q}(e^{-iq\tau}-e^{iq\tau})
 +\frac{i}{8q^2}(e^{-iq\tau}+e^{iq\tau})
 =\frac{it}{2q}\sin(q\tau)+\frac{i}{4q^2}\cos(q\tau).
\]
The reflected difference is
\(-i\cos(qu)/(4q^2)\).
The identities hold with the same Abel factor, and
Lemma~\ref{lem:Fourier} permits its distributional removal.
\end{proof}

\begin{lemma}[Global radial representatives]
\label{lem:radial}
The cosine distribution is the locally integrable function
\[
 H(v,\mathbf z)=\frac{\mathbf1_{\{R>|v|\}}}{4\pi R}.
 \label{eq:H}
\]
Moreover \(D=-\partial_vH\). For \(R>0\),
\[
 D(v,R)=\frac{\delta(v-R)-\delta(v+R)}{4\pi R}.
 \label{eq:D}
\]
The derivative of \eqref{eq:H} specifies the distribution
at the spatial apex, with no added point-supported term.
\end{lemma}

\begin{proof}
Angular integration gives
\[
 H_\epsilon(v,R)=\frac1{2\pi^2R}
  \int_0^\infty e^{-\epsilon q}
                   \frac{\sin(qR)\cos(qv)}q\,\dd q.
\]
For real \(a\),
\[
 \int_0^\infty e^{-\epsilon q}\frac{\sin(aq)}q\,\dd q
             =\arctan(a/\epsilon),
\]
as follows by differentiating in \(a\), integrating the
elementary Laplace transform, and using the value zero
at \(a=0\).
Consequently
\[
 H_\epsilon(v,R)=
 \frac{\arctan((R+v)/\epsilon)
             +\arctan((R-v)/\epsilon)}{4\pi^2R}.
\]
It converges almost everywhere to \eqref{eq:H}.
For \(R>0\), its absolute value is at most \(1/(4\pi R)\),
which is locally integrable in \((v,\mathbf z)\).
Dominated convergence gives the global distributional
limit, including \(R=0\).

Fourier differentiation gives \(D=-\partial_vH\).
Differentiating the indicator at \(R>0\) gives
\eqref{eq:D}. Since the global limit of \(H_\epsilon\)
has already been identified as a locally integrable
function, its distributional derivative leaves no
undetermined apex contact.
\end{proof}

\begin{theorem}[Exact imaginary part]
\label{thm:imag}
For \(t,s>0\) and \(R>0\),
\begin{equation}
 \boxed{
 \begin{split}
 \ImPart K(x,y)
 ={}&\frac{t}{16\pi R}
       \bigl[\delta(\tau-R)-\delta(\tau+R)\bigr]\\
 &+\frac1{32\pi R}
       \bigl[\Theta(R-|\tau|)-\Theta(R-u)\bigr].
 \end{split}}
 \label{eq:imag}
\end{equation}
Away from the two cone boundaries it equals
\[
 \ImPart K=
 \begin{cases}
 0,&R<|t-s|,\\[1mm]
 (32\pi R)^{-1},&|t-s|<R<t+s,\\[1mm]
 0,&R>t+s.
 \end{cases}
\]
The reflected cone is a jump locus, not an additional
delta distribution.
\end{theorem}

\begin{proof}
Substitute Lemma~\ref{lem:radial} into
\eqref{eq:imagdecomp}, using \(t+s>|t-s|\).
The direct delta terms are retained separately.
\end{proof}

This rederives the locked evaluation of IX-E-2
\cite{IXE2}; it changes no inherited coefficient.

\begin{corollary}[Support, including the spatial apex]
\label{cor:imagsupport}
In the open positive-time chart,
\[
 \supp\ImPart K
   =\{(x,y): |t-s|\le|\mathbf x-\mathbf y|\le t+s\}.
 \label{eq:imagsupport}
\]
\end{corollary}

\begin{proof}
For \(R>0\), \eqref{eq:imag} vanishes off the displayed
closed slab and is positive and smooth in its interior.
Every point of the slab with \(R>0\) is a limit of
interior points.
At \(R=0\), the slab requires \(t=s\). Those points are
also limits of interior points.
Lemma~\ref{lem:radial} supplies the global distributions
and introduces no support outside the closure.
\end{proof}

At \(t=0\), the time-slice identity is \(K(0,s,\mathbf z)=0\).
At \(s=0\),
\[
 \ImPart K(t,0,\mathbf z)=\frac t4D(t,\mathbf z).
\]
These are spatial distribution identities, not assigned
pointwise values on a null cone.
The inherited observation tests here lie at positive
times; no enlargement of that test domain is required.

%=====================================================================
\section{The settled witness class and the unfinished bridge}
\label{sec:witness}
%=====================================================================

\begin{theorem}[Vanishing on every strongly separated pair]
\label{thm:strongzero}
Every pair satisfying Lemma~\ref{lem:spacelike} obeys
\[
 fg\,\ImPart K=0,\qquad
 \mathcal C_{f,g}=0.
\]
Both actual support orderings hold for every such pair.
\end{theorem}

\begin{proof}
On \(F\times G\),
\[
 R\ge|\mathbf x_0-\mathbf y_0|-r-s_0>2T\ge t+s.
\]
There is a positive compact separation from the
commutator support \eqref{eq:imagsupport}.
Thus its product with \(fg\) is zero distributionally.
The ordering statement was already proved by the
upper-support argument.
\end{proof}

\begin{proposition}[A nonzero observation-spacelike control]
\label{prop:control}
There are nonnegative nonzero compact tests \(f,g\)
supported in the laboratory with
\[
 |t-s|<R<t+s\quad\text{on }F\times G,
\]
for which \(\mathcal C_{f,g}\ne0\).
Observation-spacelike separation does not certify both
actual functional-support orderings.
\end{proposition}

\begin{proof}
Choose \(\lambda>0\) small enough that neighbourhoods
of
\[
 x_*=(\lambda,\mathbf a),\qquad
 y_*=(\lambda,\mathbf a+\lambda\mathbf e_1)
\]
and their retained shadows fit in the chart.
At the central pair, \(0<R=\lambda<2\lambda\).
The strict inequalities persist on sufficiently small
product neighbourhoods.

Take nonnegative bumps there, set
\(\partial_t\phi=1\) near \(F\), and \(h_{00}=1\) near
\(G\). Then
\[
 \mathcal C_{f,g}
   =-\frac{i}{8\pi}
      \int\frac{f(x)g(y)}{|\mathbf x-\mathbf y|}
                                  \,\dd^4x\,\dd^4y\ne0.
\]
This uses observation supports only.
The functional \(B_f\) can also depend on metric
configurations on its retained past and initial surface.
No two-way certificate has been supplied for the control.
\end{proof}

\begin{definition}[The actual support bridge (SB)]
\label{def:SB}
The remaining commutator-coverage obligation is
\begin{equation}
 B_f\gtrsim W_g,\quad W_g\gtrsim B_f
 \quad\Longrightarrow\quad
             f(x)g(y)\ImPart K(x,y)=0
 \quad\text{in }\mathcal D'(V^2),
 \tag{SB}
 \label{eq:SB}
\end{equation}
for every retained first-stage pair, followed by its
flip and conjugate transfer.
\end{definition}

\begin{proposition}[Upper support is not the bridge]
\label{prop:uppernotlower}
The inclusions in Theorem~\ref{thm:support} do not by
themselves establish (SB).
In particular, intersection of two upper support sets
does not establish intersection of the actual supports.
\end{proposition}

\begin{proof}
An inclusion \(A\subset A_+\) has no reverse inclusion.
Replacing the actual dependence set by \(P_F\cup F\)
in a contradiction requires a lower-support theorem.
The commutator evaluation only identifies a distribution
on observation variables and supplies no such reverse
support inclusion.
\end{proof}

\begin{theorem}[IX-E-2-ST stage release]
\label{thm:E2release}
Part III proves the exact imaginary part, its full
positive-time distributional support, vanishing on the
entire strongly separated two-way class, and a nonzero
observation-spacelike control.

The retained-pair obstruction criterion remains valid,
but no nonzero pair satisfying both actual orderings
has been certified. The release is
\textbf{Unresolved at the actual support bridge}.
No time-ordered replacement is constructed.
\end{theorem}

\begin{proof}
The positive results are
Theorem~\ref{thm:imag},
Corollary~\ref{cor:imagsupport},
Theorem~\ref{thm:strongzero}, and
Proposition~\ref{prop:control}.
Proposition~\ref{prop:uppernotlower} identifies the
missing inference.
\end{proof}

%=====================================================================
\part{IX-E-3-ST: the boundary-trace certificate}
%=====================================================================

\section{Exact quadratic support and surface non-cancellation}
\label{sec:surface}
%=====================================================================

\begin{proposition}[Exact support of the quadratic slot]
\label{prop:Wexact}
For every test \(g\),
\[
 \fsupp W_g=\supp g.
 \label{eq:Wexact}
\]
\end{proposition}

\begin{proof}
The upper inclusion is immediate.
At the allowed configuration \(h_{00}=1\),
the metric derivative is \(2g\) in the \(00\)-component.
Its distributional support is \(\supp g\).
Lemma~\ref{lem:derivativesupport} gives the lower inclusion.
\end{proof}

The surface map in the copied sharp adjoint has the
algebraic form
\[
 \Bsurf^{\alpha\beta}(v)
 =-n^{(\alpha}v^{\beta)}
       +\frac12\eta^{\alpha\beta}n_\mu v^\mu,
\]
where \(n\) is a non-null normal to \(\Sigma\).

\begin{lemma}[Injective surface coefficient]
\label{lem:surfaceinjective}
The map \(v\mapsto\Bsurf(v)\) is injective.
\end{lemma}

\begin{proof}
Contraction gives
\[
 n_\alpha\Bsurf^{\alpha\beta}(v)
               =-\frac12(n_\alpha n^\alpha)v^\beta.
\]
The scalar factor is nonzero.
\end{proof}

\begin{lemma}[A bounded bulk term cannot cancel a surface delta]
\label{lem:nocancel}
Let \(c\) be locally bounded near \(\Sigma\), and let
\(\beta\) be smooth on \(\Sigma\).
If \(\beta(\mathbf z_0)\ne0\), then
\[
 \theta(t)c(t,\mathbf z)+\delta(t)\beta(\mathbf z)
\]
is not zero in any neighbourhood of
\((0,\mathbf z_0)\).
\end{lemma}

\begin{proof}
Choose a spatial test \(\psi\) supported arbitrarily
near \(\mathbf z_0\) with
\(\int\beta\psi\ne0\).
Pair with
\(\chi(t/\epsilon)\psi(\mathbf z)\), where
\(\chi(0)=1\) and \(\chi\) is compactly supported.
The delta pairing is fixed and nonzero.
Local boundedness makes the bulk pairing \(O(\epsilon)\).
For sufficiently small \(\epsilon\) they cannot cancel.
\end{proof}

This concerns the regular initial surface, not the conical
worldsheet. The certificate below is not the carrier's
abstract trace coordinate.

%=====================================================================
\section{The certificate and its lower-support consequence}
\label{sec:TC}
%=====================================================================

\begin{assumption}[Boundary-trace certificate (TC)]
\label{ass:TC}
For every compact smooth covector source \(a\) in \(V\),
the \emph{same actual adjoint} \(b=\Ezero^*a\) appearing
in \eqref{eq:sharpadjoint} is smooth up to \(\Sigma\),
\(C^*b\) is locally bounded there, and
\begin{equation}
 b_\mu(0,\mathbf z)
  =\varepsilon_{\mathrm{tr}}
    \int
      \frac{\delta(t-|\mathbf w-\mathbf z|)}
           {4\pi|\mathbf w-\mathbf z|}
           a_\mu(t,\mathbf w)\,\dd t\,\dd^3w,
 \qquad \varepsilon_{\mathrm{tr}}\in\{1,-1\}
 \tag{TC}
 \label{eq:TC}
\end{equation}
with one fixed convention sign.
All relevant initial points and cone segments are
retained in the laboratory.
\end{assumption}

The nonzero overall sign does not affect support.
The statement is more precise than an upper causal-ball
bound. It is not assumed for the inherited operator in
the unconditional release.

\begin{theorem}[Null-sphere lower support under (TC)]
\label{thm:sphere}
Assume (TC) and the copied sharp adjoint.
For every \(x=(t,\mathbf x)\in F=\supp f\), \(t>0\),
\begin{equation}
 \{(0,\mathbf z):|\mathbf z-\mathbf x|=t\}
                                  \subset\fsupp B_f.
 \label{eq:sphere}
\end{equation}
\end{theorem}

\begin{proof}
First take \(f(x)\ne0\), and fix a sphere point
\(\mathbf z\). Near \(x\),
\(r_{\mathbf z}(\mathbf w)=|\mathbf w-\mathbf z|\)
is smooth and positive.
Choose a nonnegative compact cutoff \(\chi\), positive
at \(x\), supported in that neighbourhood, and set
\[
 \phi_{\CC}(v,\mathbf w)
     =(v-r_{\mathbf z}(\mathbf w))
                         \overline{f(v,\mathbf w)}\chi(v,\mathbf w).
\]
Its support is in the positive-time chart.
The metric derivative of \(B_f\) is \(L^*a\), where
\[
 a=-f\,\dd\phi_{\CC}.
\]
On \(v=r_{\mathbf z}(\mathbf w)\),
\(\partial_v\phi_{\CC}=\overline f\,\chi\).
Thus (TC) gives
\[
 b_0(0,\mathbf z)
 =-\varepsilon_{\mathrm{tr}}
  \int
   \frac{|f(r_{\mathbf z}(\mathbf w),\mathbf w)|^2
               \chi(r_{\mathbf z}(\mathbf w),\mathbf w)}
        {4\pi r_{\mathbf z}(\mathbf w)}
                        \,\dd^3w\ne0.
\]
The integrand is positive on a nonempty open set.
This respects the restricted source \(a=-f\,\dd\phi\);
its components have not been chosen independently.

Decompose \(\phi_{\CC}\) into real and imaginary parts.
At least one real configuration has nonzero trace.
Lemma~\ref{lem:surfaceinjective} gives a nonzero surface
coefficient; Lemma~\ref{lem:nocancel} prevents its
cancellation by the bulk term.
The derivative-support characterization places
\((0,\mathbf z)\) in \(\fsupp B_f\).

For an arbitrary \(x\in F\), choose
\(x_j=(t_j,\mathbf x_j)\to x\) with \(f(x_j)\ne0\).
Writing \(\mathbf z=\mathbf x+t\mathbf n\), use
\(\mathbf z_j=\mathbf x_j+t_j\mathbf n\).
Closedness of functional support proves the result.
\end{proof}

For a separately declared boundary-touching test extension,
the same closure argument would give
\(F\cap\Sigma\subset\fsupp B_f\), provided its derivatives,
adjoint identity, and boundary pairing are included in
that extension. No boundary test-domain enlargement is
needed for the interior inherited sector treated here.

\begin{lemma}[Sphere--ball intersection]
\label{lem:sphereball}
For \(t>0\), \(s\ge0\), and
\(R=|\mathbf x-\mathbf y|\),
\[
 \{|\mathbf z-\mathbf x|=t\}
       \cap\{|\mathbf z-\mathbf y|\le s\}\ne\varnothing
 \quad\Longleftrightarrow\quad
                 t-s\le R\le t+s.
\]
\end{lemma}

\begin{proof}
The minimum distance from \(\mathbf y\) to the sphere
is \(|R-t|\), including \(R=0\).
The condition is \(|R-t|\le s\), which is equivalent
to the displayed inequalities.
\end{proof}

\begin{theorem}[The two-way bridge under (TC)]
\label{thm:bridge}
Under Assumption~\ref{ass:TC}, (SB) holds for every
retained first-stage pair.
In particular, the first-stage commutator vanishes on
every retained pair satisfying both actual orderings.
\end{theorem}

\begin{proof}
By Proposition~\ref{prop:Wexact}, every \(y\in G\)
belongs to \(\fsupp W_g\).
Suppose an observation pair \(x\in F,y\in G\) belongs
to the closed commutator slab
\[
 |t-s|\le R\le t+s.
\]
Then \(t-s\le R\le t+s\).
Lemma~\ref{lem:sphereball} supplies an initial sphere
point \(z=(0,\mathbf z)\) of \(x\) with
\(|\mathbf z-\mathbf y|\le s\).
Theorem~\ref{thm:sphere} places \(z\) in
\(\fsupp B_f\), while \(z\in J^-(y)\).
Thus \(B_f\gtrsim W_g\) fails.

Consequently a two-way pair has \(F\times G\) disjoint
from the entire closed support in
\eqref{eq:imagsupport}. Multiplication by \(fg\)
annihilates \(\ImPart K\), including its direct cone
and apex. Equation~\eqref{eq:commutator} proves vanishing.
\end{proof}

The proof needs null spheres, not solid-ball lower support.
It also does not require scalar-slot controllability.

\begin{proposition}[Flip and conjugate transfer]
\label{prop:conjugatebridge}
Let \(J(d)=S(d)-S(\sigma d)\).
Then
\[
 J(\gamma d)=-J(d)^*.
\]
Conjugation preserves functional support, so a proved
original-sector bridge transfers to retained flips and
conjugates.
This does not evaluate arbitrary relations among sums
of actual tensors.
\end{proposition}

\begin{proof}
Free reversal gives
\(S(\gamma d)=S(\sigma d)^*\) and
\(S(\sigma\gamma d)=S(d)^*\).
Subtract. A functional changes under a local perturbation
exactly when its complex conjugate changes, proving
support invariance.
\end{proof}

%=====================================================================
\section{A specified flat realization and the solid-ball correction}
\label{sec:flat}
%=====================================================================

The following is a diagnostic realization, not a replacement
of an unspecified inherited operator. Let
\[
 (Ch)^\mu=\partial_\nu h^{\mu\nu}
             -\frac12\partial^\mu(\eta^{\alpha\beta}h_{\alpha\beta}),
\]
and define the componentwise flat zero-Cauchy response
\begin{equation}
 (\Eflat j)(t,\mathbf x)=
 \int_0^t\int_{\RR^3}
  \frac{\delta(t-v-|\mathbf x-\mathbf w|)}
       {4\pi|\mathbf x-\mathbf w|}
           j(v,\mathbf w)\,\dd^3w\,\dd v.
 \label{eq:Eflat}
\end{equation}
All applications are supported inside the retained chart.

\begin{proposition}[(TC) for the specified realization]
\label{prop:flatTC}
The actual transpose of \eqref{eq:Eflat}, with the same
pairing convention, satisfies (TC) with
\(\varepsilon_{\mathrm{tr}}=1\).
\end{proposition}

\begin{proof}
Transpose the compact supported pairing and collect the
coefficient of \(j(v,\mathbf z)\):
\[
 (\Eflat^*a)(v,\mathbf z)=
 \int_{t\ge v}\int
   \frac{\delta(t-v-|\mathbf w-\mathbf z|)}
        {4\pi|\mathbf w-\mathbf z|}
             a(t,\mathbf w)\,\dd^3w\,\dd t.
\]
At \(v=0\) this is \eqref{eq:TC}.
Equivalently,
\[
 (\Eflat^*a)(v,\mathbf z)
   =\frac1{4\pi}\int_0^\infty r
          \int_{S^2}a(v+r,\mathbf z+r\mathbf n)
                              \,\dd\Omega(\mathbf n)\,\dd r.
\]
On compact parameter sets the effective \(r\)-range is
bounded; all derivatives pass under the integral.
The result is smooth near \(\Sigma\), and the first-order
constant-coefficient operator \(C^*\) preserves smoothness.
\end{proof}

This explicit formula represents the local flat response.
It supplies no conical Green operator.

For compact \(F\) in positive times, define
\[
 S_F=\{\mathbf z:\exists(t,\mathbf x)\in F,\
                        |\mathbf z-\mathbf x|=t\},
\]
\[
 N_F=\{(v,\mathbf z):\exists(t,\mathbf x)\in F,\
        0\le v\le t,\ |\mathbf z-\mathbf x|=t-v\}.
\]

\begin{theorem}[Exact initial-surface support in the flat realization]
\label{thm:surfaceexact}
For \(L_{\mathrm{fl}}=\Eflat C\),
\[
 \fsupp B_f^{\mathrm{fl}}\cap\Sigma
                               =\{0\}\times S_F.
 \label{eq:surfaceexact}
\]
\end{theorem}

\begin{proof}
The lower inclusion is Theorem~\ref{thm:sphere}.
For every source \(a=-f\,\dd\phi\), the transposed formula
has support in \(N_F\). Applying the local \(C^*\)
does not enlarge it. The surface term has support in
\(\{0\}\times S_F\).
The scalar derivative is supported in \(F\), away from
\(\Sigma\).
The compact set \(N_F\cup F\) contains every first
derivative support and meets \(\Sigma\) exactly in
\(\{0\}\times S_F\).
Lemma~\ref{lem:derivativesupport} proves the upper inclusion.
\end{proof}

\begin{proposition}[Solid-ball lower support is false]
\label{prop:solidball}
There are nonzero \(f\) for which a relatively open
initial collar inside a backward causal ball is disjoint
from \(\fsupp B_f^{\mathrm{fl}}\).
\end{proposition}

\begin{proof}
Choose a nonzero bump positive at \((1,\mathbf0)\), with
\[
 F\subset[9/10,11/10]\times\overline B(\mathbf0,1/10).
\]
Use the relative collar
\[
 U_0=[0,1/4)\times B(\mathbf0,1/4).
\]
For \((t,\mathbf x)\in F\), \((v,\mathbf z)\in U_0\),
\[
 |\mathbf x-\mathbf z|<7/20,\qquad t-v>13/20.
\]
There is no backward null incidence, so \(U_0\cap N_F\)
is empty. All first derivative kernels vanish there,
including the surface contribution.
Yet the time-zero ball from \((1,\mathbf0)\) contains
\(B(\mathbf0,1/4)\).
A translation and positive rescaling places the same
diagnostic in a sufficiently large retained chart.
\end{proof}

The gap does not produce a two-way obstruction witness.
The sphere--ball intersection in
Theorem~\ref{thm:bridge} still excludes every observation
pair in the commutator slab.

\begin{proposition}[Observation support is visible in the flat model]
\label{prop:flatF}
For the specified flat realization,
\(F\subset\fsupp B_f^{\mathrm{fl}}\).
\end{proposition}

\begin{proof}
At an interior point \(x\) with \(f(x)\ne0\), choose
\(w\in\mathcal D(V)\), supported in a prescribed small
neighbourhood, with
\(\dd w(x)=0\), \(Pw(x)\ne0\).
Set \(h_{\alpha\beta}=\eta_{\alpha\beta}Pw\).
Then \(Ch=-P\,\dd w\); the compact zero-data identity
for \eqref{eq:Eflat} gives \(L_{\mathrm{fl}}h=-\dd w\).
The scalar derivative kernel is
\[
 -\partial_\mu(f\partial^\mu w),
\]
whose value at \(x\) is \(-f(x)Pw(x)\ne0\).
Real test variations detect a nonzero complex kernel
by decomposition if necessary.
Taking closures proves the assertion.
\end{proof}

\begin{corollary}[Full geometric exclusion in the flat model]
\label{cor:flatstrong}
For the specified realization, both actual orderings
imply
\[
 |\mathbf x-\mathbf y|>t+s
       \quad\text{for every }x\in F,\ y\in G.
\]
In particular (SB) holds there unconditionally.
\end{corollary}

\begin{proof}
If \(R<t-s\), then \(y\in J^-(x)\), and
Proposition~\ref{prop:flatF} makes
\(W_g\gtrsim B_f\) fail.
If \(t-s\le R\le t+s\), a lower-support initial sphere
point lies in \(J^-(y)\), making
\(B_f\gtrsim W_g\) fail.
These exhaust \(R\le t+s\).
\end{proof}

%=====================================================================
\section{The inherited identification audit}
\label{sec:identification}
%=====================================================================

\begin{proposition}[Same-adjoint audit]
\label{prop:sameadjoint}
There are two distinct legitimate conclusions.
\begin{enumerate}[label=\textup{(\roman*)}]
\item From the weak inherited inputs
Assumptions~\ref{ass:carrier}--\ref{ass:parent},
the present manuscript has not verified (TC) for the
inherited operator. Its domain-wide bridge remains
conditional.
\item If the inherited response and actual transpose on
all required compact covector sources are identified
with \eqref{eq:Eflat} and its transpose, with the
specified normalization and retained surface term,
Proposition~\ref{prop:flatTC} verifies (TC), and
Theorem~\ref{thm:bridge} clears the commutator gate
for that identified realization.
\end{enumerate}
In neither case is a time-ordered product constructed.
\end{proposition}

\begin{proof}
In case (i), the displayed trace identity for the same
actual adjoint has not been supplied as an input or
proved for that inherited realization.
In case (ii), the identity and regularity have been
proved by transposition, and the bridge theorem applies.
The trace and support statements contain no binary
time-ordered replacement kernels or old time-ordered map.
\end{proof}

\begin{remark}[Correction relative to an earlier combined draft]
\label{rem:prioraudit}
An earlier IX-C-ST draft may display an ``advanced trace
formula'' on the sharp source domain.
If that formula is accepted as proved for the very same
actual adjoint, on every source needed here, and with
the local boundedness required in (TC), then it already
supplies the certificate, up to the stated convention
sign. In that reading the bridge must be marked proved,
not simultaneously assumed and unverified.

If that operator/domain identification has not been
established, the formula cannot be imported by notation
alone. The weak inherited release retains that precise
verification obligation. This distinction avoids both
silently withdrawing an accepted premise and silently
adding an unverified one.
\end{remark}

The certificate concerns a componentwise adjoint trace
on null-sphere incidences. It is not:
\begin{itemize}
\item the abstract carrier trace modulo microcausal linear
kernels;
\item a VII-E/VII-F observation-boundary theorem;
\item an VIII matching certificate;
\item a global inverse on the conical spacetime.
\end{itemize}

\begin{theorem}[IX-E-3-ST stage release]
\label{thm:E3release}
Part IV proves exact support of \(W_g\), surface
non-cancellation, the null-sphere lower-support theorem
and two-way bridge under (TC), and verification of (TC)
for the explicitly specified flat realization.
It also disproves the unnecessary solid-ball
lower-support assertion in that realization.

For the weak inherited operator contract, verification
of (TC) remains \textbf{Unresolved}.
If the same-adjoint identification is supplied, the
commutator bridge is proved; the overall causal-product
release still remains \textbf{Unresolved}.
\end{theorem}

\begin{proof}
The positive claims are proved in
Sections~\ref{sec:surface}--\ref{sec:flat}.
Proposition~\ref{prop:sameadjoint} gives the two
version-consistent bridge verdicts.
Neither branch supplies the analytical construction
required in Requirement~\ref{req:analytic}.
\end{proof}

%=====================================================================
\section{Shared finite Enter certificate interface}
\label{sec:operational}
%=====================================================================

This section is independent of the unresolved field
construction. It represents an installed finite
certificate, not the continuum field or a physical
measurement of its commutator.

\subsection{Clock and description register}

Choose one finite clock
\(C\cong\CC^{2^m}\), \(m\ge1\), with basis
\(\{\ket{\tau_k}\}\), and let \(S\) contain all surviving
registers. Put
\[
 D_k=\bra{\tau_k}_C\otimes I_S,\qquad P_k=\proj{\tau_k}.
\]

\begin{theorem}[Complete destructive clock]
\label{thm:instrument}
The map
\[
 \mathcal M_C(X)
  =\sum_k\proj k_R\otimes D_kXD_k^\dagger
  =\sum_k\proj k_R\otimes
      \Tr_C[(P_k\otimes I)X(P_k\otimes I)]
\]
is CPTP and obeys
\[
 \Tr_R\mathcal M_C(X)=\Tr_CX.
\]
These identities hold after adjoining every untouched
reference. The clock has no quantum output factor.
\end{theorem}

\begin{proof}
The recorded Kraus operators
\(\ket k_R\otimes D_k\) have squared moduli summing to
\(I_{CS}\). Clock-basis expansion identifies the
\(k\)-block with \(X_{kk}\), proving the formulae and
the discard identity. Tensoring the calculation proves
the reference assertion.
\end{proof}

This is the finite instrument used in I-B and En09-A
\cite{IB,En09}. It consumes the clock encoding, not
the geometric time coordinate.

A certificate catalogue has finitely many entries in
one experiment, each recording, for example,
\[
 (\text{stage},\text{domain ID},\hbar\text{-order},
 c\text{-ID},\text{support status},\text{TC status},
 \text{error enclosure}).
\]
Real parameters and smooth tests are stored by declared
finite descriptions or approximations. No universal
finite-bit encoding of arbitrary reals or functions
is asserted.
One stage tag does not create another geometric clock.

\begin{proposition}[Calibration and recovery limits]
\label{prop:clocklimits}
At one fixed event, exact agreement of distinct
calibrated values with that event's time allows at most
one positive-probability code.
The clock readout has no left inverse on all clock states.
\end{proposition}

\begin{proof}
The first claim is distinctness of the calibration.
The states
\((\ket{\tau_0}\pm\ket{\tau_1})/\sqrt2\) give identical
readout outputs with the same surviving input, so both
cannot be recovered.
\end{proof}

A nontrivial stochastic certificate clock is therefore
a programme/history calibration unless an additional
time-observable contract is given.

\subsection{A fixed finite-table comparison}

Let \(i\) be a classical catalogue index and \(P\) a
surviving payload. Denote by \(X_{ki}\) the input block
after clock readout and catalogue-basis pinching.
For supplied \(v_{ki}\in[-1,1]\), define
\[
 p_y(k,i)=\frac{1+yv_{ki}}2,\qquad y=\pm1,
\]
\[
 \mathcal I_v(X)=
   \sum_{k,i,y}\proj{k,i,y,r(k,i)}
                         \otimes p_y(k,i)X_{ki},
\]
with a fixed finite report function \(r\).

\begin{proposition}[Fixed-interface approximation]
\label{prop:table}
The channel \(\mathcal I_v\) is CPTP.
With the same labels, pinching, report function, and
payload interface,
\[
 \ddia(\mathcal I_v,\mathcal I_{\widetilde v})
       =\frac12\max_{ki}|v_{ki}-\widetilde v_{ki}|,
 \qquad \ddia(\Phi,\Psi)=\frac12\|\Phi-\Psi\|_\diamond.
\]
\end{proposition}

\begin{proof}
Kraus operators are
\[
 \sqrt{p_y(k,i)}\ket{k,i,y,r(k,i)}
       (\bra{\tau_k}\bra i)\otimes I_P.
\]
They are complete.
Including a reference, orthogonal output blocks make
the trace norm of the difference at most
\[
 \max_{ki}|v_{ki}-\widetilde v_{ki}|
                                  \sum_{ki}\|X_{ki}\|_1.
\]
Pinching is an average of unitary conjugations and
contracts trace norm even on arbitrary operators.
A basis input at a maximizing index attains the bound.
\end{proof}

A supplied finite enclosure of an evaluation may determine
\(v_{ki}\). The table does not acquire the field,
verify (TC), read a causal past, or construct \(\Ttwo\).
Changing orthogonal report labels is not covered by
the numerical comparison above.

\begin{proposition}[Record equality is weaker than residual equality]
\label{prop:residual}
Two finite instruments have the same record laws on all
inputs exactly when their outcome effects agree.
Agreement on all recorded residual observables requires
agreement of the corresponding adjoint maps on those
observables. Equal records alone do not suffice.
\end{proposition}

\begin{proof}
Pull the record effects or recorded residual observables
back to the input, and use separation by density matrices.
For a strict example, identity and computational
dephasing with the same one-outcome record have equal
record law. On \(\proj+\), the residuals are \(\proj+\)
and \(I/2\), at trace distance \(1/2\).
\end{proof}

\subsection{Scheduled support and physical containment}

\begin{theorem}[Complete-network locality]
\label{thm:locality}
For a finite layered block-channel network and a joint
output \(Y\), the recursively defined backwards ancestor
set \(N_{s,t}(Y)\) satisfies
\[
 (\Phi_{s+1}^*\cdots\Phi_t^*)(\AA(Y))
                               \subseteq\AA(N_{s,t}(Y)).
\]
An intervention outside that complete ancestor set cannot
alter the joint output law.
Reference-assisted comparison retains the joint
ancestor--reference reduction.

If every dependency port has a regular laboratory
placement and every dependency edge has a supplied
future-causal route, then those dependencies are contained
in the prescribed host causal relation.
\end{theorem}

\begin{proof}
Every channel adjoint is unital. A block disjoint from
the current support acts on an identity factor; a meeting
block enlarges support only inside that block.
Reverse induction proves the inclusion.
Testing all output observables gives the intervention
statement, with references carried throughout.
Concatenating the supplied causal routes proves
physical containment.
\end{proof}

This keeps scheduled ancestry, actual influence, and
physical containment distinct \cite{En03,STInterfaces}.
A contraction graph or an association schedule is not
a physical port network.

\subsection{Nonempty regular transport realization}

Assume finite local preparation, classical processing,
destructive readout, and exact finite-register carriage
along declared causal paths are permitted.
These are ideal operational permissions, not derived
field dynamics.

Choose a developed segment of length \(\ell>0\) in a
compact regular tube. Install \(n+1\) stations with
\(p\)-qubit payload registers, \(p\ge1\).
Initialize all but the sender in a fixed blank.
Generate and retain the complete classical certificate,
wait for a positive buffer, and forward it on explicit
causal wires.
At each hop exchange neighbouring register contents
by opposite carriage paths of developed duration
\(2\ell/n\), not by an instantaneous distant gate.

\begin{theorem}[Reference-preserving certificate transport]
\label{thm:transport}
The complete route transmits an arbitrary payload and
all its untouched reference correlations exactly.
All non-output payload registers end in independent
blanks. The complete classical certificate is forwarded.
Every dependency has a causal regular route.
\end{theorem}

\begin{proof}
After hop \(j\), the original payload factor, including
its reference correlations, occupies station \(j\);
the other payload stations are blank.
Tensor-factor exchange proves this by induction.
Copying a designated classical record preserves its
joint law and is not cloning an unknown quantum state.
Each carriage path has speed \(1/2\) in developed units.
Local processing and buffering take positive duration;
receiver controls wait for every required input.
\end{proof}

Orthogonal sender payloads give receiver trace-distance
contrast one. This is a declared transport witness,
not entanglement generated by the cone \cite{IB,En08}.

If the certificate has \(b\) bits, the catalogue \(g\)
bits, and lookup uses \(w\) work bits, a conservative
reserve is
\[
 m+g+1+(n+1)p+w+(n+1)b
\]
qubit-sized basis-state carriers, with external references
separately declared.
There are \(n\) exchanges and \(n\) certificate
transmissions. Carriage takes developed time \(2\ell\);
all processing, copying, and buffering times are added
before choosing the experiment window.
No reset-cost or thermodynamic theorem is claimed.

For compatible implementations on the same complete
interfaces, replacing one channel factor at a time gives
\[
 \ddia(\widetilde\Gamma,\Gamma)
 \le\min\{1,\epsilon_{\mathrm{enc}}+
              \epsilon_{\mathrm{dec}}+
              \epsilon_{\mathrm{table}}+\sum_j\epsilon_j\}.
\]
This finite-channel estimate is distinct from every
continuity question for the field-theoretic maps
\cite{Watrous}.

%=====================================================================
\section{Final assembly and exact remaining gate}
\label{sec:release}
%=====================================================================

\begin{theorem}[Combined IX-D-ST release]
\label{thm:release}
Under the stated inherited inputs, the four ordered
parts establish:
\begin{enumerate}[label=\textup{(\roman*)}]
\item laboratory-local causal interfaces, support inclusions,
the free-word scalar non-lift, and separation of causal
factorization from free coherence;
\item the first-stage commutator identity, fixed-domain
obstruction criterion, and exact algebraic finite-relation
extension criterion;
\item the direct-plus-reflected evaluation
\eqref{eq:imag}, exact vanishing on the entire strongly
separated two-way class, and a nonzero observation-spacelike
control without an inherited two-way certificate;
\item exact support of \(W_g\), the null-sphere lower-support
theorem and bridge under (TC), and a fully specified
flat realization verifying that certificate;
\item a common finite destructive-clock, certificate,
locality, and regular reference-preserving transport
interface.
\end{enumerate}
Each stage is a local Grade S interface package.
For the weak inherited operator, (TC) remains an explicit
verification obligation. If its same-adjoint identification
is supplied, the commutator gate clears.

In both cases, the complete sharp causal-product
release is \textbf{Unresolved}: no sharp \(\TO\),
\(\Ttwo\), normalized \(R_1\), or \(R_2\) is constructed.
\end{theorem}

\begin{proof}
The stage releases are
Theorems~\ref{thm:Drelease},
\ref{thm:Erelease},
\ref{thm:E2release}, and
\ref{thm:E3release}.
The operational section proves every finite interface
clause independently of the absent time-ordered map.
The same-adjoint audit distinguishes the two bridge
statuses without changing the fixed causal target.
Requirement~\ref{req:analytic} has not been discharged
in either branch.
\end{proof}

\begin{center}
\small
\renewcommand{\arraystretch}{1.15}
\begin{tabularx}{\linewidth}{@{}p{.17\linewidth}XX@{}}
\toprule
Stage & Finished here & Not released\\
\midrule
IX-D-ST &
Interfaces, support bounds, non-lift, conditional
subtraction and contact contradiction, order audit &
Sharp time ordering and normalized retarded maps\\
IX-E-ST &
Ordering geometry, commutator identity, fixed-domain
criterion, algebraic relation criterion &
Analytical extension and its complete consistency\\
IX-E-2-ST &
Exact imaginary part and full strong-class vanishing &
The inherited actual-support bridge\\
IX-E-3-ST &
Exact quadratic support and bridge under (TC);
specified flat verification &
(TC) identification for a weak unspecified inherited
adjoint; any time-ordered product\\
\bottomrule
\end{tabularx}
\end{center}

\scopebox{The next analytical task}{%
The free gate is not the live stop.
The next construction must supply a sharp time-ordered
extension on the fixed actual domain, prove all ordered
restrictions and actual relations, establish admission
and named continuity, solve its permitted contact and
old-overlap equations, and prove its involution.

A trace certificate clears a commutator consistency test.
It does not carry out that construction.
No general free-domain enlargement, higher time ordering,
or switched G2 construction has been started.}

\paragraph{Retained topology boundary.}
The VII-C obstruction remains under its original joint
requirements (E1)--(E4), as documented in
\cite{VIIC}. Numerical subtraction is not a proof of
normal-topology admission continuity.
F9a is not F9b; separate classical multiplication is
not quantum hypocontinuity. The unchanged sharp
approximants still do not converge in \(\taus\).

\paragraph{Geometry boundary.}
Chart \(J^\pm\), the spacelike comparison construction,
and the trace witness are local comparison statements.
They do not resolve the worldsheet or construct global
conical propagators.
The catalogue and every time-ordering token leave the
host metric fixed.

\paragraph{Quantum and downstream boundary.}
No inherited interacting characteristic quantum
coefficient is admitted. The already inherited formal
free coefficients are not denied by this statement.
No interacting BRST/BV differential, fieldwise Ward
identity, ultraviolet completion, or interacting field
is constructed.

Grade E is not constructed.
O.1 stays \loc{NOT_CLOSED} in its stated inherited scope.
XV-B is not opened as a downstream quantum-admission
exit. XVI-N is not discharged.
This manuscript discharges neither the historical H2
problem nor the full I3/J2 characteristic-map obligations.
It does not withdraw XIV-I's narrower constructed
internal-amplitude result.

%=====================================================================
\appendix
\section{Debugging audit}
\label{app:debug}
%=====================================================================

\begin{longtable}{@{}p{.33\linewidth}p{.62\linewidth}@{}}
\toprule
Invalid upgrade & Correction\\
\midrule
\endfirsthead
\toprule
Invalid upgrade & Correction\\
\midrule
\endhead

The four sheets are independent constructions &
They use one host contract, one inherited free sector,
and four ordered stage releases.\\[4pt]

Free coherence constructs time ordering &
The interfaces and the auxiliary classical-product
counterexample separate these assertions.\\[4pt]

A constant projection defines a retarded map &
It loses nonconstant and lower-order coefficient
information and supplies no causal extension.\\[4pt]

Double ordering requires overlap &
It requires causal disjointness, excluding null relation
and coincidence.\\[4pt]

A later slab proves exactly one ordering &
It proves one ordering. Actual causal relation is needed
to rule out the reverse.\\[4pt]

Full support or injectivity computes the commutator &
The commutator depends on \(K-\overline K\), evaluated
independently.\\[4pt]

Observation-spacelike means functionally two-way &
The sharp metric dependence includes its retained
past and potentially its initial surface.\\[4pt]

An upper causal ball proves lower support &
No reverse inclusion follows. A solid-ball lower theorem
is false in the specified flat realization.\\[4pt]

The reflected cone carries a second delta &
It is a jump of the locally integrable cosine difference.
The direct delta remains separate.\\[4pt]

The apex can receive an arbitrary contact &
The common-Abel limit and global locally integrable
cosine representative already fix it.\\[4pt]

The source \(a=-f\,\dd\phi\) can be chosen componentwise &
The sphere detector uses a single explicit scalar
configuration respecting that restriction.\\[4pt]

An abstract carrier trace is (TC) &
(TC) identifies the same actual adjoint on its required
source domain and gives its null-sphere formula.\\[4pt]

A flat trace calculation verifies every inherited operator &
A same-operator, same-domain, same-normalization
identification is required.\\[4pt]

An earlier accepted trace formula can be assumed while
(TC) is still declared unverified &
If the formula has all of (TC)'s hypotheses for the
same adjoint, the bridge is already proved. The two
input regimes are explicitly separated.\\[4pt]

An algebraic complement gives continuity &
The extension criterion is algebraic; no continuous
complement or sharp kernel is produced.\\[4pt]

A contact changes two unequal forced free values into one &
Factorization requires equality to both; the fixed-domain
contradiction is independent of the proposed contact.\\[4pt]

The parent \(cr\) class classifies binary contacts &
It is a supplied three-observation numerical conversion
class, not a binary causal ambiguity theorem.\\[4pt]

A third-order numerator gives a third-order quotient &
Only the quotient through second order is determined.\\[4pt]

Conditional subtraction is a slot-support theorem &
It proves a functional-pair vanishing implication only.\\[4pt]

A certificate clock consumes geometric time &
Only the finite measured register names are consumed.\\[4pt]

Scheduled ancestry is a physical causal past &
Physical containment needs separately certified causal
routes.\\[4pt]

Certificate transport is field transport or generated
gravitational entanglement &
The transported object is a finite register; the host and
carriage permissions are prescribed.\\

\bottomrule
\end{longtable}

%=====================================================================
\section{Routing and documentary separations}
\label{app:routing}
%=====================================================================

The following are proposed documentary routing records,
not an assertion that the registry was modified.

\begin{verbatim}
delivery:
  filename: IX-D-ST.tex
  form: one manuscript, four ordered local stages

shared:
  host: supported regular IX-A-ST / I-B presentation
  track: product
  bearingProblem: products
  nearUv: false
  emergenceSource: false
  quantumCertificate: RG-open
  authorField: empty
  compilationAsserted: false

stages:
  - identifier: IX-D-ST
    localGrade: S
    timeLandmarks: 1
    causalProduct: Unresolved

  - identifier: IX-E-ST
    localGrade: S
    timeLandmarks: 1
    causalProduct: Unresolved

  - identifier: IX-E-2-ST
    localGrade: S
    timeLandmarks: 1
    inheritedSupportBridge: Unresolved
    causalProduct: Unresolved

  - identifier: IX-E-3-ST
    localGrade: S
    timeLandmarks: 1
    weakInheritedTC: Unverified
    bridgeUnderTC: Proved
    specifiedFlatBridge: Proved
    causalProduct: Unresolved

notStarted:
  - X-A-ST
  - G2 sheet
  - unified IX-ST
\end{verbatim}

The intended source/adaptation order is
\[
 \mathrm{IX\!-\!D},\ \mathrm{IX\!-\!D\!-\!ST},\
 \mathrm{IX\!-\!E},\ \mathrm{IX\!-\!E\!-\!ST},
\]
followed by IX-E-2, IX-E-2-ST, IX-E-3, IX-E-3-ST.
The one-file packaging does not claim four separate
registry submissions.

\paragraph{Product obligations.}
\loc{causal-interface-not-time-ordered-product},
\loc{commutator-not-causal-product},
\loc{support-bridge-not-time-ordered}, and
\loc{trace-certificate-not-causal-product}
remain explicit separations.
The corresponding \loc{not-emergence} obligations hold
at every stage: the cone, lapse, and metric are inputs.

\paragraph{Documentary comparisons, not extra premises.}
I-B and IX-A-ST have the explicit roles restated above.
The IX-Free-2 release is imported only as the specified
free coefficient assignment.
VII-D/IX-B supplies the conditional numerical parent,
not a causal prescription.
VIII-ST and VII-J-ST compare fixed-host catalogue
control and complete-network locality; they are not
analytical product inputs \cite{STInterfaces}.

VII-E, VII-F, and VIII observation or matching certificates
do not verify (TC).
En05-A and En08-B distinguish prescribed causal geometry
from a derived cone.
En03-A and En09-A do not remove external time.
En10-A's source-weight acquisition contract does not
acquire this commutator or residue
\cite{OperationalRecords}.

VII-H, VII-I, Em01-B, and Em01-C concern different
benchmarks, smoothing estimates, and scalar expansions.
They are not the binary time-ordered extension here.
XV-B, XVI-N, XVI-O, and XIV-I retain their separate,
version-qualified analytical boundaries
\cite{BoundaryRecords}.

\begin{remark}[The OpenAI catalogue is not a premise]
\label{rem:not-premise}
No OpenAI theorem or catalogue family is a premise.
No family proof is independently verified.

Oai282-A/B and Oai069-A do not make this interface a
fieldwise Ward identity or an ultraviolet completion.
Oai283-A is, at most, a comparison for a fixed finite
channel approximation interface.
Oai365-A supplies no metric derived from a certificate
tag.
Oai212-A, Family 265, Oai272, Oai276, Oai279, Oai227,
and Oai119 are not Page curves or entanglement tests
for this transport. Their documentary comparison
does not pass any causal-product gate.
\end{remark}

%=====================================================================
\section*{Declarations}
\addcontentsline{toc}{section}{Declarations}

\paragraph{Authorship.}
The author field is intentionally empty.
Citing N.~Cheung does not assign authorship of this
adaptation. Authorized authorship and submission
metadata must be supplied for a signed submission.

\paragraph{Source and hypothesis status.}
The source manuscripts are cited by identifier and
version. Analytical inputs are restated explicitly.
A source quotation, a documentary link, and a verified
same-operator identification are not interchangeable.

\paragraph{No overstated completion.}
The complete results are the proved interfaces,
distributional evaluation, algebraic criterion, and
conditional support bridge.
The missing time-ordered construction is not hidden
inside an assumption or declared complete by renaming
a free coefficient.

\paragraph{Operational status.}
Installed finite tables encode supplied data and status
records. No detector coupling to the continuum
functional, no acquisition of (TC), and no microscopic
implementation of the carriage permissions is derived.

\paragraph{Verification.}
The source uses conventional pdfLaTeX and an internal
bibliography. No successful compilation, machine check,
numerical execution, independent execution, hardware
synthesis, experimental implementation, independent
referee verification, or journal acceptance is asserted.

%=====================================================================
\begin{thebibliography}{99}
\addcontentsline{toc}{section}{References}

\bibitem{IXD}
N.~Cheung,
\emph{Landmark IX-D: Causal-support interfaces for one sharp
ordered word after construction of the declared partial
free product}.
\loc{IX-D-v3.tex}, version 3.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/IX-D}.
Especially \loc{thm:interfaces}, \loc{thm:support},
\loc{thm:nonlift}, \loc{lem:separation},
\loc{prop:contact}, \loc{prop:conditionalret},
\loc{lem:hbaraudit}, and \loc{thm:release}.

\bibitem{IXE}
N.~Cheung,
\emph{Landmark IX-E: Binary time ordering and causal subtraction
on the declared sharp comparison sector}.
\loc{IX-E.tex}, version 1.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/IX-E}.
Especially \loc{prop:geometry}, \loc{lem:spacelike},
\loc{prop:commutator}, \loc{thm:obstruction},
\loc{thm:algebraic}, and \loc{thm:subtraction}.

\bibitem{IXE2}
N.~Cheung,
\emph{Landmark IX-E-2: Exact imaginary part of the locked
Cauchy kernel and the first-stage commutator on the
retained two-way sector}.
\loc{IX-E-2.tex}, version 1.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/IX-E-2}.
Common-regulator subtraction, exact imaginary part,
strongly separated witness class, and support-bridge stop.

\bibitem{IXE3}
N.~Cheung,
\emph{Landmark IX-E-3: Functional support of the sharp insertion
and the two-way commutator bridge}.
\loc{IX-E-3.tex}, version 1.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/IX-E-3}.
Boundary-trace certificate, null-sphere lower support,
specified flat realization, solid-ball correction,
and inherited-operator identification boundary.

\bibitem{IXFreeTwo}
N.~Cheung,
\emph{Landmark IX-Free-2: Degree-four descent and overlap
agreement for one sharp ordered word}.
\loc{IX-Free-2.tex}, version 1.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/IX-Free-2}.
Inherited free partial product only.

\bibitem{IXCST}
\emph{IX-C-ST: A supported partial product for one sharp
ordered word}.
Supplied preceding combined adaptation of IX-C,
IX-Free, and IX-Free-2; author field empty.
Used only with its explicit analytical premises.
Its adjoint-trace statement requires the same-operator
audit in Section~\ref{sec:identification}.
No public registration or independent verification is
asserted.

\bibitem{IXAST}
\emph{IX-A-ST: Boundary-sensitive admission on a prescribed
conical Enter spacetime}.
Version 1 adaptation record.
Enter Calculus Companion.
\url{https://enter.grok.me/browse/IX-A-ST}.
Especially \loc{lem:saturation}, \loc{thm:separator},
\loc{thm:separate}, and \loc{thm:release}.
The inherited carrier is the adapted carrier.

\bibitem{IXB}
N.~Cheung,
\emph{Landmark IX-B}.
\loc{IX-B-v2.tex}, version 2.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/IX-B}.
Source-locked parent calibration under its VII-D premise.

\bibitem{VIID}
N.~Cheung,
\emph{Landmark VII-D: Strong finite part and conversion of the
regulated Cauchy-reflection triangle}.
\loc{VII-D.tex}, version 1.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/VII-D}.
Especially \loc{thm:finitepart} and \loc{thm:conversion}.
The ultraviolet estimate is inherited, not re-proved.

\bibitem{VIIC}
N.~Cheung,
\emph{Landmark VII-C: The mixed-Wick obstruction for the sharp
Cauchy sector}.
\loc{VII-C.tex}, version 1.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/VII-C}.
The logarithmic result and obstruction retain their
original joint hypotheses.

\bibitem{IB}
N.~Cheung,
\emph{I-B-v1: A Finite Enter Spacetime:
Calibrated Destructive Time Readout on a Prescribed
Conical Product}.
\loc{I-B-v1.tex}, version 1.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/I-B}.

\bibitem{EnterArticle}
N.~Cheung,
``The Enter Calculus: A Linear Quantum Lambda Calculus with
an Operational Characterization of Measurement,''
\emph{Frontiers in Physics} \textbf{14} (2026),
article 1954943.
Accepted manuscript record, accepted September 28, 2026.
DOI: \loc{10.3389/fphy.2026.1954943}.

\bibitem{EnterI}
N.~Cheung,
\emph{Manuscript I: Finite operational characterization
of destructive measurement in the Enter calculus}.
\loc{I.tex}, version 2.
Enter Calculus Companion, manuscript record.
\url{https://enter.grok.me/browse/I}.
Its structural class is not re-proved here.

\bibitem{EnterPhil}
N.~Cheung,
\emph{The Philosophy of Enter:
Destructive Readout, Quantum Recovery, and the Refusal
of Identification}.
\loc{EntPhil-v2.tex}, version 2.
Introductory essay, not a theorem premise.
\url{https://enter.grok.me/enter}.

\bibitem{FR}
K.~Fredenhagen and K.~Rejzner,
\emph{Perturbative algebraic quantum field theory}.
Lecture notes, version 2, 2013.
\url{https://arxiv.org/abs/1208.1428}.
Documentary comparison for regular time ordering and
renormalized extension, not existence for this sharp sector.

\bibitem{BF}
R.~Brunetti and K.~Fredenhagen,
``Microlocal analysis and interacting quantum field theories:
Renormalization on physical backgrounds,''
\emph{Communications in Mathematical Physics}
\textbf{208} (2000), 623--661.
\url{https://arxiv.org/abs/math-ph/9903028}.
Extension framework under its stated hypotheses;
not applied as an existence theorem for the missing map.

\bibitem{BGP}
C.~B\"ar, N.~Ginoux, and F.~Pf\"affle,
\emph{Wave Equations on Lorentzian Manifolds and Quantization}.
European Mathematical Society, 2007.
\url{https://arxiv.org/abs/0806.1036}.
Local and global Cauchy/Green-operator hypotheses are
kept distinct.

\bibitem{Watrous}
J.~Watrous,
\emph{The Theory of Quantum Information}.
Cambridge University Press, 2018.
Author manuscript and errata:
\url{https://cs.uwaterloo.ca/~watrous/TQI/}.

\bibitem{En09}
N.~Cheung,
\emph{En09-A: Relational Enter}.
Version 1, supplied manuscript record.
\url{https://enter.grok.me/browse/En09-A}.
Complete destructive-clock identity and conditioning
scope only.

\bibitem{En03}
N.~Cheung,
\emph{En03-A}.
Version 1, supplied manuscript record.
\url{https://enter.grok.me/browse/En03-A}.
Finite scheduled support and separately supplied
geometric interfaces.

\bibitem{En08}
N.~Cheung,
\emph{En08-A} and \emph{En08-B}.
Version 1, supplied manuscript records.
\url{https://enter.grok.me/browse/En08-A};
\url{https://enter.grok.me/browse/En08-B}.
Scheduler/cone separation and transport relative to a
prescribed null boundary.

\bibitem{STInterfaces}
\emph{VIII-ST} and \emph{VII-J-ST}.
Version 1 adaptation records.
Enter Calculus Companion.
\url{https://enter.grok.me/browse/VIII-ST};
\url{https://enter.grok.me/browse/VII-J-ST}.
Fixed-host and operational interface comparisons only.

\bibitem{OperationalRecords}
N.~Cheung,
\emph{VII-E}, \emph{VII-F},
\emph{VIII-A}, \emph{VIII-B}, \emph{VIII-C},
\emph{En05-A}, and \emph{En10-A}.
Version-qualified supplied records in the
Enter Calculus Companion.
Observation boundaries, matching, scheduled locality,
and source-weight acquisition are separate contracts.
\url{https://enter.grok.me/browse}.

\bibitem{BoundaryRecords}
N.~Cheung,
\emph{VII-H} and \emph{VII-I}, version 1;
\emph{Em01-B} and \emph{Em01-C}, version 3;
\emph{XIV-H}, \emph{XIV-I}, and \emph{XIV-J}, version 1;
technical \emph{XV-B}, version 2;
\emph{XVI-N}, revision r12;
\emph{XVI-O}, revision o70-sync.
Supplied manuscript records, Enter Calculus Companion.
Documentary boundaries, not analytical inputs replacing
the missing causal extension.
\url{https://enter.grok.me/browse}.

\end{thebibliography}

\end{document}