12 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.
12.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 12.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.
12.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 12.2 the iterate acts as \(D_x(T^{[n]})\), so Lemma 12.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 12.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 12.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 12.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 12.8), and the trace–determinant identity (Theorem 6.20) rewrites the full sum as \(\int \log \left\lvert \det A \right\rvert \, d\mu \).
12.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 12.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 9.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 12.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 9.24), and the expanding-case right-hand-side identity (Theorem 12.9), aligning the two determinant hypotheses along the \(\operatorname {fderiv}\)-to-matrix bridge.
12.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 12.14), not an abstract constant. The atom-count hypothesis is automatic for the binary partition, where the bound is attained (Theorem 12.17).
Specialize the abstract atom-count-growth entropy bound (the arithmetic backbone of the per-partition Ruelle inequality, cf. Theorem 9.23) to the doubling map at the exponential rate \(R = \log 2\), then identify the rate with the positive-exponent sum via Corollary 12.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 12.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 12.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 12.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\).
12.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 12.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 12.23) and evaluate the sorted eigenvalues of \(\left\lvert M \right\rvert = M\) by the closed form computed for Theorem 12.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 12.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 12.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 12.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 9.23) over the measure-preserving base \(\operatorname {catTorus}\) (Proposition 12.22) at the rate \(R = \log \bigl((3+\sqrt5)/2\bigr)\).