% !TEX program = pdflatex
%=====================================================================
% IX-Free-2.tex
%
% Standalone pdfLaTeX source. No external bibliography is required.
%
% Suggested build:
%   pdflatex -interaction=nonstopmode -halt-on-error IX-Free-2.tex
%   pdflatex -interaction=nonstopmode -halt-on-error IX-Free-2.tex
%
% RELEASE: CONSTRUCTED, relative to the explicitly stated inherited
% carrier, graph, calibration, and old-product premises.
%
% New proofs:
%   * restricted sharp-generator separation;
%   * injectivity of the degree-four presentation maps;
%   * descent of the four prescribed degree-four coefficients;
%   * an explicit nonzero boundary-charge witness for every nonzero f;
%   * separation from both partial-contraction spaces and the old
%     microcausal algebra;
%   * simultaneous gluing of all declared new and old domains;
%   * evaluation of C_glue as R;
%   * wordwise coherence through hbar^3 and partial-product reversal;
%   * fixed-support test-family continuity.
%
% Important boundaries:
%   * no actual-stage continuity or quantum hypocontinuity;
%   * no associativity assertion for unspecified triples;
%   * no global quantum algebra, causal lift, IX-D, or G2 opening;
%   * inherited companion results are premises, not independently
%     reverified proofs.
%
% Compilation, proof-assistant verification, and independent review
% have not been executed or claimed.
%=====================================================================

\documentclass[11pt,a4paper]{article}

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

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

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\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{\R}{\mathbb R}
\newcommand{\C}{\mathbb C}
\newcommand{\dd}{\,\mathrm d}
\newcommand{\supp}{\operatorname{supp}}
\newcommand{\WF}{\operatorname{WF}}
\newcommand{\Span}{\operatorname{span}}
\newcommand{\Sym}{\operatorname{Sym}}
\newcommand{\kerop}{\operatorname{ker}}
\newcommand{\ord}{\operatorname{ord}}
\newcommand{\id}{\operatorname{id}}
\newcommand{\cl}{\operatorname{cl}}
\newcommand{\Dtest}{\mathcal D}
\newcommand{\Eprime}{\mathcal E'}
\newcommand{\Ddir}{\mathrm D}
\newcommand{\Padm}{\mathscr P_\Sigma}
\newcommand{\Pdist}{\mathscr P_{\mathrm{dist}}}
\newcommand{\Pmc}{\mathscr P_{\mathrm{mc}}}
\newcommand{\taus}{\tau_\Sigma}
\newcommand{\Slin}{\mathscr S_1}
\newcommand{\Mlin}{\mathscr M_1}
\newcommand{\Qlin}{\mathscr Q_\Sigma}
\newcommand{\Ezero}{\mathsf E_0}
\newcommand{\GA}{G_{\mathrm A}^{0}}
\newcommand{\Charge}{\mathsf b}
\newcommand{\pair}[2]{\left\langle #1,#2\right\rangle}
\newcommand{\Tspace}{\mathcal T}
\newcommand{\Bspace}{\mathscr B}
\newcommand{\Wspace}{\mathscr W}
\newcommand{\PLspace}{\mathscr L_4}
\newcommand{\QLspace}{\mathscr L_2}
\newcommand{\PRspace}{\mathscr R_4}
\newcommand{\QRspace}{\mathscr R_2}
\newcommand{\Lspace}{\mathscr L}
\newcommand{\Rspace}{\mathscr R}
\newcommand{\EL}{\mathcal E_L}
\newcommand{\ER}{\mathcal E_R}
\newcommand{\Graph}{\mathsf G}
\newcommand{\Cal}{\mathcal N_c}
\newcommand{\Cdesc}{\mathcal C_{\mathrm{desc}}}
\newcommand{\Cglue}{\mathcal C_{\mathrm{glue}}}
\newcommand{\Rtr}{\C[\hbar]/(\hbar^4)}
\newcommand{\Vmod}{\Padm\otimes_\C\Rtr}
\newcommand{\Dfirst}{D_{\mathrm{first}}}
\newcommand{\Dsecond}{D_{\mathrm{second}}}
\newcommand{\Dold}{D_{\mathrm{old}}}
\newcommand{\Dnew}{D_{\mathrm{new}}}
\newcommand{\Ddecl}{D_{\mathrm{decl}}}
\newcommand{\Dformal}{\widehat D_{\mathrm{decl}}}

\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{Landmark IX-Free-2}\\[0.4em]
Degree-four descent and overlap agreement\\
for one sharp ordered word}
\author{}
\date{}

\usepackage{tikz}
\begin{document}
\maketitle

\begin{abstract}
We complete the algebraic descent and overlap tests left open in
IX-Free for the ordered word \(B_f,W_g,B_{f'}\). The previously
constructed graph outputs are used as inherited values.

A compact spatial-diagonal metric direction, obtained by applying
the wave operator to a test tensor, proves sharp-generator
separation even when the \(00\)-metric component is constrained to
vanish. Slot isolation then proves injectivity of both degree-four
presentation maps. Consequently all four prescribed degree-four
coefficients descend to actual functionals.

An explicit advanced-trace witness proves that every nonzero sharp
generator has nonzero intrinsic metric-derivative charge at some
smooth configuration. The partial contractions have zero charge.
The old microcausal algebra also has zero charge: a nonzero boundary
coefficient would produce a timelike conormal singularity.
These facts eliminate the live new-domain intersection and separate
the sharp space from the old algebra. An algebraic anchored-domain
lemma eliminates the old overlap of the entire new-domain sum,
including possible multi-domain relations.

For every real common parent parameter, the prescriptions therefore
glue to one truncated partial product preserving the locked first
stages and the old product. The two associations of the selected
word agree through order \(\hbar^3\). Reversal, presentation
independence, and fixed-support test-family continuity hold.
Actual-stage continuity, associativity on unspecified triples,
and the IX-D and G2 constructions are not asserted.
\end{abstract}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[x=1cm,y=1cm]
\node[draw,rounded corners,align=center,text width=3.15cm,font=\small,inner sep=3pt] (a) at (0,0) {Named tensor domain};
\node[draw,rounded corners,align=center,text width=3.15cm,font=\small,inner sep=3pt] (b) at (5,0) {Truncated partial product};
\node[draw,rounded corners,align=center,text width=3.15cm,font=\small,inner sep=3pt] (c) at (10,0) {Absolute time-ordered product};
\node[draw,dashed,rounded corners,align=center,text width=9.6cm,font=\small,inner sep=3pt] (s) at (5,-2.35) {The product is relative to the inherited premises.};
\draw[->] (a) -- (b);
\draw[->] (b) -- (c);
\draw[->] (b) -- (s);
\end{tikzpicture}
\caption{One partial product stays relative. The three boxes name objects this manuscript keeps separate. The dashed box is the stated stop. Not a proof, and not an admission of a quantum coefficient.}
\label{fig:scope-IX-Free-2}
\end{figure}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[x=1cm,y=1cm]
\node[draw,rounded corners,align=center,text width=4.3cm,font=\small,inner sep=3pt] (a) at (0,0) {Named tensor domain};
\node[draw,rounded corners,align=center,text width=4.3cm,font=\small,inner sep=3pt] (b) at (6.4,0) {Absolute time-ordered product};
\node[draw,dashed,rounded corners,align=center,text width=9.6cm,font=\small,inner sep=3pt] (s) at (3.2,-2.35) {The product is relative to the inherited premises.};
\draw[->] (a) -- (s);
\draw[->] (b) -- (s);
\end{tikzpicture}
\caption{One partial product stays relative. The boxes name objects this manuscript keeps separate. The dashed box is the stated stop. Not a proof, and not an admission of a quantum coefficient.}
\label{fig:split-IX-Free-2}
\end{figure}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[x=1cm,y=1cm]
\node[draw,rounded corners,align=center,text width=7.2cm,font=\small,inner sep=3pt] (a) at (0,0) {Named tensor domain};
\node[draw,rounded corners,align=center,text width=7.2cm,font=\small,inner sep=3pt] (b) at (0,-1.7) {Truncated partial product};
\node[draw,rounded corners,align=center,text width=7.2cm,font=\small,inner sep=3pt] (c) at (0,-3.4) {Absolute time-ordered product};
\node[draw,dashed,rounded corners,align=center,text width=7.2cm,font=\small,inner sep=3pt] (s) at (0,-5.2) {The product is relative to the inherited premises.};
\draw[->] (a) -- (b);
\draw[->] (b) -- (c);
\draw[->] (c) -- (s);
\end{tikzpicture}
\caption{Reading downward is not a transfer. The boxes name objects this manuscript keeps separate. The dashed box is the stated stop. Not a proof, and not an admission of a quantum coefficient.}
\label{fig:chain-IX-Free-2}
\end{figure}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[x=1cm,y=1cm]
\node[draw,rounded corners,align=center,text width=4.2cm,font=\small,inner sep=3pt] (a) at (0,0) {Named tensor domain};
\node[align=center,font=\small] (m) at (5.2,0) {not the same object};
\node[draw,rounded corners,align=center,text width=4.2cm,font=\small,inner sep=3pt] (b) at (10.4,0) {Absolute time-ordered product};
\node[draw,dashed,rounded corners,align=center,text width=9.6cm,font=\small,inner sep=3pt] (s) at (5.2,-2.35) {Truncated partial product. The product is relative to the inherited premises.};
\draw (a) -- (m);
\draw (m) -- (b);
\draw[->] (m) -- (s);
\end{tikzpicture}
\caption{Named tensor domain is not Absolute time-ordered product. The boxes name objects this manuscript keeps separate. The dashed box is the stated stop. Not a proof, and not an admission of a quantum coefficient.}
\label{fig:pair-IX-Free-2}
\end{figure}

\begin{figure}[ht]
\centering
\begin{tikzpicture}[x=1cm,y=1cm]
\node[draw,rounded corners,align=center,text width=3.15cm,font=\small,inner sep=3pt] (a) at (0,0) {Named: Named tensor domain};
\node[draw,rounded corners,align=center,text width=3.15cm,font=\small,inner sep=3pt] (b) at (5,0) {Used here: Truncated partial product};
\node[draw,rounded corners,align=center,text width=3.15cm,font=\small,inner sep=3pt] (c) at (10,0) {Not claimed: Absolute time-ordered product};
\node[draw,dashed,rounded corners,align=center,text width=9.6cm,font=\small,inner sep=3pt] (s) at (5,-2.5) {The product is relative to the inherited premises.};
\draw[->] (a) -- (b);
\draw[->] (b) -- (c);
\draw[->] (b) -- (s);
\end{tikzpicture}
\caption{Three statuses stay separate. The boxes name objects this manuscript keeps separate. The dashed box is the stated stop. Not a proof, and not an admission of a quantum coefficient.}
\label{fig:gate-IX-Free-2}
\end{figure}

Figure~\ref{fig:split-IX-Free-2} records one view of the same separation. Figure~\ref{fig:chain-IX-Free-2} records one view of the same separation. Figure~\ref{fig:pair-IX-Free-2} records one view of the same separation. Figure~\ref{fig:gate-IX-Free-2} records one view of the same separation. The drawings add no hypothesis.


Figure~\ref{fig:scope-IX-Free-2} records that separation.
The drawing adds no hypothesis.



\scopebox{Release and scope}{%
\textbf{Release: Constructed, relative to the inherited premises
stated below.}
The result is one truncated partial product on an explicitly named
tensor domain, together with coherence for the single ordered word
\(A=B_f,\ W=W_g,\ C=B_{f'}\).

No graph-existence or triangle-calibration proof is reconstructed.
No Einstein equation, time-ordered product, retarded product,
global quantum algebra, causal-support lift, IX-D construction,
or G2 opening is included.}

\tableofcontents

%=====================================================================
\section{Release alternatives and inherited contract}
\label{sec:contract}
%=====================================================================

The release alternatives are kept distinct:
\begin{enumerate}
\item \emph{Constructed}: the prescribed coefficients descend and
glue with all declared existing coefficients, satisfying the copied
interfaces on the named sector.
\item \emph{Canonical prescription obstructed}: an explicit
actual-presentation relation or overlap discrepancy contradicts the
prescribed coefficients.
\item \emph{Contract proved obstructed}: a contradiction excludes
every coefficient system satisfying the copied interfaces.
\item \emph{Unresolved}: a required proof remains unfinished.
\end{enumerate}
A missing proof is not an obstruction. Failure of one prescription
is not a universal contract obstruction.

Fix one real parent parameter \(c\) at the outset. It is not changed
by association, presentation, or observation descendant. The
results below hold for every such fixed \(c\).

\subsection{Geometry and smooth operators}

Let
\[
M=\R^{1+3},\qquad M_+=\{t>0\},\qquad
\Sigma=\{t=0\},\qquad X=M_+^3,
\]
with metric
\[
\eta=\operatorname{diag}(-1,1,1,1),\qquad
\Box=-\partial_t^2+\Delta_{\mathbf x}.
\]
Metric configurations are smooth symmetric covariant tensors.
Set
\begin{equation}
(Ch)^\mu
=\partial_\nu h^{\mu\nu}
-\frac12\partial^\mu(\eta^{\alpha\beta}h_{\alpha\beta}),
\qquad
L=\Ezero C,\qquad w=Lh.
\label{eq:C}
\end{equation}
The operator \(\Ezero\) is the inverse of \(\Box\) with zero
Cauchy value and zero first time derivative at \(t=0\).
The operator \(\GA\) is the componentwise advanced inverse
of the same massless wave operator.

All configurations and directions are smooth and off shell.
Compact directions supported in \(M_+\) are allowed. We use the
usual smooth mapping properties, Cauchy uniqueness, and finite
propagation of these fixed linear operators.

With
\[
\Tspace=C_c^\infty(M_+;\C),
\]
the generators are
\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}
Complex tests define complex-valued functionals on real smooth
configurations. Complexified directions can equivalently be used
by multilinearity.

\subsection{Explicit inherited premises}

The supplied IX-Free source is used through the following ledger.
Statements reported there from companion manuscripts remain
inherited premises, not independently certified companion proofs.

\begin{assumption}[Carrier, charge, and classical operations]
\label{ass:carrier}
The carrier \(\Padm\) consists of actual finite polynomial
functionals with compact symmetric distributional kernels,
subject to
\begin{equation}
(\Ddir_{\boldsymbol\eta}F)'_h(\psi)\in\Slin
=\Mlin+\Qlin
\label{eq:admission}
\end{equation}
for every smooth configuration \(\psi\) and every finite list
of smooth configuration directions \(\boldsymbol\eta\).

The linear sharp kernels and intrinsic charge are
\[
q_a=L^*a=C^*(\theta\GA a),\qquad
\Qlin=\{q_a:a\in C_c^\infty(M_+;T^*M)_\C\},
\]
\begin{equation}
\Charge(m+q_a)=(\GA a)|_\Sigma.
\label{eq:charge}
\end{equation}
The charge is well defined on actual linear kernels and vanishes
on \(\Mlin\). Every element of \(\Mlin\) has no nonzero
nonspacelike wavefront covector; compact smooth metric kernels
belong to \(\Mlin\).

The sharp adjoint retains its surface term:
\begin{equation}
C^*(\theta b)
=\theta C^*b+\delta(t)\mathcal B(b|_\Sigma).
\label{eq:boundary}
\end{equation}
Classical multiplication, smooth directional differentiation,
and conjugation preserve \(\Padm\). Classical multiplication
is separately continuous in the locally convex topology \(\taus\),
which records strong compact-distribution coefficients and all
intrinsic trace coordinates.

The generating test maps are injective and have fixed-support
test-family continuity. The inherited nonconvergence
\(B_{f,\varepsilon}\not\to B_f\) in \(\taus\) for nonzero real \(f\)
is retained, but is not used as a charge witness.
\end{assumption}

\begin{assumption}[Old microcausal product]
\label{ass:old}
The full old compact polynomial microcausal algebra \(\Pmc\)
is included in \(\Padm\). Its functional derivatives satisfy
the standard microcausal wavefront condition: no nonzero joint
covector is entirely future causal or entirely past causal,
where zero individual covectors are allowed in those closed
causal cones.

The inherited old product \(\star_H\) is defined on
\(\Pmc\otimes\Pmc\), has classical order zero, and has its
unchanged coefficients
\[
C_j^H:\Pmc\otimes\Pmc\longrightarrow\Pmc,
\qquad 0\le j\le3.
\]
For the reversal statement we use the inherited Hermitian
old convention
\[
C_j^H(G^*,F^*)=C_j^H(F,G)^*.
\]
No new continuity property of \(\star_H\) is introduced.
\end{assumption}

The microcausal condition just specified is the usual
functional-derivative condition; see \cite{FR}. We will prove
the zero-charge consequence needed here, rather than infer it
from the informal word ``bulk.''

\begin{assumption}[Locked stages and inherited graph outputs]
\label{ass:graphs}
The fixed mixed kernel \(K\) has
\(\supp K=M_+^2\). The first stages are the actual maps
\begin{align}
B_f\star_1W_g&=B_fW_g+\hbar\mathcal Q_{f,g},
&
\mathcal Q_{f,g}
&=-2\pair{f(x)g(y)K(x,y)}
{\partial_t\phi(x)h_{00}(y)},
\label{eq:firstL}\\
W_g\star_1B_{f'}&=W_gB_{f'}+\hbar\mathcal Q^R_{g,f'},
&
\mathcal Q^R_{g,f'}
&=-2\pair{g(y)f'(x')\overline{K(x',y)}}
{h_{00}(y)\partial_{t'}\phi(x')}.
\label{eq:firstR}
\end{align}
Their metric derivatives are compact smooth kernels, also
after the required directional insertions.

Write
\[
S_{\mu\nu}(x,x')
=\partial_\mu^x\partial_\nu^{x'}\Delta_m^+(x-x')
\]
for the fixed scalar contraction kernel, and
\[
\mathcal T_{f,f'}
=\pair{f(x)f'(x')S_{\mu\nu}(x,x')}
{w^\mu(x)w^\nu(x')}.
\]
The three one-edge outputs
\begin{equation}
\Graph_{12}=\mathcal Q_{f,g}B_{f'},\qquad
\Graph_{23}=B_f\mathcal Q^R_{g,f'},\qquad
\Graph_{13}=\mathcal T_{f,f'}W_g
\label{eq:oneedges}
\end{equation}
exist and belong to \(\Padm\).

For \(V=f\otimes g\otimes f'\), the three two-edge values are
the already defined and admitted functionals
\begin{align}
\Graph_{12,23}
&=2\pair{V K(x,y)\overline{K(x',y)}}
{\partial_t\phi(x)\partial_{t'}\phi(x')},
\label{eq:G1223}\\
\Graph_{12,13}
&=2\pair{V K(x,y)S_{0\nu}(x,x')}
{h_{00}(y)w^\nu(x')},
\label{eq:G1213}\\
\Graph_{13,23}
&=2\pair{V S_{\mu0}(x,x')\overline{K(x',y)}}
{w^\mu(x)h_{00}(y)}.
\label{eq:G1323}
\end{align}
Their defining wavefront products, compact coefficient kernels,
admission decompositions, and all required descendants have
already been established in IX-Free. Their fixed-support
test-family continuity is inherited.

The maps \(q_L,q_R\) defined below are injective. The inherited
degree-two second-stage maps are
\begin{align}
L_1(\mathcal Q_{f,g},B_{f'})
&=\Graph_{12,23}+\Graph_{12,13},
&
L_2(\mathcal Q_{f,g},B_{f'})
&=\Cal(f,g,f')\,1,
\label{eq:degree2L}\\
R_1(B_f,\mathcal Q^R_{g,f'})
&=\Graph_{12,23}+\Graph_{13,23},
&
R_2(B_f,\mathcal Q^R_{g,f'})
&=\Cal(f,g,f')\,1.
\label{eq:degree2R}
\end{align}
They are maps on actual arguments, with inherited reversal
and presentation independence.
\end{assumption}

\begin{assumption}[One calibrated parent]
\label{ass:parent}
Fix the inherited regulator and scale. The calibrated distributions
\(u_\mu^\rho,r\in\Dtest'(X)\) exist under the analytical premise
explicitly reported in IX-Free. For the one fixed real parameter
\(c\), set
\begin{equation}
U_c=u_\mu^\rho+cr,\qquad
\Cal(f,g,f')=\pair{U_c}{f\otimes g\otimes f'}.
\label{eq:parent}
\end{equation}
The parent has dagger symmetry under conjugation and exchange
of \(x,x'\), and its declared numerical observation operations
use this same parameter. Algebraic scalar descent has already
been evaluated:
\[
\Cdesc=\R.
\]
The scalar family has inherited fixed-support continuity.
No claim about arbitrary nonconstant contact terms follows
from this scalar calibration.
\end{assumption}

The sign ledger is unchanged: each first-stage partial has factor
\(-2\); the complete word has two sharp insertion signs, whose
product is \(+1\); the middle-slot assignment factor is \(2\),
not \(4\).

\subsection{Copied interfaces}

\begin{requirement}[C-I1--C-I9]
\label{req:interfaces}
The construction must satisfy:
\begin{enumerate}[label=\textbf{C-I\arabic*.}]
\item Every output is admitted, including the required metric
derivatives and directional descendants.
\item Order zero is classical multiplication.
\item Every specified old-product overlap agrees with \(\star_H\).
\item The first stages are locked to
\eqref{eq:firstL}--\eqref{eq:firstR}.
\item The constant kernel is \(U_c\), using one real common parent
parameter and its declared observation compatibility.
\item No subtraction changes a fixed old product.
\item Unchanged approximants need not converge sharply in \(\taus\).
\item All finite relations between actual presentations are respected.
\item Every continuity claim has a named domain and proof;
test-family continuity is not actual-stage hypocontinuity.
\end{enumerate}
\end{requirement}

\begin{center}
\small
\renewcommand{\arraystretch}{1.12}
\begin{tabularx}{\linewidth}{@{}p{.34\linewidth}p{.22\linewidth}X@{}}
\toprule
Object & Entering status & Present obligation\\
\midrule
First stages and one-edge outputs &
Constructed, inherited &
Retain their values\\
Two-edge outputs and admission &
Constructed in IX-Free &
Use, do not reconstruct\\
\(q_L,q_R\), degree-two maps &
Constructed in IX-Free &
Overlap agreement\\
\(\Cdesc\) &
Evaluated as \(\R\) &
Do not reopen\\
\(\kerop p_L,\kerop p_R\) &
Concrete, unevaluated &
Evaluate the kernels\\
Degree-four coefficients &
Values admitted; descent open &
Actual-functional descent\\
Live degree-two intersection &
Unevaluated &
Separate its factors\\
Old and sum-domain overlaps &
Unevaluated &
Simultaneous gluing\\
F9a &
Constructed for inherited families &
Extend to degree-four families\\
F9b &
Unclaimed &
No assertion here\\
\bottomrule
\end{tabularx}
\end{center}

%=====================================================================
\section{Actual spaces, declared domain, and coefficient assignment}
\label{sec:domains}
%=====================================================================

All spans and tensor products in this paper are algebraic over
\(\C\). Define
\[
\Bspace=\Span\{B_f:f\in\Tspace\},\qquad
\Wspace=\Span\{W_g:g\in\Tspace\},
\]
\[
\PLspace=\Span\{B_fW_g\},\qquad
\QLspace=\Span\{\mathcal Q_{f,g}\},
\]
\[
\PRspace=\Span\{W_gB_{f'}\},\qquad
\QRspace=\Span\{\mathcal Q^R_{g,f'}\},
\]
and
\[
\Lspace=\PLspace\oplus\QLspace,\qquad
\Rspace=\PRspace\oplus\QRspace.
\]
These last sums are direct by total field degree. The actual
spaces \(\PLspace,\PRspace\) coincide, but their ordered roles
remain distinct.

Let
\[
\EL=\Tspace\otimes\Tspace,\qquad
\ER=\Tspace\otimes\Tspace,
\]
with ordered presentation maps
\[
p_L(f\otimes g)=B_fW_g,\qquad
q_L(f\otimes g)=\mathcal Q_{f,g},
\]
\[
p_R(g\otimes f')=W_gB_{f'},\qquad
q_R(g\otimes f')=\mathcal Q^R_{g,f'}.
\]

Inside \(\Padm\otimes\Padm\), the declared domains are
\begin{align}
\Dfirst
&=(\Bspace\otimes\Wspace)+(\Wspace\otimes\Bspace),
\label{eq:Dfirst}\\
\Dsecond
&=(\Lspace\otimes\Bspace)+(\Bspace\otimes\Rspace),
\label{eq:Dsecond}\\
\Dnew&=\Dfirst+\Dsecond,
&
\Dold&=\Pmc\otimes\Pmc,
\label{eq:Dnewold}\\
\Ddecl&=\Dnew+\Dold.
\label{eq:Ddecl}
\end{align}
Thus the full inherited old domain is used, not a smaller
regular subdomain.

We will define coefficient maps
\[
C_j:\Ddecl\longrightarrow\Padm,\qquad 0\le j\le3.
\]
Their prescribed restrictions are displayed below.
On the degree-four rows, \(L_j,R_j\) initially denote the
labelled prescriptions; their actual descent is proved in
Section~\ref{sec:descent}.

\begin{center}
\small
\renewcommand{\arraystretch}{1.2}
\begin{tabularx}{\linewidth}{@{}p{.27\linewidth}p{.24\linewidth}X p{.08\linewidth}@{}}
\toprule
Domain & \(C_1\) & \(C_2\) & \(C_3\)\\
\midrule
\(\Bspace\otimes\Wspace\) &
\(\mathcal Q_{f,g}\) &
\(0\) & \(0\)\\
\(\Wspace\otimes\Bspace\) &
\(\mathcal Q^R_{g,f'}\) &
\(0\) & \(0\)\\
\(\PLspace\otimes\Bspace\) &
\(L_1\) &
\(L_2\) & \(0\)\\
\(\Bspace\otimes\PRspace\) &
\(R_1\) &
\(R_2\) & \(0\)\\
\(\QLspace\otimes\Bspace\) &
\(\Graph_{12,23}+\Graph_{12,13}\) &
\(\Cal(f,g,f')\,1\) & \(0\)\\
\(\Bspace\otimes\QRspace\) &
\(\Graph_{12,23}+\Graph_{13,23}\) &
\(\Cal(f,g,f')\,1\) & \(0\)\\
\(\Dold\) &
\(C_1^H\) &
\(C_2^H\) & \(C_3^H\)\\
\bottomrule
\end{tabularx}
\end{center}

On every row,
\[
C_0(F\otimes G)=FG.
\]
The explicit zero entries are part of the selected contraction
prescription. They are not a classification excluding every
alternative contact term.

%=====================================================================
\section{The concrete degree-four relation kernel}
\label{sec:relations}
%=====================================================================

For
\[
v=\sum_i\alpha_i f_i\otimes g_i\in\EL,
\qquad
v(x,y)=\sum_i\alpha_i f_i(x)g_i(y),
\]
use the inherited injective realization of this algebraic tensor
product as smooth compact joint functions.

Let \(J^\mu_{\alpha\beta}(x,z)\) be the distribution kernel of \(L\),
and let \(e_{00}^{\alpha\beta}h_{\alpha\beta}=h_{00}\).
The relation kernel is copied unchanged:
\begin{equation}
\begin{split}
\mathsf P[v](x,z_1,z_2,z_3)
={}&\Sym_{(z_i,\alpha_i,\beta_i)}
\partial_\mu^x\Big[
v(x,z_2)J^\mu_{\alpha_1\beta_1}(x,z_1)
\\
&\qquad\qquad{}\times
\delta(z_2-z_3)e_{00}^{\alpha_2\beta_2}
e_{00}^{\alpha_3\beta_3}
\Big].
\end{split}
\label{eq:P}
\end{equation}
The symmetrization is the average over the three metric slots.
IX-Free establishes
\begin{equation}
p_L(v)
=\pair{\mathsf P[v]}
{\phi(x)h(z_1)h(z_2)h(z_3)},
\qquad
p_L(v)=0\ \Longleftrightarrow\ \mathsf P[v]=0.
\label{eq:Prelation}
\end{equation}
For \(v_R(y,x')\), set
\(\widetilde v(x',y)=v_R(y,x')\). The right relation is
\[
p_R(v_R)=0\ \Longleftrightarrow\ \mathsf P[\widetilde v]=0.
\]

Full coefficient recovery uses one scalar derivative and three
metric derivatives. The metric polarization factor is \(3!\).
Two metric derivatives do not recover this coefficient.

The prescribed values whose descent remains to be proved are
\begin{align}
\lambda^L_1(f,g,f')
&=\Graph_{13}+\Graph_{23},
&
\lambda^L_2(f,g,f')
&=\Graph_{13,23},
\label{eq:lambdaL}\\
\lambda^R_1(f,g,f')
&=\Graph_{12}+\Graph_{13},
&
\lambda^R_2(f,g,f')
&=\Graph_{12,13}.
\label{eq:lambdaR}
\end{align}
They descend precisely when
\begin{equation}
\lambda^L_j((\kerop p_L)\otimes\Tspace)=0,
\qquad
\lambda^R_j(\Tspace\otimes(\kerop p_R))=0,
\qquad j=1,2.
\label{eq:annihilation}
\end{equation}

We now evaluate the kernels. No inference from injectivity of
\(q_L,q_R\) will be used.

%=====================================================================
\section{Gate K: restricted sharp separation and kernel evaluation}
\label{sec:kernel}
%=====================================================================

The restricted separation lemma can be proved without a general
range theorem for \(C\).

\begin{lemma}[Restricted sharp-generator separation]
\label{lem:restricted}
Let \(f\in\Tspace\). Suppose
\[
B_f[k,\varphi]=0
\]
for every smooth symmetric metric direction \(k\) with \(k_{00}=0\)
and every smooth scalar \(\varphi\). Then \(f=0\).
It is enough to use compact metric directions supported in \(M_+\).
\end{lemma}

\begin{proof}
For \(\chi\in C_c^\infty(M_+)\), let \(H\) have its only nonzero
component
\[
H_{11}=\chi,
\qquad k=\Box H.
\]
Then \(k_{00}=0\). Because \(C\) has constant coefficients,
\[
Ck=\Box(CH).
\]
The vector \(CH\) is compactly supported away from \(\Sigma\),
so has zero Cauchy data there. Cauchy uniqueness gives
\begin{equation}
Lk=\Ezero\Box(CH)=CH.
\label{eq:compactinverse}
\end{equation}
Directly from \eqref{eq:C},
\[
(CH)^0=\frac12\partial_t\chi,\quad
(CH)^1=\frac12\partial_1\chi,\quad
(CH)^2=-\frac12\partial_2\chi,\quad
(CH)^3=-\frac12\partial_3\chi.
\]

Choose \(\varphi=t\). This is an allowed smooth configuration.
Alternatively, use a compact smooth scalar agreeing with \(t\)
near \(\supp f\). The hypothesis becomes
\[
0=B_f[k,t]=-\frac12\int f(x)\partial_t\chi(x)\dd^4x
\]
for every \(\chi\). Hence \(\partial_t f=0\).
A smooth function independent of \(t\) on \(M_+\) and compactly
supported there must vanish. Thus \(f=0\).

Real \(\chi\) already suffice for complex \(f\), by applying the
distributional identity to its real and imaginary parts.
\end{proof}

The test direction \(k=\Box H\) is off shell. Equation
\eqref{eq:compactinverse} is an identity for the fixed Cauchy
inverse on compact zero-data tests, not an equation-of-motion
restriction on configurations.

\begin{theorem}[Injectivity of the degree-four presentations]
\label{thm:pinjective}
The maps
\[
p_L:\EL\longrightarrow\PLspace,\qquad
p_R:\ER\longrightarrow\PRspace
\]
are linear isomorphisms onto their actual-functional images.
In particular,
\[
\kerop p_L=\kerop p_R=\{0\}.
\]
\end{theorem}

\begin{proof}
Suppose \(p_L(v)=0\). Choose metric directions \(k,a,b\) with
\[
k_{00}=0,\qquad a_{00}=u,\qquad b_{00}=z,
\]
where \(u,z\in C_c^\infty(M_+)\); the other components of \(a,b\)
may be zero. Differentiate once in a scalar direction
\(\varphi\) and three times in these metric directions at the
zero configuration.

Using the unsymmetrized functional expression,
\[
p_L(v)[h,\phi]
=-\int v(x,y)(Lh)^\mu(x)\partial_\mu\phi(x)h_{00}(y)^2
\dd^4x\dd^4y,
\]
the only surviving terms place \(k\) in the \(Lh\)-slot.
Consequently the derivative is exactly
\begin{equation}
-2\int v(x,y)(Lk)^\mu(x)\partial_\mu\varphi(x)
u(y)z(y)\dd^4x\dd^4y.
\label{eq:isolation}
\end{equation}
The factor \(2\) is the surviving permutation count after
\(k_{00}=0\); it is consistent with the \(3!\) recovery of
the fully symmetric coefficient.

Define
\[
f_{u,z}(x)=\int v(x,y)u(y)z(y)\dd^4y.
\]
It is a smooth compact test. Since \eqref{eq:isolation} vanishes
for all \(k,\varphi\), Lemma~\ref{lem:restricted} gives
\(f_{u,z}=0\) for every \(u,z\).

For any \(d\in C_c^\infty(M_+)\), take \(u=d\) and choose \(z\)
equal to one near \(\supp d\). Then
\[
\int v(x,y)d(y)\dd^4y=0
\]
for every \(x\). Thus every \(y\)-test contraction of \(v\)
vanishes, so \(v=0\) as a joint smooth function and hence as an
algebraic tensor.

The right map is the same classical product after
\(v_R\mapsto\widetilde v\). Therefore its kernel is also zero.
Surjectivity onto the named images is their definition.
\end{proof}

\begin{corollary}[Evaluation of the copied relation equation]
\label{cor:Pevaluated}
For the algebraic presentation tensors of this paper,
\[
\mathsf P[v]=0\quad\Longleftrightarrow\quad v=0.
\]
The exchanged right equation has the same conclusion.
\end{corollary}

\begin{proof}
Combine \eqref{eq:Prelation} with
Theorem~\ref{thm:pinjective}.
\end{proof}

The conclusion concerns this particular polynomial product.
It is not the false general principle that products of injective
linear generating maps are automatically tensor-injective.

%=====================================================================
\section{Gate A: degree-four descent}
\label{sec:descent}
%=====================================================================

\begin{theorem}[Descended degree-four coefficient maps]
\label{thm:degree4}
The four prescriptions \eqref{eq:lambdaL}--\eqref{eq:lambdaR}
define unique algebraic bilinear maps
\[
L_j:\PLspace\times\Bspace\longrightarrow\Padm,
\qquad
R_j:\Bspace\times\PRspace\longrightarrow\Padm,
\qquad j=1,2,
\]
with the prescribed values.
\end{theorem}

\begin{proof}
Theorem~\ref{thm:pinjective} makes both relation kernels zero.
Thus all four annihilation tests \eqref{eq:annihilation} hold.

More explicitly, an element of \(\PLspace\) has a unique
presentation tensor in \(\EL\), and an element of \(\Bspace\)
has a unique sharp test. The graph prescriptions are linear
in that tensor and in the additional test. They therefore
define unique bilinear maps on the actual images. The same
argument applies on the right.

Their values are finite sums of inherited admitted graphs,
so belong to \(\Padm\), including the required admission
descendants. Classical multiplication defines \(L_0,R_0\).
\end{proof}

No operation on an unproved ``zero graph factor'' is used.
Linearity becomes sufficient only after the relevant actual
presentation kernel has been evaluated as zero.

%=====================================================================
\section{Gate S: boundary-charge separation}
\label{sec:charge}
%=====================================================================

We first justify the zero-charge property of the old algebra
using only its microcausal definition and the copied sharp
boundary identity.

\subsection{Nonzero charge forces a timelike boundary singularity}

For the component convention in \eqref{eq:C}, integration by parts
gives
\[
(C^*b)^{\alpha\beta}
=-\partial^{(\alpha}b^{\beta)}
+\frac12\eta^{\alpha\beta}\partial^\mu b_\mu.
\]
Its surface coefficient in \eqref{eq:boundary} is
\begin{equation}
\mathcal B(b)^{00}=-\frac12b_0,\qquad
\mathcal B(b)^{0i}=\frac12b_i,\qquad
\mathcal B(b)^{ij}=-\frac12\delta^{ij}b_0.
\label{eq:Bsurface}
\end{equation}
In particular, \(\mathcal B\) is injective on the boundary
covector \(b\).

\begin{lemma}[A nonzero surface coefficient is not microcausal]
\label{lem:surfaceWF}
Let \(b\) be smooth near \(\Sigma\). If \(b|_\Sigma\ne0\), then
\(C^*(\theta b)\) has a nonzero timelike wavefront covector.
\end{lemma}

\begin{proof}
By \eqref{eq:Bsurface}, some component of
\(\beta=\mathcal B(b|_\Sigma)\) is nonzero on a boundary patch.
That component has local form
\[
\delta(t)\beta(\mathbf x)+\theta(t)c(t,\mathbf x),
\]
with \(c\) smooth.

Choose compact localizers \(\chi(t),\rho(\mathbf x)\), with
\(\chi(0)=1\), so that
\(\int\rho(\mathbf x)\beta(\mathbf x)\dd^3\mathbf x\ne0\).
The Fourier transform of the localized delta term at
\((\tau,\mathbf 0)\) is this nonzero constant.
The transform of the localized Heaviside term is
\(O(|\tau|^{-1})\), by one-sided integration by parts.
Thus the localized distribution is not rapidly decreasing
along the normal rays as \(|\tau|\to\infty\).

If the distribution had no timelike wavefront covectors on
that compact patch, the local wavefront estimates, after a
finite partition of unity, would give rapid decay in a cone
around those normal rays. This contradicts the preceding
asymptotic. Hence a timelike covector occurs.
\end{proof}

\begin{lemma}[Microcausal admitted linear kernels have zero charge]
\label{lem:MCcharge}
If \(\ell\in\Slin\) has no nonzero nonspacelike wavefront
covector, then \(\Charge(\ell)=0\).
\end{lemma}

\begin{proof}
Write \(\ell=m+q_a\). The kernel \(m\) has only spacelike
wavefront covectors by Assumption~\ref{ass:carrier}.
Therefore
\[
\WF(q_a)=\WF(\ell-m)\subset\WF(\ell)\cup\WF(m)
\]
also has no nonspacelike covector.
The source \(a\) is compact smooth, so \(b=\GA a\) is smooth.
Lemma~\ref{lem:surfaceWF} forces \(b|_\Sigma=0\).
Equation \eqref{eq:charge} now gives the conclusion.
\end{proof}

This argument does not reverse the stated inclusion for
\(\Mlin\): it does not assume that every spacelike linear
kernel has already been identified with an element of
\(\Mlin\).

\begin{proposition}[Zero-charge comparison classes]
\label{prop:zerocharge}
At every smooth configuration and after every finite smooth
directional insertion,
\[
\Charge\bigl((\Ddir_{\boldsymbol\eta}F)'_h(\psi)\bigr)=0
\]
for
\[
F\in\QLspace\cup\QRspace\cup\Pmc.
\]
\end{proposition}

\begin{proof}
For the partial contractions, the inherited metric derivative
is compact smooth. Inserting a scalar direction replaces the
smooth scalar configuration by that direction. Inserting a
metric direction removes the only metric slot, so subsequent
metric differentiation is zero. Higher derivatives vanish
by polynomial degree. All nonzero metric kernels in this
calculation are therefore compact smooth elements of
\(\Mlin\), with zero charge.

For \(F\in\Pmc\), contraction of its higher functional
derivatives against smooth directions is a proper
pushforward after inserting compact cutoffs equal to one on
the coefficient supports. A wavefront covector of the
remaining one-slot kernel can arise only from a joint
covector with all integrated covectors zero.

A nonzero causal covector in the remaining slot, together
with those zeros, would belong entirely to one of the
excluded closed causal cones. Thus the remaining metric
kernel has only spacelike wavefront covectors. It belongs
to \(\Slin\) by carrier admission, and
Lemma~\ref{lem:MCcharge} proves its charge is zero.
\end{proof}

\subsection{An explicit sharp trace witness}

The following trace formula fixes the sign for
\(\Box=-\partial_t^2+\Delta\):
\begin{equation}
(\GA a)_\mu(0,\mathbf z)
=-\frac1{4\pi}\int_{\R^3}
\frac{a_\mu(|\mathbf x-\mathbf z|,\mathbf x)}
{|\mathbf x-\mathbf z|}\dd^3\mathbf x,
\qquad a\in C_c^\infty(M_+;T^*M).
\label{eq:advancedtrace}
\end{equation}
It is the advanced Kirchhoff formula; compare \cite{Ivrii}.
To see the normalization, the spatial Fourier transform of
\(\delta(s-|\mathbf x|)/(4\pi|\mathbf x|)\), for \(s>0\), is
\(\sin(s|p|)/|p|\). The zero-future-data solution of
\[
\partial_t^2\widehat u+|p|^2\widehat u=-\widehat a
\]
at \(t=0\) is
\[
-\int_0^\infty\frac{\sin(s|p|)}{|p|}
\widehat a(s,p)\dd s.
\]
Inverting the spatial transform gives
\eqref{eq:advancedtrace}.

\begin{lemma}[Sharp charge separation for every nonzero test]
\label{lem:sharpcharge}
For every nonzero \(f\in\Tspace\), there is a real smooth scalar
configuration \(\phi\), which can be chosen compactly supported
in \(M_+\), such that
\[
\Charge(B_f'_h[h,\phi])\ne0.
\]
No directional descendant is needed.
\end{lemma}

\begin{proof}
The metric derivative is
\begin{equation}
B_f'_h[h,\phi]=q_{a_{f,\phi}},
\qquad
a_{f,\phi,\mu}=-f\,\partial_\mu\phi.
\label{eq:Bderivative}
\end{equation}
Choose \(x_0=(t_0,\mathbf x_0)\) with \(f(x_0)\ne0\).
Select \(\mathbf z\) with
\[
|\mathbf x_0-\mathbf z|=t_0.
\]
Since \(t_0>0\), a neighborhood \(U\Subset M_+\) of \(x_0\)
can be chosen away from the spatial point \(\mathbf z\).
Let
\[
r(\mathbf x)=|\mathbf x-\mathbf z|
\]
on that neighborhood. Choose
\(\chi\in C_c^\infty(U;\R)\), nonnegative and positive at \(x_0\),
and form the complex scalar
\[
\phi_{\C}(t,\mathbf x)
=(t-r(\mathbf x))\,\overline{f(t,\mathbf x)}\,\chi(t,\mathbf x).
\]
Extended by zero outside \(U\), it is compact smooth.

On the cone \(t=r(\mathbf x)\),
\[
\partial_t\phi_{\C}
=\overline f\,\chi.
\]
Using \eqref{eq:advancedtrace} and \eqref{eq:Bderivative},
\begin{equation}
(\GA a_{f,\phi_{\C}})_0(0,\mathbf z)
=\frac1{4\pi}\int_{\R^3}
\frac{|f(r(\mathbf x),\mathbf x)|^2
\chi(r(\mathbf x),\mathbf x)}
{r(\mathbf x)}\dd^3\mathbf x>0.
\label{eq:positivewitness}
\end{equation}
The denominator is bounded away from zero on the relevant
support. Positivity holds on an open spatial patch near
\(\mathbf x_0\).

Write \(\phi_{\C}=\phi_1+i\phi_2\) with real compact smooth
\(\phi_1,\phi_2\). The trace is complex linear in the scalar
configuration. Since \eqref{eq:positivewitness} is nonzero,
at least one of the traces for \(\phi_1,\phi_2\) is nonzero.
Choose that real configuration. The metric configuration
may be zero, since \eqref{eq:Bderivative} is independent of \(h\).
\end{proof}

This witness is independent of the inherited nonconvergence of
regularized sharp generators.

\begin{theorem}[The required actual-space separations]
\label{thm:separation}
The intersections are
\[
\Bspace\cap\QLspace=\{0\},\qquad
\Bspace\cap\QRspace=\{0\},\qquad
\Bspace\cap\Pmc=\{0\}.
\]
Consequently,
\[
(\QLspace\otimes\Bspace)\cap
(\Bspace\otimes\QRspace)=\{0\}.
\]
\end{theorem}

\begin{proof}
Every element of \(\Bspace\) is \(B_f\) for one test \(f\),
because the generating map is linear. A nonzero such element
has \(f\ne0\). Lemma~\ref{lem:sharpcharge} gives a configuration
at which its metric derivative has nonzero charge.

Every element of either partial-contraction space or the old
algebra has zero charge at that configuration by
Proposition~\ref{prop:zerocharge}. Equality of actual
functionals would imply equality of their actual metric
derivatives and intrinsic charges, a contradiction.

For algebraic tensor products,
\[
(U\otimes V)\cap(U'\otimes V')
=(U\cap U')\otimes(V\cap V').
\]
Apply this identity to the displayed degree-two domains.
\end{proof}

%=====================================================================
\section{Gate G: simultaneous new-domain and old-domain gluing}
\label{sec:gluing}
%=====================================================================

\subsection{Compatibility of all new domains}

Metric--scalar homogeneity separates the locked first stages
from the second stages. The species degrees are
\[
\deg(B)=(1,1),\qquad
\deg(W)=(2,0),\qquad
\deg(P)=(3,1),\qquad
\deg(Q)=(1,1).
\]
Here the entries count metric and scalar slots.

The six new domains therefore have argument species degrees
\[
\begin{array}{c|c}
\text{domain}&(\text{first argument};\text{second argument})\\ \hline
\Bspace\otimes\Wspace&((1,1);(2,0))\\
\Wspace\otimes\Bspace&((2,0);(1,1))\\
\PLspace\otimes\Bspace&((3,1);(1,1))\\
\Bspace\otimes\PRspace&((1,1);(3,1))\\
\QLspace\otimes\Bspace&((1,1);(1,1))\\
\Bspace\otimes\QRspace&((1,1);(1,1)).
\end{array}
\]

\begin{proposition}[Direct decomposition of the new domain]
\label{prop:newdirect}
The new domain is the algebraic direct sum
\begin{equation}
\begin{split}
\Dnew={}&
(\Bspace\otimes\Wspace)
\oplus(\Wspace\otimes\Bspace)
\oplus(\PLspace\otimes\Bspace)
\oplus(\Bspace\otimes\PRspace)
\\
&\oplus(\QLspace\otimes\Bspace)
\oplus(\Bspace\otimes\QRspace).
\end{split}
\label{eq:newdirect}
\end{equation}
The prescribed coefficient maps therefore glue uniquely on
\(\Dnew\).
\end{proposition}

\begin{proof}
The zero intersections involving the degree-four blocks are
the inherited field-degree results of IX-Free.
The locked first-stage domains have species degrees distinct
from all second-stage domains and from each other.

All relations can be projected onto the distinct homogeneous
argument-species components. The only component containing
two listed domains is \(((1,1);(1,1))\). Its two domains have
zero intersection by Theorem~\ref{thm:separation}. Thus that
sum is direct as well.

This proves a direct decomposition of the entire sum, not
merely pairwise agreement. Each coefficient restriction is
an actual linear map by the inherited first stages, inherited
degree-two descent, and Theorem~\ref{thm:degree4}. Their sum
is consequently a unique linear map on \(\Dnew\).
\end{proof}

\subsection{An anchored-domain lemma}

\begin{lemma}[Vanishing of the old overlap of an anchored sum]
\label{lem:anchored}
Let \(A\) be a complex vector space and let \(B,P\subset A\)
satisfy \(B\cap P=\{0\}\). Then
\[
(A\otimes B+B\otimes A)\cap(P\otimes P)=\{0\}.
\]
\end{lemma}

\begin{proof}
On \(P\oplus B\), define \(\pi(p+b)=p\). Extend this linear
map algebraically to \(A\), using a vector-space complement,
with values in \(P\). Then
\[
\pi|_P=\id,\qquad \pi|_B=0.
\]
The map \(\pi\otimes\pi\) is the identity on \(P\otimes P\)
and vanishes on \(A\otimes B+B\otimes A\). An element in
their intersection must therefore be both unchanged and
annihilated by this map, hence zero.
\end{proof}

No continuity of \(\pi\) is asserted or needed.

\begin{theorem}[Whole-sum old-product compatibility]
\label{thm:oldgluing}
The full new-domain sum has zero old overlap:
\[
\Dnew\cap\Dold=\{0\}.
\]
Thus
\[
\Ddecl=\Dnew\oplus\Dold.
\]
For each fixed real \(c\), all prescribed coefficients glue
uniquely with the unchanged old coefficients on \(\Ddecl\).
\end{theorem}

\begin{proof}
Every new domain has a factor in \(\Bspace\) in at least one
argument. Hence
\[
\Dnew\subset
\Padm\otimes\Bspace+\Bspace\otimes\Padm.
\]
Theorem~\ref{thm:separation} gives
\(\Bspace\cap\Pmc=0\). Apply Lemma~\ref{lem:anchored} with
\(A=\Padm\), \(B=\Bspace\), and \(P=\Pmc\).
This proves vanishing of the old overlap of the entire new
sum, including any potential sum-domain relation.

Proposition~\ref{prop:newdirect} already constructs each
coefficient on \(\Dnew\). Combining it with \(C_j^H\) on
the disjoint old domain gives a unique map on \(\Ddecl\).
\end{proof}

This proof does not subtract a regular coefficient, alter a fixed
old product, or make a convergence assertion.

\subsection{Evaluation of the gluing parameter set}

Define
\[
\Cglue
=\{c\in\R:\text{all declared coefficient overlap equations hold}\}.
\]

\begin{corollary}[All real common parents pass gluing]
\label{cor:cglue}
For this declared sector,
\[
\Cdesc=\R,\qquad \Cglue=\R.
\]
\end{corollary}

\begin{proof}
The first equality is inherited. Every degree-four prescription
descends independently of \(c\). The degree-two scalar maps
descend for every real \(c\).

Proposition~\ref{prop:newdirect} and
Theorem~\ref{thm:oldgluing} show that the complete declared
domain has no overlap imposing an additional scalar equation.
Thus gluing holds for every real \(c\).
\end{proof}

The parameter is free only within the inherited parent family.
No conclusion is drawn about other normalizations or larger
domains.

%=====================================================================
\section{The constructed truncated partial product}
\label{sec:product}
%=====================================================================

\begin{definition}[Truncated partial product]
\label{def:product}
For \(d\in\Ddecl\), set
\[
\star_c(d)=\sum_{j=0}^3\hbar^jC_j(d)\in\Vmod.
\]
Extend this map \(\Rtr\)-linearly to
\[
\Dformal=\Ddecl\otimes_\C\Rtr.
\]
A pair of formal functionals is admissible when its formal
tensor lies in \(\Dformal\). On such a pair, the partial
product is obtained by this linearized map.
\end{definition}

This formulation does not assert that every pair of elements of
\(\Vmod\) is admissible, or that the declared domain is closed
under every intermediate multiplication.

\begin{proposition}[Interface audit]
\label{prop:interfaces}
The product of Definition~\ref{def:product} satisfies
C-I1--C-I9 on its declared sector, with the continuity
assertions proved in Section~\ref{sec:continuity}.
\end{proposition}

\begin{proof}
For C-I1, every new positive coefficient is a finite sum of
inherited admitted graphs or an admitted constant. Classical
closure handles \(C_0\); old coefficients are inherited.
All required admission descendants are included in those
statements.

C-I2 is the definition of \(C_0\). C-I3 follows from the
unchanged restriction
\[
\star_c|_{\Dold}=\star_H\pmod{\hbar^4};
\]
the simultaneous-gluing proof shows this restriction is
well defined. C-I4 is the first-stage coefficient assignment.

For C-I5, the only new scalar coefficients are the inherited
maps with kernel \(U_c\), using the one parameter fixed at the
start. Their observation compatibility is recorded below.
No new parent is selected during descent or gluing.

C-I6 holds because no old coefficient is changed. C-I7 is
respected because no convergence of unchanged sharp
approximants is invoked. C-I8 follows from descent to
actual spaces and unique gluing on the full declared domain.
C-I9 is satisfied by the precisely delimited fixed-support
continuity theorem; no actual-stage continuity is asserted.
\end{proof}

%=====================================================================
\section{Gate C: coherence for the selected word}
\label{sec:coherence}
%=====================================================================

Write
\[
A=B_f,\qquad W=W_g,\qquad C=B_{f'},
\]
\[
P_L=AW,\quad Q_L=\mathcal Q_{f,g},\qquad
P_R=WC,\quad Q_R=\mathcal Q^R_{g,f'}.
\]
Both formal intermediate tensors
\[
(P_L+\hbar Q_L)\otimes C,\qquad
A\otimes(P_R+\hbar Q_R)
\]
belong to \(\Dformal\). Thus both associations now exist.

\begin{theorem}[Wordwise coherence through order three]
\label{thm:coherence}
For every fixed real common parent \(c\),
\[
(A\star_cW)\star_cC
=A\star_c(W\star_cC)
\quad\text{in }\Vmod.
\]
Their common coefficients are
\[
\begin{array}{c|l}
\hbar\text{-order}&\text{common actual output}\\ \hline
0&AWC\\
1&\Graph_{12}+\Graph_{13}+\Graph_{23}\\
2&\Graph_{12,23}+\Graph_{12,13}+\Graph_{13,23}\\
3&\Cal(f,g,f')\,1.
\end{array}
\]
\end{theorem}

\begin{proof}
The left association is
\begin{align*}
P_LC
&+\hbar\bigl(L_1(P_L,C)+Q_LC\bigr)\\
&+\hbar^2\bigl(L_2(P_L,C)+L_1(Q_L,C)\bigr)
+\hbar^3L_2(Q_L,C),
\end{align*}
and the right association is
\begin{align*}
AP_R
&+\hbar\bigl(R_1(A,P_R)+AQ_R\bigr)\\
&+\hbar^2\bigl(R_2(A,P_R)+R_1(A,Q_R)\bigr)
+\hbar^3R_2(A,Q_R).
\end{align*}
There is no \(C_3\) contribution on these new blocks by the
selected coefficient assignment.

Classical associativity gives equality at order zero.
The descended degree-four prescriptions and inherited
degree-two maps give
\begin{align*}
L_1(P_L,C)+Q_LC
&=(\Graph_{13}+\Graph_{23})+\Graph_{12},\\
R_1(A,P_R)+AQ_R
&=(\Graph_{12}+\Graph_{13})+\Graph_{23},\\
L_2(P_L,C)+L_1(Q_L,C)
&=\Graph_{13,23}+\Graph_{12,23}+\Graph_{12,13},\\
R_2(A,P_R)+R_1(A,Q_R)
&=\Graph_{12,13}+\Graph_{12,23}+\Graph_{13,23},\\
L_2(Q_L,C)&=R_2(A,Q_R)=\Cal(f,g,f')\,1.
\end{align*}
These are now equalities of coefficients of existing actual
partial products. Equality of all four coefficients is
equality in \(\Vmod\).
\end{proof}

The residual total field degrees are \(6,4,2,0\).
This theorem is coherence for the selected word, not associativity
for every triple whose individual factors happen to lie in
\(\Padm\).

A discrepancy in a nonconstant coefficient could not be moved
into \(cr\), since the scalar and nonconstant orders are distinct.

%=====================================================================
\section{Reversal, presentation independence, and observations}
\label{sec:reversal}
%=====================================================================

For an actual functional, \(F^*\) denotes complex conjugation
on real configurations. On the tensor domain define
\[
(F\otimes G)^\dagger=G^*\otimes F^*.
\]
This reversal-conjugation, rather than componentwise conjugation
alone, is the appropriate domain operation for a partial-product
involution.

\begin{theorem}[Partial-product reversal]
\label{thm:reversal}
The declared domain is dagger stable and, for \(0\le j\le3\),
\[
C_j(d^\dagger)=C_j(d)^*.
\]
Consequently every admissible pair has an admissible reversed
conjugate pair and
\[
(F\star_cG)^*=G^*\star_cF^*.
\]
The formula extends coefficientwise to formal admissible pairs,
with \(\hbar^*=\hbar\).
\end{theorem}

\begin{proof}
Reality of the smooth operators gives
\[
\Bspace^*=\Bspace,\qquad \Wspace^*=\Wspace,\qquad
\PLspace^*=\PRspace.
\]
The inherited first-stage exchange gives
\[
\mathcal Q_{f,g}^*
=\mathcal Q^R_{\bar g,\bar f},
\qquad
\QLspace^*=\QRspace.
\]
Thus dagger exchanges the two first-stage domains and the
corresponding left and right second-stage domains.
The old domain is dagger stable by its inherited convention.

On the descended degree-four blocks, the inherited graph
exchanges give
\[
L_j(F,B)^*=R_j(B^*,F^*),\qquad j=1,2.
\]
For example, \(\Graph_{13}+\Graph_{23}\) exchanges with
\(\Graph_{13}+\Graph_{12}\), and
\(\Graph_{13,23}\) exchanges with \(\Graph_{12,13}\).
The inherited degree-two reversal gives the same identity
on those blocks. The scalar exchange uses real \(c\) and the
parent dagger symmetry. Classical multiplication and the
zero coefficients obey the identity as well.

It holds on the old domain by Assumption~\ref{ass:old}.
Unique gluing on \(\Ddecl\) extends these component identities
to every declared tensor.
\end{proof}

Componentwise conjugation of an ordered left block need not
remain a left block. No stronger componentwise domain-stability
assertion is needed.

\begin{proposition}[Actual-functional presentation independence]
\label{prop:presentation}
The constructed coefficient maps preserve every rewriting
that leaves the declared tensor of actual off-shell
functionals unchanged. This includes finite presentation
relations, polarization, kernel permutations, tensor
symmetries, and integration by parts with all boundary
terms retained.
\end{proposition}

\begin{proof}
The coefficient maps are linear maps on a subspace of the
actual tensor product \(\Padm\otimes\Padm\).
Within the presentation blocks, actual equality is respected
by the inherited degree-two descent and
Theorem~\ref{thm:degree4}. Across blocks it is respected by
simultaneous gluing. Hence equal actual tensors have equal
coefficients.
\end{proof}

The surface term in \eqref{eq:boundary} remains part of the actual
kernel. Omitting it changes the argument; it is not a presentation
rewrite. No equation-of-motion quotient is introduced.

\begin{proposition}[One-parent numerical observation compatibility]
\label{prop:observations}
For every declared smooth multiplier \(a\) and
smooth-coefficient differential operator \(D\) on \(X\),
\[
aDU_c=aDu_\mu^\rho+c\,aDr.
\]
In particular,
\[
\Cal(\partial_t^n f,g,f')
=\pair{(-\partial_{x^0})^nU_c}{f\otimes g\otimes f'}.
\]
The parameter in these identities is the same \(c\) used
in the partial product.
\end{proposition}

\begin{proof}
These are distributional differentiation and multiplication
identities for the fixed parent \eqref{eq:parent}. The
inherited numerical calibration supplies the declared
analytical compatibility. No descent or gluing step
changes the parent.
\end{proof}

A general joint observation multiplier supplies a numerical
operation. It does not, without a separate factorization,
enlarge the actual partial-product domain or open new
configuration slots.

%=====================================================================
\section{Gate T: fixed-support continuity and its boundary}
\label{sec:continuity}
%=====================================================================

Fix compact sets
\[
K_1,K_2,K_3\Subset M_+,
\qquad
\Dtest_{K_i}
=\{f\in C_c^\infty(M_+):\supp f\subset K_i\}.
\]
These are Fr\'echet spaces with their usual smooth seminorms.

We first record the continuity argument needed for classical
products of inherited families.

\begin{lemma}[Fr\'echet multilinear continuity]
\label{lem:Frechet}
A separately continuous finite multilinear map from a finite
product of Fr\'echet spaces to a locally convex space is
jointly continuous.
\end{lemma}

\begin{proof}
It suffices to obtain a local bound for each target seminorm.
Induct on the number of arguments. For a fixed first
argument, the map of the remaining arguments is jointly
continuous by induction.

Choose countable neighborhood bases in the remaining
Fr\'echet spaces. The sets of first arguments for which
the target seminorm is bounded by one on a specified product
of those neighborhoods are closed, balanced, and convex.
Their countable dilates cover the first space. The Baire
theorem therefore makes one such set have interior; its
balanced convex structure then gives a neighborhood of zero.
This supplies the required bound on a product of
neighborhoods. Multilinearity and homogeneity give joint
continuity.
\end{proof}

For completeness, the one-edge factor \(\mathcal T_{f,f'}\)
has the fixed-support continuity needed below. This is a
mapping estimate for an inherited value, not a new graph
construction.

\begin{lemma}[Continuity of the sharp--sharp one-edge family]
\label{lem:Tcontinuity}
For fixed \(K_1,K_3\), the map
\[
(f,f')\longmapsto\mathcal T_{f,f'}
\]
is jointly continuous from
\(\Dtest_{K_1}\times\Dtest_{K_3}\) to \((\Padm,\taus)\).
\end{lemma}

\begin{proof}
Its compact coefficient kernels arise from the fixed
distribution \(S_{\mu\nu}\), multiplication by
\(f\otimes f'\), and the fixed field-slot transpositions of
\(L\). The compact-distribution estimates and continuity
of these transpositions are the same inherited operations
used in IX-Free. They control all strong coefficient
seminorms.

At a fixed smooth metric configuration, its metric derivative
is \(q_{a^{(1)}+a^{(2)}}\), where
\begin{align*}
a^{(1)}_\mu(x)
&=f(x)\int f'(x')S_{\mu\nu}(x,x')w^\nu(x')\dd^4x',\\
a^{(2)}_\nu(x')
&=f'(x')\int f(x)S_{\mu\nu}(x,x')w^\mu(x)\dd^4x.
\end{align*}
These are compact smooth sources supported in \(K_1\) and
\(K_3\), respectively. The fixed difference-variable
distribution \(S\), convolved against a compact smooth
test times the fixed smooth field \(w\), gives a smooth
function continuously in that test. On compact sets this
follows directly from finite-order distribution estimates
after differentiating the smooth test.

Multiplication by \(f\) or \(f'\) is continuous in the fixed
smooth topologies. Thus both sources depend jointly
continuously on \((f,f')\), and the trace
\[
(\GA(a^{(1)}+a^{(2)}))|_\Sigma
\]
does so as well by the smooth Green-operator mapping property.
After one metric direction, replace \(w\) by \(L\eta_h\).
Later metric derivative traces vanish by quadratic degree.
Scalar directions have no effect.

These are all coefficient and trace coordinates required
by \(\taus\), proving the assertion.
\end{proof}

\begin{theorem}[F9a for the completed new families]
\label{thm:F9a}
On
\[
\Dtest_{K_1}\times\Dtest_{K_2}\times\Dtest_{K_3},
\]
the descended degree-four coefficient families
\[
L_j(B_fW_g,B_{f'}),\qquad
R_j(B_f,W_gB_{f'}),\qquad j=0,1,2,
\]
are jointly continuous into \((\Padm,\taus)\).
The corresponding degree-two families and scalar family
retain their inherited F9a continuity. The zero new
\(C_3\)-families are continuous.
\end{theorem}

\begin{proof}
For degree-four \(j=2\), the assertions are exactly the
inherited two-edge test-family continuity.

At degree-four \(j=1\), the terms
\[
\mathcal Q_{f,g}B_{f'},\qquad
B_f\mathcal Q^R_{g,f'},\qquad
\mathcal T_{f,f'}W_g
\]
are separately continuous trilinear maps of the fixed-support
tests. This follows from inherited test-family continuity,
Lemma~\ref{lem:Tcontinuity}, and separately continuous
classical multiplication on the carrier.
Lemma~\ref{lem:Frechet} makes each trilinear family jointly
continuous. Their prescribed sums are therefore continuous.

For \(j=0\), the family \(B_fW_gB_{f'}\) is separately
continuous in the three tests by repeated classical
multiplication. The same Fr\'echet multilinear argument
gives joint continuity.

The degree-two positive coefficients and the scalar family
are inherited from IX-Free. Their order-zero families also
follow from the same classical-product argument. Explicit
zero coefficients require no estimate.
\end{proof}

\paragraph{F9b remains unclaimed.}
The theorem concerns compositions with named test
presentations. It does not assert continuity of
\[
L_j:\PLspace\times\Bspace\longrightarrow\Padm,\qquad
R_j:\Bspace\times\PRspace\longrightarrow\Padm
\]
in actual-stage subspace topologies, nor corresponding
actual-stage continuity on the degree-two blocks.

Algebraic injectivity of \(p_L,p_R\) does not give continuous
inverse presentation maps. The algebraic projection in
Lemma~\ref{lem:anchored} carries no topology claim.
No quantum hypocontinuity on \(\Ddecl\), or on all of
\(\Padm\), has been proved.

%=====================================================================
\section{Final release and retained boundaries}
\label{sec:release}
%=====================================================================

\begin{theorem}[IX-Free-2 release]
\label{thm:release}
Relative to Assumptions~\ref{ass:carrier}--\ref{ass:parent},
the prescribed degree-four coefficients descend to actual
functionals. All declared new coefficients glue with the
locked first stages and the unchanged full old product
on the named domain \(\Ddecl\).

For every fixed real common parent \(c\), the resulting
truncated partial product satisfies C-I1--C-I9.
Its two associations of \(B_f,W_g,B_{f'}\) agree through
order \(\hbar^3\), and it has partial-product reversal and
actual-functional presentation independence.
Moreover,
\[
\Cdesc=\Cglue=\R.
\]
Fixed-support test-family continuity holds on the named
domains. Actual-stage continuity is not asserted.

The release outcome is \emph{Constructed}.
\end{theorem}

\begin{proof}
Theorem~\ref{thm:pinjective} evaluates both degree-four
relation kernels. Theorem~\ref{thm:degree4} proves descent.

Lemma~\ref{lem:sharpcharge} supplies the explicit sharp
charge witness, while Proposition~\ref{prop:zerocharge}
establishes the comparison zero-charge classes.
Theorem~\ref{thm:separation} proves all required separations.
Proposition~\ref{prop:newdirect} handles the entire new
domain, including the locked first stages.
Theorem~\ref{thm:oldgluing} handles its whole-sum old overlap.
Corollary~\ref{cor:cglue} evaluates the gluing parameter set.

Definition~\ref{def:product} gives one partial product, and
Proposition~\ref{prop:interfaces} audits the copied contract.
Theorem~\ref{thm:coherence}, Theorem~\ref{thm:reversal},
Proposition~\ref{prop:presentation}, and
Theorem~\ref{thm:F9a} prove the remaining assertions.
\end{proof}

\begin{center}
\small
\renewcommand{\arraystretch}{1.12}
\begin{tabularx}{\linewidth}{@{}p{.31\linewidth}p{.20\linewidth}X@{}}
\toprule
Release alternative & Outcome & Exact scope\\
\midrule
Constructed &
Achieved &
Prescribed truncated product on \(\Ddecl\), relative to the
stated inherited premises\\
Canonical prescription obstructed &
Not the outcome &
The prescribed candidate is constructed; no violating
relation is exhibited\\
Contract proved obstructed &
Not the outcome &
No universal no-go theorem is claimed\\
Unresolved required gate &
None in this release &
F9b and larger-domain constructions are outside the claim,
not silently completed\\
\bottomrule
\end{tabularx}
\end{center}

\begin{center}
\small
\renewcommand{\arraystretch}{1.12}
\begin{tabularx}{\linewidth}{@{}p{.36\linewidth}p{.20\linewidth}X@{}}
\toprule
Object & Final status & Proof or boundary\\
\midrule
First stages and one-edge outputs &
Constructed, inherited &
Values unchanged\\
Three two-edge outputs &
Constructed, inherited &
Existence and admission not reconstructed\\
\(\Cdesc\) &
Constructed, inherited &
\(\R\)\\
\(\kerop p_L,\kerop p_R\) &
Evaluated &
Both zero\\
Four degree-four coefficient maps &
Constructed &
Actual-functional descent\\
Sharp charge witness &
Constructed &
Explicit cone-local scalar test\\
Live degree-two overlap &
Evaluated &
Zero\\
Whole new-domain decomposition &
Constructed &
Direct sum, including first stages\\
Whole-sum old overlap &
Evaluated &
Zero by the anchored-domain lemma\\
\(\Cglue\) &
Evaluated &
\(\R\)\\
One declared partial product &
Constructed &
\(\Ddecl\), modulo \(\hbar^4\)\\
Both sharp associations &
Constructed &
Selected word through \(\hbar^3\)\\
Partial-product involution &
Constructed &
Dagger-stable declared domain\\
Presentation independence &
Constructed &
Actual off-shell arguments; boundary terms retained\\
F9a, new test families &
Constructed &
Named fixed-support Fr\'echet domains\\
F9b &
Unclaimed &
No inverse topology estimates\\
Associativity for unspecified triples &
Unclaimed &
No domain-closure theorem\\
VII-C under (E1)--(E4) &
Retained boundary &
Not reopened or repaired\\
IX-D and G2 &
Closed &
Not begun\\
\bottomrule
\end{tabularx}
\end{center}

\subsection{Retained obstruction and enlargement boundaries}

The inherited VII-C obstruction under its original
(E1)--(E4) hypotheses is retained. In particular, this paper
does not establish normal-topology sequential admission
continuity, unchanged sharp-approximant convergence, or
hypocontinuous quantum multiplication with continuous
coefficient extraction on a larger carrier.

No old coefficient is repaired by subtracting \(u_\mu^\rho\).
The calibrated family \(U_c\) is not identified with a
contact term. Admission of a generator does not admit an
unspecified quadratic correction. No logarithm is removed
by an observation-diagonal replacement.

The constructed domain is not advertised as the complete
free-product domain required by an unspecified IX-D
construction. No causal-support theorem or G2 compatibility
is obtained.

\scopebox{What was actually missing}{%
IX-Free had already supplied the two-edge outputs and their
admission. The missing algebraic steps were actual-functional
descent and simultaneous overlap agreement.

Here the degree-four relation equation has only the zero
presentation tensor. The live new-domain overlap vanishes by
an explicit boundary-charge separation, and the entire new
sum has zero old overlap. These facts, rather than another
graph sum or another singular-product construction, release
the selected word.}

%=====================================================================
\appendix
\section{Proof and verification audit}
%=====================================================================

\subsection{Polarization and operator audit}

The degree-four polynomial has one scalar slot and three metric
slots. Full coefficient recovery therefore uses one scalar
derivative and three metric derivatives, with the symmetric
metric factor \(3!\).

In the slot-isolation calculation, setting \(k_{00}=0\) leaves
two surviving middle-slot permutations. This gives the exact
factor \(-2\) in \eqref{eq:isolation}; it does not change the
inherited two-edge assignment factor.

The identity
\[
\Ezero\Box(CH)=CH
\]
uses compact support away from the initial surface and uniqueness
of the zero-data Cauchy problem. It neither assumes that \(w\)
and \(h_{00}\) are independent fields nor imposes an equation
of motion on the configuration.

\subsection{Charge audit}

The advanced-trace sign is determined by
\(\Box=-\partial_t^2+\Delta\). With the source
\(a_0=-f\partial_t\phi\), this sign produces the positive
integral in \eqref{eq:positivewitness}.

The complex witness is reduced to real smooth configurations
by linear decomposition, not by an assumption that
nonconvergence itself supplies a charge coordinate.

For the old algebra, zero charge follows from its microcausal
wavefront condition, admission, the injective boundary tensor
\(\mathcal B\), and the noncancellation of a delta coefficient
by a lower-order Heaviside coefficient.

\subsection{Algebraic and topological audit}

The new-domain proof is a direct-sum proof. The old-overlap proof
applies to the entire new sum. Thus no untested intersection
with an already glued sum remains.

All tensor products and separating projections used in these
arguments are algebraic. None identifies a presentation map
with a quotient map or a topological isomorphism.

The following implications are not asserted:
\[
\text{algebraic injectivity}
\ \Longrightarrow\
\text{continuous inverse},
\]
\[
\text{F9a}
\ \Longrightarrow\
\text{F9b or quantum hypocontinuity},
\]
\[
\text{one-word coherence}
\ \Longrightarrow\
\text{associativity on an unspecified domain},
\]
\[
\text{sector construction}
\ \Longrightarrow\
\text{IX-D or G2 opening}.
\]

\subsection{Verification disclosure}

The new proof calculations are the compact spatial-diagonal
test for restricted sharp separation, degree-four slot
isolation, the explicit advanced-trace witness, the
microcausal zero-charge argument, and simultaneous
algebraic gluing.

Graph construction, graph admission, the degree-two presentation
theorem, and the analytical triangle calibration are inherited
as explicitly stated. The complete companion manuscripts
are not independently reverified here.

This source is intended for two-pass pdfLaTeX compilation.
No successful compilation, page count, proof-assistant
verification, or independent review is claimed.

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

\paragraph{Nature of the result.}
A relative construction of one explicitly declared truncated
partial product and coherence for one ordered word.

\paragraph{Source boundary.}
IX-Free is the supplied reference. Its reports of IX-A, IX-C,
IX-B, and VII-D are used only through the explicit inherited
premises in this manuscript.

\paragraph{Continuity boundary.}
Fixed-support test-family continuity is proved.
Actual-stage continuity and quantum hypocontinuity are unclaimed.

\paragraph{Quantum and causal boundary.}
No global algebra, unrestricted associativity, causal realization,
interacting construction, retarded or time-ordered map,
IX-D construction, or G2 opening is asserted.

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

\bibitem{IXFree}
\emph{Landmark IX-Free:
Actual-functional binary factorization of one sharp ordered word}.
Supplied source, \texttt{IX-Free.tex}.
Used for the explicitly stated relation kernels,
degree-two presentation injectivity, scalar descent,
graph existence and admission, degree-two maps,
reversal, and fixed-support continuity.

\bibitem{IXC}
\emph{Landmark IX-C:
Actual-functional factorization and coefficientwise coherence
for one sharp ordered word}.
Companion reported in the supplied IX-Free source.
Used through the copied first stages, one-edge values,
interfaces, and preservation boundaries.

\bibitem{IXA}
\emph{Landmark IX-A:
An off-shell admission domain and boundary-sensitive topology
for sharp Cauchy relational insertions}.
Companion reported in IX-Free.
Used through the stated carrier, intrinsic charge,
sharp adjoint, and classical closure premises.

\bibitem{Calibration}
\emph{Landmark IX-B:
Derivative-stable triangle calibration and counterterm
constraints for sharp Cauchy insertions};
and \emph{Finite part of the regulated Cauchy-reflection triangle}.
Companions reported in IX-Free.
Used only through the inherited numerical parent-calibration
premise, not independently reverified.

\bibitem{VIIC}
\emph{Landmark VII-C:
A mixed-Wick obstruction to a normal-topology boundary extension
for sharp Cauchy harmonic insertions}.
Companion reported in IX-Free.
Its original conditional obstruction boundary is retained.

\bibitem{FR}
K.~Fredenhagen and K.~Rejzner.
\emph{Perturbative algebraic quantum field theory}.
Lecture notes, arXiv:1208.1428v2, 2013.
Section 4, especially the microcausal functional-derivative
condition, and Appendix A on wavefront sets.
\url{https://arxiv.org/abs/1208.1428}

\bibitem{Ivrii}
V.~Ivrii.
\emph{Partial Differential Equations}.
Online textbook, Section 9.1:
Wave equation in dimensions three and two.
Kirchhoff and Duhamel formulas.
\url{https://www.math.toronto.edu/ivrii/PDE-textbook/Chapter9/S9.1.html}

\end{thebibliography}

\end{document}