7 The two-sided splitting
The one-sided multiplicative ergodic theorem produces, for a measurable matrix cocycle over an ergodic system, a decreasing measurable equivariant filtration \(\mathbb {R}^d = V_0(x) \supsetneq V_1(x) \supsetneq \cdots \supsetneq V_k(x) = 0\) whose successive quotients carry the distinct Lyapunov exponents \(\lambda _0 {\gt} \cdots {\gt} \lambda _{k-1}\). When the base dynamics is invertible and the generator is everywhere invertible with \(\log ^+\left\lVert A \right\rVert , \log ^+\left\lVert A^{-1} \right\rVert \in L^1\), the filtration upgrades to a genuine direct-sum splitting \(\mathbb {R}^d = E_0(x) \oplus \cdots \oplus E_{k-1}(x)\), with each \(E_i\) equivariant and the cocycle growing at the exact rate \(+\lambda _i\) forward and \(-\lambda _i\) backward on \(E_i \setminus \{ 0\} \).
This chapter develops that upgrade. The strategy applies the one-sided theorem twice — once forward to \((T, A)\), once to a reflected backward generator over \(T^{-1}\) — and intersects the two filtrations. Two genuinely new analytic nodes carry the argument: an identification of the Kingman subadditive constant with the limit of integral means, and a backward-orbit growth envelope for restricted cocycles. Their consequence is the transversality crux: forward and backward exponents of any common nonzero vector add to a nonnegative number, so opposite-side sublevels meet in \(0\). A pure multiset reflection lemma then aligns the backward spectrum to the negated forward one, after which a telescoping-flag lattice argument assembles the splitting.
7.1 The invertible setup and the backward generator
The base dynamics is an invertible measure-preserving system \(T : X \simeq _m X\) (a MeasurableEquiv) with \(T^{-1} = T.\mathrm{symm}\). The backward iterates of the cocycle \(A^{(n)}(x) = \mathrm{cocycle}\, A\, T\, n\, x\) are governed by the backward generator, a generator over \(T^{-1}\) whose cocycle reflects the forward one through inverse and orbit reversal.
For \(A : X \to \mathrm{Matrix}\, (\mathrm{Fin}\, d)\, (\mathrm{Fin}\, d)\, \mathbb {R}\) and \(T : X \simeq _m X\), the backward generator is
Its cocycle is taken over \(T^{-1}\).
For any generator \(A\) and map \(T\), \(A^{(n+1)}(x) = A(T^{[n]}x)\cdot A^{(n)}(x)\).
This is the companion of the standard recursion \(A^{(n+1)}(x) = A^{(n)}(Tx)\cdot A(x)\): apply the additive law \(A^{(m+n)} = A^{(m)}(T^{[n]}\cdot )\cdot A^{(n)}\) with \(m = 1\) after commuting the summands.
Writing \(B = \mathrm{backwardGen}\, A\, T\), the cocycle of \(B\) over \(T^{-1}\) satisfies
Induct on \(n\). The successor step expands \(B^{(n+1)}\) by the left recursion, applies the inductive hypothesis at \(T^{-1}x\), rewrites \(B = (A\circ T^{-1})^{-1}\) by lemma 7.2, and collapses the product of inverses by \(\mathrm{Matrix.mul\_ inv\_ rev}\); a left-inverse iterate identity \((T\circ T^{-1})^{[n]} = \mathrm{id}\) reindexes the orbit point. The dual form follows by substituting \(x = T^{n}y\) and cancelling \((T^{-1}\circ T)^{[n]} = \mathrm{id}\). This identity is exactly what makes the second (backward) growth limit in the splitting theorem the cocycle \((A^{(n)}(T^{-n}x))^{-1}\), avoiding any moving-point singular-value bookkeeping.
If \(\det A(x) \neq 0\) for all \(x\), \(A\) is measurable, \(T\) is measure-preserving, and \(\log ^+\left\lVert A \right\rVert , \log ^+\left\lVert A^{-1} \right\rVert \in L^1(\mu )\), then the backward system \((T^{-1}, B)\) satisfies the same four hypotheses: \(\det B \neq 0\) everywhere, \(B\) measurable, and \(\log ^+\left\lVert B \right\rVert , \log ^+\left\lVert B^{-1} \right\rVert \in L^1(\mu )\).
Invertibility of \(B = (A\circ T^{-1})^{-1}\) is \(\det (M^{-1}) = (\det M)^{-1} \neq 0\); measurability is composition of matrix inversion with the measurable \(T^{-1}\). For integrability, \(T^{-1}\) is measure-preserving (Mathlib’s \(\mathrm{MeasurePreserving.symm}\)), so \(\log ^+\left\lVert B \right\rVert = \log ^+\left\lVert A^{-1} \right\rVert \circ T^{-1}\) and \(\log ^+\left\lVert B^{-1} \right\rVert = \log ^+\left\lVert A \right\rVert \circ T^{-1}\) (using \((M^{-1})^{-1} = M\)) transfer by composition. Crucially \(T\) ergodic implies \(T^{-1}\) ergodic (Mathlib’s \(\mathrm{Ergodic.symm}\)), so the one-sided theorem applies verbatim to the backward system.
For \(T\) measure-preserving on a probability space and a conull measurable set \(S\), there is a conull measurable \(S' \subseteq S\) invariant under both \(T\) and \(T^{-1}\).
Take \(S' = \bigl(\bigcap _n (T^{[n]})^{-1}S\bigr) \cap \bigl(\bigcap _n (T^{-[n]})^{-1}S\bigr)\). Each iterate is measure-preserving, so every preimage of the conull \(S\) is conull and the countable intersection is conull. Membership is "all forward and backward iterates land in \(S\)"; applying \(T\) or \(T^{-1}\) merely shifts the index, the cross term collapsing through \(T^{-1}\circ T = \mathrm{id}\).
7.2 The strong one-sided export with dimensions
The crux argument needs the dimensions of the filtration spaces, which the headline one-sided statement quantifies away. We re-run the one-sided composition with concrete witnesses, exposing the spectrum \(\lambda \) and the filtration \(V\) together with a dimension formula.
Under the one-sided hypotheses (with \([\mathrm{NeZero}\, d]\)) there exist a decreasing exponent sequence \(\mathrm{lam0} : \mathbb {N}\to \mathbb {R}\) realizing the a.e. per-index singular-value limits, and a measurable filtration \(V : \mathrm{Fin}(k+1) \to X \to \mathrm{Submodule}\, \mathbb {R}\, (\mathbb {R}^d)\) where \(k = \mathrm{numExp}\, \mathrm{lam0}\, d\), such that for a.e. \(x\): \(V_0 x = \top \), \(V_k x = \bot \), \(V\) is strictly decreasing and \(A\)-equivariant, every \(v \in V_{i}x \setminus V_{i+1}x\) grows at rate \(\mathrm{expEnum}\, \mathrm{lam0}\, d\, i\), and
This is the committed one-sided assembly, re-run with the concrete witness \(V = V'\, A\, T\, \mathrm{lam0}\): obtain \(\mathrm{lam0}\) from the singular-value exponents, discharge the top-gap mass envelope, build the spectral, slow-flag and growth interfaces exactly as the headline proof does, and read the structural block off the same conull set. The dimension formula is supplied by proposition 7.7 combined with the slow-flag identification \(V'_i x = \mathrm{vslow}\, (\exp \lambda _i)\, x\).
For a.e. \(x\) and all \(t \in \mathbb {R}\),
The sanitized limit operator \(\widehat\Lambda \) has an orthonormal eigenbasis with eigenvalues \(\exp (\mathrm{lamSing}\, x\, e)\), and a.e. \(\mathrm{lamSing}\, x\, j = \mathrm{lam0}\, j\) (a countable conjunction over \(j {\lt} d\)). The slow space is the range of a spectral sublevel projector \(\mathrm{cfc}\, f\, \widehat\Lambda \); lemma 7.8 shows it acts diagonally on the eigenbasis with eigenvalues in \(\{ 0,1\} \), and the rank of such a self-adjoint idempotent equals the number of \(1\)-eigenvectors, which by \(\exp \)-monotonicity of the threshold is \(\# \{ j : \mathrm{lam0}\, j \le t\} \).
If \(M\) is self-adjoint and \(M v = c\, v\) for \(v \neq 0\), then \((\mathrm{cfc}\, f\, M)\, v = f(c)\cdot v\).
The eigenvalue \(c\) lies in the (finite) spectrum of \(M\). Pick a Lagrange interpolating polynomial \(q\) with \(q = f\) on the spectrum; then \(\mathrm{cfc}\, f\, M = \mathrm{cfc}\, q\, M = q(M)\), and \(q(M)v = q(c)v = f(c)v\) because \(v\) is an eigenvector. This is pointwise, so no measurability is incurred.
7.3 The Kingman means identification
The repository’s ergodic Kingman theorem exhibits a constant \(c\) with \((1/n)g_n \to c\) a.e., but defers identifying \(c\) with the Fekete infimum of the integral means. The two-sided theorem is the first consumer that needs the means form, in order to equate the Kingman constants of a subadditive cocycle over \(T\) and of its orbit-reversed version over \(T^{-1}\).
Under the hypotheses of the ergodic Kingman theorem, there is a constant \(c\) with
Let \(L\) be the Fekete limit of the means (existing by subadditivity). For \(c \le L\): iterate subadditivity \(g_{mn}(x) \le \sum _{j{\lt}m} g_n(T^{[jn]}x)\), divide by \(mn\) and let \(m\to \infty \); the left side converges to \(c\) along a subsequence, the right to the Birkhoff average of \((1/n)g_n\) for the measure-preserving \(T^{[n]}\) (no ergodicity needed), whose integral is \((1/n)\int g_n\); integrate the inequality. For \(c \ge L\): apply Fatou to the nonnegative sequence \(A_n - \mathrm{cdiv}_n\), where \(A_n\) is the Birkhoff average of \(g_1\) (nonnegative by single-step subadditivity) and \(\mathrm{cdiv}_n\) tends to \(L\); since \(A_n - \mathrm{cdiv}_n \to B - c\) a.e. and \(\int A_n = \int g_1\), Fatou yields \(\int g_1 - L \ge \int g_1 - c\).
7.4 Restricted cocycles and their exponent
To measure the growth of \(A^{(n)}\) restricted to a filtration level \(V_i\), we form a restricted cocycle by post-composing the orthogonal projector onto \(V_i\). A floor term repairs the failure of everywhere-subadditivity off the good set, so that Kingman applies without an a.e. caveat.
For a measurable family \(V : X \to \mathrm{Submodule}\, \mathbb {R}\, (\mathbb {R}^d)\), set \(\mathrm{restGen}\, A\, V\, x = A(x)\cdot P_{V(x)}\) (with \(P_K\) the orthogonal projector onto \(K\)), \(\mathrm{sFloor}\, A\, T\, n\, x = \prod _{j{\lt}n}\left\lVert (A(T^{[j]}x))^{-1} \right\rVert ^{-1}\), and
\(\mathrm{restLog}\, A\, V\, T\) is an everywhere subadditive cocycle: for all \(m,n,x\), \(\mathrm{restLog}\, (m+n)\, x \le \mathrm{restLog}\, m\, x + \mathrm{restLog}\, n\, (T^{[m]}x)\).
The floor is multiplicative, \(\mathrm{sFloor}\, (m+n) = \mathrm{sFloor}\, m \cdot (\mathrm{sFloor}\, n)\circ T^{[m]}\), the norm of the restricted product is submultiplicative, and \(\max (ab, cd) \le \max (a,c)\max (b,d)\) for nonnegatives; taking \(\log \) (monotone) gives subadditivity with no exceptional set. The floor is the only mechanism that keeps the everywhere signature Kingman requires; on the good set it is dominated and disappears.
Kingman applied to \(\mathrm{restLog}\) over \(T\) yields a constant \(\chi _V\); the orbit-reversed cocycle \(h_n(x) = \mathrm{restLog}_n(T^{-n}x)\) is subadditive over \(T^{-1}\) with the same integral means, hence converges a.e. to the same \(\chi _V\).
Over \(T\), lemma 7.11 together with integrability of the endpoints gives a Kingman constant \(\chi _V\). The reversed family \(h_n = \mathrm{restLog}_n\circ T^{-n}\) is subadditive over \(T^{-1}\) by an index juggle through the additive law, and \(\int h_n = \int \mathrm{restLog}_n\) by measure-preservation of \(T^{-n}\). Since \(T^{-1}\) is ergodic, proposition 7.9 forces the two Kingman constants — both being the common limit of the identical integral means — to coincide.
For the forward level \(V_i\), the restricted Kingman constant equals the \(i\)-th exponent: \(\chi _{V_i} = \mathrm{expEnum}\, \mathrm{lam0}\, d\, i\).
Lower bound \(\ge \): on the good set, for \(v \in V_i x\) the restricted cocycle equals \(A^{(n)}(x)v\); a stratum witness from strictness of the filtration realizes the rate \(\lambda _i\). Upper bound \(\le \): pointwise, expand any \(P_{V_i(y)}w\) in a classical orthonormal basis of \(V_i(y)\); then \(\left\lVert A^{(n)}P w \right\rVert \le \sum _j \left\lVert A^{(n)}e_j \right\rVert \) with each \(e_j\) in a stratum of index \(\ge i\), so its growth is \(\le \lambda _i\); the log-of-a-finite-sum lemma passes the maximum through. Both bounds match the a.e.-constant Kingman limit.
For a.e. \(x\),
This is the analytic heart. By lemma 7.12 the reversed restricted log converges a.e. to the same constant \(\chi _{V_i}\), which proposition 7.13 identifies as \(\lambda _i\). On the good set the floor is absorbed, so the \(\limsup \) of the genuine restricted norm along the backward orbit is bounded by \(\lambda _i\). Only the \(\le \) direction is consumed downstream.
7.5 The transversality crux
The envelope feeds the central nonnegativity fact: a vector cannot decay backward strictly faster than \(-\lambda _i\) while lying in \(V_i\). The crux is pointwise — ergodicity is not used here — and directly kills nonzero intersection vectors of opposite-side sublevels.
Fix \(x\). If the forward envelope for \(V_x\) holds at rate \(a\), \(U_x\) decays backward at rate \(\le b\), and \(a + b {\lt} 0\), then \(V_x \sqcap U_x = \bot \).
Suppose \(0 \neq v \in V_x \sqcap U_x\). Put \(v_n = B^{(n)}(x)v\); by lemma 7.3 \(v = A^{(n)}(T^{-n}x)\, v_n\) and, by forward equivariance along the backward orbit, \(v_n \in V_i(T^{-n}x)\). Hence \(\log \left\lVert v \right\rVert \le \mathrm{restLog}\text{-envelope}_n(x) + \log \left\lVert v_n \right\rVert \), whose right side behaves like \(n(a + b + 2\varepsilon )\), tending to \(-\infty \). This contradicts \(\left\lVert v \right\rVert \) being a positive constant.
For a.e. \(x\), for every forward level \(i\) and backward level \(s\) with \(\mathrm{expEnum}\, \mathrm{lam0}\, d\, i + \mathrm{expEnum}\, \mathrm{mu0}\, d\, s {\lt} 0\),
Bundle all the a.e. facts — the forward envelope (one application of proposition 7.14 per forward level), the backward growth (flag descent in \(W\)) and equivariance along the orbit — onto a single biinvariant conull set via lemma 7.5. On it, every pair \((i,s)\) with negative exponent sum satisfies the hypotheses of proposition 7.15, so the intersection is \(\bot \). The quantifiers over the finite \(\mathrm{Fin}\, k \times \mathrm{Fin}\, l\) are discharged simultaneously.
For all \(a, b \in \mathbb {R}\) with \(a + b {\lt} 0\),
Convert thresholds to filtration levels and apply proposition 7.16 at one good point: the two sublevel spaces meet in \(\bot \), so by the Grassmann formula their dimensions sum to at most \(\dim \mathbb {R}^d = d\). The dimension formula of proposition 7.6 (forward and backward) turns the dimensions into the stated counts. The bound is deterministic, so it holds outright.
7.6 Spectral reflection
The backward spectrum must be aligned to the forward one. The determinant identity \(\sum _j \mathrm{lam0}\, j = \int \log \left\lvert \det A \right\rvert \) — and its backward negation — together with the counting bound pin the backward exponents to the negated, reversed forward ones, by a purely combinatorial multiset argument that avoids any exterior-power calculus for \(\left\lVert \textstyle \bigwedge ^q M^{-1} \right\rVert \).
Any exponent sequence \(\mathrm{lam0}\) realizing the a.e. singular-value limits satisfies \(\sum _{j{\lt}d}\mathrm{lam0}\, j = \int _X \log \left\lvert \det A(x) \right\rvert \, d\mu \).
By uniqueness of a.e. limits at a common conull point, \(\mathrm{lam0}\, j\) equals the chosen spectrum \(\mathrm{exponents}\, j\) for each \(j {\lt} d\); the sum of those is the integral of \(\log \left\lvert \det A \right\rvert = \log \prod _j \sigma _j\) via the established singular-value/determinant identity.
For a backward exponent sequence \(\mathrm{mu0}\), \(\sum _{j{\lt}d}\mathrm{mu0}\, j = -\sum _{j{\lt}d}\mathrm{lam0}\, j\).
Apply proposition 7.18 to the backward system (legitimate by proposition 7.4): \(\sum \mathrm{mu0}\, j = \int \log \left\lvert \det B \right\rvert \). The pointwise identity \(\log \left\lvert \det B \right\rvert = -\log \left\lvert \det (A\circ T^{-1}) \right\rvert \) and the change of variables along the measure-preserving \(T^{-1}\) give \(\int \log \left\lvert \det B \right\rvert = -\int \log \left\lvert \det A \right\rvert = -\sum \mathrm{lam0}\, j\).
Let \(p, q : \mathbb {N}\to \mathbb {R}\) be antitone on \([0,d)\). If \(\# \{ p \le a\} + \# \{ q \le b\} \le d\) whenever \(a + b {\lt} 0\), and \(\sum _{j{\lt}d} q\, j = -\sum _{j{\lt}d} p\, j\), then \(q\, j = -p\, (d-1-j)\) for all \(j {\lt} d\).
Apply the counting bound at \(b\) and \(a = -q(j) - \varepsilon \): since antitone tuples are their own sorted enumerations, this gives the sorted domination \(q\, j \ge -p\, (d-1-j)\) for each \(j\). A pointwise \(\ge \) whose total sum is an equality forces pointwise equality, so \(q\, j = -p\, (d-1-j)\). This is pure finite combinatorics with no analytic content.
Under the reflection \(\mathrm{mu0}\, j = -\mathrm{lam0}\, (d-1-j)\), the backward count of distinct exponents equals the forward one, and the index \(\mathrm{sidx}\, i = \mathrm{cast}\, (\mathrm{Fin.rev}\, i)\) satisfies \(\mathrm{expEnum}\, \mathrm{mu0}\, d\, (\mathrm{sidx}\, i) = -\mathrm{expEnum}\, \mathrm{lam0}\, d\, i\).
From proposition 7.20 the multisets of distinct values agree up to negation and reversal, so \(\mathrm{numExp}\, \mathrm{mu0}\, d = \mathrm{numExp}\, \mathrm{lam0}\, d\) and the enumerations satisfy \(\mathrm{expEnum}\, \mathrm{mu0}\, d\, a = -\mathrm{expEnum}\, \mathrm{lam0}\, d\, (\mathrm{Fin.rev}\, a)\). Substituting \(a = \mathrm{sidx}\, i = \mathrm{Fin.rev}\, i\) and computing the index by \(\mathrm{omega}\) gives the negated forward exponent.
7.7 Measurability of the intersection bundle
The split bundle is \(x \mapsto V_i x \sqcap W_{\mathrm{sidx}\, i}\, x\). Measurable subspaces do not close under \(\sqcap \) for free, and Mathlib has no alternating-projection theorem; instead a single von Neumann-style power lemma supplies measurability.
For subspaces \(K, L\) of \(\mathbb {R}^d\), with \(P_K, P_L\) the orthogonal projectors,
The matrix \(S = P_K P_L P_K\) is self-adjoint, PSD, and a contraction, so its eigenvalues lie in \([0,1]\); by lemma 7.23 its \(1\)-eigenspace is exactly \(K \sqcap L\). Diagonalizing by the spectral theorem, \(c^n \to 1\) if \(c = 1\) and \(\to 0\) otherwise, so \(S^n\) converges to the orthogonal projection onto the \(1\)-eigenspace, namely \(P_{K\sqcap L}\).
\((P_K\, P_L\, P_K)\, v = v\) if and only if \(v \in K \sqcap L\).
The "if" direction is immediate since both projectors fix vectors in \(K \sqcap L\). For "only if", \(\langle Sv, v\rangle = \left\lVert P_L P_K v \right\rVert ^2\); the Cauchy–Schwarz equality chain \(\left\lVert v \right\rVert ^2 = \langle Sv, v\rangle \le \left\lVert v \right\rVert ^2\) forces \(v \in K\) and \(P_K v \in L\), whence \(v \in K \sqcap L\).
If \(x \mapsto V(x)\) and \(x \mapsto W(x)\) are measurable subspace families, then so is \(x \mapsto V(x) \sqcap W(x)\).
Each \(x \mapsto (P_{V(x)} P_{W(x)} P_{V(x)})^{n}\) is measurable (matrix powers of measurable matrices). By proposition 7.22 these converge pointwise to \(P_{V(x)\sqcap W(x)}\), so the limiting projector is measurable entrywise as a limit of measurable functions; this exhibits the intersection family as measurable.
7.8 Assembling the splitting
With the aligned reflection, the crux disjointness, and the dimension formulas in hand, the splitting is assembled by intersecting each forward level with the matching backward level and telescoping a flag into a direct sum.
A descending flag \(V_0 \supseteq \cdots \supseteq V_k = \bot \) in a modular lattice, with complements \(E_i\) satisfying \(V_i = E_i \sqcup V_{i+1}\) and \(E_i \sqcap V_{i+1} = \bot \), telescopes into an independent family \((E_i)\) with \(\bigsqcup _i E_i = V_0\).
Induct on \(k\). The cons step shows that prepending a head \(E_0\) disjoint from the supremum of an already-independent tail preserves independence, using modularity to peel \(E_0\) off the join \(E_0 \sqcup C\) intersected with the tail bound. The supremum identity unfolds \(\bigsqcup _{i} E_i = E_0 \sqcup \bigsqcup _i E_{i+1} = E_0 \sqcup V_1 = V_0\) via the first telescoping identity.
Define \(E_i = V_i \sqcap W_{\mathrm{sidx}\, i}\). Then \(\mathrm{finrank}\, E_i \ge 1\), the telescoping identities \(V_i = E_i \sqcup V_{i+1}\) and \(E_i \sqcap V_{i+1} = \bot \) hold, and consequently \((E_i)\) is independent with \(\bigsqcup _i E_i = V_0 = \top \).
The crux proposition 7.16 at the negated-exponent pair gives \(V_{i+1} \sqcap W_{\mathrm{sidx}\, i} = \bot \), so by Grassmann \(V_{i+1} \sqcup W_{\mathrm{sidx}\, i} = \top \), and the reflection corollary 7.21 fixes \(\mathrm{finrank}\, W_{\mathrm{sidx}\, i} = d - \# \{ \mathrm{lam0} {\lt} \lambda _i\} \). Combining with the dimension formula of proposition 7.6 yields \(\mathrm{finrank}\, E_i = \# \{ \mathrm{lam0} \le \lambda _i\} - \# \{ \mathrm{lam0} {\lt} \lambda _i\} \ge 1\), the telescoping totality \(V_i = E_i \sqcup V_{i+1}\) by equal finrank, and disjointness from a second crux instance. lemma 7.25 then telescopes to independence and total supremum.
Let \(T : X \simeq _m X\) be an invertible ergodic measure-preserving transformation of a probability space, and let \(A : X \to \mathrm{Matrix}\, (\mathrm{Fin}\, d)\, (\mathrm{Fin}\, d)\, \mathbb {R}\) be measurable with \(\det A(x) \neq 0\) for all \(x\) and \(\log ^+\left\lVert A \right\rVert , \log ^+\left\lVert A^{-1} \right\rVert \in L^1(\mu )\). Then there exist \(k \in \mathbb {N}\), a strictly decreasing \(\lambda : \mathrm{Fin}\, k \to \mathbb {R}\), and measurable subspace families \(E : \mathrm{Fin}\, k \to X \to \mathrm{Submodule}\, \mathbb {R}\, (\mathbb {R}^d)\) such that for \(\mu \)-a.e. \(x\):
\(\mathbb {R}^d = \bigoplus _{i} E_i(x)\) is an internal direct sum with every \(E_i(x) \neq \bot \);
each \(E_i\) is \(A\)-equivariant: \(\bigl(A(x)\bigr)\bigl(E_i(x)\bigr) = E_i(Tx)\);
for every nonzero \(v \in E_i(x)\),
\[ \tfrac {1}{n}\log \bigl\lVert A^{(n)}(x)\, v \bigr\rVert \to \lambda _i \qquad \text{and}\qquad \tfrac {1}{n}\log \bigl\lVert \bigl(A^{(n)}(T^{-n}x)\bigr)^{-1}\, v \bigr\rVert \to -\lambda _i. \]
For \(d = 0\) take \(k = 0\) (the empty internal sum of the zero module). For \(d {\gt} 0\), apply proposition 7.6 forward to obtain \(\mathrm{lam0}, V\) and, via proposition 7.4, to the backward system \((T^{-1}, B)\) to obtain \(\mathrm{mu0}, W\), each with its dimension formula. Run the crux proposition 7.16 and counting bound corollary 7.17; combine with proposition 7.19 through proposition 7.20 to get the reflection \(\mathrm{mu0}\, j = -\mathrm{lam0}\, (d-1-j)\), hence \(l = k\) and the index alignment corollary 7.21. Set \(\lambda = \mathrm{expEnum}\, \mathrm{lam0}\, d\) and \(E_i(x) = V_i x \sqcap W_{\mathrm{sidx}\, i}\, x\); measurability is proposition 7.24. On a conull set, proposition 7.26 provides the internal direct sum and nonzeroness. Equivariance is \(\mathrm{Submodule.map}\) over \(\sqcap \) (injective \(A(x)\)): the forward factor is the one-sided equivariance, and the backward factor is transported through \(\mathrm{backwardGen}\, A\, T\, (Tx) = (A(x))^{-1}\) by lemma 7.3. For growth, a nonzero \(v \in E_i(x)\) lies in the \(i\)-th forward stratum and the \(\mathrm{rev}\, i\)-th backward stratum (two crux instances exclude deeper levels), so the two one-sided growth limits apply; the backward limit is rewritten as \(-\lambda _i\) through lemma 7.3 and corollary 7.21.