13 Smooth maps and worked examples
The multiplicative ergodic theorem of Chapter 5 is a statement about abstract measurable matrix cocycles. This chapter connects it to the setting it was invented for — smooth dynamics — and then instantiates the whole chain on classical worked examples.
The bridge is the derivative (tangent) cocycle: for a differentiable self-map \(T\) of \(E = \mathbb {R}^d\) (formalized as \(\operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\)), the chain rule makes the family of Jacobian matrices \(x\mapsto D_xT\) a linear cocycle over \(T\), so the Oseledets theorem applies verbatim and produces the Lyapunov exponents of the smooth system. On top of the bridge we prove the expanding-map results: every Lyapunov exponent of a uniformly expanding map is at least \(\log K {\gt} 0\), and consequently the sum of the positive exponents \(\sum \lambda ^{+}\) (the Pesin / Margulis–Ruelle right-hand side) collapses onto the full exponent sum and hence, by the trace–determinant identity, onto \(\int \log \left\lvert \det D_xT \right\rvert \, d\mu \) (the Rokhlin right-hand side). This is the honest, foliation-free expanding-case identity of the two right-hand sides — no stable foliation, no SRB-density machinery, and not a claim of the full Pesin entropy formula. The entropy-side companion, Rokhlin’s formula \(h_\mu (T,\xi ) = \int \log \left\lvert \det D_xT \right\rvert \, d\mu \), is proved via a conditional-expectation / change-of-variables argument (Coudène), and the two are chained into an expanding-map Pesin formula — a correct implication whose hypothesis bundle is disclosed to be vacuous on the non-compact space \(\mathbb {R}^d\), the genuinely instantiated equality living on the compact circle.
The worked examples then exercise every layer. The doubling map \(y\mapsto 2y\) on the unit circle has top exponent \(\log 2\), positive-exponent sum \(\log 2\), a per-partition Margulis–Ruelle bound at exactly that rate, and — the highlight — the genuinely instantiated Rokhlin equality \(h(\alpha ,T) = \int \log \left\lvert \det DT \right\rvert \, d\mu = \log 2\) for the binary partition. The Arnold cat map, the hyperbolic automorphism of \(\mathbb {T}^2\) induced by the matrix
is formalized as genuine toral dynamics: it is measure-preserving and ergodic for Haar measure (a Fourier-analytic proof on the multivariate character basis), its Lyapunov spectrum is \(\log \bigl((3\pm \sqrt5)/2\bigr)\), and the derivative cocycle of its linear lift to the universal cover has strictly positive top exponent — the formalized hyperbolicity of the cat map. Everything in this chapter is sorry-free.
13.1 The derivative cocycle of a smooth self-map
For a self-map \(T\) of \(E = \operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\), the derivative cocycle generator is the matrix-valued map
the matrix representing the Fréchet derivative \(D_xT = \operatorname {fderiv}\, \mathbb {R}\, T\, x\), transported along the star-algebra equivalence between \(d\times d\) real matrices and continuous linear endomorphisms of \(E\). Since that equivalence is an \(L^2\)-operator-norm isometry, the generator has the same norm as \(D_xT\). Feeding it to the iterated cocycle construction of Definition 2.2 yields the tangent cocycle of the smooth system.
For a differentiable \(T\), the \(n\)-th cocycle iterate of the derivative generator represents the derivative of the \(n\)-th iterate of the map:
Induction on \(n\). The base case is \(D(\operatorname {id}) = \operatorname {id}\). For the step, peel the innermost factor \(T\) simultaneously from the cocycle recursion \(A^{(n+1)}(x) = A^{(n)}(Tx)\cdot A(x)\) and from the iterate \(T^{[n+1]} = T^{[n]}\circ T\); the chain rule \(D_x(T^{[n]}\circ T) = D_{Tx}(T^{[n]})\circ D_xT\) (differentiability of \(T\) gives differentiability of all iterates) matches the two factorizations, and the star-algebra equivalence turns the matrix product into the composition.
Let \(\mu \) be a probability measure on \(E = \operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\) and let \(T\) be ergodic for \(\mu \), differentiable, with everywhere nonvanishing Jacobian determinant \(\det (\operatorname {derivativeCocycle}\, T\, x)\ne 0\) and with the log-integrability \(\log ^{+}\left\lVert D_xT \right\rVert ,\ \log ^{+}\bigl\lVert (D_xT)^{-1} \bigr\rVert \in L^1(\mu )\) (stated for the matrix generator and its matrix inverse; by the isometry these are exactly the \(\operatorname {fderiv}\) conditions). Then:
for every \(n\) and \(x\), the cocycle iterate represents \(D_x(T^{[n]})\) — the cocycle is the genuine tangent cocycle; and
there exist \(k\le d\), strictly decreasing exponents \(\lambda _1 {\gt} \dots {\gt} \lambda _k\), and a measurable family of subspaces \(E = V_0(x) \supsetneq V_1(x) \supsetneq \dots \supsetneq V_k(x) = 0\), a.e. equivariant under \(D_xT\), such that for every \(v\in V_{i-1}(x)\setminus V_i(x)\),
\[ \frac1n\, \log \bigl\lVert D_x\bigl(T^{[n]}\bigr)v \bigr\rVert \; \longrightarrow \; \lambda _i . \]
The first conjunct is Theorem 13.2. The second is the one-sided Oseledets theorem (Theorem 5.30) applied to the generator \(A = \operatorname {derivativeCocycle}\, T\), whose measurability is proved entrywise: each entry is a (continuous) coordinate projection of \(x\mapsto (D_xT)e_j\), measurable by Mathlib’s measurability of the Fréchet derivative in the base point.
13.2 Uniformly expanding maps: the foliation-free right-hand-side identity
A differentiable map \(T\) is uniformly expanding with constant \(K {\gt} 1\) when \(K\left\lVert v \right\rVert \le \left\lVert D_xT\, v \right\rVert \) for every base point \(x\) and tangent vector \(v\). The results of this section are stated exactly as the module discloses them: they establish the all-positive-spectrum collapse of \(\sum \lambda ^{+}\) onto \(\int \log \left\lvert \det D_xT \right\rvert \, d\mu \) — the honest, foliation-free expanding-case identity of the Pesin and Rokhlin right-hand sides — and no more.
If \(T\) is differentiable and uniformly expanding with constant \(K {\gt} 1\), then the derivative of the \(n\)-th iterate stretches every vector by at least \(K^n\):
Induction on \(n\), using the chain rule \(D_x(T^{[n+1]}) = D_{Tx}(T^{[n]})\circ D_xT\) to peel off one expanding factor at each step: \(K^{n+1}\left\lVert v \right\rVert = K^n(K\left\lVert v \right\rVert ) \le K^n\left\lVert D_xT\, v \right\rVert \le \left\lVert D_{Tx}(T^{[n]})(D_xT\, v) \right\rVert \).
Under the same hypotheses, every singular value of the cocycle iterate \(A^{(n)}(x) = \operatorname {cocycle}(\operatorname {derivativeCocycle} T)\, T\, n\, x\) is at least \(K^n\): \(\ K^n\le \sigma _i\bigl(A^{(n)}(x)\bigr)\) for every \(i {\lt} d\).
By Theorem 13.2 the iterate acts as \(D_x(T^{[n]})\), so Lemma 13.4 gives the uniform stretching \(K^n\left\lVert v \right\rVert \le \left\lVert f v \right\rVert \) for \(f = A^{(n)}(x)\). A uniform lower stretching bound passes to every singular value: evaluate \(f\) on the unit-norm right singular vector \(u_i\) (an eigenvector of \(f^{*}f\)), where \(\sigma _i(f) = \left\lVert f u_i \right\rVert \ge K^n\left\lVert u_i \right\rVert = K^n\).
For an ergodic, log-integrable, differentiable uniformly expanding map with constant \(K {\gt} 1\) (and \(d\ge 1\)), each Lyapunov exponent of the tangent cocycle satisfies \(\log K \le \lambda _i\).
Pick a base point where the per-index singular-value limit \(\frac1n\log \sigma _i(A^{(n)}(x))\to \lambda _i\) of Theorem 6.12 holds. By Lemma 13.5 each pre-limit term is at least \(\frac1n\log K^n = \log K\), and the limit inherits the lower bound.
Every Lyapunov exponent of a uniformly expanding map is strictly positive: \(0 {\lt} \log K \le \lambda _i\).
\(K {\gt} 1\) gives \(\log K {\gt} 0\); chain with Theorem 13.6.
For a uniformly expanding map the positive-part exponent sum is the full exponent sum: \(\sum \lambda ^{+} = \sum _i\lambda _i\) (with multiplicity).
By Corollary 13.7 the filter \(\{ i \mid 0 {\lt} \lambda _i\} \) is all of the index set, so the two finite sums have identical terms.
For an ergodic, log-integrable, differentiable uniformly expanding self-map \(T\), the sum of the strictly positive Lyapunov exponents — the Pesin / Margulis–Ruelle right-hand side — equals the integrated volume distortion — the Rokhlin right-hand side:
This is the honest foliation-free instance of the identity between the two right-hand sides; it is not a claim of the full Pesin entropy formula (no entropy appears in the statement).
Since all exponents are positive, \(\sum \lambda ^{+} = \sum \lambda \) (Proposition 13.8), and the trace–determinant identity (Theorem 6.20) rewrites the full sum as \(\int \log \left\lvert \det A \right\rvert \, d\mu \).
13.3 Rokhlin’s entropy formula for an expanding map
The entropy-side companion identifies the Kolmogorov–Sinai entropy itself with the determinant integral, for an absolutely continuous invariant measure. The proof is Coudène’s conditional-expectation argument: the conditional entropy of a partition given the \(\sigma \)-algebra \(T^{-1}\mathcal{A}\) is computed by a per-branch change of variables.
For a self-map \(T\) of \(\operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\) and a finite measurable partition \(\xi \), the predicate \(\texttt{IsInjectivityPartition}\, \mu \, T\, \xi \) packages the two hypotheses the conditional-expectation proof needs: \(T\) is injective on each cell of \(\xi \), and each cell is measurable. (These are literally the hypotheses of Mathlib’s change-of-variables lemma; no Markov condition and no generating condition are baked in.)
Let \(\mu \) be an invariant probability measure with \(\mu \ll \operatorname {volume}\), let \(T\) be differentiable with everywhere nonvanishing Jacobian, let \(\xi \) be an injectivity partition, and assume \(\log \rho \in L^1(\mu )\) for the density \(\rho = d\mu /d\operatorname {vol}\) and \(\log \left\lvert \det D T \right\rvert \in L^1(\mu )\). Then the conditional Shannon entropy of \(\xi \) given the pulled-back \(\sigma \)-algebra \(T^{-1}\mathcal{A}\) is
independently of the partition (no generating hypothesis).
Per cell \(\xi _i\), the change-of-variables crux (measure_cell_inter_preimage_eq_setLIntegral_transfer) recovers \(\mu (\xi _i\cap T^{-1}B)\) as the integral over \(T(\xi _i)\cap B\) of the per-branch transfer density \(\rho (g_i^{-1}y)/\left\lvert \det DT \right\rvert _{g_i^{-1}y}\), where \(g_i^{-1}\) is the branch inverse of \(T\) on \(\xi _i\). This identifies the regular-conditional kernel mass of each cell with the branch-weight candidate; the entropy integrand \(\sum _i\operatorname {negMulLog}\) of these masses pulls out, per cell, to \(\int _{\xi _i}\bigl(\log \left\lvert \det DT \right\rvert + \log \rho \circ T - \log \rho \bigr)d\mu \), the cells partition the space, and the density bracket \(\log \rho \circ T - \log \rho \) telescopes to \(0\) by \(T\)-invariance of \(\mu \), leaving the Jacobian integral.
The assembly of Theorem 13.11 into the per-partition Rokhlin formula \(h_\mu (T,\xi ) = \int \log \left\lvert \det D_xT \right\rvert \, d\mu \) for a one-sided generating injectivity partition — via the sharp-rate identity expressing \(h_\mu (T,\xi )\) as the conditional entropy of \(\xi \) against its own strict future, and the \(\sigma \)-algebra glue identifying that future with \(T^{-1}\mathcal{A}\) — is the node Theorem 10.24 of the classical-entropy chapter. Here we chain it with the expanding-case right-hand-side identity into the Pesin formula.
For an ergodic, absolutely continuous (\(\mu \ll \operatorname {volume}\)), differentiable, uniformly expanding self-map of \(\operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\) with everywhere-nonsingular derivative, log-integrable derivative data, a one-sided generating injectivity partition, and integrable \(\log \rho \) and \(\log \left\lvert \det DT \right\rvert \):
Honest disclosure: this is a correct implication whose hypothesis bundle has no model on the non-compact space \(\mathbb {R}^d\) — a globally uniformly expanding map of \(\mathbb {R}^d\) admits no ergodic absolutely continuous invariant probability measure (uniform expansion forces mass to escape to infinity; for \(T = c\cdot \operatorname {id}\) the nested preimages of a ball force an atom at the fixed point). The theorem is therefore vacuously true as stated on \(\mathbb {R}^d\), and is disclosed as such; the instantiated Pesin/Rokhlin equality lives on the compact circle (Theorem 13.18).
Compose three theorems: the Kolmogorov–Sinai generator theorem \(h_\mu (T) = h_\mu (T,\xi )\) for the generating \(\xi \), Rokhlin’s per-partition formula (Theorem 10.24), and the expanding-case right-hand-side identity (Theorem 13.9), aligning the two determinant hypotheses along the \(\operatorname {fderiv}\)-to-matrix bridge.
13.4 The doubling map
The phase space is the unit circle \(\mathbb {T} = \operatorname {UnitAddCircle}\) with its Haar probability measure (Mathlib’s default \(\operatorname {volume}\)), and the map is \(\operatorname {doublingMap}: y\mapsto 2\cdot y\) (), ergodic by Mathlib’s AddCircle.ergodic_nsmul (). Its derivative is the constant \(1\times 1\) matrix \((2)\), realized as a constant cocycle.
The constant cocycle with generator \(M = (2)\) over the ergodic doubling map has top Lyapunov exponent \(\log 2\).
For a constant cocycle with symmetric invertible generator \(M\), the sorted Lyapunov spectrum is \(\log \) of the sorted eigenvalues of \(\left\lvert M \right\rvert \) (exponents_const); for positive semidefinite \(M\) the functional calculus collapses \(\left\lvert M \right\rvert = M\). The single eigenvalue of \((2)\) is its trace \(2\), so the unique exponent is \(\log 2\).
The sum of the strictly positive Lyapunov exponents of the doubling-map cocycle is \(\log 2\), with every spectrum hypothesis (invertibility, measurability, both log-integrability conditions) discharged unconditionally from the constant-cocycle API.
The spectrum consists of the single exponent \(\log 2 {\gt} 0\), so the positive-part filter is the full (one-element) index set and the sum is that one term.
For any finite measurable partition \(P\) of the circle whose \(n\)-fold refinement \(\bigvee _{k=0}^{n-1}T^{-k}P\) under the doubling map eventually has at most \(C\cdot e^{n\log 2}\) non-empty atoms (\(C\ge 1\)),
This is the per-partition bound \(h(\alpha ,T)\le \sum \lambda ^{+}\), not the system Margulis–Ruelle inequality; the right-hand side is the computed Lyapunov datum (Corollary 13.14), not an abstract constant. The atom-count hypothesis is automatic for the binary partition, where the bound is attained (Theorem 13.17).
Specialize the abstract atom-count-growth entropy bound (the arithmetic backbone of the per-partition Ruelle inequality, cf. Theorem 10.23) to the doubling map at the exponential rate \(R = \log 2\), then identify the rate with the positive-exponent sum via Corollary 13.14.
Let \(T\) preserve a probability measure and let \(P\) be a finite partition indexed by a type of cardinality \(b\) such that for every \(n\), every cell of the \(n\)-fold join \(\bigvee _{k=0}^{n-1}T^{-k}P\) has measure exactly \(b^{-n}\). Then \(h(P,T) = \log b\).
The \(n\)-fold join is indexed by the \(b^n\) formal cell-tuples, each of measure \(b^{-n}\), so its Shannon entropy is a sum of \(b^n\) equal terms \(\operatorname {negMulLog}(b^{-n}) = b^{-n}\, n\log b\), totalling \(n\log b\). The averaged sequence \(H_n/n\) is thus eventually the constant \(\log b\), and it converges to \(h(P,T)\); the two limits agree.
For the binary partition \(\alpha = \{ [0,\tfrac 12), [\tfrac 12,1)\} \) of the circle (), the partition-relative Kolmogorov–Sinai entropy under the doubling map is exactly \(\log 2\).
The dynamical crux (volume_binJoinCell) shows every cell of the \(n\)-fold join is a dyadic arc of measure exactly \(2^{-n}\): the doubling map restricted to a half-arc is the affine two-fold magnification onto the whole circle, so \(\operatorname {vol}(\alpha _i\cap T^{-1}B) = \operatorname {vol}(B)/2\), and induction on \(n\) halves the measure at each refinement step. Feeding this uniform-join datum into Proposition 13.16 with \(b = 2\) gives \(h(\alpha ,T) = \log 2\).
For the doubling map and the binary partition,
the genuinely instantiated Pesin/Rokhlin equality on a real expanding system (in contrast to the vacuous-on-\(\mathbb {R}^d\) assembly Theorem 13.12). The integrand is the honest log-Jacobian: the generator \((2)\) is proved to be the Fréchet derivative of the doubling map’s linear lift \(x\mapsto 2x\) to the universal cover (), and the covering projection \(\mathbb {R}\to \mathbb {T}\) intertwines that lift with the doubling map () — so \((2)\) genuinely is \(DT\), not an arbitrary constant of the right determinant.
The entropy side is Theorem 13.17. For the integral side, \(\det (2) = 2\), so the integrand is the constant \(\log 2\), which integrates against the probability measure to \(\log 2\). Both sides equal \(\log 2\).
13.5 The Arnold cat map
The Arnold cat map is the automorphism of the \(2\)-torus \(\mathbb {T}^2 = \operatorname {UnitAddTorus}(\operatorname {Fin}2)\) induced by the unimodular hyperbolic matrix \(M\in \mathrm{SL}_2(\mathbb {Z})\) displayed in the chapter introduction. Its eigenvalues are \(\lambda _{\pm } = (3\pm \sqrt5)/2\), with \(\lambda _+ {\gt} 1 {\gt} \lambda _- {\gt} 0\) and \(\lambda _+\lambda _- = 1\). We first read off the Lyapunov spectrum of the matrix (as a constant cocycle), then formalize the genuine toral dynamics, and finally combine them.
Realized as a constant cocycle with generator the cat-map matrix \(M\) over an ergodic base (here the doubling map — the spectrum depends only on \(M\)), the two Lyapunov exponents are
Honesty caveat (as in the Lean docstring): the cocycle here is the constant matrix, not the derivative cocycle of the genuine toral automorphism; the genuine dynamics is treated below.
\(M\) is symmetric positive definite with trace \(3\) and determinant \(1\), so its sorted eigenvalues \(a\ge b\) satisfy \(a + b = 3\), \(ab = 1\), whence \((a-b)^2 = 9 - 4 = 5\) and \(a,b = (3\pm \sqrt5)/2\). The constant-cocycle spectrum theorem (exponents_const) evaluates the sorted exponents to \(\log \) of the sorted eigenvalues of \(\left\lvert M \right\rvert = M\).
\(\lambda _1 + \lambda _2 = 0\): the cocycle is conservative (\(\det M = 1\)).
\(\log \lambda _+ + \log \lambda _- = \log (\lambda _+\lambda _-) = \log 1 = 0\), computing \(\lambda _+\lambda _- = \bigl(9 - (\sqrt5)^2\bigr)/4 = 1\).
The map \(\operatorname {catTorus}:\mathbb {T}^2\to \mathbb {T}^2\), \((\operatorname {catTorus} y)_i = \sum _j M_{ij}\cdot y_j\), with the integer cat-map matrix \(M\) acting by integer scalar multiplication on each circle coordinate. Since \(\det M = 1\), the integer matrix \(M^{-1}\) (with rows \((1,-1)\) and \((-1,2)\)) induces a two-sided inverse, so \(\operatorname {catTorus}\) is a continuous additive automorphism of the compact group \(\mathbb {T}^2\). Throughout this section \(\mathbb {T}^2\) carries the product Haar probability measure (the normalization for which Mathlib’s multivariate Fourier basis is stated).
\(\operatorname {catTorus}\) preserves the Haar probability measure on \(\mathbb {T}^2\).
\(\operatorname {catTorus}\) is a continuous surjective additive homomorphism of a compact group; the pushforward of Haar measure under such a map is again a translation-invariant probability measure, hence equals Haar (Mathlib’s \(\texttt{AddMonoidHom.measurePreserving}\), with equal total mass \(1\)).
\(\operatorname {catTorus}\) is ergodic for the Haar probability measure on \(\mathbb {T}^2\).
The classical Fourier / character argument. The Koopman operator permutes the multivariate characters: \(\texttt{mFourier}\, n\circ \operatorname {catTorus} = \texttt{mFourier}(M^{\top }n)\), and since \(M\) is symmetric the index action is \(n\mapsto M n\). For a measurable invariant set \(s\), the indicator \(\mathbf1_s\in L^2\) has Fourier coefficients constant along each index orbit \(p\mapsto M^{p}n\). The hyperbolicity input is that this orbit is infinite for every \(n\ne 0\) (orbit_infinite: pairing with the two eigen-covectors of \(M\), a period would force \(\varphi (n)\lambda _+^{k} = \varphi (n)\) and \(\psi (n)\lambda _+^{-k} = \psi (n)\) with \(\lambda _+^k\ne 1\), so \(n = 0\)). A square-summable sequence constant on an infinite set vanishes there, so all nonzero-index coefficients of \(\mathbf1_s\) are \(0\); the Fourier series collapses to the constant term, \(\mathbf1_s\) is a.e. constant, and \(s\) is a.e. empty or full.
Realized as a constant cocycle with generator \(M\) over the genuine ergodic Arnold cat map \(\operatorname {catTorus}\), the two Lyapunov exponents are \(\log \bigl((3+\sqrt5)/2\bigr)\) and \(\log \bigl((3-\sqrt5)/2\bigr)\) — the same spectrum as Theorem 13.19, now over the hyperbolic toral automorphism itself rather than a surrogate base.
The constant-cocycle spectrum theorem applies over any ergodic base; instantiate it over \(\operatorname {catTorus}\) (Theorem 13.23) and evaluate the sorted eigenvalues of \(\left\lvert M \right\rvert = M\) by the closed form computed for Theorem 13.19.
Let \(\operatorname {catLift}:\mathbb {R}^2\to \mathbb {R}^2\) () be the linear lift of the cat map to the universal cover — the continuous linear map with matrix \(M\), which genuinely lifts \(\operatorname {catTorus}\): the covering projection \(\mathbb {R}^2\to \mathbb {T}^2\) satisfies \(\pi \circ \operatorname {catLift} = \operatorname {catTorus}\circ \pi \) (). Its derivative cocycle in the sense of Definition 13.1 is the constant matrix \(M\) at every point (), and the top Lyapunov exponent of this genuine derivative cocycle, over the genuine ergodic base \(\operatorname {catTorus}\), is
the formalized hyperbolicity of the Arnold cat map. (Reading the derivative on the torus manifold itself via \(\texttt{mfderiv}\) is a documented gap: Mathlib has no manifold-derivative API for \(\texttt{AddCircle}\) endomorphisms; the lift and the map share the same derivative everywhere because the covering projection is a local diffeomorphism with identity derivative.)
The Fréchet derivative of a continuous linear map is the map itself, so \(\operatorname {derivativeCocycle}\, \operatorname {catLift}\) is the constant \(M\); transporting along this equality, the top exponent is the constant-cocycle top exponent \(\log \bigl((3+\sqrt5)/2\bigr)\) of Theorem 13.24, positive because \((3+\sqrt5)/2 {\gt} 1\).
For any finite measurable partition \(P\) of \(\mathbb {T}^2\) whose \(n\)-fold refinement under \(\operatorname {catTorus}\) eventually has at most \(C\cdot e^{\, n\log \lambda _+}\) non-empty atoms (\(C\ge 1\), \(\lambda _+ = (3+\sqrt5)/2\)),
As in the doubling-map case this is the per-partition bound, not the system inequality; the rate \(\log \lambda _+\) is the genuine top Lyapunov exponent of the cat map (Theorem 13.25), and the atom-count growth is the honest named geometric input. The sharp system-level equality \(h_\mu = \log \lambda _+\) is a documented wall (it needs an Adler–Weiss Markov generating partition for the upper bound and Pesin/Ledrappier–Young machinery for the lower bound).
A thin specialization of the abstract atom-count-growth entropy bound (the arithmetic backbone of the per-partition Ruelle inequality, cf. Theorem 10.23) over the measure-preserving base \(\operatorname {catTorus}\) (Proposition 13.22) at the rate \(R = \log \bigl((3+\sqrt5)/2\bigr)\).
13.5.1 Strong mixing
Ergodicity (Theorem 13.23) says the Fourier coefficients of an invariant indicator are constant along the infinite index orbits; strong mixing is the sharper spectral statement that all correlations decay to the product of the means. The cat map is the library’s first smooth mixing example, and the proof is the same character machinery pushed one step further: exact decorrelation on characters, promoted to arbitrary \(L^2\) observables by density of their span.
Let \(U_k v = v\circ \operatorname {catTorus}^{[k]}\) be the Koopman operator (an \(L^2\)-isometry, ) and \(\Phi _k(u,v) = \langle u, U_k v\rangle \) the correlation (). For every \(u,v\in L^2(\mathbb {T}^2)\),
the orthogonal projection onto the constants.
The Koopman operator sends the character \(\texttt{mFourier}\, n\) to \(\texttt{mFourier}(M^{k}n)\) (). By hyperbolicity the index \(M^{k}b\) eventually escapes any fixed value for \(b\ne 0\) (), so orthonormality of the characters () makes the character correlation \(\Phi _k(\texttt{mFourier}\, a,\texttt{mFourier}\, b)\) eventually zero whenever \(b\ne 0\), matching the product of the means (which also vanishes there). A finite-span approximation of arbitrary \(u,v\in L^2\) (density of the character span, ) together with the Cauchy–Schwarz bound \(\left\lvert \Phi _k(u,v) \right\rvert \le \left\lVert u \right\rVert \, \left\lVert v \right\rVert \) promotes the exact character result to the limit for all \(L^2\) pairs.
For arbitrary measurable sets \(A,B\subseteq \mathbb {T}^2\),
i.e. \(\operatorname {catTorus}\) is strongly mixing for the Haar probability measure.
Feed the indicator functions \(u = \mathbf1_A\) and \(v = \mathbf1_B\) to Theorem 13.27: the means are \(\int \overline{\mathbf1_A} = \operatorname {vol}(A)\) and \(\int \mathbf1_B = \operatorname {vol}(B)\), and the correlation \(\Phi _k(\mathbf1_A,\mathbf1_B)\) is exactly \(\operatorname {vol}(A\cap \operatorname {catTorus}^{[k]\, -1}B)\) by measure preservation (Proposition 13.22). Taking real parts of the complex limit gives the set-level statement.
A reusable spectral interface: for a strongly mixing measure-preserving map on a probability space, any measurable eigenfunction \(g\) with \(g\circ f = l\cdot g\), \(\left\lvert l \right\rvert = 1\), \(l\ne 1\), vanishes a.e.
If \(g\) were not a.e. zero, the eigen-equation \(g\circ f^{[n]} = l^{n} g\) forces the correlation of a positive-measure sublevel set \(A = g^{-1}(\text{small ball})\) with itself to oscillate — a frequently far-from-\(1\) power \(l^{n}\) keeps \(\operatorname {vol}(A\cap f^{[n]\, -1}A)\) bounded away from \(\operatorname {vol}(A)^2\), contradicting mixing.
A measurable \(g:\mathbb {T}^2\to \mathbb C\) with \(g(\operatorname {catTorus} x) = l\cdot g(x)\), \(\left\lvert l \right\rvert = 1\), \(l\ne 1\), vanishes a.e. — re-deriving Theorem 13.31 through the mixing interface rather than the direct Fourier argument.
Discharge Lemma 13.29 with the strong mixing of the cat map (Theorem 13.28) as the correlation-decay hypothesis.
13.5.2 Eigenfunction rigidity and the ergodic time-one cat suspension
The cat map has no nontrivial measurable eigenfunctions with unimodular eigenvalue \(\ne 1\); this Fourier rigidity is exactly the spectral hypothesis of the abstract time-one ergodicity theorem (Theorem 9.31), so it upgrades the cat map to an ergodic time-one suspension in the same way the Bernoulli shift does (Theorem 9.32).
A measurable \(g : \mathbb {T}^2 \to \mathbb {C}\) with \(g(\operatorname {catTorus} x) = l\cdot g(x)\) for all \(x\), where \(\left\lVert l \right\rVert = 1\) and \(l \ne 1\), vanishes almost everywhere.
Since \(\left\lVert l \right\rVert = 1\), the modulus \(\left\lVert g \right\rVert \) is \(\operatorname {catTorus}\)-invariant, hence a.e. constant by ergodicity (Theorem 13.23); so \(g \in L^2\). The eigen-equation transports the multivariate Fourier coefficients \(\texttt{mFourier}\, n\) of \(g\) along the infinite \(\operatorname {catTorus}\)-orbit of indices with the unimodular weight \(l\); Parseval forces every nonzero mode to vanish, and \(l \ne 1\) kills the constant mode. (Einsiedler–Ward, Ergodic Theory with a View towards Number Theory, §2.4.)
For the Arnold cat map with Haar \(\operatorname {volume}\) on \(\mathbb {T}^2\) and any positive irrational roof \(r\), the time-\(1\) map of the constant-roof suspension flow is ergodic for the invariant suspension probability measure.
Discharge the abstract Theorem 9.31 with base ergodicity (Theorem 13.23) and the no-nontrivial-eigenfunctions input (Theorem 13.31).
The irrational roof \(r := \sqrt2\) yields an ergodic time-\(1\) map of the cat suspension.
Instantiate Theorem 13.32 at \(r = \sqrt2\), positive and irrational.
13.6 The sharp Kolmogorov–Sinai entropy of the cat map
The per-partition Ruelle bound Theorem 13.26 gave only \(h(\alpha , \operatorname {catTorus}) \le \log \lambda _+\) for one partition. Issue #52 closes the full system entropy to the exact value
the entropy statement of the Adler–Weiss classification of ergodic toral automorphisms (R. L. Adler and B. Weiss, Entropy, a complete metric invariant for automorphisms of the torus, Proc. Nat. Acad. Sci. USA 57 (1967) 1573–1576) together with Sinai’s identification of the metric entropy of a hyperbolic automorphism with its sum of positive Lyapunov exponents. The two inequalities are proved by structurally distinct geometric mechanisms and glued by le_antisymm.
13.6.1 The lower bound: grid partition and eigencoordinate telescoping
The number of index families \(f : \operatorname {Fin} n \to \iota \) whose atom of the flat \(n\)-fold join \(\bigvee _{k{\lt}n} T^{-k}P\) (Definition 10.8) has nonzero \(\mu \)-mass. It is at most the set-nonempty atom count, yet still bounds the entropy from above (a null junk cell is not counted), giving a sharper crude Ruelle backbone.
Every atom of the \(n\)-fold forward join of the \(5 \times 5\) grid partition under \(\operatorname {catTorus}\) has \(\operatorname {volume}\) at most \((9\sqrt5/25)\cdot \lambda \cdot \mu ^n\). Two points sharing every grid cell for \(n\) steps stay \(1/5\)-close along the orbit, so a nearest-integer lift of their difference telescopes into an eigencoordinate slab \(\left\lvert \operatorname {eigCoordU} \right\rvert \le (3/10)\mu ^{n-1}\), \(\left\lvert \operatorname {eigCoordS} \right\rvert \le 3/10\); translation invariance and the projection contraction give the measure bound.
\(\log \! \big((3+\sqrt5)/2\big) \le h(\operatorname {catTorus})\).
The wall lemma Theorem 13.35 caps each atom’s measure by \(c\lambda \mu ^n\), so the positive-measure atom count Definition 13.34 of the grid join is at least \(\lambda _+^{\, n}\) up to a constant; its exponential growth rate is a lower bound for the entropy.
\(0 {\lt} h(\operatorname {catTorus})\).
13.6.2 The upper bound: the Adler–Weiss two-box generator
The golden two-box partition of \(\mathbb {T}^2\) into the projected branches of the two golden rectangles \(R_1 = [0,\varphi )\times [0,\varphi )\) and \(R_2 = [\varphi ,\varphi ^2)\times [0,1)\) (in the eigen-coordinates), a six-cell \(\operatorname {MeasurePartition}\) (five branch cells plus a junk cell).
The junk cell of Definition 13.38 is literally empty, not merely null: a four-case skew-lattice reduction shows every torus point, lifted to the unit square, lands in \(R_1 \cup R_2\) after subtracting one of the four lattice vectors \((0,0),(0,1),(-1,0),(-1,1)\). Hence the two golden rectangles tile the torus exactly.
For a measurable automorphism of a standard Borel space and a finite measurable partition \(P\), if the two-sided family of cell-preimages separates points then \(P\) is two-sided generating (Definition 10.16). The identity map from the ambient Borel structure to the coarser saturated \(\sigma \)-algebra is an injective measurable map into a countably separated space, hence a measurable embedding by Blackwell’s theorem.
\(\operatorname {catAWPartition}\) is two-sided generating for \(\operatorname {catTorus}\). Each point has a unique admissible two-sided itinerary (consecutive symbols satisfy \(\operatorname {tgt} = \operatorname {src}\), by the geometric branch-step keystone and injectivity of the covering projection on \(R_1 \cup R_2\)); two points with the same itinerary have difference propagating linearly, so the contraction estimate forces them equal. Separation then yields generation through Theorem 13.40.
\(h(\operatorname {catTorus}, \operatorname {catAWPartition}) \le \log \! \big((3+\sqrt5)/2\big)\). The positive-measure atoms of the join inject into admissible golden itineraries, whose weighted count satisfies the exact recurrence \(W(n+1) = \lambda \cdot W(n)\) via the golden weight identity \(\sum _{\operatorname {src} e' = b} w(e') = \lambda _+\, w(b)\); the atom-count backbone converts this growth rate into the entropy bound.
\(h(\operatorname {catTorus}) \le \log \! \big((3+\sqrt5)/2\big)\).
Since \(\operatorname {catAWPartition}\) is a two-sided generator (Theorem 13.41), the two-sided generator theorem (Theorem 10.17) reduces \(h(\operatorname {catTorus})\) to \(h(\operatorname {catTorus}, \operatorname {catAWPartition})\), bounded by Theorem 13.42.
13.6.3 The crown equality
\(h(\operatorname {catTorus}) = \log \! \big((3+\sqrt5)/2\big) = \log \lambda _+\). This is the exact Kolmogorov–Sinai entropy of a hyperbolic system, formalized end-to-end; we have not located a prior formalization.
le_antisymm of the Adler–Weiss generator upper bound Theorem 13.43 and the grid-slab lower bound Theorem 13.36.
13.7 Statistical laws for the cat map
The ergodicity (Theorem 13.23) and strong mixing (Theorem 13.28) of the cat map are qualitative. Issue #62 upgrades them to the quantitative statistical package of a hyperbolic system: an explicit exponential rate of decay of correlations, and the second-moment limit laws — Green–Kubo variance asymptotics and finite-sample concentration — that summable correlations entail. The observable regularity is measured not by a Hölder modulus (a purely metric \(2\)-torus Hölder coefficient decays too slowly to feed the lattice sums) but by the Fourier coefficient-decay class \(\mathcal C_s\), following the Fourier proof of exponential mixing for hyperbolic toral automorphisms (Einsiedler–Ward, Ergodic Theory with a View towards Number Theory, Ch. 2; Katok–Hasselblatt §17–18 for the Anosov decay context). Throughout \(\lambda _+ = (3+\sqrt5)/2\) is the expanding eigenvalue and \(\theta = \lambda _+^{-(s-2)/4} {\lt} 1\) the geometric rate.
13.7.1 The Fourier-decay class and the Diophantine norm form
Writing \(\langle n\rangle = \max \{ 1, \left\lvert n_0 \right\rvert , \left\lvert n_1 \right\rvert \} \) for the Japanese bracket of a frequency \(n\in \mathbb {Z}^2\) (), a function \(f:\mathbb {T}^2\to \mathbb {C}\) lies in \(\mathcal C_s = \operatorname {FourierDecay} s\) when its multivariate Fourier coefficients decay at least like \(\langle n\rangle ^{-s}\): \(\ \left\lVert \hat f(n) \right\rVert \le K\, \langle n\rangle ^{-s}\) for some constant \(K\). Every character \(\texttt{mFourier}\, m\) lies in every class (, its coefficients a Kronecker delta), and the class is closed under integrable sums and scalar multiples (), so every trigonometric polynomial belongs to it.
For \(2 {\lt} s\) the family \(n\mapsto \langle n\rangle ^{-s}\) is summable over \(\mathbb {Z}^2\), and the sum over any set of frequencies with \(\langle n\rangle \ge R\) is at most \(C_s\, R^{-(s-2)/2}\) (), with \(C_s\) the total sum of the faster-decaying family \(\langle n\rangle ^{-(s+2)/2}\). This is exactly the shape the mixing argument consumes to bound a geometric tail \(\sum _{\langle b\rangle {\gt}\lambda _+^{k/2}} K\langle b\rangle ^{-s} \le C\, \theta ^{k}\).
Split the exponent and dominate the sup norm by a product of one-dimensional factors, reducing to a one-dimensional \(p\)-series comparison (\(p = s/2 {\gt} 1\)); the tail bound isolates the radius-\(R\) cut of the same comparison.
The norm form \(Q(p,q) = p^2 - p q - q^2\) of the cat-map matrix \(A = \bigl(\begin{smallmatrix} 2 & 1 \\ 1 & 1 \end{smallmatrix}\bigr)\) is the norm form of the ring \(\mathbb {Z}[\varphi ]\) (discriminant \(5\)). It is exactly \(A\)-invariant, \(Q(A^k n) = Q(n)\) (), and — being the norm of a nonzero element of \(\mathbb {Z}[\varphi ]\) — never vanishes on a nonzero lattice vector (), hence \(\left\lvert Q(n) \right\rvert \ge 1\) there.
Factoring \(Q\) over the eigen-line coordinates \(a_{\pm }\), with \(a_+\) scaling by \(\lambda _+^k\) under \(A^k\) () and \(a_+\cdot a_- = Q\), the lower bound \(\left\lvert Q \right\rvert \ge 1\) combines with the elementary sup-norm bounds \(\left\lvert a_- \right\rvert \le \lambda _+\left\lVert \cdot \right\rVert \), \(\left\lvert a_+ \right\rvert \le (\lambda _+-1)\left\lVert \cdot \right\rVert \) into the quantitative expansion estimate: for every nonzero \(n\in \mathbb {Z}^2\) and every \(k\),
Write \(\left\lvert Q(n) \right\rvert = \left\lvert a_+(A^k n) \right\rvert \cdot \left\lvert a_-(A^k n) \right\rvert /\lambda _+^{k}\); bounding \(\left\lvert a_-(A^k n) \right\rvert \le \lambda _+\left\lVert A^k n \right\rVert \) and using \(\left\lvert Q(n) \right\rvert \ge 1\) with \(\left\lvert a_+(n) \right\rvert \le (\lambda _+-1)\left\lVert n \right\rVert \) rearranges to the stated lower bound, the constant \(\sqrt5 - 2\) coming from \(1/(\lambda _+(\lambda _+-1))\).
13.7.2 Exponential decay of correlations
For continuous \(f, g:\mathbb {T}^2\to \mathbb {C}\), Parseval turns the time-\(k\) correlation into a bilinear character sum, and the Koopman action \(\texttt{mFourier}\, n\circ \operatorname {catTorus}^{[k]} = \texttt{mFourier}(A^k n)\) shifts the index on one factor: the sum over \(b\ne 0\) of \(\overline{\hat f(A^k b)}\, \hat g(b)\) converges to the centred correlation \(\int \overline f\, (g\circ \operatorname {catTorus}^{[k]}) - (\int \overline f)(\int g)\).
Parseval’s identity for the multivariate Fourier basis expands the \(L^2\) inner product as the bilinear coefficient sum; the Koopman coefficient shift () reindexes one factor by \(A^k\), and removing the \(b = 0\) term (, \(\hat g(0) = \int g\)) subtracts exactly the product of the means.
For \(f, g\in \mathcal C_s\) (\(s {\gt} 2\)) there is a constant \(C\ge 0\) with, for every \(k\),
A real-observable corollary records \(\left\lvert \int f\, (f\circ \operatorname {catTorus}^{[k]}) - (\int f)^2 \right\rvert \le C\theta ^{k}\) (), the Green–Kubo input downstream. This is the repository’s first quantitative-rate mixing statement.
Split the centred character sum Theorem 13.49 at radius \(\langle b\rangle = \lambda _+^{k/2}\). On the near part the norm-form expansion Theorem 13.48 forces \(\langle A^k b\rangle \ge (\sqrt5 - 2)\lambda _+^{k/2}\), so the decay class caps \(\left\lVert \hat f(A^k b) \right\rVert \) by a \(\lambda _+^{-ks/4}\)-multiple; on the far part the lattice tail Lemma 13.46 contributes \(\lambda _+^{-k(s-2)/4}\). Both parts are dominated by \(C\theta ^{k}\) with \(\theta = \lambda _+^{-(s-2)/4}\).
13.7.3 Green–Kubo variance and concentration
The centred autocorrelation of a bounded real observable \(f\) is \(\rho (k) = \operatorname {cov}[f, f\circ \operatorname {catTorus}^{[k]}]\) (); Theorem 13.50 makes it geometrically summable for \(f\in \mathcal C_s\).
For \(f\in C(\mathbb {T}^2,\mathbb {R})\) with \(\mathcal C_s\)-complexification (\(s {\gt} 2\)), \(\left\lvert \rho (k) \right\rvert \le C\theta ^{k}\) with the same rate \(\theta = \lambda _+^{-(s-2)/4}\); this is the bridge identifying the probabilistic autocovariance with the centred correlation of Theorem 13.50.
The autocovariance \(\operatorname {cov}[f, f\circ \operatorname {catTorus}^{[k]}]\) equals the centred correlation \(\int f\, (f\circ \operatorname {catTorus}^{[k]}) - (\int f)^2\) by measure preservation; apply the real-observable corollary of Theorem 13.50.
For \(f\in \mathcal C_s\) the rescaled Birkhoff variance converges to the Green–Kubo variance,
together with a linear variance bound \(\operatorname {Var}(S_n)\le B\, n\) ().
A Toeplitz/Cesàro collapse expresses \(\operatorname {Var}(S_n) = 2\sum _{d{\lt}n}(n-d)\rho (d) - n\rho (0)\); geometric summability of \(\rho \) (Theorem 13.51) makes the averaged double sum converge to \(\sigma ^2\) and bounds it linearly.
For \(f\in \mathcal C_s\) there is a constant \(B\ge 0\) with, for every sample size \(n\ge 1\) and threshold \(\varepsilon {\gt} 0\),
the tier-3 headline law: the empirical average concentrates around the space mean at the Chebyshev rate.
Chebyshev’s inequality against the linear variance bound of Theorem 13.52.
Honest scope. A full dynamical central limit theorem is not claimed: Mathlib carries no martingale/Gordin CLT, so only these second-moment laws follow from summable correlations. Likewise entropy-from-orbit estimation is out of scope — it would need a Shannon–McMillan–Breiman theorem with rates. The \(\mathcal C_s\) certificates given at compile time (trigonometric polynomials) have autocorrelations that vanish exactly for large \(k\) (the dual index orbit escapes any finite frequency support); the geometric rate \(\theta ^{k}\) is proved for the full class, which does contain infinite-frequency members with genuinely \(\theta ^{k}\)-tight decay.
13.7.4 A finite-sample rate for the exponent estimator
Because the derivative cocycle of the cat map is the constant hyperbolic matrix \(\texttt{cat}_{\mathbb {R}} = \bigl(\begin{smallmatrix} 2 & 1 \\ 1 & 1 \end{smallmatrix}\bigr)\), the length-\(n\) top-exponent estimator \((1/n)\log \left\lVert \texttt{cat}_{\mathbb {R}}^{\, n} \right\rVert \) is deterministic and converges to \(\log \lambda _+\) at the explicit rate
with \(C_0 = \left\lvert \log C \right\rvert \), \(C = (\left\lVert \texttt{cat}_{\mathbb {R}} \right\rVert + \lambda _+ + 1)/\sqrt5\).
Cayley–Hamilton gives \(\texttt{cat}_{\mathbb {R}}^{\, n} = a_n\, \texttt{cat}_{\mathbb {R}} + b_n\, \mathbf1\) with coefficients \((\lambda _+^n - \mu ^n)/\sqrt5\), \(\mu = (3-\sqrt5)/2\in (0,1)\), whence the two-sided Gelfand bound \(\lambda _+^n \le \left\lVert \texttt{cat}_{\mathbb {R}}^{\, n} \right\rVert \le C\lambda _+^n\) (lower by applying to the \(\lambda _+\)-eigenvector, upper by the triangle inequality). Taking logarithms and dividing by \(n\) yields the \(C_0/n\) rate; letting \(n\to \infty \) re-derives the limit ().
13.7.5 Transport to the suspension flow
The base decay of Theorem 13.50 transports to the constant-roof cat suspension flow, subject to the fibre-rotation obstruction of a constant roof.
For base observables \(f, g\in \mathcal C_s\) with \(g\) centred (\(\int g = 0\)) and bounded measurable fibre profiles \(\psi , \chi \), the centred flow correlation of the fibre-product observables \(F[x,s] = f(x)\psi (s)\), \(G[x,s] = g(x)\chi (s)\) on the constant-unit-roof cat suspension decays as
On the fundamental domain the fibre product factors by Fubini; the flow \(\zeta _t[x,s] = [x, s+t]\) moves the floor \(\lfloor s+t\rfloor \) through only the two values \(\lfloor t\rfloor , \lfloor t\rfloor + 1\), so the inner base integral is a base correlation at time \(\lfloor t\rfloor \) or \(\lfloor t\rfloor + 1\), bounded by the real form of Theorem 13.50. Centring \(g\) kills the surviving product-of-means term.
The fibre-rotation obstruction. A constant-roof suspension is never mixing as a flow: on the trivial fibre product \(f = g = 1\) the correlation is the circle-rotation correlation \(\int _0^1\psi (s)\chi (\{ t+s\} )\, ds\), which does not decay in \(t\) (for \(\psi = \chi = \cos (2\pi \cdot )\) it equals \(\tfrac 12\cos (2\pi t)\), of modulus \(\tfrac 12\) at every integer time). Decay therefore requires centring the base part (\(\int g = 0\)); the estimate above is the full centred flow correlation. (Cornfeld–Fomin–Sinai, Ergodic Theory, Ch. 11, on the reduction of special-flow correlations to base correlations.)
13.8 The Adler–Weiss coding as a factor and the symbolic flow tower
The sharp entropy computation of Section 13.6 extracts a number from the Adler–Weiss Markov partition; issue #58 extracts the coding map itself and stacks two of them into a flow tower. The two-box generator Definition 13.38 is upgraded from a generating partition to a genuine measure-theoretic factor map onto the golden subshift of finite type, and — because the half-open golden tiling has an empty (not merely null) junk cell (Lemma 13.39) — the coding is exactly (everywhere) equivariant and injective on the nose, with no boundary null sets discarded. Instantiating the suspension functor (Theorem 9.66) twice lifts the picture to the two mapping-torus flows. (R. L. Adler and B. Weiss, Similarity of automorphisms of the torus, Memoirs AMS 98 (1970); R. L. Adler, Symbolic dynamics and Markov partitions, Bull. AMS 35 (1998), 1–56; D. Lind and B. Marcus, An Introduction to Symbolic Dynamics and Coding, CUP (1995), Ch. 6; J. G. Kemeny and J. L. Snell, Finite Markov Chains, Springer (1976), on lumpability.)
13.8.1 The coding as a factor and a conjugacy onto its range
\(\operatorname {awSymbFull} : \mathbb {T}^2\to (\operatorname {Fin} 5)^{\mathbb {Z}}\), \(\operatorname {awSymbFull} x\, k = \operatorname {awSymb} x\, k\), records the branch symbol of the forward orbit of \(x\) at every integer time \(k\), landing in the two-sided full shift on the five golden branches.
\(\operatorname {awSymbFull}\) is a measure-theoretic factor map from \((\mathbb {T}^2, \operatorname {catTorus}, \mathrm{vol})\) onto the two-sided full shift, with the intertwining \(\operatorname {awSymbFull}\circ \operatorname {catTorus} = \operatorname {biShiftMap} \circ \operatorname {awSymbFull}\) holding everywhere (not merely a.e.): the empty junk cell of Lemma 13.39 gives every point a well-defined symbol at every time. The pushforward concentrates on the golden subshift-of-finite-type carrier, which has full measure \(1\) ().
Matching two-sided itineraries force equality of points (the Adler–Weiss contraction estimate), so \(\operatorname {awSymbFull}\) is injective on the nose — again no boundary null set is discarded. It is therefore a measurable embedding (, \(\mathbb {T}^2\) standard Borel), and the induced measurable equivalence onto its range is measure preserving (): a measure conjugacy of the cat map onto the golden SFT.
A disclosed frontier. The pushforward \(\operatorname {Measure.map}\, \operatorname {awSymbFull} \, \mathrm{vol}\) is the Markov measure of the golden Adler–Weiss data; identifying its cylinder values with the explicit golden transition probabilities is a follow-up (the factor map and the conjugacy onto the range are complete without it).
13.8.2 The coarse two-box partition: a \(\log 2\) ceiling with strict positivity
Merging the five golden branches by their source rectangle \(\operatorname {src}\) leaves the two original Adler–Weiss golden rectangles \(R_1, R_2\), a genuine two-cell partition and a factor of the fine generator.
The two-cell \(\operatorname {MeasurePartition}\) of \(\mathbb {T}^2\) into the two projected golden rectangles \(R_1, R_2\); its symbolic factor is the merged itinerary \(k\mapsto \operatorname {src}(\operatorname {awSymb} x\, k)\).
\(h(\operatorname {catTorus}, \operatorname {coarseAWPartition})\le \log 2\), strictly below the system entropy \(\log \lambda _+\) (): the coarse partition, unlike the fine generator, is far from generating. This is the abstract \(\log (\operatorname {card})\) ceiling for a partition into two cells.
\(0 {\lt} h(\operatorname {catTorus}, \operatorname {coarseAWPartition})\); indeed \(\log \lambda _+ - \log 2\le h(\operatorname {catTorus}, \operatorname {coarseAWPartition})\) (), strictly positive because \(\lambda _+ = (3+\sqrt5)/2 {\gt} 2\). The merged symbolic factor is thus a two-symbol system whose entropy lies in the nontrivial band \([\log \lambda _+ - \log 2, \log 2]\).
The substantive estimate is the fine forward-cylinder volume bound: an admissible word of length \(n+1\) cuts out a cylinder of measure \(\le 2(\varphi -1)\varphi /(\varphi +2)\cdot \lambda _+^{-n}\), as its unstable width contracts by \(\lambda _+^{-n}\) while its stable height stays \(\le \varphi \) (the \(\operatorname {bbInv}\) affine toolkit). A coarse \(n\)-join atom is a union of such cylinders, and the transfer-matrix fibre count of compatible admissible words is \(\le 5\cdot 2^n\) (each interior symbol has \(\le 2\) admissible choices). Multiplying gives a coarse-atom bound \(\le C\cdot (2/\lambda _+)^n\), which the entropy lower-bound glue converts into \(\log \lambda _+ - \log 2\le h\).
13.8.3 Entropy across the two coding stages
The golden-SFT image system \(\operatorname {Measure.map}\, \operatorname {awSymbFull}\, \mathrm{vol}\) under the shift has Kolmogorov–Sinai entropy exactly \(\log \! \big((3+\sqrt5)/2\big)\): being an injective factor, the Adler–Weiss coding is an entropy-preserving conjugacy, so the issue’s expectation of a strict drop at every step is impossible on this stage and is disclosed as such.
The \(1\)-block source merge \(\operatorname {mergeSrc} : (\operatorname {Fin} 5)^{\mathbb {Z}}\to (\operatorname {Fin} 2)^{\mathbb {Z}}\), \(y\mapsto (k\mapsto \operatorname {src}(y\, k))\), composed with the coding is the coarse itinerary \(\operatorname {coarseSymb}\); its image two-symbol system has entropy \(= h(\operatorname {catTorus}, \operatorname {coarseAWPartition})\le \log 2 {\lt} \log \lambda _+\) ( for the exact value): a genuine lumping with a strict entropy drop.
13.8.4 The depth-two symbolic flow tower
Instantiating the suspension functor twice at time \(1\) yields two suspension-flow factor maps: the first () is injective — the conjugacy stage, cat suspension \(\cong \) SFT\(_5\) suspension — and the second () is a genuine non-injective flow factor onto the two-symbol suspension with a strict flow-entropy drop \(h(\zeta ^{(2)}_1)\le \log 2 {\lt} \log \! \big((3+\sqrt5)/2\big) = h(\zeta ^{\mathrm{cat}}_1)\). All three levels are alive, with the merged level bracketed in \([\log \lambda _+ - \log 2, \log 2]\) by Theorem 13.61.
Honest disclosures. Stage 1 is a conjugacy, so a strict drop at each step is impossible on this lineage (the strict drop lives at stage 2); the pushforward \(=\) explicit-Markov-measure cylinder identification is deferred; and the issue’s \(\sqrt2\)-roof tower object does not exist — the unit roof is used throughout.