Orbit-Majorant Centering for Subadditive Processes

Begin with a three-state orbit

Take the finite base space

and let \(T\) move clockwise:

Give every state probability \(1/3\). The map preserves this measure because it permutes equally weighted atoms. Every subset is measurable, and every real-valued function on this finite discrete space is measurable.

Define the one-step values

Their one-step expectation is

The finite one-step orbit sum is

Now define the complete process by subtracting a deterministic penalty:

This is not circular. The right side uses the already specified one-step function \(X_1\); the penalty vanishes at \(n=1\), so the formula reproduces the three one-step values exactly.

Finally, subtract the one-step orbit sum:

For this model,

at every state. The residual is zero at horizons zero and one, then strictly negative.

Why this process is genuinely subadditive

The orbit sum has the exact shifted addition law

The penalty satisfies

Subtract the second identity from the first:

So this is an exact shifted-subadditive process. The gap in the inequality is \(2mn\), independent of the state.

Read the finite horizon ledger

The first five horizons are:

The target theorem calls \(S_n\) a majorant because

pointwise. In this model the difference is exactly \(n(n-1)\).

At horizon three, the finite normalized split is especially transparent:

This is an equality of three finite numbers. It does not assert that any sequence converges as \(n\) grows.

Measurability and integrability are visible here

On this finite probability space, the integral of a function \(f:\Omega\to\mathbb R\) is

Integrability asks for a finite integral of the absolute value:

At horizon three,

All are finite. The same reasoning works at every fixed horizon because each function is a finite list of finite real numbers.

This small model separates three interfaces:

• measurability says the values can be used in measure-theoretic events and integrals;
• integrability says the absolute integral is finite; and
• measure preservation says orbit shifts do not distort the underlying measure.

The general Lean theorem cannot use “finite list” as its proof. Instead, the candidate supplies integrability of every \(X_n\), and measure preservation transports integrability of \(X_1\) to \(X_1\circ T^j\). Finite-sum closure then proves the Birkhoff sum integrable. Subtracting two integrable real functions proves the centered horizon integrable.

No probability normalization is required by the module. The uniform probability measure only makes this example and its expectations concrete.

The shift is determined by the early block

Now use the same model to split horizon three as

starting at state \(\omega=2\).

The early block has length one:

After consuming it, the later block begins at

The correct later value is

The shifted-subadditive theorem therefore reads

The gap is \(4=2mn\), exactly as the process formula predicted.

The orbit majorant splits with equality:

The exponent on \(T\) is \(m\), the length of the early block. It is not the length \(n\) of the later block.

A wrong shift that actually breaks the inequality

If one mistakenly starts the later block at \(T^n\omega=T^2(2)=1\), then

The false calculation becomes

which is wrong. This is more than an aesthetic indexing complaint: the incorrect shift produces a false theorem on a three-point example.

Two other seductive meanings of “centered”

The project definition subtracts majorant from process:

Reversing the subtraction gives \(S_3-X_3=+6\), destroying the nonpositivity conclusion.

Subtracting the expectation of \(X_1\) is a different legitimate operation:

That vector has mean zero, but it is neither identically zero nor pointwise nonpositive. The project theorem is not expectation centering. It is pointwise compensation by an additive orbit majorant.

Choose a route up

Learning objectives

By the summit, you should be able to reproduce the three-state ledger; prove its shifted subadditivity with exact slack \(2mn\); explain why the correct later start is \(T^m\omega\); distinguish orbit-majorant and expectation centering; read seven Lean bridges token by token; execute the bounded Std worksheet; explain how preservation transports integrability; reconstruct centered subadditivity by cancellation; audit all eighteen public declarations and two private helpers; and state precisely which normalized, ergodic, cocycle, and Lyapunov conclusions remain absent.

In Lean: seven bridges from orbit slack to the cocycle

Bridge one: subtract the finite one-step Birkhoff sum

centeredProcess T X n ω

The simplification theorems say centeredProcess T X 0 = X 0 and centeredProcess T X 1 = 0. At time zero the Birkhoff sum is empty; at time one it is exactly \(X_1\).

Bridge two: majorize every positive horizon

hX.oneStepBirkhoffMajorant_of_ne_zero n hn ω

Bridge three: turn the majorant into a sign theorem

hX.centeredProcess_nonpos hX0 n ω

Bridge four: preserve the shifted-subadditive structure

hX.centeredProcess_add_le m n ω

Bridge five: preserve finite-horizon integrability

hX.integrable_centeredProcess hT n

The companion hX.centeredProcess_candidate hT packages both this integrability field and bridge four into a new process candidate.

Bridge six: split the normalized finite value

normalized_eq_centered_add_birkhoffAverage n ω

Bridge seven: specialize the reduction to cocycle positive-log growth

C.centeredLogPlusNormObservable_nonpos n ω

Check the exact project interface

import NonlinearDynamics.Random.RandomCocycles.SubadditiveCentering

open NonlinearDynamics.Random.RandomCocycles

#print centeredProcess
#check centeredProcess_zero
#check centeredProcess_one
#check IsIntegrableSubadditiveProcessCandidate.oneStepBirkhoffMajorant_of_ne_zero
#check IsIntegrableSubadditiveProcessCandidate.oneStepBirkhoffMajorant
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_nonpos_of_ne_zero
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_nonpos
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_add_le
#check IsIntegrableSubadditiveProcessCandidate.integrable_centeredProcess
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_candidate
#check normalized_eq_centered_add_birkhoffAverage
#check DiscreteMatrixCocycle.birkhoffSum_logPlusNormObservable_one_eq_orbitLogPlusSum
#print DiscreteMatrixCocycle.centeredLogPlusNormObservable
#check DiscreteMatrixCocycle.centeredLogPlusNormObservable_apply
#check DiscreteMatrixCocycle.centeredLogPlusNormObservable_nonpos
#check DiscreteMatrixCocycle.centeredLogPlusNormObservable_add_le
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.centeredLogPlusNormObservable_candidate
#check DiscreteMatrixCocycle.logPlusNormObservable_normalized_eq_centered_add_birkhoffAverage

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

Type the entire ledger with Lean and Std

The project theorem uses Mathlib’s Birkhoff sums, measures, integrability, and cocycle interfaces. The complete finite arithmetic can be checked first by a bounded file that imports only Std.

Create a scratch directory outside formalization/. Save this exact block as OrbitMajorantCenteringTutorial.lean:

import Std

namespace OrbitMajorantCenteringTutorial

/-
Three equally weighted states form the cycle 0 → 1 → 2 → 0.
The one-step process values are 9, 1, and 2.

The finite process is deliberately subadditive:

  X_n(ω) = S_n(ω) - n(n - 1),

where S_n is the orbit sum of the one-step values.  Its centered residual is
therefore Y_n(ω) = -n(n - 1).
-/

def nextState (state : Nat) : Nat :=
  (state + 1) % 3

def iterateState (steps state : Nat) : Nat :=
  (state + steps) % 3

def oneStep (state : Nat) : Int :=
  match state % 3 with
  | 0 => 9
  | 1 => 1
  | _ => 2

def orbitSum (state horizon : Nat) : Int :=
  ((List.range horizon).map
    (fun j => oneStep (iterateState j state))).sum

def penalty (horizon : Nat) : Int :=
  (horizon : Int) * ((horizon : Int) - 1)

def process (state horizon : Nat) : Int :=
  orbitSum state horizon - penalty horizon

def oneStepMajorant (state horizon : Nat) : Int :=
  ((List.range horizon).map
    (fun j => process (iterateState j state) 1)).sum

def centered (state horizon : Nat) : Int :=
  process state horizon - oneStepMajorant state horizon

def processVector (horizon : Nat) : List Int :=
  (List.range 3).map (fun state => process state horizon)

def majorantVector (horizon : Nat) : List Int :=
  (List.range 3).map (fun state => oneStepMajorant state horizon)

def centeredVector (horizon : Nat) : List Int :=
  (List.range 3).map (fun state => centered state horizon)

def uniformMean (values : List Int) : Rat :=
  (values.sum : Rat) / values.length

def uniformAbsoluteMean (values : List Int) : Rat :=
  (((values.map Int.natAbs).sum : Nat) : Rat) / values.length

structure HorizonLedger where
  horizon : Nat
  majorant : List Int
  process : List Int
  centered : List Int
  processMean : Rat
  centeredAbsoluteMean : Rat
  deriving Repr, DecidableEq

def horizonLedger (horizon : Nat) : HorizonLedger :=
  { horizon := horizon
    majorant := majorantVector horizon
    process := processVector horizon
    centered := centeredVector horizon
    processMean := uniformMean (processVector horizon)
    centeredAbsoluteMean := uniformAbsoluteMean (centeredVector horizon) }

structure ShiftLedger where
  start : Nat
  earlyLength : Nat
  laterLength : Nat
  fullProcess : Int
  earlyProcess : Int
  correctLaterStart : Nat
  correctLaterProcess : Int
  correctRightSide : Int
  correctInequality : Bool
  wrongLaterStart : Nat
  wrongLaterProcess : Int
  wrongRightSide : Int
  wrongInequality : Bool
  fullMajorant : Int
  correctMajorantPieces : Int × Int
  wrongMajorantPieces : Int × Int
  deriving Repr, DecidableEq

def shiftLedger : ShiftLedger :=
  let state := 2
  let m := 1
  let n := 2
  let full := process state (m + n)
  let early := process state m
  let correctStart := iterateState m state
  let correctLater := process correctStart n
  let correctRight := correctLater + early
  let wrongStart := iterateState n state
  let wrongLater := process wrongStart n
  let wrongRight := wrongLater + early
  { start := state
    earlyLength := m
    laterLength := n
    fullProcess := full
    earlyProcess := early
    correctLaterStart := correctStart
    correctLaterProcess := correctLater
    correctRightSide := correctRight
    correctInequality := decide (full ≤ correctRight)
    wrongLaterStart := wrongStart
    wrongLaterProcess := wrongLater
    wrongRightSide := wrongRight
    wrongInequality := decide (full ≤ wrongRight)
    fullMajorant := oneStepMajorant state (m + n)
    correctMajorantPieces :=
      (oneStepMajorant state m, oneStepMajorant correctStart n)
    wrongMajorantPieces :=
      (oneStepMajorant state m, oneStepMajorant wrongStart n) }

def wrongSignCentered (state horizon : Nat) : Int :=
  oneStepMajorant state horizon - process state horizon

def expectationCenteredOneStep (state : Nat) : Int :=
  process state 1 - 4

def unshiftedRepeatedCentering (state horizon : Nat) : Int :=
  process state horizon - (horizon : Int) * process state 1

def constantOneProcess (_state _horizon : Nat) : Int :=
  1

def constantOneCentered (horizon : Nat) : Int :=
  constantOneProcess 0 horizon -
    ((List.range horizon).map
      (fun _ => constantOneProcess 0 1)).sum

def normalizedHorizonThree : Rat × Rat × Rat :=
  ((process 0 3 : Rat) / 3,
    (centered 0 3 : Rat) / 3,
    (oneStepMajorant 0 3 : Rat) / 3)

#eval (List.range 3).map oneStep
#eval (List.range 5).map horizonLedger
#eval shiftLedger
#eval (List.range 3).map (fun state => wrongSignCentered state 3)
#eval (List.range 3).map expectationCenteredOneStep
#eval (centered 2 3, unshiftedRepeatedCentering 2 3)
#eval (List.range 4).map constantOneCentered
#eval normalizedHorizonThree

example : (List.range 3).map oneStep = [9, 1, 2] := by
  native_decide

example : majorantVector 2 = [10, 3, 11] := by native_decide
example : processVector 2 = [8, 1, 9] := by native_decide
example : centeredVector 2 = [-2, -2, -2] := by native_decide

example : majorantVector 3 = [12, 12, 12] := by native_decide
example : processVector 3 = [6, 6, 6] := by native_decide
example : centeredVector 3 = [-6, -6, -6] := by native_decide

example : (List.range 9).all fun horizon =>
    (List.range 3).all fun state =>
      decide (process state horizon ≤ oneStepMajorant state horizon) := by
  native_decide

example : shiftLedger.correctLaterStart = 0 := by native_decide
example : shiftLedger.correctRightSide = 10 := by native_decide
example : shiftLedger.correctInequality = true := by native_decide
example : shiftLedger.wrongLaterStart = 1 := by native_decide
example : shiftLedger.wrongRightSide = 3 := by native_decide
example : shiftLedger.wrongInequality = false := by native_decide
example : shiftLedger.correctMajorantPieces = (2, 10) := by native_decide
example : shiftLedger.wrongMajorantPieces = (2, 3) := by native_decide

example : uniformAbsoluteMean (processVector 3) = 6 := by native_decide
example : uniformAbsoluteMean (centeredVector 3) = 6 := by native_decide
example : normalizedHorizonThree = (2, -2, 4) := by native_decide

example : (List.range 3).map expectationCenteredOneStep = [5, -3, -2] := by
  native_decide

example : (List.range 4).map constantOneCentered = [1, 0, -1, -2] := by
  native_decide

end OrbitMajorantCenteringTutorial

Open a terminal in that scratch directory and type:

source "$HOME/.elan/env"
elan run leanprover/lean4:v4.32.0 lean OrbitMajorantCenteringTutorial.lean

Resource label: small standalone Lean tutorial, ordinary Mac or Linux. This exact worksheet was executed with Lean 4.32.0 and printed this complete transcript:

[9, 1, 2]
[{ horizon := 0,
   majorant := [0, 0, 0],
   process := [0, 0, 0],
   centered := [0, 0, 0],
   processMean := 0,
   centeredAbsoluteMean := 0 },
 { horizon := 1,
   majorant := [9, 1, 2],
   process := [9, 1, 2],
   centered := [0, 0, 0],
   processMean := 4,
   centeredAbsoluteMean := 0 },
 { horizon := 2,
   majorant := [10, 3, 11],
   process := [8, 1, 9],
   centered := [-2, -2, -2],
   processMean := 6,
   centeredAbsoluteMean := 2 },
 { horizon := 3,
   majorant := [12, 12, 12],
   process := [6, 6, 6],
   centered := [-6, -6, -6],
   processMean := 6,
   centeredAbsoluteMean := 6 },
 { horizon := 4,
   majorant := [21, 13, 14],
   process := [9, 1, 2],
   centered := [-12, -12, -12],
   processMean := 4,
   centeredAbsoluteMean := 12 }]
{ start := 2,
  earlyLength := 1,
  laterLength := 2,
  fullProcess := 6,
  earlyProcess := 2,
  correctLaterStart := 0,
  correctLaterProcess := 8,
  correctRightSide := 10,
  correctInequality := true,
  wrongLaterStart := 1,
  wrongLaterProcess := 1,
  wrongRightSide := 3,
  wrongInequality := false,
  fullMajorant := 12,
  correctMajorantPieces := (2, 10),
  wrongMajorantPieces := (2, 3) }
[6, 6, 6]
[5, -3, -2]
(-6, 0)
[1, 0, -1, -2]
(2, -2, 4)

The first line is the one-step function. The next record list is the complete horizon-zero-through-four ledger. The shift record contains both the valid right side \(10\) and invalid right side \(3\), with the corresponding Boolean checks. The remaining lines expose the wrong sign, expectation centering, unshifted repeated subtraction, the constant-one time-zero boundary, and the normalized triple \(2,-2,4\).

The example declarations state all recorded values as propositions that Lean’s kernel checks. The nested Boolean check additionally verifies \(X_n\le S_n\) at all three states for horizons zero through eight. This worksheet models the finite arithmetic only. Mathlib’s actual birkhoffSum, MeasurePreserving, Integrable, and cocycle interfaces remain the full project check above.

Why the generic theorem works

The candidate separates algebra from analysis

The predecessor defines IsIntegrableSubadditiveProcessCandidate T μ X with exactly two fields:

integrable : ∀ k, Integrable (X k) μ
add_le : ∀ m n ω, X (m + n) ω ≤ X n (T^[m] ω) + X m ω

The structure does not store probability normalization, measure preservation, ergodicity, invertibility, or a limit. Measure preservation is requested only when a theorem actually pulls functions along the base orbit.

Positive-horizon majorization is pure induction

For \(n=1\), the Birkhoff sum contains only \(X_1(\omega)\), so the bound is equality. For the successor, shifted subadditivity gives

Apply the induction hypothesis to the second term and use Mathlib’s successor identity

Only the candidate’s add_le field is read. The private helper oneStepBirkhoffMajorant_of_add_le makes that dependency explicit.

At \(n=0\), the Birkhoff sum is zero while subadditivity alone only forces \(X_0\ge0\). Exact normalization \(X_0=0\) is therefore a separate premise for the uniform theorem.

The constant-one boundary

On a singleton, let \(X_n=1\) for every \(n\). Then

so the process is subadditive and every horizon is integrable. Its centered values are

Positive horizons are nonpositive, but \(Y_0=1\). This model is a counterexample to the uniform nonpositivity theorem with the X 0 = 0 premise removed.

Centered subadditivity is cancellation

Let \(A_n\) denote the Birkhoff sum of \(X_1\). Mathlib proves

Subtract this equality from

Regrouping produces

The source’s first private helper, centeredProcess_add_le_of_add_le, performs exactly this rewrite and finishes with linear arithmetic. It needs neither integrability nor time-zero normalization.

Integrability uses preservation at one narrow gate

The candidate already says \(X_n\) and \(X_1\) are integrable. If \(T\) preserves \(\mu\), then every iterate \(T^j\) preserves \(\mu\), so

is integrable. The finite Birkhoff sum is integrable by finite-sum closure. Then

is integrable by closure under subtraction.

Without preservation, composition can move mass into a heavy part of an integrable function and destroy integrability. The premise is analytic, not decorative.

The complete eighteen-declaration map

The source contains two private raw-algebra helpers and eighteen public declarations.

Private helpers in source order

Public declarations in source order

Declarations 4 through 10 are methods in the IsIntegrableSubadditiveProcessCandidate namespace. Declarations 12 through 18 live in the DiscreteMatrixCocycle namespace.

The cocycle specialization is intentionally thin

For a discrete matrix cocycle, the earlier module defines

and its one-step orbit sum

The target proves by reflexivity that this \(S_n\) is Mathlib’s birkhoffSum with the same base, range, and iterate convention. It then defines

The earlier pointwise majorant \(P_n\le S_n\) immediately yields \(Y_n^C\le0\), including time zero because \(P_0=0\). The earlier shifted subadditivity of \(P_n\) feeds the raw centering helper and proves shifted subadditivity of \(Y^C\).

These pointwise facts need no HasIntegrableGeneratorLogPlus. That hypothesis enters only when declaration 17 packages every centered horizon as integrable.

The cocycle normalized identity is

It remains a finite equality. Positive log has already clipped contraction, so the residual cannot reconstruct signed logarithmic growth, inverse norms, or an Oseledets splitting.

Edge cases that determine the theorem statements

Time zero is totalized, not ignored

Mathlib’s real division and Birkhoff average are total at zero:

Therefore declaration 11 is algebraically true at \(n=0\). This does not make \(X_0/0\) a classical growth rate; it records Lean’s totalized field operations.

Candidate packaging does not need \(X_0=0\)

The centered candidate needs integrability and shifted subadditivity. Neither field asks for nonpositivity or a normalized time-zero value. The constant-one model has \(Y_0=1\) and still forms a valid centered candidate.

The zero measure is allowed

The generic module assumes an arbitrary measure. Under the zero measure, every measurable real-valued function is integrable and the identity map preserves the measure. No probability instance is used.

Empty matrix dimension is allowed

The cocycle layer assumes a finite matrix index type but not a nonempty one. In empty dimension the positive-log observable and its orbit sum are both zero, so the centered cocycle process is zero.

Additive processes are the zero-residual boundary

If \(X_n\) already equals the Birkhoff sum of \(X_1\), then \(Y_n=0\). The normalized identity reduces to

That still does not force the orbit average to converge. One can build a single binary orbit with alternating blocks whose lengths dominate everything before them; its empirical averages have subsequences near zero and one.

Exercises from foothill to summit

Foothill

1. Starting at each state, compute \(S_2\) and recover \([10,3,11]\).
2. Subtract \(2(2-1)\) and recover \(X_2=[8,1,9]\).
3. Verify \(Y_2=[-2,-2,-2]\).
4. Compute the three absolute means at horizon three.
5. Check \(2=-2+4\) in the normalized horizon-three split.
6. Explain why every function in the ledger is measurable.

Ridge

7. Prove the exact penalty identity with the \(2mn\) cross term.
8. Derive shifted subadditivity for the three-state process.
9. Recompute the \(m=1,n=2,\omega=2\) correct split.
10. Replace \(T^m\omega\) by \(T^n\omega\) and identify the false inequality.
11. Prove the Birkhoff addition law by dividing the index range into its first \(m\) and next \(n\) terms.
12. Reconstruct positive-horizon majorization by induction.
13. Use the constant-one process to refute uniform nonpositivity without \(X_0=0\).
14. Explain why expectation centering has mean zero but does not prove the target sign theorem.

Summit

15. Translate integrable_centeredProcess into its three closure operations.
16. Audit all eighteen public declarations and identify which proof fields each consumes.
17. Explain why the normalized identity has no analytic premises.
18. Build an additive process whose normalized orbit sum fails to converge.
19. State the additional assumptions and theorem needed to obtain an almost-everywhere Birkhoff limit.
20. State the stronger assumptions needed for a subadditive ergodic limit.
21. Explain why the cocycle-centered positive-log process cannot recover negative logarithmic growth.
22. Describe what a derivative-cocycle bridge would need before this scalar reduction could speak about nonlinear dynamics.

Reproduce the chapter

The bounded Std worksheet above is a standalone tutorial for an ordinary macOS or Linux host. The target module imports Mathlib and is a full project check. From the repository root, run:

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

This command may require substantial disk space and memory. Passing automated checks would still leave human mathematical, source, accessibility, scientific-integrity, and editorial review pending.

Summit: what has and has not been proved

The strongest justified summary is finite: subtracting the exact additive one-step orbit route exposes a nonpositive residual, preserves the shifted-subadditive structure, and, under measure preservation, preserves finite-horizon integrability. The normalized split prepares later arguments but proves no limit.

Where to continue

Finite Block Decomposition for Subadditive Processes is the immediate predecessor. It develops exact block-and-remainder bounds; the present one-step majorant is the block-length-one reduction.

Orbit-Majorant Centering Before Any Ergodic Limit is the Development Notebook companion that follows the Lean implementation and records its boundary probes.

The orbit-majorant centering glossary entry gives the compact operational definition. The Birkhoff sum entry isolates the finite orbit convention.

Finite Phase Averaging for Nonpositive Subadditive Processes is the immediate finite successor. It averages shifted block bounds across residue phases. It remains finite combinatorics, not an almost-everywhere theorem.

References

Mathlib contributors. Birkhoff sums, Mathlib 4 documentation. The exact pinned source defines the finite sum and its zero, one, successor, and shifted addition laws.

Mathlib contributors. Birkhoff averages, Mathlib 4 documentation. The pinned definition records the totalized finite average used by the normalized identity.

Mathlib contributors. Measure-preserving maps, Mathlib 4 documentation. This is the analytic interface used to transport integrability along the orbit.

Mathlib contributors. Integrable functions, Mathlib 4 documentation. The pinned source supplies composition under measure preservation and closure under finite sums and subtraction.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499–510, 1968. This is primary asymptotic context. RMT-19 proves a finite reduction only.

Steven P. Lalley. Kingman’s Subadditive Ergodic Theorem, University of Chicago lecture notes, undated, accessed 2026-07-21. These notes serve only as a teaching guide to later proof architecture.

Anders Karlsson and Gregory A. Margulis. A Multiplicative Ergodic Theorem and Nonpositively Curved Spaces, Communications in Mathematical Physics 208, 107–123, 1999. This paper is a later geometric destination. Its almost-sure tracking theorem is not used or formalized here.

The exact upstream revision audited for this chapter is Mathlib commit 81a5d257, the revision pinned by formalization/lake-manifest.json.