Rational-Slack Lower-Deviation Events and Ergodic Null Selection

Base camp: a nonempty event can still be the null branch

Start with the two-state space

and the probability measure

The point \(a\) exists in the sample space, but it is a null state : the singleton \(\{a\}\) has measure zero. The point \(b\) carries all probability mass. Let the dynamics collapse the null state into the supported state and then remain there:

Because the only point seen with positive probability is the fixed point \(b\), \(T\) is measure preserving and ergodic for this measure. This does not erase \(a\) as a set-theoretic point; it means that events differing only at \(a\) agree almost everywhere .

Define \(X_0=0\). At every positive horizon \(n\), set

The one-step observable is zero at both states. Its orbit sum is therefore zero, so the project’s centered process is exactly this process:

Check subadditivity before using the example

The process is not merely a table chosen to fit the conclusion. It is a shifted-subadditive candidate. The cases with \(m=0\) or \(n=0\) are equalities because \(X_0=0\). When \(m,n\gt0\), the supported state gives

At the null state, \(T^m a=b\) for positive \(m\), so

The finite Std worksheet later checks every triple \((m,n,\omega)\) with \(0\le m,n\le12\). The displayed symbolic calculation, which does not depend on that finite cutoff, establishes the formula at every horizon.

This exact two-state ledger is the chapter’s pedagogical model, not one of the six anonymous Mathlib-backed probes compiled in RMT-32. The source contains nearby collapse, identity, half-mass, zero-process, and empty-index probes. The complete source-order map below keeps those checked artifacts separate from this executable teaching worksheet.

Fix one rational margin below the target

Choose

The margin is strict:

At \(a\), the positive-time normalized values are

The inequality \(X_n(a)\lt qn\) is equivalent to

Thus every \(n\ge5\) is a strict \(q\)-witness. At \(b\),

so no rational threshold below \(c\) can ever be a witness there.

The phrase arbitrarily late has exact quantifiers. Given any cutoff \(N\), choose

Then \(N\le n\), \(n\gt0\), and \(X_n(a)\lt qn\). One formula answers every possible cutoff, although the chosen witness may depend on that cutoff.

Consequently the fixed-margin and target events are

Compute the preimage before saying “invariant”

No state maps to \(a\). Therefore

Literal invariance is false. But the symmetric difference is \(\{a\}\), a null set, so

This one example separates set inclusion, equality, and almost-everywhere equality.

Let the integrated rate select the branch

Integration sees only the supported point \(b\):

For every positive \(n\),

Our target satisfies \(c=-5/4\lt\delta=-1\). The inherited RMT-31 ratio is

Ergodicity and probability normalization give the numerical fork

The strict subunit estimate rules out \(1\), so

The direct set computation already told us the answer. The point of the theorem architecture is that the same branch selection works when an event cannot be enumerated point by point.

The full branch is not fictional. At the higher target \(c_{\mathrm{full}}=-3/4\), state \(a\) uses margin \(-3/2\) and state \(b\) uses margin \(-4/5\). Hence

There is no conflict with the strict estimate because

is false. The hypothesis \(c\lt\delta\) is a mathematical gate, not proof ceremony.

The lower half of a subadditive ergodic theorem has a particular logical shape. First construct the right exceptional event. Then show that shifting time does not change it except on a null set. Only after that may ergodicity force the event to be almost empty or almost full. Finally, a quantitative estimate must rule out the full branch.

Random-matrix-theory milestone 32 (RMT-32) formalizes that event-level architecture for the centered process used throughout this project. Its central lesson is concise but technically important:

Strict asymptotic deviation needs one margin that survives arbitrarily far into time. Repeated inequalities at the target line are not enough.

The durable margin is chosen from the rational numbers. That choice preserves the intended real threshold through density while keeping the event a countable union, exactly the form needed by the available null-measurability closure theorems.

This chapter is the textbook companion to the RMT-32 Development Notebook. It continues From Finite Centered Bad-Block Bounds to All-Positive-Length Control and uses the quantitative estimate from Finite Bad-Block Measure Bounds Before Kingman Lower Liminf. Compact background is available in orbit-majorant centering , ergodicity , ergodic probability base , and almost everywhere .

Choose a route up

Common setup and notation

Let \(\Omega\) be a type of states, let \(\mu\) be a measure on \(\Omega\), and let \(T:\Omega\to\Omega\) advance the base dynamics by one step. Let

be a shifted-subadditive process:

The repository subtracts the additive orbit sum of the one-step observable:

This is pointwise orbit-majorant centering . It is not subtraction of an expectation. The resulting centered process has

and remains shifted-subadditive. In particular, the split \(1+n\) gives

For positive \(n\), write the normalized centered slope as

RMT-32 avoids formal use of \(z_n\) and division inside its event. It writes the equivalent positive-time inequality \(Y_n(\omega)\lt qn\). This keeps the witnesses close to the finite bad-block machinery inherited from RMT-31.

Why one witness cannot carry an asymptotic theorem

RMT-31 studies the all-positive-length once-bad event

A point enters after one finite witness. That is exactly the right union for passing a finite-cap measure estimate to all possible lengths. It is not the right event for a lower asymptotic slope.

A transient defect can create one strict inequality and then disappear. If a process has \(Y_2=-1\) but \(Y_n=-1\) for every later \(n\), then \(z_n=-1/n\) returns to zero. At the target \(c=-2/5\), time two is bad, but sufficiently late times are not. The point is once-bad without having a negative lower asymptotic slope below \(-2/5\).

The required quantifier change is therefore

The new universal cutoff is what turns a finite incident into an asymptotic pattern.

Build one fixed-margin event

Fix a real slope \(q\). RMT-32 defines

The Lean definition spells this out as a countable intersection over cutoffs, followed by a countable union over candidate witness lengths, followed by a logical guard recording \(N\le n\) and \(0\lt n\). The membership theorem packages the nested set expression back into the readable quantifiers above.

The condition means arbitrarily late, not eventually always. For every cutoff there is a later witness, but good lengths may occur between witnesses. On natural-number time, this is equivalent to having an unbounded set of bad witness lengths. It is stronger than having at least one witness and weaker than requiring every sufficiently large length to be bad.

The positivity guard matters at cutoff zero. The normalized slope is a positive-time object, and \(Y_0\lt q\cdot0\) would not carry the intended information.

Exhaust the target from below

Now fix the target \(c\in\mathbb R\). The strict lower-deviation event is

Thus \(\omega\in D_c\) means that one rational \(q\lt c\) works beyond every cutoff. The same \(q\) must work throughout the argument. It may not drift toward \(c\) as the cutoff grows.

The definition immediately gives two useful inclusions:

For the second inclusion, choose the rational witness \(q\lt c\), take any positive arbitrarily-late witness, and use positivity of \(n\) to obtain \(qn\lt cn\). This bridge is where RMT-31’s quantitative once-bad estimate will later enter.

Why strict rational slack is essential

It is tempting to define a target event using arbitrarily late inequalities at \(c\) itself:

That condition is too weak for a strict lower-limit conclusion. Consider

Every term lies strictly below \(c\), so the same-threshold condition holds at every positive time. Yet \(z_n\) converges upward to \(c\). Its lower limit equals \(c\), not a value strictly below \(c\).

For any fixed \(q\lt c\), put \(\varepsilon=c-q\gt0\). Once \(1/(n+1)\lt\varepsilon\), we have \(z_n\gt q\). Therefore no fixed rational \(q\lt c\) has witnesses arbitrarily late. The event \(D_c\) correctly rejects this sequence.

Why use rational rather than real margins? Two reasons coincide.

First, the rational numbers are dense: whenever a real value \(d\lt c\), one can choose \(q\in\mathbb Q\) with \(d\lt q\lt c\). A genuine strict gap is therefore detectable by a rational threshold.

Second, the rational numbers are countable. A union over all real \(q\lt c\) would be uncountable, and null-measurable sets are not generally closed under arbitrary uncountable unions. Rational density keeps the semantic resolution while supplying the countable syntax needed by measure theory.

RMT-32 does not prove an equality between \(D_c\) and a Mathlib expression involving liminf. The countersequence above validates the design. The exact guarded bridge is proved in SubadditiveKingman.lean and explained in the later RMT-33 Deep Dive.

Pull a shifted witness back one step

The dynamical part of the module begins with a point \(\omega\in T^{-1}A_q\). This means \(T\omega\in A_q\). For every large cutoff, there is a positive \(n\) with

Centered shifted subadditivity at the split \(1+n\), together with \(Y_1=0\), gives

The witness moves back to \(\omega\), but its length changes from \(n\) to \(n+1\). At the same threshold, the comparison between \(qn\) and \(q(n+1)\) has the wrong direction when \(q\lt0\). Same-threshold setwise invariance is therefore not available.

Spend a little threshold to absorb the endpoint

Choose real slopes \(q\lt r\). The arithmetic lemma proves that some natural cutoff \(K\) satisfies

To see why, rewrite the desired inequality as

Since \(r-q\gt0\), it is enough to choose a natural number larger than \((-r)/(r-q)\). Mathlib’s Archimedean theorem provides such a natural number. No sign assumption on \(q\) or \(r\) is needed.

The supported state in base camp gives a fully numerical instance. Take

At \(n=32\),

The final comparison is only one fortieth wide: \(-128/5=-1024/40\lt-1023/40\). It is nevertheless strict, which is all the set inclusion needs. Smaller horizons may fail that endpoint comparison; the theorem promises an eventual cutoff, not a uniform inequality from time one.

Given a requested cutoff \(N\), ask the \(A_q\) hypothesis at \(\max(N,K)\). The resulting \(n\) is late enough both for the user’s cutoff and for the endpoint arithmetic. Then

Thus

The public theorem carrying this step has an integrable-candidate receiver because that is the repository’s reusable process interface. Its proof uses only the centered shifted-subadditivity add_le field. Integrability first does mathematical work in the null-measurability layer below. This is a proof-dependency observation, not a claim that the public shift theorem has no assumptions.

Recover the same target through rational density

Suppose \(T\omega\in D_c\). Then some rational \(q\lt c\) satisfies \(T\omega\in A_q\). Rational density supplies another rational \(r\) with

The relaxed shift theorem gives \(\omega\in A_r\), and \(r\lt c\) puts that event back into the same union \(D_c\). Hence

This is a one-sided set inclusion. It is neither setwise equality nor an almost-everywhere statement. The distinction is the hinge for the next measure-theoretic layer.

Establish null measurability without finite mass

Assume the public integrable shifted-subadditive candidate interface and that \(T\) preserves \(\mu\). Every centered process value is integrable, hence almost-everywhere measurable. Therefore each threshold set

is null measurable. Mathlib’s countable closure operations then assemble the event:

followed by the countable rational union defining \(D_c\).

The result is NullMeasurableSet, not necessarily MeasurableSet. Null measurability is exactly the stable language for representatives that may differ from measurable functions or sets on a null set.

Finite total mass, probability normalization, and ergodicity are absent from both regularity theorems. Preservation appears because the existing integrability theorem for the centered process transports the one-step observable along the orbit.

Upgrade inclusion to almost-invariance

Let \(D=D_c\). Three facts are now available:

1. \(T^{-1}D\subseteq D\);
2. \(D\) is null measurable; and
3. preservation gives \(\mu(T^{-1}D)=\mu(D)\).

If \(\mu\) is finite, the larger set cannot contain a positive-measure remainder. Mathlib’s subset-plus-measure comparison theorem yields

Here \(=^{\mu}_{\mathrm{ae}}\) means that membership agrees for \(\mu\)-almost every point. It does not mean literal set equality.

Finite mass enters at one precise point: the target measure must not be infinite. Without that gate, a proper subset can have the same infinite measure as its superset. Equality \(\infty=\infty\) cannot prove that the difference is null.

This also explains why preservation alone is not invariance. It equates measures of a null-measurable set and its preimage. The one-sided dynamical inclusion and finite target are the additional ingredients that turn equality of numbers into almost-equality of sets.

Separate dichotomy from branch selection

Assume now that \(T\) is ergodic and \(\mu\) is finite. Mathlib’s quasi-ergodic almost-invariance theorem applies to the null-measurable event:

This is the ergodic dichotomy. Probability normalization is not needed for it. On a finite measure of total mass \(m\), the full branch has measure \(m\), whatever \(m\) is.

If \(\mu\) is a probability measure, then \(m=1\), and the setwise dichotomy becomes the numerical statement

Ergodicity does not by itself tell us which branch occurs.

Use RMT-31 to exclude the full branch

Suppose a real number \(\delta\) satisfies the uniform centered-integral lower bound

and choose \(c\lt\delta\). The time-one identity \(Y_1=0\) forces \(\delta\le0\), hence \(c\lt0\).

The inclusion \(D_c\subseteq B_\infty(c)\) and RMT-31 give

Because the denominator is negative, \(c\lt\delta\) is exactly what yields

Therefore \(\mu_{\mathbb R}(D_c)\lt1\). This strict estimate needs finite mass, preservation, the candidate interface, the rate premise, and \(c\lt\delta\). It needs neither probability nor ergodicity.

On an ergodic probability space, however, the full branch would have real mass one. The strict estimate excludes it, leaving

The order matters:

1. finite-measure ergodicity yields the almost-empty or almost-full dichotomy;
2. probability identifies the full branch numerically with mass one; and
3. the strict RMT-31 ratio selects the null branch.

Probability is not being used retroactively to prove almost-invariance.

Walk through the boundary models

Boundary models are not decorative examples. Each removes one tempting shortcut from the theorem narrative.

Boundary 1: one bad block can disappear forever

On the two-point state space Bool, let the base map send both points to true and use the Dirac measure at true. The one-shot process is zero at true. At false it is zero at short length and equals \(-1\) from length two onward.

At slope \(-2/5\), the RMT-31 once-bad event is exactly \(\{\texttt{false}\}\): length two gives \(-1\lt-4/5\). But the normalized value is \(-1/n\), which returns to zero. Beyond a sufficiently large cutoff there is no witness below any fixed rational slope less than \(-2/5\). Consequently the RMT-32 strict event is empty.

This model preserves its chosen measure and satisfies the integrable subadditive candidate interface. It shows why one finite witness cannot be relabelled as an asymptotic deviation.

Boundary 1b: same-threshold recurrence can still miss strict deviation

The same checked one-shot process isolates rational slack at target zero. At false, every length from two onward has centered value \(-1\), so there are witnesses below the target line zero beyond every cutoff. The source therefore proves

But strict target membership requires some rational \(q\lt0\). For each such fixed \(q\), the normalized values \(-1/n\) eventually rise above \(q\). Hence

This is the compiled counterpart of the approaching-target countersequence. It is a set-semantic audit, not a positive-probability counterexample: under the preserved Dirac measure at true, the point false and the raw set \(A_0\) have measure zero.

Boundary 2: invariant half mass is possible without ergodicity

Let \(T\) be the identity on Bool with equal mass on the two points. Put

The one-step observable is zero, so centering changes nothing. At \(c=-3/4\), the normalized values at false approach \(-1\), while those at true remain zero. A rational margin between \(-1\) and \(-3/4\) works arbitrarily late at false. Hence

The event is exactly invariant because the map is the identity. The system is not ergodic, so invariant half-mass events are allowed. This separates invariance from ergodic rigidity.

Boundary 3: a subunit full event is possible without probability

Now use a one-point space with the measure \(\frac12\delta_{()}\), the identity map, and the scalar process \(X_n=-(n-1)\). The one-point system is ergodic, the strict event at \(-3/4\) is the whole space, and

The checked numeric audit records

Thus the full event still obeys a strict subunit ceiling.

There is no contradiction: the total mass is \(1/2\), not one. This model pinpoints why probability normalization is needed for null-branch selection, even though finite-measure ergodicity already supplies the empty-or-full dichotomy.

Boundary 4: the zero process respects strict negative thresholds

For \(X_n=0\), the centered process is zero. If \(c\le0\), then every rational \(q\lt c\) is negative, so \(qn\lt0\) at every positive length. The required inequality \(0\lt qn\) is impossible. Therefore \(D_c\) is empty at every nonpositive target.

This audit checks strictness, positivity of witness lengths, and the direction of multiplication by a positive natural number.

Boundary 5: an empty matrix index remains legal

The cocycle theorem works with the matrix index type Empty. The proof never selects a coordinate or assumes a positive matrix dimension; it consumes the already bundled log-positive norm process. This is an interface boundary, not a claim that zero-dimensional matrices model a physical random dynamical system.

Boundary 6: approaching the target from below is rejected

The scalar sequence \(z_n=c-1/(n+1)\) is below \(c\) at every time but has no durable margin below \(c\). It is the direct semantic audit for the rational slack. Unlike the finite-state process models above, it is used to test the event definition itself rather than the full candidate-and-measure interface.

Specialize the architecture to matrix cocycles

Let \(C\) be a one-sided discrete matrix cocycle. Its process is

where \(\log^+(x)=\max(\log x,0)\) and the norm is the induced infinity operator norm. RMT-32 names both the fixed-margin arbitrarily-late event and the rationally generated strict event for this process.

If C.HasIntegrableGeneratorLogPlus, the preceding RMT-30 canonization exposes the centered Fekete-offset lower bound

where \(\gamma^+_\mu(C)\) is the integrated log-positive growth rate . On an ergodic probability base, every \(c\lt\delta_C\) satisfies

The result concerns the centered log-positive norm process. It does not construct a signed logarithmic growth rate, a Lyapunov exponent, or an Oseledets splitting. It also does not prove pointwise convergence of the normalized cocycle process.

In Lean: seven bridges from cutoffs to the null branch

Base camp used two named states and exact rational numbers. The project source works with arbitrary state types, real-valued integrable shifted-subadditive candidates, and Mathlib measures. Read each bridge in four layers: ordinary language, paper mathematics, exact Lean, and the tokens that carry its assumptions.

Bridge 1: expose every cutoff and its later witness

mem_centeredArbitrarilyLateBadBlockSet_iff

Bridge 2: expose one durable rational margin

mem_centeredStrictLowerDeviationSet_iff

Bridge 3: pull back a witness by relaxing its slope

hX.preimage_centeredArbitrarilyLateBadBlockSet_subset_of_lt hqr

Bridge 4: upgrade same-target inclusion to almost-invariance

hX.preimage_centeredStrictLowerDeviationSet_ae_eq hT c

Bridge 5: let ergodicity create the fork

hX.centeredStrictLowerDeviationSet_ae_empty_or_univ hT c

Bridge 6: use the strict ratio to select zero

hX.measure_centeredStrictLowerDeviationSet_eq_zero hT δ c hδ hc

Bridge 7: specialize the event to log-positive cocycle growth

hC.measure_centeredLogPlusStrictLowerDeviationSet_eq_zero hErg c hc

Try every public declaration in the repository

import NonlinearDynamics.Random.RandomCocycles.SubadditiveLowerDeviation

open MeasureTheory Set Filter Topology Function
open NonlinearDynamics.Random.RandomCocycles

-- The nineteen RMT-32 public declarations, in source order.
#check centeredArbitrarilyLateBadBlockSet
#check mem_centeredArbitrarilyLateBadBlockSet_iff
#check centeredStrictLowerDeviationSet
#check mem_centeredStrictLowerDeviationSet_iff
#check exists_nat_forall_mul_lt_mul_succ
#check centeredArbitrarilyLateBadBlockSet_subset_allLength
#check centeredStrictLowerDeviationSet_subset_allLength
#check IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_centeredArbitrarilyLateBadBlockSet
#check IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_centeredStrictLowerDeviationSet
#check IsIntegrableSubadditiveProcessCandidate.preimage_centeredArbitrarilyLateBadBlockSet_subset_of_lt
#check IsIntegrableSubadditiveProcessCandidate.preimage_centeredStrictLowerDeviationSet_subset
#check IsIntegrableSubadditiveProcessCandidate.preimage_centeredStrictLowerDeviationSet_ae_eq
#check IsIntegrableSubadditiveProcessCandidate.centeredStrictLowerDeviationSet_ae_empty_or_univ
#check IsIntegrableSubadditiveProcessCandidate.measure_centeredStrictLowerDeviationSet_eq_zero_or_one
#check IsIntegrableSubadditiveProcessCandidate.measureReal_centeredStrictLowerDeviationSet_lt_one
#check IsIntegrableSubadditiveProcessCandidate.measure_centeredStrictLowerDeviationSet_eq_zero
#check DiscreteMatrixCocycle.centeredLogPlusArbitrarilyLateBadBlockSet
#check DiscreteMatrixCocycle.centeredLogPlusStrictLowerDeviationSet
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.measure_centeredLogPlusStrictLowerDeviationSet_eq_zero

cd formalization
lake env lean NonlinearDynamics/SubadditiveLowerDeviationChecks.lean

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

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

Type the finite witness and branch ledgers with Lean and Std

The next worksheet contains no Mathlib import. It computes the two-state process, the fixed \(q=-3/2\) witnesses, the endpoint-relaxation arithmetic, the strict preimage inclusion, the probability masses, the \(4/5\) branch ceiling, and the transient no-slack boundary. It also checks shifted subadditivity for every pair of horizons through twelve.

The finite Boolean search illustrates the formulas; it does not replace the general quantified proofs or define a measure-theoretic liminf. Save this exact text as /tmp/RationalSlackLowerDeviationTutorial.lean:

import Std

namespace RationalSlackLowerDeviationTutorial

inductive Point where
  | a
  | b
  deriving Repr, DecidableEq, BEq

def points : List Point := [.a, .b]

def step : Point → Point
  | .a => .b
  | .b => .b

def iterate : Nat → Point → Point
  | 0, p => p
  | n + 1, p => iterate n (step p)

def weight : Point → Nat
  | .a => 2
  | .b => 1

def process (n : Nat) (p : Point) : Int :=
  -((weight p * (n - 1) : Nat) : Int)

def normalize (z : Int) (n : Nat) : Rat :=
  if n = 0 then 0 else (z : Rat) / (n : Rat)

def slope (n : Nat) (p : Point) : Rat :=
  normalize (process n p) n

def q : Rat := -3 / 2
def c : Rat := -5 / 4
def delta : Rat := -1

def strictBad (threshold : Rat) (n : Nat) (p : Point) : Bool :=
  decide (0 < n) &&
    decide ((process n p : Rat) < threshold * (n : Rat))

def badTimes (threshold : Rat) (p : Point) (horizon : Nat) : List Nat :=
  (List.range (horizon + 1)).filter fun n => strictBad threshold n p

def processRow (n : Nat) :=
  (n, process n .a, slope n .a, strictBad q n .a,
    process n .b, slope n .b, strictBad q n .b)

def recurringWitness (cutoff : Nat) : Nat := max cutoff 5

def recurringWitnessRow (cutoff : Nat) :=
  let n := recurringWitness cutoff
  (cutoff, n, process n .a, q * (n : Rat), strictBad q n .a)

def subadditiveThrough (bound : Nat) : Bool :=
  (List.range (bound + 1)).all fun m =>
    (List.range (bound + 1)).all fun n =>
      points.all fun p =>
        process (m + n) p ≤ process m p + process n (iterate m p)

def qShift : Rat := -4 / 5
def rShift : Rat := -31 / 40

def endpointLedger :=
  let n := 32
  (n, process n .b, qShift * (n : Rat), process (n + 1) .b,
    rShift * ((n + 1 : Nat) : Rat),
    decide (process (n + 1) .b ≤ process n .b),
    decide ((process n .b : Rat) < qShift * (n : Rat)),
    decide (qShift * (n : Rat) < rShift * ((n + 1 : Nat) : Rat)))

def nullEvent : List Point := [.a]
def fullEvent : List Point := points

def preimage (event : List Point) : List Point :=
  points.filter fun p => event.contains (step p)

def pointMass : Point → Rat
  | .a => 0
  | .b => 1

def eventMass (event : List Point) : Rat :=
  (event.map pointMass).sum

def transient (n : Nat) (p : Point) : Int :=
  if p == .a && decide (2 ≤ n) then -1 else 0

def transientSlope (n : Nat) (p : Point) : Rat :=
  normalize (transient n p) n

def transientBad (threshold : Rat) (n : Nat) (p : Point) : Bool :=
  decide (0 < n) &&
    decide ((transient n p : Rat) < threshold * (n : Rat))

def transientBadTimes
    (threshold : Rat) (p : Point) (horizon : Nat) : List Nat :=
  (List.range (horizon + 1)).filter fun n => transientBad threshold n p

def transientRow (n : Nat) :=
  (n, transient n .a, transientSlope n .a,
    transientBad 0 n .a, transientBad (-1 / 10) n .a)

#eval (List.range 8).map fun k => processRow (k + 1)
#eval [0, 1, 4, 5, 10, 100].map recurringWitnessRow
#eval endpointLedger
#eval (nullEvent, preimage nullEvent,
  eventMass nullEvent, eventMass (preimage nullEvent))
#eval (delta, c, delta / c, decide (delta / c < 1),
  eventMass nullEvent, eventMass fullEvent)
#eval transientBadTimes (-2 / 5) .a 12
#eval [2, 3, 5, 9, 10, 20].map transientRow
#eval subadditiveThrough 12

example : q < c := by native_decide
example : badTimes q .a 8 = [5, 6, 7, 8] := by native_decide
example : badTimes q .b 20 = [] := by native_decide
example : preimage nullEvent = [] := by native_decide
example : eventMass nullEvent = 0 := by native_decide
example : delta / c = 4 / 5 := by native_decide
example : transientBadTimes (-2 / 5) .a 12 = [2] := by native_decide
example : subadditiveThrough 12 = true := by native_decide

end RationalSlackLowerDeviationTutorial

From any directory, type:

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

The byte-for-byte standard output emitted by Lean is:

[(1, 0, 0, false, 0, 0, false),
 (2, -2, -1, false, -1, (-1 : Rat)/2, false),
 (3, -4, (-4 : Rat)/3, false, -2, (-2 : Rat)/3, false),
 (4, -6, (-3 : Rat)/2, false, -3, (-3 : Rat)/4, false),
 (5, -8, (-8 : Rat)/5, true, -4, (-4 : Rat)/5, false),
 (6, -10, (-5 : Rat)/3, true, -5, (-5 : Rat)/6, false),
 (7, -12, (-12 : Rat)/7, true, -6, (-6 : Rat)/7, false),
 (8, -14, (-7 : Rat)/4, true, -7, (-7 : Rat)/8, false)]
[(0, 5, -8, (-15 : Rat)/2, true),
 (1, 5, -8, (-15 : Rat)/2, true),
 (4, 5, -8, (-15 : Rat)/2, true),
 (5, 5, -8, (-15 : Rat)/2, true),
 (10, 10, -18, -15, true),
 (100, 100, -198, -150, true)]
(32, -31, (-128 : Rat)/5, -32, (-1023 : Rat)/40, true, true, true)
([RationalSlackLowerDeviationTutorial.Point.a], [], 0, 0)
(-1, (-5 : Rat)/4, (4 : Rat)/5, true, 0, 1)
[2]
[(2, -1, (-1 : Rat)/2, true, true),
 (3, -1, (-1 : Rat)/3, true, true),
 (5, -1, (-1 : Rat)/5, true, true),
 (9, -1, (-1 : Rat)/9, true, true),
 (10, -1, (-1 : Rat)/10, true, false),
 (20, -1, (-1 : Rat)/20, true, false)]
true

The first ledger has columns \((n,X_n(a),X_n(a)/n,\text{bad at }a,X_n(b),X_n(b)/n,\text{bad at }b)\). The second turns six requested cutoffs into explicit witnesses. The three Boolean values in the endpoint row check

The next tuple computes \(D_c=\{a\}\), \(T^{-1}D_c=\varnothing\), and the two zero masses. The branch tuple records \((\delta,c,\delta/c,\delta/c\lt1,\mu(D_c),\mu(\Omega))\). The singleton list [2] is the transient once-bad witness, while the final ledger shows same-target recurrence and the fixed \(-1/10\) margin expiring at equality when \(n=10\). The last true is the bounded exhaustive subadditivity check.

Standalone tutorial, suitable for a normal macOS or Linux machine. It imports only Std and never opens the project’s Mathlib dependency graph. This exact file and output were checked with the pinned Lean 4.32.0 toolchain. The exact project module uses the full project commands above.

Complete source-order declaration, helper, probe, and axiom map

The authoritative source is 668 lines and has SHA-256 1bdcfd6b3be654f52bae22bdb2b44c15848e66d51f3a0973ce1c8aba61db14d4. It contains nineteen public declarations, twenty-one private support items, six anonymous compiled probes, and ten axiom queries. The complete sequence is:

The module prints the axiom dependencies of the ten declarations in items 47 through 56. The checked build uses the standard classical and quotient principles already used by Mathlib, with no sorry, admit, or project-local axiom.

Keep an exact assumption ledger

Two qualifications determine how these theorem signatures should be read.

First, both public preimage-inclusion methods are stated on the bundled integrable candidate even though their dynamical bodies project only the shifted-subadditivity add_le field. The public receiver remains an assumption of each theorem. Integrability first enters the argument when the threshold sets must be proved null measurable.

Second, Ergodic T μ supplies preservation through its bundled interface. The prose separates the jobs of preservation and ergodicity, but the final theorem need not ask for preservation twice.

Stop exactly at the RMT-32 boundary

RMT-32 proves that \(D_c\) is null under the centered rate hypotheses on an ergodic probability base. It deliberately stops before translating that set statement into the final asymptotic theorem.

The subsequent milestone proves a guarded bridge of the following mathematical kind. For positive-time normalized slopes, strict lower-limit deviation below \(c\) produces one rational \(q\lt c\) with witnesses beyond every cutoff, and conversely the rational event implies the matching strict lower-limit statement when the real sequence has the required eventual lower bound. The pinned Mathlib lower-limit API makes those boundedness gates part of the theorem rather than silent paper notation.

RMT-33 then combines:

1. the RMT-32 null lower-deviation events;
2. RMT-29’s normalized upper-limsup estimate; and
3. the ergodic Birkhoff limit of the one-step orbit majorant.

RMT-32 does not prove full samplewise Kingman convergence, \(L^1\) convergence, interchange of a limit and an integral, powered-map ergodicity, signed logarithmic growth, a Lyapunov exponent, or an Oseledets splitting.

The proof architecture is adapted to this repository. Steele’s exposition centers a subadditive process, obtains a one-sided shifted inequality, and uses preservation in the almost-everywhere invariance step (Steele 1989). The particular rationally generated event \(D_c\), its Lean declaration surface, and the RMT-32/RMT-33 division are project constructions, not definitions attributed to Steele. Kingman’s original paper remains the primary source for the full subadditive ergodic theorem that this sequence of milestones is rebuilding (Kingman 1968).

Thirty-six solved exercises

Exercise 1: unpack the fixed-margin event

What does \(\omega\in A_q\) say?

Solution. For every natural cutoff \(N\), there is a natural \(n\ge N\) with \(n\gt0\) and \(Y_n(\omega)\lt qn\). The witness may depend on \(N\), but the slope \(q\) is fixed.

Exercise 2: compare arbitrarily late and eventually always

Does \(\omega\in A_q\) imply that every sufficiently large length is bad?

Solution. No. It only supplies at least one bad length beyond each cutoff. Good lengths may occur between an unbounded subsequence of bad lengths.

Exercise 3: recover a once-bad witness

Why does \(A_q\subseteq B_\infty(q)\)?

Solution. Apply the arbitrarily-late condition at cutoff zero. It returns one positive \(n\) satisfying the strict inequality, which is exactly the once-bad membership witness.

Exercise 4: retain positive time

Why is \(0\lt n\) stated separately from \(N\le n\)?

Solution. The cutoff may be zero, so \(N\le n\) alone permits \(n=0\). The slope interpretation and later division by \(n\) require positive time.

Exercise 5: unpack the target event

What does \(\omega\in D_c\) add to fixed-margin membership?

Solution. It supplies one rational \(q\lt c\) such that \(\omega\in A_q\). The rational choice is made once and survives all future cutoffs.

Exercise 6: reject drifting thresholds

May one choose a new \(q_N\lt c\) for every cutoff?

Solution. Not in \(D_c\). Such choices could approach \(c\) and encode no uniform gap. The existential rational quantifier sits outside the universal cutoff quantifier.

Exercise 7: test the approaching-target sequence

For \(z_n=c-1/(n+1)\), why does the same-threshold condition hold?

Solution. The correction \(1/(n+1)\) is positive, so \(z_n\lt c\) for every \(n\). In particular there is a witness beyond every cutoff at the target \(c\).

Exercise 8: show that no durable lower margin survives

Fix \(q\lt c\) in Exercise 7. Why are sufficiently late terms above \(q\)?

Solution. Let \(\varepsilon=c-q\gt0\). Eventually \(1/(n+1)\lt\varepsilon\), so \(z_n=c-1/(n+1)\gt c-\varepsilon=q\). Thus \(A_q\) fails.

Exercise 9: use rational density

Suppose a real \(d\lt c\) is visited arbitrarily late by normalized slopes. How can a rational margin record the gap?

Solution. Choose \(q\in\mathbb Q\) with \(d\lt q\lt c\). Every witness with normalized slope at most \(d\) is strictly below \(q\), so the same unbounded witness sequence certifies \(A_q\).

Exercise 10: explain countability

Why not take the union over all real \(q\lt c\)?

Solution. Null-measurable sets are closed under countable unions, not arbitrary uncountable unions. Rational density preserves every strict real gap while keeping the outer union countable.

Exercise 11: prove threshold monotonicity

If \(q\le r\), why is \(A_q\subseteq A_r\)?

Solution. Reuse every witness. Positive \(n\) gives \(qn\le rn\), so \(Y_n\lt qn\le rn\).

Exercise 12: embed the strict event into RMT-31

Why is \(D_c\subseteq B_\infty(c)\)?

Solution. Choose \(q\lt c\), then take a positive witness from \(A_q\) at cutoff zero. Positivity gives \(qn\lt cn\), so the same length witnesses membership in \(B_\infty(c)\).

Exercise 13: rearrange the endpoint inequality

Show that \(qn\lt r(n+1)\) is equivalent to \(-r\lt(r-q)n\).

Solution. Expand the right side as \(rn+r\), subtract \(qn\), and move \(r\) to the other side. Both transformations preserve strict inequality because they only add or subtract equal real quantities.

Exercise 14: choose the arithmetic cutoff

Why does \(q\lt r\) provide a natural \(K\) that makes Exercise 13 true for all \(n\ge K\)?

Solution. Since \(r-q\gt0\), it suffices that \(n\gt(-r)/(r-q)\). The Archimedean property supplies a natural number above that real bound, and every larger natural also works.

Exercise 15: remove sign assumptions

Must \(q\) and \(r\) be negative in the arithmetic lemma?

Solution. No. Only \(r-q\gt0\) is used. The quotient \((-r)/(r-q)\) and the Archimedean cutoff handle every sign of \(r\).

Exercise 16: derive the centered one-step inequality

Which split of shifted subadditivity gives \(Y_{n+1}(\omega)\le Y_n(T\omega)\)?

Solution. Use the split \(1+n\): \(Y_{1+n}(\omega)\le Y_n(T\omega)+Y_1(\omega)\). Centering gives \(Y_1=0\), and \(1+n=n+1\).

Exercise 17: orient the preimage correctly

What does \(\omega\in T^{-1}A_q\) mean?

Solution. It means \(T\omega\in A_q\). The proof begins with later witnesses at the shifted state and pulls them back to blocks one unit longer at \(\omega\).

Exercise 18: satisfy two cutoffs at once

Why request the shifted witness beyond \(\max(N,K)\)?

Solution. The witness must be beyond the user’s requested cutoff \(N\) and beyond the arithmetic cutoff \(K\). The maximum enforces both inequalities with one natural number.

Exercise 19: explain threshold relaxation

Why does the proof conclude \(T^{-1}A_q\subseteq A_r\) rather than \(T^{-1}A_q\subseteq A_q\)?

Solution. Pulling a witness back changes its length from \(n\) to \(n+1\). For negative \(q\), the comparison \(qn\lt q(n+1)\) is false. A strictly larger \(r\) supplies the margin that absorbs the endpoint.

Exercise 20: close the target event

How does rational density turn relaxed fixed-slope inclusions into \(T^{-1}D_c\subseteq D_c\)?

Solution. Start with a rational \(q\lt c\) witnessing shifted membership. Choose rational \(r\) with \(q\lt r\lt c\). Transport from \(A_q\) to \(A_r\), which is still one of the events in the union defining \(D_c\).

Exercise 21: build fixed-margin regularity

Which set operations appear in \(A_q\)?

Solution. There is a countable intersection over cutoffs and countable unions over witness lengths and their logical guards. Each terminal strict threshold set is null measurable, so Mathlib’s countable closure theorems assemble the result.

Exercise 22: keep the regularity claim narrow

Does the theorem prove that \(A_q\) and \(D_c\) are ordinary measurable sets?

Solution. Not in the chosen representative-level interface. It proves null measurability, which permits disagreement with a measurable set on a null subset.

Exercise 23: locate finite mass in regularity

Is finite total mass needed to prove null measurability?

Solution. No. Countable closure and almost-everywhere measurability of the centered process values do not require \(\mu(\Omega)\lt\infty\).

Exercise 24: turn preservation into equal event mass

Once \(D_c\) is null measurable, what does measure preservation give?

Solution. It gives \(\mu(T^{-1}D_c)=\mu(D_c)\). This is equality of extended nonnegative real numbers, not yet equality of sets.

Exercise 25: locate finite mass in almost-invariance

Why is finite mass needed after Exercise 24?

Solution. With \(T^{-1}D_c\subseteq D_c\), equal finite measures force the difference to be null. If both measures were infinite, equality would not exclude a positive or infinite remainder.

Exercise 26: distinguish almost and literal invariance

What exactly does the theorem conclude?

Solution. It concludes that the indicator memberships of \(T^{-1}D_c\) and \(D_c\) agree almost everywhere. The underlying sets may differ on a null set.

Exercise 27: state the finite-measure ergodic fork

What does ergodicity add after almost-invariance?

Solution. It forces \(D_c\) to be almost equal either to the empty set or to the whole space. Probability normalization is not required for this set-level dichotomy.

Exercise 28: convert the fork under probability

Why does a probability measure turn the alternatives into zero and one?

Solution. Almost equality preserves measure. The empty set has measure zero and the whole space has total measure one under IsProbabilityMeasure.

Exercise 29: force the sign of the rate

Why does the uniform rate premise imply \(\delta\le0\)?

Solution. Evaluate it at \(n=1\). Since \(Y_1=0\), the normalized integral is zero, so the premise reads \(\delta\le0\).

Exercise 30: force the sign of the target

Why is \(c\lt0\)?

Solution. The hypothesis gives \(c\lt\delta\), and Exercise 29 gives \(\delta\le0\). Transitivity yields \(c\lt0\).

Exercise 31: obtain the strict ratio

Why does \(c\lt\delta\) imply \(\delta/c\lt1\) when \(c\lt0\)?

Solution. Multiplication by the negative denominator reverses the inequality. The statement \(\delta/c\lt1\) is equivalent to \(c\lt\delta\), exactly the assumed strict ordering.

Exercise 32: separate the strict estimate from ergodicity

Does \(\mu_{\mathbb R}(D_c)\lt1\) require ergodicity?

Solution. No. It follows from inclusion into the RMT-31 once-bad event and the finite-measure ratio. Ergodicity enters only when converting almost-invariance into an empty-or-full fork.

Exercise 33: diagnose the nonergodic two-point model

Why can the invariant event \(\{\texttt{false}\}\) have mass \(1/2\)?

Solution. The identity map preserves every subset, but the equal two-point system is not ergodic. Invariance alone imposes no zero-one law.

Exercise 34: diagnose the half-mass one-point model

Why does a full event of real mass \(1/2\lt1\) not contradict the strict estimate?

Solution. The whole space itself has mass \(1/2\). Without probability normalization, “full” does not mean mass one, so a subunit estimate cannot exclude that branch.

Exercise 35: reject the one-shot shortcut

Why is the collapse-model point once-bad at \(-2/5\) but absent from the strict event?

Solution. Length two gives the strict finite witness, but later normalized values equal \(-1/n\) and approach zero. No fixed rational slope below \(-2/5\) receives witnesses beyond every cutoff.

Exercise 36: name the next proof obligation

What remains before a lower-liminf theorem can use RMT-32?

Solution. RMT-33 proves the guarded implication and equivalence bridges between strict lower-limit deviation and the rationally generated event using the pinned Mathlib filter and lower-limit APIs. It then combines the null event with the existing upper-limsup and additive Birkhoff results. RMT-32 itself proves neither step.

Full project check

After installing the repository’s pinned dependencies, run this from the repository root:

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

This command may compile substantial parts of the pinned Mathlib graph and therefore may require substantial disk space and memory. The Standalone tutorial above remains the lighter route for following the finite arithmetic interactively. The paired Development Notebook contains the source-order proof ledger, compiled boundary inventory, and axiom reports.

Continue the learning path

From Finite Centered Bad-Block Bounds to All-Positive-Length Control explains the RMT-31 once-bad union and finite-target measure projection.

Finite Bad-Block Measure Bounds Before Kingman Lower Liminf derives the finite-cap ratio that selects the RMT-32 null branch.

Subadditive Upper-Limsup Bounds Before Kingman Convergence develops the upper half later combined with this event architecture. Continue to The Guarded Real-Liminf Bridge to Log-Positive Kingman Convergence for that completed assembly.

Ergodicity reviews invariant-event rigidity, and ergodic probability base separates preservation, total-mass normalization, and ergodicity.

References

The library links below target Mathlib 4.32.0 at pinned commit 81a5d257c8e410db227a6665ed08f64fea08e997.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499-510, 1968, doi:10.1111/j.2517-6161.1968.tb00749.x. This is the version-of-record page for the full subadditive ergodic theorem; RMT-32 proves only its countable lower-deviation event layer.

J. Michael Steele. Kingman’s subadditive ergodic theorem, Annales de l’Institut Henri Poincare, Probabilites et Statistiques 25(1), 93-98, 1989. The archival PDF shows the centered-process and one-sided-shift architecture on page 94. The rational event in this chapter is a repository adaptation, not a source-defined object.

Mathlib contributors. Countable unions and intersections of null-measurable sets, Mathlib 4.32.0. These closures assemble \(A_q\) and \(D_c\).

Mathlib contributors. Null measurability of strict order events for almost-everywhere measurable functions, Mathlib 4.32.0. RMT-32 applies this to a centered process value and a constant threshold.

Mathlib contributors. A natural number above any Archimedean value, Mathlib 4.32.0. This theorem supplies the endpoint-absorption cutoff.

Mathlib contributors. A rational number strictly between two real numbers, Mathlib 4.32.0. This density step restores the target event after threshold relaxation.

Mathlib contributors. Measure of a null-measurable preimage under a measure-preserving map, Mathlib 4.32.0. It equates the masses of \(D_c\) and its preimage.

Mathlib contributors. Almost-everywhere equality from inclusion and reverse measure comparison, Mathlib 4.32.0. The finite-target premise is the exact almost-invariance gate.

Mathlib contributors. Almost-empty or almost-full rigidity for a null-measurable almost-invariant set, Mathlib 4.32.0. RMT-32 applies the quasi-ergodic form after proving almost-invariance.

Mathlib contributors. Monotonicity of real-valued measure under a finite target, Mathlib 4.32.0. It transfers the RMT-31 ceiling along \(D_c\subseteq B_\infty(c)\).

Mathlib contributors. Division below one with a negative denominator, Mathlib 4.32.0. It turns \(c\lt\delta\) and \(c\lt0\) into the strict ratio \(\delta/c\lt1\).