The Guarded Real-Liminf Bridge to Log-Positive Kingman Convergence

Start with three sequences you can calculate by hand

Before filters, null sets, or cocycles enter, write down three exact rational sequences. They isolate three logically different questions that are often conflated.

The guarded sequence: the rational event and liminf agree

Define

Take the event target \(c=-1\) and the rational witness \(q=-5/4\). The first eleven values are

Every odd time is a witness beyond any proposed cutoff, so \(u_n\lt q\) occurs frequently. At the same time,

for every \(n\). The eventual-lower-bound guard is therefore present, and the ordinary answer is informative:

At the strict boundary \(c=-3/2\), however, there is no rational \(q\lt c\) crossed frequently: the sequence never goes below \(-3/2\). Equality with the liminf does not enter a strict lower-deviation event.

The strictness near-miss: crossing the target is not enough

Now take

Every positive term satisfies \(a_n\lt0\), but for the sample margin \(q=-1/4\), the strict inequality \(a_n\lt q\) holds only at \(n=1,2,3\); equality at \(n=4\) does not count. The same phenomenon holds for every fixed rational \(q\lt0\): eventually \(q\lt a_n\lt0\). Thus

This is why the event stores a durable rational margin below the target, not just arbitrarily late strict crossings of the target itself.

The guard near-miss: a real totalization can hide escape to \(-\infty\)

The project source uses the genuine subadditive process \(X_n=-n^2\) on the one-point probability space. After subtracting its one-step orbit sum and normalizing, its exact values are

At target \(c=-1\), choose \(q=-2\). Then \(q\lt c\) and \(e_n\lt q\) for every \(n\ge4\), so the rational lower-deviation event really occurs. But no real number lies below all sufficiently late values. For example, the candidate bound \(-10\) survives through \(n=11\), where \(e_{11}=-10\), and fails at \(n=12\), where \(e_{12}=-11\). Every other finite candidate fails in the same way.

The defining set of eventual real lower bounds is empty. In the pinned real-order implementation, its supremum is totalized:

Consequently the unguarded implication

would demand the false statement \(0\lt-1\). This is not a hypothetical arbitrary-sequence objection: the paired Lean module checks the subadditive candidate, event membership, absence of the guard, and totalized value.

A finite squeeze that says exactly what the final theorem says

For a second hand-check, set

and let \(s_k\) alternate between the upper and lower rails. Then

so \(s_k\to\gamma_+\). This is a finite-arithmetic picture of the final proof architecture, with one essential provenance label on each rail:

• this module supplies the lower rail \(\gamma_+\le\liminf a_n(\omega)\);
• the earlier RMT-29 module supplies the upper rail \(\limsup a_n(\omega)\le\gamma_+\); and
• actual lower and upper boundedness let Mathlib turn those two inequalities into convergence.

The conclusion concerns

It does not manufacture a signed logarithm. The nearby zero-rate sequence \(1/k\to0\) is a faithful endpoint: \(\gamma_+\) can be zero, while a constant contraction can simultaneously have a negative signed rate that the log-positive observable erases.

The actual paired-source zero probe is even simpler: its normalized process is identically zero, its real liminf is zero, and its strict lower-liminf deviation set at target zero is empty. The \(1/k\) row is only a visual model of approaching the same permitted endpoint; it is not being attributed to that source probe.

The last step of a long proof is often described as a squeeze:

That line is correct for the endpoint of RMT-33, but it hides the hardest formal question. What does the middle real limit inferior (liminf) mean when the codomain is only conditionally complete? Mathlib gives it a value for every real sequence, even one that escapes to negative infinity. In such a case the set of eventual real lower bounds is empty, and its real supremum is totalized to zero. A naked inequality involving that value can therefore say something very different from the intended extended asymptotic statement.

RMT-33 solves the problem constructively. It does not merely show that the bad lower-liminf set is null. Off a related countable rational null set, it extracts one fixed rational number below all sufficiently late normalized centered values. That witness certifies that the real lower limit is being used in its standard bounded-below regime.

The proof then adds back a convergent one-step Birkhoff average, identifies the centered offset with the integrated Fekete rate, and combines the lower estimate with the upper-limsup theorem from RMT-29. The result is the project’s first almost-everywhere Kingman-style convergence theorem:

The subscript \(+\) is essential. The limit sees expansion above norm one and forgets contraction below norm one.

This chapter continues Rational-Slack Lower-Deviation Events and Ergodic Null Selection and Subadditive Upper-Limsup Bounds Before Kingman Convergence. The deterministic rate was constructed in Integrated Log-Positive Cocycle Growth and the Fekete Limit.

Choose a route up

Common setup and notation

Let \((\Omega,\mu)\) be a probability space and let \(T:\Omega\to\Omega\) preserve \(\mu\). A real process \(X=(X_n)_{n\in\mathbb N}\) is shifted-subadditive in the convention used by the repository when

for all natural \(m,n\) and all \(\omega\). Every slice \(X_n\) is assumed integrable.

The one-step orbit sum is

The centered process is

Centering is pointwise and dynamical. It subtracts an orbit sum, not an expectation. At every positive horizon, the one-step majorant inherited from subadditivity gives

After total normalization, \(u_0=0\), so \(u_n\le0\) holds at every natural time even when the unnormalized generic value \(Y_0\) is not assumed nonpositive.

Lean packages total normalization as

At \(n=0\), real division is total and returns zero. Thus the normalized process is defined at every natural time even when \(X_0\) is arbitrary. For positive time this is ordinary division, and removing the zero term does not change either lower or upper asymptotics along natural infinity.

Write

With the total convention at time zero, the exact identity is

for every \(n\in\mathbb N\), including zero.

For the matrix-cocycle specialization, let \(C_n(\omega)\) be the ordered finite product and set

The deterministic integrated sequence is

and its Fekete rate is

The equality with the positive-horizon infimum is already checked in the repository. RMT-33 proves that the samplewise normalized process converges to that same real number almost everywhere.

See the whole summit route

The proof has five bridges. Each one changes the language of the statement.

1. A bad block becomes a frequent inequality along the filter at natural infinity.
2. A strict real lower-liminf deviation enters a countable union of rational bad events.
3. Nullity of that union supplies both a lower-liminf inequality and an eventual lower bound.
4. The centered estimate is added to a convergent Birkhoff average.
5. A prior upper-limsup estimate and explicit boundedness close the convergence squeeze.

The central design choice is visible at stage three. A theorem that returned only

would be numerically useful but semantically incomplete. RMT-33 returns the conjunction

That stronger interface prevents later proofs from silently treating a totalized real lower limit as an extended-real one.

Why real liminf needs a guard

Mathlib’s real lower limit

For a real sequence \(a:\mathbb N\to\mathbb R\), the pinned Mathlib definition can be read as

The word eventually means that there is some cutoff after which the inequality always holds. The set inside the supremum is the set of eventual real lower bounds.

The real numbers are conditionally complete, not complete as an order. If the sequence has no eventual lower bound, that set is empty. Mathlib nevertheless keeps liminf total. In the pinned release, Real.sSup_empty states

Consequently, the formal real lower limit of an unbounded-below sequence can be zero.

A checked countermodel

The module uses the process

on the one-point probability space. It is subadditive because

Its centered process is

so for positive \(n\),

This sequence crosses every fixed negative slope eventually and has no eventual real lower bound. The intended extended lower limit is negative infinity. Yet the set of eventual real lower bounds is empty, so Mathlib’s total real liminf is zero.

The countermodel refutes the statement with the lower-boundedness guard removed. Without it, membership in a rational strict lower-deviation event need not force the total real lower limit below the event target.

Read the guard in filter language

The Lean proposition

IsBoundedUnder (· ≥ ·) atTop a

means that \(a_n\) is eventually bounded below. Explicitly, there exists \(b\in\mathbb R\) such that

for every sufficiently large \(n\).

The orientation may appear reversed because the relation is written \((\cdot\ge\cdot)\). The reliable reading is to expand the definition and ask which side of \(a_n\) receives the witness. In this case the witness lies below the eventual values.

The companion proposition

IsBoundedUnder (· ≤ ·) atTop a

means eventual upper boundedness.

Time zero is not the problem

At time zero,

under Lean’s total division. This convention does not contaminate asymptotic limits. The theorem liminf_nat_add removes a finite natural prefix, and RMT-33 exposes the specialized equality

The theorem normalizedProcess_update_zero goes farther: replacing the entire time-zero slice by any function leaves every normalized value unchanged. The genuine semantic hazard is unbounded escape at late times, not division at the first index.

Translate arbitrarily late blocks into frequency

RMT-32 defined an arbitrarily-late centered bad-block event at slope \(q\):

On natural time, a property \(P(n)\) holds frequently along atTop exactly when

Positive witnesses make division legitimate, so RMT-33 proves the exact translation

The symbol on the right means frequently along natural infinity. It does not mean eventually always.

The rationally generated strict event at a real target \(c\) is

Its membership theorem becomes

This says that one durable rational margin below \(c\) is crossed arbitrarily late.

The guarded equivalence

Suppose \(u(\omega)\) is eventually bounded below. If \(\omega\in D_c\), then some rational \(q\lt c\) is crossed frequently. The Mathlib theorem liminf_le_of_frequently_le yields

Conversely, suppose

Choose a rational \(q\) strictly between the lower limit and \(c\). Since the normalized centered sequence is pointwise nonpositive, it has the coboundedness gate needed by frequently_lt_of_liminf_lt. That theorem gives frequent crossings below \(q\), hence membership in \(D_c\).

Therefore, under the explicit eventual-lower-bound guard,

The two directions use different order hypotheses:

For the centered candidate, pointwise nonpositivity supplies the second gate. The first gate must be constructed almost everywhere.

Why one rational margin is not enough

Consider

It converges to zero and is strictly negative at every positive time. Thus

However, for every fixed rational \(q\lt0\), the sequence is eventually above \(q\). Hence

Strict crossings at the target do not provide a durable strict gap below the target. This is why the event is generated by rational slopes below \(c\), not by the slope \(c\) itself.

The checked module includes formal proofs of the three properties exhibited by this example:

That triple is the smallest counterexample to the tempting same-threshold shortcut.

Spend two rational margins

Let

and fix a desired lower bound \(\delta\). We want to cover the exceptional set

by RMT-32 events known to be null.

RMT-32 proves nullity of \(D_c\) when its event target \(c\) is strictly below a deterministic lower bound \(\delta\) for all positive normalized centered integrals. It cannot be invoked with \(c=\delta\), because that would require the false hypothesis \(\delta\lt\delta\).

The repair uses two rational margins.

1. If \(L(\omega)\lt\delta\), choose an outer target \(c\in\mathbb Q\) with

   \[ L(\omega)\lt c\lt\delta. \]

2. To prove \(\omega\in D_c\), choose an inner witness slope \(q\in\mathbb Q\) with

   \[ L(\omega)\lt q\lt c. \]

The outer target makes RMT-32 applicable because \(c\lt\delta\). The inner slope supplies the durable strict margin required by membership in \(D_c\). The two numbers have different logical jobs and cannot safely be identified.

The outer exhaustion is the countable set

The two-margin argument proves

Since the rational numbers are countable, RMT-32 nullity of every \(D_c\) implies \(\mu(R_\delta)=0\), and monotonicity gives \(\mu(E_\delta)=0\).

Make one null cover do two jobs

The exhaustion \(R_\delta\) supports two distinct conclusions.

Deliverable one: the lower-liminf inequality

Because \(E_\delta\subseteq R_\delta\) and \(R_\delta\) is null,

for almost every \(\omega\).

This is the numerical conclusion needed for the final squeeze.

Deliverable two: an actual eventual lower bound

Take \(\omega\notin R_\delta\). Choose rationals

Since \(\omega\notin D_c\), it cannot cross \(q\) frequently. The negation of frequency along atTop is eventual negation, so

for all sufficiently large \(n\). Thus \(q\) is a concrete eventual lower bound.

Notice that this construction does not infer boundedness from the numerical real-liminf inequality. It builds boundedness directly from the complement of the rational event. That direction is robust against totalization.

The generic centered endpoint is therefore

This is the correctly scoped lower half of the theorem.

Where the hypotheses enter

Suppose that for every positive \(n\),

Then each outer event \(D_c\) with \(c\lt\delta\) is null by RMT-32. That earlier theorem uses integrability, shifted subadditivity, a measure-preserving ergodic probability base, and the strict separation \(c\lt\delta\). RMT-33 adds no independence assumption.

Add back the Birkhoff average

The exact normalized decomposition is

where

On an ergodic probability base, the project’s pointwise Birkhoff theorem gives

for almost every \(\omega\).

For such a sample:

• \(u_n\) is eventually bounded below by the null-cover construction;
• \(u_n\le0\) pointwise by centering;
• \(v_n\) is eventually bounded below and above because it converges;
• convergence also gives the coboundedness condition required by the liminf-of-sum theorem.

The pinned Mathlib theorem le_liminf_add then yields

Since \(v_n\) converges,

Combining this equality with the centered lower estimate gives

This step explains why the proof centered by the one-step orbit sum rather than by a constant expectation. The orbit sum produces both pointwise nonpositivity of \(Y_n\) and an exact additive component governed by Birkhoff.

Specialize the centered offset to the Fekete rate

For the log-positive cocycle process, set

The deterministic rate \(\gamma_+\) lies below every positive-horizon normalized integral:

The centered integral satisfies

Therefore

for every positive \(n\). Choose

The generic transfer theorem gives

After cancellation,

almost everywhere.

This cancellation is why the centered Fekete offset appears throughout RMT-30 to RMT-33. It is not an additional rate. It is exactly the original rate expressed in centered coordinates.

Close the log-positive squeeze

RMT-29 already proved

almost everywhere. Intersect its full-measure set with the RMT-33 lower set and the full-measure set on which the one-step Birkhoff average converges.

The pointwise normalized log-positive process is nonnegative:

This supplies an eventual lower bound. The one-step orbit majorant gives, for positive \(n\),

The right side converges, so it is eventually bounded above. Hence the normalized process is eventually bounded above as well.

Now the pinned theorem tendsto_of_le_liminf_of_limsup_le applies:

together with explicit eventual upper and lower bounds, imply

The checked endpoint is:

No independent or identically distributed hypothesis appears. Dependence is organized by a deterministic measure-preserving base transformation and the cocycle law.

Separate log-positive growth from signed growth

The positive logarithm is

It has three behaviors that matter here:

In Mathlib, \(\log^+0=0\). Thus the observable records expansion above one and erases contraction and singular collapse.

By contrast, a signed logarithmic growth theorem studies

usually in an extended-real setting because the norm can vanish. Ruelle’s 1979 matrix-product corollary permits a limit in \(\mathbb R\cup\{-\infty\}\). RMT-33 does not.

Constant contraction test

Let

Then the signed normalized growth is

But

at every positive time. RMT-33 returns \(\gamma_+=0\), not \(\log a\).

Zero-product test

If a finite product is the zero matrix, its signed logarithm naturally points to negative infinity. The log-positive observable is instead zero. It carries no record of the collapse.

The phrase log-positive Kingman endpoint is therefore a scope label. It says that the proof architecture is subadditive and Kingman-style while the observable is the nonnegative envelope chosen by this project.

Seven bridges from the sequence ledger to Lean

Each bridge below has four layers: the sentence a mathematician says, the paper formula, the exact checked Lean interface, and a token map. Read them in order once; afterward the declaration names become a compact proof roadmap. The literal full project command appears after bridge seven.

Bridge 1: normalize at every natural time

normalizedProcess X n ω

Bridge 2: expose the durable rational witness

mem_centeredStrictLowerDeviationSet_iff_exists_frequently_normalized_lt

Bridge 3: pass from the event to liminf only through the guard

liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet hlower hω

Bridge 4: spend an outer rational target as well as an inner witness

hX.centeredLowerLiminfDeviationSet_subset_rationalExhaustion δ

Bridge 5: make the null cover return two deliverables

hX.ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess hT δ hδ

Bridge 6: add back the convergent Birkhoff average

hX.ae_add_oneStepIntegral_le_liminf_normalized hT δ hδ

Bridge 7: squeeze the nonnegative log-positive observable

hC.ae_tendsto_normalizedLogPlusNormObservable hT

Type-check the exact project interface

import NonlinearDynamics.Random.RandomCocycles.SubadditiveKingman

open MeasureTheory Set Filter Topology
open NonlinearDynamics.Random.RandomCocycles

#check normalizedProcess
#check normalizedProcess_zero
#check normalizedProcess_update_zero
#check liminf_normalizedProcess_succ
#check mem_centeredStrictLowerDeviationSet_iff_exists_frequently_normalized_lt
#check liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet
#check IsIntegrableSubadditiveProcessCandidate.mem_centeredStrictLowerDeviationSet_iff_liminf_normalizedCenteredProcess_lt
#check IsIntegrableSubadditiveProcessCandidate.centeredLowerLiminfDeviationSet_subset_rationalExhaustion
#check IsIntegrableSubadditiveProcessCandidate.ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess
#check IsIntegrableSubadditiveProcessCandidate.ae_add_oneStepIntegral_le_liminf_normalized
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_integratedLogPlusGrowthRate_le_liminf_normalized
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_tendsto_normalizedLogPlusNormObservable

cd formalization
lake env lean NonlinearDynamics/Random/RandomCocycles/SubadditiveKingman.lean

cd formalization
lake env lean -DwarningAsError=true NonlinearDynamics/Random/RandomCocycles/SubadditiveKingman.lean

Run the exact finite ledger with Lean and Std

The project theorem needs Mathlib’s filters, measures, liminf, Birkhoff theorem, and cocycle hierarchy. Its numerical spine can be explored without building any of that. The following standalone worksheet imports only Lean’s Std library and uses exact rationals throughout.

Save this block byte for byte as /tmp/GuardedRealLiminfTutorial.lean:

import Std

namespace GuardedRealLiminfTutorial

structure SequenceRow where
  n : Nat
  value : Rat
  belowInnerQ : Bool
  deriving Repr, DecidableEq

def boundedAlternation (n : Nat) : Rat :=
  if n = 0 then 0
  else if n % 2 = 1 then (-3 : Rat) / 2
  else (-1 : Rat) / 2

def boundedRows : List SequenceRow :=
  (List.range 11).map fun n =>
    { n := n
      value := boundedAlternation n
      belowInnerQ := decide (boundedAlternation n < (-5 : Rat) / 4) }

def approachZero (n : Nat) : Rat :=
  if n = 0 then 0 else (-1 : Rat) / n

def approachRows : List SequenceRow :=
  (List.range 9).map fun n =>
    { n := n
      value := approachZero n
      belowInnerQ := decide (approachZero n < (-1 : Rat) / 4) }

def quadraticEscapeNormalized (n : Nat) : Rat :=
  if n = 0 then 0 else 1 - n

def escapeRows : List SequenceRow :=
  (List.range 9).map fun n =>
    { n := n
      value := quadraticEscapeNormalized n
      belowInnerQ := decide (quadraticEscapeNormalized n < (-2 : Rat)) }

structure EscapeBoundary where
  target : Rat
  innerQ : Rat
  innerBelowTarget : Bool
  bound : Rat
  boundHoldsThrough : Nat
  valueThere : Rat
  firstDisplayedFailure : Nat
  valueAtFailure : Rat
  boundFailsThere : Bool
  sourceProvedTotalizedRealLiminf : Rat
  unguardedConclusion : Bool
  deriving Repr, DecidableEq

def escapeBoundary : EscapeBoundary :=
  { target := -1
    innerQ := -2
    innerBelowTarget := decide ((-2 : Rat) < -1)
    bound := -10
    boundHoldsThrough := 11
    valueThere := quadraticEscapeNormalized 11
    firstDisplayedFailure := 12
    valueAtFailure := quadraticEscapeNormalized 12
    boundFailsThere := decide (quadraticEscapeNormalized 12 < (-10 : Rat))
    sourceProvedTotalizedRealLiminf := 0
    unguardedConclusion := decide ((0 : Rat) < -1) }

structure SqueezeRow where
  k : Nat
  lowerRail : Rat
  sample : Rat
  upperRail : Rat
  width : Rat
  insideRails : Bool
  deriving Repr, DecidableEq

def gamma : Rat := 3 / 2

def lowerRail (k : Nat) : Rat := gamma - 1 / k

def upperRail (k : Nat) : Rat := gamma + 1 / k

def squeezedSample (k : Nat) : Rat :=
  if k % 2 = 0 then lowerRail k else upperRail k

def squeezeRow (k : Nat) : SqueezeRow :=
  { k := k
    lowerRail := lowerRail k
    sample := squeezedSample k
    upperRail := upperRail k
    width := upperRail k - lowerRail k
    insideRails := decide
      (lowerRail k ≤ squeezedSample k ∧ squeezedSample k ≤ upperRail k) }

def squeezeRows : List SqueezeRow :=
  (List.range 8).map fun n => squeezeRow (n + 1)

def zeroRateRows : List (Nat × Rat) :=
  (List.range 6).map fun n =>
    let k := n + 1
    (k, 1 / (k : Rat))

#eval boundedRows
#eval approachRows
#eval escapeRows
#eval escapeBoundary
#eval squeezeRows
#eval zeroRateRows

example : boundedAlternation 0 = 0 := by native_decide
example : boundedAlternation 9 = (-3 : Rat) / 2 := by native_decide
example : boundedAlternation 10 = (-1 : Rat) / 2 := by native_decide
example : (List.range 11).all fun n =>
    decide ((-3 : Rat) / 2 ≤ boundedAlternation n ∧
      boundedAlternation n ≤ 0) := by native_decide
example : (List.range 5).all fun j =>
    decide (boundedAlternation (2 * j + 1) < (-5 : Rat) / 4) := by
  native_decide
example : (List.range 11).all fun n =>
    decide (¬ boundedAlternation n < (-3 : Rat) / 2) := by native_decide

example : (List.range 8).all fun n =>
    decide (approachZero (n + 1) < 0) := by native_decide
example : (List.range 5).all fun n =>
    decide (¬ approachZero (n + 4) < (-1 : Rat) / 4) := by
  native_decide

example : quadraticEscapeNormalized 11 = -10 := by native_decide
example : quadraticEscapeNormalized 12 = -11 := by native_decide
example : (List.range 5).all fun j =>
    decide (quadraticEscapeNormalized (j + 4) < (-2 : Rat)) := by
  native_decide
example : escapeBoundary.unguardedConclusion = false := by native_decide

example : (List.range 8).all fun n =>
    (squeezeRow (n + 1)).insideRails := by native_decide
example : (List.range 8).all fun n =>
    decide ((squeezeRow (n + 1)).width = 2 / ((n + 1 : Nat) : Rat)) := by
  native_decide
example : (List.range 6).all fun n =>
    decide (0 < (zeroRateRows[n]!).2) := by native_decide

end GuardedRealLiminfTutorial

Open a terminal and type:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean \
  /tmp/GuardedRealLiminfTutorial.lean

Standalone tutorial: Lean 4.32.0 plus Std, suitable for an ordinary macOS or Linux host. This exact file ran in 3.4 seconds and printed the following complete transcript:

[{ n := 0, value := 0, belowInnerQ := false },
 { n := 1, value := (-3 : Rat)/2, belowInnerQ := true },
 { n := 2, value := (-1 : Rat)/2, belowInnerQ := false },
 { n := 3, value := (-3 : Rat)/2, belowInnerQ := true },
 { n := 4, value := (-1 : Rat)/2, belowInnerQ := false },
 { n := 5, value := (-3 : Rat)/2, belowInnerQ := true },
 { n := 6, value := (-1 : Rat)/2, belowInnerQ := false },
 { n := 7, value := (-3 : Rat)/2, belowInnerQ := true },
 { n := 8, value := (-1 : Rat)/2, belowInnerQ := false },
 { n := 9, value := (-3 : Rat)/2, belowInnerQ := true },
 { n := 10, value := (-1 : Rat)/2, belowInnerQ := false }]
[{ n := 0, value := 0, belowInnerQ := false },
 { n := 1, value := -1, belowInnerQ := true },
 { n := 2, value := (-1 : Rat)/2, belowInnerQ := true },
 { n := 3, value := (-1 : Rat)/3, belowInnerQ := true },
 { n := 4, value := (-1 : Rat)/4, belowInnerQ := false },
 { n := 5, value := (-1 : Rat)/5, belowInnerQ := false },
 { n := 6, value := (-1 : Rat)/6, belowInnerQ := false },
 { n := 7, value := (-1 : Rat)/7, belowInnerQ := false },
 { n := 8, value := (-1 : Rat)/8, belowInnerQ := false }]
[{ n := 0, value := 0, belowInnerQ := false },
 { n := 1, value := 0, belowInnerQ := false },
 { n := 2, value := -1, belowInnerQ := false },
 { n := 3, value := -2, belowInnerQ := false },
 { n := 4, value := -3, belowInnerQ := true },
 { n := 5, value := -4, belowInnerQ := true },
 { n := 6, value := -5, belowInnerQ := true },
 { n := 7, value := -6, belowInnerQ := true },
 { n := 8, value := -7, belowInnerQ := true }]
{ target := -1,
  innerQ := -2,
  innerBelowTarget := true,
  bound := -10,
  boundHoldsThrough := 11,
  valueThere := -10,
  firstDisplayedFailure := 12,
  valueAtFailure := -11,
  boundFailsThere := true,
  sourceProvedTotalizedRealLiminf := 0,
  unguardedConclusion := false }
[{ k := 1, lowerRail := (1 : Rat)/2, sample := (5 : Rat)/2, upperRail := (5 : Rat)/2, width := 2, insideRails := true },
 { k := 2, lowerRail := 1, sample := 1, upperRail := 2, width := 1, insideRails := true },
 { k := 3,
   lowerRail := (7 : Rat)/6,
   sample := (11 : Rat)/6,
   upperRail := (11 : Rat)/6,
   width := (2 : Rat)/3,
   insideRails := true },
 { k := 4,
   lowerRail := (5 : Rat)/4,
   sample := (5 : Rat)/4,
   upperRail := (7 : Rat)/4,
   width := (1 : Rat)/2,
   insideRails := true },
 { k := 5,
   lowerRail := (13 : Rat)/10,
   sample := (17 : Rat)/10,
   upperRail := (17 : Rat)/10,
   width := (2 : Rat)/5,
   insideRails := true },
 { k := 6,
   lowerRail := (4 : Rat)/3,
   sample := (4 : Rat)/3,
   upperRail := (5 : Rat)/3,
   width := (1 : Rat)/3,
   insideRails := true },
 { k := 7,
   lowerRail := (19 : Rat)/14,
   sample := (23 : Rat)/14,
   upperRail := (23 : Rat)/14,
   width := (2 : Rat)/7,
   insideRails := true },
 { k := 8,
   lowerRail := (11 : Rat)/8,
   sample := (11 : Rat)/8,
   upperRail := (13 : Rat)/8,
   width := (1 : Rat)/4,
   insideRails := true }]
[(1, 1), (2, (1 : Rat)/2), (3, (1 : Rat)/3), (4, (1 : Rat)/4), (5, (1 : Rat)/5), (6, (1 : Rat)/6)]

Read the output as four separate ledgers:

1. the alternating sequence repeatedly crosses \(-5/4\) and remains between \(-3/2\) and zero;
2. \(-1/n\) is negative at every displayed positive time but stops strictly crossing \(-1/4\) at equality \(n=4\);
3. \(1-n\) keeps crossing \(-2\), defeats the displayed lower bound one step after equality, and makes the proposed unguarded conclusion false; and
4. the exact squeeze rows lie between their two rails with width \(2/k\), while the positive zero-rate rows \(1/k\) approach the allowed endpoint zero.

The example declarations kernel-check every recorded finite identity and Boolean window. The field sourceProvedTotalizedRealLiminf := 0 is an explicit reference to the paired Mathlib proof, not a reimplementation of liminf in Std. The infinite frequency, eventual boundedness, totalized real-liminf, null-set, Birkhoff, and cocycle claims remain exactly the full project interfaces above.

Audit every checked interface

RMT-33 declaration ledger

The private helper ae_isBoundedUnder_ge_normalizedCenteredProcess is intentionally not public. Its content is exposed through the stronger public conjunction theorem.

Complete paired-source manifest

The authoritative paired file is formalization/NonlinearDynamics/Random/RandomCocycles/SubadditiveKingman.lean. At this chapter revision it has 627 lines and SHA-256 digest 55680bc2afa18d0a195a7fa7426e6afb2b55fcbb3f588d3474bc6f52764025ef. It imports exactly:

1. NonlinearDynamics.Random.RandomCocycles.SubadditiveLowerDeviation; and
2. NonlinearDynamics.Random.RandomCocycles.SubadditiveUpperLimsup.

The 24 public declarations appear in source order in the ledger above. The remaining named private surface is complete in the following table.

Five anonymous example probes then test the public boundary:

Finally, the source contains exactly 11 explicit axiom-audit probes:

#print axioms normalizedProcess_update_zero
#print axioms liminf_normalizedProcess_succ
#print axioms mem_centeredArbitrarilyLateBadBlockSet_iff_frequently_normalized_lt
#print axioms liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet
#print axioms IsIntegrableSubadditiveProcessCandidate.mem_centeredStrictLowerDeviationSet_of_liminf_normalizedCenteredProcess_lt
#print axioms IsIntegrableSubadditiveProcessCandidate.centeredLowerLiminfDeviationSet_subset_rationalExhaustion
#print axioms IsIntegrableSubadditiveProcessCandidate.measure_centeredLowerLiminfDeviationSet_eq_zero
#print axioms IsIntegrableSubadditiveProcessCandidate.ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess
#print axioms IsIntegrableSubadditiveProcessCandidate.ae_add_oneStepIntegral_le_liminf_normalized
#print axioms DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_integratedLogPlusGrowthRate_le_liminf_normalized
#print axioms DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_tendsto_normalizedLogPlusNormObservable

These lines are part of the source manifest, not a substitute for the full project check. Their printed results come from the checked build rather than from text inspection alone.

Pinned Mathlib API ledger

The repository pins Mathlib tag v4.32.0, commit 81a5d257c8e410db227a6665ed08f64fea08e997. These declarations are the exact library interfaces used or audited for the bridge.

Assumption ledger

The final theorem asks for PreErgodic C.base μ, not a bare Ergodic C.base μ, because the cocycle already stores C.base_preserving. The proof constructs

from those two pieces. Pre-ergodicity alone would not be sufficient for an arbitrary map.

Checked nonclaim ledger

RMT-33 does not prove any of the following:

• convergence in \(L^1\);
• convergence in probability as a separately packaged theorem;
• equality obtained by interchanging a samplewise limit and an integral;
• convergence of normalized integrals as a consequence of the samplewise theorem, although the deterministic Fekete convergence was proved earlier;
• convergence of the signed quantity \(n^{-1}\log\lVert C_n(\omega)\rVert\);
• detection of negative growth rates;
• a Lyapunov exponent in the usual signed sense;
• inverse-cocycle integrability or control;
• invertibility or nonzero determinant of the matrices;
• an Oseledets filtration, splitting, or multiplicity theorem;
• independence, identical distribution, or stationarity formulated as a stochastic-process law;
• a rate of convergence, concentration bound, or finite-sample confidence statement;
• a claim that the original 1923 Fekete paper states Mathlib’s modern general subadditive-sequence theorem verbatim;
• the full matrix-product corollary stated by Ruelle in 1979;
• a nondegenerate matrix dimension requirement. The Lean theorem deliberately retains the empty-index boundary.

Boundary audits

Zero process

For \(X_n=0\), centering, normalization, liminf, limsup, and the integrated rate are all zero. The strict lower-liminf deviation set at target zero is empty. This checks strictness at the endpoint.

Arbitrary time-zero replacement

Changing \(X_0\) to any function changes no normalized value because division at zero returns zero. It therefore changes no lower limit and no convergence statement.

Approach zero from below

The sequence \(-1/n\) crosses zero strictly at every positive time but no fixed rational slope below zero frequently. It checks the necessity of durable rational slack.

Quadratic escape

The centered normalized sequence \(1-n\) belongs to strict rational lower-deviation events but has no eventual lower bound. Its formal real liminf is zero because the eventual-lower-bound set is empty. It checks the necessity of the guard.

Empty matrix dimension

When the matrix index type is empty, the operator norm observable is formalized so that every log-positive value is zero. The final theorem still typechecks and yields convergence to zero. This is a Lean boundary guarantee, not a classical theorem’s advertised matrix regime.

Constant expansion and contraction

For \(C_n=a^nI\) with \(a\gt1\), log-positive and signed normalized growth both equal \(\log a\). For \(0\lt a\lt1\), the signed rate is \(\log a\), while the log-positive rate is zero. This pair checks exactly where the two observables agree and separate.

Place the result beside the classical theorems

The historical sources illuminate the architecture, but their statements should not be substituted for the checked Lean theorem.

Kingman 1968

J. F. C. Kingman’s “The Ergodic Theory of Subadditive Stochastic Processes” appeared in volume 30, issue 3 of the Journal of the Royal Statistical Society, Series B, pp. 499 to 510. Section 1 on p. 500 introduces the stationary subadditive setting and the deterministic time constant as an infimum of normalized expectations. Theorem 1 on p. 501 handles an upper asymptotic quantity and mean behavior. Theorem 3 on p. 504 identifies the invariant limit structure, and Theorem 5 on p. 506 gives existence of the almost-sure normalized limit.

RMT-33 shares the subadditive, measure-preserving, ergodic architecture. It does not reproduce all of Kingman’s conclusions, especially mean convergence. The publisher PDF was access-restricted during this audit; exact anchors were checked against a scan, while the publisher landing page confirms the bibliographic record.

Steele 1989

J. Michael Steele’s “Kingman’s subadditive ergodic theorem” gives an accessible compact proof in Annales de l’Institut Henri Poincaré, Probabilités et Statistiques 25(1), pp. 93 to 98. The theorem is stated on pp. 93 to 94. Section 2 centers by a one-step orbit sum on p. 94. The interval-decomposition and bad-set estimates occupy pp. 94 to 96, and equation (2.5) on p. 96 closes the limsup versus liminf argument.

Steele is a useful conceptual map for the project’s RMT-30 through RMT-33 sequence. It is not a line-by-line source for the Lean declarations, whose event encodings and totalized real-order guards are specific to the pinned library.

Ruelle 1979

David Ruelle’s “Ergodic theory of differentiable dynamical systems” appeared in Publications Mathématiques de l’IHÉS 50, pp. 27 to 58. The open PDF states a subadditive theorem as Theorem 1.1 on p. 29. Corollary 1.2 on pp. 29 to 30 treats products of real matrices under integrability of the one-step positive log norm.

That corollary concludes convergence of the signed, extended-real normalized log norm and includes a normalized-integral formula. RMT-33 proves the narrower real-valued log-positive envelope theorem. Constant contractions and zero products show why the two statements are not interchangeable.

Fekete 1923

Michael Fekete’s 1923 paper, DOI 10.1007/BF01504345, contains at Theorem II on printed p. 233 a multiplicative convergence argument for extremal polynomial quantities using a block and remainder decomposition. It is a historical antecedent of the lemma now bearing his name.

The exact modern formal source used here is instead Mathlib/Analysis/Subadditive.lean, whose Subadditive.lim, Subadditive.lim_le_div, and Subadditive.tendsto_lim state the general real-sequence interface needed by the project.

Furstenberg and Kesten 1960

H. Furstenberg and H. Kesten’s “Products of Random Matrices” appeared in The Annals of Mathematical Statistics 31, pp. 457 to 469. The original full text was not accessible in this source audit, so this chapter does not assign an unchecked theorem number or exact assumption list to it. Ruelle’s introduction on p. 28 provides an accessible primary historical connection between the matrix-product result and Kingman’s subadditive theorem.

What the proof teaches beyond this theorem

Several reusable formalization principles emerge.

1. A total operation needs a semantic certificate. Total definitions are convenient for rewriting, but their intended mathematical interpretation may require side conditions.
2. Countable event design is theorem design. Rational margins make the exceptional set both expressive enough for real strict inequalities and small enough for countable measure closure.
3. A null set can carry constructive data. Its complement may produce an eventual numerical witness, not merely a proposition with measure one.
4. Centering should match the available convergence theorem. Subtracting the one-step orbit sum creates a nonpositive residual and an additive Birkhoff component.
5. Conditional completeness should remain visible at public interfaces. RMT-33 returns boundedness beside the lower-limit inequality instead of burying it inside a private proof.
6. Boundary models are part of the theorem specification. The \(-1/n\), quadratic escape, contraction, zero-product, and empty-dimension examples each reject a different overclaim.

Forty solved exercises

The exercises are arranged in eight ropes of five. Each rope begins with a direct reconstruction and ends with a boundary or design problem.

Rope I: total normalization and filter time

Exercise 1: prove that time-zero replacement is invisible

Let \(X:\mathbb N\to\Omega\to\mathbb R\), let \(z:\Omega\to\mathbb R\), and replace \(X_0\) by \(z\). Prove pointwise that the total normalized process is unchanged.

Solution. Fix \(n\) and \(\omega\). If \(n=0\), both normalized values are zero because division by zero in \(\mathbb R\) is totalized to zero. The numerators may differ, but neither survives normalization. If \(n\ne0\), a function update at index zero does not change the \(n\)-th slice, so the numerators and denominators agree. The two cases prove equality for every \(n,\omega\), and function extensionality proves equality of the normalized processes. This is the argument checked by normalizedProcess_update_zero.

The result is stronger than finite-prefix invariance of a limit. It says every normalized value is identical before any asymptotic operation is applied.

Exercise 2: expand frequency at natural infinity

Show that

is equivalent to

Solution. A property is frequent in a filter when its negation is not eventual. For the natural-number atTop filter, eventual \(Q(n)\) means that there is a cutoff \(N\) such that \(Q(n)\) holds whenever \(N\le n\). Negating “eventually not \(P\)” gives: for every proposed cutoff \(N\), there is some \(n\ge N\) at which \(P(n)\) holds. Mathlib packages this equivalence as frequently_atTop.

It expresses arbitrarily late recurrence. It does not say there is a cutoff after which \(P\) always holds.

Exercise 3: separate frequent from eventual

Let \(P(n)\) mean that \(n\) is even. Prove that \(P\) and its negation are both frequent along natural infinity, while neither is eventual.

Solution. Given any cutoff \(N\), the number \(2N\) is at least \(N\) and even, so \(P\) is frequent. The number \(2N+1\) is at least \(N\) and odd, so \(\neg P\) is frequent. If \(P\) were eventual, its frequent negation would be impossible. Likewise, if \(\neg P\) were eventual, frequent \(P\) would be impossible.

This model explains why an arbitrarily-late bad-block event can coexist with arbitrarily late good blocks. RMT-33 needs only recurrent strict crossings at one fixed rational slope.

Exercise 4: remove a finite prefix

Suppose \(a,b:\mathbb N\to\mathbb R\) agree for every \(n\ge17\). Under the usual library side conditions needed for real lower limits, explain why they have the same liminf.

Solution. Agreement from index 17 onward is eventual equality along atTop. The declaration liminf_congr says eventual equality is enough to identify lower limits. One may also shift each sequence by 17 and use liminf_nat_add, then identify the shifted sequences pointwise.

For RMT-33 the first route proves that the exact centered-plus-Birkhoff identity may be rewritten under liminf. The second route proves that the totalized time-zero term has no asymptotic effect.

Exercise 5: decode the relation orientation

Translate the following filter propositions into ordinary quantified sentences:

Solution. The first means there is \(b\in\mathbb R\) such that eventually \(b\le a_n\). It is eventual lower boundedness. The second means there is \(B\in\mathbb R\) such that eventually \(a_n\le B\). It is eventual upper boundedness.

A reliable Lean-reading method is to ignore the English word “under,” expand the relation, and locate the fixed witness. With relation \(\ge\), the eventual assertion has the form \(a_n\ge b\), so \(b\) lies below the sequence. With relation \(\le\), it has the form \(a_n\le B\), so \(B\) lies above it.

Rope II: the guarded real lower limit

Exercise 6: compute the totalized liminf of \(1-n\)

Let \(a_n=1-n\). Show that the set of eventual real lower bounds of \(a\) is empty, then compute Mathlib’s real liminf.

Solution. Fix any \(b\in\mathbb R\). By the Archimedean property, choose a natural \(n\) with \(n\gt1-b\). Then \(1-n\lt b\). The same argument works beyond every proposed cutoff by increasing \(n\), so \(b\le1-n\) cannot hold eventually. Since \(b\) was arbitrary, there is no eventual real lower bound.

The defining set for real liminf is therefore empty. In the pinned real-order implementation, Real.sSup_empty gives \(\sup\varnothing=0\). Hence the formal real liminf is zero. The extended-real lower limit would be negative infinity, so the two notions intentionally diverge outside the bounded-below regime.

Exercise 7: prove event membership forces a low liminf under the guard

Assume \(u\) is eventually bounded below and there is a rational \(q\lt c\) such that \(u_n\lt q\) frequently. Prove

Solution. Frequent strict inequality implies frequent weak inequality \(u_n\le q\). The theorem liminf_le_of_frequently_le, supplied with the eventual lower-bound hypothesis, gives

Composing this weak inequality with \(q\lt c\) yields the desired strict inequality. The rational nature of \(q\) is not used by the liminf theorem. It is used earlier to keep the event family countable.

Exercise 8: prove a low liminf creates a rational event

Assume \(u_n\le0\) for every \(n\) and

Explain how to prove membership in \(D_c\).

Solution. Rational density gives \(q\in\mathbb Q\) satisfying

The global upper bound \(u_n\le0\) supplies the order-coboundedness hypothesis needed by frequently_lt_of_liminf_lt. Applying that theorem to the first strict inequality gives frequent \(u_n\lt q\). The second strict inequality and the event membership characterization then give \(\omega\in D_c\).

The proof uses an upper bound, not the eventual lower bound from Exercise 7. This asymmetry is a feature of conditionally complete liminf APIs.

Exercise 9: locate the false unguarded implication

Use \(u_n=1-n\) and \(c=-1\) to refute

when no eventual lower bound is assumed.

Solution. The sequence is eventually below every fixed rational slope. For example, \(q=-2\) satisfies \(q\lt c\), and \(1-n\lt-2\) for every \(n\gt3\). Thus the point belongs to \(D_{-1}\).

Exercise 6 computed the total real liminf as zero. The claimed conclusion would be \(0\lt-1\), which is false. This counterexample is also compatible with subadditivity after using the checked quadratic-escape process, so the problem cannot be dismissed as an artifact of an unrelated arbitrary sequence.

Exercise 10: compare a real and extended-real design

What would change if the entire proof used \(\mathbb R\cup\{-\infty,+\infty\}\) for lower limits?

Solution. An extended-real liminf can represent unbounded negative escape as negative infinity, so the empty-eventual-lower-bound totalization issue would disappear. Event membership could imply a low extended liminf without first constructing a finite real lower bound.

Several other costs would appear. The centered-plus-Birkhoff identity would mix extended and real arithmetic. Addition near opposing infinities requires care. The final target \(\gamma_+\) is real, so one would still need to prove finiteness before using a real convergence theorem. Existing project APIs for the Birkhoff average and integrated Fekete rate are real-valued. RMT-33’s guarded-real design keeps those interfaces aligned and makes the required finiteness witness explicit. Neither design is universally superior; the right choice depends on whether negative-infinite behavior is part of the intended theorem.

Rope III: rational margins and countable event design

Exercise 11: construct the two margins

Given real numbers \(L\lt\delta\), prove that there are rationals \(q,c\) such that

Solution. First use rational density to choose \(c\in\mathbb Q\) with \(L\lt c\lt\delta\). Apply rational density again to the strict interval \((L,c)\) to choose \(q\in\mathbb Q\) with \(L\lt q\lt c\). Combining the inequalities yields the required chain.

The order of construction matters conceptually. The first choice secures an event target where the prior nullity theorem applies. The second choice secures a witness slope for membership in that event.

Exercise 12: prove the exceptional-set inclusion

Let

Assuming the normalized centered process is nonpositive, prove \(E_\delta\subseteq R_\delta\).

Solution. Fix \(\omega\in E_\delta\), so \(L(\omega)\lt\delta\). Exercise 11 provides rational \(q,c\) with

Normalized centered nonpositivity supplies the coboundedness gate for frequently_lt_of_liminf_lt. Therefore \(u_n(\omega)\lt q\) frequently. Since \(q\lt c\), the event characterization gives \(\omega\in D_c\). Since \(c\lt\delta\), this particular \(D_c\) is one member of the outer union, so \(\omega\in R_\delta\).

Exercise 13: pass nullity through the exhaustion

Suppose \(\mu(D_c)=0\) for every rational \(c\lt\delta\). Prove \(\mu(R_\delta)=0\).

Solution. The index type

is a subtype of the countable type \(\mathbb Q\), hence countable. The set \(R_\delta\) is a countable union of null sets. The measure theorem measure_iUnion_null gives zero measure for the union.

No disjointness is needed. No summability estimate is needed either, because every summand is exactly null. The countability of the rational generator is the decisive closure property.

Exercise 14: diagnose the \(\delta\lt\delta\) failure

Why is the inclusion \(E_\delta\subseteq D_\delta\) insufficient for invoking RMT-32 at target \(\delta\)?

Solution. The RMT-32 nullity theorem separates two parameters. A deterministic \(\delta\) is assumed to lie below every positive normalized centered integral, while the event target \(c\) must satisfy \(c\lt\delta\). This strict gap is what makes the earlier measure ratio strictly below one and selects the null branch.

Calling the theorem with \(c=\delta\) would demand \(\delta\lt\delta\), an impossible hypothesis. The outer rational \(c\) is not proof bureaucracy. It preserves the strict separation on which the prior argument depends.

Exercise 15: replace rationals by another set

Could the proof use dyadic rationals instead of all rationals?

Solution. Yes, provided the chosen set is countable and order-dense in \(\mathbb R\). Dyadic rationals of the form \(k/2^m\) are countable and dense, so both rational choices can be replaced by dyadic choices. Countability still closes the null union, and density still detects every strict real gap.

The current Lean proof uses \(\mathbb Q\) because Mathlib already provides exists_rat_lt and exists_rat_btwn, and the RMT-32 event was defined with rational slopes. A dyadic redesign would add encoding work without strengthening the theorem.

Rope IV: one null cover, two outputs

Exercise 16: extract a concrete eventual lower bound

Fix \(\omega\notin R_\delta\). Choose rationals \(q\lt c\lt\delta\). Prove that \(q\le u_n(\omega)\) eventually.

Solution. Since \(c\lt\delta\), the event \(D_c\) is included in the union \(R_\delta\). Therefore \(\omega\notin D_c\). If \(u_n(\omega)\lt q\) held frequently, then \(q\lt c\) and the membership theorem would put \(\omega\) in \(D_c\), a contradiction.

Thus \(u_n(\omega)\lt q\) is not frequent. In any filter, not_frequently converts this to eventual negation. Eventually it is not true that \(u_n(\omega)\lt q\), which in a linear order is exactly \(q\le u_n(\omega)\). The rational \(q\) is now an explicit witness for eventual lower boundedness.

Exercise 17: extract the lower-liminf inequality

Assume \(\mu(E_\delta)=0\). Prove

almost everywhere.

Solution. A null set has an almost-everywhere complement. Outside \(E_\delta\), the defining statement \(L(\omega)\lt\delta\) is false. Linear order turns \(\neg(L(\omega)\lt\delta)\) into \(\delta\le L(\omega)\). In Lean, measure_eq_zero_iff_ae_notMem crosses from measure-zero language to almost-everywhere nonmembership, and simplification of the set definition finishes the order step.

Exercise 18: explain why Exercise 17 cannot replace Exercise 16

Why not derive eventual lower boundedness directly from the almost-everywhere inequality \(\delta\le L(\omega)\)?

Solution. Because \(L\) is the total real liminf. For \(u_n=1-n\), the formal value is zero even though no eventual lower bound exists. Taking \(\delta=-1\) makes the numerical inequality \(-1\le0\) true, but it provides no lower-bound witness.

Exercise 16 instead uses the logical content of avoiding a frequent rational crossing. That content survives totalization and produces a fixed number below all late values. The proof must therefore retain the rational exhaustion even after it has already shown the lower-liminf exceptional set null.

Exercise 19: combine the almost-everywhere statements safely

Suppose \(P(\omega)\) holds almost everywhere and \(Q(\omega)\) holds almost everywhere. Explain why the conjunction holds almost everywhere and apply this to RMT-33’s generic centered endpoint.

Solution. Filters are closed under finite intersection. The almost-everywhere filter associated with \(\mu\) therefore contains the set where both \(P\) and \(Q\) hold. Lean’s filter_upwards tactic packages this operation.

Take \(P\) to be eventual lower boundedness from the complement of \(R_\delta\). Take \(Q\) to be \(\delta\le\liminf u\) from the complement of \(E_\delta\). Their conjunction is the public theorem ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess. The theorem records that both facts hold at the same sample, which is required before applying le_liminf_add.

Exercise 20: identify the minimal data retained from nullity

Could the helper return only a Boolean statement that the sequence is bounded below?

Solution. The proposition IsBoundedUnder (· ≥ ·) atTop u is existential. Its proof contains a lower-bound witness and an eventual proof, although later theorems normally consume only the packaged proposition. A plain Boolean flag would lose the logical witness and would not satisfy Mathlib’s order APIs.

The proof specifically obtains a rational \(q\) and an eventual statement \(q\le u_n\). Packaging that pair into IsBoundedUnder preserves exactly the information required by liminf_le_of_frequently_le, le_liminf_add, and the final squeeze.

Rope V: centering and Birkhoff transfer

Exercise 21: derive centered nonpositivity

Starting from shifted subadditivity, prove for every positive \(n\) that

then conclude \(Y_n(\omega)\le0\).

Solution. Write a positive horizon as \(n+1\) and induct on \(n\). At the first positive horizon, the orbit sum is \(X_1(\omega)\), so the inequality is equality. For the successor step, use the candidate split:

Apply the induction hypothesis to the earlier positive horizon, then recognize the successor orbit sum. Subtracting that sum from both sides gives \(Y_n(\omega)\le0\) at positive \(n\). Division by a positive natural cast preserves nonpositivity, while normalized time zero is separately zero by totalization. No sign claim about a generic unnormalized \(Y_0\) is needed.

Exercise 22: verify the normalized decomposition at zero

The identity

follows directly for positive \(n\). Why does it also hold at \(n=0\) in Lean?

Solution. Each quotient has denominator zero, so every quotient is zero. The right side is \(0+0\), and the left side is zero. No assertion about \(X_0\), \(Y_0\), or the empty orbit sum needs to be divided algebraically by a nonzero number.

This total identity is valuable because liminf_congr can rewrite the sum without carrying an eventual positivity guard. The positive-time meaning is recovered separately when inequalities are divided by \(n\).

Exercise 23: list the four gates of le_liminf_add

For \(u_n=Y_n/n\) and \(v_n=S_nX_1/n\), identify the four hypotheses supplied in RMT-33.

Solution. The pinned declaration requires:

1. eventual lower boundedness of \(u\);
2. eventual upper boundedness of \(u\);
3. eventual lower boundedness of \(v\);
4. the appropriate lower-side coboundedness condition for \(v\).

The rational null cover supplies item 1. Centered nonpositivity supplies the global upper bound zero for item 2. Birkhoff convergence supplies eventual lower and upper bounds for \(v\); the upper bound yields the needed coboundedness statement for item 4 through the filter-order helper used in the proof.

The theorem then concludes

Exercise 24: prove convergence supplies eventual two-sided bounds

If \(v_n\to\ell\) in \(\mathbb R\), construct explicit eventual bounds.

Solution. Use the open interval \((\ell-1,\ell+1)\), a neighborhood of \(\ell\). Convergence implies \(v_n\in(\ell-1,\ell+1)\) eventually. Hence eventually

Mathlib exposes the same conclusion abstractly through Filter.Tendsto.isBoundedUnder_ge and Filter.Tendsto.isBoundedUnder_le. RMT-33 uses those interfaces instead of selecting radius one manually.

Exercise 25: derive the generic transferred lower bound

Assume almost everywhere that

and that the gates from Exercise 23 hold. Prove

Solution. Convergence gives \(\liminf v=I_1\). Add the assumed centered inequality to equality on the second coordinate:

Apply le_liminf_add to bound the right side by \(\liminf(u+v)\). Finally use eventual, in fact pointwise, equality

and liminf_congr to rewrite the last lower limit. Chaining the three inequalities gives the result.

Rope VI: deterministic Fekete rate and cocycle specialization

Exercise 26: prove integrated subadditivity

Let

Explain why

for \(A_n=\int X_n\,d\mu\).

Solution. Cocycle multiplication and submultiplicativity of the operator norm give a shifted pointwise inequality

The log-positive product inequality is the scalar bridge. Integrate both sides. Measure preservation of \(T^m\) gives

The remaining term integrates to \(A_m\). Finite-horizon integrability licenses integral monotonicity and addition. Thus \(A_{m+n}\le A_n+A_m\), which is the same scalar inequality by commutativity.

Exercise 27: compute the centered Fekete offset

Let

Prove for positive \(n\) that

Solution. The deterministic Fekete property gives

Measure preservation and finite-sum integration give

Therefore

Subtract \(I_1\) from the Fekete inequality to obtain

The left side is \(\delta\).

Exercise 28: propagate one-step integrability

Assume \(X_1\) is integrable and

Why is every \(X_n\) integrable?

Solution. Measure preservation makes every pullback \(X_1\circ T^j\) integrable. A finite sum of integrable functions is integrable, so the orbit majorant is integrable. The observable \(X_n\) is measurable, nonnegative, and bounded above by that integrable majorant. The domination theorem for integrability then gives integrability of \(X_n\).

For the cocycle, one-step integrability is exactly HasIntegrableGeneratorLogPlus. It controls the positive logarithmic envelope only. It does not imply integrability of the negative part of the signed logarithm.

Exercise 29: explain why independence is absent

Identify the mechanism replacing independent increments in the proof.

Solution. The process is generated along one deterministic dynamical orbit. Dependence is controlled by three structural properties:

• the cocycle law splits a long product at a deterministic time;
• the base transformation preserves the measure, so shifted observables have the same integrals;
• ergodicity makes long additive orbit averages converge to their space average and drives the earlier invariant-event dichotomy.

None of these statements asserts independence. A strongly dependent stationary process realized over an ergodic base fits the architecture. The theorem is dynamical, not an independent-sampling limit theorem.

Exercise 30: audit the empty-index boundary

Why does the final theorem remain valid when the matrix index type is empty?

Solution. The prior matrix-observable layer explicitly proves that the norm observable and log-positive observable reduce to their degenerate values for an empty index. In particular,

for every \(n,\omega\). One-step integrability is automatic, every integrated value is zero, and \(\gamma_+=0\). The normalized process is identically zero, so it converges to zero.

The final theorem quantifies over any finite index type and does not add a nonemptiness hypothesis. This is a formal boundary supported by the definitions. It should not be attributed to a classical source as an advertised zero-dimensional matrix theorem.

Rope VII: the final squeeze and the observable boundary

Exercise 31: prove global lower boundedness of the final process

Show that

for every natural \(n\), including zero.

Solution. The numerator is nonnegative by Real.posLog_nonneg. The natural cast of \(n\) is also nonnegative. Division of two nonnegative reals is nonnegative. At \(n=0\), the quotient is zero by total division, consistent with the same inequality.

Thus zero is a global lower bound, stronger than the eventual lower bound required by the final convergence theorem.

Exercise 32: produce the final upper bound

Assume

for all positive \(n\), and \(v_n(\omega)\to I_1\). Prove the normalized process is eventually bounded above.

Solution. Convergence makes \(v_n\) eventually bounded above, say by \(B\). The majorant inequality is eventual because every sufficiently large natural is positive. Therefore the normalized process is eventually at most \(B\). In Lean, the proof packages the majorant as an eventual relation and uses IsBoundedUnder.mono_le to transfer the Birkhoff sequence’s upper-boundedness certificate.

This upper bound is not inferred from the limsup inequality alone. It is constructed from an actual convergent majorant.

Exercise 33: close convergence from four hypotheses

Let \(a:\mathbb N\to\mathbb R\). Assume

and that \(a\) is eventually bounded both below and above. Prove \(a_n\to\gamma\).

Solution. General order gives

under the relevant boundedness regime. Combining all inequalities forces

A real sequence with equal finite lower and upper limits converges to their common value. The pinned declaration tendsto_of_le_liminf_of_limsup_le packages the entire argument and asks for the two boundedness witnesses explicitly.

RMT-33 instantiates \(a_n=X_n(\omega)/n\) and \(\gamma=\gamma_+\) on a common almost-everywhere set.

Exercise 34: compute constant-contraction limits

Let \(C_n=a^nI\) with \(0\lt a\lt1\) and \(\lVert I\rVert=1\). Compute the signed and log-positive normalized limits.

Solution. The norm is \(a^n\). For positive \(n\),

Since \(a^n\le1\),

Therefore

for every positive \(n\), and its limit is zero.

This example refutes any claim that RMT-33 recovers negative Lyapunov exponents.

Exercise 35: compute the zero-product observables

Suppose \(C_n(\omega)=0\) for all \(n\ge N\). Compare the signed extended log and the real log-positive observable.

Solution. The norm is zero after \(N\). In an extended signed convention,

so the normalized signed value is negative infinity after the collapse. In Mathlib’s real positive logarithm,

Thus the log-positive normalized observable is zero after \(N\).

The two observables answer different questions. Signed growth detects collapse. Log-positive growth records only expansion above one. RMT-33 is correct for the latter and silent about the former.

Rope VIII: assumptions, sources, and next formalizations

Exercise 36: assemble full ergodicity

The final theorem assumes PreErgodic C.base μ. Explain why Birkhoff may nevertheless use a full Ergodic C.base μ instance.

Solution. A DiscreteMatrixCocycle stores C.base_preserving. In pinned Mathlib, PreErgodic supplies the rigidity condition but not preservation, while Ergodic extends both MeasurePreserving and PreErgodic. The proof constructs the full structure from the bundled preservation proof and the explicit pre-ergodicity hypothesis.

For an arbitrary map without bundled preservation, pre-ergodicity alone would not license integral transport or the pointwise Birkhoff theorem used here.

Exercise 37: explain why almost-sure convergence does not prove \(L^1\)

convergence

RMT-33 proves \(a_n\to\gamma_+\) almost everywhere. Why can it not conclude

from that statement alone?

Solution. Almost-everywhere convergence does not control the size of rare large deviations. \(L^1\) convergence would follow from additional hypotheses such as domination by one integrable function or uniform integrability, but neither is established for the normalized sequence in RMT-33. The one-step Birkhoff majorant is samplewise useful and convergent almost everywhere, yet the theorem does not package an integrable dominator uniform in \(n\).

Classical versions of Kingman’s theorem may prove mean convergence under their assumptions. That historical fact cannot be imported into the narrower checked theorem without a formal proof.

Exercise 38: compare the four cited sources

Assign one careful role to each of Kingman 1968, Steele 1989, Ruelle 1979, and Fekete 1923.

Solution.

• Kingman 1968 is the primary source for the subadditive ergodic theorem and its stationary process architecture.
• Steele 1989 gives a compact accessible proof organized around one-step centering, finite interval decomposition, bad sets, and a final limsup-liminf comparison.
• Ruelle 1979 supplies a primary matrix-cocycle specialization, but for the signed extended-real logarithm and with conclusions stronger than RMT-33.
• Fekete 1923 is a historical multiplicative antecedent of normalized subadditive convergence. The exact modern general theorem used by Lean is Mathlib’s Analysis/Subadditive API.

These roles avoid claiming that any source states the present formal theorem word for word.

Exercise 39: map proof moves to pinned declarations

Choose declarations for the following jobs: remove time zero, turn low liminf into frequent crossings, turn frequent crossings into low liminf, nullify a countable union, transfer lower limits through addition, and close convergence.

Solution.

The middle two order declarations have different side conditions. A correct proof audit must record those conditions rather than treating the declarations as unconditional converses.

Exercise 40: design the next signed theorem

List the new mathematical interfaces needed to turn the project from log-positive convergence toward a signed Lyapunov growth theorem.

Solution. At minimum, the project would need:

1. a signed or extended-real log-norm observable that represents zero norms without real totalization;
2. integrability assumptions controlling the positive part, and a clear policy for the negative part;
3. extended-real liminf, limsup, addition, and measurability interfaces, or a proof that the relevant norms stay positive and the signed rate stays finite;
4. a signed subadditive convergence theorem with its samplewise and integral conclusions stated precisely;
5. boundary tests for singular products and contractions;
6. additional inverse-cocycle hypotheses if the goal includes finite two-sided exponents;
7. substantially more linear algebra and invariant-subspace machinery for an Oseledets filtration or splitting.

RMT-33 provides none of these merely by changing notation. Its reusable contribution is the event, centering, rational-cover, and boundedness architecture.

Final theorem card

Under a probability measure, a discrete finite-dimensional matrix cocycle whose base preserves the measure and is pre-ergodic, and whose one-step log-positive generator norm is integrable, satisfies

for almost every \(\omega\).

The proof is valid because the rational null cover establishes not only the lower-liminf inequality but also the eventual lower boundedness needed to interpret and manipulate the real lower limit under its exact hypotheses.

The limit is nonnegative and expansion-only. It need not equal the signed top Lyapunov exponent.

The next checked layer is The Forward-and-Inverse Tail Sandwich for Finite-Time Real Log Norms. It supplies pointwise unit and inverse-tail hypotheses that make every finite-time signed real-log observable integrable and subadditive. It also isolates the strictly positive-rate case where the theorem above can be unclipped without those hypotheses. That successor still does not prove a general signed almost-everywhere limit or an Oseledets splitting.