Ergodic Theory in Lean 4

9 Suspension flows: exponents, ergodicity, entropy

The abstract continuous-flow multiplicative ergodic theorem of Chapter 8 governs any measure-preserving \(\mathbb {R}\)-action carrying a continuous-time cocycle. This chapter studies the single most important source of such flows — the suspension (special-flow, or mapping-torus) construction, which manufactures a flow from a discrete base automorphism \(T\) and a positive roof function \(\tau \) — and computes its three characteristic invariants over concrete hyperbolic and Bernoulli bases: the Lyapunov exponents of the flow cocycle, the ergodicity of individual time-\(t\) maps, and the Kolmogorov–Sinai entropy of the flow.

The unifying theme is Abramov’s principle of time rescaling: a suspension flow runs the base clock at speed set by the roof, so a base invariant of rate type is divided by the mean roof \(\int \tau \). This yields the Lyapunov analogue \(\lambda _{\mathrm{flow}} = \lambda _{\mathrm{base}}/\int \tau \) of Abramov’s entropy formula \(h(\text{flow}) = h(\text{base})/\int \tau \) (L. M. Abramov, On the entropy of a flow, Dokl. Akad. Nauk SSSR 128 (1959) 873–875; L. Barreira, Lyapunov Exponents, Birkhäuser 2017, Ch. 3, on exponents under time rescaling). The time-\(1\) ergodicity holds exactly for irrational roofs; the time-\(1\) entropy identity \(h(\zeta ^{(r)}_1) = H_\nu /r\) is now proved for every roof \(r {\gt} 0\) via the abstract Abramov flow-entropy homogeneity \(h(\varphi _t) = t\, h(\varphi _1)\) (Theorem 9.48), following Ito’s elementary generator-free argument — retiring the former rational-roof restriction. Throughout, the standing references for the special-flow bookkeeping are Cornfeld–Fomin–Sinai (Ergodic Theory, Grundlehren 245, Springer 1982, Ch. 10–11) and the Ambrose–Kakutani structure theorem for measurable flows (Duke Math. J. 9 (1942) 25–42).

9.1 The suspension space and its invariant measure

The suspension of a measurable automorphism \(T : X \simeq X\) under a measurable roof \(\tau : X \to \mathbb {R}\) is the quotient of the cover \(X \times \mathbb {R}\) by the \(\mathbb {Z}\)-action generated by the shear \(G(x, s) = (Tx,\, s - \tau x)\); a point flows upward, \(\zeta _t[x, s] = [x, s + t]\), and re-enters the base after time \(\tau x\). We recall only the objects the rest of the chapter consumes; the abstract flow theorem they feed is Chapter 8’s Theorem 8.13.

Definition 9.1 The suspension (mapping-torus) space
#

The suspension space \(\Sigma = \operatorname {SuspensionSpace} T\, \tau \) is the orbit quotient of \(X \times \mathbb {R}\) by the suspension \(\mathbb {Z}\)-action \(G(x, s) = (Tx,\, s - \tau x)\), i.e. the mapping torus of \(T\) under the roof \(\tau \). As a Quotient it carries the canonical pushed-forward MeasurableSpace, and the projection \(\pi = \operatorname {suspensionMk} : X \times \mathbb {R}\to \Sigma \) is measurable.

Definition 9.2 The invariant suspension probability measure

The suspension measure \(\hat\mu = \operatorname {suspensionMeasure} T\, \tau \, \mu \) is obtained by restricting \(\mu \times \operatorname {vol}\) to the fundamental box \(\{ (x, s) : 0 \le s {\lt} \tau x\} \), pushing forward along \(\pi \), and normalising by \((\int \tau )^{-1}\). The generator \(G\) preserves \(\mu \times \operatorname {vol}\) whenever \(T\) preserves \(\mu \) (), because the shear is a fibered translation and \(\mathbb {R}\)-translation is Haar-invariant.

Theorem 9.3 \(\hat\mu \) is a probability measure

For a nonnegative integrable roof with \(0 {\lt} \int \tau \), the normalised suspension measure \(\hat\mu \) is a probability measure.

Proof

The raw box push-forward has total mass \(\int \tau \) (Fubini: the \(x\)-fibre of the box is \([0, \tau x)\), of length \(\tau x\)), which is positive and finite; multiplying by \((\int \tau )^{-1}\) makes the total mass \(1\).

The upward translation descends to a genuine measure-preserving flow on \(\Sigma \). Its time-\(t\) map is \(\operatorname {suspensionFlowMap} T\, \tau \, t\) (), packaged as a MeasurePreservingFlow \(\operatorname {suspensionFlow}\) (, ), with the base cross-section \(x \mapsto [x, 0]\) recorded as \(\operatorname {suspensionSection}\) (). These are exactly the ingredients Definition 8.1 of Chapter 8 asks for, so the abstract flow MET applies verbatim once a flow cocycle is supplied. The rest of the chapter supplies and analyses that cocycle.

9.2 The flow Lyapunov exponent over the suspension

A base matrix generator \(A : X \to \operatorname {Mat}_d(\mathbb {R})\) generates, over the cross-section flow, a cover cocycle on \(X \times \mathbb {R}\): reading a base point \(x\) at fibre height \(h\), advancing the special flow for time \(t\) accumulates the base cocycle over the total elapsed section time \(h + t\).

Definition 9.4 The cover flow cocycle
#

For a cover point \(p = (x, h)\) the cover cocycle \(\operatorname {coverCocycle} A\, T\, \tau \, (x, h)\, t\) is the cross-section flow cocycle read at the total elapsed time \(h + t\) from the base point \(x\). This is the cover-level form of the Cornfeld–Fomin–Sinai special-flow cocycle, one step before the orbit-quotient descent.

Lemma 9.5 Agreement on the base section

At height \(0\) the cover cocycle is the cross-section flow cocycle: \(\operatorname {coverCocycle}(x, 0)\, t = \operatorname {flowCocycleSection} t\, x\), since the total elapsed time \(0 + t\) collapses to \(t\).

Proof

Immediate from the definition on rewriting \(0 + t = t\) in the fibre coordinate.

Theorem 9.6 Section multiplicativity at a return boundary

Starting on the base section at \(x\), the cover cocycle over flow time \(\operatorname {returnTime} n\, x + r\) (for \(0 \le r\)) factors as the residual flow over time \(r\) from the shifted base point \(T^n x\), composed on the left of the discrete base cocycle for the \(n\) completed laps:

\[ \operatorname {coverCocycle}(x, 0)\bigl(\operatorname {returnTime} n\, x + r\bigr) = \operatorname {coverCocycle}(T^n x, 0)\, r \cdot \operatorname {cocycle} A\, T\, n\, x. \]
Proof

The accumulated matrix splits at the return boundary because the lap counter does; the return cocycle is multiplicative across the split, and its first \(n\) laps give \(\operatorname {cocycle} A\, T\, n\, x\) by the return identity. Reordering the split so the \(n\) completed laps sit on the right yields the stated factorisation.

The matrix cover cocycle does not descend to \(\Sigma \): re-basing along \(n\) orbit steps post-multiplies it by the fixed factor \(\operatorname {cocycle} A\, T\, n\, x\). What descends is the growth rate, because that fixed multiplicative factor becomes a fixed additive \(\log \) shift, washed out by the \(1/t\) Birkhoff average.

Theorem 9.7 Additive \(\log \)-discrepancy across an orbit step

Under invertibility of the base cocycle and strict positivity of both cover-cocycle norms, for \(\operatorname {returnTime} n\, x \le s + t\) the two \(\log \)-norms differ by at most a constant in \(t\):

\[ \bigl|\log \left\lVert \operatorname {coverCocycle}(\operatorname {suspensionAct} n\, (x, s))\, t \right\rVert - \log \left\lVert \operatorname {coverCocycle}(x, s)\, t \right\rVert \bigr| \le \bigl|\log \left\lVert \operatorname {cocycle} A\, T\, n\, x \right\rVert \bigr| + \bigl|\log \left\lVert (\operatorname {cocycle} A\, T\, n\, x)^{-1} \right\rVert \bigr|. \]

The absolute values keep the bound honest: an operator norm need not be \(\ge 1\), so an individual \(\log \)-norm can be negative.

Proof

Take \(\log \) of the two operator-norm brackets supplied by Theorem 9.6 (which bound \(\left\lVert \operatorname {coverCocycle}(x, s)\, t \right\rVert \) between \(\left\lVert \cdot \right\rVert \) at the re-based point times \(\left\lVert \operatorname {cocycle} \right\rVert ^{\pm 1}\)), using \(\log \)-monotonicity and \(\log (ab) = \log a + \log b\) on the strictly positive factors, then bound each \(\log \) factor by its absolute value.

Theorem 9.8 The Lyapunov-exponent limit transfer

If the cover-cocycle growth rate \(t^{-1}\log \left\lVert \operatorname {coverCocycle}(x, s)\, t \right\rVert \) converges to \(L\) as \(t \to \infty \), the base cocycle is invertible, and both cover-cocycle norms are eventually strictly positive, then the growth rate at the re-based orbit point \(\operatorname {suspensionAct}(n)\, (x, s)\) converges to the same \(L\).

Proof

The per-\(t\) average at the re-based point lies within \(C/t\) of the average at \((x, s)\), where \(C\) is the \(t\)-independent additive discrepancy of Theorem 9.7; since \(C/t \to 0\), a Filter.Tendsto squeeze transfers the limit.

Definition 9.9 The flow Lyapunov exponent of an orbit class

\(\operatorname {HasFlowExponent} q\, L\) holds when some representative \((x, s)\) of the orbit class \(q \in \Sigma \) carries the cover-cocycle growth rate \(L\): \(\pi (x, s) = q\) and \(t^{-1}\log \left\lVert \operatorname {coverCocycle}(x, s)\, t \right\rVert \to L\). The existential form lifts cleanly to the quotient; the well-definedness results below show that, under base-cocycle invertibility, the rate is in fact the same for every representative.

Theorem 9.10 Two-sided well-definedness across a forward step

If \((x_2, s_2) = \operatorname {suspensionAct}(n)\, (x, s)\) for a natural \(n\), the base cocycle is invertible, and both cover-cocycle norms are eventually strictly positive, then the cover-cocycle growth rates at \((x, s)\) and at \((x_2, s_2)\) converge to one and the same \(L\): the two Tendsto statements are equivalent.

Proof

The \(\to \) direction is Theorem 9.8. The \(\leftarrow \) direction is its mirror: the additive \(\log \)-discrepancy bound of Theorem 9.7 is symmetric in the two points, so the same \(1/t\) squeeze transfers the limit the other way.

Theorem 9.11 Orbit-class invariance of the flow exponent

If two cover points are connected by a forward orbit step \(\operatorname {suspensionAct}(n)\, (x, s) = (x_2, s_2)\), then a growth rate \(L\) computed at \((x, s)\) witnesses \(\operatorname {HasFlowExponent}(\pi (x_2, s_2))\, L\): the exponent is a property of the whole orbit class, read off from any representative.

Proof

Orbit-equivalent points have equal \(\pi \)-images, so \((x, s)\) itself serves as the witness for the common class; its growth rate is \(L\) by hypothesis. (Invertibility is needed only to guarantee the same \(L\) from the other representative, via Theorem 9.10.)

9.2.1 The Abramov exponent formula

Disintegrating \(\hat\mu \) over the base measure and feeding in the base Birkhoff limits gives the headline: the flow exponent is the base exponent divided by the mean roof.

Theorem 9.12 The special-flow Lyapunov exponent, \(\lambda _{\mathrm{flow}} = \lambda _{\mathrm{base}}/\int \tau \)

Under a bounded roof \(c \le \tau \le C\) (\(0 {\lt} c\)), positive integral \(0 {\lt} \int \tau \), measurable base generator \(A\), and the base-a.e. Birkhoff limits — discrete base growth rate \(\to \lambda _{\mathrm{base}}\) and roof average \(\to \int \tau \) — for \(\hat\mu \)-almost every orbit class \(q\),

\[ \operatorname {HasFlowExponent} q\ \Bigl(\lambda _{\mathrm{base}}\big/\! \int \tau \Bigr). \]
Proof

The base exponent-set measurability is supplied internally: the full-time cover-cocycle exponent set is rewritten pointwise as the discrete return-time exponent set (the between-returns squeeze) and is measurable by measurableSet_tendsto, so only \(A\) measurable is assumed. The base-a.e. growth and roof limits are transported to \(\hat\mu \)-a.e. orbit classes through the fundamental-domain disintegration, and the between-returns squeeze converts the discrete return-time exponent \(\lambda _{\mathrm{base}}/\int \tau \) into the full-time flow exponent.

Theorem 9.13 The exponent along genuine flow orbits

Under the same hypotheses (and \(T\) measure-preserving), for \(\hat\mu \)-a.e. \(q\) there are a base point \(x\) and a flow time \(s\) with \(q = \operatorname {suspensionFlow} s\, (\text{section } x)\) and \(\operatorname {HasFlowExponent} q\, (\lambda _{\mathrm{base}}/\int \tau )\): the exponent is realised on the genuine measure-preserving flow orbit of a cross-section point.

Proof

The disintegration already identifies each a.e. class with a flow-orbit point of the base section; carry that identification alongside the exponent conclusion of Theorem 9.12.

9.2.2 The representative-free descent

The predicate \(\operatorname {HasFlowExponent}\) is existential over representatives. Upgrading it to a genuine function \(\Sigma \to \mathbb {R}\) requires closing the signed orbit step (a backward step \(m {\lt} 0\)) and paying one honest cost: a global base-cocycle invertibility hypothesis that makes the Quotient.lift total.

Lemma 9.14 Strict positivity under global invertibility

If the base generator \(A\) is everywhere invertible (\(\det \ne 0\)), then \(0 {\lt} \left\lVert \operatorname {coverCocycle} p\, t \right\rVert \) for every cover point \(p\) and time \(t\): the cover cocycle reduces to a base-cocycle iterate whose norm is strictly positive.

Proof

Unfold the cover cocycle to \(\operatorname {cocycle} A\, T\, (\text{lap count})\, x\), a product of invertible matrices, hence nonzero with positive operator norm.

Theorem 9.15 Signed-step cross-representative uniqueness

If two cover points are connected by a signed orbit step \(\operatorname {suspensionAct} m\, (x_2, s_2) = (x_1, s_1)\) for \(m \in \mathbb {Z}\), and the base cocycle is everywhere invertible, then the cover-cocycle growth rates at \((x_1, s_1)\) and \((x_2, s_2)\) converge to the same \(L\).

Proof

Both signs reduce to the forward iff of Theorem 9.10 at a different base point: for \(0 \le m\) at base \((x_2, s_2)\); for \(m \le 0\) after inverting the connection to \(\operatorname {suspensionAct}(-m)\, (x_1, s_1) = (x_2, s_2)\), at base \((x_1, s_1)\). Global invertibility discharges the unit-determinant and eventual strict-positivity side conditions on both representatives via Lemma 9.14.

Definition 9.16 The representative-level and descended exponents
#

\(\operatorname {repExponent} p\) () is the growth-rate limit \(\lim _t t^{-1}\log \left\lVert \operatorname {coverCocycle} p\, t \right\rVert \) read off from a representative, with a fixed junk value \(0\) off the convergence locus (a plain \(\texttt{dite}\)/\(\texttt{choose}\) rather than \(\texttt{limUnder}\), whose junk is not constant across representatives). \(\operatorname {flowExponentAt} : \Sigma \to \mathbb {R}\) is its \(\texttt{Quotient.lift}\), made total by global base-cocycle invertibility.

Theorem 9.17 \(\operatorname {flowExponentAt}\) reads off the exponent

If \(q\) carries the flow exponent \(L\) (some representative has cover-cocycle growth rate \(L\)), then \(\operatorname {flowExponentAt} q = L\).

Proof

Well-definedness of the lift (Theorem 9.15) transfers existence of the limit across any orbit step; where it exists on both sides, uniqueness of limits forces the two values to agree, so the descended value equals the witnessing \(L\).

Theorem 9.18 The representative-free Abramov exponent

Under a bounded roof, positive \(\int \tau \), measurable base generator, global invertibility \(\forall x,\ \det (A x) \ne 0\), and the base-a.e. Birkhoff limits, for \(\hat\mu \)-almost every orbit class \(q\) the genuine (representative-free) flow exponent equals \(\lambda _{\mathrm{base}}/\int \tau \): \(\operatorname {flowExponentAt} q = \lambda _{\mathrm{base}}/\int \tau \).

Proof

Combine the existential a.e. exponent of Theorem 9.12 with the read-off equality Theorem 9.17; the added global-invertibility hypothesis is the documented honest cost of upgrading the predicate to the actual lifted value.

9.2.3 The cat-map suspension flow

The exponent theory is instantiated on the suspension of the Arnold cat map \(\operatorname {catTorus}\) (Definition 13.21) under the unit roof \(\tau \equiv 1\), fed the base’s own derivative cocycle (Definition 13.1), which is the constant hyperbolic matrix \(M = \left(\begin{smallmatrix} 2 & 1 \\ 1 & 1 \end{smallmatrix}\right)\). Its spectrum (Theorem 13.24) gives the base top exponent \(\log \bigl((3+\sqrt5)/2\bigr) {\gt} 0\), and \(\int \tau = 1\), so \(\lambda _{\mathrm{flow}} = \lambda _{\mathrm{base}}\).

Theorem 9.19 The cat suspension realises the base derivative-cocycle exponent

For \(\hat\mu \)-a.e. orbit class \(q\) of the cat-map suspension under the unit roof, the flow Lyapunov exponent of the base’s own derivative cocycle is \(\operatorname {HasFlowExponent} q\ \bigl(\log ((3+\sqrt5)/2)\bigr) = \lambda _{\mathrm{base}}/\int \tau \).

Proof

The generator is constant in the base point, so its discrete growth rate is the deterministic Gelfand limit \(n^{-1}\log \left\lVert M^n \right\rVert \to \log ((3+\sqrt5)/2)\) (spectral radius identified through the Grade-1 cat spectrum Theorem 13.24), and the unit-roof Birkhoff average is \(1 = \int \tau \). Instantiate Theorem 9.12 at this data.

Theorem 9.20 Positivity of the cat suspension exponent (issue #30)

For \(\hat\mu \)-a.e. orbit class \(q\) there is a positive \(L\) with \(\operatorname {HasFlowExponent} q\, L\): the hyperbolicity of the cat map, \((3+\sqrt5)/2 {\gt} 1\), makes \(L = \log ((3+\sqrt5)/2) {\gt} 0\).

Proof

Take \(L = \log ((3+\sqrt5)/2)\) from Theorem 9.19; positivity is \(\log \) of a number exceeding \(1\).

Theorem 9.21 Abramov quotient reading, existential form

The flow exponent equals the base top Lyapunov exponent of \(M\) over the genuine ergodic cat map divided by the mean roof \(\int \tau \); since \(\int \tau = 1\) this is the same numerical value, exposed in its Abramov-style quotient form.

Proof

Rewrite the base top exponent as the Grade-1 spectral value \(\log ((3+\sqrt5)/2)\) and divide by \(\int \tau = 1\); the result is the exponent of Theorem 9.19.

The three headlines are then upgraded from “some representative realises \(L\)” to genuine equalities of the descended function \(\operatorname {flowExponentAt}\), the base generator \(M\) having determinant \(1 \ne 0\) (so the descent is total).

Theorem 9.22 Representative-free cat exponent

For \(\hat\mu \)-a.e. \(q\), the descended flow exponent is \(\operatorname {flowExponentAt} q = \log ((3+\sqrt5)/2)\).

Proof

Apply Theorem 9.17 to the existential exponent Theorem 9.19; global invertibility of \(M\) makes the lift total.

Theorem 9.23 Representative-free Abramov reading

The descended flow exponent equals the base top exponent of \(M\) divided by \(\int \tau \), an honest equality of the \(\Sigma \to \mathbb {R}\) function rather than an existential over representatives.

Proof

Rewrite the base exponent as \(\log ((3+\sqrt5)/2)\) and \(\int \tau = 1\) in Theorem 9.22.

Theorem 9.24 Representative-free positivity

For \(\hat\mu \)-a.e. \(q\), the descended flow exponent is strictly positive: \(0 {\lt} \operatorname {flowExponentAt} q\).

Proof

Substitute the value \(\log ((3+\sqrt5)/2)\) from Theorem 9.22; it is positive because \((3+\sqrt5)/2 {\gt} 1\).

9.3 Ergodicity of the time-one map

Fix a constant roof \(\tau \equiv r\). The time-\(1\) map of the suspension flow acts on the lifted plane by \((x, s) \mapsto (x, s + 1)\) modulo the deck relation, so its ergodicity is a fibre-Fourier question with transform window the invariance period \(1\) — not the roof \(r\). This is the constant-roof special-flow dichotomy of Cornfeld–Fomin–Sinai (Ch. 11). The spectral input is that the base has no nontrivial unimodular eigenfunctions, which for a strongly mixing base is automatic.

Theorem 9.25 Strong mixing of the two-sided Bernoulli shift

For the invertible two-sided Bernoulli shift with i.i.d. measure \(\operatorname {bernZ}\nu \) and measurable sets \(A, B\), the diagonal correlations converge to the product of measures:

\[ \hat\nu (A \cap \sigma ^{-k} B) \to \hat\nu (A)\, \hat\nu (B) \qquad (k \to \infty ). \]
Proof

Approximate \(A, B\) by finite-block cylinder sets in symmetric difference; on cylinders the correlation is eventually exactly the product (independence past the block width), and the measure-preserving iterate keeps the symmetric-difference mass, so the \(\varepsilon /5\) bookkeeping pushes the exact identity to the limit. Classical (Cornfeld–Fomin–Sinai §10; Walters, An Introduction to Ergodic Theory, Thm. 1.30): Bernoulli shifts are strong mixing.

Theorem 9.26 Mixing kills eigenvalues

A measurable eigenfunction \(g\) (with \(g \circ f = l\, g\)) of a strongly-mixing transformation \(f\), whose eigenvalue \(l\) is unimodular (\(\left\lVert l \right\rVert = 1\)) but \(l \ne 1\), vanishes almost everywhere.

Proof

Purely set-theoretic. The powers \(l^n\) stay a fixed distance \(\delta = \left\lVert l - 1 \right\rVert /2\) from \(1\) infinitely often (the two-consecutive-powers trick, ). If \(g\) were not a.e. zero, pick an admissible ball \(B = \operatorname {ball} q\, \rho \) with \(q \ne 0\) and \(2\rho \le \left\lVert q \right\rVert \delta \) whose preimage \(A = g^{-1}B\) has positive measure. A point of \(A \cap (f^n)^{-1}A\) would place both \(g x\) and \(l^n g x\) inside \(B\), forcing \(\left\lVert l^n q - q \right\rVert {\lt} 2\rho \le \left\lVert q \right\rVert \left\lVert l^n - 1 \right\rVert = \left\lVert l^n q - q \right\rVert \) whenever \(\left\lVert l^n - 1 \right\rVert \ge \delta \); this happens frequently, so the diagonal correlation vanishes along a subsequence — contradicting mixing, which drives it to \(\hat\mu (A)^2 {\gt} 0\).

The harmonic-analysis engine works on the lifted plane. The transform window is the unit invariance period, so no lap decomposition of the roof is needed.

Definition 9.27 The fibre Fourier coefficient
#

For \(F : X \times \mathbb {R}\to \mathbb {C}\) the \(n\)-th fibre Fourier coefficient over the unit invariance window is \(\operatorname {coeffFn} F\, n\, x = \int _0^1 \overline{e_n(s)}\, F(x, s)\, ds\), where \(e_n\) is the \(n\)-th character of the length-\(1\) circle. Its window is the period of the time-one map, not the roof.

Theorem 9.28 The twisted eigenfunction relation

If \(F\) is \(1\)-periodic in the fibre and satisfies the deck identity \(F(Tx, s) = F(x, s + r)\), then

\[ \operatorname {coeffFn} F\, n\, (Tx) = e^{2\pi i n r}\, \operatorname {coeffFn} F\, n\, x. \]
Proof

A three-step change of variables over the unit window: character algebra factoring out \(e^{2\pi i n r}\), the translation \(\int _0^1 G(s + r)\, ds = \int _r^{1+r} G\), and \(1\)-periodicity of \(G\) to return the window to \([0, 1]\).

For a \(\zeta _1\)-invariant set \(A\) in a constant-roof suspension, its lifted indicator \(\operatorname {liftedIndicator} A = \mathbf1_{\pi ^{-1}A}\) () is \(1\)-periodic in the fibre and satisfies the deck identity, so its fibre coefficients are twisted eigenfunctions ().

Theorem 9.29 Per-fibre Parseval bridge
#

For a bounded measurable \(f : \mathbb {R}\to \mathbb {C}\), the squared fibre-coefficient sum equals the fibre \(L^2\) mass: \(\sum _{n \in \mathbb {Z}}\left\lVert \operatorname {coeffFn}(f)\, n \right\rVert ^2 = \int _0^1\left\lVert f \right\rVert ^2\).

Proof

Lift \(f\) to the length-\(1\) circle \(\operatorname {AddCircle}(1)\); the interval coefficients are the circle’s Fourier coefficients and the interval \(L^2\) mass is the circle \(L^2\) mass, so Mathlib’s circle Parseval identity \(\sum \left\lVert \hat f(n) \right\rVert ^2 = \left\lVert f \right\rVert _2^2\) gives the claim.

Theorem 9.30 Indicator dichotomy

Let \(g : \mathbb {R}\to \mathbb {R}\) be measurable, \(1\)-periodic, \(\{ 0, 1\} \)-valued, with all nonzero-mode Fourier coefficients (over period \(1\)) vanishing. Then \(g = 0\) a.e. on \((0, 1]\) or \(g = 1\) a.e. on \((0, 1]\).

Proof

Parseval collapses to the zero mode: \(\bigl(\int _0^1 g\bigr)^2 = \int _0^1\left\lVert g \right\rVert ^2 = \int _0^1 g\) (the last since \(g^2 = g\) on \(\{ 0, 1\} \)), so \(\int _0^1 g \in \{ 0, 1\} \). If the integral is \(0\) then \(g = 0\) a.e.; if it is \(1\) then \(1 - g = 0\) a.e. A periodic null-set spread () then carries the null fibre across every unit cell.

Theorem 9.31 Time-one ergodicity, abstract base-generic form (issue #35)

Let \(T\) be ergodic and measure-preserving on a probability space whose only measurable eigenfunction with a unimodular eigenvalue \(\ne 1\) is \(0\). For a positive irrational roof \(r\), the time-\(1\) map of the constant-roof suspension flow is ergodic for \(\hat\mu \).

Proof

Fix a \(\zeta _1\)-invariant \(A\) with lifted indicator \(F\). For \(n \ne 0\) the twist eigenvalue \(e^{2\pi i n r}\) is unimodular and \(\ne 1\) (irrationality of \(r\)), so the spectral hypothesis forces \(\operatorname {coeffFn} F\, n = 0\) a.e. (Theorem 9.28); the zero mode is \(T\)-invariant, hence a.e. constant by base ergodicity. Per fibre, the dichotomy Theorem 9.30 makes \(F(x, \cdot )\) a.e. \(0\) or a.e. \(1\), and the periodic spread fills the roof window \([0, r)\); Fubini over the fundamental box then gives \(\hat\mu (A) \in \{ 0, 1\} \).

Theorem 9.32 Time-one ergodicity of the irrational-roof Bernoulli suspension

For the two-sided Bernoulli shift with measure \(\operatorname {bernZ}\nu \) and any positive irrational roof \(r\), the time-\(1\) map of the constant-roof suspension flow is ergodic for the invariant suspension probability measure.

Proof

Discharge the abstract Theorem 9.31 with base ergodicity of the shift and the no-nontrivial-eigenfunctions input: strong mixing (Theorem 9.25) feeds Theorem 9.26, forcing every measurable unimodular eigenfunction with eigenvalue \(\ne 1\) to vanish a.e.

Theorem 9.33 Concrete non-vacuity witness \(r = \sqrt2\)

The irrational roof \(r := \sqrt2\) yields an ergodic time-\(1\) map, confirming the hypothesis \(\operatorname {Irrational} r\) is satisfiable.

Proof

Instantiate Theorem 9.32 at \(r = \sqrt2\), positive and irrational.

The irrationality is essential. For the unit roof \(r = 1\) the time-\(1\) map is genuinely non-ergodic (Theorem 12.21 records that only the full flow is ergodic).

Theorem 9.34 Non-ergodicity at the unit roof

The time-\(1\) map of the unit-roof Bernoulli suspension flow is not ergodic.

Proof

With \(r = 1\) the deck translation advances the fibre by exactly the invariance period, so the saturated half-section \(\{ [x, s] : \operatorname {frac} s {\lt} 1/2\} \) is a nontrivial time-\(1\)-invariant set of mass \(1/2\). Equivalently, the flow-generator eigenfunction \(e^{2\pi i s}\) has eigenvalue \(e^{2\pi i} = 1\) at time \(1\) and descends to a non-constant invariant function; the zero-one law fails.

9.4 Entropy descent

The Kolmogorov–Sinai entropy of the flow’s time-\(t\) maps is governed by the discrete power rule and the Abramov time-change. The base algebra is the entropy analogue of Theorem 9.8.

Theorem 9.35 Discrete entropy power rule

For a measure-preserving \(T\) on a probability space and \(n \in \mathbb {N}\), \(h(T^n) = n \cdot h(T)\).

Proof

Walters, An Introduction to Ergodic Theory, Theorem 4.13. The \(n\)-fold refinement of a partition under \(T^n\) is a subsequence of the refinement under \(T\), and the Fekete limit along the arithmetic progression \(kn\) equals \(n\) times the full limit.

Theorem 9.36 Flow iterate identity
#

For a measure-preserving flow \(\varphi \), the \(n\)-th iterate of the time-\(t\) map is the time-\((nt)\) map: \((\varphi _t)^{[n]} = \varphi _{nt}\).

Proof

Induction on \(n\) using \(\varphi _{s+t} = \varphi _s \circ \varphi _t\) and the iterate recursion.

Theorem 9.37 Flow entropy homogeneity along \(\mathbb {N}\)-multiples

For a measure-preserving flow \(\varphi \) on a probability space, \(n \cdot h(\varphi _t) = h(\varphi _{nt})\).

Proof

Apply the power rule Theorem 9.35 to \(T = \varphi _t\), whose \(n\)-th iterate is \(\varphi _{nt}\) by Theorem 9.36; entropy depends only on the underlying map.

The Abramov time-change conjugates a constant-\(r\) roof to the unit roof, rescaling the fibre.

Definition 9.38 The fibre-rescaling equivalence
#

The fibre map \((x, s) \mapsto (x, s/r)\) descends to a measurable equivalence \(\operatorname {suspensionRescale} : \operatorname {SuspensionSpace} T\, (\tau \equiv r) \simeq \operatorname {SuspensionSpace} T\, (\tau \equiv 1)\), conjugating the constant-\(r\) generator \((x, s) \mapsto (Tx, s - r)\) to the unit generator \((x, s) \mapsto (Tx, s - 1)\) (since \((s - r)/r = s/r - 1\)). It is the constant-roof case of the Ambrose–Kakutani/Abramov time-change.

Theorem 9.39 The time-\(r\) entropy conjugacy

The time-\(t\) map of the constant-\(r\) suspension flow has the same Kolmogorov–Sinai entropy as the time-\((t/r)\) map of the unit-roof suspension flow.

Proof

Measurable-conjugacy invariance of entropy applied to \(\operatorname {suspensionRescale}\): it intertwines \(\zeta ^{(r)}_t\) with \(\zeta ^{(1)}_{t/r}\) and transports the invariant measure (the box \(X \times [0, r)\) maps to \(X \times [0, 1)\), scaling the fibre length by \(r\), exactly cancelling the \(r^{-1}\) vs \(1^{-1}\) normalisations).

Theorem 9.40 Time-\(r\) entropy of the Bernoulli suspension

For the constant-roof (\(\tau \equiv r\)) suspension of the two-sided Bernoulli shift, the time-\(r\) map has Kolmogorov–Sinai entropy exactly the per-symbol Shannon entropy \(H_\nu \).

Proof

Theorem 9.39 at \(t = r\) (so \(t/r = 1\)) reduces to the unit-roof time-\(1\) value \(h(\zeta ^{(1)}_1) = H_\nu \) (Theorem 12.22).

Theorem 9.41 Constant-roof time-one entropy, rational roof (issue #38)

For a rational roof \(r = a/b\) (\(a, b \in \mathbb {N}\) positive), the time-\(1\) map of the constant-roof Bernoulli suspension flow has Kolmogorov–Sinai entropy \(H_\nu /r\).

Proof

Fibre time-rescaling reduces \(h(\zeta ^{(r)}_1)\) to the unit-roof \(h(\zeta ^{(1)}_{1/r})\); writing \(1/r = b/a\), homogeneity along \(\mathbb {N}\)-multiples (Theorem 9.37) gives \(a \cdot h(\zeta ^{(1)}_{b/a}) = h(\zeta ^{(1)}_b) = b \cdot h(\zeta ^{(1)}_1) = b\, H_\nu \). Since \(H_\nu \) is finite and \(a {\gt} 0\), the \(\mathbb {N}\)-scalar \(\overline\mathbb {R}\)-equation \(a \cdot h(\zeta ^{(r)}_1) = b\, H_\nu \) pins \(h(\zeta ^{(r)}_1) = b\, H_\nu /a = H_\nu /r\), the arithmetic descending to \(\mathbb {R}\).

Theorem 9.42 Multiplicative form

For a rational roof \(r = a/b\), \(\; h(\zeta ^{(r)}_1) \cdot r = H_\nu \).

Proof

Multiply the value form Theorem 9.41 by \(r\); the product \((H_\nu /r) \cdot r = H_\nu \) is real arithmetic.

9.5 Abstract Abramov flow-entropy homogeneity

The rational restriction of Theorem 9.41 is an artefact of the discrete power rule, not of the mathematics: the full Abramov homogeneity \(h(\varphi _t) = t\, h(\varphi _1)\) holds for every real time \(t {\gt} 0\). We prove it abstractly for any measure-continuous measure-preserving flow on a standard Borel probability space, following Ito’s elementary generator-free argument (Y. Ito, An elementary proof of Abramov’s result on the entropy of a flow, Nagoya Math. J. 41 (1971), 1–5), which avoids the flow generators / Rokhlin towers (Ambrose–Kakutani structure) of Abramov’s original approach (L. M. Abramov, On the entropy of a flow, Dokl. Akad. Nauk SSSR 128 (1959) 873–875).

Definition 9.43 Measure-continuity of a flow

A measure-preserving flow \(\varphi \) is measure-continuous if for every measurable set \(A\) the real measure of the symmetric difference \(\varphi _t^{-1} A \, \triangle \, A\) tends to \(0\) as \(t \to 0\).

Theorem 9.44 Measure-continuity of the suspension flow

The unit-roof suspension flow of an arbitrary measure-preserving base is measure-continuous: for every measurable \(A\), \(\mu \! \left(\varphi _t^{-1} A \, \triangle \, A\right) \to 0\) as \(t \to 0\). This is the keystone hypothesis; the Bernoulli suspension flow instantiates it ().

Proof

Fibre-translation continuity of the roof-1 fundamental box, combined with dominated convergence over the box.

Theorem 9.45 Ito’s L1: the partition moves little under a small shift

For a measure-continuous flow and a finite partition \(P\), the conditional Shannon entropy \(H(\varphi _t P \mid P) \to 0\) as \(t \to 0\) (Ito’s (2.2)).

Proof

The self-conditioning \(H(P \mid P) = 0\), and the cell measures \(\mu (\varphi _t^{-1}P_i \cap P_j)\) are continuous at \(t = 0\) by measure-continuity; continuity of the Shannon cell functional transports the limit.

Theorem 9.46 Two-family Shannon comparison

For two finite families \(\beta = (\beta _k)\), \(\gamma = (\gamma _k)\) of finite partitions, \(H\! \left(\bigvee _k \gamma _k\right) \le H\! \left(\bigvee _k \beta _k\right) + \sum _k H(\gamma _k \mid \beta _k)\).

Proof

Pure Shannon entropy: refinement monotonicity, the chain rule, conditional subadditivity over the family, and anti-monotonicity of conditioning.

Theorem 9.47 \(\varepsilon \)–\(\delta \) alignment proposition

For a measure-continuous flow on a standard Borel space and a finite partition \(P\), the ratio \(t \mapsto h(\varphi _t, P)/t\) converges as \(t \downarrow 0\) to its least upper bound \(L \in \overline{\mathbb {R}}\) over all positive times. The statement is genuinely in \(\overline{\mathbb {R}}\): the \(\mathbb {R}\)-valued form is false for infinite-entropy flows, and this repair is disclosed in-module.

Proof

The alignment inequality (from Theorem 9.45 and Theorem 9.46) makes each slope eventually dominate every value below the supremum; the supremum is thus the limit.

Theorem 9.48 Abstract Abramov homogeneity

For a measure-continuous measure-preserving flow \(\varphi \) on a standard Borel probability space and \(t {\gt} 0\), \(\; h(\varphi _t) = t \cdot h(\varphi _1)\) in \(\overline{\mathbb {R}}\).

Proof

Interchange the supremum over partitions with the alignment proposition (Theorem 9.47), using the discrete \(\mathbb {N}\)-homogeneity (Theorem 9.37); at \(t = 1\) the slope is \(h(\varphi _1)\), giving the stated multiple.

Theorem 9.49 Unit-roof time-\(s\) entropy, all \(s {\gt} 0\)

For the unit-roof Bernoulli suspension flow and every \(s {\gt} 0\), \(h(\zeta ^{(1)}_s) = s \cdot H_\nu \).

Proof

Theorem 9.48 for the measure-continuous Bernoulli suspension flow, at the finite value \(h(\zeta ^{(1)}_1) = H_\nu \).

Theorem 9.50 Constant-roof time-one entropy, all roofs (issue #48)

For every roof \(r {\gt} 0\) (irrational included), the time-\(1\) map of the constant-roof Bernoulli suspension flow has Kolmogorov–Sinai entropy \(H_\nu /r\).

Proof

Fibre time-rescaling reduces \(h(\zeta ^{(r)}_1)\) to the unit-roof \(h(\zeta ^{(1)}_{1/r})\); Theorem 9.49 at \(s = 1/r\) gives \((1/r)\, H_\nu = H_\nu /r\).

This retires the entropy-side wall of Theorem 9.41: the value \(H_\nu /r\) now holds, with a formalized proof, for every roof \(r {\gt} 0\). The two headline features of the constant-roof time-\(1\) map are then complementary. Ergodicity holds exactly for irrational roofs (Theorem 9.32) and fails for rational ones (Theorem 9.34); the entropy is \(H_\nu /r\) for all \(r {\gt} 0\) (Theorem 9.50), so on the irrational roofs a single object carries both an ergodic time-\(1\) map and pinned positive entropy \(H_\nu /r\). The ergodicity turns on the deck twist \(e^{2\pi i n r}\) being nontrivial (irrational \(r\)); the entropy, on the flow homogeneity, which no longer sees the arithmetic of \(r\).

9.6 The quotient-level suspension flow cocycle

The representative-free exponent above lives on orbit classes but is built from a chosen representative. Issue #53 asks for the strictly finer object: the flow’s own matrix derivative data, packaged as a genuine Definition 8.3 on the quotient (mapping-torus) space, the very interface consumed by the continuous-flow MET Theorem 8.13. This is achievable for the constant unit roof \(\tau \equiv 1\), where the fundamental domain is the box \(X \times [0,1)\) and the quotient projection restricted to it is a measurable bijection — the measurable trivialization of the suspension bundle over a standard Borel base.

Definition 9.51 The two-sided \(\mathbb {Z}\)-indexed matrix cocycle
#

Over an invertible measure-preserving base \(T : X \simeq X\), the one-sided iterated cocycle (indexed by \(\mathbb {N}\)) extends to a two-sided \(\mathbb {Z}\)-indexed cocycle \(\operatorname {cocycleZ} A\, T\, n\): for \(n \ge 0\) the forward cocycle, and for \(n {\lt} 0\) the backward cocycle of the inverse dynamics with generator \(x \mapsto (A(T^{-1}x))^{-1}\).

Theorem 9.52 The two-sided cocycle identity
#

\(\operatorname {cocycleZ}(m + n)\, x = \operatorname {cocycleZ} m\, (\operatorname {baseIter} n\, x) \cdot \operatorname {cocycleZ} n\, x\), where \(\operatorname {baseIter}\) is the \(\mathbb {Z}\)-iterate of the base. This is the keystone that lets the discrete object assemble into a continuous-time cocycle.

Definition 9.53 The genuine quotient flow cocycle

For the constant unit roof, reading off a measurable canonical representative \(\operatorname {unitFwd} q = (\operatorname {baseIter}\lfloor s\rfloor x, \{ s\} )\) of each orbit class \(q = [x,s]\), the assignment \(t \mapsto \operatorname {cocycleZ} A\, T\, \lfloor \{ s\} + t\rfloor \, (\operatorname {unitFwd} q)_1\) is a genuine Definition 8.3 on the mapping torus. The four cocycle fields follow from Theorem 9.52 transported through the floor split \(\lfloor a + t\rfloor = \lfloor a\rfloor + \lfloor \{ a\} + t\rfloor \).

Theorem 9.54 Cohomology to the cover cocycle

Over the quotient, Definition 9.53 is cohomologous to the cover cocycle (Definition 9.4): at a general representative \((x,s)\) with \(0 \le s\) the two differ by the measurable rep-level frame \(C(x,s) = \operatorname {cocycleZ} A\, T\, \lfloor s\rfloor x\). Because different representatives of one class carry different \(\lfloor s\rfloor \), the issue’s schematic class-level conjugacy is provably impossible; the honest general statement is this rep-level frame, collapsing to the conjugation-free canonical identity at \(\operatorname {unitFwd}\).

Proof

Take \(B = \operatorname {quotientFlowCocycle}\) and \(C(p) = \operatorname {cocycleZ} A\, T \lfloor p_2\rfloor p_1\); measurability of \(C\) is the composition of \(\lfloor \cdot \rfloor \) with the measurable-in-index cocycle, and the frame identity is the floor split of Theorem 9.52.

Theorem 9.55 Exponent transport

Along the \(\operatorname {atTop}\) half-line \(0 \le t\), the growth rate of Definition 9.53 equals the descended flow exponent \(\operatorname {flowExponentAt}\) (Definition 9.16).

The general non-constant roof is out of scope and disclosed: the orbit quotient has no measurable canonical representative there, so only the exponent, not the matrix cocycle, descends.

9.6.1 The cat-map instance

Definition 9.56 The cat map’s quotient flow cocycle

Instantiating Definition 9.53 at the Arnold cat map Definition 13.21 under the constant unit roof, with base generator the cat map’s own derivative cocycle (the constant hyperbolic matrix \(\operatorname {cat}_{\mathbb {R}}\)), yields a genuine Definition 8.3 on the cat suspension.

Theorem 9.57 The cat quotient flow-cocycle Lyapunov exponent

For \(\hat\mu \)-a.e. orbit class \(q\), the growth rate of Definition 9.56 converges to the flow Lyapunov exponent \(\log \! \big((3+\sqrt5)/2\big)\) — the log of the cat matrix’s top eigenvalue.

Proof

Chain the descended cat-suspension exponent (Theorem 9.22) through the exponent-transport Theorem 9.55.

9.7 The Bowen–Walters metric on the suspension

The measure theory above never needed a metric on the quotient \(\Sigma \); a genuine Bowen–Walters metric (R. Bowen and P. Walters, Expansive one-parameter flows, J. Diff. Eq. 12 (1972) 180–193; Barreira–Saussol, Comm. Math. Phys. 214 (2000); Barreira–Radu–Wolf, Dyn. Syst. 19 (2004) §2.1) is, however, the substrate on which the Hölder-regularity Livšic theory of the next chapter is measured, and on which the flow acts by essentially isometric time translations. Issue #63 builds it in two stages — a constant-roof-\(1\) metric, then a variable-roof one — and, notably, does not take the naive finite-route gauge as the metric, because that gauge provably fails the triangle inequality.

A horizontal segment joining \((x, t)\) and \((y, t)\) at common height \(t\in [0,1)\) has the height-interpolated length \(\operatorname {hlen} t\, x\, y = (1-t)\, d(x, y) + t\, d(Tx, Ty)\) (), matching the seam gluing \((x, 1)\sim (Tx, 0)\); a vertical segment moves along the flow at unit speed. The classical chain-infimum distance is bi-Lipschitz, on the canonical fundamental-domain representatives, to the minimum of five explicit routes (direct, low, high, up-wrap, down-wrap), packaged as the route gauge \(\operatorname {routeDist}\) ().

Proposition 9.58 The route gauge is not a metric
#

The low and high routes are essential: a naive minimum of only the direct and two wrap routes provably fails the triangle inequality (when \(T\) strongly contracts a pair, the cheap path climbs both fibres to the seam and traverses at cost \(d(Tx, Ty)\) without crossing it). Even the full five-route minimum \(\operatorname {routeDist}\) is only bi-Lipschitz to, not equal to, the chain-infimum distance, so it is a gauge, not a metric — a documented counterexample rules out the triangle inequality. The genuine metric is built by embedding instead.

Definition 9.59 The Bowen–Walters embedding metric
#

Under \(\operatorname {diam} X \le 1\) the Kuratowski embedding \(\operatorname {kur} a = d(a, \cdot )\) () isometrically embeds \(X\) into the bounded continuous functions \(X \to ^{b} \mathbb {R}\). Two test bundles \(\operatorname {muFun}\), \(\operatorname {nuFun}\) (, ) interpolate the Kuratowski images of \(x\) and \(Tx\) with two distinct height weightings, and \(\operatorname {hgt}\) () measures the vertical \(\mathbb {R}/\mathbb {Z}\) coordinate. Evaluated at the canonical fundamental-domain representatives, the sum

\[ \operatorname {embDist}(p, q) = d\bigl(\operatorname {muFun} p, \operatorname {muFun} q\bigr) + d\bigl(\operatorname {nuFun} p, \operatorname {nuFun} q\bigr) + \operatorname {hgt}(p_2, q_2) \]

is the embedding metric \(\operatorname {embDist}\) on the constant-roof-\(1\) suspension space.

Theorem 9.60 \(\operatorname {embDist}\) is a metric

\(\operatorname {embDist}\) satisfies the triangle inequality and separates points (): the two test parts descend from the sup-norm triangle inequality of \(X \to ^{b} \mathbb {R}\), the height part from the \(\mathbb {R}/\mathbb {Z}\) quotient metric, and a \(2\times 2\) linear solve on the two weightings recovers the base point from a vanishing distance. It is bi-Lipschitz to the route gauge \(\operatorname {routeDist}\).

Proof

The Kuratowski map is an isometry into \(X \to ^{b} \mathbb {R}\), so both test distances are genuine metrics; the height gauge \(\operatorname {hgt}\) is the standard circle metric. Their sum inherits symmetry, the triangle inequality and nonnegativity; zero distance forces equal heights (height part) and, at the common height, equal Kuratowski images through the two weightings (test parts), hence \(x = y\).

Theorem 9.61 Metric-space topology and Polishness

For a compact metric base \(X\) with \(\operatorname {diam} X\le 1\) and a homeomorphism \(T\), the \(\operatorname {embDist}\) metric induces exactly the quotient topology (, via \(\texttt{MetricSpace.ofDistTopology}\)), under which the suspension space is compact, complete and separable — hence Polish.

Proof

The metric topology agrees with the quotient topology (an open-ball criterion), so \(\texttt{MetricSpace.ofDistTopology}\) packages \(\operatorname {embDist}\) into a genuine MetricSpace on \(\Sigma \). Compactness of \(\Sigma \) (a continuous image of \(X\times [0,1]\)) plus completeness of a compact metric space and second-countability give Polishness.

Theorem 9.62 The flow is Lipschitz in time

The suspension flow is \(5\)-Lipschitz in the time parameter along each orbit: \(\operatorname {embDist}(\zeta _a q, \zeta _b q)\le 5\, \left\lvert a - b \right\rvert \).

Proof

Both flowed points share the base coordinate of the canonical representative; the height advances by \(a - b\), so the height gauge contributes \(\le \left\lvert a-b \right\rvert \) and each test bundle at most twice that, totalling the \(5\left\lvert a-b \right\rvert \) bound (with the seam-wrap regime handled by the vertical/step estimates).

9.7.1 The variable-roof metric

The construction generalises to a roof \(\tau \) bounded below by \(\rho _{\min } {\gt} 0\) by rescaling each fibre to the unit circle before comparison: the normalized height \(u = s/\tau x\in [0,1)\) runs over \([0,1)\) on every fibre regardless of \(\tau \), so the seam gluing \((x, \tau x)\sim (Tx, 0)\) becomes roof-independent and the constant-roof Kuratowski bundles are reused verbatim on the normalized coordinate.

Definition 9.63 The variable-roof embedding metric
#

For a roof \(\tau \ge \rho _{\min } {\gt} 0\), the canonical box representative \(\operatorname {suspensionRepVar}\) () is the unique orbit representative in \(\{ (x,s) : 0\le s {\lt} \tau x\} \) (the roof-cocycle is strictly increasing with gaps \(\ge \rho _{\min }\), so it partitions \(\mathbb {R}\)), and \(\operatorname {normHeightVar}\) () is its normalized height \(s/\tau x\). The metric \(\operatorname {embDistVar}\) is the constant-roof sum evaluated at the normalized representatives; it is a genuine metric ().

Theorem 9.64 Variable-roof flow-Lipschitz bound

The realisation cost of the variable roof appears only in the flow-Lipschitz constant: the flow moves the raw height at unit speed, hence the normalized height at speed \(1/\tau \le 1/\rho _{\min }\), giving \(\operatorname {embDistVar}(\zeta _a q, \zeta _b q)\le (5/\rho _{\min })\, \left\lvert a - b \right\rvert \).

Proof

Repeat the constant-roof estimate Theorem 9.62 on the normalized coordinate, where the time increment \(a - b\) is scaled by \(1/\tau x\le 1/\rho _{\min }\) before entering the height and test gauges.

Route \(\beta \) is a wall. Rescaling a variable roof to a constant roof (a time change) is bi-Lipschitz only when \(\tau \) is cohomologous to a constant, \(\tau = c + \varphi \circ T - \varphi \) — precisely the hypothesis one wants to avoid — so the metric is built directly on the normalized fibre coordinate, never by reduction to the constant-roof case.

9.8 Functoriality of the suspension on factor maps

The unit-roof suspension is not only a construction but a functor: a factor map between two base automorphisms lifts to a factor map of their suspension flows. This is the constant-roof (\(\tau \equiv \sigma \equiv 1\)) case of the Ambrose–Kakutani functoriality (W. Ambrose and S. Kakutani, Structure and continuity of measurable flows, Duke Math. J. 9 (1942), 25–42), and it is the engine of the symbolic flow tower of issue #58 (Section 13.8).

Definition 9.65 The descended suspension factor map
#

For measurable automorphisms \(T : X\simeq X\), \(S : Y\simeq Y\) with unit roofs and a base factor map \(\pi : X\to Y\) (measurable, \(\pi \circ T = S\circ \pi \)), the fibrewise raw map \((x,s)\mapsto (\pi x, s)\) on \(X\times \mathbb {R}\) descends through the two orbit quotients to \(\operatorname {suspensionFactorMap} : \widehat X\to \widehat Y\), \([x,s]\mapsto [\pi x, s]\).

Theorem 9.66 The suspension factor package

\(\operatorname {suspensionFactorMap}\) intertwines the two suspension flows () and pushes the invariant measure of the source suspension to that of the target (), so it is measure preserving; packaged at time \(1\) it is an \(\operatorname {Entropy.IsFactorMap}\) of the time-\(1\) flow maps. When the base map \(\pi \) is injective, so is the lift (), giving a conjugacy stage of the tower.

Proof

The base semiconjugacy \(\pi \circ T = S\circ \pi \) makes the raw fibre map intertwine the two orbit generators, so it descends; the unit-roof equalities \(\tau x = 1 = \sigma (\pi x)\) keep the time coordinate fixed, giving the flow intertwining. Measure transport follows from the product measure \(\mu \times \text{(Lebesgue)}\) on the fundamental domain, and injectivity transports fibrewise from \(\pi \).