Finite Centered Bad-Block Measure Control in Lean

For reusable vocabulary, see orbit-majorant centering , ordered interval packing , Birkhoff sums , finite orbit-visit counts , and integrated log-positive growth rate . The textbook companion is Finite Bad-Block Measure Bounds Before Kingman Lower Liminf.

Orientation: what the theorem measures

The theorem concerns a fixed finite menu of possible witness lengths. A point \(\omega\) is bad when at least one length \(n\in\{1,\ldots,m\}\) makes the centered value \(Y_n(\omega)\) fall strictly below the line \(cn\). It does not ask whether infinitely many lengths are bad, whether the normalized process has a limit, or whether a pointwise lower liminf is controlled.

The auxiliary horizon \(H\) asks how often the first \(H\) orbit positions visit this finite bad set. Each visit supplies one witness length. RMT-21’s greedy theorem packs the resulting intervals and converts their total cost into a bound for the centered process at the enlarged horizon \(H+m\).

Prior work, contribution, and nonclaims

Prior work. Kingman’s 1968 paper is the primary historical source for the subadditive ergodic theorem (Kingman 1968). Its full argument includes a maximal-ergodic lower-bound mechanism, but the present module formalizes only one finite bad-block estimate used on the way to that destination. Steele’s 1989 paper gives an algorithmic proof based on interval decomposition (Steele 1989). Lalley’s short lecture notes present an especially close pedagogical pattern: define bad starts, select a leftmost family, and integrate the resulting contradiction (Lalley notes). Those notes are expository rather than a primary theorem source. RMT-21 supplies the repository’s checked half-open interval repair and finite packing API, while RMT-29 supplies the exact centered-integral identity used by the cocycle specialization.

Contribution. RMT-30 adds a reusable natural-valued finite orbit count, identifies its real cast with an indicator Birkhoff sum, integrates that count exactly under finite measure preservation, defines finite centered bad blocks, and composes witness choice, greedy packing, integration, and a horizon limit into the ratio estimate \(\mu(B_{m,c})\le\delta/c\). It then discharges the generic lower-rate premise for the log-positive matrix-cocycle process.

Not claimed. The module proves no lower liminf estimate, samplewise convergence, equality with an integrated rate, full Kingman theorem, \(L^1\) convergence, limit-integral interchange, powered-map ergodicity, signed logarithmic growth, Lyapunov exponent, or Oseledets splitting. It also does not replace the finite cap \(m\) by an infinite union.

Notation and sign ledger

The sign logic deserves to be read before the division. Since centeredProcess_one is zero,

The strict premise \(c\lt\delta\) therefore gives \(c\lt0\). After the proof obtains

division by the negative number \(c\) reverses the inequality and yields the advertised measure bound. The ratio \(\delta/c\) is nonnegative because both numbers are nonpositive and the denominator is strictly negative.

The proof as a finite-to-measure bridge

Step 1: count visits without measure theory

finiteOrbitVisitCount T s H ω filters Finset.range H by membership of \(T^j\omega\) in \(s\) and takes the cardinality. It is natural-valued and total at \(H=0\). Casting it to \(\mathbb R\) gives exactly

This identity is pure finite combinatorics. It has no measurable space, measure, preservation, finiteness, probability, or ergodicity premise.

Step 2: integrate visits exactly

If \(s\) is null measurable, its constant-one indicator is integrable on a finite measure space. Preservation makes every orbit translate have the same integral. Therefore

Null measurability is enough. The source deliberately avoids strengthening the requirement to ordinary measurability.

Step 3: choose one witness at every marked start

Fix \(H,m,c,\omega\). The marked starts are precisely the indices \(j\lt H\) for which \(T^j\omega\in B_{m,c}\). Membership in the finite union supplies a witness \(n\in[1,m]\) with

Classical choice selects one such length at each marked start. The proof then weakens strict inequality to a non-strict cost bound because the imported packing theorem is stated with ≤.

Step 4: invoke ordered packing pointwise

RMT-21’s le_mul_card_of_greedy_cover consumes the centered process’s shifted subadditivity, its nonpositivity away from the joint zero corner, the marked starts, and their witness lengths. When \(c\le0\) and \(H+m\ne0\), it returns

The enlargement from \(H\) to \(H+m\) is the finite tail needed to absorb a witness starting near the end of the visited window.

Step 5: integrate the pointwise packing inequality

Both sides are integrable. Monotonicity of the integral and the exact visit identity give

The lower-rate premise at \(H+m\gt0\) gives

Step 6: let the auxiliary horizon grow

For fixed \(m\),

ge_of_tendsto transfers the eventual inequalities to the limit and yields \(\delta\le c\mu(B_{m,c})\). Negative division completes the generic theorem. This is a limit in the auxiliary deterministic horizon only. It is not a samplewise limit of \(X_n/n\).

Step 7: specialize to the matrix cocycle

For a discrete matrix cocycle with an integrable generator log-positive norm, set

RMT-29’s centered-integral identity and the existing normalized-rate lower bound show that this \(\delta\) satisfies the generic premise for every positive \(n\). Declaration 9 now exposes that implication as a reusable public theorem, and declaration 10 applies it to the same ratio estimate for centeredLogPlusBadBlockSet.

Public declaration surface in exact source order

The module exports ten declarations. Namespace variables already in scope are described in prose where omitting them makes the signature easier to read.

1. finiteOrbitVisitCount

noncomputable def finiteOrbitVisitCount {Ω : Type uΩ} (T : Ω → Ω)
    (s : Set Ω) (H : ℕ) (ω : Ω) : ℕ

Counts marked starts in Finset.range H. It is noncomputable because set membership is filtered classically.

2. natCast_finiteOrbitVisitCount_eq_birkhoffSum_indicator

theorem natCast_finiteOrbitVisitCount_eq_birkhoffSum_indicator
    {Ω : Type uΩ} (T : Ω → Ω) (s : Set Ω) (H : ℕ) (ω : Ω) :
    (finiteOrbitVisitCount T s H ω : ℝ) =
      birkhoffSum T (s.indicator fun _ ↦ (1 : ℝ)) H ω

This is the combinatorial cast bridge and has no analytic hypotheses.

3. integral_finiteOrbitVisitCount

theorem integral_finiteOrbitVisitCount
    {Ω : Type uΩ} [MeasurableSpace Ω] {T : Ω → Ω} {μ : Measure Ω}
    [IsFiniteMeasure μ] (hT : MeasurePreserving T μ μ)
    {s : Set Ω} (hs : NullMeasurableSet s μ) (H : ℕ) :
    (∫ ω, (finiteOrbitVisitCount T s H ω : ℝ) ∂μ) = H * μ.real s

The natural horizon is coerced to a real scalar on the right.

4. finiteCenteredBadBlockSet

def finiteCenteredBadBlockSet {Ω : Type uΩ} (T : Ω → Ω)
    (X : ℕ → Ω → ℝ) (m : ℕ) (c : ℝ) : Set Ω :=
  ⋃ n ∈ Finset.Icc 1 m,
    {ω | centeredProcess T X n ω < c * (n : ℝ)}

The witness window is positive, finite, and inclusive at both endpoints. The sublevel comparison is strict.

5. IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_finiteCenteredBadBlockSet

theorem nullMeasurableSet_finiteCenteredBadBlockSet
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (hT : MeasurePreserving T μ μ) (m : ℕ) (c : ℝ) :
    NullMeasurableSet (finiteCenteredBadBlockSet T X m c) μ

Finite centered integrability makes each strict sublevel set null measurable; a finite binary union closes the construction.

6. IsIntegrableSubadditiveProcessCandidate.centeredProcess_le_badBlockVisitCount

theorem centeredProcess_le_badBlockVisitCount
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (H m : ℕ) (hHm : H + m ≠ 0) (c : ℝ) (hc : c ≤ 0) (ω : Ω) :
    centeredProcess T X (H + m) ω ≤
      c * (finiteOrbitVisitCount T
        (finiteCenteredBadBlockSet T X m c) H ω : ℝ)

This theorem is pointwise and purely finite after the candidate structure is available. It assumes neither a finite measure nor preservation.

7. IsIntegrableSubadditiveProcessCandidate.measureReal_finiteCenteredBadBlockSet_le_rateRatio

theorem measureReal_finiteCenteredBadBlockSet_le_rateRatio
    [IsFiniteMeasure μ]
    (hX : IsIntegrableSubadditiveProcessCandidate T μ X)
    (hT : MeasurePreserving T μ μ) (m : ℕ) (δ c : ℝ)
    (hδ : ∀ n : ℕ, n ≠ 0 →
      δ ≤ (∫ ω, centeredProcess T X n ω ∂μ) / (n : ℝ))
    (hc : c < δ) :
    μ.real (finiteCenteredBadBlockSet T X m c) ≤ δ / c

This is the generic finite-measure endpoint. No probability or ergodicity typeclass appears.

8. DiscreteMatrixCocycle.centeredLogPlusBadBlockSet

def centeredLogPlusBadBlockSet
    (C : DiscreteMatrixCocycle (ι := ι) μ) (m : ℕ) (c : ℝ) : Set Ω :=
  finiteCenteredBadBlockSet C.base C.logPlusNormObservable m c

This is a thin cocycle-facing name for the generic bad set.

9. DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.centeredFeketeOffset_le_normalizedIntegral

theorem HasIntegrableGeneratorLogPlus.centeredFeketeOffset_le_normalizedIntegral
    {C : DiscreteMatrixCocycle (ι := ι) μ}
    (hC : C.HasIntegrableGeneratorLogPlus) (n : ℕ) (hn : n ≠ 0) :
    C.integratedLogPlusGrowthRate hC - C.integratedLogPlusNorm 1 ≤
      (∫ ω, centeredProcess C.base C.logPlusNormObservable n ω ∂μ) /
        (n : ℝ)

Extracts the reusable numerical bridge from the deterministic integrated Fekete rate to every positive normalized centered integral. It uses the RMT-29 centered-integral identity and requires no finite-measure, probability, or ergodicity typeclass.

10. DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.measureReal_centeredLogPlusBadBlockSet_le_rateRatio

theorem HasIntegrableGeneratorLogPlus.measureReal_centeredLogPlusBadBlockSet_le_rateRatio
    [IsFiniteMeasure μ]
    {C : DiscreteMatrixCocycle (ι := ι) μ}
    (hC : C.HasIntegrableGeneratorLogPlus) (m : ℕ) (c : ℝ)
    (hc : c < C.integratedLogPlusGrowthRate hC -
      C.integratedLogPlusNorm 1) :
    μ.real (C.centeredLogPlusBadBlockSet m c) ≤
      (C.integratedLogPlusGrowthRate hC -
        C.integratedLogPlusNorm 1) / c

The index type needs Fintype and DecidableEq, but not Nonempty.

Complete local proof-step ledger

This ledger follows the executable source from top to bottom. It includes the named local let and have steps, plus the short tactic chains in the small declarations, so a reader can reconstruct the proof without searching the file.

Private boundary-support declarations

The source next introduces eleven private items. They are compiled support for the anonymous probes and do not enlarge the public API.

Nine compiled boundary probes in exact source order

1. Zero length cap. finiteCenteredBadBlockSet T X 0 c = ∅ because Finset.Icc 1 0 is empty.
2. Zero horizon with positive cap. The pointwise packing inequality still holds at \(H=0\) when \(m\ne0\). The right side is zero, and centered nonpositivity controls the left side.
3. Zero process with negative threshold. No positive length can satisfy \(0\lt cn\) when \(c\lt0\), so the finite bad set is empty.
4. Joint zero corner is genuinely false. For the process equal to one only at time zero, \(Y_0=1\), while the horizon-zero visit count is zero. This refutes the pointwise theorem with \(H=m=0\).
5. Zero measure. Every finite centered bad set has real measure zero, independently of the process or threshold.
6. Preserved nonergodic identity. The two-point identity is not pre-ergodic. For the process equal to −(n - 1) on one atom and zero on the other, the bad set at \(m=5\) and \(c=-3/4\) is exactly the first atom. Its measure is \(1/2\), and the generic theorem proves the genuine bound \(1/2\le(-1/2)/(-3/4)=2/3\). This exercises the ratio while compiling the absence of an ergodicity premise.
7. Strict-threshold equality. At length one and threshold zero, the centered value equals zero, so strict < marks no point.
8. Finite-measure rescaling. A mass-two measure on Unit satisfies the theorem. Probability normalization is not hidden in the proof.
9. Empty matrix index. The cocycle endpoint compiles with ι := Empty. No coordinate choice or nonempty-index premise is required.

Complete source-order map

Seven axiom reports

The module ends with seven #print axioms commands in the same theorem order as the mathematical dependency chain. A warning-fatal Lean run reports:

'NonlinearDynamics.Random.RandomCocycles.natCast_finiteOrbitVisitCount_eq_birkhoffSum_indicator'
depends on axioms: [propext, Classical.choice, Quot.sound]

'NonlinearDynamics.Random.RandomCocycles.integral_finiteOrbitVisitCount'
depends on axioms: [propext, Classical.choice, Quot.sound]

'NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate.nullMeasurableSet_finiteCenteredBadBlockSet'
depends on axioms: [propext, Classical.choice, Quot.sound]

'NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate.centeredProcess_le_badBlockVisitCount'
depends on axioms: [propext, Classical.choice, Quot.sound]

'NonlinearDynamics.Random.RandomCocycles.IsIntegrableSubadditiveProcessCandidate.measureReal_finiteCenteredBadBlockSet_le_rateRatio'
depends on axioms: [propext, Classical.choice, Quot.sound]

'NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.centeredFeketeOffset_le_normalizedIntegral'
depends on axioms: [propext, Classical.choice, Quot.sound]

'NonlinearDynamics.Random.RandomCocycles.DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.measureReal_centeredLogPlusBadBlockSet_le_rateRatio'
depends on axioms: [propext, Classical.choice, Quot.sound]

These are the standard logical and quotient principles inherited through Lean and Mathlib. No project-specific axiom appears.

Assumption and conclusion ledger

The generic theorem does not assume pointwise nonnegativity of \(X\). Its centered process has the nonpositive property required by the finite packing theorem because of the candidate’s one-step majorant. This differs from RMT-29, where nonnegativity was needed for the real-valued limsup API.

Common wrong turns

Treating the ratio as a probability bound

μ.real is the real-valued measure of the set. It need not be at most one. The mass-two boundary probe is deliberate. Calling the left side a probability is correct only after adding a probability-measure assumption.

Forgetting that the divisor is negative

From \(\delta\le c\mu(B)\), division by \(c\lt0\) reverses the direction. Any derivation that divides before proving hcneg is incomplete.

Replacing strict < by ≤

The bad-set definition uses a strict sublevel set. The length-one equality probe compiles that choice. A closed-threshold theorem would have a different boundary and would require separate proof work.

Letting m become infinity silently

The theorem controls a finite union. Passing to all lengths requires an increasing-union argument and a correctly identified limiting set. That is a separate theorem now supplied by RMT-31, not notation hidden inside RMT-30.

Reading the auxiliary limit as process convergence

Only \(H/(H+m)\to1\) is used. There is no proof that \(X_n/n\) or \(Y_n/n\) converges samplewise.

Adding ergodicity to explain preservation

Ergodicity is stronger than needed. The generic theorem consumes a MeasurePreserving witness directly, and the nonergodic identity probe ensures that boundary remains visible.

Forgetting the time-zero exception

The candidate interface does not force \(X_0\le0\). Therefore the pointwise packing theorem excludes exactly \(H+m=0\). The positive-at-zero process shows this is a semantic boundary, not a tactic inconvenience.

Calling log-positive growth a Lyapunov exponent

The observable clips logarithmic contraction at zero. The cocycle theorem is about a nonnegative envelope and cannot recover signed exponential rates or invariant subspaces.

Twenty-four solved exercises

Exercise 1: expand the orbit count

Compute finiteOrbitVisitCount T s 3 ω in words.

Solution. It is the number of true membership tests among \(\omega\in s\), \(T\omega\in s\), and \(T^2\omega\in s\).

Exercise 2: check horizon zero

What is the count at \(H=0\)?

Solution. Finset.range 0 is empty, so the filtered card is zero.

Exercise 3: derive the indicator identity

Why does the cast of the filtered card equal the indicator sum?

Solution. At each index, both sides contribute one when the orbit point belongs to the set and zero otherwise; finite sum congruence finishes.

Exercise 4: locate finite total mass

Why does integral_finiteOrbitVisitCount assume IsFiniteMeasure μ?

Solution. It needs the constant-one function, and hence its indicator, to be integrable. The combinatorial cast identity does not need this assumption.

Exercise 5: explain null measurability

Why is ordinary measurability not required for the visited set?

Solution. Bochner integration is insensitive to completion-null changes, and Mathlib’s indicator₀ and integral_indicator₀ accept a NullMeasurableSet.

Exercise 6: empty the witness window

Evaluate \(B_{0,c}\).

Solution. There is no natural \(n\) satisfying \(1\le n\le0\), so the finite union is empty.

Exercise 7: test equality

If \(Y_n(\omega)=cn\), is \(\omega\) marked by length \(n\)?

Solution. No. Membership requires the strict inequality \(Y_n\lt cn\).

Exercise 8: find the time-one center

Compute \(Y_1\).

Solution. The one-step Birkhoff sum of \(X_1\) is exactly \(X_1\), so \(Y_1=X_1-X_1=0\).

Exercise 9: force the rate sign

Use Exercise 8 to constrain \(\delta\).

Solution. Apply the lower-rate premise at \(n=1\): \(\delta\le\int Y_1=0\).

Exercise 10: force the threshold sign

What follows from \(c\lt\delta\le0\)?

Solution. Transitivity gives \(c\lt0\).

Exercise 11: explain the default length

Why does the length function return one at unmarked starts?

Solution. Lean needs a total function on naturals. The packing theorem queries its positivity and cost only for marked starts, so the default is irrelevant.

Exercise 12: weaken the witness cost

Why change \(Y_{\ell(j)}\lt c\ell(j)\) to ≤?

Solution. Strict inequality implies non-strict inequality, matching the imported packing theorem’s premise.

Exercise 13: explain the tail m

Why does the pointwise target use \(H+m\) rather than \(H\)?

Solution. A marked start just before \(H\) may carry a witness interval of length as large as \(m\); the enlarged endpoint contains every selected interval.

Exercise 14: isolate the false corner

Why is \(H=m=0\) excluded?

Solution. Then the target is \(Y_0=X_0\), which the candidate interface does not force nonpositive, while the visit count is zero.

Exercise 15: integrate the right side

What is \(\int c\operatorname{visits}_{B,H}\,d\mu\)?

Solution. Pull out the scalar and use the visit identity to obtain \(cH\mu(B)\).

Exercise 16: normalize the finite inequality

Why does the factor \(H/(H+m)\) appear?

Solution. The lower-rate premise divides the centered integral at horizon \(H+m\) by \(H+m\), while the visit integral contributes a factor \(H\).

Exercise 17: pass to the horizon limit

What happens to the correction factor for fixed \(m\)?

Solution. \(H/(H+m)\to1\) as natural \(H\to\infty\).

Exercise 18: divide with the correct order

From \(\delta\le c\mu(B)\) and \(c\lt0\), derive the result.

Solution. Negative division reverses order, giving \(\mu(B)\le\delta/c\).

Exercise 19: inspect zero measure

What does the theorem say when \(\mu=0\)?

Solution. Every real set measure is zero, and the compiled boundary probe computes the left side as zero.

Exercise 20: reject hidden ergodicity

Which compiled model instantiates the theorem without ergodicity?

Solution. The identity map on the two-point probability space is not pre-ergodic. In the compiled model, the finite bad set is one atom of mass \(1/2\), and the theorem proves the nontrivial bound \(1/2\le2/3\).

Exercise 21: reject hidden probability

Which compiled model instantiates the theorem without total mass one?

Solution. rmt30MassTwoMeasure has total mass two and still satisfies the generic theorem.

Exercise 22: build the cocycle rate premise

Which two ingredients establish hδ in the specialization?

Solution. The integrated Fekete rate is below each positive normalized block integral, and RMT-29 computes the centered integral by subtracting \(n\) times the one-step integral.

Exercise 23: audit the empty index

Why can ι := Empty compile?

Solution. The endpoint assumes finite decidable equality but never chooses a coordinate, so no Nonempty ι instance is required.

Exercise 24: state the next missing bridge

What must happen before this result can contribute to a lower-liminf theorem?

Solution. One must pass from the increasing family of finite bad sets to the all-length bad event with the correct measure-continuity argument, then connect absence or smallness of that event to an eventual samplewise lower bound. RMT-31 now proves the first bridge; the asymptotic bridge remains open.

Reproduction and audit

The frozen source inspected for this note has 506 lines and SHA-256 a8aee618a10f8434c1c33d8e433fd77e98ed3e5c8dee399e7d6fa323c5079b28.

Build the leaf module with warnings fatal:

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

Regenerate and verify the page-owned social card from any working directory:

site/content/development-notebook/2026/07/finite-centered-bad-block-measure-control-in-lean/generate-card.sh
site/content/development-notebook/2026/07/finite-centered-bad-block-measure-control-in-lean/generate-card.sh --verify

Validate the site after the shared coverage and navigation surfaces are updated in their own release step:

make content-coverage
make content-hygiene
make site-check

Discussion

RMT-30 changes the epistemic status of one narrow bridge. Before this module, the development had a checked finite interval-packing theorem and an upper limsup theorem, but no checked theorem that converted short centered-block witnesses into a quantitative finite-measure bound. The new source now checks that conversion, including the exact visit integral, sign reversal, and finite-horizon correction.

The formalization clarifies three often hidden distinctions. Counting is combinatorial before it is measurable. Preservation is enough for exact finite visit integration, while ergodicity is irrelevant. A finite measure is enough, so the result controls real measure rather than necessarily probability. The two nonprobability probes and the nonergodic probe make those distinctions executable rather than editorial.

The required epistemic downgrade is substantial. A bound for each finite witness cap is not an infinite-horizon bad-event theorem. An auxiliary limit of \(H/(H+m)\) is not convergence of the normalized process. The cocycle offset uses log-positive norms and is not a signed Lyapunov exponent. Thus RMT-30 advances one finite-measure component of a Kingman route while leaving the lower liminf, equality, and convergence layers open.

Navigation: previous and next milestones

Previous, RMT-29: Subadditive Upper Limsup Bounds from Phase Averaging in Lean proves the complementary samplewise upper-limsup ceiling and supplies the centered-integral identity reused in the cocycle specialization.

Next, RMT-31: All-Positive-Length Centered Bad-Block Control in Lean identifies the increasing union over length caps, proves extended-measure and finite-real-measure continuity, and passes this chapter’s uniform ratio to the uncapped event. Its compiled countermodel also shows why that raw once-bad event must not be called invariant.

References

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 primary historical theorem source. Its full result is stronger than RMT-30.

J. Michael Steele. Kingman’s subadditive ergodic theorem, Annales de l’Institut Henri Poincaré, Probabilités et Statistiques 25(1), 93-98, 1989, MR 995293, Zbl 0669.60039. Section 2 gives an algorithmic interval-decomposition proof related to the finite packing architecture.

Steven P. Lalley. Kingman’s Subadditive Ergodic Theorem, University of Chicago lecture notes, undated, accessed 2026-07-22. Pages 2-3 give the closest prose blueprint for bad starts and leftmost selection. These notes are pedagogical context, not the primary theorem source, and RMT-21’s checked half-open formulation governs the present endpoint conventions.

Mathlib contributors. Birkhoff sums, Mathlib commit 81a5d257. The pinned source defines birkhoffSum and its finite-sum interface.

Mathlib contributors. Bochner integration over sets, Mathlib commit 81a5d257. The pinned source contains integral_indicator₀.

Mathlib contributors. Null-measurable sets, Mathlib commit 81a5d257. The pinned source contains finite null-measurable bi-union closure.

This project. Ordered Disjoint Interval Packing for Subadditive Cocycles, RMT-21. This checked predecessor supplies OrderedNatIntervalPacking.le_mul_card_of_greedy_cover.

This project. Subadditive Upper Limsup Bounds from Phase Averaging in Lean, RMT-29. This predecessor supplies exact finite Birkhoff-sum integration and the centered-integral identity used by the cocycle wrapper.