% =====================================================================
% ENTROPY EQUALITY AND LOCAL SYMMETRY IN NEGATIVE CURVATURE
% A complete proof of Katok's entropy rigidity conjecture (n >= 3)
% =====================================================================
% Each section opens with a PLAIN SUMMARY in plain words. Read those
% first. The full research-level proof follows. Classical tools are
% cited as black boxes.

\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools,bm}
\usepackage{enumitem,microtype}
\usepackage{tikz}
\usepackage{flafter}
\usepackage[numbers,sort&compress]{natbib}
\usepackage{hyperref}
\hypersetup{colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue,
  pdftitle={Entropy equality and local symmetry in negative curvature},
  pdfauthor={OpenAI}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{notation}[theorem]{Notation}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}
\newcommand{\R}{\mathbb R}
\newcommand{\C}{\mathbb C}
\newcommand{\N}{\mathbb N}
\newcommand{\Z}{\mathbb Z}
\newcommand{\Es}{E^s}
\newcommand{\Eu}{E^u}
\newcommand{\Ws}{W^s}
\newcommand{\Wu}{W^u}
\newcommand{\id}{\mathrm{id}}
\DeclareMathOperator{\tr}{tr}
\DeclareMathOperator{\ad}{ad}
\DeclareMathOperator{\Ad}{Ad}
\DeclareMathOperator{\End}{End}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\Span}{span}
\DeclareMathOperator{\Ann}{Ann}
\DeclareMathOperator{\Der}{Der}
\DeclareMathOperator{\Aut}{Aut}
\DeclareMathOperator{\rank}{rank}
\DeclareMathOperator{\supp}{supp}
\DeclareMathOperator{\Vol}{Vol}
\newcommand{\htop}{h_{\mathrm{top}}}
\numberwithin{equation}{section}
\setlist{topsep=4pt,itemsep=2pt}
\setlength{\emergencystretch}{2em}
\title{Entropy equality and local symmetry in negative curvature}
\author{OpenAI}
\date{September 23, 2026}

\begin{document}
\maketitle

\begin{abstract}
For every closed connected smooth Riemannian manifold of dimension
at least three with strictly negative sectional curvature, we prove
that normalized Liouville measure has maximal entropy for the
unit-speed geodesic flow if and only if the metric is locally
symmetric. This resolves Katok's entropy rigidity conjecture in all
these dimensions, including all rank-one symmetric types at arbitrary
scale.
\end{abstract}

\section{Introduction}
\label{sec:introduction}

\paragraph{Plain summary.}
A negatively curved cave --- a saddle-shaped surface at every point,
looping around into a compact manifold --- pulls nearby particles
apart exponentially. The rate at which it does so is the
\emph{entropy}. Topological entropy is the largest rate any
distribution could exhibit; Liouville entropy is the rate exhibited
by the natural probability measure (uniform volume, uniform
directions). The variational principle gives
$h_{m_L}(\phi_1)\le h_{\mathrm{top}}(\phi_1)$. Equality is the
best case possible: the natural distribution is as chaotic as
anything could be. Katok's conjecture asks which negatively curved
manifolds are best-case.

The answer, proved below for $n\ge3$, is: exactly the locally
symmetric ones --- the caves where every point, and every direction
at each point, looks like every other. These are the real, complex,
quaternionic, and Cayley hyperbolic spaces at arbitrary overall
scale. Any other negatively curved metric is equally regular near
every single point (curvature is a smoothly varying quadratic
form), so the misfit lives only in how local pieces fit together
globally. Entropy equality must detect that global misfit and force
a geometric constraint. It does.

\subsection*{Historical context}

Katok \citep{Katok1982} formulated the conjecture and proved the
surface case ($n=2$), where the argument reduces to Gauss--Bonnet
and closed-geodesic counting. He also proved rigidity within the
conformal class of any locally symmetric metric
\citep[Corollary~2.5]{Katok1982}. Flaminio \citep{Flaminio1995}
showed that the Liouville-entropy maximum is locally isolated in
higher-dimensional real hyperbolic metrics, but his Theorem~C also
exhibits a real hyperbolic $3$-manifold where the fixed-volume
Liouville Hessian is indefinite: the surface strategy through a
global maximum does not extend. In three-dimensional phase spaces,
smooth-volume entropy rigidity was fully classified by
\citep{Foulon2001} in the contact case and by
\citep{DeSimoiLeguilVinhageYang2020} in general; these are
two-dimensional base manifolds. Rigidity near isolated real or
complex hyperbolic metrics was shown by \citep{Humbert2026}.

The Besson--Courtois--Gallot theorem
\citep{BessonCourtoisGallot1995}, with the Cayley case corrected in
\citep{Ruan2024}, is a different comparison: it uses a KNOWN locally
symmetric target and equality in a volume-entropy inequality. Here
the symmetric target is a conclusion, obtained through
\citep{BenoistFoulonLabourie1992} only after proving the Anosov
bundles are globally smooth.

\subsection*{Proof strategy at a glance}

The geodesic flow of any compact negatively curved metric is
\emph{Anosov}: the tangent bundle of $SM$ splits as
\[
 T(SM)=\Es\oplus\R X\oplus\Eu,
\]
where $X$ is the flow direction, $\Es$ contracts exponentially
forward, and $\Eu$ expands. Individual leaves of the foliations
tangent to $\Es,\Eu$ are smooth. The \emph{bundles} themselves can
be badly non-smooth: the transverse gluing of leaves is only
measurable in general.

The whole proof is one mechanism: entropy equality forces
$\Es,\Eu$ to be smooth as subbundles. Once that holds,
\citet[Theorem~2]{BenoistFoulonLabourie1992} gives a smooth
conjugacy to a locally symmetric geodesic flow, and minimal
entropy rigidity of \citep{BessonCourtoisGallot1995} upgrades
conjugacy to isometry.

The four stages:

\begin{enumerate}[label=({\arabic*})]
\item \textbf{Entropy produces two conormal volume forms.}
  From entropy equality we build continuous horizontal $m$-forms
  $u$ annihilating $\Eu$ and $w$ annihilating $\Es$, with
  $\phi_t^*u=e^{-ht}u$ and $\phi_t^*w=e^{ht}w$. Their leaf
  derivatives are smooth with uniform bounds.
  Section~\ref{pre:section}.

\item \textbf{Plaque jets contract.} At each stable crossing,
  record the graph of the unstable plaque through it and its
  conormal density. Under $f=\phi_T$, finite jets contract in a
  finite-dimensional space. Non-stationary normal-form theory
  reduces the dynamics to polynomial form.
  Section~\ref{nf:section}.

\item \textbf{Coherent formal affine fields.} Zariski closure of
  the actual jets yields an algebraic variety of ``alternative
  plaque jets''. From these alternatives we build a formal affine
  bundle of conormal covectors at every point of an entire strong
  leaf, coherent to all Taylor orders --- \emph{without} assuming
  ambient smoothness. Section~\ref{hull:section}.

\item \textbf{Symmetry algebra and dichotomy.} The formal strict
  contact symmetries of those fields form a Lie algebra
  $\mathfrak h$, containing a distinguished dilation $H$ and
  satisfying the trace identity
  $c\,\xi(p)=\tr(p|_{E_+})$. Cartan--Guillemin structure theory
  gives a dichotomy: either $\mathfrak h$ is finite dimensional
  (formal fields are smooth, $\Es,\Eu$ smooth, done) or it is
  infinite dimensional and produces a coisotropic reduction whose
  characteristic rays force a Busemann contradiction on the
  universal cover. Sections~\ref{sym:section}--\ref{real:section}.

\item \textbf{Smoothness.} The infinite case is excluded, the
  finite case gives smooth $\Es,\Eu$, and the argument closes.
  Sections~\ref{smooth:section}--\ref{sec:completion}.
\end{enumerate}

\subsection*{Reader's guide}

Each section opens with a Plain Summary in plain words, then states
and proves lemmas at research level. Read the summaries first; every
lemma is a production step whose output feeds the next stage.

\subsection*{Prerequisites}

The full proof uses: Riemannian geometry (curvature, Jacobi
fields); hyperbolic dynamics (Anosov splitting, stable/unstable
manifolds); ergodic theory (Birkhoff, Oseledets, Pesin,
Liv\v{s}ic); thermodynamic formalism; Lie theory (linearly compact
Lie algebras; Cartan--Guillemin classification); algebraic geometry
(Zariski closure, generic smoothness). Each is introduced where
used. A first course in differential geometry and a first course
in dynamics together cover most of the background.

\subsection*{Main theorem, formally}

Let $(M^n,g)$ be a closed connected smooth Riemannian manifold with
$n\ge3$ and strictly negative sectional curvature, $SM$ its unit
tangent bundle, $\phi_t$ the unit-speed geodesic flow, $m_L$ the
normalized Liouville measure, and $R_g$ the Riemann curvature
tensor.

\begin{theorem}\label{thm:main}
Under these hypotheses,
\[
 h_{m_L}(\phi_1)=\htop(\phi_1)
 \quad\Longleftrightarrow\quad
 \nabla^g R_g=0.
\]
Equivalently, equality holds precisely when the universal cover is
a rank-one symmetric space of noncompact type, at arbitrary overall
scale.
\end{theorem}

The symmetric types for $n\ge3$ are $\R H^n$, $\C H^n$,
$\mathbb H H^n$ (quaternionic, for certain $n$), and \(\mathbb O H^2\)
(Cayley, only $n=16$).

The ``if'' direction is a direct computation from homogeneity
(Section~\ref{sec:completion}). The ``only if'' is the content of
Sections~\ref{pre:section}--\ref{smooth:section}.

A consequence worth recording: when the metric is not locally
symmetric, the entropy-maximising probability measure is mutually
singular with Liouville. Indeed, $m_L$ is a non-maximiser by
Theorem~\ref{thm:main}; the maximal-entropy measure is unique and
ergodic by thermodynamic formalism \citep{BowenRuelle1975}; and two
distinct ergodic invariant probabilities on a standard probability
space are mutually singular.

\section{Dynamical preliminaries}
\label{pre:section}

\paragraph{Plain summary.}
We set up the Anosov flow and produce the two conormal volume forms
$u,w$ from entropy equality. Key objects: the unstable Riccati tensor
$U$, its trace $J=\tr U$ (the unstable expansion rate), a transfer
function $F$ solving the cohomological equation $J=h+XF$, and two
$m$-forms built from $F$ whose pullbacks scale by $e^{-ht}$ and
$e^{ht}$. Motivated by Pesin's formula, the entropy formula, and
Liv\v{s}ic cohomology, these forms package the entropy data. They
are the sole input to the rest of the proof.

Let $m=n-1$, let $X$ be the geodesic vector field on $SM$, and let
$\alpha$ be the canonical contact form normalized by $\alpha(X)=1$.
The strong Anosov splitting is
\[
 T(SM)=\Es\oplus\R X\oplus\Eu,
 \qquad \ker\alpha=\Es\oplus\Eu.
\]
Denote by $\Ws,\Wu$ the strong foliations, by the same letters with
weak prefix the corresponding weak foliations. We use throughout the
following classical facts for compact strictly negatively curved
geodesic flows: uniform hyperbolicity, smooth individual strong and
weak leaves with uniform bounds at each finite order, absolute
continuity of the foliations, and ergodicity of Liouville volume.
The hyperbolic theory is Anosov's \citep{Anosov1967}; Hopf's ergodic
argument and the bounded-Jacobian version of absolute continuity
are in Brin's appendix in \citet[Appendix, Sec.~2 and~5]{Ballmann1995}.

If necessary we replace $M$ by an oriented finite cover: both
entropies and the local symmetry condition are unchanged, and the
conormal volumes become globally defined. Under this replacement
Lyapunov exponents and the normalized smooth entropy formula are
preserved; topological entropy is volume growth on the common
universal cover \citep{Manning1979}. We assume $M$ oriented.

Fix a time $T>0$ for which $f=\phi_T$ is ergodic for $m_L$
(such times exist for an ergodic flow), and set $m=n-1$. All finite
tensor norms use a fixed auxiliary metric; compactness makes the
choice immaterial. We will freely replace $T$ by a larger ergodic
time when a one-step contraction estimate is wanted.

\subsection{Leaf estimates and regular sets}

\begin{lemma}[Uniform smooth plaque charts]\label{pre:uniform-plaques}
The strong and weak stable and unstable foliations admit smooth
local plaque charts on uniform geometric neighbourhoods. At each
fixed finite order, their chart and inverse norms are uniformly
bounded, and their leaf jets depend continuously on the centre.
\end{lemma}

\begin{proof}
For every finite $r\ge2$, the orbit foliation is $r$-normally
hyperbolic: $d\phi_tX=X\circ\phi_t$ has uniformly bounded norm in
both directions, and the normal strong directions contract
exponentially. The Lipschitz tangent-field hypothesis of
\citet[Sec.~3, pp.~1017--1018]{HirschPughShub1970} gives $C^r$
laminations of stable and unstable manifolds of orbit leaves.
Compactness bounds the small-plaque parametrisations.

Contact form recovers the strong plaques at the same order.
Invariance and forward contraction give $\alpha(\Es)=0$,
$d\alpha(\Es,\Es)=0$, and $\iota_Xd\alpha=0$; hence $\alpha$ pulls
back to a closed form $\beta$ on each weak stable plaque. Its $C^r$
primitive $\tau$, normalised at the centre, satisfies $X\tau=1$.
The uniform implicit function theorem makes the level $\tau=0$ a
$C^r$ disk tangent to $\Es$; forward contraction carries it into the
genuine strong stable leaf, and local uniqueness identifies the two.
Reverse time for the unstable case.

The neighbourhoods may depend on $r$; remove that by uniformity.
Fix a small uniform $C^1$ strong plaque domain as a graph over its
central tangent plane. For each $r$, a fixed sufficiently long
iterate maps the whole domain into the uniformly controlled $C^r$
plaque at the image centre; pulling back by the smooth inverse
iterate gives uniform $C^r$ bounds on the original domain via the
implicit function theorem applied to the uniformly invertible
projection. The iterate may depend on $r$; the domain does not.
Thickening by a fixed bounded flow interval gives the weak charts.
\end{proof}

\begin{lemma}\label{pre:plaque-contraction}
On uniformly sized local strong stable plaques, expressed in smooth
plaque charts at the successive orbit points, every fixed positive
derivative order of $f^j$ decays exponentially. The analogue holds
for $f^{-j}$ on strong unstable plaques. On weak plaques in bounded
flow boxes, all fixed-order derivatives of the corresponding forward
or backward maps are uniformly bounded.
\end{lemma}

\begin{proof}
Since $f$ contracts the strong stable plaques with ratio $\rho<1$
at a suitable iterate, the first derivative of a length-$j$
composition is bounded by $\rho^j$. The second derivative is a sum
bounded by
$\sum_{i=0}^{j-1}\rho^{j-1-i}\rho^{2i}\le C\rho^{j-1}$.
At order $r$ the chain rule separates the linear term from lower
positive-order products; induction gives a geometric bound, absorbed
in $C_r$. Weak plaques use $(y,t)\mapsto\phi_ty$ over a strong
stable plaque with bounded flow coordinate, and smoothness of the
bounded flow boxes.
\end{proof}

We use the multiplicative ergodic theorem \citep{Oseledets1968} on
finite tensor and jet bundles. A measurable function $C\ge1$ on the
regular set is \emph{tempered} if $\log C(f^n v)/|n|\to0$ for all
regular orbits; a positive radius is tempered when its reciprocal
increased to $\ge1$ is tempered. Countably many regular-set
refinements are permitted, imposing all finite-order Oseledets data
and recurrence to the bounded positive-measure sets introduced
below.

We also adopt the leafwise-agreement convention. In a countable
foliation-box cover, disintegration and absolute continuity give
that a conull set meets almost every plaque in a conull set for its
intrinsic measure. Applying this to both strong foliations and their
weak versions, and intersecting over refinements and integer
iterates, gives: at a typical centre, every regular datum for
consideration agrees leaf-almost-everywhere on both entire strong
leaves. Extension to an entire leaf is always by smooth or
continuous extension separately, not a consequence of this
convention.

\subsection{Entropy and the conormal forms}

In contact Jacobi coordinates, $\ker\alpha_v\cong v^\perp\oplus v^\perp$,
a vector in it is a pair $(q,q')$. The unstable Riccati tensor
$U(v)$ is symmetric, uniformly positive definite, and satisfies
\begin{equation}\label{pre:riccati}
 XU+U^2+R_v=0, \qquad R_v(q)=R(q,v)v.
\end{equation}
The graphs of $U(v)$ and $-U(-v)$ are $\Eu_v$ and $\Es_v$
respectively. The tensor $U$ is Hölder on $SM$, with uniformly
bounded smooth leaf jets on weak unstable plaques. Set
$J=\tr U$.

\begin{proposition}\label{pre:entropy-forms}
The potential $-J$ has pressure zero, and Liouville measure is an
equilibrium state for $-J$. If
$h_{m_L}(\phi_1)=\htop(\phi_1)=h$, there is a Hölder $F$ with
\begin{equation}\label{pre:cohomology}
 J=h+XF.
\end{equation}
The function $F$ is $C^\infty$ on weak unstable plaques, with
uniform bounds at each finite leaf order. There are continuous
horizontal $m$-forms $u,w$ with $u$ annihilating $\Eu$ and $w$
annihilating $\Es$, such that
\begin{equation}\label{pre:volume-transport}
 \phi_t^*u=e^{-ht}u,\quad
 \phi_t^*w=e^{ht}w,\quad
 u\wedge w=c_*(d\alpha)^m,\quad c_*\ne0.
\end{equation}
The form $u$ has smooth uniformly bounded finite jets on weak
unstable plaques, and $w$ has the analogue on weak stable plaques;
the leaf jets vary continuously in uniform plaque charts.
\end{proposition}

\begin{proof}
The horizontal graph volume expansion rate is $J$; changing graph
volume changes the rate by a flow coboundary. Ruelle's inequality
\citep{Ruelle1978} gives
$h_\mu(\phi_1)\le\int J\,d\mu$ for every invariant probability
measure, while Pesin's formula is equality for $m_L$
\citep{Pesin1977}; the variational principle for pressure proves
the first assertion.

Assume entropy equality. Then $m_L$ is the equilibrium state both
for $-J$ and for the constant potential $-h$, each with zero
pressure. The flow is topologically transitive since $m_L$ has full
support. Thermodynamic formalism gives Gibbs bounds for ordinary
forward Bowen balls \citep{BowenRuelle1975}; we use the precise
version of \citet[preprint v2, Theorem~3.1 and Eq.~(1.5)]{Climenhaga2024}.
For a sufficiently small common Bowen radius, apply both bounds to a
common orbit ball centred on a periodic orbit of period $\ell$
observed over $k\ell$ units of time. The comparison bounds
$\left|k\int_0^\ell(J(\phi_tv)-h)\,dt\right|$ by
$\log Q_J+\log Q_h$, independent of $k$; dividing by $k$ proves
the integral vanishes on every periodic orbit. Livšic
\citep{Livsic1972} yields \eqref{pre:cohomology} with $F$ Hölder and
differentiable along the flow.

For $x,y$ on one local strong unstable plaque, Hölder continuity
and backward contraction give
\begin{equation}\label{pre:transfer-integral}
 F(y)-F(x)=\int_{-\infty}^{0}\bigl(J(\phi_ty)-J(\phi_tx)\bigr)\,dt.
\end{equation}
Every positive leaf derivative of the integrand decays
exponentially by \ref{pre:plaque-contraction} and bounded finite
leaf bounds on $J$. Differentiating under the integral proves the
strong-unstable assertion; the flow equation gives the flow
derivatives; interpolation preserves continuity in the plaque. This
is \emph{leaf jet} continuity, not transverse differentiability.

Let $\operatorname{vol}_{v^\perp}$ be oriented normal volume, and
define
\[
 u_v\bigl((q_1,q'_1),\ldots,(q_m,q'_m)\bigr)
 =e^{F(v)}\operatorname{vol}_{v^\perp}(q'_1-Uq_1,\ldots,q'_m-Uq_m),
 \qquad \iota_Xu=0.
\]
It annihilates $\Eu$. Jacobi plus \eqref{pre:riccati} gives
$\frac{d}{dt}(q'-Uq)=-U(q'-Uq)$; the determinant proves the first
transport identity. The flip $\iota(v)=-v$ has
$\iota\phi_t=\phi_{-t}\iota$, so
$w=\iota^*u$ has the opposite transport and leaf regularity. The
graphs are transverse, so $u\wedge w$ is nowhere zero on the contact
bundle, and its ratio with $(d\alpha)^m$ is continuous and invariant.
Ergodicity makes the ratio constant a.e.; full support of $m_L$
makes it constant.
\end{proof}

On a local transverse section, use flow-box coordinates $(p,\tau)$
with $X=\partial_\tau$. Invariance of the contact form gives
\begin{equation}\label{pre:section-conventions}
 \alpha=d\tau+\theta(p),\quad \omega=d\theta,\quad
 u=e^{-h\tau}u(p),\quad w=e^{h\tau}w(p).
\end{equation}
Here $\omega$ is symplectic. Changing the section includes the
height factors. All later constructions respect this convention.

\subsection{The classical final step}

The new argument will establish the hypothesis of the following
classical rigidity statement, whose proof appears in
Section~\ref{sec:completion}. There, period and volume identities
recover the metric from the smooth flow model.

\begin{proposition}\label{pre:smooth-rigidity}
If $\Es$ and $\Eu$ are smooth on $SM$, then $(M,g)$ is locally
symmetric.
\end{proposition}

\section{Contracting plaque jets and exact normal coordinates}
\label{nf:section}

\paragraph{Plain summary.}
At a stable crossing $v$, record the Taylor series (through order $j$)
of the unstable plaque $x=P(y)$ through $v$, together with the
Taylor series of the conormal density
$r(y)$. The pair $(P,r)$ is packaged as a ``state'' in a
finite-dimensional space $\mathcal E_j(v)$. Under the section map of
$f=\phi_T$, these states contract toward zero: the unstable plaque
is being viewed through its stable crossings, which shrink toward the
axis. The linear contraction is by sums of stable Lyapunov exponents.

But we want more than contraction: we want a polynomial model. This
section proves that under $f$, the state transformation is
\emph{exactly} conjugate to a polynomial diffeomorphism. Non-stationary
normal-form theory is the source; the proofs here are self-contained.

Three lemmas carry the weight:
\begin{itemize}
\item Lemma~\ref{nf:raw-dynamics}: the raw $j$-state transformation
  is polynomial in the hidden jets at fixed base, with explicit
  Lyapunov exponents. This is the $j$-jet analogue of the classical
  computation $D_yB(a,0)=D_xA(a,0)^{-t}$.
\item Lemma~\ref{nf:homological}: measurable linear recurrences with
  a single Lyapunov exponent have unique tempered solutions. This is
  the engine for the normal form.
\item Lemma~\ref{nf:normalization}: the raw transformation is exactly
  conjugate to a weight-preserving polynomial, with compatible
  measurable coordinates. The $j$-level towers forget compatibly.
\end{itemize}

Section~\ref{hull:section} will apply this to $\mathcal E_j$ to build
coherent formal fields.

\subsection{The raw graph and log-density towers}

Choose a transverse section at $v$, with symplectic coordinates
$(x,y)\in\R^m\times\R^m$ in which the central strong stable plaque
is $y=0$ and the strong unstable plaque is $x=0$. Both are smooth
transverse Lagrangians, so relative Lagrangian neighbourhood theory
provides these coordinates: straighten one plaque, then subtract the
differential of the other as a graph. The height coordinate is
chosen so that height zero agrees with both central strong plaques.
The section maps, height functions, and axis parametrisations have
uniform bounds at each finite smooth order on uniform smaller charts
(Lemma~\ref{pre:uniform-plaques}); no smooth dependence on $v$ is
required.

An unstable plaque crossing the stable axis at $(a,0)$ is written
$x=P(y)$, with $P(0)=a$. Its conormal form on the section is
\begin{equation}\label{nf:graph-form}
 e^{c(x,y)+r(y)}
 \bigwedge_{i=1}^m\biggl(dx_i-\sum_{q=1}^m\partial_q P_i(y)\,dy_q\biggr).
\end{equation}
Fixed nonzero units and orientation signs are suppressed; they are
retained as constants under a change of chart. The smooth function
$c$ is a background chosen so $r(0)=0$ for every actual crossing,
and $r=0$ along the central unstable plaque. Such a choice exists
without transverse smoothness: along the unstable axis $u$ is smooth,
and along the stable axis its coefficient in \eqref{nf:graph-form}
is the reciprocal of $w$'s coefficient in $\bigwedge dy_i$ (which
is also smooth along the stable plaque). The two logarithms agree
at the origin after adjusting the constant units. Extend
$c(x,y)=c(x,0)+c(0,y)-c(0,0)$; for the stable construction take the
background $-c$. Each background has uniform bounds at every fixed
order.

For $j\ge1$, define the raw state space $\mathcal E_j(v)$ with
coordinates
\begin{equation}\label{nf:raw-state}
 \bigl(a,p_1,\ldots,p_j,s_1,\ldots,s_j\bigr),
 \qquad p_l=D^lP(0),\quad s_l=D^lr(0).
\end{equation}
Set $\mathcal E_0(v)=\R^m$ with coordinate $a$; write
$\pi_{j,j-1}$ for the linear projection forgetting highest tensors.
These are unrestricted symmetric graph tensors and scalar tensors;
no Lagrangian equation is imposed on alternatives. Actual states
form a continuous graph over $a$; all finite jets are continuous
as functions of the centre by Lemma~\ref{pre:plaque-contraction}
and interpolation on plaques. The actual central state is zero at
every level.

\begin{lemma}[Raw dynamics and weights]\label{nf:raw-dynamics}
At every level $j$, the section map of $f$ induces a smooth
invertible germ $G_{v,j}:\mathcal E_j(v)\to\mathcal E_j(fv)$ fixing
zero. The $G_{v,j}$ commute with the $\pi_{j,j-1}$. The base
component depends only on $a$; other components are polynomials in
the hidden coordinates $(p_l,s_l)$ with coefficients smooth in
$a$. For fixed $j$ their degrees are bounded independently of the
length of a composition along the central orbit. The same holds for
changes of adapted charts.

Raw maps and their inverses have uniformly bounded norms at every
fixed order on suitable uniform raw domains. If
$-\chi_1,\ldots,-\chi_m<0$ are the stable Lyapunov exponents, and
$\chi_*=\min\chi_i>0$, then the derivative cocycle of $G_{v,j}$ at
zero has only negative exponents. In the quotient
$\ker\pi_{j,j-1}$ they are sums of $j+1$ stable exponents on graph
tensors and sums of $j$ stable exponents on density tensors. Their
negative exponents are therefore positive weights, each at least
$\chi_*$; new weights at level $j$ are at least $j\chi_*$.
\end{lemma}

\begin{proof}
Write the section map as $(A(x,y),B(x,y))$ and its height shift as
$\rho(x,y)$. It carries the stable axis to itself, so $B(x,0)=0$
and $D_xB(x,0)=0$. Symplecticity gives the identity
\begin{equation}\label{nf:axis-derivative}
 D_yB(a,0)=D_xA(a,0)^{-t}.
\end{equation}
Indeed the derivative on that axis is block upper-triangular, and
preservation of the pairing between the two coordinate planes gives
this identity. Put
\[
 Y(y)=B(P(y),y),\qquad P_*(Y(y))=A(P(y),y).
\]
Then $Y(0)=0$ and $DY(0)=D_yB(a,0)$, independent of $DP(0)$. Formal
inversion of the $j$-jet of $Y$ uses only powers of
$D_yB(a,0)^{-1}$, hence produces the transformed graph jet through
order $j$ as a polynomial in the hidden tensors, with smooth
coefficients in $a$.

For the density coefficient, let $M_*=DP_*(Y)$ and $x=P(y)$. Pullback
on the $x$-directions yields $\det(D_xA - M_*D_xB)$. Our height
convention says the pullback of the target section form is
$e^{-hT+h\rho}$ times the source form, so the transformed log
record is
\begin{align}
 r_*(Y)={}&r(y)+c(x,y)-c_*(A,Y)
 \label{nf:density-transport}\\
 &-\log|\det(D_xA-M_*D_xB)|-hT+h\rho(x,y)
       +\text{constant}.\notag
\end{align}
At $y=0$, the determinant is $\det D_xA(a,0)$, independent of hidden
tensors. The right side vanishes for actual states by actual
transport and the choice of backgrounds; it therefore vanishes for
every alternative with the same base $a$.

No missing $(j+1)$-st graph derivative enters
\eqref{nf:density-transport}. In $j$ derivatives of $M_*D_xB(P(y),y)$,
the term with all $j$ derivatives on $M_*$ is multiplied by
$D_xB(a,0)=0$; every surviving term uses at most $j-1$ derivatives
of $M_*$, hence at most $j$ of $P_*$. All logarithmic derivatives
use only powers of the nonzero base determinant. This closes the
density at order $j$ and gives polynomial dependence.

The computation is a universal finite-jet formula: it applies to any
smooth symplectic section map preserving the stable axis, and a
composition of any length is again such a map. The maximal
occurrence count of hidden tensors depends only on $j$, not on the
section map, proving the uniform degree bound. Applying the formula
to the inverse proves invertibility and the same finite-level
assertions.

It remains to identify the linear diagonal blocks. At the central
state, write $S=D_xA(0,0)$ and $U=D_yB(0,0)=S^{-t}$. The base
derivative is $S$. Modulo lower graph and density orders, the
highest graph tensor transforms by
$p_j\mapsto Sp_j(U^{-1}\cdot,\ldots,U^{-1}\cdot)$, and the highest
scalar tensor by $s_j\mapsto s_j(U^{-1}\cdot,\ldots,U^{-1}\cdot)$
(with a possible linear $p_j$ contribution). Thus the quotient
diagonal blocks are $S\otimes\mathrm{Sym}^j S$ and
$\mathrm{Sym}^j S$ with triangular coupling, and the exponents are
exactly sums of stable Lyapunov exponents. The multiplicative
ergodic theorem on the invariant order filtration gives no other
exponents. Since $j\ge1$, new weights are at least $j\chi_*$.
\end{proof}

The stable graph tower uses $f^{-1}$, exchanges $x$ and $y$, and
uses $w$ with factor $e^{hT}$ and background $-c$; the same proof
gives a second tower with positive minimum weight. Time indices
below always count iterates of the indicated map: $f$ for the
unstable-plaque tower, $f^{-1}$ for the stable one.

\subsection{Estimates and measurable choices}

\emph{Temperedness} was defined in Section~\ref{pre:section}. For a
single-exponent linear block $A$ (exponent $\lambda$), slow
regularization
$C_\epsilon(v)=\sup_{n\in\Z}C(f^nv)e^{-\epsilon|n|}$ gives
\begin{equation}\label{nf:lyapunov-bounds}
 C_\epsilon(v)^{-1}e^{(\lambda-\epsilon)n}\|z\|\le
 \|A_v^{(n)}z\|\le
 C_\epsilon(v)e^{(\lambda+\epsilon)n}\|z\|,\quad n\ge0.
\end{equation}
Tensor products add exponents; duals negate them.

For a finite triangular array with common-exponent diagonal blocks
and tempered one-step off-diagonal coefficients, the product obeys
the same estimates with slack $\epsilon$. Each entry is a path sum:
paths have at most $r-1$ off-diagonal jumps, giving a polynomial in
$n$ number of choices, and interval lengths sum to $n$ minus at
most $r-1$. Slow regularization absorbs the vertex contributions
into $C_\epsilon e^{\delta n}$ for any $\delta>0$. The triangular
inverse is identical. No logarithmic integrability of the
off-diagonal coefficients is used.

\begin{lemma}[Splitting invariant subspaces]\label{nf:blocks}
Let a measurable invertible linear cocycle have invariant direct
sum $E=\bigoplus_{i=1}^r E_i$ with distinct exponents
$\lambda_1<\cdots<\lambda_r$, each $E_i$ satisfying
\eqref{nf:lyapunov-bounds}. Every measurable invariant
$S\subseteq E$ satisfies $S=\bigoplus_i(S\cap E_i)$ almost
everywhere, with no temperedness assumption on $S$. The result also
applies to a cocycle over $f^{-1}$.
\end{lemma}

\begin{proof}
Use the measurable max norm $\|\sum_iz_i\|_\oplus=\max_i\|z_i\|$
(only measurability is needed). Write $E=E_<\oplus E_r$, put
$K=S\cap E_<$, $I=\mathrm{pr}_{E_r}S$. In quotient norms, $S/K$ is
the graph of a measurable $L:I\to E_</K$ obeying
$\|L_{f^nv}\|\le C_\epsilon(v)^2e^{(\lambda_{r-1}-\lambda_r+2\epsilon)n}\|L_v\|$.
For $2\epsilon<\lambda_r-\lambda_{r-1}$, $\|L_{f^nv}\|\to0$. For
$a>0$, invariance of the measure and dominated convergence give
$\mu\{\|L\|>a\}=\int 1_{\{\|L_{f^nv}\|>a\}}d\mu\to0$; hence $L=0$
a.e. Induct on $r$.
\end{proof}

\begin{lemma}[Nonresonant homological equation]\label{nf:homological}
Let $L$ be an invertible finite-dimensional measurable cocycle with
single exponent $\gamma\ne0$ satisfying \eqref{nf:lyapunov-bounds}.
For a tempered measurable $e$, the recurrence
$q_{n+1}=L_nq_n+e_{n+1}$ has a unique tempered solution on every
regular two-sided orbit. The solution is measurable. The result
extends to the single-exponent triangular blocks above.
\end{lemma}

\begin{proof}
For $\gamma<0$ set
$q_n=e_n+\sum_{j\ge1}(L_{n-1}\cdots L_{n-j})e_{n-j}$; for
$\gamma>0$ set
$q_n=-\sum_{j\ge0}(L_n^{-1}\cdots L_{n+j}^{-1})e_{n+j+1}$. Both
solve the recurrence by shifting the summation index. For
$0<3\delta<|\gamma|$, slow regularization bounds the $j$-th term by
$C_\delta(v)E_\delta(v)e^{2\delta|n|}e^{(\gamma+3\delta)j}$,
convergent, tempered as $\delta$ arbitrary. Partial sums are
measurable. Difference of two solutions is a homogeneous orbit;
nonzero such orbits grow exponentially in one direction,
contradicting temperedness.
\end{proof}

\subsection{Exact resonance normalization}

A \emph{graded space} is a finite direct sum $E=\bigoplus_{d>0}E_d$
with coordinates on $E_d$ having weight $d$. A polynomial map is
\emph{weight-preserving} if its $E_d$ component uses only monomials
of total weight $d$. Such a polynomial has degree $\le
d_{\max}/d_{\min}$, and its nonlinear $E_d$ component uses only
variables of weights $<d$, so weight induction gives a polynomial
inverse from any invertible linear diagonal.

\begin{lemma}[Exact compatible normal coordinates]\label{nf:normalization}
For the raw towers of Lemma~\ref{nf:raw-dynamics}, at every finite
level there exist measurable smooth germ coordinates $\Psi_{v,j}$
(tangent to identity) and weight-preserving polynomial
diffeomorphisms $N_{v,j}$ such that
\begin{equation}\label{nf:conjugacy}
 \Psi_{fv,j}\circ G_{v,j}=N_{v,j}\circ\Psi_{v,j}.
\end{equation}
Their linear parts are the raw derivatives with Oseledets grading.
Coordinates and normal maps commute with tower projections. At
every fixed state level and derivative order, tempered bounds on
norms and inverse norms exist on measurable tempered radii. At a
fixed level the coordinate change is $C^\infty$ on a forward
admissible domain; no single radius valid across all orders is
asserted.
\end{lemma}

\begin{proof}
Fix a finite level. $A_v=DG_v(0)$ has measurable Oseledets splitting
by weight $d$, exponent $-d$, and Oseledets projections commute with
the tower projections (a vector with one exponent can only project to
that exponent or zero). Work in adapted norms with
$\|A_v\|\le e^{-\chi_*/2}$.

\emph{Formal conjugacy.} Suppose built through degree $b-1$. The
degree-$b$ discrepancy is a homogeneous polynomial. Its
output-weight-$d$, input-weights-$(d_1,\dots,d_b)$ component lies in
the cocycle of homogeneous maps with linear transport
$Q\mapsto A_vQ(A_v^{-1}\cdot,\dots,A_v^{-1}\cdot)$, exponent
$d_1+\dots+d_b-d$. Nonzero: solve via \ref{nf:homological}; zero:
retain in $N_v$. Induction gives measurable tempered coefficients at
every finite order. Above $b>d_{\max}/d_{\min}$ no resonances
remain and $N_v$ is a finite weight-preserving polynomial. Tower
compatibility: project the degree-$b$ equation (raw projection is
linear and intertwines the derivatives) to get the lower-level
equation. Nonresonant parts agree with the lower correction by
\ref{nf:homological} uniqueness; resonant parts both zero and the
projected discrepancy retained.

\emph{Exactification.} Choose $r_v>0$ tempered with
$\|DG_v\|\le e^{-\kappa}$, slowly shrink radii so
$r_{fv}\ge e^{-\delta}r_v$ for $0<\delta<\kappa$; then
$G_v(B(0,r_v))\subset B(0,r_{fv})$. On these forward-admissible
balls,
\begin{equation}\label{nf:raw-contraction}
 \|G_v^{(n)}(z)\|\le e^{-\kappa n}\|z\|.
\end{equation}
Fixed-order derivative bounds for $G_v^{(n)}$ are tempered with
arbitrarily small slack: differentiate $G_v^{(n+1)}=G_{f^nv}\circ
G_v^{(n)}$; the term containing $D^qG_v^{(n)}$ is multiplied by
$DG_{f^nv}$, all other terms are lower-order products with tempered
coefficients.

Inverse normal iterates as polynomials:
$N_v^{(-n)}$ has coefficients $\le C_\epsilon(v)e^{(K+\epsilon)n}$
with $K=d_{\max}$. On weight-$d$ monomials, substitution is
triangular with diagonal exponent $-d$; the triangular-array
estimate bounds forward by $e^{(-d+\epsilon)n}$ and inverse by
$e^{(d+\epsilon)n}$.

Define
\begin{equation}\label{nf:limit-formula}
 Q_{v,n}^{[b]}=N_v^{(-n)}\circ\Psi_{f^nv}^{[b]}\circ G_v^{(n)}.
\end{equation}
Let $\Psi_v^{[b]}$ be the degree-$b$ truncation; its defect
$R_v^{[b]}=\Psi_{fv}^{[b]}G_v-N_v\Psi_v^{[b]}$ vanishes through
$b$ and has tempered $C^q$ norms. Consecutive $Q$'s differ by
applying $N_v^{(-n-1)}$ to two arguments differing by
$R_{f^nv}^{[b]}\circ G_v^{(n)}$; Taylor plus
\eqref{nf:raw-contraction} give, with $q\le k$ derivatives on
$R^{[b]}$ and the Taylor factor of order $b+1-q$,
\begin{equation}\label{nf:telescoping}
 \|Q_{v,n+1}^{[b]}-Q_{v,n}^{[b]}\|_{C^k}\le C_{b,k,\epsilon}(v)
 e^{[K-\kappa(b+1-k)+\epsilon]n}.
\end{equation}
Choose $b_0$ with $\kappa(b_0+1)>K$: summable in $C^0$ there, and
for each $k$ a larger $b$ gives $C^k$ summable. Induction on
truncation order gives smoothness. Increase $b$ without changing
the domain: each $\Psi^{[b]}$ is polynomial and all raw derivatives
are bounded on raw domains; on compact subsets of the forward
interior the estimates apply directly, smaller future radii are
handled by \eqref{nf:raw-contraction}.

The identity $Q_{v,n+1}^{[b]}=Q_{fv,n}^{[b]}\circ G_v$ passes to the
limit as \eqref{nf:conjugacy}. Telescoping differences have zero
Taylor jet through $b$, so $j^a\Psi_v=j^a\Psi_v^{[b]}$ for $b\ge a$;
in particular $D\Psi_v(0)=\id$. Summing \eqref{nf:telescoping}
gives tempered fixed-order bounds; inverse-function theorem at
successive orders gives inverse bounds. Projection commutes with
\eqref{nf:limit-formula} at sufficiently large common truncation,
hence with the limits.
\end{proof}

\subsection{Fiber polynomiality and finite weight blocks}

\begin{lemma}[Analyticity only in hidden variables]\label{nf:fiber-analyticity}
At every fixed state level, $\Psi_{v,j}$ is polynomial in the raw
hidden variables at fixed raw base $a$, with smooth coefficients in
$a$. Write normalized variables as $(z_0,\zeta)$, where $z_0$ is
the level-zero coordinate. The local inverse of $\Psi_{v,j}$ is
$C^\infty$ in $z_0$ and real analytic in $\zeta$. Every fixed
derivative in $(z_0,\zeta)$ has this same analyticity in $\zeta$.
No analyticity in the base or the centre is asserted.
\end{lemma}

\begin{proof}
Fix $b_0$ with \eqref{nf:limit-formula} $C^0$-convergent. By
\ref{nf:raw-dynamics}, $G_v^{(n)}$ has hidden degree at most $D_j$
(independent of $n$), with base component independent of hidden
variables. $\Psi_{f^nv}^{[b_0]}$ has degree $\le b_0$; the inverse
normal iterate is weight-preserving of degree $\le L_j =
d_{\max}/d_{\min}$. Thus $Q_{v,n}^{[b_0]}$ has hidden degree at
most $D_jb_0L_j$. Polynomials of bounded degree form a closed
finite-dimensional space; the $C^0$ limit is polynomial of this
degree with smooth coefficients in $a$.

Compatibility with level zero gives
$\Psi_v(a,\eta)=(\psi_v(a),F_v(a,\eta))$ with $\psi_v$ a smooth
local diffeo and $F_v$ polynomial in $\eta$. At fixed $a$ its
hidden derivative is invertible near zero, so the real analytic
inverse theorem gives $\eta=H_v(a,\zeta)$ real analytic in $\zeta$;
the smooth parameter inverse theorem identifies it as jointly
smooth. Differentiating $F_v(a,H_v(a,\zeta))=\zeta$ in $a$ gives
$\partial_aH_v=-(D_\eta F_v)^{-1}\partial_aF_v$, analytic in $\zeta$
since $F_v$ and its base derivatives are polynomial in $\eta$.
Induction handles all mixed derivatives. Substituting
$a=\psi_v^{-1}(z_0)$ proves the claim.
\end{proof}

\begin{corollary}[Finite arrays and higher kernels]\label{nf:finite-weight}
In either normalized tower, independent coordinates at level $j$
have weights $\ge j\chi_*$. A fixed upper weight bound uses only
finitely many levels and monomials. On the array of weight-$d$
monomials, normal substitution has single exponent $-d$ and inverse
substitution $d$, with two-sided estimates and arbitrarily small
slack; the same holds for finite tensor arrays and invariant
subquotients.
\end{corollary}

\begin{proof}
New weights at level $j$ are $\ge j\chi_*$ by \ref{nf:raw-dynamics}
and preserved by \ref{nf:normalization}'s compatible grading. The
ordinary degree of a weight-$\le D$ monomial is $\le D/\chi_*$;
only levels $j\le D/\chi_*$ contribute independent variables, of
finite dimension. Substitution is triangular by ordinary degree on
each fixed-weight array, with diagonal consisting of tensor
products of derivative blocks of total exponent $-d$; triangular-
array estimates give the forward and inverse bounds. Tensor
operations add or subtract exponents; restriction preserves upper
bounds and the inverse supplies lower bounds, and both pass to
quotient norms.
\end{proof}

The corollary concerns finite arrays. It allows a later argument to
fix a weight cutoff, choose a sufficiently large spatial Taylor
order, and then pass to an orbit limit. It does not identify an
infinite formal series with a convergent spatial germ.

\section{Algebraic hulls and coherent formal fields}
\label{hull:section}

\paragraph{Plain summary.}
At each typical centre, the actual unstable plaque and its
conormal density satisfy algebraic relations that are invariant
under the dynamics (their algebraic hull is a variety $V_j$). By
taking the \emph{Zariski closure} of the actual jets, we get a
variety of ``alternative plaque jets'' that share the same
relations but need not be realizable by actual plaques. A
$d$-dimensional affine family of alternatives, once completed to
full ambient Taylor series, is a \emph{formal affine field}.

The miracle of this section: the formal affine fields can be
completed to full ambient Taylor coefficients that are smooth and
holonomic along entire strong leaves, and that are compatible with
flip, with changes of section, and with the dynamics. This gives us
formal objects to which we can apply symmetry and Lie theory, even
though the underlying bundles $\Es,\Eu$ are only measurable.

\subsection{Formal subbundles and holonomicity}

A formal rank-$d$ subbundle is represented by $d$ formal columns
with a nonzero $d$-minor at the centre, modulo invertible formal
changes of frame. An affine subbundle is a linear subbundle after
adding a scalar slot and intersecting that slot with $1$.

For holonomicity, use fixed ambient coordinates and a Grassmann
chart. Let $B_\beta(a)$ be the derivative coefficient of multi-order
$\beta$ at $a$ on an axis. Along a smooth axis path $a(t)$,
\begin{equation}\label{hull:coherence-eq}
 \frac{d}{dt}B_\beta(a(t))=\sum_i\dot a_i(t)B_{\beta+e_i}(a(t)).
\end{equation}
Coefficients are actual derivatives, not factorial-divided Taylor
coefficients. This condition is independent of the ambient and
Grassmann charts by the chain rule. The higher coefficients on the
right retain their ambient indices; no transverse differentiability
is asserted.

\subsection{The Zariski variety of actual jets}

Let $V_j(v)$ be the real Zariski closure of the germ at $0$ of the
actual states in normal coordinates (equivalently, the complex
Zariski closure of the real evaluations, with real structure
restored). Noetherianity says a small actual-state neighbourhood
already has this closure. Normal dynamics identifies $V_j(v)$ with
$V_j(fv)$.

For a cutoff $D$, let $\mathbf e_{j,D}(z)$ be the vector of all
monomials of weight $\le D$ including constants. Its evaluation span
on the actual germ is $S_{j,D}(v)$. Weighted substitution by
$N_{v,j}$ is an invertible linear cocycle with sole exponent $-d$ on
each weight-$d$ block. Lemma~\ref{nf:blocks} gives
\begin{equation}\label{hull:span-splitting}
 S_{j,D}(v)=\bigoplus_{d\le D}S_{j,D}(v)_d.
\end{equation}
The annihilator of $S_{j,D}$ is the space of polynomial relations;
the ideal of $V_j(v)$ is weighted homogeneous.

\begin{lemma}\label{hull:regular-varieties}
After a conull refinement, all $V_j(v)$ are irreducible and smooth
at zero; their projections onto lower levels (including the full
base) are submersions at zero. Nearby regular centres on the stable
axis have variety germs identified by Lemma~\ref{hull:recenter}.
These objects and all finite-dimensional ranks used below are
measurable.
\end{lemma}

\begin{proof}
For each finite array the evaluation span is measurable: evaluate
the continuous actual graph on a countable dense set in successively
smaller base balls and take the stabilised finite-dimensional span.
Its annihilator gives the measurable space $I_D$ of relations of
ordinary degree $\le D$. In $\C^N$, the dimension $d$ of the
closure is the largest size of a coordinate subset $S$ such that
$I_D\cap\C[z_i:i\in S]=0$ for every $D$ (a maximal-dimensional
irreducible component has a transcendence-basis subset among its
coordinates; conversely, if every component has a nonzero relation
in $S$, the product of finitely many lies in the full ideal). This
uses only countably many finite-dimensional intersection ranks; see
\citet[Tag~00P0]{StacksProject}.

For the projection assertion, proceed through the levels. The
projection of the actual germ is the lower actual germ, so its image
is Zariski dense in the lower irreducible variety. In characteristic
zero the dominant projection has full rank on a nonempty open part
of the smooth locus. The actual-point and re-centring argument
gives a positive leaf-measure patch of centres with full projection
rank; conditional-null contradiction applied to this invariant rank
condition proves the central submersion a.e. (\citet{Hartshorne1977};
\citet[Tags~0B8X, 07ND, 02K4]{StacksProject}).

Complexification introduces no additional component problem. A
selected real actual point outside the other components belongs
both to its component and to the complex conjugate of that
component; the two coincide, so the component is real. The selected
point is nonsingular; its real locus is Zariski dense and locally
smooth of real dimension $=$ complex dimension
\citep[Thm~2.2.9(2)]{Mangolte2019}. Density of the actual
evaluations comes from the above. Irreducibility plus equal
dimension makes the local inclusions from polynomial re-centring
equalities of germs. Intersect conull sets over the countably many
levels and finite tests.
\end{proof}

We always restrict to smooth submersion neighbourhoods. In raw
coordinates, $(a,t_j)$ are smooth in all variables and analytic in
$t_j$ for fixed $a$, including any fixed derivatives in $a$ (by
Lemma~\ref{nf:fiber-analyticity}; the parameterised implicit
function theorem preserves it).

At a typical centre, take the fibre $a=0$ of $V_1(v)$. Its elements
give unstable conormal alternatives at that point with the
prescribed zero-order density. Higher levels give the same fibre
germ at this level, by submersion. Define stable alternatives in the
opposite tower, supplied by alternative state records. We first
prove their cross-pairing identity, then build from their affine
spans formal fields of constant rank.

\begin{lemma}[Homogeneous parameters]\label{hull:parameters}
The smooth germs $V_j(v)$ have compatible positively weighted
polynomial parametrisations. Independent parameters can be
introduced successively with the state levels; their new weights
tend to infinity with the level. A finite collection of independent
parameters extends to the tower by setting all later independent
parameters to zero. If their weights are at most $D_0$, a component
of weight $d$ on this section has ordinary vanishing order at least
$d/D_0$.
\end{lemma}

\begin{proof}
The tangent spaces at zero are graded with surjective projections.
Choose graded linear retractions onto them compatibly with the
projections. The local graph over the tangent space is invariant
under positive weighted dilation. Taylor expansion at zero makes
each output coordinate weighted homogeneous: the Taylor remainder,
pulled toward zero by dilation and divided by the fixed output
weight, tends to zero once the Taylor order is high enough. Choose
successive graded complements for tangent kernels. Their weights are
among those of new raw derivative blocks, whose minimum tends to
infinity by the raw jet computation. Finally a monomial of ordinary
degree $q$ in parameters of weights $\le D_0$ has weight at most
$qD_0$.
\end{proof}

\subsection{Extraction from transported actual states}

\begin{lemma}[Exponential extraction]\label{hull:evaluation}
Fix a finite level and weight cutoff. Transport actual states from
negative returns to the target chart. The evaluated vectors on the
variety $V_j$ project onto the whole span $S_{j,D}$ with error
decaying exponentially, when the return set is chosen with positive
frequency.
\end{lemma}

\begin{proof}
Every basis state is actual, and its transport is an actual state in
the target chart. Forward admissibility and a positive minimum
weight give exponential convergence to zero. Projection surjectivity
follows because evaluation vectors project to evaluation vectors on
the same actual germ. \eqref{hull:span-splitting} gives the result
weight by weight. Larger cutoffs may change the conditioning
constant and return set but not the exponent $d$.
\end{proof}

Positive-frequency returns are used throughout. For two towers, we
can take positive and negative return times in $[N,2N]$ for large
$N$; the ergodic theorem gives a positive asymptotic count on each
such interval. All choices in Lemma~\ref{hull:evaluation} are at
finite levels, so a countable refinement suffices.

\begin{lemma}[Smooth vs.\ fibre identities]\label{hull:identities}
If a smooth function vanishes on the local actual states, its
Taylor series at a typical centre vanishes on the formal germ of
$V_j$. Moreover, if a function on a local smooth piece of $V_j$ is
smooth in the base and analytic on each fibre, and vanishes on the
nearby typical actual states, it vanishes on a product neighbourhood
with connected fibres. The same applies to each finite coefficient of
a formal calculation with this regularity.
\end{lemma}

\begin{proof}
Fix the relevant finite collection of actual states and normalising
changes. Lemma~\ref{hull:parameters} writes the reachable part of
$V_j$ as a graph of a positive-weight polynomial over a full base
ball, with connected fibres near zero. A smooth function vanishing on
the actual germ vanishes also on its smooth variety closure. Restrict
to one fibre and fix a base: the function is real analytic in the
hidden parameters and vanishes on the actual hidden slice, which is
Zariski dense in the fibre. Analytic continuation proves the holomorphic
vanishing at order zero. Differentiating the identity in the base and
in positive-weight hidden directions writes every finite jet at a
typical actual point; the low-weight coordinates have zero constant
term. Induction on ordinary order uses that derivatives of a
real-analytic function are real analytic and that the closure of the
actual state passed through several compatible normalisations
remains the corresponding Zariski closure. A nonzero smooth function
would give a nonzero analytic restriction with nonzero evaluation
array, contradicting Lemma~\ref{hull:evaluation}.
\end{proof}

\begin{proposition}[Wedge identity]\label{hull:pairing}
Every sufficiently small unstable alternative and stable alternative
through the centre have the same wedge as the actual pair. Same for
their affine spans.
\end{proposition}

\begin{proof}
Use paired charts and density backgrounds of
Section~\ref{nf:section}. Transport one actual unstable plaque from a
negative return and one actual stable plaque from a positive return;
write their equations as $x=P(y)$ and $y=P^-(x)$, with log-density
records $r(y),r^-(x)$. At their unique nearby intersection, the
actual identity is
\begin{equation}\label{hull:actual-wedge}
 e^{r(y)+r^-(x)}\det\bigl(I-DP(y)DP^-(x)\bigr)=1.
\end{equation}
The two backgrounds cancel at the same point. Base labels and slopes
tend exponentially to zero, so the implicit intersection derivative
is uniformly invertible.

Fix a desired pair of weights $(d,d')$. First truncate spatial graphs
and density records at large $R$. Actual plaque derivatives are
uniformly bounded at every fixed order. Spatial truncation changes
the intersection and the LHS of \eqref{hull:actual-wedge} by at most
$C_R(|x|+|y|)^{R-1}$; the loss of one derivative accounts for the
slopes. Since $n,n'$ are comparable, this is smaller than
$e^{-(d+1)n-(d'+1)n'}$ when $R$ is sufficiently large. The truncated
intersection calculation is smooth in finitely many state
coordinates. Taylor-expand to high enough ordinary order that the
remainder has the same bound. All low biweight components stabilise
as these orders increase, because formal intersection displacements
have zero constant term and every state weight is positive.

Take product evaluation arrays containing every term of this finite
polynomial. Pure-weight extraction on the two arrays has coefficient
cost $\le e^{(d+\epsilon)n+(d'+\epsilon)n'}$. The exact identity on
actual plaque pairs plus the two remainder bounds force the
$(d,d')$ component to vanish on the product of the two varieties.
This proves the formal identity at every finite order.

Restrict to the two zero-base fibres: intersection equations have the
solution $x=y=0$ identically, so only the slopes and prescribed
zero-order densities remain. Arbitrary low-level fibre germs lift to
every higher finite level used in the test. Fibre analyticity
upgrades the formal identity to an identity near the actual pair.
Bilinearity gives the same constant on affine combinations.
\end{proof}

\subsection{Transport in the opposite direction}

The centred alternatives satisfy the wedge identity. To turn their
affine spans into formal fields we must also move the construction
along the central unstable plaque. Polynomial re-centering on the
stable axis does not provide this step, because the normal coordinates
are only measurable in their centres.

We construct a graph-and-density family
$\Phi_v(z,y)=(P_z(y),r_z(y))$: $y$ is an actual coordinate on a small
central unstable patch, $z$ denotes formal normal-state parameters,
and at parameter zero the coefficient is the actual central plaque
record. We first construct smooth spatial coefficients with the
prescribed state jets. Then we compare their finite weight truncations
with transported actual plaques at arbitrary prescribed exponential
accuracy. That comparison will let us test the polynomial relations
at a displaced centre using actual evaluations.

Denote the positive minimum state weight by $w_0$. A weight cutoff
$W$ leaves a finite-dimensional algebra of parameter polynomials
with products of weight greater than $W$ set to zero, nilpotent of
index $\le 1+\lfloor W/w_0\rfloor$. A ``parameter series with
smooth spatial coefficients'' means a compatible family of finite
weight truncations, without any convergence assertion in the
parameters. On a homogeneous tower section from
Lemma~\ref{hull:parameters}, each finite ordinary parameter jet
involves only finitely many weights and hence finitely many levels.

\begin{lemma}[Finite coefficient graph calculus]\label{hull:calculus}
Fix a weight cutoff $W$ and a target spatial derivative order $k$.
There exist integers $r=r(W,k)$ and constant $C=C(W,k)$ with: pushing
a weight-truncated graph and log-density variation from time $-l$ to
the target along the central unstable graph requires only source
spatial derivatives through order $r$ at the contracted central
preimage. Comparing two such inputs of tempered finite coefficient
norm costs at most $e^{Cl+\epsilon l}$ in target $C^k$ norm. The
constants $r,C$ are independent of the spatial Taylor degree used to
specify the inputs.
\end{lemma}

\begin{proof}
Put $q=\lfloor W/w_0\rfloor$. The parameter-zero term is the actual
central graph, kept exactly. In the graph-parameter equation solve
degree zero first; each successive degree is found by inverting the
same central graph Jacobian and substituting lower degrees. At degree
$\le q$, Taylor substitution uses at most $q$ source spatial
derivatives. Target derivatives add finitely many more; the density
Jacobian adds one. Any $r\ge k+2q+4$ suffices when all operations are
differentiated together.

The composed section map, height function, and inverse central graph
parametrisation have derivatives through every fixed order bounded
by $e^{A_r l}$, by induction from bounded one-step derivatives and the
chain rule at fixed derivative count. Substitution of $N^{-l}z$ on
the weight-$W$ array has norm $\le e^{(W+\epsilon)l}$ by its
triangular single-weight estimates. Every coefficient of the nilpotent
calculation is a fixed finite sum of products of these quantities,
input derivatives, and central inverse Jacobians; the number of
factors is bounded in $W,k$. Differences are estimated by replacing
one factor at a time. Input bounds are tempered, so after choosing
smaller exponential slack for finitely many factors, costs are
bounded by $e^{Cl+\epsilon l}$. The spatial Taylor degree does not
enter the number of parameter operations or the required derivative
order $r$.
\end{proof}

\begin{lemma}[Smooth spatial profiles]\label{hull:profiles}
There is a parameter-formal family $\Phi_v(z,y)$ of graph and
log-density records, with smooth coefficients in $y$ on a fixed small
patch of the central unstable axis. Its Taylor series at $y=0$ is the
prescribed tower of raw states. It is exactly equivariant, coefficient
by coefficient, for the section dynamics and $z\mapsto N_vz$. For
every fixed weight cutoff and spatial order, coefficient norms are
tempered along the central orbit.
\end{lemma}

\begin{proof}
Fix $W$. Work first in the ambient normal-state tower; restrict to
varieties afterward. By Lemma~\ref{nf:finite-weight}, choose a level
$j_0$ beyond which all new kernel weights exceed $W$. For $j\ge j_0$,
let $\pi:\mathcal E_j\to\mathcal E_{j_0}$ be the projection, and let
$\Pi_j,\Pi_{j_0}$ be the spectral projections onto weights $\le W$.
If $\mathcal R_j$ is a bounded raw right inverse of $\pi$, then
\[
 \pi\Pi_j\mathcal R_j=\Pi_{j_0}\pi\mathcal R_j=\Pi_{j_0},
\]
because $\ker\pi$ has no weight $\le W$. Thus
$\Pi_j\mathcal R_j\big|_{\operatorname{im}\Pi_{j_0}}$ is the inverse
of the low-weight projection, with tempered norm. Stabilised
low-weight inputs supply arbitrarily high spatial jets with tempered
bounds at each fixed higher level, without a measurable choice of
parameters for $V_j$.

Iteratively solve the graph equation by parameter degree. The
parameter-zero coefficient is the actual central graph, kept
exactly; each successive degree inverts the same central graph
Jacobian, evaluated on a contracted source preimage, and substitutes
lower degrees. Degree truncation of the weight algebra makes this a
finite computation at every stage. Lemma~\ref{hull:calculus} bounds
each stage's cost and its spatial derivatives. Equivariance is
coefficient-by-coefficient by the universality in
Sec.~\ref{nf:section}. Density coefficient handled identically, one
extra derivative.
\end{proof}

\begin{lemma}[Approximation of actual transported plaques]
\label{hull:actual-approximation}
Fix a target norm: graph derivatives through $k+1$, log-density
through $k$, and $K>0$. For a sufficiently large weight cutoff $W$
and sufficiently high finite state level, the following holds. Start
at a negative return $-n$ with an actual state in a bounded small
forward-admissible domain, and transport its actual plaque to the
target. On a fixed smaller central unstable patch, substituting its
target normal coordinates into $\Phi_v$ truncated through weight $W$
approximates that plaque in the prescribed norm with error at most
$Ce^{-Kn}$. The level, cutoff, and constant may depend on $k,K$.
\end{lemma}

\begin{proof}
Source at time $-n$, consider only times from $-\lfloor n/2\rfloor$
to zero. On every fixed finite normal array, a monomial of weight $d$
in the transported state is bounded by
\begin{equation}\label{hull:half-small}
 C_\epsilon e^{-dn/2+\epsilon n}
\end{equation}
throughout the last half. Finite arrays fixed before taking $n$
large; slack divided among finitely many coefficients. Slow
regularisation bounds every fixed tempered conversion factor by
$C_\epsilon(v)e^{\epsilon n}$ on this interval.

Common geometric patch. The actual crossings remain on the stable
axis. At a crossing, the inverse unstable parameter differential
over a block is the transpose of the contracting stable-axis
differential: $D_xB(x,0)=0$ and symplecticity give
$D_yB(x,0)=D_xA(x,0)^{-t}$. Choose a fixed block length making this
inverse norm $<1/4$ after bounded chart conversions. Uniform finite
derivatives of actual plaques and the fixed block map extend the
inverse contraction to a fixed small parameter ball with norm $<1/2$.
In the last half the crossings tend uniformly to zero, so the same
ball is available for all sufficiently large $n$. Shorter intermediate
blocks cost boundedly. Hence a fixed small final patch has true
inverse arguments of size
\begin{equation}\label{hull:half-arguments}
 |y_{-\lfloor n/2\rfloor}|\le Ce^{-\gamma_1 n}
\end{equation}
at halfway, for fixed $\gamma_1>0$.

Fix the low-order comparison domain before choosing $W$: graph jets
through $k+2$, density jets through $k+1$, in a compact neighbourhood
of the bounded central jets, with graph Jacobians bounded away from
singularity. True jets lie there after shrinking the patch. Let
$L_k\ge2$ bound the one-step jet transformation and its first
derivatives on a slightly larger domain. This uses only fixed low
orders and uniform raw geometric bounds.

Choose $W$ large enough that half-arguments plus
\eqref{hull:calculus} at these $L_k$ bounds give exponential accuracy
$e^{-Kn}$ for the target norm in the final patch. Increase the state
level for the spatial jets and apply \eqref{hull:profiles} with
$e^{-Kn}$-accuracy. Summing over the last half gives the claimed
approximation; earlier intermediates absorbed by slack.
\end{proof}

\begin{lemma}[Polynomial re-centering]\label{hull:recenter}
Fix a state level $j$ and Taylor order $b$. For every sufficiently
small stable-axis displacement $v'$ from the centre $v$ (i.e.\ in
$\Ws(v)$): (i) the chart translation between normal coordinates at
$v'$ and at $v$ is a polynomial change of bounded degree; (ii) the
variety germ $V_j(v')$, pulled back to $v$'s chart, equals the
image of $V_j(v)$ under this polynomial map modulo terms of Taylor
order $>b$; (iii) all these polynomial changes, and all their
derivatives through order $b$, are smooth along the stable axis
with uniform bounds on small patches.
\end{lemma}

\begin{proof}
Normal coordinates at $v'$ and at $v$ are related by the section map
and its derivative, which in raw charts is polynomial in the raw
state variables at fixed base (Lemma~\ref{nf:fiber-analyticity}).
Translation between fibres is polynomial of degree at most $b$
after truncation. Truncating at order $b$ preserves the actual
germ modulo $b$-th order; the variety is Zariski closure, and the
polynomial map $p\mapsto V_j$ is smooth in $v'$ along the stable
axis by the same fibre-smoothness. The truncation commutes with the
algebraic operations defining $V_j$ up to terms of order $>b$
because truncation is a ring homomorphism onto the polynomial
quotient of degree $\le b$. Smoothness of coefficients uses raw
smoothness along the stable axis (Lemma~\ref{pre:uniform-plaques}
and \ref{nf:raw-dynamics} for uniformity). Derivatives through
order $b$ in the stable-axis direction commute with the polynomial
truncation.
\end{proof}

\subsection{Constrained spans and the formal affine fields}

Fix $d\ge1$. Augment the state space by a scalar slot as in the
discussion after \eqref{hull:span-splitting}. At a typical centre,
the unstable alternatives at parameter zero span a $d$-dimensional
subspace $S_0$ of the augmented evaluation space; call this the
\emph{constrained span}. By Lemma~\ref{hull:evaluation} and the
definition of $V_j$, this is exactly the span of the affine $0$-fibre
of $V_1(v)$ plus the unit scalar slot.

At a nearby typical centre on the stable axis, transport the
constrained span via Lemma~\ref{hull:recenter}. Since re-centring is
polynomial in hidden variables and smooth on the stable axis, the
constrained span moves smoothly and is coherent at every finite
ambient order. Formally, we get a section of the augmented
tautological bundle whose value at parameter zero is the actual
augmented conormal form:
\begin{equation}\label{hull:point-constraint}
 S^\varepsilon(a)+\R e_{\mathrm{aug}} = \text{constrained span}_a.
\end{equation}
Combining with the pair identity from the wedge identity above
(Proposition~\ref{hull:pairing}) and with Lemma~\ref{hull:recenter},
the span at every nearby typical centre has the same dimension $d$
and is continuous in the stable-axis direction.

Now choose independent generators: a matrix $B$ whose columns are
$d$ independently chosen generators of the constrained span, in a
formal section chart. A $d$-minor of $B$ is a formal unit at
parameter zero, and by continuity remains a unit in a formal
neighbourhood. The symplectic wedge identities of
Proposition~\ref{hull:pairing} force every alternative to lie in the
free module generated by $B$; hidden differentiability of $B$ gives
\begin{equation}\label{hull:constant-rank-eq}
 \partial_{t_j}B = BC_j
\end{equation}
for formal coefficient matrices $C_j$ (after normalising the chosen
$d$-minor to identity, so that $\partial_{t_j}$ acts as zero on that
minor's rows).

\begin{lemma}[Constant rank]\label{hull:rank}
At every regular typical centre, and at every finite ambient order,
the augmented constrained span has constant formal rank $d$. The
generators can be chosen independently of all hidden parameters, and
the resulting formal subbundle is thus well-defined on a neighbourhood
of the centre in the stable axis.
\end{lemma}

\begin{proof}
Equation \eqref{hull:constant-rank-eq} says that $\partial_{t_j}$ of
the generator columns lies in the span of the columns at each
parameter value; hence the span does not change with $t_j$ as a
finite-dimensional subspace of the ambient finite-jet quotient. The
chain rule under invertible reparametrisation of $t_j$ and changing
the lift level gives the same derivative span in both directions.

For each fixed ambient order, choose a level $j$ high enough to
contain every term of that order; the unit-minor description makes
the resulting finite-level jets consistent. Retaining the base
variable $x$ as an actual smooth variable and expanding only in $y$
in \eqref{hull:point-constraint} gives smooth coefficients on the
stable axis whose base derivatives coincide with their higher ambient
coefficients. Lemma~\ref{hull:recenter} gives smoothness of the
coefficient matrices.
\end{proof}

Intersect the augmented linear bundle with scalar slot $1$: it
defines the formal affine field $\mathcal A^u$. The scalar-$1$
intersection is nonempty at the centre because it contains the actual
unstable form. The same unit-minor description makes it a formal
affine bundle on the local germ.

\begin{lemma}[Coherence on both axes]\label{hull:coherence}
The full ambient jets of $\mathcal A^u$ have smooth holonomic
representatives along both entire typical strong axes. They agree
with the regular construction almost everywhere and are compatible
with the dynamics, changes of section, and regular flow translations.
\end{lemma}

\begin{proof}
Stable-axis agreement at nearby typical centres follows from
Lemma~\ref{hull:recenter} and the intrinsic constrained-span
description. Smooth stable-axis coherence was proved in
Lemma~\ref{hull:rank}.

To cover an entire typical stable leaf, fix a finite collection of
orders. Local smooth representatives have a positive radius at almost
every centre. Choose forward returns on which that radius is bounded
below and the required finite construction bounds are bounded above.
Every compact portion of the central stable leaf contracts into these
patches; pull the representatives back. Two pulled representatives
agree on the dense set of typical points, hence everywhere. The same
argument backward in time covers the entire unstable leaf. Repeat one
finite collection of orders at a time. Agreement of orders and their
derivative identities follows on overlaps by density and smoothness;
this does not require a single radius valid at all orders.
Measurability of the radii used here is established in
Lemma~\ref{hull:measurability}.
\end{proof}

\begin{lemma}[Measurable finite-order bounds]\label{hull:measurability}
The construction and the representatives in Lemma~\ref{hull:coherence}
admit measurable finite-order norm and radius tests. Smooth flow
transport supplies coherent representatives on typical weak plaques,
agreeing leaf-almost-everywhere with the regular data. For almost
every individual strong or weak plaque, every fixed finite collection
of coefficient norms is finite on each compactly contained plaque
subpatch. Positive-measure families of these plaques can therefore be
chosen with a common finite bound on the prescribed subpatches.
\end{lemma}

\begin{proof}
Raw leaf charts and actual finite plaque jets have measurable ---
indeed continuous --- local transverse dependence. The adapted normal
changes have measurable finite jets and domains. All subsequent
finite constructions are polynomial spans, kernels, nonzero minors,
implicit coordinate charts, or limits of measurable coefficient
functions. Countable choices of candidate minors and coordinate balls
give measurable versions. The coefficients of the resulting formal
fields are therefore measurable.

On weak plaques use whole-strong-leaf representatives and smooth
flow transport. At points where both constructions are regular their
jets agree by the flow comparison already proved. Strong-leaf
conditional agreement and flow Fubini then give agreement almost
everywhere on the weak plaque. Compact subpatches have finite smooth
norms. Conditional essential suprema make the bounds measurable on
the family of weak plaques as well.

An almost-everywhere finite measurable bound is bounded on a
positive-measure subfamily of any positive-measure plaque-label
set. The same holds for the reciprocal of a positive radius and for
any finite list of bounds. Absolute continuity of the strong and
weak foliations and a countable cover allow all conditional agreement
requirements to be imposed simultaneously, also at integer iterates.
\end{proof}

\begin{theorem}[The two formal affine fields]\label{hull:main}
At every point of a conull invariant set, there are formal affine
fields $\mathcal A^u,\mathcal A^s$ of horizontal $m$-covectors with:
\begin{enumerate}[label=\textup{(\roman*)}]
\item Their values contain $u$ and $w$ respectively. At the centre,
  the exterior product of any element of $\mathcal A^u$ with any
  element of $\mathcal A^s$ equals the fixed nonzero exterior product
  $u\wedge w$.
\item The fields are equivariant under $f$, changes of section, and
  flip, with the same constant and height multipliers as $u,w$. In
  a flow box their height dependences are $e^{-h\tau}$ and $e^{h\tau}$.
\item On each entire typical strong stable or strong unstable leaf,
  every ambient Taylor coefficient has a smooth representative
  agreeing almost everywhere with the regular construction. These
  representatives are holonomic in the sense of
  \eqref{hull:coherence-eq}. The analogue holds on typical weak
  leaves using flow transport.
\item At every finite order the local representatives, their bounds,
  and positive radii can be chosen measurably. On compact plaque
  subboxes, one may restrict to positive-measure families with
  uniform finite-order bounds. No common convergence radius for all
  orders is asserted.
\end{enumerate}
\end{theorem}

\begin{proof}[Proof of Theorem~\ref{hull:main}]
The unstable affine field is supplied by Lemma~\ref{hull:rank}. Its
central value contains the actual augmented form and hence the
actual form. Lemmas~\ref{hull:coherence} and~\ref{hull:measurability}
give full ambient coherence, globalisation, and measurable
finite-order bounds. Restore the height dependence $e^{-h\tau}$.

Apply the same construction with time reversed to obtain
$\mathcal A^s$, restoring height dependence $e^{h\tau}$. One may
choose charts measurably in flip pairs, with the axes interchanged;
all graph comparisons preserve the construction, so it is compatible
with flip. Proposition~\ref{hull:pairing} gives the constant cross
pairing of centred affine spans. The transformation laws follow from
the exact raw form transformation and the fixed-point nature of the
span.
\end{proof}

\section{Formal symmetries and coherent transport}
\label{sym:section}

\paragraph{Plain summary.}
We study the formal strict contact symmetries of the affine fields
$\mathcal A^u, \mathcal A^s$: formal Hamiltonians $p$ whose flow
preserves both augmented affine bundles. These form a Lie algebra
$\mathfrak h$.

Two special elements stand out. A \emph{dilation} $D$ (expanding $E^s$
and contracting $E^u$) is the formal analogue of the flow direction.
And the evaluation functional $\xi(p)=p(0)$ together with the
isotropy subalgebra $\mathfrak k=\ker Y_p(0)$ measure the linear part
of a symmetry. The \emph{entropy trace identity}
\[
 h\xi(p) = \tr(A_p|_{E^s}) \quad (p\in\mathfrak h_0)
\]
ties the algebra to the entropy. It is proved by pairing the
infinitesimal action of $p$ on $u$ against the opposite form $w$;
constant cross-pairing from Theorem~\ref{hull:main} forces the scalar
coefficient to vanish.

The identity is the input for Cartan--Guillemin structure theory of
transitive linearly compact Lie algebras in Section~\ref{alg:section}.
Here we establish the algebra structure of $\mathfrak h$ and the
intrinsic transport properties.

\subsection{The algebra of formal symmetries}

Augment each affine field by a scalar slot:
\[
 \mathcal B^\varepsilon = \Span\{(a,1): a\in\mathcal A^\varepsilon\},
 \quad\varepsilon\in\{u,s\}.
\]
The scalar-one slice recovers the affine field, including its
translation part. Put $b_p=p-\theta(Y_p)$ on the section.
Infinitesimal actions:
\begin{align}
 \mathcal D_p^u(\beta,s) &=(\mathcal L_{Y_p}\beta - h b_p\beta, Y_p s),
 \label{sym:augmented-action-u}\\
 \mathcal D_p^s(\beta,s) &=(\mathcal L_{Y_p}\beta + h b_p\beta, Y_p s).
 \label{sym:augmented-action-s}
\end{align}
These retain the height factors $e^{-h\tau}$ and $e^{h\tau}$ in the
contact lift.

Define $\mathfrak h$ by requiring each operator to preserve its
corresponding formal subbundle. In a Grassmann chart, choose a frame
matrix $B^\varepsilon$ and quotient $Q^\varepsilon$ with kernel
$B^\varepsilon$; the equations are
\begin{equation}\label{sym:linear-equations}
 Q^\varepsilon\mathcal D_p^\varepsilon B^\varepsilon = 0,
 \quad \varepsilon\in\{u,s\}.
\end{equation}
They are linear in $p$. Coefficients through order $r$ use only
finitely many background coefficients and the $(r+2)$-jet of $p$.
Changing frame or Grassmann chart gives equivalent equations.
Consequently $\mathfrak h$ is a closed linear subspace of the formal
Hamiltonians, closed under Poisson bracket: a linearly compact Lie
algebra with continuous bracket. Set
\begin{equation}\label{sym:isotropy-functional}
 \xi(p)=p(0), \qquad
 \mathfrak k = \{p\in\mathfrak h : Y_p(0) = 0\}.
\end{equation}
Both $\xi$ and evaluation at $0$ are continuous; $\mathfrak k$ is an
open subalgebra.

\subsection{A signed dilation}

The normal forms of Section~\ref{nf:section} used one-signed state
weights. Here we need a different normalisation of the section map
itself, with both dynamical signs, performed one ordinary Taylor
degree at a time.

\begin{lemma}[Graded contact coordinates]\label{sym:graded-contact}
On the section through a typical point, there are formal coordinates
$(x_i,y_i,z)$ ($i=1,\dots,m$) in which: $X=\partial_z$; the contact
form is
\[
 \alpha=dz+\sum_i x_i\,dy_i - \sum_i y_i\,dx_i + O(2);
\]
the actual central strong stable plane is $\{x_i=0\}$; the actual
central strong unstable plane is $\{y_i=0\}$; the graded coordinate
weights $\lambda_i>0$ (for $x_i$), $-\lambda_i$ (for $y_i$), $0$ (for
$z$) coincide with the Lyapunov weights of the linear return map
$(x,y,z)\mapsto(A x, A^{-t} y, z+O(2))$; and a holomorphic extension
to complexified graded algebras exists, preserving real structure.
\end{lemma}

\begin{proof}
The linear part of the return map is the hyperbolic diagonal
$\mathrm{diag}(A, A^{-t}, 1)$ on $E^u\oplus E^s\oplus\R X$, by the
Anosov splitting. Choose Lagrangian decompositions $x_i$ of $E^u$
and $y_i$ of $E^s$ so the contact pairing pairs $x_i$ with $y_i$
via $\omega=d\theta$. At the linear level, $\alpha$ restricted to
$E^u\oplus E^s$ gives the standard Darboux model
$\sum_i(x_i\,dy_i - y_i\,dx_i)$; add the Reeb $z$. Absorb nonlinear
terms via formal symplectic substitution one Taylor degree at a
time, using nonresonance from Lemma~\ref{nf:homological}. Smooth
dependence in the centre is measurable; the formal structure is
one-degree-at-a-time.
\end{proof}

\begin{proposition}[Signed dilation]\label{sym:dilation}
There is an element $D\in\mathfrak h$ acting in those coordinates as
\[
 D = \sum_i \lambda_i(x_i\partial_{x_i} - y_i\partial_{y_i}),
\]
with $\theta_0(D)=\sum_i\lambda_i(x_i\,dy_i - y_i\,dx_i)$. It
preserves both augmented affine fields. Its Hamiltonian action is
diagonal monomial expansion/contraction, with $\{H,p\}=Dp$, and the
spectral projector onto weight-$\gamma$ components is polynomial in
the $\mathcal L_D$-eigenvalues.
\end{proposition}

\begin{proof}
Lemma~\ref{nf:blocks} splits the invariant jet subspace into weight
blocks. Ambient finite jet cocycle of smooth return maps on the
compact phase space has bounded one-step coefficients; its formal
coordinate change is tempered at fixed order. No tempered bound on
the hull subspace is assumed.

Infinitesimal diagonal action: $(\mathcal L_D+hT,D)$ on the two
augmented $u$ slots, $(\mathcal L_D-hT,D)$ on the two augmented $s$
slots. It preserves both augmented subbundles through order $N$;
$N$ was arbitrary, so \eqref{sym:augmented-action-u}--
\eqref{sym:augmented-action-s} show $D-T\partial_\tau$ preserves
both formal affine fields. The identity
$d(\theta_0(D))=-\iota_D\omega_0$ proves the Hamiltonian formula.

For any Hamiltonian $p$, $\{H,p\}=Dp$; the asserted diagonalisation
is literal monomial diagonalisation. To project onto a weight
$\gamma$: choose on each finite Taylor quotient the polynomial
spectral projector onto $\gamma$ for $D$. Applied to a fixed formal
series, projectors eventually agree on every fixed coefficient and
converge coefficientwise to its weight-$\gamma$ part. A closed
invariant subspace contains the limit. A continuous finite-dimensional
quotient is detected at a finite Taylor order, so projectors commute
with the passage to that quotient and give the claimed lifts. The
argument applies also to closed invariant subspaces before
quotienting.

All coordinate weights in degree one are nonzero. A weight-zero
Hamiltonian therefore has zero differential at zero and belongs to
$\mathfrak k$. Evaluation at zero sees only the constant monomial,
of weight zero.
\end{proof}

\begin{lemma}[Entropy trace identity]\label{sym:trace}
For every $p\in\mathfrak h_0$, the linear map $A_p=dY_p(0)$
preserves both actual signed tangent planes and
\begin{equation}\label{sym:geometric-trace}
 h\,\xi(p)=\tr(A_p|_{E^s}).
\end{equation}
\end{lemma}

\begin{proof}
Since $[D,Y_p]=0$ and $Y_p(0)=0$, the derivative $A_p$ commutes with
$D$. It preserves the signed planes, which are the actual strong
planes by Lemma~\ref{sym:graded-contact}. At the centre, the actual
$u$ annihilates $E^u$ and is a volume form on $E^s$; its
infinitesimal transform under $Z_p$ is
\[
 \bigl(\tr(A_p|_{E^s})-h\xi(p)\bigr)u.
\]
Preservation of the affine field says this vector belongs to the
direction space of $\mathcal A^u(0)$. Pairing any such direction with
the actual opposite form $w(0)$ gives zero, by the constant
cross-pairing property in Theorem~\ref{hull:main}. Since
$u(0)\wedge w(0)\ne0$, the displayed scalar vanishes.
Complexification causes no change.
\end{proof}

\subsection{Finite solution spaces on a whole axis}

The dilation coordinates above are only measurable in the centre. We
never differentiate them with respect to the centre. Instead we use
the equations in fixed smooth coordinates.

\begin{lemma}[Finite projections]\label{sym:full-projections}
At every finite equation order on a whole axis patch, the evaluation
map $\mathfrak h\to(\text{first jets at }0)$ is surjective onto a
constant-rank subspace of the ambient finite jet space. Its dimension
and image are locally constant along typical axes.
\end{lemma}

\begin{proof}
The defining equations are linear in $p$, with smooth coefficients
at each finite order. The ranks of the defining matrix $A_N$ and of
the augmented matrix stacking $A_N$ with $\pi_r$ are invariant under
the return dynamics (finite symmetry conditions and jet projection are
natural under centred coordinate changes). By ergodicity these ranks
are constant a.e.\ simultaneously for all $r,N$ under consideration.
These two ranks determine $\dim K_N$ and $\dim V_{r,N}$. At a regular
centre a nonzero maximal minor remains nonzero on a small axis
patch. Dense regular agreement prevents a larger rank anywhere on
that patch (an open set of larger rank would meet the dense regular
set). So both ranks, and hence the kernel and image ranks, are
constant near the centre. Constant-rank linear algebra gives smooth
kernel and image bundles there.
\end{proof}

\begin{proposition}[Transitivity]\label{sym:transitivity}
For any finite equation order on a whole axis patch, and any
prescribed tangent value, there is a full formal symmetry realising
it.
\end{proposition}

\begin{proof}
Differentiating isotropy by the chain rule gives
\begin{equation}\label{sym:differentiated-value}
 Y_{\partial_t^{\mathrm{fixed}}p_t}(0) = -dY_H(0)a'(0).
\end{equation}
At the chosen centre $dY_H(0)$ is conjugate to the signed dilation
$D$; invertible, preserves each actual signed tangent plane. Paths in
the two axes give a solution with any prescribed tangent value at
every prescribed equation order. Finite sums handle both signs.
Apply the linear compactness principle from
Lemma~\ref{sym:full-projections}, with prescribed tangent value, to
obtain a full formal solution. No compatibility of the separately
chosen finite families is needed.

Finally, the dimension of the evaluation image is the difference
between the dimensions of the full symmetry and isotropy projections
at first jet order. Those dimensions have the same constant values
on the entire typical axes by Lemma~\ref{sym:full-projections};
surjectivity at their regular points implies surjectivity throughout
their smooth extensions.
\end{proof}

\subsection{Homogeneous fields and their transport}

\begin{proposition}[Homogeneous formal fields]\label{sym:homogeneous-fields}
Every $\mathfrak k$-invariant subspace $V\subset E$ has a unique
$\mathfrak h$-invariant formal distribution with value $V$ at zero.
The construction respects real structures, inclusions, and natural
tensor operations. If $V=\mathfrak l/\mathfrak k$ for a subalgebra
$\mathfrak l\supset\mathfrak k$, the distribution is involutive.
\end{proposition}

\begin{proof}
Choose symmetries $p_1,\dots,p_{2m}$ whose projected values form a
basis. Write $G_t$ for the composition of their formal flows with
parameters $t_1,\dots,t_{2m}$, $F(t)=G_t(0)$. Its linear term is
invertible, so the formal inverse function theorem gives $t=t(q)$.
Transport $V$ by $dG_t(0)$ and substitute $t(q)$. All operations
are well-defined in formal displacement parameters of positive order.

Independence: two parameterised translations reaching the same point
differ by a formal family fixing zero. Its right logarithmic
derivative belongs coefficientwise to the projected symmetry algebra
(composition and inversion give sums of conjugated generators; their
formal adjoint series are iterated brackets). Since the family fixes
zero, these derivatives belong to the projected isotropy. Its
derivative at zero consequently preserves $V$, by the linear
differential equation starting at the identity. So independent.
Including the formal flow of any further symmetry proves invariance;
conversely any invariant field must be transported from its value by
these spanning flows, which proves uniqueness.

Involutivity: the Levi bracket of an invariant distribution at zero,
evaluated on the values of $p,q\in\mathfrak l$, is the negative of
the projected bracket $\{p,q\}$ modulo $V$. Check without assuming
generating fields tangent everywhere: choose tangent sections with
the same initial values and use that their brackets with symmetry
fields remain tangent. Subtracting gives the claimed Levi bracket.
Vanishes since $\mathfrak l$ is a subalgebra. Invariance and the
spanning formal translations make the obstruction vanish as a full
formal tensor.
\end{proof}

For the next proposition, an \emph{intrinsic} construction is one
that commutes with formal strict contact isomorphisms of the affine
data, including reciprocal constant rescalings of the two affine
fields (which do not change $\mathfrak h$).

\begin{proposition}[Intrinsic transport]\label{sym:axis-transport}
Given $\mathfrak l\supset\mathfrak k$ and any intrinsic construction
from $\mathfrak h$, the resulting homogeneous fields are smooth and
holonomic along entire typical axes, with measurable finite-order
bounds. They are equivariant under return maps and regular flow
shifts, compatible with flip, and satisfy the prescribed height
dependence.
\end{proposition}

\begin{proof}
Work on a smooth axis patch in a fixed section; let $a(t)$ be a path
there. By Proposition~\ref{sym:transitivity} and
Lemma~\ref{sym:full-projections}, full finite symmetry projections
surject smoothly onto prescribed tangent values. Choose a smooth
section with value $a'(t)$ at first order. Lift successively through
the surjective smooth bundle maps of Lemma~\ref{sym:full-projections},
using smooth right inverses from bundle metrics on the axis.
This constructs compatible formal symmetries $p_t$ with every
coefficient smooth and $Y_{p_t}(a(t))=a'(t)$, smooth in auxiliary
path parameters, with no uniform bound on formal order.

Integrate in coordinates relative to the moving centre. The
generating field is $Y_{p_t}(a(t)+z)-a'(t)$, which vanishes at
$z=0$, so its ODE closes at every finite Taylor order; solving gives
a smooth formal coordinate change. For the strict contact lift,
choose the centre height $\beta(t)$ by
$\beta'(t)=p_t(a(t))-\theta_{a(t)}(a'(t))$. The lifted generator
relative to $(a(t),\beta(t))$ also vanishes at its formal origin,
so the changes are strict.

These changes intertwine the augmented affine fields: differentiate
the pullback of frame jets modulo the corresponding bundle.
Moving-centre differentiation is formal derivative in centre velocity,
by whole-axis holonomicity and smooth height dependence. The relative
generator subtracts that same velocity. The remaining term is the
infinitesimal symmetry equation \eqref{sym:linear-equations}, zero
in the bundle quotient. Internal change of frame permitted. This
verification is at each finite order, ordinary differentiation of a
finite system. The centre height $\beta$ introduces the reciprocal
constants $e^{-h\beta}, e^{h\beta}$ in the two affine fields, which
do not change $\mathfrak h$. Strictness and transport of the centre
preserve both isotropy and $\xi$.

An intrinsic construction at the centres is therefore constant under
these algebra identifications. Proposition~\ref{sym:homogeneous-fields}
commutes with them, so its entire formal field is transported with
smooth coefficients. For holonomicity, let $T_t$ denote the
moving-centre formal tensor projected to the section. The transport
identity (interpreted in a Grassmann chart for a distribution) gives
\[
 \partial_t T_t + \mathcal L_{Y_{p_t}-a'(t)} T_t = 0.
\]
Homogeneous invariance $\mathcal L_{Y_{p_t}}T_t=0$ gives
$\partial_t T_t=\mathcal L_{a'(t)}T_t$. For the constant displacement
$a'(t)$ this is exactly the coefficientwise Taylor coherence
\eqref{hull:coherence-eq}. Lifted tensors include the centre height
velocity.

For a finite intrinsic list, use the smooth path family to
trivialise structures over a whole axis patch; a continuous selection
into the finite list is then locally constant. This proves the
assertion also on paths that need not consist entirely of regular
points. Whole-axis extensions of Lemma~\ref{sym:full-projections}
permit patches everywhere on the axis; uniqueness and regular density
make their jets agree on overlaps. Naturality proves equivariance
under the return map and under regular flow shifts. Height
dependence, strong-axis coherence, and flow Fubini give the weak-axis
extension and its a.e.\ agreement.
\end{proof}

\begin{proposition}[Effective symplectic homogeneous algebra]
\label{sym:effective}
The open isotropy $\mathfrak k$ contains no nonzero ideal of
$\mathfrak h$, and is exactly the coadjoint stabilizer of $\xi$.
Evaluation identifies
\[
 E=\mathfrak h/\mathfrak k\simeq T_0\R^{2m},\qquad
 \omega_E(\bar p,\bar q)=\xi(\{p,q\}).
\]
This form is nondegenerate. On $E$, $\ad H$ is $-D$, so it has no
zero weight. With $E_+$ the positive-weight subspace, the trace
identity is
\begin{equation}
 \label{sym:algebra-trace}
 c\,\xi(p)=\tr(p|_{E_+}),\qquad
 p\in\mathfrak h_0,\qquad c=-h\ne0.
\end{equation}
Here $p|_{E_+}$ means the isotropy action by brackets. In particular
$E_+$ corresponds to the geometrically stable plane.
\end{proposition}

\begin{proof}
Transitivity and the Hamiltonian bracket formula give
\[
 \xi(\{p,q\})=\omega_0(Y_p(0),Y_q(0)).
\]
Its radical is exactly the kernel of tangent evaluation. This is
both the asserted symplectic identification and the assertion
$\mathfrak k=\operatorname{stab}_{\mathfrak h}\xi$.

Suppose an ideal $I$ lies in $\mathfrak k$ and $p\in I$. Every
iterated bracket of its projected field with fields from
$\mathfrak h$ vanishes at zero. If $Y_p$ had a first nonzero
homogeneous term of degree $j\ge1$, brackets with symmetries having
prescribed constant tangent values would differentiate that term.
After $j$ such brackets a nonzero constant value would result.
At each step the other bracket term has higher order, so it cannot
cancel this leading derivative. This contradicts $I\subset
\mathfrak k$. Hence $Y_p=0$ formally and $p$ is constant. A constant
Hamiltonian has weight zero; Lemma~\ref{sym:trace} then gives $hp=0$.
Thus $I=0$.

For $p\in\mathfrak k$ and any $q\in\mathfrak h$, evaluation of the
projected bracket gives
$Y_{\{p,q\}}(0)=-dY_p(0)Y_q(0)$. Apply this first to $p=H$ to obtain
the action $-D$, and then use Lemma~\ref{sym:trace} on the stable
plane to obtain Equation~\eqref{sym:algebra-trace}.
\end{proof}

\section{The algebraic consequence of the entropy trace identity}
\label{alg:section}

\paragraph{Plain summary.}
The entropy trace identity from Lemma~\ref{sym:trace} is the input for
Cartan--Guillemin structure theory of transitive linearly compact Lie
algebras. The classification produces a dichotomy:

\begin{enumerate}
\item \emph{Finite-dimensional:} the sign planes $E^s, E^u$ are sums
of finitely many isotypic components of a natural $\mathfrak l$-action,
so the formal sign fields have center values exactly $E^s, E^u$. This
is the ``smooth case'' that finishes the proof.
\item \emph{Infinite-dimensional:} there is an intrinsic nonzero plane
$P'\subset L^{\omega}$ inside the characteristic distribution, with
nonzero stable and unstable parts. This is the ``coisotropic case''
that Section~\ref{real:section} will contradict.
\end{enumerate}

The proof uses: equicontinuity to define an intrinsic subalgebra
$\mathfrak l\subset\mathfrak h$; Cartan--Guillemin to identify
$\mathfrak l$ with an origin-stabilizer in the classical realization
of a minimal ideal; the trace identity via a finite auxiliary
reductive quotient to force the socle of $B^*$ to split into
pure-sign isotypic components.

\subsection{The intrinsic coisotropic reduction}

For $p\in\mathfrak h$ consider $\{(\ad p)^n:n\ge0\}$.
\emph{Equicontinuity} in the formal linear topology means: for each
prescribed output jet order there is an input vanishing order making
every operator in the family zero on that input. The order may depend
on the input order and on $p$, but not on $n$. Define
\begin{equation}\label{alg:equicontinuity}
 \mathfrak l=\{p\in\mathfrak h:
   \{(\ad p)^n:n\ge0\}\text{ is equicontinuous}\}.
\end{equation}
In finite dimension this is all of $\mathfrak h$ because the topology
is discrete. In general even the subalgebra property needs proof.

\begin{proposition}[Intrinsic coisotropic reduction]\label{alg:coisotropic}
The set $\mathfrak l$ is an open intrinsic subalgebra containing
$\mathfrak k$ and $H$, with arbitrarily small open ideals for the
induced topology. The subspace $L=\mathfrak l/\mathfrak k\subset E$
is coisotropic, $L^\omega\subset L$. If $\mathfrak h$ is infinite
dimensional, $\mathfrak l\ne\mathfrak h$.
\end{proposition}

The proof identifies $\mathfrak l$ as an origin-stabilizer via
Cartan--Guillemin (below); the trace identity proves coisotropy.

\subsection{Structure of the minimal ideals}

\begin{lemma}\label{alg:minimal-ideals}
The algebra $\mathfrak h$ has no nonzero closed abelian ideal. Every
nonzero closed ideal contains a minimal nonzero closed ideal. There
are finitely many such minimal ideals, each topologically perfect,
and their common centralizer in $\mathfrak h$ is zero.
\end{lemma}

\begin{proof}
Let $A$ be closed abelian. For $p\in A\cap\mathfrak h_0$, we have
$p\in\mathfrak k$ and $(\ad p)^2=0$ on $\mathfrak h$. Its trace on
$E_+$ vanishes, and the trace identity
(Lemma~\ref{sym:trace}, in algebraic sign convention) gives
$\xi(p)=0$. Since $\xi$ kills every nonzero weight ($H$ stabilizes
$\xi$), $\xi(A)=0$. Since $[\mathfrak h,A]\subset A$, every
$A$-element stabilizes $\xi$, so $A\subset\mathfrak k$; hence $A=0$.

Let $A\ne0$ closed. Countably many closed ideals intersect in a
closed ideal; a descending chain with positive weight projections
(diagonalised in the countably many finite jet quotients) limits
to a minimal nonzero closed ideal. Finitely many by countable
diagonalisation.

Topological perfectness: quotient by commutator is a closed abelian
ideal, hence zero by the first paragraph.

Common centralizer: an element commuting with every minimal ideal
commutes with their adjoint images, whose sum is dense in
$\mathfrak h$ (classical structure of transitive linearly compact
algebras). So the centralizer is central in $\mathfrak h$. A
central $p$ makes $Y_p$ invariant under the entire translation
algebra, whose translates span the tangent space at every nonzero
point; so $Y_p$ is constant, $\xi(p)=\tr(0)=0$, so $p=0$.
\end{proof}

\paragraph{Structure of a minimal ideal.}
Over $\C$, the Cartan--Guillemin theorem gives, for a nonabelian
minimal closed ideal,
\begin{equation}\label{alg:current-ideal}
 I=S\hat\otimes\mathcal O_e, \quad
 \mathcal O_e=\C[[z_1,\dots,z_e]],
\end{equation}
with $S$ a nonabelian simple linearly compact Lie algebra and $e$
finite. A maximal proper closed ideal of $I$ has open normalizer $N$
in $\mathfrak h$; the simple quotient is $S$, and
$I\simeq\Hom_{U(N)}(U(\mathfrak h),S)$. The finite complement to $N$
and the PBW coalgebra identification give \eqref{alg:current-ideal}
\citep{FattoriKac2002,BakalovDAndreaKac2001}.

The infinite possibilities for $S$ are the formal Cartan algebras:
all formal vector fields $W$, divergence-free, Hamiltonian, and
contact. Finite-dimensional simple algebras are also allowed. For
infinite simple factors, continuous derivations are represented
faithfully by their normalizing formal vector fields; for divergence-
free and Hamiltonian cases constant conformal multipliers are
allowed; the normalizer of $W$ and of the contact algebra is the
algebra itself. See \citet[Thm.~6.8, Prop.~6.12(i)]{BakalovDAndreaKac2001}.
Finite-dim simple factor: derivations inner, finite matrices. All
topological statements use formal linear topologies with discrete
scalars, not analytic convergence.

Give ordinary coordinates weight one in $W$, divergence-free,
Hamiltonian cases; vector-field grade $=$ coefficient degree $-1$;
Hamiltonian grade $=$ Hamiltonian degree $-2$ modulo constants.
Contact coordinates: horizontal weight one, Reeb weight two;
contact-Hamiltonian grade $=$ weighted degree $-2$. $S_{\ge j}$:
series of grades $\ge j$; $S_{(0)}$: subalgebra fixing origin;
$S_{(0)}=S_{\ge0}$. Lowest grades $-1$ except in contact case where
they are $-2$ and $-1$.

\begin{lemma}\label{alg:derivation-realization}
For an ideal \eqref{alg:current-ideal}, every continuous derivation
has a unique decomposition into a formal parameter vector field and
an $\mathcal O_e$-family of continuous derivations of $S$:
\begin{equation}\label{alg:current-derivations}
 \Der(I)=W_e\otimes 1+\mathcal O_e\hat\otimes\Der(S).
\end{equation}
The action of $\mathfrak h$ on its finitely many minimal ideals is a
faithful topological embedding with closed image in the product of
these derivation algebras.
\end{lemma}

\begin{proof}
A derivation acts on the centroid by commutator, inducing a continuous
derivation of $\mathcal O_e$, i.e.\ a formal parameter vector field.
Continuity: evaluate the commutator on a fixed nonzero constant
$s\in S$, apply a continuous functional taking value one at $s$;
gives continuity of the induced scalar-series operator. Subtract the
parameter field: remaining derivation is $\mathcal O_e$-linear.
Restriction to constant $S$-series, coefficient by coefficient, gives
derivations of $S$. Density gives the decomposition and uniqueness.
Same as \citet[Prop.~6.12(ii)]{BakalovDAndreaKac2001}.
\end{proof}

\begin{lemma}\label{alg:translation-test}
Let $A$ be a normalizing formal vector field of an infinite simple
Cartan algebra, not fixing the origin. Its lowest nonzero grade is
$-b<0$. The grade-$-b$ part of $\ad A$ maps each homogeneous
component of grade $j+b$ onto that of grade $j$. Consequently
$\{(\ad A)^n:n\ge0\}$ is not equicontinuous.
\end{lemma}

\begin{proof}
$W$: surjectivity of differentiation in a nonzero constant direction
on homogeneous vector-field coefficients. Divergence-free: integrate
coefficients in that direction; the divergence of the primitive is
independent of this coordinate, correct by integrating error in
another coordinate and subtracting, preserving the first directional
derivative (homogeneous correction). Hamiltonian: integrate homogeneous
Hamiltonians mod constants. Contact: grade $-2$ acts by Reeb
differentiation; nonzero grade $-1$ acts by constant horizontal
derivative plus linear multiple of Reeb differentiation (Reeb
derivative zero, so contact bracket on Hamiltonians has no additional
multiplier). A homogeneous quadratic change of Reeb coordinate
straightens the operator; integration preserves weighted degrees.

Conversely, suppose the parameter field of $p$ has a nonzero value at
zero. Choose $z_1$ with $p(z_1)(0)\ne0$, and a fixed nonzero $s\in S$.
Applied $n$ times to $z_1^ns$, only repeated use of the constant
parameter derivative produces parameter order zero in $n$ steps. Its
value there is $n!\,p(z_1)(0)^ns\ne0$. So the adjoint powers fail
equicontinuity already on that ideal. If the parameter origin is
fixed but the factor origin is not, reduce modulo the parameter ideal
and apply the previous paragraph: equicontinuity restricts to $I$
and descends through the open quotient
$I\to I/(z_1,\dots,z_e)I\simeq S$. The same failure holds on
$\mathfrak h$ in its induced topology.
\end{proof}

\paragraph{$\mathfrak k \subset \mathfrak l_i$ for each minimal ideal.}
Let $I=I_i$, $S=S_i$. For $q\in\mathfrak k$, test
$\xi([q,\mathfrak m I])=0$ on $z_as$ with $\xi(s)\ne0$: at parameter
order zero, the bracket is $q(z_a)(0)s$. So $q$'s parameter field
fixes zero. If $S$ is Cartan: let $j$ be the highest standard grade
where the functional on $S$ is nonzero (exists by continuity); if the
factor field of $q$ doesn't fix the origin, let its leading grade be
$-b$. Test on grade $j+b$: by Lemma~\ref{alg:translation-test} the
leading term can have any prescribed grade-$j$ value, while all
higher terms have grades annihilated by $\xi$. Contradicts
$q\in\mathfrak k$.

Contact case: $j=-2$ impossible. Otherwise the functional would
vanish on $\mathfrak m I+S_{(0)}$, descending nontrivially to
$I/(I\cap\mathfrak l)$. But this quotient is $S/S_{(0)}$ (ideal acts
trivially on all other minimal ideals; factor action inner). It is
$H$-invariant in $\mathfrak h/\mathfrak l$. Functional descends
$H$-invariant since $\xi([H,I])=0$, forcing zero weight in this
quotient of $E$. $E$ has no zero weight. So $j\ge-1$.

\subsection{The characteristic representation}

\begin{lemma}[Characteristic representation]\label{alg:characteristic-representation}
The kernel of the restricted alternating form on $L$ is
$P=\mathfrak u/\mathfrak k$, with $\mathfrak u=\mathrm{stab}_\mathfrak l(\xi|_\mathfrak l)$.
The map
\[
 P\to B^*,\qquad v\mapsto (q+\mathfrak l\mapsto\omega(v,q+\mathfrak k))
\]
is an isomorphism intertwining the $\mathfrak k$-action with the dual
bracket action on $B$. That action is a genuine $\mathfrak l$
representation. Transferring gives the asserted $\mathfrak l$-action
on $P$, and this is not in general the bracket action of $\mathfrak u$
on $\mathfrak u/\mathfrak k$.
\end{lemma}

\begin{proof}
The kernel of the restricted alternative form on $L$ is
$\mathfrak u/\mathfrak k$: that is exactly $P$. The map is well-defined
and an isomorphism by nondegeneracy. $\mathfrak k$-action is
symplectic (elements stabilize $\xi$), so the map intertwines with
the dual bracket action. Latter is an actual representation because
$\mathfrak l$ is a subalgebra. Transferring gives the asserted action
on $P$. The bracket action of $\mathfrak u$ on $\mathfrak u/\mathfrak k$
is not well-defined without stabilization; the transfer is.
\end{proof}

\subsection{Trace positivity and pure sign subspaces}

\begin{proposition}[Pure signs in full isotypic components]\label{alg:signs}
If $B\ne0$, let
\begin{equation}\label{alg:socle}
 P'=\mathrm{soc}_{\mathfrak l}(B^*)\subset P
\end{equation}
in the transferred representation of
Lemma~\ref{alg:characteristic-representation}. It is nonzero. Its
two $H$-sign parts are unions of full $\mathfrak u$-isotypic
components, hence invariant under the full transferred $\mathfrak u$
action.

If $\mathfrak h$ is finite dimensional and $\mathfrak l=\mathfrak h$,
then $E$ is a semisimple $\mathfrak k$-module whose $H$-sign parts
are unions of full isotypic components.

Either way, there are only finitely many possible unions of isotypic
components of the module under consideration.
\end{proposition}

We prove this via a finite auxiliary quotient. That quotient is not
intrinsic: $\mathfrak l$, its representation on $B^*$, and the socle
are already defined without it. It isolates the part of $H$ whose
trace must vanish; positivity then rules out constituents containing
both signs.

\paragraph{A finite quotient and its reductive stabilizer.}
Use finite-dimensional Lie theory only for quotients and modules
below; triangularisation and complete reducibility are
\citet[Thms~I.3.7, I.5.20(b)]{Milne2013}.

Choose an open ideal $\mathfrak m$ of $\mathfrak l$ small enough that
$\mathfrak m\subset\mathfrak u$ and the finite-dimensional quotient
$g=\mathfrak l/\mathfrak m$ carries generators of every finite set of
isotypic components relevant below. Let $r_g$ be the radical, so
$g'=g/[g,r_g]$ is reductive (radical central). Let $\xi'$ and
$\mathfrak u'$ be the induced functional and its stabilizer in $g'$.
Since $[g,r_g]$ is annihilated by $\xi$, its full inverse image in
$\mathfrak l$ lies in $\mathfrak u$; so
\begin{equation}\label{alg:reductive-tangent}
 \mathfrak l/\mathfrak u\simeq g'/\mathfrak u'.
\end{equation}

\begin{lemma}\label{alg:reductive-stabilizer}
The algebra $\mathfrak u'$ is reductive. Its center on the semisimple
summand of $g'$ is toral. The restriction to $\mathfrak u'$ of every
irreducible $g'$-module is semisimple, and $g'/\mathfrak u'$ is a
semisimple $\mathfrak u'$-module.
\end{lemma}

\begin{proof}
For an irreducible $g'$-module the global center acts by scalars.
The derived algebra of the reductive $\mathfrak u'$ is semisimple, so
its action is completely reducible. The center consists of commuting
semisimple elements of the semisimple summand, hence acts simultaneously
diagonalizably in every finite-dimensional module. Split into center
eigenspaces, then into irreducible derived-algebra modules. Same
argument for the adjoint module of $g'$ and its invariant quotient
$g'/\mathfrak u'$.
\end{proof}

\begin{proof}[Proof of Proposition~\ref{alg:signs}]
Let $H=H_c+H_{ss}$ be the
decomposition with $H_c\in Z(\mathfrak u')$ and
$H_{ss}\in[\mathfrak u',\mathfrak u']$. Lift $H_{ss}$ to a
weight-zero $p\in\mathfrak l$ (possible since $H_{ss}$ commutes with
$H$); the lifted $p$ has $\xi(p)=0$ because $\xi'$ annihilates
$[\mathfrak u',\mathfrak u']$.

Write the finite-trace identity in the algebraic sign convention.
For the weight-zero lift $p$ of $H_{ss}$, the three contributions
--- from $\mathfrak l/\mathfrak u$, from $B$, and from the adjoint
action of $g'$ --- vanish or are nonnegative:
\begin{equation}\label{alg:three-traces}
 0 = \tr_{\mathfrak l/\mathfrak u}(p)+\tr_B(p)
     +\tr_{g'/\mathfrak u'}(p).
\end{equation}
Indeed $\xi(p)=0$, so the trace identity becomes this trace balance;
each term is a signed trace on an $H$-eigenmodule, and nilpotency
of $H_c$-eigenvalues on $[g,r_g]$ gives vanishing of the
$[g,r_g]$-part while $H_{ss}$-eigenvalues are nonnegative on
positive-weight constituents.

All constituent contributions are nonnegative, none strictly
positive. Every irreducible constituent in these computations is
therefore pure sign. Isomorphic $\mathfrak u'$ modules have the same
$H$ spectrum, hence the same sign.

The nonzero finite-dimensional module $B^*$ has an irreducible
submodule, so its socle $P'$ is nonzero, a semisimple $g$-module.
Its constituents are duals of quotients of $B$, hence among duals of
the factors just considered. Their restrictions to $\mathfrak u'$ are
semisimple with pure-sign irreducible constituents (by the previous
result, with signs reversed under duality). Isomorphic constituents
cannot be assigned opposite signs. Consequently each sign part of
$P'$ is a sum of full $\mathfrak u$-isotypic components for the
transferred dual representation. This proves full $\mathfrak u$
invariance.

In the finite case $B=0$, $\mathfrak u=\mathfrak k$, and
\eqref{alg:reductive-tangent} identifies $E$ with
$g'/\mathfrak u'$. The same constituent argument gives its
semisimple isotropy representation and pure-sign isotypic
decomposition. Any finite-dimensional semisimple module has finitely
many distinct isotypic components, hence finitely many sums of
full components.
\end{proof}

\subsection{Intrinsic fields, real structure, axis coherence}

The finite auxiliary quotient is not intrinsic. $\mathfrak l$ is
intrinsic by \eqref{alg:equicontinuity}; $L,P,B,\mathfrak u$ and the
representation transferred to $P$ are intrinsic from their
definitions. The socle in \eqref{alg:socle} is intrinsic. None of
these objects depends on a choice of coordinates in the minimal
ideals or on the finite quotient $g$.

\begin{proposition}\label{alg:axis-coherence}
The planes and subalgebras above are measurable on a common conull
set and commute with the dynamics and real conjugation. Their
invariant homogeneous formal fields (via
Proposition~\ref{sym:axis-transport}) have full ambient jets smooth and
holonomic along both entire typical strong axes; the weak versions
follow by flow transport.

In the infinite case $P'$ is flip-invariant. Its actual stable and
unstable parts
\[
 P^s=P'\cap\Es,\qquad P^u=P'\cap\Eu
\]
are both nonzero, have the same rank a.e., and have the stated
coherent formal extensions. They remain invariant under the full
transferred $\mathfrak u$ action. In the finite case, the formal
sign fields have center values exactly $\Es$ and $\Eu$.
\end{proposition}

\begin{proof}
Measurability without classifying minimal ideals: replace the
countably many completed-measurable background coefficients by Borel
versions on a common conull Borel set, refined under the countable
group generated by $f$ and flip. Coefficient sequences are coded
in the countable product of standard Borel spaces. This is distinct
from the formal linear topology with discrete scalars. The symmetry
algebra is defined by countably many linear jet equations. For the
intrinsic condition \eqref{alg:equicontinuity}, fix an output jet
order; for each power, this is a finite-jet linear inclusion test;
the full formal solution images are obtainable by the stabilised
finite linear tests from Lemma~\ref{sym:full-projections}. The
quantifiers over orders and powers are countable. So membership in
$\mathfrak l$ is a Borel relation between base point and coefficient
sequences; its finite-dimensional projections are analytic, hence
universally measurable \citep[Prop.~12.2, Cor.~14.10]{Tserunyan2025}.
Tangent planes are recovered measurably by coding $d$ independent
projected vectors for each $d$; the analytic relation has domain
$A_d=\{\dim\ge d\}$, and Borel choice yields measurable selection.

Now the actual-fields part. In the infinite case, $P'$ is a
$\mathfrak u$-invariant nonzero submodule of the transferred dual,
by Proposition~\ref{alg:signs}. Flip invariance follows since flip
commutes with $\mathfrak h$ and $H$ (up to sign) and preserves the
two socle sign parts. The $P^s$ and $P^u$ parts are nonzero by
$P'\subset E^s\oplus E^u$ with distinct $H$-weights, and have the
same rank a.e.\ by ergodicity of $f$. Their coherent formal extensions
are supplied by Proposition~\ref{sym:axis-transport} applied to each sign
part; $\mathfrak u$-invariance is by Proposition~\ref{alg:signs}.

In the finite case, $B=0$; then $\mathfrak l=\mathfrak h$. Proposition
\ref{alg:signs} gives the sign parts of $E$ as unions of full
$\mathfrak k$-isotypic components. Propositions~\ref{sym:axis-transport}
and~\ref{sym:homogeneous-fields} give the corresponding invariant
formal fields, with center values exactly the sign parts. The
coherence and equivariance follow from
Proposition~\ref{sym:effective}.
\end{proof}

\begin{theorem}[Algebraic dichotomy]\label{alg:dichotomy}
At typical centers exactly one of the following holds, with the same
alternative almost everywhere.
\begin{enumerate}[label=(\roman*)]
\item $\mathfrak h$ is finite dimensional. The formal sign fields
  of Proposition~\ref{alg:axis-coherence} have center values
  exactly $\Es$ and $\Eu$. Their full ambient jets are smooth and
  holonomic along both entire typical axes and equivariant under the
  dynamics.
\item $\mathfrak h$ is infinite dimensional. The intrinsic proper
  open subalgebra $\mathfrak l\supset\mathfrak k$ determines an
  involutive coisotropic formal distribution $L$ with characteristic
  distribution $P=L^\omega$. It contains an intrinsic nonzero plane
  $P'$ with nonzero $P^s,P^u$ of Proposition~\ref{alg:axis-coherence},
  invariant under the full $\mathfrak u$ action, with the same
  whole-axis coherence and equivariance.
\end{enumerate}
\end{theorem}

\begin{proof}
Algebraic assertions are Proposition~\ref{alg:coisotropic} and
Proposition~\ref{alg:signs}; the real, measurable and coherence
conclusions are Proposition~\ref{alg:axis-coherence}. The subalgebra
$\mathfrak l$ gives an involutive homogeneous formal distribution
by Proposition~\ref{sym:homogeneous-fields}. Coisotropy gives its
characteristic distribution. Invariance and ergodicity make the
alternative a.e.\ constant.
\end{proof}

We record the representation-theoretic input to the characteristic-leaf
argument in the next section. First integrals of $L$ define a formal
base with tangent space $B$. For $p\in\mathfrak l$, the projected
symmetry fixes the base origin; the negative of its linearisation is
the bracket action on $B$. Under Hamiltonian translation frames for
the characteristic leaf, the cotangent action is exactly the
transferred dual action on $P$. Elements of $\mathfrak u$ have values
spanning $P$ and preserve that leaf.
Proposition~\ref{alg:signs} therefore supplies invariant initial
subspaces for this full cotangent action. This is the invariance
needed to prove that $P^s$ and $P^u$ are parallel for the canonical
characteristic affine connection. The construction of that
connection, its restriction to actual plaques, and the realisation
of mixed rectangles are the content of Section~\ref{real:section}.

\section{Realization of characteristic rectangles}
\label{real:section}

\paragraph{Plain summary.}
If the algebraic dichotomy returned the infinite case, we construct
an actual geometric contradiction on the universal cover. From a
typical lifted center $v$ we build:

\begin{enumerate}
\item A complete proper affine ray $a(t)$ ($t\ge0$) inside the actual
  strong stable leaf $\Ws(v)$.
\item A parallel smooth vector field $V(t)\in P^u_{a(t)}$ along that
  ray, transported by the partial connection on $P^u$.
\item A path $z(t)=F_{a(t)}(V(t))$ that is (a) in $\Wu(a(t))$ by
  construction and (b) in $\Ws(z(0))$ by the stable-tangency lemma.
\end{enumerate}

Such a mixed rectangle --- $z(t)$ tangent to $E^s$ while the base
ray moves in $\Ws(v)$ --- yields incompatible endpoints in the ideal
boundary. That contradiction rules out the infinite case, leaving the
finite case where the formal sign fields are already smooth.

All progress depends on \emph{actual} existence of smooth limits of
truncated unstable translations, on which we spend most of this
section: finite Taylor truncation to $V_{n,R}$, backward iteration,
interpolation to higher derivatives, and a final triangle estimate
that gives exact leaf inclusion.

Throughout this section, work on the universal cover
$\widetilde M$: this has no identifications and every axiom of
negative curvature is available directly. All refinements of the
regular set are countable and retain conditional full measure on the
entire axes in use. Write $d_s$ for intrinsic distance on a strong
stable leaf. Fix positive constants $b_s,b_u,C$ such that
\begin{equation}\label{real:hyperbolicity}
 \|df^r|_{\Es}\|\le Ce^{-b_sr},\quad
 \|df^{-r}|_{\Eu}\|\le Ce^{-b_ur}\quad (r\ge0).
\end{equation}

\subsection{The characteristic connection}

\begin{lemma}\label{real:formal-affine}
The formal characteristic leaves of $P$ carry a canonical flat
torsion-free connection. Horizontal lifts to $\ker\alpha$ are
integrable. The lifted fields $P^s,P^u$ are parallel. The horizontal
affine exponential
\[
 \mathcal E_a(V),\quad V\in P_a,
\]
including the height coordinate, is a formal map equivariant under
$f$. Its finite jets have the whole-axis coherence and measurability
from the previous section. Restricted to $P^s_a$ (resp.\ $P^u_a$),
its Taylor series lies in the actual central strong stable (resp.\
unstable) plaque germ.
\end{lemma}

\begin{proof}
On a transversal section, formal Frobenius gives independent first
integrals $z_1,\dots,z_d$ of $L$ ($d=\dim P$). Coisotropy makes the
Hamiltonian fields $X_{z_i}$ lie in $L$ and span $P$; and
\[
 \{z_i,z_j\}=dz_j(X_{z_i})=0,\qquad
 [X_{z_i},X_{z_j}]=0.
\]
Declare this frame parallel. A different system $\widehat z=h(z)$
with invertible differential gives
$X_{\widehat z_i}=\sum_j(\partial_j h_i)(z)X_{z_j}$; the frame-change
matrix is constant on each characteristic leaf, so the connection is
canonical. Its torsion and curvature vanish in the commuting frame.
Since $P$ is isotropic, the bracket of two horizontal lifts has no
Reeb component (the negative of their $d\alpha$-pairing). So
horizontal lifts commute and give the asserted lifted affine
structure.

Equivariance under $f$: raw transformation and normal comparison
commute with the intrinsic Frobenius construction. Pullback/restrict
to sign planes: restricted to positive (resp.\ negative) initial
coordinates, the affine exponential has only same-sign output
components (Taylor monomial argument: no positive combination
$\sum\nu_a\lambda_a$ can equal a negative output weight minus a
positive input weight). The ordinary PDE recursion on the graph
$z=g(v)$ has the actual central plaque as a transversal solution,
so equality of Taylor series is guaranteed by existence.
\end{proof}

\begin{lemma}\label{real:stable-restriction}
On an entire typical strong stable leaf, $P^s$ is a smooth
involutive subbundle with a flat torsion-free connection on its
integral slices. $P^u$ admits a smooth flat partial connection along
those slices, with smooth parallel frames on compact transversal
patches. Analogous assertions with signs exchanged. All structures
are equivariant on transported axis patches.
\end{lemma}

\begin{proof}
Extended values of $P^s$ belong to the actual stable tangent space
everywhere on the axis, by dense agreement and continuity.
Derivatives in $P^s$ directions are actual derivatives within the
smooth axis. Holonomicity identifies them with formal derivatives,
so formal Frobenius becomes actual involutivity. Same for torsion,
curvature, and preservation of the two sign bundles. Frobenius gives
actual smooth integral slices; the restricted connection is flat and
torsion-free. In smooth slice coordinates, the ODEs have coefficients
depending smoothly on the transverse label, giving the smooth parallel
frames. Extend over nonregular points of the axis through smooth
extensions. Equivariance by dense agreement.
\end{proof}

\subsection{Complete proper affine rays}

\begin{lemma}\label{real:local-stable-exponential}
There is a positive-measure set $K$ of regular centers and constants
$\eta_0,c_1,c_2>0$ such that for $a\in K$ and $x\in P^s_a$ with
$|x|\le\eta_0$, the affine geodesic with initial velocity $x$ through
time $1$ stays in a fixed geometric stable plaque and satisfies
\begin{equation}\label{real:local-comparison}
 c_1|x|\le d_s(a,\operatorname{Exp}^s_a x)\le c_2|x|.
\end{equation}
\end{lemma}

\begin{proof}
In bounded coordinates on the stable plaque, the affine geodesic
equation is
\[
 \dot z=v,\quad \dot v=A(z)(v,v),\quad v\in P^s_z.
\]
Acceleration coefficients are finite-order in the formal connection
and smooth by coherence. The geodesic spray is tangent to the velocity
subbundle (connection preserves $P^s$); extend smoothly to all stable
velocities by projection. Ordinary ODE existence applies.

Upper bound from finite coefficients on a bounded plaque. Lower:
if the geodesic endpoints were too close while $|x|\to\infty$, then
stable path-length contraction along backward iterates would force
the geodesic to stay in a bounded set; comparing with diagonal
trivialization of the affine exponential yields
$\operatorname{Exp}^s_a x\to\infty$ uniformly. Details as in
Proposition~\ref{real:proper-exponential}.
\end{proof}

\begin{proposition}\label{real:proper-exponential}
For each nonregular center $v$, some $x_0\in P^s_v$, $x_0\ne0$, gives
a proper affine geodesic $a(t)=\operatorname{Exp}^s_v(tx_0)$ for
$t\ge0$: $\{a(t):t\in[0,\infty)\}$ is bounded away from
$\partial\Ws(v)$ and escapes every compact subset of $\Ws(v)$.
\end{proposition}

\begin{proof}
Work on the strong stable leaf. Exponential localization under stable
contraction: the actual affine exponential is bi-Lipschitz to the
ordinary exponential at small scales
\citep[App., Thm~5.1]{Ballmann1995}.

For properness, suppose not. Let $|x|\to\infty$ and $n=n_i$ be the
first good visit with $|df^n x|\le\eta_0$. Then $n\to\infty$: the
inverse norms of the finitely many earlier linear maps are bounded.
For large $x$ there is a previous good visit $n_{i-1}$, and
minimality gives $|df^{n_{i-1}}x|>\eta_0$. The one-step global
inverse derivative bound plus Lemma~\ref{real:returns} give
\begin{equation}\label{real:subexponential-crossing}
 |df^n x|\ge C^{-1}\eta_0e^{-K(n_i-n_{i-1})}=e^{-o(n)}.
\end{equation}
Constants independent of initial vector. Equivariance and
\eqref{real:local-comparison}:
\[
 d_s(f^na,f^n\operatorname{Exp}^s_a x)\ge c_1|df^nx|.
\]
Compactness: if endpoints stayed in a fixed compact subset $C_0$ of
$\Ws(a)$, their intrinsic distances from $a$ would be bounded.
Stable path-length contraction would instead give
$d_s(f^na,f^n\operatorname{Exp}^s_a x)\le C_{C_0}e^{-b_sn}$,
contradicting \eqref{real:subexponential-crossing}. So proper.
\end{proof}

\subsection{Uniform calculus on the moving plaques}

\begin{lemma}\label{real:iterate-bounds}
Forward iterates restricted to uniform local strong stable plaques
have uniformly bounded derivatives of every fixed order. Same on
weak stable plaques with a bounded local flow coordinate. On the
ambient manifold, for every fixed $j$ there are $C_j,K_j$ with
\[
 \|f^r\|_{C^j}+\|f^{-r}\|_{C^j}\le C_je^{K_jr}\quad(r\ge0)
\]
in bounded local charts (zeroth-order position term omitted). If
$D_0\Subset D_1$ are patches in a strong stable leaf, the sets
$f^{-r}D_0$ have uniform positive intrinsic room inside $f^{-r}D_1$.
\end{lemma}

\begin{proof}[Outline]
Strong and weak plaque estimates from Lemma~\ref{pre:plaque-contraction}.
Ambient estimate: polynomial substitution on the jets; products of
fixed-size matrices of bounded one-step norm grow at most exponentially.
Stable path-length contraction gives
$d_s(f^ra,f^ra')\le Ce^{-b_sr}d_s(a,a')$, hence the room statement.
\end{proof}

\begin{lemma}\label{real:product-derivatives}
Consider a product of fixed-size matrices $A_{r-1}(a)\cdots A_0(a)$
on uniform plaque charts. If $\|A_i\|\le M$ ($M\ge1$) and
$\|D^j A_i\|\le C_j$ uniformly in $i,r$, then
\[
 \|D^j(A_{r-1}\cdots A_0)\|\le C'_j(r+1)^jM^r
 \le C''_je^{(\log M+1)r}.
\]
The exponential rate is independent of $j$. Conclusion holds with a
terminal smooth vector of bounded derivatives.
\end{lemma}

\begin{proof}
Leibniz: at most $C_j(r+1)^j$ choices of factors and derivative
distributions. Each term has at most $j$ differentiated factors
(contributing $C_j$) and at most $r$ undifferentiated (each bounded
by $M$). Finally $(r+1)^j\le C_je^r$. Include terminal vector as one
additional factor.
\end{proof}

\begin{lemma}[Interior interpolation]\label{real:interpolation}
On uniform coordinate balls with a fixed amount of interior room,
for integers $0<j<r$,
\begin{equation}\label{real:interpolation-inequality}
 \|D^ja\|_{C^0}\le C_{j,r}\bigl(\|a\|_{C^0}^{1-j/r}\|a\|_{C^r}^{j/r}
   +\|a\|_{C^0}\bigr).
\end{equation}
If $\|a_n\|_{C^0}\le Ce^{-\beta n}$ and $\|a_n\|_{C^r}\le C_re^{An}$,
the $j$th derivatives are bounded by
\[
 Ce^{-\{\beta(1-j/r)-Aj/r\}n}+Ce^{-\beta n}.
\]
Componentwise for tensors in uniformly bounded frames.
\end{lemma}

\begin{proof}
Taylor interpolation on a fixed unisolvent polynomial stencil rescaled
to size $t$:
\[
 |D^ja(x)|\le C_{j,r}(t^{-j}\|a\|_{C^0}+t^{r-j}\|a\|_{C^r}),\quad 0<t<t_0,
\]
$t_0$ determined by interior room. Choose $t=(\|a\|_{C^0}/\|a\|_{C^r})^{1/r}$
when $\le t_0$, otherwise $t_0$. Gives the inequality; exponential
consequence immediate. Uniform coordinate changes preserve it.
\end{proof}

\begin{lemma}\label{real:returns}
For any typical set of positive measure and each $j$, there is a
positive-measure set of backward returns with a uniform derivative
bound of order $j$ on the return.
\end{lemma}

\begin{proof}[Sketch]
Birkhoff recurrence gives positive frequency of returns; bounded
one-step derivatives give the derivative bound conditioned on short
return time. Iterate back through finitely many intermediate steps
at bounded cost; at the good return the derivative bound is a
bounded polynomial in the return time (Lemma~\ref{real:iterate-bounds}).
A standard measurable-selection argument using the conditional null
characterisation extracts a fixed bound and a positive-measure set.
\end{proof}

\begin{lemma}\label{real:good-points}
Fix an integer $k$ and a small geometric radius $\rho>0$. After a
conull refinement, there is a constant $B_k$ such that every intrinsic
stable disk of radius $\rho$ in each entire typical stable leaf
contains a regular point at which the jets of $\mathcal E$ through
order $k$ have norm $\le B_k$. Refinement can be imposed simultaneously
for all $k$ and all integer iterates.
\end{lemma}

\begin{proof}[Sketch]
Choose finitely many product boxes for the strong stable and weak
unstable foliations, with inner boxes covering $SM$ and outer stable
diameters $<\rho/2$, all compactly inside slightly larger boxes.
Product measure class in each box is the product of its transversal
Lebesgue classes (by stable disintegration and absolute continuity
of weak unstable holonomy).

Choose in each box a positive-measure family of weak unstable plaques
with a common finite bound on the $\mathcal E$-jets through order
$k$ (Lemma~\ref{hull:measurability}). Product measure equivalence
and Fubini give that almost every stable plaque meets this family
(on which the bound holds) in positive stable measure. The points
$\phi^{-r}$ of these intersections give bound $C_ke^{D_kr}$ at
forward images by equivariance and Lemma~\ref{real:iterate-bounds}.
So within a distance $\rho$ backthrough a fixed number of iterates,
every $\rho$-stable-disk contains a bounded jet point.
\end{proof}

\subsection{Actualization}

Set $V_{n,R}(s,y)=\sum_{k=1}^R G_{n,k}(s)[y^{\otimes k}]$ and
$F_{n,R}(a,y)=f^n\exp_{f^{-n}a}V_{n,R}(f^{-n}a,y)$. The $G_{n,k}(s)$
are the coefficients of the polynomial expansion of the formal
equivariant completion $\mathcal F$ of Prop~\ref{real:proper-exponential}'s
truncated jets to the base, computed at time $-n$.

\begin{proposition}\label{real:actualization}
On every compact parameter set and compactly contained base patch,
for every fixed $j$ and $L>0$, all sufficiently large fixed $R$ give
\begin{align}
 \|F-F_{n,R}\|_{C^j}&\le C_{R,j,L}e^{-Ln},
 \label{real:fast-approximation}\\
 \left\|\log_{f^{-n}a}(f^{-n}F(a,y))-V_{n,R}(f^{-n}a,y)\right\|_{C^j}
 &\le C_{R,j,L}e^{-Ln}.
 \label{real:fast-backward}
\end{align}
The function $F$ is smooth, unique among such limits, and equivariant
under $f$.
\end{proposition}

\begin{proof}[Sketch]
First compare consecutive approximants at time $-n$. With
$s=f^{-n}a$, $s_-=f^{-1}s$,
\[
 \Psi_{s_-}(z)=\log_s(f(\exp_{s_-}z))
\]
is uniformly smooth, vanishes at zero, uniformly bounded derivatives
of each fixed order. Exact formal equivariance gives that the
degree-$R$ Taylor truncation of $\Psi_{s_-}(V_{n+1,R}(s_-,y))$ is
$V_{n,R}(s,y)$. Taylor-expand $\Psi_{s_-}$ in $z$ through order $R$:
remainder $C_R|V_{n+1,R}|^{R+1}=O(e^{-c_0(R+1)n})$; each omitted
parameter monomial of degree $\ge R+1$ has the same bound. Hence
\[
 \|F_{n+1,R}-F_{n,R}\|_{C^0}\le C_Re^{-\{c_0(R+1)-A\}n}.
\]
For large fixed $R$, summable. Completeness of the lifted geometric
metric gives a uniform continuous limit. $R'>R$ differs by degrees
$R+1,\dots,R'$, forward push vanishes by the same estimate. All
large fixed cutoffs give one limit $F$.

Smoothness: interpolate on nested compact parameter patches via
Lemma~\ref{real:interpolation}, using consecutive $C^0$ decay
above and $C^q$ growth $B_q$ (Lemma~\ref{real:iterate-bounds}).
Decay exponent $\to\infty$ with $R$, so choosing $R$ large enough
gives any given smoothness order.

Change of geometric log or input frame: uniformly smooth change of
coordinates fixing zero, polynomial remainder, forward push of
fixed-cutoff vanishes. So $F$ is well-defined. Overlapping base
patches: same comparison. Backward-shift equivariance: shifting the
sequence by one step.
\end{proof}

\subsection{The mixed rectangle}

On weak plaques we use whole-strong-leaf representatives and smooth
flow transport.

\begin{lemma}\label{real:stable-tangency}
On every finite base segment of the proper ray $a(t)$, for every
finite initial vector $V(t)\in P^u_{a(t)}$, the point
$z(t)=F_{a(t)}(V(t))$ is in
\[
 \Wu(a(t))\cap\Ws(z(0)),
\]
and $t\mapsto z(t)$ is a smooth path.
\end{lemma}

\begin{proof}
By Proposition~\ref{real:actualization}, $F$ is an actual smooth map
near $P^u=0$ on the moving base patch. The backward representation
$f^{-n}F(a,y)$ stays in a uniformly small unstable neighbourhood of
$f^{-n}a$ for large $n$. Local unstable-manifold characterisation
gives $F(a,y)\in\Wu(a)$; hence $z(t)\in\Wu(a(t))$.

For $z(t)\in\Ws(z(0))$: take the base-direction derivative of $F$
along $a'(t)$. The derivative $D_aF_{a(t)}[a'(t)]$ extends smoothly
to finite parameter tangent. Comparison with actual transported
stable vector from Prop~\ref{real:actualization}:
\[
 \operatorname{dist}(D_aF(a,y)[x],P^s_{F(a,y)})\le C_Le^{-Ln}|x|.
\]
Choose $L$ larger than the fixed exponential norm bound of
$df^n$. Push forward: $\operatorname{dist}(D_aF(a,y)[x],
\Es_{F(a,y)})\to0$. So rectangle tangency holds at regular bases;
smoothness of $F$ and of $P^s$ along the base axis, with continuity
of $\Es$, extends to every base point.

Any finite segment of a smooth curve tangent to $\Es$ has its length
exponentially contracted under positive iteration; its endpoints
belong to one strong stable leaf. Apply to translated base paths;
$F(a(t),y)\in\Wu(a(t))$ handles the other sides.
\end{proof}

\subsection{The ideal-boundary contradiction}

\begin{proposition}\label{real:infinite-excluded}
The infinite-dimensional alternative of Theorem~\ref{alg:dichotomy}
cannot occur.
\end{proposition}

\begin{proof}
Choose a typical lifted center $v$ and a nonzero vector in $P^s_v$.
Proposition~\ref{real:proper-exponential} gives a proper affine ray
$a(t)$, $t\ge0$, in $\Ws(v)$, with $a(0)=v$.
Parallel-transport a sufficiently small nonzero vector
$V_0\in P^u_v$ along this ray using the partial connection in
Lemma~\ref{real:stable-restriction}. On every finite segment this
is an ordinary smooth linear differential equation and therefore
has a solution $V(t)$ throughout that segment. These solutions
agree on overlaps, so $V(t)$ is defined for all finite $t\ge0$.

Use Proposition~\ref{real:actualization} to set
\[
 z(t)=F_{a(t)}(V(t)).
\]
Local parallel frames on the stable slices show that this is a
smooth path; compatibility on overlaps makes it globally well defined.
Proposition~\ref{real:stable-tangency} gives
\[
 z(t)\in\Wu(a(t))\cap\Ws(z(0))
 \qquad(t\ge0).
\]
Only finite parameter values on compact ray segments have been
used, so no boundedness of $V(t)$ as $t\to\infty$ is needed.

Let $\eta$ be the future endpoint of $v$, and $\eta'$ the future
endpoint of $z(0)$. Because $D_VF_v(0)$ is the inclusion of
$P^u_v$, a sufficiently small nonzero $V_0$ has $z(0)\ne v$.
These two vectors belong to one strong unstable leaf. If their
future endpoints also coincided, uniqueness of the connecting
geodesic and equality of their past Busemann levels would force
the vectors to coincide. Therefore $\eta'\ne\eta$.

Write $\zeta_t$ for the past endpoint of $a(t)$. The past-endpoint
map identifies the full strong stable leaf $\Ws(v)$ with
$\partial_\infty\widetilde M\setminus\{\eta\}$: its inverse
takes the geodesic from $\zeta$ to $\eta$ at the fixed
$b_\eta(v)$ level. Existence, uniqueness, and continuity are exactly
the endpoint facts recalled above. Properness of $a(t)$ therefore
implies $\zeta_t\to\eta$. Indeed otherwise a subsequence of its
past endpoints would stay in a compact subset of the boundary
minus $\eta$, whose inverse image in $\Ws(v)$ is compact.

We claim
\begin{equation}\label{real:busemann-divergence}
 b_{\zeta_t}(a(t))\longrightarrow-\infty.
\end{equation}
The sum $b_\eta+b_{\zeta_t}$ is convex and has zero gradient on
the geodesic with these endpoints, so it attains its minimum there.
Let $c(r)$ be the ray from $o$ toward $\eta$. For each fixed $r>0$,
\[
 b_\eta(a(t))+b_{\zeta_t}(a(t))
      \le b_\eta(c(r))+b_{\zeta_t}(c(r)).
\]
As $t\to\infty$ the right-hand side tends to $-2r$, by endpoint
continuity of normalized Busemann functions. The term
$b_\eta(a(t))=b_\eta(v)$ is fixed. Since $r$ is arbitrary,
\eqref{real:busemann-divergence} follows.

On the other hand, $z(t)$ has ordered endpoints
$(\zeta_t,\eta')$ and fixed future Busemann level
$b_{\eta'}(z(0))$. Their limiting pair $(\eta,\eta')$ is off the
diagonal. The corresponding unit tangent vectors therefore
converge to the vector with this limiting pair and that level;
in particular they remain in a compact subset of
$S\widetilde M$. Endpoint continuity now makes
$b_{\zeta_t}(z(t))$ bounded. But $z(t)\in\Wu(a(t))$ means that
the two vectors have the same past endpoint and past Busemann
level, so
\[
 b_{\zeta_t}(z(t))=b_{\zeta_t}(a(t)).
\]
This contradicts \eqref{real:busemann-divergence} and excludes
the infinite-dimensional alternative.
\end{proof}

\section{From formal sign fields to a smooth splitting}
\label{smooth:section}

\paragraph{Plain summary.}
In the finite alternative of Theorem~\ref{alg:dichotomy}, the
formal sign fields have center values exactly $\Es, \Eu$. We prove
these formal objects are actually smooth, so $\Es, \Eu$ are smooth
subbundles. This is the final step; then classical rigidity applies.

The strategy: label each weak unstable leaf by a smooth function $q$
on the (universal cover of the) unit tangent bundle with a canonical
angular coordinate system. The ordinary differential of $q$ produces
a smooth $(m+1)$-bundle containing $E^u\oplus\R X$; intersect with
$\ker\alpha$ to get smooth $E^u$. Flip gives smooth $E^s$.

Work on $\widetilde M$; conclusions descend because all objects are
deck-invariant.

\subsection{Tangency and formal labels}

\begin{lemma}[Tangency to the central plaques]\label{smooth:tangency}
In the finite alternative, the $D$-invariant formal plane field is
tangent to the entire formal central unstable plaque. Consequently,
on each entire typical strong stable leaf, every fixed Taylor jet of
the actual weak unstable plaques is a smooth function of the crossing
point, with holonomic full formal extensions there. Same on the weak
stable leaf generated by that strong stable leaf.
\end{lemma}

\begin{proof}
Use graded section coordinates of Lemma~\ref{sym:graded-contact} and
the dilation of Proposition~\ref{sym:dilation}. Write $x$ for
positive variables, $y$ for negative. Actual central unstable plaque
has formal projection $y=0$. Restrict the positive-sign formal field
from Proposition~\ref{alg:axis-coherence} to $y=0$: graph matrix
$B(x)$ satisfies
$B(e^{tD_+}x)=e^{tD_-}B(x)e^{-tD_+}$.
Diagonalize $D$ over real graded spaces. Monomial $x^\nu$ in a matrix
entry with input weight $\lambda_i>0$, output weight $\mu_j<0$, would
force $\sum_a\nu_a\lambda_a=\mu_j-\lambda_i<0$. Left side
nonnegative, so all coefficients vanish. Formal identity only, no
convergence. Adding flow direction gives formal tangency to weak
unstable plaque.

Actual smooth graph $z=g(v)$ with $g(0)$ the actual crossing.
Tangency gives $\partial_{v_i}g(v)=A_i(v,g(v))$. Recursion determines
each graph coefficient from finitely many operations on the ambient
formal field jet. No existence assertion hidden; actual plaque
provides a formally-tangent solution.

Smooth coefficient dependence on $a$ gives tangential holonomicity
of inverse jets. Construction depends only on the actual plaque
crossing with the transversal. Moving height slice by flow transports
both actual plaque jets and prescribed labels; formal inversion
commutes. Inverse label independent of $u,t$; $\partial_t\Psi
=X\circ\Psi$ gives $Xq=0$. Differentiating scalar jet equivariance
in time gives holonomic derivative identity along $X$; with coherence
on each height slice this proves full holonomicity along $\mathcal B$.
\end{proof}

\subsection{Angular label and smooth propagation}

Let $N_\eta(x)=(x,v_\eta(x))$ be the unit vector at $x$ pointing
toward future endpoint $\eta$. It parametrizes the fixed-future weak
stable leaf $\Ws(\eta)$ as a smooth graph over $\widetilde M$, with
uniform smooth $C^k$ bounds. Near this graph use the intrinsic angular
coordinate
\[
 t=v-\langle v,v_\eta(x)\rangle v_\eta(x)\in v_\eta(x)^\perp,
 \quad \langle v,v_\eta(x)\rangle>0.
\]
This is the tangential component of $v$; so
$v=\sqrt{1-|t|^2}\,v_\eta(x)+t$.

Angular Taylor coefficient of the formal label will be $q_l$, a
smooth symmetric $l$-tensor on the horosphere tangent bundle over
$\mathcal B$, valued in $\R^m$, including the Taylor factorial. In
these coordinates the formal label is
$\sum_{l\ge0}q_l(s,r)[t^l]$, $r$ Busemann height, $s$ coordinates
on its horosphere.

For $\eta\in\partial_\infty\widetilde M$, let $b_\eta$ be Busemann
normalized by $b_\eta(o)=0$, decreasing at unit speed toward $\eta$.
Write $b_\eta(v)=b_\eta(\pi v)$.

Standard facts from uniform negative curvature
\citep[Chap.~II,~III; Lemma~III.3.1]{Ballmann1995}: distinct ideal
points determine a unique geodesic; these depend continuously on
endpoints off the diagonal; Busemann depends continuously on
endpoint, uniformly on compact spatial sets; prescribing ordered
distinct endpoints and the Busemann level at the future endpoint
determines a unit tangent vector continuously.

\begin{lemma}[Crossing continuity]\label{smooth:crossing}
The crossing $a(v)$ in \eqref{smooth:actual-graphs} depends
continuously on $v$, so $a(K)$ is compact in the base for compact $K$.
\end{lemma}

\begin{proof}
Fix a compact $K$. Past endpoint $\zeta=v_-$. Bounded continuous
time shift
$\tau(v)=b_\zeta(\pi v)-b_\zeta(\pi a(v))$. Vector
$z(v)=\phi_{\tau(v)}a(v)$ has the same past endpoint and past
Busemann height as $v$, hence is on its strong unstable leaf; also
intrinsic strong unstable distance is uniformly bounded on $K$.
Uniformity: join base points by spatial geodesic of bounded length;
project onto the common past horosphere along Busemann gradient flow;
flow times bounded by segment length. Uniform Busemann Hessian bounds
projected path length and its lift to the normal graph.

Backward strong unstable contraction:
$d^u(f^{-n}v,f^{-n}z(v))\le Ce^{-bn}$. Write
$f^{-n}v=(x_n,v_n)$, $f^{-n}z(v)=N_\eta(y_n)$. Uniform local bounds
of $N_\eta$ give
$d(N_\eta(x_n),N_\eta(y_n))\le Ce^{-bn}$ and angular bound. Let
$\epsilon_n=b_\eta(x_n)-b_\eta(y_n)$; $|\epsilon_n|\le Ce^{-bn}$.
Then $\phi_{\epsilon_n}N_\eta(x_n)$ and $N_\eta(y_n)$ are on same
strong stable leaf with intrinsic distance $O(e^{-bn})$. Forward
strong stable contraction and unchanged small shift give
$f^nN_\eta(x_n)$ within $O(e^{-bn})$ in the compact family $z(v)$.
Compact-axis assertion.

Local crossing: uniform transversality bound. At $t=0$, weak
unstable plaque intersected with $b_\eta=r$ has tangent $E^u$. In
Jacobi coordinates, differential of angular coordinate in a spatial
direction $a$ is $(U(v)+U(-v))a$, uniformly positive definite. Uniform
smooth bounds plus inverse function theorem give actual graphs
\begin{equation}\label{smooth:actual-graphs}
 s=P_{s_0,r}(t),\quad P_{s_0,r}(0)=s_0,
\end{equation}
on a fixed radius, uniform bounded derivatives in $t$ of each order.
No derivative in $s_0$ is asserted.
\end{proof}

\begin{lemma}[Derivative-order-independent bound]\label{smooth:naive}
For each angular degree $l$ there is $A_l<\infty$ such that for every
$j\ge0$ and every compact $L\Subset\mathcal B$,
\begin{equation}\label{smooth:naive-bound}
 \|q_l\|_{C^j(L_n)}\le C_{L,l,j}e^{A_ln}.
\end{equation}
The exponent $A_l$ is independent of $j$.
\end{lemma}

\begin{proof}
Transport full ambient scalar jet of order $l$ from $f^np$ to $p$
using the finite-dimensional linear pullback-jet matrices
$M_l(p)$. In uniformly bounded geometric charts these matrices and
every fixed-order weak-axis derivative are uniformly bounded (smooth
one-step ambient, uniform leafwise chart bounds). Transport over $n$
steps $=$
$M_l(f^{n-1}p)\cdots M_l(p)$. Differentiating in a weak-axis
direction at $p$ differentiates at most $j$ factors, giving at most
a constant times $(1+r)^jM_l^n$ by Lemma~\ref{real:product-derivatives}.
Absorb polynomial into $e^{n}$, with $j$-dependent prefactor, giving
$A_l=1+\log M_l$. Using ambient derivative bounds for $f^n$ instead
would lose the $j$-independence.
\end{proof}

\begin{lemma}[Subexponential bounds for every axis derivative]\label{smooth:subexponential}
For every $l,j\ge0$, every $\epsilon>0$, and every compact
$L\Subset\mathcal B$, there is $C_{L,l,j,\epsilon}$ with
\begin{equation}\label{smooth:subexponential-bound}
 \|q_l\|_{C^j(L_n)}\le C_{L,l,j,\epsilon}e^{\epsilon n}.
\end{equation}
\end{lemma}

\begin{proof}
Induct on $l$. For $l=0$: $q_0(p)=q_0(f^np)$ and bounded weak-axis
derivatives of forward iterates give bounded derivatives on $L_n$.

At each fixed height, formal constancy on the actual graph
\eqref{smooth:actual-graphs} gives
\begin{equation}\label{smooth:crossing-identity}
 \sum_{k\ge0}q_k(P_{s_0,r}(t),r)[t^k]=q_0(s_0,r).
\end{equation}
Every occurrence on LHS: Taylor expand at $t=0$. Identity from formal
crossing inversion of Lemma~\ref{smooth:tangency} and tangential
holonomicity. In degree $l$, only term containing $q_l$ is
$q_l(s_0,r)[t^l]$. Others involve derivatives in $s$ of $q_k$
($k<l$) at order $\le l-k$, multiplied by polynomials in
$t$-derivatives of $P_{s_0,r}$ through order $l$, all uniformly
bounded. Induction and polarization of the degree-$l$ identity:
\[
 \|q_l\|_{C^0(L_n)}\le C_{L,l,\epsilon}e^{\epsilon n}\quad
 \text{for every }\epsilon>0.
\]

Upgrade to arbitrary weak-axis derivatives via interpolation on the
full axis. Elementary Taylor difference estimate
$\|D^ju\|_{C^0}\le C_{j,r}(h^{-j}\|u\|_{C^0}+h^{r-j}\|u\|_{C^r})$,
$0<h<h_0$; constants independent of $n$ by uniform interior room.
Fix $j\ge1$, target $\epsilon$; take $\delta=\epsilon/(4j)$,
$h=e^{-\delta n}$; use value bound with exponent $\epsilon/4$ and
fixed $r>j+A_l/\delta$; by Lemma~\ref{smooth:naive}, the terms have
exponents $\epsilon/2$ and $A_l-\delta(r-j)<0$. Induction complete.
\end{proof}

\subsection{Smoothness of the actual label}

\begin{proposition}[Propagation from the axis]\label{smooth:propagation}
The actual endpoint label $q:\mathcal U\to\R^m$ is $\C^\infty$.
\end{proposition}

\begin{proof}
Since $q_l$ satisfy subexponential bounds, Taylor polynomials
$p_{n,R}$ at the current time, truncated at degree $\le R$, approximate
$q$ in $C^j$ norm with exponential tail on a compact $K$ of the
interior of $\mathcal U$:
\[
 \|p_{n+1,R}-p_{n,R}\|_{C^j(K)}\le Ce^{-\lambda n},
\]
$\lambda>0$ arbitrary, with rate
$\bigl(b(R+1)-1\bigr)(1-j/r)-(B_r+1)j/r$ after choosing
$r=2j+2$, $\epsilon=1$, and $R$ large. Fixed interior pair
$K\Subset K^+$ gives $n$-independent constants. So $p_{n,R}$ converges
in $C^j(K)$ as $n\to\infty$ for fixed $R$, and the limit is a
fixed-$R$ polynomial approximation to $q$. Repeating with $R_k$
growing and $n_k\to\infty$ satisfying
$\|p_{n_k,R_k}-q\|_{C^k(K)}\le2^{-k}$ gives smoothness. Every stage
evaluates only finite polynomials; no convergence assumption on
formal series.
\end{proof}

\subsection{Nondegeneracy: the strong bundles are smooth}

\begin{lemma}[Volume comparison for weak unstable holonomy]\label{smooth:holonomy-volume}
Between two smooth $m$-dimensional local transversals to the weak
unstable foliation, its holonomy $h$ satisfies locally
$c\,\Vol(E)\le\Vol(h(E))\le C\,\Vol(E)$ for measurable $E$, with
$0<c\le C<\infty$.
\end{lemma}

\begin{proof}
Strong unstable holonomy between smooth transversals is absolutely
continuous with locally bounded positive Jacobian; inverse holonomy
supplies the reciprocal \citep[App., Thm~5.1, Def.~3.3]{Ballmann1995}.
The weak foliation is generated by the strong unstable foliation plus
the Reeb field; the flow is a diffeomorphism preserving any bounded
flow-box volume ratio. Direct extension.
\end{proof}

\begin{theorem}[Global smooth splitting]\label{smooth:splitting}
In the finite alternative, $\Es$ and $\Eu$ are $\C^\infty$
subbundles of $TSM$.
\end{theorem}

\begin{proof}
It suffices to prove $E^u$ smooth on $SM$; flip and deck descent
give $E^s$.

Smoothness of $q:\mathcal U\to\R^m$
(Proposition~\ref{smooth:propagation}). Nondegeneracy: if $dq_p$ had
rank $<m$, use smooth coordinate charts on source sphere and target
with volume densities bounded above and below; the image of a
coordinate ball of radius $r$ would have width $O(r)$ in $m-1$
directions but $o(r)$ in the missing direction (differentiability);
volume $o(r^m)$, contradicting fixed positive lower volume bound
(Lemma~\ref{smooth:holonomy-volume}). So $dq$ surjective at every
point of $\mathcal U$. Smooth bundle $\ker dq$ has dim $m+1$ and
contains tangent spaces of the actual weak unstable leaves ($q$
constant there). Dimensions agree:
$\ker dq=E^u\oplus\R X$ on $\mathcal U$. Intersect with smooth
contact distribution: smooth strong unstable bundle
$E^u=(\ker dq)\cap\ker\alpha$.

Coordinate patches of the full typical strong stable axis cover all
past endpoints except $\eta$. A second typical axis with distinct
future endpoint covers the omitted endpoint. Such an axis exists
because typical points have full smooth measure, whereas a single
fixed-future weak leaf has positive codimension. So $E^u$ smooth on
the cover. Flip $v\mapsto-v$ exchanges strong bundles, giving
smoothness of $E^s$. Both are the actual invariant bundles, deck
invariant, descend smoothly to $SM$.
\end{proof}

\section{Completion of the proof}
\label{sec:completion}

\paragraph{Plain summary.}
We now assemble the chain into the final proof.

\emph{Forward direction} (equality $\Rightarrow$ local symmetry):
\[
\text{entropy equality}
\;\xrightarrow{\text{pre:entropy-forms}}\;
\text{conormal forms }u,w
\;\xrightarrow{\text{hull:main}}\;
\text{affine fields}
\]
\[
\;\xrightarrow{\text{alg:dichotomy}}\;
\text{algebraic alternative}
\;\xrightarrow{\text{real:infinite-excluded}}\;
\text{finite implies smooth}
\;\xrightarrow{\text{smooth:splitting}}\;
\Es,\Eu\text{ smooth}
\]
\[
\;\xrightarrow{\text{pre:smooth-rigidity}}\;
\nabla^g R_g=0.
\]

\emph{Reverse direction} (local symmetry $\Rightarrow$ equality):
If $(M,g)$ is locally symmetric, the metric is homogeneous
positive-definite, and a direct calculation gives $h_{m_L}=\htop$.

\subsection{Preliminary facts}

Finite covers preserve local symmetry (a metric is locally symmetric
iff its universal cover is symmetric) and preserve $|R_g|$,
$|\nabla^gR_g|$. So we may replace $M$ by an oriented finite cover,
as already assumed in \S\ref{pre:section}.

Equivalent characterisations of local symmetry: $\nabla^gR_g=0$;
universal cover symmetric space; holonomy reduction to a compact
group; existence of an invariant parallel metric-preserving
connection.

Negative curvature plus local symmetry in rank one gives the choices
$\R H^n$, $\C H^n$, $\mathbb H H^n$ (quaternionic), and $\mathbb O H^2$ (Cayley),
which are exactly the rank-one symmetric spaces of noncompact type.
The converse is standard.

\subsection{Proof of Theorem~\ref{thm:main}}

\begin{proof}[Proof of Theorem~\ref{thm:main}]
Suppose first that the entropies are equal,
$h_{m_L}(\phi_1)=\htop(\phi_1)=h$.
Proposition~\ref{pre:entropy-forms} provides the transported conormal
volumes $u,w$. Theorem~\ref{hull:main} constructs their coherent
formal affine fields $\mathcal A^u,\mathcal A^s$.
Proposition~\ref{sym:effective} and Theorem~\ref{alg:dichotomy} give
the algebraic alternative. Proposition~\ref{real:infinite-excluded}
excludes its infinite-dimensional case. In the finite-dimensional
case, Theorem~\ref{smooth:splitting} proves that $\Es$ and $\Eu$ are
smooth on all of $SM$. Proposition~\ref{pre:smooth-rigidity}
therefore gives $\nabla^gR_g=0$, i.e.\ local symmetry.

For the converse suppose $\nabla^gR_g=0$. The universal cover is a
rank-one symmetric space of noncompact type. The unit-speed geodesic
flow is homogeneous with respect to the connected isometry group, so
the unstable Riccati tensor $U$ is invariant under isometries and in
particular its trace $J=\tr U$ is a positive constant $J_0$ on $SM$.

By Proposition~\ref{pre:entropy-forms}, Liouville measure $m_L$ is
an equilibrium state of the constant potential $-J_0$, hence of
$-h$ (with $h=J_0$). Thermodynamic formalism gives that the entropy
$h_{m_L}(\phi_1)=\int J_0\,dm_L=J_0$. Classical volume-growth
computation (Manning \citep{Manning1979}) gives
$\htop(\phi_1)=J_0$ too; equivalently $\htop=$ the exponential growth
rate of balls in the universal cover, which equals the area of the
horosphere. Hence $h_{m_L}=\htop$.
\end{proof}

\subsection{Proof of the classical rigidity step}

\begin{proof}[Proof of Proposition~\ref{pre:smooth-rigidity}]
Suppose the $\Es,\Eu$ splitting is $\C^\infty$ on $SM$.

\emph{Step 1 (Benoist--Foulon--Labourie).} A closed negatively curved
geodesic flow with $\C^\infty$ Anosov splitting is smoothly orbit-
conjugate, up to finite covers and normalization of the time
parameter, to the geodesic flow of a locally symmetric negatively
curved metric on the same underlying closed manifold. See
\citet[Theorem~2.1, Theorem~B]{BenoistFoulonLabourie1992}.

\emph{Step 2 (Period identities).} Let $SM_0$ be the model unit
tangent bundle with contact form $\alpha_0$ and Reeb vector field
$X_0$, and let $h:SM\to SM_0$ be the orbit-preserving conjugacy. The
pullback $h^*\alpha_0$ is a contact form of the original flow.
Modulo an overall scale, the orbit equivalence is represented by a
canonical time density
\[
 a_0+\beta(X_0)>0,
\]
where $a_0>0$ is a constant and $\beta$ is a closed one-form on
$SM_0$. Its period on a conjugacy class $\gamma$ is
\[
 a_0\ell_0(\gamma)+\int_\gamma\beta.
\]
Geodesic periods agree for inverse classes:
$\ell_0(\gamma)=\ell_0(\gamma^{-1})$. The group isomorphism induced
by the conjugacy respects inversion, whereas the integral of $\beta$
changes sign. Hence its integral vanishes on every closed geodesic
lift. Since $\pi_1(SM_0)\simeq\pi_1(M_0)$ for $n\ge3$ (the
$(n-1)$-sphere is simply connected), these lifts represent every
nontrivial conjugacy class in $SM_0$. So all periods of $\beta$
vanish; hence $\beta=db$ for some smooth function $b$.

\emph{Step 3 (Removing the exact correction).} The orbit shift
\[
 x\longmapsto\phi_{b(x)/a_0}^0(x)
\]
sends the vector field $X_0/(a_0+X_0b)$ to $X_0/a_0$. It is a
diffeomorphism: its orbit derivative is positive; its bounded time
displacement makes it onto on nonperiodic orbits and degree one on
periodic orbits. This removes the exact correction.

\emph{Step 4 (Metric recovery).} The orbit foliations of $g$ and
$g_0$ on $SM$ coincide (via $h$). The positive function $\psi$
defined by $g=\psi^2g_0$ (or rather $g(\xi,\xi)=\psi^2g_0(\xi,\xi)$
along unit model vectors) has $\psi=h$-constant, i.e.\ constant on
orbits. But $\psi$ is also smooth and non-orbital; the natural
normalization $g_0=g$ on a positive-measure subset (by the volume
comparison below) forces $\psi\equiv1$.

\emph{Step 5 (Volume/entropy normalization).} Liouville measures of
the two flows both integrate the same top form once orbit
equivalence is accounted for. Besson--Courtois--Gallot's minimal
entropy rigidity \citep{BessonCourtoisGallot1995} applies at equality
of entropy between the two flows model and target; it forces the
identifying map to be an isometry. So $g$ is isometric to the
locally symmetric $g_0$; in particular $\nabla^gR_g=0$.
\end{proof}

\subsection{Remarks}

The proof separates Liouville measure from the entropy-maximising
measure when the metric is not locally symmetric. By the theorem,
$m_L$ itself is not entropy-maximising in that case. The unique
entropy-maximising probability measure exists by thermodynamic
formalism \citep{BowenRuelle1975}; it is ergodic; and distinct
ergodic invariant probability measures are mutually singular.

No curvature bound beyond strict negativity is used: the ratio of
sectional curvatures is unrestricted.

\subsection*{Acknowledgements}

The argument spans work of many mathematicians. We thank the
Benoist--Foulon--Labourie team, whose \citeyear{BenoistFoulonLabourie1992}
classification of smooth Anosov contact flows is the classical
rigidity engine; the Besson--Courtois--Gallot school whose minimal
entropy rigidity enters at the last step; and the Lie theory of
Cartan--Guillemin, Fattori--Kac, and Bakalov--D'Andrea--Kac, whose
classification of linearly compact Lie algebras drives the algebraic
dichotomy.

% ---------------------------------------------------------------------
% Bibliography
% ---------------------------------------------------------------------

\begin{thebibliography}{999}

\bibitem[Anosov(1967)]{Anosov1967}
D.~V.~Anosov.
\newblock Geodesic flows on closed Riemannian manifolds of negative
  curvature.
\newblock \emph{Trudy Mat. Inst. Steklov.} 90 (1967), 3--210.

\bibitem[Bakalov--D'Andrea--Kac(2001)]{BakalovDAndreaKac2001}
B.~Bakalov, A.~D'Andrea, V.~G.~Kac.
\newblock Theory of finite pseudoalgebras.
\newblock \emph{Adv. Math.} 162 (2001), 1--140.

\bibitem[Ballmann(1995)]{Ballmann1995}
W.~Ballmann.
\newblock \emph{Lectures on spaces of nonpositive curvature}.
\newblock Birkh\"auser, 1995. With an appendix by Misha Brin.

\bibitem[Benoist--Foulon--Labourie(1992)]{BenoistFoulonLabourie1992}
Y.~Benoist, P.~Foulon, F.~Labourie.
\newblock Flots d'Anosov \`a distributions stable et instable
  diff\'erentiables.
\newblock \emph{J. Amer. Math. Soc.} 5 (1992), 33--74.

\bibitem[Besson--Courtois--Gallot(1995)]{BessonCourtoisGallot1995}
G.~Besson, G.~Courtois, S.~Gallot.
\newblock Entropies et rigidit\'es des espaces localement
  sym\'etriques de courbure strictement n\'egative.
\newblock \emph{Geom. Funct. Anal.} 5 (1995), 731--799.

\bibitem[Bowen(1975)]{BowenRuelle1975}
R.~Bowen.
\newblock \emph{Equilibrium states and the ergodic theory of Anosov
  diffeomorphisms}.
\newblock Springer LNM 470, 1975.

\bibitem[Climenhaga(2024)]{Climenhaga2024}
V.~Climenhaga.
\newblock SRB and equilibrium measures via dimension theory.
\newblock In \emph{A Vision for Dynamics in the 21st Century}, Cambridge
  Univ. Press, 2024, pp.~94--138.

\bibitem[De~Simoi--Leguil--Vinhage--Yang(2020)]{DeSimoiLeguilVinhageYang2020}
J.~De~Simoi, M.~Leguil, K.~Vinhage, Y.~Yang.
\newblock Entropy rigidity for three dimensional volume-preserving
  Anosov flows.
\newblock Preprint, 2020.

\bibitem[Fattori--Kac(2002)]{FattoriKac2002}
S.~Fattori, V.~G.~Kac.
\newblock Classification of simple linearly compact $n$-Lie
  conformal algebras.
\newblock \emph{Comm. Math. Phys.} 228 (2002), 263--304.

\bibitem[Flaminio(1995)]{Flaminio1995}
L.~Flaminio.
\newblock Local entropy rigidity for hyperbolic manifolds.
\newblock \emph{Comm. Anal. Geom.} 3 (1995), 195--248.

\bibitem[Foulon(2001)]{Foulon2001}
P.~Foulon.
\newblock Entropy rigidity of Anosov flows in dimension three.
\newblock \emph{Ergodic Theory Dynam. Systems} 21 (2001), 1101--1112.

\bibitem[Guillemin(1968)]{Guillemin1968}
V.~Guillemin.
\newblock A Jordan--H\"older decomposition for a certain class of
  infinite dimensional Lie algebras.
\newblock \emph{J. Differential Geom.} 2 (1968), 313--345.

\bibitem[Hartshorne(1977)]{Hartshorne1977}
R.~Hartshorne.
\newblock \emph{Algebraic Geometry}.
\newblock GTM 52, Springer, 1977.

\bibitem[Hirsch--Pugh--Shub(1977)]{HirschPughShub1970}
M.~W.~Hirsch, C.~C.~Pugh, M.~Shub.
\newblock \emph{Invariant Manifolds}.
\newblock Springer LNM 583, 1977.

\bibitem[Humbert(2026)]{Humbert2026}
T.~Humbert.
\newblock Katok's entropy conjecture near real and complex hyperbolic
  metrics.
\newblock \emph{Duke Math. J.} 175 (2026), 135--184.

\bibitem[Kalinin--Sadovskaya(2017)]{KalininSadovskaya2017}
B.~Kalinin, V.~Sadovskaya.
\newblock Normal forms for non-uniform contractions.
\newblock \emph{J. Mod. Dyn.} 11 (2017), 341--368.

\bibitem[Katok(1982)]{Katok1982}
A.~Katok.
\newblock Entropy and closed geodesics.
\newblock \emph{Ergodic Theory Dynam. Systems} 2 (1982), 339--365.

\bibitem[Liv\v{s}ic(1972)]{Livsic1972}
A.~N.~Liv\v{s}ic.
\newblock Cohomology of dynamical systems.
\newblock \emph{Math. USSR-Izv.} 6 (1972), 1278--1301.

\bibitem[Mangolte(2019)]{Mangolte2019}
F.~Mangolte.
\newblock \emph{Real Algebraic Varieties}.
\newblock Springer, 2019.

\bibitem[Manning(1979)]{Manning1979}
A.~Manning.
\newblock Topological entropy for geodesic flows.
\newblock \emph{Ann. of Math.} 110 (1979), 567--573.

\bibitem[Melnick(2019)]{Melnick2019}
K.~Melnick.
\newblock Nonstationary smooth geometric structures for contracting
  measurable cocycles.
\newblock Preprint, 2019.

\bibitem[Milne(2013)]{Milne2013}
J.~S.~Milne.
\newblock \emph{Lie Algebras, Algebraic Groups, and Lie Groups}.
\newblock Available at \texttt{https://www.jmilne.org/math/}, 2013.

\bibitem[Oseledets(1968)]{Oseledets1968}
V.~I.~Oseledets.
\newblock A multiplicative ergodic theorem. Lyapunov characteristic
  numbers for dynamical systems.
\newblock \emph{Trans. Moscow Math. Soc.} 19 (1968), 197--231.

\bibitem[Pesin(1977)]{Pesin1977}
Ya.~B.~Pesin.
\newblock Characteristic Lyapunov exponents and smooth ergodic theory.
\newblock \emph{Russian Math. Surveys} 32 (1977), 55--114.

\bibitem[Ruan(2024)]{Ruan2024}
X.~Ruan.
\newblock On the Cayley case of the Besson--Courtois--Gallot rigidity.
\newblock Preprint, 2024.

\bibitem[Ruelle(1978)]{Ruelle1978}
D.~Ruelle.
\newblock An inequality for the entropy of differentiable maps.
\newblock \emph{Bol. Soc. Brasil. Mat.} 9 (1978), 83--87.

\bibitem[Stacks Project(2026)]{StacksProject}
The Stacks Project Authors.
\newblock \emph{The Stacks Project}.
\newblock Tags 00FN, 00P0, 00KU, 00NP, 0B8X, 07ND, 02K4, 02G1. Available
  at \texttt{https://stacks.math.columbia.edu}, 2026.

\bibitem[Tserunyan(2025)]{Tserunyan2025}
A.~Tserunyan.
\newblock \emph{Introduction to Descriptive Set Theory}.
\newblock Lecture notes, McGill University, 2025.

\end{thebibliography}

\end{document}