Log-Positive Kingman Convergence from Rational Lower Deviations in Lean

For reusable vocabulary, see limit inferior , limit superior , Birkhoff sums , orbit-majorant centering , ergodic probability bases , the integrated log-positive growth rate , one-sided discrete matrix cocycles , and almost-everywhere statements . The companion textbook chapter is The Guarded Real-Liminf Bridge to Log-Positive Kingman Convergence.

Orientation: the missing endpoint is a guarded bridge

RMT-32 proved that rationally generated strict centered lower-deviation events are null below the centered Fekete offset. That theorem did not yet identify those events with a real lower-limit statement. RMT-33 performs that translation, but only after stating the conditional-completeness guard that the real codomain requires.

The whole milestone can be read as five interfaces:

1. normalize every natural time, including zero;
2. connect rational frequent crossings with a real lower limit under the correct one-sided boundedness assumptions;
3. build a countable null cover below the desired target and recover an actual eventual lower bound off that cover;
4. add the convergent one-step Birkhoff average back to the centered process;
5. combine the lower endpoint with RMT-29’s upper endpoint for the log-positive cocycle observable.

The immediate predecessor is Countably Generated Centered Lower-Deviation Events in Lean. The complementary upper endpoint is Subadditive Upper Limsup from Phase Averaging in Lean, and the additive convergence input is Identifying the Ergodic Birkhoff Constant in Lean.

Prior work, this milestone’s contribution, and exact nonclaims

Prior work. Kingman’s 1968 paper is the primary historical source for the subadditive ergodic theorem (Kingman 1968). Steele’s 1989 account gives a short centering-based route through the subadditive argument (Steele 1989). Birkhoff’s original ergodic theorem is the historical source for the additive average used when centering is reversed (Birkhoff 1931). The formal endpoint here is narrower than the broadest classical formulations: it is tailored to the project’s real-valued process interfaces and then specialized to a nonnegative log-positive matrix observable.

This milestone’s formal contribution. RMT-33:

• defines total normalized original and centered processes;
• proves that replacing the time-zero slice changes no normalized value;
• records finite-prefix invariance of real liminf along natural time;
• translates arbitrarily-late bad blocks into Frequently normalized inequalities;
• proves the rational event to lower-liminf implication under an eventual lower bound;
• proves the reverse implication from the candidate’s pointwise upper ceiling;
• exposes an exact guarded equivalence between the event and real strict lower-liminf deviation;
• covers a strict lower-liminf event by countably many RMT-32 events at genuinely smaller rational targets;
• proves both that cover and the lower-liminf deviation event are null;
• extracts an almost-everywhere eventual lower bound from the complement of the same cover;
• adds the one-step Birkhoff integral to the centered lower estimate;
• specializes the lower endpoint to the integrated log-positive growth rate; and
• combines lower liminf, upper limsup, and explicit boundedness gates into almost-everywhere convergence.

Not claimed. The module does not prove the full classical Kingman theorem for arbitrary signed real subadditive processes. It does not assert an unconditional equivalence between \(D_c\) and \(\liminf u_n\lt c\); the event-to-liminf direction requires eventual lower boundedness. It makes no extended-real lower-limit claim for unbounded-below sequences. It proves no convergence in \(L^1\), in probability, or uniformly, and no rate or concentration inequality. It performs no limit-integral interchange and does not identify an expectation of the samplewise limit. It proves no signed logarithmic growth, negative-tail estimate, inverse-cocycle control, Lyapunov exponent, Lyapunov spectrum, Oseledets filtration, or Oseledets splitting. It assumes no powered-map ergodicity, mixing, or independence. It draws no nonlinear-stability, bifurcation, or physical-chaos conclusion.

The positive endpoint is precise: on a probability base, bundled preservation plus PreErgodic dynamics and one-step log-positive integrability give almost-everywhere convergence of the normalized log-positive norm observable. The theorem remains valid for an empty finite matrix index.

Total normalization and the finite-prefix boundary

For a real process \(X:\mathbb N\to\Omega\to\mathbb R\), the module defines

In Lean, real division is total. At \(n=0\), the denominator is zero and the quotient evaluates to zero. Thus normalizedProcess X 0 ω forgets X 0 ω completely. This is a useful total API, but the note does not claim that the zero-time quotient carries asymptotic information.

Two facts make the convention safe:

• replacing X 0 by any function leaves the total normalized process pointwise unchanged; and
• liminf_nat_add removes any fixed finite prefix, so starting at time one gives the same real lower limit as starting at time zero.

The exact centering identity is also total:

At time zero both normalized terms are zero. The identity is formally true there, though its mathematical content belongs to positive time.

The event bridge has asymmetric boundedness gates

Fix a point \(\omega\) and abbreviate

RMT-32’s fixed-slope event is exactly

The positive witness in the original set definition is important. In the forward direction it permits division by \(n\gt0\). In the reverse direction, a frequent witness is requested beyond max N 1, which reconstructs both the cutoff and positivity conditions.

The rational event \(D_c\) is therefore equivalent to the existence of a rational \(q\lt c\) crossed frequently. From event membership to \(\liminf u_n\lt c\), Mathlib’s liminf_le_of_frequently_le requires

an actual eventual lower bound.

The reverse direction uses a different gate. Candidate centered subadditivity gives \(u_n\le0\) for every \(n\), including the separate zero-time case. This pointwise upper ceiling implies the coboundedness condition required by frequently_lt_of_liminf_lt. A rational \(q\) between the real lower limit and \(c\) then supplies the event witness.

This asymmetry is the central design decision of the module. Hiding the lower bound inside an informal appeal to the usual extended-real meaning of liminf would make the statement stronger than Mathlib’s real-valued API justifies.

Why the proof chooses two rational cuts

Suppose the real lower limit \(L(\omega)\) satisfies \(L(\omega)\lt\delta\). RMT-32 proves nullity only for events whose target is strictly below the integral offset \(\delta\). Substituting \(\delta\) itself would demand the false premise \(\delta\lt\delta\).

RMT-33 chooses an outer rational target \(c\) with

The lower-limit-to-event theorem then proves membership in \(D_c\). Inside that theorem, rational density chooses an inner witness \(q\) with

The two cuts have distinct scopes. The outer cut places the point in a member of a countable null cover indexed below \(\delta\). The inner cut witnesses the strict rational event at that outer target.

The outer exhaustion is

Every member event has measure zero by RMT-32, so the countable union is null. The strict lower-liminf deviation set is a subset of \(E_\delta\), hence null by monotonicity.

The totalized real lower limit needs a countermodel

The guard is not merely an artifact of a difficult proof. Consider the genuine subadditive candidate on Unit

Its centered process relative to \(X_1=-1\) is

and for positive time

The values escape to negative infinity. The point belongs to \(D_{-1}\), and there is no eventual lower bound. Yet the module proves that Mathlib’s totalized real liminf for this normalized sequence is zero. Internally, the set of real eventual lower bounds is empty and Real.sSup_empty is zero.

This example does not say that the extended-real lower limit is zero. It says the opposite lesson: a total real-valued operation can return a conventional value when the conditional-completeness side conditions fail. The module therefore returns boundedness together with its almost-everywhere real lower-liminf estimate.

One null cover delivers two outputs

Off \(E_\delta\), choose rationals \(q\lt c\lt\delta\). Since the point is not in \(D_c\), it cannot cross \(q\) frequently. The negation of frequent strict inequality becomes an eventual weak inequality:

Thus \(q\) is an actual eventual lower bound. Independently, the complement of the strict lower-liminf deviation set gives \(\delta\le\liminf u_n\). Both bad sets are null, so their almost-everywhere intersection returns the pair

Adding back the one-step Birkhoff average

Write \(u_n\) for the normalized centered process and \(v_n\) for the one-step Birkhoff average. The exact identity gives the original normalized process as \(u_n+v_n\). Ergodic Birkhoff convergence supplies

The lower-limit addition theorem used by Lean is deliberately explicit about boundedness. The centered sequence has the almost-everywhere eventual lower bound just constructed and a pointwise upper bound of zero. The convergent Birkhoff sequence supplies its own lower and upper boundedness data. Therefore

Since the Birkhoff lower limit equals its limit, the generic original-process endpoint is

The log-positive cocycle endpoint

For a discrete matrix cocycle \(C\), the generic candidate is C.logPlusNormObservable. Choose

RMT-30 supplies this value as a lower bound for every positive normalized centered integral. Adding the one-step integral cancels the subtraction, so the generic theorem becomes

almost everywhere.

RMT-29 supplies the matching almost-everywhere upper endpoint

The normalized log-positive sequence is nonnegative, which supplies its eventual lower bound. The one-step Birkhoff majorant bounds it eventually above by a convergent sequence, which supplies its eventual upper bound. Mathlib’s tendsto_of_le_liminf_of_limsup_le then yields convergence.

The theorem assumes PreErgodic C.base μ, not a separate preservation hypothesis, because the cocycle structure already bundles C.base_preserving. The proof combines them locally into Ergodic C.base μ.

Public declaration surface in exact source order

The module exports twenty-four declarations. The signatures below are the public interface in source order. Each code block is an interface excerpt; proof bodies remain in the checked Lean source.

1. normalizedProcess

def normalizedProcess {Ω : Type uΩ} (X : ℕ → Ω → ℝ)
    (n : ℕ) (ω : Ω) : ℝ :=
  X n ω / (n : ℝ)

Defines the total positive-time normalization and fixes the zero-time value by total real division.

2. normalizedProcess_zero

@[simp] theorem normalizedProcess_zero
    {Ω : Type uΩ} (X : ℕ → Ω → ℝ) (ω : Ω) :
    normalizedProcess X 0 ω = 0

Records the time-zero convention as a simplification theorem.

3. normalizedProcess_update_zero

@[simp] theorem normalizedProcess_update_zero
    {Ω : Type uΩ} (X : ℕ → Ω → ℝ) (z : Ω → ℝ) :
    normalizedProcess (Function.update X 0 z) = normalizedProcess X

Shows that the total normalized process is pointwise insensitive to the entire time-zero slice.

4. normalizedCenteredProcess

def normalizedCenteredProcess {Ω : Type uΩ} (T : Ω → Ω)
    (X : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ :=
  normalizedProcess (centeredProcess T X) n ω

Names the total normalization of the orbit-majorant-centered process.

5. normalizedCenteredProcess_zero

@[simp] theorem normalizedCenteredProcess_zero
    {Ω : Type uΩ} (T : Ω → Ω) (X : ℕ → Ω → ℝ) (ω : Ω) :
    normalizedCenteredProcess T X 0 ω = 0

Keeps the centered zero-time boundary visible at the named API.

6. liminf_normalizedProcess_succ

theorem liminf_normalizedProcess_succ
    {Ω : Type uΩ} (X : ℕ → Ω → ℝ) (ω : Ω) :
    liminf (fun n ↦ normalizedProcess X (n + 1) ω) atTop =
      liminf (fun n ↦ normalizedProcess X n ω) atTop

Uses liminf_nat_add to prove that dropping the time-zero prefix changes no real lower limit.

7. normalized_eq_normalizedCenteredProcess_add_birkhoffAverage

theorem normalized_eq_normalizedCenteredProcess_add_birkhoffAverage
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    (n : ℕ) (ω : Ω) :
    normalizedProcess X n ω = normalizedCenteredProcess T X n ω +
      birkhoffAverage ℝ T (X 1) n ω

Exposes the exact pointwise decomposition used when the centered estimate is transferred back to the original process.

8. mem_centeredArbitrarilyLateBadBlockSet_iff_frequently_normalized_lt

theorem mem_centeredArbitrarilyLateBadBlockSet_iff_frequently_normalized_lt
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    {q : ℝ} {ω : Ω} :
    ω ∈ centeredArbitrarilyLateBadBlockSet T X q ↔
      ∃ᶠ n in atTop, normalizedCenteredProcess T X n ω < q

Translates the beyond-every-cutoff set into filter language while preserving the positive-time boundary.

9. mem_centeredStrictLowerDeviationSet_iff_exists_frequently_normalized_lt

theorem mem_centeredStrictLowerDeviationSet_iff_exists_frequently_normalized_lt
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    {c : ℝ} {ω : Ω} :
    ω ∈ centeredStrictLowerDeviationSet T X c ↔
      ∃ q : ℚ, (q : ℝ) < c ∧
        ∃ᶠ n in atTop, normalizedCenteredProcess T X n ω < (q : ℝ)

Makes the fixed rational margin in \(D_c\) explicit.

10. liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet

theorem liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    {c : ℝ} {ω : Ω}
    (hlower : IsBoundedUnder (· ≥ ·) atTop
      (fun n ↦ normalizedCenteredProcess T X n ω))
    (hω : ω ∈ centeredStrictLowerDeviationSet T X c) :
    liminf (fun n ↦ normalizedCenteredProcess T X n ω) atTop < c

Provides the guarded event-to-liminf implication. The lower-bound premise is mathematically necessary for the real-valued liminf API.

11. centeredRationalLowerDeviationExhaustionSet

def centeredRationalLowerDeviationExhaustionSet {Ω : Type uΩ}
    (T : Ω → Ω) (X : ℕ → Ω → ℝ) (δ : ℝ) : Set Ω :=
  ⋃ c : {c : ℚ // (c : ℝ) < δ},
    centeredStrictLowerDeviationSet T X (c : ℝ)

Defines the countable outer cover whose event targets are all genuinely below \(\delta\).

12. mem_centeredRationalLowerDeviationExhaustionSet_iff

@[simp] theorem mem_centeredRationalLowerDeviationExhaustionSet_iff
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    {δ : ℝ} {ω : Ω} :
    ω ∈ centeredRationalLowerDeviationExhaustionSet T X δ ↔
      ∃ c : ℚ, (c : ℝ) < δ ∧
        ω ∈ centeredStrictLowerDeviationSet T X (c : ℝ)

Exposes one outer rational target and its RMT-32 event membership.

13. centeredLowerLiminfDeviationSet

def centeredLowerLiminfDeviationSet {Ω : Type uΩ}
    (T : Ω → Ω) (X : ℕ → Ω → ℝ) (δ : ℝ) : Set Ω :=
  {ω | liminf (fun n ↦ normalizedCenteredProcess T X n ω) atTop < δ}

Names the strict real lower-liminf deviation set without claiming that it is measurable by definition.

14. mem_centeredLowerLiminfDeviationSet_iff

@[simp] theorem mem_centeredLowerLiminfDeviationSet_iff
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    {c : ℝ} {ω : Ω} :
    ω ∈ centeredLowerLiminfDeviationSet T X c ↔
      liminf (fun n ↦ normalizedCenteredProcess T X n ω) atTop < c

Provides the definitional membership interface.

15. IsIntegrableSubadditiveProcessCandidate.normalizedCenteredProcess_nonpos

theorem normalizedCenteredProcess_nonpos
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (n : ℕ) (ω : Ω) : normalizedCenteredProcess T X n ω ≤ 0

Turns centered candidate subadditivity into the pointwise upper ceiling used by the reverse event bridge.

16. IsIntegrableSubadditiveProcessCandidate.mem_centeredStrictLowerDeviationSet_of_liminf_normalizedCenteredProcess_lt

theorem mem_centeredStrictLowerDeviationSet_of_liminf_normalizedCenteredProcess_lt
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    {c : ℝ} {ω : Ω}
    (hlim : liminf (fun n ↦ normalizedCenteredProcess T X n ω) atTop < c) :
    ω ∈ centeredStrictLowerDeviationSet T X c

Chooses a rational between the real lower limit and the target, using the pointwise upper ceiling as Mathlib’s coboundedness gate.

17. IsIntegrableSubadditiveProcessCandidate.mem_centeredStrictLowerDeviationSet_iff_liminf_normalizedCenteredProcess_lt

theorem mem_centeredStrictLowerDeviationSet_iff_liminf_normalizedCenteredProcess_lt
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    {c : ℝ} {ω : Ω}
    (hlower : IsBoundedUnder (· ≥ ·) atTop
      (fun n ↦ normalizedCenteredProcess T X n ω)) :
    ω ∈ centeredStrictLowerDeviationSet T X c ↔
      liminf (fun n ↦ normalizedCenteredProcess T X n ω) atTop < c

Packages the two directions as an equivalence under the stated boundedness guard.

18. IsIntegrableSubadditiveProcessCandidate.centeredLowerLiminfDeviationSet_subset_rationalExhaustion

theorem centeredLowerLiminfDeviationSet_subset_rationalExhaustion
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X) (δ : ℝ) :
    centeredLowerLiminfDeviationSet T X δ ⊆
      centeredRationalLowerDeviationExhaustionSet T X δ

Chooses the outer rational cut and delegates the inner cut to declaration 16.

19. IsIntegrableSubadditiveProcessCandidate.measure_centeredRationalLowerDeviationExhaustionSet_eq_zero

theorem measure_centeredRationalLowerDeviationExhaustionSet_eq_zero
    [IsProbabilityMeasure μ]
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (hT : Ergodic T μ) (δ : ℝ)
    (hδ : ∀ n : ℕ, n ≠ 0 →
      δ ≤ (∫ ω, centeredProcess T X n ω ∂μ) / (n : ℝ)) :
    μ (centeredRationalLowerDeviationExhaustionSet T X δ) = 0

Uses measure_iUnion_null and invokes RMT-32 at each subtype index \(c\lt\delta\).

20. IsIntegrableSubadditiveProcessCandidate.measure_centeredLowerLiminfDeviationSet_eq_zero

theorem measure_centeredLowerLiminfDeviationSet_eq_zero
    [IsProbabilityMeasure μ]
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (hT : Ergodic T μ) (δ : ℝ)
    (hδ : ∀ n : ℕ, n ≠ 0 →
      δ ≤ (∫ ω, centeredProcess T X n ω ∂μ) / (n : ℝ)) :
    μ (centeredLowerLiminfDeviationSet T X δ) = 0

Combines declaration 18 with declaration 19 by measure_mono_null.

21. IsIntegrableSubadditiveProcessCandidate.ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess

theorem ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess
    [IsProbabilityMeasure μ]
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (hT : Ergodic T μ) (δ : ℝ)
    (hδ : ∀ n : ℕ, n ≠ 0 →
      δ ≤ (∫ ω, centeredProcess T X n ω ∂μ) / (n : ℝ)) :
    ∀ᵐ ω ∂μ,
      IsBoundedUnder (· ≥ ·) atTop
          (fun n ↦ normalizedCenteredProcess T X n ω) ∧
        δ ≤ liminf
          (fun n ↦ normalizedCenteredProcess T X n ω) atTop

Returns the actual eventual lower bound and the real lower-liminf inequality together.

22. IsIntegrableSubadditiveProcessCandidate.ae_add_oneStepIntegral_le_liminf_normalized

theorem ae_add_oneStepIntegral_le_liminf_normalized
    [IsProbabilityMeasure μ]
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (hT : Ergodic T μ) (δ : ℝ)
    (hδ : ∀ n : ℕ, n ≠ 0 →
      δ ≤ (∫ ω, centeredProcess T X n ω ∂μ) / (n : ℝ)) :
    ∀ᵐ ω ∂μ,
      δ + ∫ x, X 1 x ∂μ ≤
        liminf (fun n ↦ normalizedProcess X n ω) atTop

Adds the convergent one-step Birkhoff average and transports the centered lower bound to the original process.

23. DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_integratedLogPlusGrowthRate_le_liminf_normalized

theorem HasIntegrableGeneratorLogPlus.ae_integratedLogPlusGrowthRate_le_liminf_normalized
    [IsProbabilityMeasure μ]
    {C : DiscreteMatrixCocycle (ι := ι) μ}
    (hC : C.HasIntegrableGeneratorLogPlus) (hT : PreErgodic C.base μ) :
    ∀ᵐ ω ∂μ,
      C.integratedLogPlusGrowthRate hC ≤
        liminf
          (fun n ↦ normalizedProcess C.logPlusNormObservable n ω) atTop

Specializes declaration 22 at the centered Fekete offset and cancels the one-step integral.

24. DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_tendsto_normalizedLogPlusNormObservable

theorem HasIntegrableGeneratorLogPlus.ae_tendsto_normalizedLogPlusNormObservable
    [IsProbabilityMeasure μ]
    {C : DiscreteMatrixCocycle (ι := ι) μ}
    (hC : C.HasIntegrableGeneratorLogPlus) (hT : PreErgodic C.base μ) :
    ∀ᵐ ω ∂μ,
      Tendsto
        (fun n ↦ normalizedProcess C.logPlusNormObservable n ω) atTop
        (𝓝 (C.integratedLogPlusGrowthRate hC))

Intersects the lower endpoint, RMT-29’s upper endpoint, and Birkhoff convergence, then discharges the two boundedness gates for the final squeeze.

Complete local proof-step ledger

Private support surface in exact source order

Private declarations are not part of the importable API, but they are part of the audited proof artifact. There are eleven, in this order.

The first helper is logically central. It is private because the public pair theorem is the safer endpoint: callers receive the boundedness certificate and the lower-limit inequality together. The remaining ten declarations make the boundary audits compact and reproducible without widening the production API.

Five checked boundary examples in exact source order

The third and fourth examples diagnose different possible overstatements. The approach-to-zero example shows why frequent crossing of the target itself is weaker than a rationally exhausted strict event. The quadratic example shows why even genuine rational event membership does not control a totalized real lower limit without eventual lower boundedness.

Exact complete source-order map

This linear map interleaves public declarations, private support, anonymous examples, and the final axiom reports exactly as they occur in the 627-line module.

The source map counts twenty-four public declarations, eleven private support items, five anonymous examples, and eleven axiom reports.

Lean engineering notes

IsBoundedUnder and IsCoboundedUnder are not cosmetic dual names

With relation (· ≥ ·), IsBoundedUnder supplies a real value that is eventually below the sequence. That is the lower-bound gate needed by liminf_le_of_frequently_le. With the same written relation, IsCoboundedUnder expresses the upper-side conditional-completeness gate used by frequently_lt_of_liminf_lt. The candidate’s pointwise estimate \(u_n\le0\) produces the latter, not the former.

Negating frequency is the constructive lower-bound move

Once \(q\) is fixed, Lean can transform

¬ ∃ᶠ n in atTop, u n < q

into an eventual statement by not_frequently.mp. A monotonicity step turns the resulting pointwise negation into q ≤ u n. Packaging that witness gives IsBoundedUnder (· ≥ ·) atTop u. This is stronger and more reusable than a bare proof that the real lower limit happens not to be below \(\delta\).

The outer union uses a subtype index

The definition indexes over

{c : ℚ // (c : ℝ) < δ}

rather than over all rationals plus an empty branch. Each index therefore carries the strict hypothesis needed by RMT-32. measure_iUnion_null receives that proof as c.property, and no endpoint case is generated.

liminf_congr separates asymptotic identity from syntactic identity

The normalized centered-plus-Birkhoff identity is pointwise at every natural time, but the sum is introduced through local abbreviations. liminf_congr lets the proof identify the functions eventually, avoiding fragile unfolding of both abstractions inside a large calc chain.

PreErgodic is the unbundled logical half needed at the cocycle boundary

The generic process theorem assumes Ergodic T μ, which packages measure preservation and pre-ergodicity. A DiscreteMatrixCocycle already stores preservation of its base map. The public cocycle theorem therefore asks only for PreErgodic C.base μ and builds the combined structure locally.

Axiom audit

The module ends with eleven #print axioms commands. A warning-fatal direct check of the final source reports the same standard Mathlib trio for every printed theorem:

[propext, Classical.choice, Quot.sound]

The eleven printed declarations, in source order, are:

1. normalizedProcess_update_zero
2. liminf_normalizedProcess_succ
3. mem_centeredArbitrarilyLateBadBlockSet_iff_frequently_normalized_lt
4. liminf_normalizedCenteredProcess_lt_of_mem_centeredStrictLowerDeviationSet
5. IsIntegrableSubadditiveProcessCandidate.mem_centeredStrictLowerDeviationSet_of_liminf_normalizedCenteredProcess_lt
6. IsIntegrableSubadditiveProcessCandidate.centeredLowerLiminfDeviationSet_subset_rationalExhaustion
7. IsIntegrableSubadditiveProcessCandidate.measure_centeredLowerLiminfDeviationSet_eq_zero
8. IsIntegrableSubadditiveProcessCandidate.ae_isBoundedUnder_ge_and_le_liminf_normalizedCenteredProcess
9. IsIntegrableSubadditiveProcessCandidate.ae_add_oneStepIntegral_le_liminf_normalized
10. DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_integratedLogPlusGrowthRate_le_liminf_normalized
11. DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.ae_tendsto_normalizedLogPlusNormObservable

This report rules out hidden sorry declarations in the printed dependency closures. It does not replace review of whether the formal definitions match the intended mathematics.

Reproduce the Lean and teaching artifacts

From the repository root, load the pinned Elan environment and check the leaf module with warnings treated as errors:

cd formalization
. "$HOME/.elan/env"
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomCocycles/SubadditiveKingman.lean

Build the whole formalization:

cd formalization
. "$HOME/.elan/env"
lake build

Regenerate and verify the deterministic social card from any working directory:

site/content/development-notebook/2026/07/\
log-positive-kingman-convergence-from-rational-lower-deviations-in-lean/\
generate-card.sh

site/content/development-notebook/2026/07/\
log-positive-kingman-convergence-from-rational-lower-deviations-in-lean/\
generate-card.sh --verify

magick identify -format '%wx%h\n' \
  site/content/development-notebook/2026/07/\
log-positive-kingman-convergence-from-rational-lower-deviations-in-lean/\
log-positive-kingman-convergence-from-rational-lower-deviations-in-lean-card.png

The expected dimensions are 1200x630. Validate the generator and all eight conceptual SVGs when the optional tools are installed:

shellcheck \
  site/content/development-notebook/2026/07/\
log-positive-kingman-convergence-from-rational-lower-deviations-in-lean/\
generate-card.sh

xmllint --noout \
  site/content/development-notebook/2026/07/\
log-positive-kingman-convergence-from-rational-lower-deviations-in-lean/*.svg

Run the teaching-source gate and render every draft page in memory:

python3 scripts/check_teaching_source_hygiene.py
hugo --source site --config hugo.yaml --buildDrafts \
  --panicOnWarning --noBuildLock --renderToMemory

The repository-wide content-coverage check is intentionally separate from this bundle. Its manifest is updated with the coherent milestone integration, not by this isolated page artifact.

Exercises with worked solutions

Exercise 1: evaluate the total zero-time normalization

Why does normalizedProcess X 0 ω not depend on X 0 ω?

Solution. The definition is X 0 ω / (0 : ℝ). Division in a field is total, with division by zero reducing to multiplication by the inverse of zero. Since that inverse is zero, the quotient simplifies to zero for every numerator. This is a formal convention, not a claim that a time-zero growth rate is analytically meaningful.

Exercise 2: prove update insensitivity without filter theory

Sketch the two cases needed to prove that updating X at time zero leaves normalizedProcess X unchanged as a function.

Solution. Apply function extensionality to a horizon \(n\) and point \(\omega\). If \(n=0\), both normalized values simplify to zero. If \(n\ne0\), Function.update returns the original slice, and both quotients are definitionally the same. No asymptotic theorem is needed because the result is pointwise at every horizon.

Exercise 3: distinguish update insensitivity from prefix invariance

Why is declaration 6 still useful after declaration 3?

Solution. Declaration 3 concerns only a replacement at index zero and is an equality of total normalized functions. Declaration 6 says that shifting the entire sequence by one index leaves its lower limit unchanged. The latter is a filter fact and would also ignore any other finite prefix after an appropriate natural shift.

Exercise 4: translate one bad-block witness

Assume \(n\gt0\) and \(Y_n(\omega)\lt qn\). Derive the normalized inequality used by the frequent-crossing event.

Solution. The cast \((n:\mathbb R)\) is positive. Divide both sides by that positive number, which preserves strict order, to obtain \(Y_n(\omega)/n\lt q\). In Lean the relevant equivalence is div_lt_iff₀, and the positivity proof is Nat.cast_pos.mpr hn.

Exercise 5: recover positivity from frequency

Why does the reverse event bridge query a frequent predicate at max N 1 instead of at \(N\)?

Solution. A witness beyond max N 1 is automatically beyond the caller’s cutoff \(N\) and at least one. The first fact reconstructs the beyond-every-cutoff quantifier, while the second makes division or multiplication by the cast horizon order-safe. Querying only at \(N\) would leave the case \(N=0,n=0\) unresolved.

Exercise 6: compare strict target crossing with a fixed margin

For \(a_n=-1/n\), explain why \(a_n\lt0\) frequently but no fixed rational \(q\lt0\) satisfies \(a_n\lt q\) frequently.

Solution. Every positive-time value is negative, so strict crossing of zero occurs beyond every cutoff. But \(a_n\to0\). For fixed \(q\lt0\), the tail eventually lies strictly above \(q\), which makes \(a_n\lt q\) eventually false and therefore not frequent. This is why \(D_0\) encodes a fixed strict margin rather than raw frequent crossing of the target.

Exercise 7: identify the event-to-liminf gate

Which hypothesis permits liminf_le_of_frequently_le to turn frequent weak crossing of \(q\) into \(\liminf u_n\le q\)?

Solution. It needs IsBoundedUnder (· ≥ ·) atTop u, an eventual real lower bound for the sequence. This ensures the set of eventual lower bounds is nonempty in the conditionally complete real order. Event membership alone supplies frequent upper comparisons, not this lower boundedness.

Exercise 8: identify the lower-limit-to-event gate

Why is the candidate estimate \(u_n\le0\) useful in the reverse direction?

Solution. frequently_lt_of_liminf_lt needs a coboundedness condition on the relevant real family. The pointwise ceiling zero supplies it uniformly. After choosing rational \(q\) with \(\liminf u_n\lt q\lt c\), the theorem produces frequent \(u_n\lt q\), exactly the witness required for \(D_c\).

Exercise 9: reject an unconditional equivalence

State the smallest visible change that would make the guarded equivalence mathematically false in this module’s real-valued semantics.

Solution. Remove the hlower : IsBoundedUnder (· ≥ ·) atTop u premise. The quadratic boundary process then belongs to \(D_{-1}\) but has formal real lower limit zero, so the implication from membership to a lower limit below \(-1\) fails. Candidate subadditivity does not repair this because it gives an upper bound, not a lower bound.

Exercise 10: choose the outer rational cut

Given \(L\lt\delta\), what strict inequalities must the outer rational \(c\) satisfy, and what job does each side perform?

Solution. Choose \(L\lt c\lt\delta\). The left inequality lets the lower-limit-to-event theorem place the point in \(D_c\). The right inequality meets RMT-32’s strict threshold hypothesis and makes \(D_c\) one of the null events in the outer exhaustion.

Exercise 11: locate the inner rational cut

Where does the second rational \(q\) appear after the outer target \(c\) has already been chosen?

Solution. It appears inside mem_centeredStrictLowerDeviationSet_of_liminf_normalizedCenteredProcess_lt. That theorem chooses \(q\) with \(L\lt q\lt c\) and proves frequent crossing of \(q\). Thus \(c\) indexes the countable cover, while \(q\) witnesses membership in its selected event.

Exercise 12: audit countability

Why is the subtype {c : ℚ // (c : ℝ) < δ} preferable to an outer union over all real numbers below \(\delta\)?

Solution. The subtype is countable because the rationals are countable, so measure_iUnion_null applies directly. Rational density loses no strict gap: every lower limit strictly below \(\delta\) admits an intermediate rational target. A union over reals would not provide the same countable measure interface.

Exercise 13: transfer nullity through a subset

Which two facts suffice to prove that the strict lower-liminf deviation set is null?

Solution. First prove it is a subset of the rational exhaustion. Then prove the exhaustion has measure zero by a countable union of RMT-32 null events. measure_mono_null transfers the zero measure to the subset without requiring an independent measurability proof for the lower-liminf set.

Exercise 14: compute the quadratic centered process

For \(X_n=-n^2\) and one-step observable \(X_1=-1\), compute \(Y_n=X_n-S_n(X_1)\).

Solution. On the identity action over Unit, the Birkhoff sum of the constant one-step value \(-1\) is \(-n\). Therefore \(Y_n=-n^2-(-n)=-n^2+n\). At positive time the normalized value is \(-n+1=-(n-1)\).

Exercise 15: verify quadratic subadditivity

Reduce \(X_{m+n}\le X_m+X_n\) for \(X_n=-n^2\) to a nonnegative product.

Solution. Expanding gives \(-(m+n)^2\le-m^2-n^2\), equivalent to \(2mn\ge0\). Natural-number casts are nonnegative, so their product is nonnegative. The Lean proof records the cast facts and lets nlinarith close the polynomial inequality.

Exercise 16: explain the formal quadratic lower limit

Why does Mathlib’s real liminf evaluate to zero for the positive-time sequence \(-n\)?

Solution. The real liminf is expressed as the supremum of real eventual lower bounds. No real \(a\) is eventually below every \(-n\), so that set is empty. Mathlib totalizes the supremum of the empty real set as Real.sSup_empty = 0, producing zero despite negative escape.

Exercise 17: avoid an extended-real misreading

What would be wrong with reporting the previous result as saying that the ordinary asymptotic lower limit of \(-n\) is zero?

Solution. In the extended reals the sequence tends to negative infinity, so its extended lower limit is negative infinity. The value zero belongs only to the totalized real operation outside its conditional-completeness regime. The boundary example documents API semantics, not a new analytic convention.

Exercise 18: construct an eventual lower bound off the cover

Suppose \(\omega\notin D_c\) and \(q\lt c\). Show why \(q\le u_n(\omega)\) eventually.

Solution. If \(u_n(\omega)\lt q\) were frequent, the rational witness \(q\) would put \(\omega\) in \(D_c\), contradicting the premise. Therefore the strict inequality is not frequent. The filter identity for negated frequency gives eventual failure of that inequality, equivalent over reals to eventual \(q\le u_n(\omega)\).

Exercise 19: distinguish a witness from its enclosing target

Could the helper choose only one rational below \(\delta\) and use it both as the fixed lower bound and as the target of the same strict event?

Solution. No. Membership in \(D_c\) requires a rational witness strictly below \(c\). To infer a contradiction from frequent crossing at \(q\), the helper needs \(q\lt c\). A second inequality \(c\lt\delta\) places that event inside the null exhaustion. The two values encode the strict slack explicitly.

Exercise 20: justify returning a pair

Why does the public centered endpoint return boundedness together with \(\delta\le\liminf u_n\)?

Solution. The numerical inequality alone could be misread as an extended-real conclusion even where Mathlib’s real liminf is totalized. Returning IsBoundedUnder certifies that an eventual real lower bound exists at the same sample point. The pair is also exactly what the later addition theorem needs.

Exercise 21: obtain the centered upper gate

Which bound supplies IsBoundedUnder (· ≤ ·) atTop u in the add-back proof?

Solution. Declaration 15 gives \(u_n\le0\) for every natural \(n\). The constant zero is therefore a global upper bound, hence an eventual upper bound. This is independent of the almost-everywhere lower bound extracted from the rational cover.

Exercise 22: obtain both Birkhoff gates

Why does convergence of \(v_n\) supply the lower and upper boundedness data required by le_liminf_add?

Solution. Every convergent real sequence is eventually bounded below and above. Mathlib exposes these as properties of the Tendsto proof. The add-back theorem uses the lower property directly and converts the upper property into the coboundedness form expected by the lower-limit addition API.

Exercise 23: read the direction of le_liminf_add

Why is \(\liminf u+\liminf v\le\liminf(u+v)\) the direction needed here?

Solution. The centered theorem gives a lower bound on \(\liminf u\), and Birkhoff convergence identifies \(\liminf v\). Adding these known lower bounds gives a lower bound on their sum. The displayed theorem then transfers that quantity below the lower limit of the original normalized process.

Exercise 24: separate pointwise and lower-limit equality

What does liminf_congr contribute after the exact centering identity is already known?

Solution. The proof has locally named functions \(u\) and \(v\), while the goal names normalizedProcess X. liminf_congr accepts eventual pointwise equality between those function expressions. The exact identity proves that eventual equality at every index without forcing broad definitional unfolding.

Exercise 25: cancel the cocycle offset

Show algebraically why the generic lower endpoint becomes the integrated log-positive growth rate.

Solution. Substitute \(\delta=g-I_1\), where \(g\) is the integrated growth rate and \(I_1\) is the one-step integrated log-positive norm. The generic left side is \((g-I_1)+I_1=g\). Lean closes this with sub_add_cancel after unfolding the one-step integral notation.

Exercise 26: assemble cocycle ergodicity

Why does the cocycle-facing theorem assume PreErgodic rather than the full Ergodic structure?

Solution. The cocycle structure already bundles that its base map preserves \(\mu\). PreErgodic supplies the remaining invariant-set rigidity. The proof constructs ⟨C.base_preserving, hT⟩, avoiding a duplicated preservation assumption at the public endpoint.

Exercise 27: produce the final lower boundedness gate

Why is the normalized log-positive observable bounded below even at time zero?

Solution. The numerator logPlusNormObservable is nonnegative, and every natural cast denominator is nonnegative. Real division of two nonnegative values is nonnegative. At zero, total division produces zero, so the same pointwise lower bound holds uniformly across all horizons.

Exercise 28: produce the final upper boundedness gate

How does the one-step Birkhoff majorant lead to eventual upper boundedness of the normalized cocycle observable?

Solution. At every positive horizon, divide the finite-horizon majorant by the positive cast horizon to compare the normalized observable with the one-step Birkhoff average. The comparison is eventual because horizons are eventually at least one. The Birkhoff average converges, hence is eventually bounded above, and boundedness transfers through the eventual comparison.

Exercise 29: state the four final squeeze inputs

List the hypotheses consumed by tendsto_of_le_liminf_of_limsup_le in the final theorem.

Solution. The integrated rate is below the real lower limit; the real upper limit is below the same integrated rate; the sequence is eventually bounded above; and it is eventually bounded below. The first two identify a single candidate limit. The latter two ensure the totalized real lower and upper limits are operating in their intended conditionally complete regime.

Exercise 30: audit the empty-index boundary

Which part of the final statement excludes ι := Empty?

Solution. None. The index type needs Fintype and DecidableEq, both of which exist for Empty. The checked anonymous example instantiates the final theorem directly. The endpoint therefore does not require a nonempty matrix-dimension hypothesis.

Exercise 31: reject a signed Lyapunov conclusion

Why does convergence of normalized logPlusNormObservable not by itself produce a signed top Lyapunov exponent?

Solution. The positive part discards negative logarithmic behavior. A signed theorem would need control of the negative tail, including possible singularity or small norms, and often inverse-cocycle information. This module proves convergence only for the nonnegative envelope named in its statement.

Exercise 32: compare a possible extended-real redesign

What would an extended-real formulation change, and why is the present real formulation still useful?

Solution. An extended-real lower limit could represent negative escape directly and would alter the conditional-completeness bookkeeping. It would also require new interfaces for integration, addition, and comparison with the real Birkhoff term. The present formulation stays compatible with the existing real-valued process library and exports the eventual boundedness certificate whenever real lower-limit algebra is used.

Discussion prompts

The following are research and design questions, not claims established by RMT-33.

1. Would an EReal lower-deviation layer simplify future signed-process extensions, or merely move complexity into integration and addition?
2. Which negative-tail hypotheses are minimal for replacing logPlus by a signed logarithmic norm observable?
3. Can the generic process endpoint be strengthened to convergence without specializing to a pointwise nonnegative observable, and which explicit upper and lower boundedness witnesses would be needed?
4. Which additional uniform-integrability argument would be required before claiming \(L^1\) convergence or exchanging limit and integral?
5. How should a future multiplicative ergodic theorem layer distinguish a scalar top growth rate from a filtration or splitting theorem?

Source-backed scope notes

Kingman is cited for the historical subadditive ergodic theorem, not as a source for the exact Lean declarations or their totalized-real boundary design. Steele is cited for a centering-oriented proof architecture, not for the project’s rational subtype exhaustion or its particular API split. Birkhoff is cited for the additive ergodic theorem whose Mathlib formalization supplies the convergent one-step average. The details of liminf, conditional completeness, and the final squeeze are grounded in the pinned Mathlib source rather than in an informal convention.

The primary artifact for every formal claim is the checked module at the lean_source path in the front matter. The prose deliberately distinguishes historical motivation, project-specific theorem design, and machine-checked content.

Navigation

• Signed finite-time successor: Real Log-Norm Integrability from Forward and Inverse Tails in Lean
• Companion textbook chapter: The Guarded Real-Liminf Bridge to Log-Positive Kingman Convergence
• Previous lower-event milestone: Countably Generated Centered Lower-Deviation Events in Lean
• Complementary upper endpoint: Subadditive Upper Limsup from Phase Averaging in Lean
• Additive convergence input: Identifying the Ergodic Birkhoff Constant in Lean
• Integrated-rate construction: Integrated Log-Positive Growth and a Deterministic Fekete Limit

References

1. J. F. C. Kingman, “The Ergodic Theory of Subadditive Stochastic Processes,” Journal of the Royal Statistical Society: Series B 30(3), 499-510 (1968). Version of record. DOI.
2. J. Michael Steele, “Kingman’s Subadditive Ergodic Theorem,” Annales de l’I.H.P. Probabilités et statistiques 25(1), 93-98 (1989). Article record. PDF.
3. George D. Birkhoff, “Proof of the Ergodic Theorem,” Proceedings of the National Academy of Sciences 17(12), 656-660 (1931). DOI.
4. Mathlib contributors, Mathlib/Order/LiminfLimsup.lean, pinned project revision 81a5d257c8e410db227a6665ed08f64fea08e997. Pinned source.
5. Mathlib contributors, Mathlib/Topology/Algebra/Order/LiminfLimsup.lean, pinned project revision 81a5d257c8e410db227a6665ed08f64fea08e997. Pinned source.
6. Mathlib contributors, Mathlib/Topology/Order/LiminfLimsup.lean, pinned project revision 81a5d257c8e410db227a6665ed08f64fea08e997. Pinned source.