\section{Literal squares, finite order, and telescoping}
\label{slide:sec:squares-order-closure}

The cube is the point at which local compatibility becomes a global relation.
We first compare the supported maps as smooth maps of the common compression
body, then transport that equality to the outgoing boundary and finally to
Walker cylinders.  The order and telescoping statements are consequences of
that pointwise geometry.

For reference, the edge notation records successive views of one supported
move.  The imported local model \(F_\gamma\) is transported to \(f_a\),
extended by the identity to the ambient map \(\widehat F_a\), and then typed
at its source vertex as \(F_{a\mid A}\).  Its outgoing boundary map is
\(h_{a\mid A}\), and \(H_{a\mid A}=C(h_{a\mid A},0)\) is the corresponding
weight-zero Walker cylinder.  The set \(A\) records which other disjoint
slides have already been completed; it does not change the supported ambient
map in direction \(a\).

We now assemble the pairwise-disjoint edge directions into the finite cube.
The geometric statement comes first.  By
\eqref{slide:eq:completed-edge-map}, every edge in direction \(a\) is represented by
the same ambient map \(\widehat F_a\), independently of the source vertex, and
the closed protected sectors---including their full product collars---are
pairwise disjoint.  We will use these facts to prove equality of the two
smooth composites pointwise on the common compression body.  The outgoing and
Walker squares will then follow from that equality; they are not inferred from
commuting homology matrices.

Throughout the section, composition is right-factor first.  We also retain
the common-Lagrangian identities
\begin{equation}
 (h_{a\mid A})_*\Lambda=\Lambda,
 \qquad
 (h_{a\mid A}^{-1})_*\Lambda=\Lambda
 \label{slide:eq:square-common-lagrangian}
\end{equation}
from \cref{slide:prop:edge-homology-lagrangian}.

\subsection{The pointwise smooth square}

\begin{proposition}[Literal disjoint-support square]
\label{slide:prop:literal-disjoint-square}
Let \(A\subseteq[s]\), and let \(a,b\notin A\) be distinct.  Then, as
literal smooth maps on the common underlying compression body \(W\),
\begin{equation}
 \boxed{
 F_{b\mid A\cup\{a\}}\circ F_{a\mid A}
 =
 F_{a\mid A\cup\{b\}}\circ F_{b\mid A}.}
 \label{slide:eq:literal-disjoint-square}
\end{equation}
Both sides are the map \(\Phi_{a,b}\colon W\to W\) given pointwise by
\begin{equation}
 \Phi_{a,b}(x)=
 \begin{cases}
  \widehat F_a(x),&x\in\operatorname{int}(U_a),\\
  \widehat F_b(x),&x\in\operatorname{int}(U_b),\\
  x,&x\in
  W\setminus\bigl(\operatorname{int}U_a\cup
                   \operatorname{int}U_b\bigr).
 \end{cases}
 \label{slide:eq:common-pointwise-square-map}
\end{equation}
The branches in \eqref{slide:eq:common-pointwise-square-map} agree on full product
neighborhoods of the interfaces.  In particular, \(\Phi_{a,b}\) is smooth,
and \eqref{slide:eq:literal-disjoint-square} is an equality of complete-marked
relative maps from \(\mathfrak C_A\) to
\(\mathfrak C_{A\cup\{a,b\}}\), with every spectator marking fixed.
\end{proposition}

\begin{proof}
 Disjoint supports allow the two fixed ambient maps to be evaluated pointwise:
on the first support only the \(a\)-map acts, on the second only the \(b\)-map
acts, and outside both supports the identity remains.  The full product
collars make these descriptions agree smoothly at the interfaces, yielding a
literal equality of marked maps before any homology or Walker calculation.

The four active labels \(i_a,j_a,i_b,j_b\) are distinct, but the support
hypothesis is stronger than this label condition: the closures of \(U_a\)
and \(U_b\), with every protected neighborhood and full product collar, are
disjoint.  By \cref{slide:lem:local-model-identification}, the map
\(\widehat F_a\) carries \(U_a\) to itself and is the identity on a full
neighborhood of the complement of its support.  The same holds with \(a\)
and \(b\) interchanged.

If \(x\in U_a\), then \(\widehat F_b\) fixes both \(x\) and
\(\widehat F_a(x)\in U_a\).  Hence
\[
 (\widehat F_b\widehat F_a)(x)=\widehat F_a(x)
 =(\widehat F_a\widehat F_b)(x).
\]
The same argument on \(U_b\) gives the common value
\(\widehat F_b(x)\).  Outside the two interiors both maps are the identity.
On an interface collar these descriptions overlap, but the supported map has
the identity product germ on an open neighborhood of the collar.  Thus the
three branches in \eqref{slide:eq:common-pointwise-square-map} agree smoothly, not
merely along the interface disk.

Finally,
\[
 F_{a\mid A}=F_{a\mid A\cup\{b\}}=\widehat F_a,
 \qquad
 F_{b\mid A}=F_{b\mid A\cup\{a\}}=\widehat F_b
\]
as underlying maps.  The two composites therefore equal
\(\Phi_{a,b}\) pointwise.  Each route begins with the same completed source
chart and ends with the same completed target chart.  The literal equality
also retains every label, framing, collar, ribbon, detector, cellulation, and
spectator row carried by the two constituent edges.  No comparison isotopy or
homological uniqueness assertion is used.
\end{proof}

\begin{proposition}[Outgoing square]
\label{slide:prop:outgoing-square}
With the cube-compatible endpoint parameterizations,
\begin{equation}
 \boxed{
 h_{b\mid A\cup\{a\}}h_{a\mid A}
 =
 h_{a\mid A\cup\{b\}}h_{b\mid A}.}
 \label{slide:eq:outgoing-square}
\end{equation}
This is equality of the actual marked outgoing maps on \(Y\), with the
source row \(p_A\) and target row \(p_{A\cup\{a,b\}}\) retained.
\end{proposition}

\begin{proof}
Expanding the left side from \eqref{slide:eq:edge-transition-cylinder} gives
\begin{align*}
 h_{b\mid A\cup\{a\}}h_{a\mid A}
 &=p_{A\cup\{a,b\}}
   \bigl(F_{b\mid A\cup\{a\}}|_{\partial_+W}\bigr)
   p_{A\cup\{a\}}^{-1}
   p_{A\cup\{a\}}
   \bigl(F_{a\mid A}|_{\partial_+W}\bigr)p_A^{-1}\\
 &=p_{A\cup\{a,b\}}
   \bigl((F_{b\mid A\cup\{a\}}F_{a\mid A})
         |_{\partial_+W}\bigr)p_A^{-1}.
\end{align*}
The middle parameterizations cancel literally.  Expanding the other route
gives
\[
 p_{A\cup\{a,b\}}
 \bigl((F_{a\mid A\cup\{b\}}F_{b\mid A})
       |_{\partial_+W}\bigr)p_A^{-1}.
\]
The middle maps agree by \cref{slide:prop:literal-disjoint-square}, which proves
\eqref{slide:eq:outgoing-square}.  This argument is exactly where the simultaneous,
cube-compatible construction of the rows is needed: an independent
postcomposition of an intermediate \(p_A\) would destroy the literal
cancellation.
\end{proof}

\subsection{The weight-zero Walker square}

The equality of outgoing maps does not by itself determine the Walker
integers.  We therefore calculate the two products separately, in the order
prescribed by \eqref{common:eq-walker-product}.

\begin{lemma}[The two square corrections]
\label{slide:lem:square-walker-corrections}
For the left route through the square, the actual ordered correction is
\begin{equation}
 \mu_Y\!\left(
   (h_{a\mid A})_*\Lambda,
   \Lambda,
   (h_{b\mid A\cup\{a\}}^{-1})_*\Lambda
 \right)
 =\mu_Y(\Lambda,\Lambda,\Lambda)=0.
 \label{slide:eq:left-square-walker-correction}
\end{equation}
For the right route, the separately derived correction is
\begin{equation}
 \mu_Y\!\left(
   (h_{b\mid A})_*\Lambda,
   \Lambda,
   (h_{a\mid A\cup\{b\}}^{-1})_*\Lambda
 \right)
 =\mu_Y(\Lambda,\Lambda,\Lambda)=0.
 \label{slide:eq:right-square-walker-correction}
\end{equation}
\end{lemma}

\begin{proof}
 Compute the two routes separately in right-factor-first order: each route
places its image, seam, and inverse-image Lagrangians in its own Maslov
triple, and only then does the common Lagrangian reduce that triple to a
repeated pair.  The right route is not obtained by permuting or reversing the
left calculation; these two independent zero corrections are the input to
the literal Walker square.

On the left route, the first applied cylinder is \(H_{a\mid A}\) and the
second is \(H_{b\mid A\cup\{a\}}\).  Walker multiplication therefore puts
the image through the first map in the first Maslov slot, the declared seam
Lagrangian in the second slot, and the inverse image through the second map
in the third slot.  This gives the ordered triple in
\eqref{slide:eq:left-square-walker-correction} before simplification.  Applying
\eqref{slide:eq:square-common-lagrangian} to the two source-state-tagged edges
turns it into \((\Lambda,\Lambda,\Lambda)\), whose Maslov index vanishes.

On the right route, the first applied cylinder is \(H_{b\mid A}\) and the
second is \(H_{a\mid A\cup\{b\}}\).  A new application of the multiplication
formula gives the triple in \eqref{slide:eq:right-square-walker-correction}.  It is
not obtained by permuting or formally reversing the first calculation.
Equation~\eqref{slide:eq:square-common-lagrangian} again makes all three entries
equal, so this correction also vanishes.
\end{proof}

\begin{proposition}[Literal Walker square]
\label{slide:prop:walker-square}
In the Walker endomorphism set of \((Y,\Lambda)\),
\begin{equation}
 \boxed{
 H_{b\mid A\cup\{a\}}H_{a\mid A}
 =
 H_{a\mid A\cup\{b\}}H_{b\mid A}.}
 \label{slide:eq:walker-square}
\end{equation}
Both composites have actual integer weight zero.
\end{proposition}

\begin{proof}
Every edge cylinder has weight zero by definition.  Hence the two composite
weights are, respectively,
\begin{align*}
 0+0-
 \mu_Y\!\left(
   (h_{a\mid A})_*\Lambda,\Lambda,
   (h_{b\mid A\cup\{a\}}^{-1})_*\Lambda
 \right)&=0,\\
 0+0-
 \mu_Y\!\left(
   (h_{b\mid A})_*\Lambda,\Lambda,
   (h_{a\mid A\cup\{b\}}^{-1})_*\Lambda
 \right)&=0
\end{align*}
by \cref{slide:lem:square-walker-corrections}.  Their underlying marked outgoing
maps agree by \cref{slide:prop:outgoing-square}.  Equality of that map together
with equality of the retained integer is precisely the equality of Walker
cylinders in \eqref{slide:eq:walker-square}; no projectivization or target
evaluation is involved.
\end{proof}

\subsection{Finite order independence}

Let \(\mathfrak S_s\) denote the set of orders of the slide directions.  For
\(\omega=(\omega_1,\ldots,\omega_s)\in\mathfrak S_s\), set
\[
 A_q^\omega:=\{\omega_1,\ldots,\omega_q\},
 \qquad
 A_0^\omega:=\varnothing.
\]
Define the ordered total cylinder and its prefixes by
\begin{equation}
 H_\omega
 :=H_{\omega_s\mid A_{s-1}^\omega}\cdots
   H_{\omega_1\mid\varnothing},
 \qquad
 H_{\omega,\leq q}
 :=H_{\omega_q\mid A_{q-1}^\omega}\cdots
   H_{\omega_1\mid\varnothing},
 \label{slide:eq:ordered-total-cylinder}
\end{equation}
where \(H_{\omega,\leq0}:=C(\operatorname{id}_Y,0)\).  Let
\(\varphi_{\omega,\leq q}\) denote the underlying marked map of
\(H_{\omega,\leq q}\), with
\(\varphi_{\omega,\leq0}=\operatorname{id}_Y\).

\begin{lemma}[Zero weight of every prefix]
\label{slide:lem:prefix-zero-weight}
For every \(\omega\in\mathfrak S_s\) and \(0\leq q\leq s\),
\begin{equation}
 (\varphi_{\omega,\leq q})_*\Lambda=\Lambda,
 \qquad
 H_{\omega,\leq q}=C(\varphi_{\omega,\leq q},0).
 \label{slide:eq:prefix-lagrangian-and-weight}
\end{equation}
In particular, every prefix has Walker weight zero.
\end{lemma}

\begin{proof}
 The prefix induction is typed at every stage: assume the current marked map
preserves the common Lagrangian and has weight zero, then append the next edge
on the left.  The edge’s common-Lagrangian property forces the ordered Walker
triple to be a repeated pair, so the correction stays zero and the induction
retains both assertions.

The assertion is immediate for the empty prefix.  Suppose it holds through
\(q-1\).  The next edge map
\(h_{\omega_q\mid A_{q-1}^\omega}\) preserves \(\Lambda\) by
\eqref{slide:eq:square-common-lagrangian}, so its composite with
\(\varphi_{\omega,\leq q-1}\) does as well.  Before simplification, the Walker
correction for adjoining this edge on the left is
\[
 \mu_Y\!\left(
   (\varphi_{\omega,\leq q-1})_*\Lambda,
   \Lambda,
   (h_{\omega_q\mid A_{q-1}^\omega}^{-1})_*\Lambda
 \right).
\]
The induction hypothesis and \eqref{slide:eq:square-common-lagrangian} reduce this
ordered triple to \((\Lambda,\Lambda,\Lambda)\).  Its index is zero; the old
prefix and the new edge both have weight zero.  This proves
\eqref{slide:eq:prefix-lagrangian-and-weight} at \(q\).
\end{proof}

\begin{proposition}[Order-independent total slide cylinder]
\label{slide:prop:finite-order-independence}
All expressions in \eqref{slide:eq:ordered-total-cylinder} have one common value:
\begin{equation}
 \boxed{H_\omega=:H_{[s]}\qquad(\omega\in\mathfrak S_s).}
 \label{slide:eq:finite-order-independent-cylinder}
\end{equation}
This is literal equality in the Walker category, and the common cylinder has
weight zero.  The subscript \([s]\) records the terminal set of slide
directions; it is not the handle-label set \([k]\).
\end{proposition}

\begin{proof}
 An adjacent interchange is replaced by the already proved literal
weight-zero Walker square.  The reached vertex is the same after the two
factors, so every later tagged edge is unchanged; reducing arbitrary order
words by adjacent inversions then identifies all total cylinders with the
reference order.

First suppose two order words differ by interchanging adjacent entries at
positions \(q,q+1\).  Let \(P\) be the set of the preceding \(q-1\) slide
directions, and call the adjacent entries \(a,b\).  The two affected
right-factor-first fragments are
\[
 H_{b\mid P\cup\{a\}}H_{a\mid P}
 \quad\text{and}\quad
 H_{a\mid P\cup\{b\}}H_{b\mid P}.
\]
They are literally equal by \cref{slide:prop:walker-square}.  After either fragment
has been applied, the reached vertex is \(P\cup\{a,b\}\).  Every later left
factor therefore has the same source-state tag on both sides, and every
earlier right factor is unchanged.  Substitution gives equality of the two
full Walker composites.

Any order can be reduced to \((1,\ldots,s)\) by finitely many adjacent
interchanges: move \(1\) left to the first position, then move \(2\) left
within the remaining suffix, and continue.  The inversion number decreases
at every step, so the procedure terminates.  Repeated substitution of the
literal square equality identifies every \(H_\omega\) with the reference-order
composite, and hence with every other \(H_{\omega'}\).  Taking \(q=s\) in
\cref{slide:lem:prefix-zero-weight} proves that this common value has weight zero.
\end{proof}

The preceding proof uses adjacent replacement only as a method for proving
equality.  The next statement records the resulting Coxeter-shaped closure
without adding swap morphisms to the construction.

\begin{proposition}[Equality-only Coxeter-shaped closure]
\label{slide:prop:equality-only-coxeter-closure}
For an order expression, let \(\tau_q\) mean only the replacement of the
entries in positions \(q,q+1\) by the opposite order, using the literal
Walker equality \eqref{slide:eq:walker-square}.  With \(1\) denoting the unchanged
equality path, the following precisely ranged replacement diagrams close:
\begin{align}
 \tau_q^2&=1
 &&(1\leq q\leq s-1),
 \label{slide:eq:replacement-involution}\\
 \tau_q\tau_r&=\tau_r\tau_q
 &&(1\leq q,r\leq s-1,\ |q-r|>1),
 \label{slide:eq:replacement-distant}\\
 \tau_q\tau_{q+1}\tau_q
 &=\tau_{q+1}\tau_q\tau_{q+1}
 &&(1\leq q\leq s-2).
 \label{slide:eq:replacement-three-term}
\end{align}
These formulas concern paths of equality substitutions.  There is no mapping
cylinder \(\tau_q\), no retained swap map or comparison isotopy, and no
\(\mathfrak S_s\)-action.
\end{proposition}

\begin{proof}
 Each \(\tau_q\) is only a local equality substitution at the subset tag
determined by the preceding entries.  Involution, distant commutation, and
the three-term relation follow by comparing the resulting order words;
their stated ranges handle the low-dimensional cases without introducing a
swap cylinder or a symmetric-group action.

Fix an order expression.  A single \(\tau_q\)-step substitutes
\eqref{slide:eq:walker-square} at the prefix set determined by the entries before
positions \(q,q+1\).

For \eqref{slide:eq:replacement-involution}, the first substitution changes the
adjacent substring \((a,b)\) to \((b,a)\); applying the same literal equality
in the opposite direction returns to \((a,b)\).  This uses neither an inverse
slide nor a cylinder representing \(\tau_q\).

For \eqref{slide:eq:replacement-distant}, the two affected pairs occupy disjoint
positions.  Replacing one pair does not change the set of indices preceding
the other pair; it changes only their order.  Both routes therefore use the
same two square equalities in opposite succession and end at the identical
order expression.

For \eqref{slide:eq:replacement-three-term}, it is enough to display the affected
three consecutive entries.  The two routes are
\[
 (a,b,c)\longmapsto(b,a,c)\longmapsto(b,c,a)
 \longmapsto(c,b,a)
\]
and
\[
 (a,b,c)\longmapsto(a,c,b)\longmapsto(c,a,b)
 \longmapsto(c,b,a).
\]
At every arrow, the entries before the affected pair determine the exact
subset tag, and the two entries are distinct because the word is an order of
\([s]\).  Hence each arrow is an instance of
\eqref{slide:eq:walker-square}, and both replacement routes have the same initial
and terminal Walker expressions.

For \(s=1\), all three families are vacuous.  For \(s=2\), only the
involution family occurs, with \(q=1\); the distant and three-term ranges are
empty.  Thus the displayed ranges introduce no exceptional low-dimensional
case and no action.
\end{proof}

\subsection{Telescoping to the terminal vertex}

\begin{proposition}[Phase-zero and all-phase telescoping]
\label{slide:prop:telescoped-covariance}
For arbitrary base-weight vectors
\(\mathbf c,\mathbf r\in\mathbb Z^k\),
\begin{equation}
 \boxed{
 H_{[s]}J_\varnothing^0(\mathbf c)=J_{[s]}^0(\mathbf c),
 \qquad
 R_{[s]}^0(\mathbf r)H_{[s]}=R_\varnothing^0(\mathbf r).}
 \label{slide:eq:telescoped-phase-zero-covariance}
\end{equation}
For every \(\epsilon,\eta\in\{0,1\}^k\) and arbitrary
\(\mathbf u^+,\mathbf u^-\in\mathbb Z^k\),
\begin{equation}
 \boxed{
 H_{[s]}J_\varnothing^\epsilon(\mathbf c,\mathbf u^+)
 =J_{[s]}^\epsilon(\mathbf c,\mathbf u^+)}
 \label{slide:eq:telescoped-forward-all-phase}
\end{equation}
and
\begin{equation}
 \boxed{
 R_{[s]}^\eta(\mathbf r,\mathbf u^-)H_{[s]}
 =R_\varnothing^\eta(\mathbf r,\mathbf u^-).}
 \label{slide:eq:telescoped-reverse-all-phase}
\end{equation}
The common weights in \eqref{slide:eq:telescoped-phase-zero-covariance} are \(c_\Sigma\)
and \(r_\Sigma\).  Those in \eqref{slide:eq:telescoped-forward-all-phase} and
\eqref{slide:eq:telescoped-reverse-all-phase} are
\(c_\Sigma+U^+(\epsilon)\) and \(r_\Sigma+U^-(\eta)\), respectively.  The vectors remain
label-attached throughout the substitutions; the completed Walker morphisms
retain only the base totals and active phase-weight sums described in
\cref{slide:prop:endpoint-phase-words}.
\end{proposition}

\paragraph{Route replacement and telescoping.}
Choose one order only as a temporary route through the already constructed
edge family.  The phase-zero and all-phase covariance identities replace each
successive edge-plus-trace composite by the trace at the next vertex, while
finite order independence replaces the chosen total edge word by the terminal
one.  Because every replacement is already a Walker equality with its weight
retained, the telescoping changes the endpoint but introduces no new seam
correction.

\begin{proof}
Fix \(\omega\in\mathfrak S_s\), abbreviate \(A_q=A_q^\omega\), and use the
prefixes from \eqref{slide:eq:ordered-total-cylinder}.  For \(1\leq q\leq s\),
the two phase-zero edge equalities of
\cref{slide:prop:phase-zero-walker-covariance} are
\[
 H_{\omega_q\mid A_{q-1}}J_{A_{q-1}}^0(\mathbf c)
 =J_{A_q}^0(\mathbf c),
 \qquad
 R_{A_q}^0(\mathbf r)H_{\omega_q\mid A_{q-1}}
 =R_{A_{q-1}}^0(\mathbf r).
\]
Successive substitution gives
\begin{equation}
 H_{\omega,\leq q}J_\varnothing^0(\mathbf c)
 =J_{A_q}^0(\mathbf c),
 \qquad
 R_{A_q}^0(\mathbf r)H_{\omega,\leq q}
 =R_\varnothing^0(\mathbf r).
 \label{slide:eq:phase-zero-prefix-telescoping}
\end{equation}
At \(q=s\), the reached set is \([s]\), and
\cref{slide:prop:finite-order-independence} replaces
\(H_{\omega,\leq s}\) by \(H_{[s]}\).  This proves
\eqref{slide:eq:telescoped-phase-zero-covariance}.

The all-phase edge identities of \cref{slide:prop:all-phase-edge-covariance} give,
with the same source-state tags,
\[
 H_{\omega_q\mid A_{q-1}}
 J_{A_{q-1}}^\epsilon(\mathbf c,\mathbf u^+)
 =J_{A_q}^\epsilon(\mathbf c,\mathbf u^+)
\]
and
\[
 R_{A_q}^\eta(\mathbf r,\mathbf u^-)
 H_{\omega_q\mid A_{q-1}}
 =R_{A_{q-1}}^\eta(\mathbf r,\mathbf u^-).
\]
The identical finite substitution yields
\[
 H_{\omega,\leq q}J_\varnothing^\epsilon(\mathbf c,\mathbf u^+)
 =J_{A_q}^\epsilon(\mathbf c,\mathbf u^+)
\]
and
\[
 R_{A_q}^\eta(\mathbf r,\mathbf u^-)
 H_{\omega,\leq q}
 =R_\varnothing^\eta(\mathbf r,\mathbf u^-).
\]
Taking \(q=s\) proves
\eqref{slide:eq:telescoped-forward-all-phase}--
\eqref{slide:eq:telescoped-reverse-all-phase}.  Every step is already an equality
of Walker morphisms with its integer weight retained, so telescoping creates
no additional seam correction.  The zero weight of \(H_{[s]}\), together
with the endpoint-weight calculation in
\cref{slide:prop:endpoint-phase-words}, gives the four weights stated above.
\end{proof}

When \(s=1\), there is no two-face and the order statement is tautological;
the telescoped identities reduce to the single-edge covariances.  For
\(s\geq2\), every replacement used above involves distinct directions with
disjoint protected sectors.  Nothing in the argument supplies a relation for
shared-label or overlapping slides, a retained permutation action, or a
general slide sequence outside this fixed finite family.

\paragraph{Assembly of the disjoint cube.}
The final theorem packages the construction in the order forced by its
geometry.  First, the protected local model gives compatible vertices and
supported edge maps with a common Lagrangian.  Second, the phase-zero and
all-phase calculations supply the edge covariances and their Walker weights.
Third, disjoint supports give literal two-faces, while prefix substitutions
and finite route replacement remove order dependence.  Finally, the endpoint
telescoping identities assemble these local equalities into the stated cube
and preserve the theorem's equality-only scope.

\begin{proof}[Proof of
\cref{slide:thm-complete-marked-disjoint-slide-cube}]
The protected-sector construction, reference interface, local-model
identification, and identity extension are established in\newline
\cref{slide:prop:reference-vertex-interface,slide:lem:local-model-identification}.
\Cref{slide:prop:compatible-vertex-rows,slide:prop:edge-homology-lagrangian}
then prove complete compatibility of the vertices and edges, the actual
inverse, the signed integral symplectic formulas, and both directions of the
common-Lagrangian assertion.

Ordinary phase-zero covariance is
\cref{slide:prop:ordinary-phase-zero-covariance}; its two independently
ordered Walker lifts are
\cref{slide:lem:phase-zero-seam-data,slide:prop:phase-zero-walker-covariance}.
The actual-vertex phase words, their fixed-site reference comparison,
conjugacy preserving the complete markings, four phase-cylinder corrections, and all-phase
covariance are proved in
\cref{slide:prop:endpoint-phase-words,slide:prop:phase-cylinder-commutation,slide:prop:all-phase-edge-covariance}.

For two distinct directions,
\cref{slide:prop:literal-disjoint-square,slide:prop:outgoing-square}
establish the pointwise and outgoing squares before
\cref{slide:lem:square-walker-corrections,slide:prop:walker-square}
establish the literal weight-zero Walker square.  The prefix calculation,
finite route replacement, equality-only closure, and endpoint telescoping are
\cref{slide:lem:prefix-zero-weight,slide:prop:finite-order-independence,slide:prop:equality-only-coxeter-closure,slide:prop:telescoped-covariance}.
These results prove the six clauses of the theorem without importing any
several-slide assertion from the two-site companion construction.
\end{proof}