Finite Ordered Interval Packing for Nonpositive Subadditive Processes

Begin with six positions you can count by hand

Before introducing an indexed type or a subadditive process, compare two families of half-open intervals inside the horizon \([0,10)\).

The valid family is

It covers the six positions

Its interval lengths are \(2,1,3\), so the arithmetic ledger is

The equality is not a coincidence. The first two intervals merely abut: the endpoint \(3\) is excluded from \([1,3)\) and included in \([3,4)\). The endpoint tests \(3\le3\) and \(4\le6\) show that the family is ordered.

Now slide the middle interval one step left:

The covered set is still \(\{1,2,3,6,7,8\}\), but the three lengths now sum to \(2+2+3=7\). The ledger becomes

The failed test \(3\le2\) identifies the overlap. Counting interval lengths as though they were disjoint has counted position \(2\) twice.

This small example gives the chapter’s first invariant:

only after order and disjointness have been established. It also exposes the two legal edge cases that the representation must retain:

• a singleton such as \([3,4)\) has positive length one; and
• two intervals may abut when the first endpoint equals the next start.

The rest of the chapter scales this exact ledger up. We will start with six marked positions, keep only three left endpoints, decode the resulting packing from gaps and lengths, and then use a nonpositive coefficient to convert nine covered positions into a bound by six marked starts.

A finite subadditive argument often reaches the following situation. Along an orbit of a map \(T\), some starting positions are marked because a short process interval beginning there has favorable average cost. The interval length can vary with the start. If every marked interval were kept, overlaps would prevent the sum of lengths from measuring the size of their union. If intervals were discarded without a rule, marked starts could disappear from the argument.

The solution is a leftmost packing rule. Select the interval at the least remaining marked start. Remove every candidate whose start is already covered by that interval. Repeat with the next remaining start. This produces a family that is ordered and pairwise disjoint, while every original marked start is still covered by some selected interval.

RMT-21 turns that sentence into a checked finite interface. It also proves the finite process inequality needed after selection. The result is a bridge from local favorable intervals to a bound by the number of marked starts. Nothing in that bridge says how many starts are marked along a typical orbit. That later density or ergodic step remains separate.

The immediate predecessor is Finite Phase Averaging for Nonpositive Subadditive Processes. The compact definition is the ordered interval packing glossary chapter. The declaration-complete implementation narrative is Pack the Marked Starts: Ordered Disjoint Intervals for Subadditive Cocycles in Lean.

Choose a route up

Learning objectives

By the summit, a reader should be able to:

1. define a half-open natural interval and calculate its cardinality;
2. translate an inclusive interval \([j,j+k-1]\) into \([j,j+k)\);
3. explain why \(k=1\) is a legal singleton;
4. explain why endpoint equality is legal for adjacent intervals;
5. distinguish a marked start from a covered position;
6. state the finite leftmost-selection problem;
7. decode a gap-length-tail packing into absolute endpoints;
8. explain why the packing horizon is a type index;
9. recover the list of selected intervals and its length;
10. recover the finite set of covered positions;
11. prove membership in that set has an interval witness;
12. derive pairwise endpoint order from recursive placement;
13. convert endpoint order to set disjointness;
14. derive exact covered cardinality;
15. distinguish Covers and SelectedFrom;
16. explain the absolute offset in SelectedFromFrom;
17. follow the minimum-and-filter selector step;
18. prove each deleted mark is covered;
19. prove the recursive tail horizon is smaller;
20. explain the branch where the selected interval crosses the old horizon;
21. derive the enlarged horizon \(H+m\);
22. distinguish generic endpoint containment from selector endpoint slack;
23. define recursive packing cost;
24. transport per-mark costs to selected interval costs;
25. sum weak costs over any packing;
26. state why strict cost summation requires nonempty packing;
27. split a shifted-subadditive process around selected intervals;
28. delete a positive initial gap;
29. avoid introducing an \(X_0\) term at zero gap;
30. avoid introducing an \(X_0\) term at zero terminal gap;
31. derive the weak covered-length process bound;
32. derive the strict covered-length process bound;
33. turn coverage into a marked-cardinality inequality;
34. reverse that inequality under \(c\le0\);
35. state the weak all-marked-sets theorem;
36. state the strict nonempty-mark theorem;
37. reproduce the empty-set strict counterexample;
38. reproduce the horizon-zero process counterexample;
39. interpret the candidate wrapper according to its stated fields;
40. interpret the centered-process wrapper according to its stated fields;
41. interpret the empty-index cocycle wrapper according to its stated fields;
42. identify which source claims are motivational rather than formal inputs;
43. explain why finite coverage is not an asymptotic density;
44. list the analytic infrastructure still missing before Kingman’s theorem.

The common setup and notation ledger

Let:

• \(\Omega\) be a state space;
• \(T:\Omega\to\Omega\) be a discrete-time map;
• \(X:\mathbb N\to\Omega\to\mathbb R\) be a finite-horizon process;
• \(H\in\mathbb N\) be a horizon containing eligible starts;
• \(m\in\mathbb N\) be a uniform upper bound on selected lengths;
• \(B\subseteq\{0,\ldots,H-1\}\) be a finite set of marked starts; and
• \(\ell:\mathbb N\to\mathbb N\) assign a length to each start, with \(0\lt\ell(j)\le m\) whenever \(j\in B\).

The shifted-subadditive convention is

The later finite process theorem assumes

It does not assume a sign or normalization at time zero.

The coefficient \(c\in\mathbb R\) in a favorable interval estimate is nonpositive. That sign is used only when a lower bound on selected length is converted into the desired upper bound on process cost.

From a favorable start to a bounded interval

At each \(j\in B\), suppose the chosen length satisfies a local estimate such as

The corresponding geometric object is

The length function can vary. One start may choose length one and the next length five. Two such intervals can overlap even when their starts are distinct. The selection problem therefore requires more than sorting a list.

We need two outcomes simultaneously:

1. selected intervals must be ordered and disjoint so their lengths add exactly; and
2. every original marked start must lie in the selected union so marked cardinality is controlled.

The second condition does not require every mark to remain a selected start. A mark inside an earlier selected interval is allowed to disappear from the candidate list because it is already covered.

Half-open intervals remove two off-by-one traps

Lalley’s lower-estimate discussion uses inclusive integer intervals \([j,j+k-1]\) and the finite inequality labeled equation (6) (Lalley). The following greedy paragraph permits \(1\le k\le m\).

The displayed endpoint chain nevertheless includes a strict comparison from the start to \(j+k-1\). At \(k=1\), it asks \(j\lt j\). That is impossible, although the interval should be the legal singleton \(\{j\}\).

The half-open translation is

Now positive length is exactly \(j\lt j+k\). The separation between two inclusive intervals,

becomes

Equality means the intervals abut. No integer position is shared.

Mathlib’s Finset.Ico and Set.Ico implement the same convention in finite and set-theoretic forms (Mathlib finite intervals).

Repair the source at the level of sets

The safest translation begins with membership, not with a chain of endpoint symbols. For \(k\gt0\), membership in Lalley’s inclusive interval means

For natural numbers, the second comparison is equivalent to \(r\lt j+k\). Therefore

This extensional equality preserves the intended \(k\) positions. It also shows exactly where the singleton lives. When \(k=1\), both presentations denote \(\{j\}\); the half-open endpoint inequality is \(j\lt j+1\), which is true. The displayed strict inequality \(j\lt j+k-1\) would instead become \(j\lt j\), which is false. The repair removes that accidental exclusion without changing the following stated range \(1\le k\le m\).

Now compare two selected intervals. The inclusive separation condition says the last point of the first lies strictly before the first point of the next:

Over natural numbers this is equivalent to \(j+k\le j'\). That is exactly the order needed for disjoint half-open intervals. Equality means the first interval excludes the boundary that the second includes.

There are consequently two separate corrections:

1. positive length becomes the strict start-to-excluded-endpoint comparison \(j\lt j+k\); and
2. chronological separation becomes the weak comparison \(j+k\le j'\).

Keeping the first comparison strict and the second weak admits singletons and abutment simultaneously. Strengthening either one changes the mathematical class of packings.

An indexed packing stores the proof in the data

An arbitrary list of endpoint pairs would require propositions saying:

• each start is below its endpoint;
• every endpoint is inside the horizon;
• the list is chronological; and
• different intervals are disjoint.

RMT-21 instead uses an indexed inductive family. The empty constructor selects nothing but retains any horizon. The cons constructor stores a natural gap, a positive interval length, and a valid recursive tail. Its result horizon is definitionally the sum of those three lengths.

The first interval starts after the gap. The recursive tail begins after that interval. Therefore every later interval begins no earlier than the current endpoint. Zero gaps allow equality. Positive interval lengths rule out empty selected regions.

The type does not promise that the packing is maximal, that its gaps are minimal, or that it came from a selector. Those are separate questions.

A concrete packing from gaps

Consider a horizon of ten positions. Choose:

• an initial gap of one;
• a selected length of two;
• a zero intermediate gap;
• a selected length of one;
• a gap of two;
• a selected length of three; and
• a terminal gap of one.

The decoded intervals are

The covered finite set is

The interval count is three and covered length is six. The first two intervals abut. The middle interval is a singleton. Every endpoint is at most ten.

The recursive representation can be read as a run-length description of the horizon, alternating unselected gaps and selected regions. Unlike an arbitrary binary mask, it also preserves interval boundaries.

A complete greedy example, including deletion

Let the old start horizon be \(H=10\), the uniform length bound be \(m=4\), and the marked set be

Prescribe \(\ell(1)=3\), \(\ell(4)=2\), and \(\ell(8)=4\). The remaining prescribed values may be any positive natural numbers at most four. They are part of the input but are never inspected once their starts are deleted.

The first minimum is one. Its interval is \([1,4)\). The survivor filter keeps exactly starts \(r\) satisfying \(4\le r\), so the state changes as follows:

Why is deletion safe? A deleted mark \(r\) satisfies \(r\lt4\). Minimum selection gives \(1\le r\). Hence \(r\in[1,4)\). In particular, the deleted mark two remains covered even though it never becomes a selected start. The mark four survives because it is the excluded endpoint.

The next minimum is four. Selecting \([4,6)\) produces

The intervals \([1,4)\) and \([4,6)\) abut. Their shared written boundary does not create a shared set member.

The next minimum is eight. The proposed endpoint is twelve, which passes the old horizon endpoint ten. This is the selector’s terminal branch. Every remaining mark \(r\) satisfies \(8\le r\) by minimality and \(r\lt10\) by the original start bound. Since \(10\le12\), both remaining marks lie in \([8,12)\). No recursive survivor set is needed.

The final selected family is

Its gap-length-tail representation is

The type index is not approximate bookkeeping. It checks the exact identity

The last selected endpoint, twelve, is strictly below fourteen even though it is beyond the old endpoint ten. The terminal tail of two fills the remainder of the indexed horizon.

The union contains nine positions:

Here is the distinction between selection provenance and coverage in full. Every selected start is covered, but three covered marks were deliberately discarded:

The selected-start set is \(\{1,4,8\}\). The covered set is larger because an interval covers positions, not merely its own left endpoint. The proof needs both facts: selected intervals inherit local cost hypotheses from their left endpoints, while coverage controls the cardinality of the original marked set.

Thus

The interval count is only three. Neither interval count nor covered length equals marked cardinality in general. The proof needs the chain

not a claim that one interval was selected for every mark.

Now take \(c=-2\). Suppose the three selected costs are bounded by \(-6\), \(-4\), and \(-8\), the coefficient times their respective lengths. Summation gives

Coverage gives \(6\le9\), but the coefficient is nonpositive, so the real-number comparison reverses:

If the raw packing inequality gives \(X_{14}(\omega)\le\operatorname{cost}(P)\), transitivity yields \(X_{14}(\omega)\le-12=c|B|\). This is the complete finite route from local favorable intervals to a marked-cardinality estimate.

Covered positions, interval provenance, and three distinct predicates

Three propositions should never be conflated.

Geometric validity

Every value of OrderedNatIntervalPacking N is geometrically valid inside \(N\). Public theorems recover endpoint containment, chronological order, and pairwise disjointness.

Coverage

P.Covers B means

It says every mark is contained. It says nothing about the origin of selected intervals.

Selection provenance

P.SelectedFrom B ell means every selected interval begins at a member of \(B\) and has the prescribed length there. It says nothing about whether unselected marks are covered.

The greedy theorem returns all three layers: geometric validity through the type, coverage through Covers, and provenance through SelectedFrom.

The recursive predicate is named SelectedFromFrom because it must remember an absolute offset. The packing tail stores relative gaps. The marked set and process hypotheses use absolute orbit positions. The offset is the bridge between those coordinate systems.

The leftmost rule and why every deleted mark stays covered

The offset selector proceeds by strong induction on the remaining old-horizon length.

If no marks remain, return an empty packing whose horizon includes the old tail and the uniform extra allowance \(m\).

Otherwise, let \(j\) be the least marked start and let \(k=\ell(j)\). The positive-length premise gives \(j\lt j+k\).

There are two branches.

The interval ends within the old horizon

Keep \([j,j+k)\). Filter the remaining marked set by the predicate

A removed mark \(r\lt j+k\) is at least \(j\) because \(j\) was least, so it lies in the selected interval. A surviving mark lies at or to the right of the endpoint. The recursive old tail is strictly shorter, so strong induction applies.

The recursive selector certifies provenance relative to the filtered set. Because that set is a subset of the original marked set, SelectedFromFrom.mono widens the certificate.

The interval crosses the old horizon

Keep the same interval and stop. Every marked start was below the old horizon, at least \(j\), and now strictly below \(j+k\). Thus one interval covers all remaining marks.

This branch is not an error case. It is the reason the target horizon is enlarged.

Strong induction and the two endpoint branches

Ordinary successor induction would force the proof to decrement the horizon by one. The selector can jump by the selected interval length and by the distance from the current offset to the leftmost mark. Strong induction instead allows recursion at any strictly smaller remaining horizon.

The proof must reconstruct the target type index after each recursive call. Suppose the selected start is \(j\), current offset is \(o\), interval length is \(k\), and recursive old tail length is \(R\). The new packing horizon is

The natural-number equalities include truncated subtraction. The branch hypotheses ensure the subtractions are exact, and Lean’s omega tactic closes the linear arithmetic.

In the crossing branch, the terminal tail is chosen as the difference between \(H+m\) and the used prefix plus interval. The length bound \(k\le m\) proves this difference is defined and reconstructs the same target index.

Why \(H+m\) is the correct enlarged horizon

The eligible-start premise controls only \(j\lt H\). The length premise gives \(k\le m\). Therefore

The strict endpoint slack is stronger than the generic packing invariant. A generic interval may end exactly at its ambient horizon. The selector target has an extra uniform length allowance, so every selected endpoint is strictly inside it.

Why not use \(H+m-1\)? In natural arithmetic that expression complicates the empty and zero cases, while \(H+m\) is uniform and follows directly from the hypotheses. The later process theorem evaluates \(X_{H+m}\). This has the same start-window-plus-maximal-length shape as Lalley’s \(nm+m\) horizon, but it is a zero-based adaptation rather than an exact reindexing of Lalley’s marked sample window.

Why not use an infinite interval family? The subsequent subadditive inequality is finite. Keeping a finite explicit horizon lets Lean audit every gap and time-zero branch before any limiting argument is designed.

Exact covered cardinality and the marked-count inequality

The interval decoder provides an ordered list. The covered decoder provides a finite union. The following theorem identifies the two quantities needed by the later marked-count estimate:

Inductively, the current Finset.Ico is disjoint from the recursive tail. Its cardinality is the current selected length. Mathlib then adds the cardinalities of the disjoint union (finite-set cardinality).

Coverage gives

The inequality can be strict. If marks zero and one choose lengths three and one, the leftmost selector may keep \([0,3)\) alone. It covers both marks, while selected covered length is three and marked cardinality is two.

This strictness is useful when \(c\le0\): a longer selected cover gives a more negative intermediate bound, which is at most the desired marked-card bound.

The selected cost is not a pointwise sum

For a selected interval \([j,j+k)\), the cost contribution is

It is one variable-horizon process value. It is not defined as

Shifted subadditivity may bound the first expression by a sum of smaller pieces, but it does not make them equal. This distinction is essential for a genuinely subadditive process.

The recursive cost definition evaluates the first selected interval after its prefix gap, then evaluates the recursive tail after both the gap and interval. Natural-iterate addition proves that this nested sample shift equals the absolute interval start recovered by SelectedFromFrom (function iteration).

Discard only positive gaps in the subadditive proof

Let \(P\) be a packing inside a nonzero horizon \(N\). Repeated shifted subadditivity decomposes \(X_N\) into selected interval terms and gap terms. Every positive gap has nonpositive process value and may be discarded from the upper bound.

The proof must not say every gap is nonpositive. A zero gap would ask for \(X_0\le0\), which is not assumed.

Three branches prevent that mistake:

1. Zero initial gap. Start directly with the first selected interval.
2. Zero terminal tail. Stop at the final interval instead of splitting a zero remainder.
3. Nonempty recursive tail. Its horizon is positive because it contains a positive-length interval, even if its own leading gap is zero.

The resulting raw inequality is

An empty packing at positive \(N\) reduces the theorem to \(X_N\le0\). At \(N=0\), the theorem is false without a time-zero premise. This exact boundary is retained rather than hidden behind \(X_0=0\).

Transport per-mark costs through SelectedFrom

The selector hypothesis is naturally stated at marked starts:

The recursive packing-cost theorem requires the same fact at every cons node. The SelectedFromFrom.everyIntervalCostLE theorem transports it. Its strict sibling transports a strict inequality. The zero-offset public forms remove the initial iterate by zero.

These bridge theorems are why SelectedFrom is not replaced by a mere endpoint-list proposition. Its recursive shape aligns with the recursive cost definition and makes the orbit shifts provable by induction.

Weak interval bounds sum over any packing:

Strict interval bounds sum strictly only if the packing contains an interval. The empty recursion branch carries True, but an empty strict sum would demand \(0\lt0\).

Weak and strict marked-card bounds

Combine four finite facts:

1. the whole horizon is at most the packing cost;
2. local weak or strict estimates bound packing cost by \(cL\);
3. coverage gives \(|B|\le L\); and
4. \(c\le0\) gives \(cL\le c|B|\).

The universal weak conclusion is

It requires \(N\ne0\), even if \(B\) is empty.

The strict conclusion is

It requires \(B\) to be nonempty. Coverage then forces a nonempty packing, so horizon positivity follows automatically.

The end-to-end greedy theorems instantiate \(N=H+m\), construct \(P\), use SelectedFrom to transport per-mark costs, and use Covers for cardinality.

Why the empty set destroys universal strictness

Take \(X_n=0\) at positive horizons and \(B=\varnothing\). Every statement of the form

is true because there is no \(j\). The selected packing can be empty. Its cost and \(c|B|\) are both zero. A strict conclusion would be \(0\lt0\).

This is a mathematical counterexample, not a Lean inconvenience. The strict theorem therefore accepts marked.Nonempty.

Why time zero destroys an unconditional weak theorem

Define \(X_0=1\) and \(X_n=-n\) for positive \(n\). This process is shifted-subadditive and nonpositive at positive horizons. The empty packing at horizon zero has cost zero, so \(X_0\le0\) fails.

The weak greedy theorem retains \(H+m\ne0\). The strict theorem derives it from nonempty marks and positive selected length.

Candidate and cocycle wrappers

The generic candidate wrapper has a measurable space, a measure, and a finite horizon integrability field in its receiver type. The pointwise packing proof uses only its shifted-subadditivity field, plus a separate positive-horizon sign hypothesis. Prose should distinguish receiver baggage from consumed fields.

The orbit-majorant-centered process already has the two algebraic properties needed here:

• shifted subadditivity; and
• nonpositivity at positive horizons.

Its packing theorem needs no \(X_0=0\) and no extra preservation theorem.

The discrete matrix-cocycle wrapper specializes to the centered log-positive norm observable. It imposes no generator-integrability package, probability, ergodicity, or nonempty matrix index. The cocycle receiver still stores base preservation because that is part of the object, but this finite pointwise proof does not use an integral.

The observable remains log-positive. It controls expansion after clipping contraction and is not a signed Lyapunov observable.

Seven bridges from paper mathematics to checked Lean

Each bridge below says the same fact three ways: first as a sentence a human might write, then as mathematics, then as the exact Lean interface. The project declarations are full project checks that import Mathlib. The later Std worksheet is a standalone tutorial small enough for an ordinary macOS or Linux computer.

Lean bridge 1: the data itself enforces positive lengths

OrderedNatIntervalPacking.cons gap length length_pos rest

inductive OrderedNatIntervalPacking : ℕ → Type
  | empty (horizon : ℕ) : OrderedNatIntervalPacking horizon
  | cons (gap length : ℕ) {tail : ℕ} (length_pos : 0 < length)
      (rest : OrderedNatIntervalPacking tail) :
      OrderedNatIntervalPacking (gap + length + tail)

Lean bridge 2: covered membership has an interval witness

P.mem_coveredFinset_iff_exists_interval

theorem mem_coveredFinset_iff_exists_interval {N j : ℕ}
    (P : OrderedNatIntervalPacking N) :
    j ∈ P.coveredFinset ↔
      ∃ I ∈ P.intervals, I.1 ≤ j ∧ j < I.2

Lean bridge 3: disjoint geometry becomes exact cardinality

P.card_coveredFinset

theorem card_coveredFinset {N : ℕ} (P : OrderedNatIntervalPacking N) :
    P.coveredFinset.card = P.coveredLength

Lean bridge 4: leftmost selection returns coverage and provenance

exists_orderedPacking_covering H m marked length hmarked hlength

theorem exists_orderedPacking_covering
    (H m : ℕ) (marked : Finset ℕ) (length : ℕ → ℕ)
    (hmarked : marked ⊆ Finset.range H)
    (hlength : ∀ j ∈ marked, 0 < length j ∧ length j ≤ m) :
    ∃ P : OrderedNatIntervalPacking (H + m),
      P.Covers marked ∧
        P.SelectedFrom marked length

Lean bridge 5: positive gaps may be discarded, zero gaps may not

P.le_cost_of_add_le_nonpos hadd hnonpos hN ω

theorem le_cost_of_add_le_nonpos
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    (hadd : ∀ m n ω, X (m + n) ω ≤ X n (T^[m] ω) + X m ω)
    (hnonpos : ∀ n, n ≠ 0 → ∀ ω, X n ω ≤ 0)
    {N : ℕ} (P : OrderedNatIntervalPacking N) (hN : N ≠ 0) (ω : Ω) :
    X N ω ≤ P.cost T X ω

Lean bridge 6: a nonpositive coefficient reverses the counting inequality

P.le_mul_card_of_add_le_nonpos_of_covers hadd hnonpos hN marked hcover ω c hc hcost

theorem le_mul_card_of_add_le_nonpos_of_covers
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    (hadd : ∀ m n ω, X (m + n) ω ≤ X n (T^[m] ω) + X m ω)
    (hnonpos : ∀ n, n ≠ 0 → ∀ ω, X n ω ≤ 0)
    {N : ℕ} (P : OrderedNatIntervalPacking N) (hN : N ≠ 0)
    (marked : Finset ℕ) (hcover : P.Covers marked)
    (ω : Ω) (c : ℝ) (hc : c ≤ 0)
    (hcost : P.EveryIntervalCostLE T X ω c) :
    X N ω ≤ c * (marked.card : ℝ)

Lean bridge 7: strictness needs at least one marked start

lt_mul_card_of_greedy_cover hadd hnonpos H m marked length hmarked hlength hmarked_nonempty ω c hc hcost

theorem lt_mul_card_of_greedy_cover
    {Ω : Type uΩ} {T : Ω → Ω} {X : ℕ → Ω → ℝ}
    (hadd : ∀ a b ω, X (a + b) ω ≤ X b (T^[a] ω) + X a ω)
    (hnonpos : ∀ n, n ≠ 0 → ∀ ω, X n ω ≤ 0)
    (H m : ℕ) (marked : Finset ℕ) (length : ℕ → ℕ)
    (hmarked : marked ⊆ Finset.range H)
    (hlength : ∀ j ∈ marked, 0 < length j ∧ length j ≤ m)
    (hmarked_nonempty : marked.Nonempty)
    (ω : Ω) (c : ℝ) (hc : c ≤ 0)
    (hcost : ∀ j ∈ marked,
      X (length j) (T^[j] ω) < c * (length j : ℝ)) :
    X (H + m) ω < c * (marked.card : ℝ)

Type-check the seven project bridges

import NonlinearDynamics.Random.RandomCocycles.SubadditiveIntervalPacking

open NonlinearDynamics.Random.RandomCocycles

#check OrderedNatIntervalPacking
#check OrderedNatIntervalPacking.mem_coveredFinset_iff_exists_interval
#check OrderedNatIntervalPacking.card_coveredFinset
#check OrderedNatIntervalPacking.exists_orderedPacking_covering
#check OrderedNatIntervalPacking.le_cost_of_add_le_nonpos
#check OrderedNatIntervalPacking.le_mul_card_of_add_le_nonpos_of_covers
#check OrderedNatIntervalPacking.lt_mul_card_of_greedy_cover

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

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

The checked declaration architecture

The frozen source has fifty-four public named declarations and thirteen private named declarations. The architecture is best read in nine layers.

Layer 1: representation and two decoders

OrderedNatIntervalPacking, intervalCount, coveredLength, intervalsFrom, intervals, length_intervalsFrom, length_intervals, coveredFinsetFrom, and coveredFinset define and decode the structural object.

Layer 2: membership, bounds, and exact cardinality

The two covered-membership equivalences connect the finite union to decoded intervals. mem_coveredFinsetFrom_bounds supplies containment. card_coveredFinsetFrom and card_coveredFinset compute exact size. coveredFinset_subset_range gives the public horizon containment.

Layer 3: coverage and interval geometry

Covers, intervalCount_ne_zero_of_covers_of_nonempty, and card_le_coveredLength_of_covers form the coverage interface. The five intervals… theorems prove shifted containment, endpoint order, pairwise set disjointness, and public containment.

Layer 4: provenance and selection

SelectedFromFrom, SelectedFrom, monotonicity, both decoded-interval provenance theorems, and the enlarged-horizon endpoint theorem expose selection provenance. The private exists_orderedPacking_covering_from is the strong-induction engine; exists_orderedPacking_covering is the public selector.

Layer 5: local costs

cost, the two horizon-length facts, the weak and strict recursive cost predicates, strict-to-weak conversion, four provenance-to-cost bridges, and the two total-cost theorems turn local hypotheses into selected-length bounds.

Layer 6: raw and covered-length process inequalities

le_cost_of_add_le_nonpos and its nonempty form charge the horizon to the packing. The weak and strict covered-length theorems compose that bound with local costs.

Layer 7: marked-cardinality and end-to-end selector inequalities

The two …of_covers theorems use coverage and \(c\le0\). The weak and strict …of_greedy_cover theorems add selector existence and per-mark cost transport.

Layer 8: project wrappers

Two candidate methods, one centered-process method, and one direct matrix-cocycle method expose the finite packing sum and covered-length form in the established project namespaces.

Layer 9: private regression fixtures

The time-zero witness and candidate test the exact missing normalization. The empty, full-terminal, abutting, outer-gap, intermediate-gap, singleton, long-choice, and long-cover fixtures test every endpoint and cardinality boundary. Anonymous examples check empty selector output, unit abutment, strict versus weak marked-card bounds, a strict coverage inequality, positive and zero gaps, final endpoints, centered wrappers, and empty matrix dimension.

The Development Notebook lists all sixty-seven named declarations individually in exact source order.

Complete declaration manifest

This chapter also records that source-order manifest directly, so a reader can audit the frozen module without treating any helper as invisible prose. The public surface contains exactly fifty-four names:

The thirteen private named declarations are implementation machinery or regression fixtures. They are not additional public assumptions:

Unnamed example declarations below these fixtures exercise equalities, inequalities, endpoints, wrapper specializations, and empty-index matrix behavior. They are checked regression examples, but they do not add names to the fifty-four-plus-thirteen manifest.

Why the public API has this shape

Several tempting convenience theorems are deliberately absent from the frozen surface.

There is no single predicate combining Covers and SelectedFrom. A packing can cover a marked set even when its intervals came from elsewhere, and it can be selected from eligible marks while failing to cover all of them. Keeping the predicates separate lets later arguments consume only the contract they need. The greedy existence theorem returns their conjunction because that construction proves both.

There is no separate marked-card theorem from packing cost alone. The useful route needs three logically different ingredients: a process-to-packing-cost inequality, a local-cost-to-covered-length inequality, and a coverage-to-marked-cardinality comparison under a nonpositive coefficient. The public …of_covers declarations expose that composition while making no claim that the packing cost itself contains marked-set information.

There is also no extensional equivalence theorem saying that equality of decoded interval lists is the same as equality of indexed packing values. The representation stores proof-relevant positive-length witnesses and recursive horizon structure. Downstream mathematics uses decoded intervals, covered positions, and cost, so an extensional quotient would add machinery without helping this milestone.

Weak and strict estimates are parallel declarations instead of one theorem with a boolean mode. Their bases differ mathematically. Weak summation has the valid empty base \(0\le0\). Strict summation needs a nonzero interval count, and the marked-card version obtains it from marked.Nonempty plus coverage. Separate names keep that additional premise visible at every call site.

Finally, the selector engine remains private while its existence theorem is public. Later files should rely on coverage and provenance, not on a particular implementation of finite minimum and filtering. This leaves room to replace the algorithm without changing consumers, while the private boundary fixtures protect the current construction against singleton, abutment, terminal-tail, outer-gap, and long-cover regressions.

The declaration count reflects these choices: fifty-four public named declarations form the reusable mathematical interface; the private selector and twelve private named fixtures support implementation and auditing. The thirteen private names are not missing public mathematics.

This separation also prevents unsupported claims in future asymptotic work. A density theorem will be able to provide a new marked set and a lower bound on its cardinality without reopening selector internals. A matrix-cocycle application will be able to provide local favorable costs without proving coverage again. The finite packing layer is the junction: provenance receives local analytic information, coverage emits a counting inequality, and the indexed geometry ensures the selected costs do not overlap.

Lean proofcraft

Indexed induction replaces repeated validity proofs

Pattern matching on a packing gives exactly the geometric decomposition needed for both cardinality and process proofs.

Offset helpers reconcile relative storage with absolute statements

Every From definition accepts an absolute origin. Its public wrapper starts at zero. This pattern avoids repeatedly translating a tail back to global coordinates.

Pairwise list order is enough

The recursive list theorem proves each earlier endpoint is at most each later start. A simple implication converts that relation to pairwise disjoint Set.Ico intervals.

Strong induction matches greedy jumps

The recursive selector advances to the selected right endpoint, not merely to the successor horizon. Strong induction permits that variable-size decrease.

Finite filtering carries the coverage invariant

The remaining set is filtered by an endpoint comparison. Removed elements are proved inside the current interval; retained elements satisfy the recursive start horizon.

Function-iterate addition aligns samples

The cost bridge rewrites nested shifts to absolute exponents. The exact pinned iteration law is finite and requires no dynamics or measure theory.

Sign-aware multiplication closes the marked-card step

Lean makes the reversal under \(c\le0\) explicit. This prevents an intuitive but directionally wrong use of the coverage inequality.

Replay the two hardest Lean proof states

The indexed types make two additional pieces of bookkeeping explicit in the informal selector. Replaying those states explains why the implementation uses an offset theorem and strong induction.

The recursive endpoint branch

Suppose the recursive call begins at absolute offset \(o\) with old remaining horizon \(H\). Let \(j\) be the least mark and \(\ell=\operatorname{length}(j)\). In the branch

the proof defines

Two arithmetic facts are required before recursion:

and

The first aligns the new half-open range with the old endpoint. The second is the well-founded decrease for strong induction. Positive length matters in the second proof: after reaching the least mark, the algorithm advances past at least one position.

The survivor set is

For \(r\in B'\), the old containment proof supplies \(r\lt o+H\). Rewriting the endpoint with the first arithmetic identity gives

which is exactly membership in the recursive half-open start range.

The recursive result has type

Adding the new gap and interval gives the apparent index

The proof records \(o+(j-o)=j\), then uses the endpoint identity to show this index equals \(H+m\). A rewrite transports the existential witness across that equality. The indexed representation is useful because every unit of horizon must be accounted for explicitly.

Coverage in this branch is a local decision. For an original mark \(r\), the proof splits on \(r\lt j+\ell\). In the true branch, minimality supplies \(j\le r\), placing \(r\) in the current interval. In the false branch, \(j+\ell\le r\), so \(r\) belongs to \(B'\) and recursive coverage applies.

Provenance has a different shape. The current interval uses the facts \(j\in B\) and \(\ell=\operatorname{length}(j)\). The recursive certificate mentions \(B'\). Since \(B'\subseteq B\), SelectedFromFrom.mono widens it. Coverage and provenance are therefore proved by different arguments even though the selector returns both.

The crossing endpoint branch

If \(j+\ell\gt o+H\), define the final tail by

The length bound \(\ell\le m\), least-start bounds, and natural arithmetic prove

That fact makes the subtraction exact, so

The packing consists of one cons node followed by an empty tail. For any mark \(r\), minimality gives \(j\le r\); the old start bound gives \(r\lt o+H\); and the branch condition gives \(o+H\lt j+\ell\). Therefore \(r\in[j,j+\ell)\). The terminal branch covers all survivors at once.

This branch also explains why targeting \(H\) alone is impossible. A legal start near the end of the old horizon can choose a legal length that crosses that endpoint. The additional \(m\) is a uniform budget for exactly this case.

The marked-cardinality proof state

After the process and local-cost theorems, the weak coverage theorem has two facts of different numeric types:

and

in natural numbers. The Lean proof proceeds in three explicit stages.

First, card_le_coveredLength_of_covers supplies the natural inequality. Second, exact_mod_cast turns it into

Third, mul_le_mul_of_nonpos_left applies \(c\le0\) and returns

The weak theorem composes two non-strict inequalities. The strict theorem first obtains a strict covered-length estimate and then uses LT.lt.trans_le with the same non-strict sign-reversed comparison. Nonempty coverage proves the packing has nonzero interval count, which is the missing premise for strict summation.

Trace the end-to-end declaration route

For the weak public theorem, a reader can follow this exact dependency path:

1. exists_orderedPacking_covering constructs \(P\), coverage, and selection provenance.
2. SelectedFrom.everyIntervalCostLE transports the local marked-start hypothesis to the recursive interval-cost predicate.
3. le_mul_coveredLength_of_add_le_nonpos combines the raw process inequality with the interval costs.
4. card_le_coveredLength_of_covers changes geometric coverage into a cardinality comparison.
5. le_mul_card_of_add_le_nonpos_of_covers performs the cast and sign reversal.
6. le_mul_card_of_greedy_cover packages all five steps.

The strict route substitutes the LT cost predicates and the strict covered-length theorem, then asks for marked.Nonempty. Keeping the weak and strict paths parallel makes their single logical difference explicit.

Common wrong turns

Reusing the inclusive endpoint chain unchanged

That loses singleton intervals and obscures legal abutment. Translate the sets, not just the typography.

Asking Covers to prove local costs

Coverage provides no selected-start provenance. Use SelectedFrom.

Asking SelectedFrom to prove coverage

Provenance constrains what was selected but does not require all marks to be represented. Use both contracts.

Making gaps positive

The selector naturally produces zero gaps when a next uncovered mark equals the prior endpoint.

Making intervals longer than one

The source selection allows length one, and the frozen unit-abutting fixture checks it.

Using only horizon \(H\)

Starts are bounded by \(H\); endpoints need the uniform extra length \(m\).

Removing the weak horizon premise

Combinatorial selection works at \(H=m=0\), but positive-time process sign does not control \(X_0\).

Making the strict theorem universal

The empty marked set turns strict local hypotheses into vacuous truths and the conclusion into a false strict empty-sum inequality.

Forgetting \(c\le0\)

The cardinality comparison points the wrong way for a positive coefficient.

Calling selected cost a Birkhoff sum

Intervals have variable lengths. Their process values are not one fixed observable sampled along consecutive times.

Claiming a density from finite coverage

No sequence of marked sets or normalized cardinalities appears in the theorem.

Importing Steele as the selector theorem

Steele’s algorithmic decomposition is related proof lineage, but its interval classes and full asymptotic proof do not state the exact Covers/SelectedFrom result checked here (Steele).

Forty-four solved exercises

Base camp: see the geometry

Exercise 1: translate an inclusive singleton

Translate \([7,7]\) to half-open form.

Solution. The inclusive set contains the natural numbers \(r\) satisfying \(7\le r\le7\), so it contains exactly seven. Replacing the last included point by the next excluded endpoint gives \([7,8)\). Its membership condition is \(7\le r\lt8\), which again admits only seven. The endpoint difference is \(8-7=1\), so this is a positive-length interval, not an empty boundary case. Any formalization that demands the excluded endpoint be more than one step past the start would incorrectly lose this singleton.

Exercise 2: translate separation

Translate \(j+k-1\lt j'\) to half-open endpoints.

Solution. The last included point of the first interval is \(j+k-1\). Saying it is strictly before \(j'\) means its successor is at most \(j'\). That successor is \(j+k\), the excluded half-open endpoint. Hence the translated relation is \(j+k\le j'\). If equality holds, the first interval excludes \(j'\) and the next interval includes it, so the sets are disjoint. Replacing the translated weak comparison by \(j+k\lt j'\) would insert an unnecessary uncovered position and forbid legal abutment.

Exercise 3: test abutment

Do \([0,2)\) and \([2,5)\) overlap?

Solution. No. Two belongs only to the second interval.

Exercise 4: decode a prefix

At offset four, gap three, and length two, what is the interval?

Solution. \([7,9)\).

Exercise 5: identify a zero gap

What does a zero recursive gap mean geometrically?

Solution. The next interval begins at the previous endpoint.

Exercise 6: identify an empty tail

What does .empty 5 after the last interval record?

Solution. A terminal uncovered gap of length five.

Exercise 7: compare two sizes

Can interval count equal covered length?

Solution. Sometimes, for example when every interval is a singleton. In general they measure different quantities.

Exercise 8: find the toy covered set

What positions are covered by \([1,3)\), \([3,4)\), and \([6,9)\)?

Solution. \(\{1,2,3,6,7,8\}\).

Exercise 9: count it two ways

What is its cardinality, and what is the sum of lengths?

Solution. Both are six, using \(2+1+3\).

Exercise 10: distinguish a covered mark

In the same packing, may two be marked without being selected?

Solution. Yes. It is covered by the interval beginning at one.

Exercise 11: state the three contracts

Name geometry, coverage, and provenance.

Solution. The packing type supplies geometry, Covers supplies coverage, and SelectedFrom supplies provenance.

Mid-mountain: rebuild the selector

Exercise 12: choose the first start

Why use the least marked start?

Solution. It ensures every other mark is at or to its right, which makes the coverage split exhaustive.

Exercise 13: choose the filter

After selecting \([j,j+k)\), which starts remain?

Solution. Those \(r\) with \(j+k\le r\).

Exercise 14: cover a deleted start

Why is any deleted \(r\) inside the interval?

Solution. The start \(j\) was chosen as the minimum of the current finite marked set, so every current candidate \(r\) satisfies \(j\le r\). The survivor filter keeps exactly candidates with \(j+k\le r\). A deleted candidate fails that comparison; linear order therefore gives \(r\lt j+k\). Combining the two inequalities yields \(j\le r\lt j+k\), precisely the membership condition for \([j,j+k)\). This proves coverage at the moment of deletion. The recursive call never needs to remember that candidate again.

Exercise 15: allow the endpoint

Why does \(r=j+k\) remain?

Solution. The first interval excludes its right endpoint, so that start is not covered yet.

Exercise 16: prove positive movement

Why is \(j+k\gt j\)?

Solution. The length premise gives \(k\gt0\).

Exercise 17: justify strong induction

Why not recurse on marked-set cardinality alone?

Solution. That could prove termination, but the construction also needs an exact indexed tail horizon. Strong induction on remaining horizon aligns with the target type arithmetic.

Exercise 18: explain the crossing branch

If \(j+k\) exceeds the old horizon end, why are all marks covered?

Solution. Let the old endpoint be \(o+H\). For any remaining mark \(r\), minimum selection gives \(j\le r\), while the input range gives \(r\lt o+H\). The crossing branch is the negation of \(j+k\le o+H\), so linear order gives \(o+H\lt j+k\). Thus \(j\le r\lt o+H\lt j+k\), and therefore \(r\in[j,j+k)\). One selected interval covers every remaining mark, so returning an empty recursive tail loses nothing. The endpoint may cross the old horizon but remains within the enlarged one because \(k\le m\).

Exercise 19: derive endpoint slack

Show \(j+k\lt H+m\) from \(j\lt H\) and \(k\le m\).

Solution. Monotonicity of addition gives \(j+k\le j+m\) from \(k\le m\). Adding \(m\) to \(j\lt H\) gives \(j+m\lt H+m\). Transitivity then yields \(j+k\lt H+m\). Equivalently, add the strict inequality \(j\lt H\) to the weak inequality \(k\le m\). The strictness comes from the start bound, not from \(k\lt m\); an interval of maximal allowed length is still valid.

Exercise 20: inspect empty input

What packing exists when \(B=\varnothing\) and \(H=m=0\)?

Solution. The empty packing at horizon zero, with vacuous coverage and provenance.

Exercise 21: reject uniqueness

Does the existence theorem say the returned packing is unique?

Solution. No. It specifies contracts, not an extensional uniqueness property.

Exercise 22: explain monotonicity

Why widen a selection certificate from filtered marks to original marks?

Solution. Recursive intervals start in the filtered subset, which is also a subset of the original eligible set.

High camp: connect costs and cardinality

Exercise 23: write one selected cost

What term corresponds to \([j,j+k)\)?

Solution. \(X_k(T^j\omega)\).

Exercise 24: reject additivity

Why can this not be replaced by a sum of \(X_1\) terms?

Solution. Shifted subadditivity gives only an upper inequality for a general process.

Exercise 25: align an offset

What library law turns a nested iterate into an absolute start?

Solution. Function.iterate_add_apply, together with natural addition rearrangement.

Exercise 26: sum weak costs

Why does the weak theorem include an empty packing?

Solution. Its base case is \(0\le0\).

Exercise 27: sum strict costs

Why does strictness require at least one interval?

Solution. An empty strict sum would require \(0\lt0\).

Exercise 28: derive positive horizon

Why does a nonempty packing have positive horizon?

Solution. It contains a selected interval of positive natural length.

Exercise 29: delete an initial gap

When is \(X_g\le0\) available?

Solution. Exactly when \(g\ne0\).

Exercise 30: handle zero initial gap

What should the proof do when \(g=0\)?

Solution. Avoid splitting a gap term and begin at the selected interval.

Exercise 31: handle zero terminal gap

What should the proof do when the last interval ends at the horizon?

Solution. Stop at that interval rather than introduce \(X_0\).

Exercise 32: derive the raw inequality

What remains after every positive gap is deleted?

Solution. The sum of selected interval process costs.

Exercise 33: use coverage

What cardinality inequality follows from \(B\subseteq P.coveredFinset\)?

Solution. \(|B|\le P.coveredLength\).

Exercise 34: use the sign of \(c\)

If \(c\le0\), what follows from \(|B|\le L\)?

Solution. After casting the natural inequality to the reals, multiply both sides by the nonpositive number \(c\). Order reverses, giving \(cL\le c|B|\). For a concrete check, take \(c=-2\), \(|B|=6\), and \(L=9\). Then \(-18\le-12\). This direction is what the process proof needs: an intermediate upper bound by the more negative number \(cL\) implies the weaker requested bound by \(c|B|\). If \(c\) were positive, the comparison would point the other way and coverage alone would not close the theorem.

Summit: audit boundaries and claims

Exercise 35: empty weak conclusion

What does the weak marked-card theorem say for \(B=\varnothing\)?

Solution. At positive horizon, \(X_N\le0\).

Exercise 36: empty strict failure

Why are strict local assumptions not enough for empty \(B\)?

Solution. They are vacuous, while the desired strict empty-sum conclusion can be false.

Exercise 37: time-zero failure

Use \(X_0=1\) to refute an unconditional empty-packing theorem.

Solution. At horizon zero the empty cost is zero, so \(1\le0\) fails.

Exercise 38: positive empty validity

Why is the same empty packing valid at positive horizon under the sign premise?

Solution. The theorem reduces to the assumed \(X_N\le0\).

Exercise 39: long cover inequality

Can one interval of length three cover two marks?

Solution. Yes. Let the interval be \([0,3)\) and the marked set be \(\{0,1\}\). Both starts lie in the selected union, so Covers holds. If the prescribed length at zero is three, the single interval can also satisfy SelectedFrom. The marked cardinality is two, the interval count is one, and the covered length is three. This single fixture shows that all three quantities can differ. It also exercises strict coverage-to-length inequality without suggesting any asymptotic density.

Exercise 40: audit candidate baggage

Which candidate field does the pointwise packing theorem use?

Solution. Shifted subadditivity. Integrability remains in the receiver but is not projected by the proof.

Exercise 41: audit centered time zero

Does the centered wrapper require its process value at zero to vanish?

Solution. No. The packing theorem discards only positive gaps and retains an explicit positive-horizon boundary.

Exercise 42: audit matrix index

Can the cocycle wrapper be instantiated on an empty finite index type?

Solution. Yes. The compiled smoke test does so.

Exercise 43: reject density language

Why is \(|B|\le L\) not a density theorem?

Solution. It contains no growing sequence, normalization by horizon, or limit.

Exercise 44: name the next theorem gap

What remains before a lower asymptotic estimate?

Solution. First define the favorable-start event with exact measurable quantifiers over the allowed finite lengths, then prove its measurability. Second connect the event to a stationary finite-measure dynamical system and obtain an orbit-frequency statement, for example through a suitable pointwise ergodic theorem whose hypotheses are all checked. Third combine that frequency with the finite marked-card bound along a growing sequence of horizons. Finally justify normalization, passage to a liminf or limit, almost-everywhere exceptional sets, integrability, and any expectation identity required by the intended Kingman statement. RMT-21 provides the finite inequality inserted into that future argument; it provides none of the measure-theoretic or limiting bridges by itself.

Run the complete finite worksheet on a normal computer

The following file imports only Lean’s Std library. It does not import Mathlib or this project. It computes both numeric examples, exposes every greedy round, prints the gap-length-tail decoder, separates selected starts from covered marks, checks the sign reversal, and evaluates the empty, nonempty, singleton, abutting, and time-zero boundaries.

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

import Std

namespace OrderedIntervalPackingDeepDiveTutorial

abbrev NatInterval := Nat × Nat

def packing : List NatInterval :=
  [(1, 3), (3, 4), (6, 9)]

def nearMiss : List NatInterval :=
  [(1, 3), (2, 4), (6, 9)]

def openingMarked : List Nat :=
  [1, 2, 3, 6, 8]

def inside (I : NatInterval) (j : Nat) : Bool :=
  decide (I.1 ≤ j ∧ j < I.2)

def coveredPositions (horizon : Nat)
    (family : List NatInterval) : List Nat :=
  (List.range horizon).filter fun j =>
    family.any fun I => inside I j

def intervalLength (I : NatInterval) : Nat :=
  I.2 - I.1

def totalLength (family : List NatInterval) : Nat :=
  family.foldl (fun total I => total + intervalLength I) 0

def isOrdered : List NatInterval → Bool
  | [] => true
  | [_] => true
  | I :: J :: rest =>
      decide (I.2 ≤ J.1) && isOrdered (J :: rest)

def allCovered (marked : List Nat)
    (horizon : Nat) (family : List NatInterval) : Bool :=
  marked.all fun j => (coveredPositions horizon family).contains j

/-
The deeper example uses H = 10, m = 4, and marked starts
[1, 2, 4, 5, 8, 9].  The leftmost start chooses its prescribed interval;
every mark inside it is deleted; recursion continues with the survivors.
-/

def marked : List Nat :=
  [1, 2, 4, 5, 8, 9]

def prescribedLength (start : Nat) : Nat :=
  match start with
  | 1 => 3
  | 4 => 2
  | 8 => 4
  | _ => 1

structure GreedyRound where
  remainingBefore : List Nat
  selectedStart : Nat
  selectedInterval : NatInterval
  coveredMarks : List Nat
  survivors : List Nat
  deriving Repr, DecidableEq

def greedyRoundsWithFuel :
    Nat → List Nat → List GreedyRound
  | 0, _ => []
  | _ + 1, [] => []
  | fuel + 1, start :: rest =>
      let endpoint := start + prescribedLength start
      let covered :=
        start :: rest.filter (fun j => decide (j < endpoint))
      let survivors :=
        rest.filter (fun j => decide (endpoint ≤ j))
      { remainingBefore := start :: rest
        selectedStart := start
        selectedInterval := (start, endpoint)
        coveredMarks := covered
        survivors := survivors } ::
        greedyRoundsWithFuel fuel survivors

def greedyRounds (starts : List Nat) : List GreedyRound :=
  greedyRoundsWithFuel starts.length starts

def greedyPacking (starts : List Nat) : List NatInterval :=
  (greedyRounds starts).map GreedyRound.selectedInterval

def selectedStarts (family : List NatInterval) : List Nat :=
  family.map Prod.fst

def selectionCoverageLedger :
    List (Nat × Bool × Bool) :=
  let family := greedyPacking marked
  let selected := selectedStarts family
  let covered := coveredPositions 14 family
  marked.map fun j =>
    (j, selected.contains j, covered.contains j)

def encodeFrom (cursor horizon : Nat) :
    List NatInterval → List Nat
  | [] => [horizon - cursor]
  | I :: rest =>
      (I.1 - cursor) :: intervalLength I ::
        encodeFrom I.2 horizon rest

def gapLengthTail (horizon : Nat)
    (family : List NatInterval) : List Nat :=
  encodeFrom 0 horizon family

structure SignLedger where
  markedCount : Nat
  coveredLength : Nat
  coefficient : Int
  coefficientTimesCovered : Int
  coefficientTimesMarked : Int
  nonpositiveReversalHolds : Bool
  positiveCoefficientWouldWork : Bool
  weakSelectedCost : Int
  strictSelectedCost : Int
  strictMarkedBoundHolds : Bool
  deriving Repr, DecidableEq

def signLedger : SignLedger :=
  let family := greedyPacking marked
  let covered := totalLength family
  let count := marked.length
  let c : Int := -2
  let weakCost : Int := ([-6, -4, -8] : List Int).sum
  let strictCost : Int := ([-7, -5, -9] : List Int).sum
  { markedCount := count
    coveredLength := covered
    coefficient := c
    coefficientTimesCovered := c * covered
    coefficientTimesMarked := c * count
    nonpositiveReversalHolds := decide (c * covered ≤ c * count)
    positiveCoefficientWouldWork :=
      decide ((2 : Int) * covered ≤ 2 * count)
    weakSelectedCost := weakCost
    strictSelectedCost := strictCost
    strictMarkedBoundHolds := decide (strictCost < c * count) }

def positiveAtZeroProcess (horizon : Nat) : Int :=
  if horizon = 0 then 1 else -(horizon : Int)

structure BoundaryLedger where
  emptyGreedyPacking : List NatInterval
  emptyWeakAtPositiveTime : Bool
  emptyWeakAtTimeZero : Bool
  emptyStrictSum : Bool
  nonemptyStrictSum : Bool
  singletonOrdered : Bool
  abuttingOrdered : Bool
  deriving Repr, DecidableEq

def boundaryLedger : BoundaryLedger :=
  { emptyGreedyPacking := greedyPacking []
    emptyWeakAtPositiveTime := decide (positiveAtZeroProcess 4 ≤ 0)
    emptyWeakAtTimeZero := decide (positiveAtZeroProcess 0 ≤ 0)
    emptyStrictSum := decide ((0 : Int) < 0)
    nonemptyStrictSum := signLedger.strictMarkedBoundHolds
    singletonOrdered := isOrdered [(3, 4)]
    abuttingOrdered := isOrdered [(1, 3), (3, 4)] }

#eval coveredPositions 10 packing
#eval [totalLength packing, (coveredPositions 10 packing).length]
#eval [isOrdered packing, allCovered openingMarked 10 packing]
#eval coveredPositions 10 nearMiss
#eval [totalLength nearMiss, (coveredPositions 10 nearMiss).length]
#eval isOrdered nearMiss
#eval greedyRounds marked
#eval greedyPacking marked
#eval gapLengthTail 14 (greedyPacking marked)
#eval [totalLength (greedyPacking marked),
  (gapLengthTail 14 (greedyPacking marked)).sum]
#eval coveredPositions 14 (greedyPacking marked)
#eval selectionCoverageLedger
#eval signLedger
#eval boundaryLedger

example : coveredPositions 10 packing = [1, 2, 3, 6, 7, 8] := by
  native_decide
example : [totalLength packing, (coveredPositions 10 packing).length] =
    [6, 6] := by native_decide
example : isOrdered packing = true := by native_decide
example : allCovered openingMarked 10 packing = true := by native_decide

example : coveredPositions 10 nearMiss = [1, 2, 3, 6, 7, 8] := by
  native_decide
example : [totalLength nearMiss, (coveredPositions 10 nearMiss).length] =
    [7, 6] := by native_decide
example : isOrdered nearMiss = false := by native_decide

example : greedyPacking marked = [(1, 4), (4, 6), (8, 12)] := by
  native_decide
example : gapLengthTail 14 (greedyPacking marked) =
    [1, 3, 0, 2, 2, 4, 2] := by native_decide
example : coveredPositions 14 (greedyPacking marked) =
    [1, 2, 3, 4, 5, 8, 9, 10, 11] := by native_decide
example : allCovered marked 14 (greedyPacking marked) = true := by
  native_decide
example : selectedStarts (greedyPacking marked) = [1, 4, 8] := by
  native_decide

example : signLedger.nonpositiveReversalHolds = true := by native_decide
example : signLedger.positiveCoefficientWouldWork = false := by native_decide
example : signLedger.weakSelectedCost = -18 := by native_decide
example : signLedger.strictSelectedCost = -21 := by native_decide
example : signLedger.strictMarkedBoundHolds = true := by native_decide

example : boundaryLedger.emptyWeakAtPositiveTime = true := by native_decide
example : boundaryLedger.emptyWeakAtTimeZero = false := by native_decide
example : boundaryLedger.emptyStrictSum = false := by native_decide
example : boundaryLedger.nonemptyStrictSum = true := by native_decide
example : boundaryLedger.singletonOrdered = true := by native_decide
example : boundaryLedger.abuttingOrdered = true := by native_decide

end OrderedIntervalPackingDeepDiveTutorial

The important syntax is deliberately ordinary:

• List.range horizon enumerates \(0,\ldots,\text{horizon}-1\);
• filter keeps the positions or survivors satisfying a Boolean test;
• decide computes a proposition such as \(j\lt\text{endpoint}\);
• structure GreedyRound gives names to the four columns of one algorithm step;
• #eval prints a value; and
• each example ... := by native_decide is a kernel-checked proof of the displayed finite equality or inequality.

With the repository’s pinned Lean toolchain already installed, a human types:

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

This is a small standalone tutorial. It imports only Std, uses short lists, and is suitable for a normal macOS or Linux host. It does not validate the Mathlib project module. Successful execution prints exactly:

[1, 2, 3, 6, 7, 8]
[6, 6]
[true, true]
[1, 2, 3, 6, 7, 8]
[7, 6]
false
[{ remainingBefore := [1, 2, 4, 5, 8, 9],
   selectedStart := 1,
   selectedInterval := (1, 4),
   coveredMarks := [1, 2],
   survivors := [4, 5, 8, 9] },
 { remainingBefore := [4, 5, 8, 9],
   selectedStart := 4,
   selectedInterval := (4, 6),
   coveredMarks := [4, 5],
   survivors := [8, 9] },
 { remainingBefore := [8, 9],
   selectedStart := 8,
   selectedInterval := (8, 12),
   coveredMarks := [8, 9],
   survivors := [] }]
[(1, 4), (4, 6), (8, 12)]
[1, 3, 0, 2, 2, 4, 2]
[9, 14]
[1, 2, 3, 4, 5, 8, 9, 10, 11]
[(1, true, true), (2, false, true), (4, true, true), (5, false, true), (8, true, true), (9, false, true)]
{ markedCount := 6,
  coveredLength := 9,
  coefficient := -2,
  coefficientTimesCovered := -18,
  coefficientTimesMarked := -12,
  nonpositiveReversalHolds := true,
  positiveCoefficientWouldWork := false,
  weakSelectedCost := -18,
  strictSelectedCost := -21,
  strictMarkedBoundHolds := true }
{ emptyGreedyPacking := [],
  emptyWeakAtPositiveTime := true,
  emptyWeakAtTimeZero := false,
  emptyStrictSum := false,
  nonemptyStrictSum := true,
  singletonOrdered := true,
  abuttingOrdered := true }

The transcript connects the diagrams to executable facts. The first six lines are the separate six-position valid/near-miss worksheet. The remaining lines belong to the larger \(H=10,m=4\) greedy worksheet.

Read and reproduce the checked Lean slice

The source-order entry point is NonlinearDynamics.Random.RandomCocycles.SubadditiveIntervalPacking. From the repository root, the direct full project check is:

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

The integrated repository module has 1,131 lines and SHA-256 732187ce77b5efa14df3a992f194d5dce4dfc8d9f5fa6dbaf658c5ed41ef4f4d. That hash records the exact source audited for this chapter; the repository module is the present authority. This is a full project check, not a standalone tutorial. It may compile substantial dependencies and therefore may require substantial disk space and memory.

What the milestone establishes

RMT-21 establishes:

1. a structural finite type for ordered positive-length half-open intervals;
2. absolute endpoint and covered-position decoders;
3. interval-count preservation;
4. containment and pairwise disjointness;
5. exact covered cardinality;
6. separate coverage and selection-provenance contracts;
7. an explicit leftmost selector at enlarged horizon \(H+m\);
8. coverage of every original marked start;
9. exact prescribed length for every selected interval;
10. strict endpoint slack for selector output;
11. weak and strict per-interval cost transport;
12. a raw finite subadditive packing inequality with exact time-zero boundary;
13. weak and strict covered-length bounds;
14. weak marked-cardinality bounds for arbitrary finite marked sets;
15. strict marked-cardinality bounds for nonempty marked sets;
16. end-to-end greedy-cover theorems; and
17. candidate, centered-process, and centered cocycle packing-sum wrappers.

The exact stopping point

This milestone does not establish:

1. measurability of a future favorable-start event;
2. a positive or asymptotic measure for that event;
3. a pointwise Birkhoff theorem;
4. a maximal inequality;
5. a density theorem for marked starts;
6. Kingman’s subadditive ergodic theorem;
7. almost-everywhere convergence of \(X_n/n\);
8. convergence in mean;
9. identification of a limit with an infimum of expectations;
10. invariance or constancy of a liminf;
11. a probability-space normalization;
12. ergodicity of a base or its powers;
13. independence of intervals or marks;
14. uniqueness or optimality of the packing;
15. a signed cocycle growth rate;
16. a Lyapunov exponent; or
17. an Oseledets splitting.

The leftmost selector is a finite combinatorial theorem. The cost inequality is a finite algebraic theorem. Their composition remains finite.

Where to continue

Finite Phase Averaging for Nonpositive Subadditive Processes is the immediate predecessor and complementary finite upper mechanism.

The ordered interval packing glossary chapter is the compact convention, boundary, and theorem reference. The phase averaging and orbit-majorant centering chapters explain the finite upper estimate and positive-horizon sign reduction.

Pack the Marked Starts: Ordered Disjoint Intervals for Subadditive Cocycles in Lean gives the complete declaration-by-declaration source tour and boundary-smoke ledger.

The next checked ridge is Birkhoff Convergence Events Before the Pointwise Ergodic Theorem. It constructs a measurable, representative-safe, exactly invariant event for ordinary Birkhoff-average convergence and proves conditional ergodic rigidity. It does not yet produce membership, orbit frequency for the marked set, or the pointwise and subadditive limit theorems still needed after this finite packing layer.

References

All links below were checked on 2026-07-21. The pinned local Mathlib checkout at commit 81a5d257c8e410db227a6665ed08f64fea08e997 is the exact authority for upstream declarations.

Mathlib contributors. Finite interval definitions, with the pinned half-open membership theorem, and natural interval cardinality. These sources define the finite half-open intervals and endpoint-difference cardinality used by the packing decoder.

Mathlib contributors. Finite-set cardinality, with the pinned disjoint-union theorem. This theorem is the library bridge from structural disjointness to exact covered cardinality.

Mathlib contributors. Function iteration, with the pinned addition law. RMT-21 uses this finite identity to align recursively shifted samples with absolute selected starts.

Steven P. Lalley. Kingman’s Subadditive Ergodic Theorem, University of Chicago lecture notes, 3 pages, undated, accessed 2026-07-21. Page 2 states the packed-process inequality as equation (6). Page 3 gives the leftmost blue-interval selection and explains why all bad starts remain covered. The notes use inclusive intervals and their displayed strict start-to-end chain excludes length one despite the next paragraph allowing \(1\le k\le m\). This chapter uses the corrected half-open convention and also separates the weak empty-set conclusion from the strict nonempty one.

J. Michael Steele. Kingman’s subadditive ergodic theorem, Annales de l’Institut Henri Poincare, Probabilites et Statistiques 25(1), 93-98, 1989, with the archival PDF. Page 95 gives a related conceptually algorithmic interval decomposition in a full proof of Kingman’s theorem. It motivates explicit finite algorithms but does not state RMT-21’s selector contract.

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 primary source is the historical asymptotic destination. The present chapter proves and explains only a finite ingredient.

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