Pack the Marked Starts: Ordered Disjoint Intervals for Subadditive Cocycles in Lean

This is the proof-to-prose companion for formalization/NonlinearDynamics/Random/RandomCocycles/SubadditiveIntervalPacking.lean. It covers all fifty-four public named declarations, the private selector engine, and all twelve private named boundary fixtures in exact source order. Anonymous compiled examples are audited together in the boundary section.

Its immediate predecessor is Average the Phases: Sliding-Block Bounds for Subadditive Cocycles in Lean. That chapter supplies a complementary finite upper mechanism. The compact definition here is the ordered interval packing glossary entry. The parallel textbook treatment is Finite Ordered Interval Packing for Nonpositive Subadditive Processes.

Its immediate successor is Convergence Without Existence: Birkhoff Events and Ergodic Rigidity in Lean. That chapter isolates a measurable or null-measurable convergence event for one-step Birkhoff averages and proves its exact finite-prefix invariance and conditional ergodic rigidity. It does not yet make the marked set here large.

Choose a route up

Learning objectives

By the summit, a reader should be able to:

1. translate an inclusive integer interval into a half-open natural interval;
2. explain why positive length admits a singleton interval;
3. explain why endpoint equality permits two half-open intervals to abut;
4. read the horizon index of OrderedNatIntervalPacking;
5. distinguish a prefix gap, selected length, recursive tail, and terminal gap;
6. recover absolute endpoints from recursively relative gaps;
7. distinguish the interval list from the finite set of covered positions;
8. prove that recovered interval count equals the structural interval count;
9. explain why structural order implies pairwise set disjointness;
10. derive exact covered cardinality from disjoint finite unions;
11. distinguish Covers from SelectedFrom;
12. explain why selector provenance needs an absolute recursive offset;
13. state the enlarged-horizon selector theorem;
14. justify \(H+m\) from \(j\lt H\) and \(\ell(j)\le m\);
15. describe the leftmost-mark filtering rule;
16. explain why every deleted mark remains covered;
17. explain the branch in which the first interval crosses the old horizon;
18. explain why selected endpoints are strictly below the enlarged horizon;
19. define the cost of a packing;
20. distinguish one interval cost from a pointwise sum over its covered sites;
21. transport per-marked-start estimates through SelectedFrom;
22. sum weak interval estimates over an empty or nonempty packing;
23. explain why strict summation needs a nonempty packing;
24. derive horizon positivity from nonzero interval count;
25. split and discard only positive gaps in the process inequality;
26. reproduce the time-zero countermodel;
27. turn coverage into \(|B|\le L\), where \(L\) is covered length;
28. explain why multiplication by \(c\le0\) reverses that comparison;
29. state both covered-length process bounds;
30. state both marked-cardinality process bounds;
31. state both end-to-end greedy-cover bounds;
32. identify the extra horizon premise on the universal weak greedy theorem;
33. identify the nonempty-mark premise on the strict greedy theorem;
34. separate wrapper fields from fields used by a pointwise proof;
35. explain why the empty matrix index remains allowed;
36. list every asymptotic claim that this finite module deliberately does not make.

Why favorable starts overlap

The lower-estimate stage of a classical subadditive argument begins with a finite set of orbit positions where some short interval has favorable average cost. At a marked position \(j\), choose a positive length \(\ell(j)\le m\). The associated half-open interval is

Keeping every \(I_j\) is usually impossible because they may overlap. Yet discarding intervals arbitrarily can lose the coverage needed to compare total selected length with the number of marked starts.

Lalley’s lecture notes use a leftmost rule: keep the interval at the leftmost remaining marked start, delete every candidate whose left endpoint is already inside that interval, then repeat (Lalley). A deleted start is not forgotten. It is covered by the interval that caused its deletion. The next retained start lies at or to the right of the previous right endpoint, so the retained half-open intervals are disjoint.

The Lean theorem is not a transcription of every later probabilistic step in those notes. It isolates and checks only the finite selector, coverage, cardinality, and subadditive-cost layer.

What is inherited, repaired, and newly packaged

Three source roles must stay separate. Lalley’s equation (6) motivates the finite packed-process inequality, and the following paragraph motivates leftmost selection. Steele supplies related algorithmic proof lineage for a finite interval decomposition. Kingman’s 1968 paper is the historical asymptotic destination. None of those sources states the exact Lean interface Covers ∧ SelectedFrom, the indexed gap representation, or the weak-versus-strict empty-set API used here.

The endpoint repair can be verified extensionally. For \(k\gt0\),

Thus the repair preserves the set and its \(k\) integer positions. It changes only the faulty strict start-to-last-point comparison. Likewise,

so the corrected separation relation is weak at the excluded endpoint.

RMT-21 then adds formal packaging needed by later code: exact interval and covered-set decoders, a proof that covered cardinality equals summed length, separate coverage and provenance contracts, weak and strict local-cost predicates, a time-zero countermodel, and wrappers for the established subadditive-process and cocycle layers. Those are checked elaborations of the finite idea, not claims that the cited sources used the same data type or theorem names.

Half-open intervals encode the boundary convention

A half-open natural interval \([a,b)\) contains exactly those \(j\) with \(a\le j\lt b\). It has \(b-a\) positions when \(a\le b\). This convention has three advantages here:

1. length is the endpoint difference;
2. adjacent intervals \([a,b)\) and \([b,c)\) are disjoint; and
3. the horizon \([0,N)\) contains exactly the natural positions below \(N\).

Mathlib provides both Finset.Ico for finite covered positions and Set.Ico for set-theoretic disjointness. The pinned definitions and cardinality theorems are cited below (finite interval definitions, natural interval cardinality).

The module stores endpoints as pairs of natural numbers. It does not introduce a parallel interval structure. The packing itself carries the stronger invariant that the pairs arise in chronological order with positive lengths.

The gap-length-tail code is already a proof

The central type is indexed by its ambient horizon:

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

The empty constructor retains a horizon even though it selects no intervals. The cons constructor lays out three consecutive regions:

• an uncovered gap, which may have length zero;
• one selected interval, whose length is strictly positive; and
• a recursively encoded tail.

The recursive tail begins after the first gap and interval. A gap stored in the tail is therefore an intermediate gap in absolute coordinates. An empty value at the end retains the terminal gap. No separate proposition is needed to say that a later interval begins after the earlier one.

Two elementary folds expose the packing size. intervalCount counts constructors of the second kind. coveredLength adds their lengths. Neither count includes any gap.

Decode endpoints and covered positions

The packing stores relative gaps, but users need absolute starts. The helper intervalsFrom carries an absolute offset through recursion. At a cons node with gap \(g\) and length \(\ell\), it emits

and recurses from the emitted right endpoint. The public intervals decoder starts at offset zero.

The finite-set decoder follows the same traversal. coveredFinsetFrom unions the current Finset.Ico with the shifted tail. The public coveredFinset again starts at zero.

The two views answer different questions:

Theorems connect the views. length_intervalsFrom and length_intervals show that decoding preserves interval count. The two membership equivalences state that a position belongs to the covered finite set exactly when one recovered interval contains it. The shifted bounds theorem then places every covered position inside the shifted horizon.

Coverage and provenance are different contracts

For a finite marked set \(B\),

def Covers (P : OrderedNatIntervalPacking N) (marked : Finset ℕ) : Prop :=
  marked ⊆ P.coveredFinset

says only that every mark lies somewhere in the selected union. It does not say that selected intervals began at marks. It does not say their lengths came from the prescribed function. A large unrelated interval could satisfy Covers.

The provenance predicate SelectedFromFrom supplies the missing contract recursively. At an absolute offset, every cons node must begin at a member of the eligible marked set and its stored length must equal the value of the prescribed length function at that start. SelectedFrom is the zero-offset public form.

This separation is not bureaucracy. The later proof uses each certificate for a different purpose:

• Covers gives the cardinality comparison;
• SelectedFrom transports a cost hypothesis stated only at marked starts to every selected interval.

The monotonicity theorem permits a recursive certificate over a filtered set of remaining marks to be widened back to the original set. The two intervals_chosen theorems expose the recursive certificate in terms of decoded endpoints. The enlarged-horizon endpoint theorem combines that provenance with \(j\lt H\) and \(\ell(j)\le m\) to prove every selected right endpoint is strictly below \(H+m\).

The leftmost selector covers every marked start

Fix \(H,m\in\mathbb N\), a finite set \(B\subseteq\operatorname{range}(H)\), and \(\ell:\mathbb N\to\mathbb N\) with \(0\lt\ell(j)\le m\) on \(B\). The public selector states

The private engine proves an offset form by strong induction on the remaining old-horizon length.

1. If the marked set is empty, return an empty packing with horizon \(H+m\).
2. Otherwise choose its minimum \(j\).
3. Let \(\ell=\ell(j)\).
4. If \(j+\ell\le\text{offset}+H\), filter the remaining marks to starts at least \(j+\ell\), then recurse on the shorter tail horizon.
5. If the interval crosses the old horizon, stop after this interval. Every remaining marked start lies between \(j\) and the interval endpoint.

The first branch is where abutment appears. A later start equal to \(j+\ell\) survives the filter and may begin the next selected interval. That is correct for half-open intervals.

The second branch is why the target horizon is enlarged. Because \(j\lt H\) and \(\ell\le m\), the chosen endpoint still lies strictly below \(H+m\), even when it passes the end of the old horizon.

At each deletion, coverage is local: a mark removed because it lies before \(j+\ell\) belongs to the current interval. A mark that survives is covered by the recursive packing. This induction proves coverage without a separate maximality or optimality theorem.

Trace one greedy run all the way through

The selector becomes easier to audit when the candidate set, deletion filter, and type index are written side by side. Take

Use prescribed lengths \(\ell(1)=3\), \(\ell(4)=2\), and \(\ell(8)=4\). The other marked starts may have any positive length at most four because they will be removed before selection.

Round one removes one and two because both are below the endpoint four. The mark four survives: the filter keeps starts satisfying \(4\le r\), exactly matching membership outside the half-open interval \([1,4)\). Round two removes four and five. The first two selected intervals abut, and the weak endpoint comparison certifies that they remain disjoint.

Round three exposes the enlarged-horizon case. The endpoint twelve passes the old endpoint ten. Every remaining mark is at least eight because eight is minimal, and every one is below ten by the input bound. Therefore every remaining mark lies in \([8,12)\), and recursion can stop.

The output packing has the run-length code

Reading those numbers gives an initial gap of one, selected length three, zero gap, selected length two, gap two, selected length four, and terminal tail two. The type index checks the entire sum:

Its selected intervals cover

so the covered length is nine while \(|B|=6\). The three additional covered positions are harmless. Coverage is the inclusion \(B\subseteq P.\operatorname{coveredFinset}\), not equality of those finite sets.

This trace mirrors the private induction engine almost line for line:

1. marked.min’ produces the least start and its membership proof.
2. marked.filter (j + ell ≤ ·) records precisely the survivors.
3. A second comparison decides whether the endpoint remains within the old horizon.
4. In the recursive branch, Finset.filter_subset and SelectedFromFrom.mono widen tail provenance back to the original marked set.
5. In the crossing branch, minimality and the old start bound prove coverage directly.
6. omega proves both the strictly smaller induction index and the reconstructed \(H+m\) type index.

The deletion proof and the coverage proof are the same argument viewed from opposite sides. If a candidate fails the survivor test, then it is below the selected endpoint. Minimality puts it at or above the selected start. Those two inequalities place it inside the current interval.

Why deleted starts still carry length hypotheses

In the worked run, the selector never consults the prescribed lengths at two, five, or nine. The public theorem nevertheless assumes a positive bounded length at every original mark. This is intentional uniformity, not a hidden claim that every length is used. Before execution, any marked start could become the minimum of a recursive survivor set. The global hypothesis lets each recursive call obtain its chosen length without rebuilding a new partial function.

After selection, SelectedFrom records lengths only for intervals that were actually kept. Likewise, the local-cost bridge consumes the marked-start cost hypothesis only at selected starts. A deleted mark is accounted for geometrically through coverage, not algebraically through its own process term. This separation is why one long favorable interval can pay for several marked starts without double-counting overlapping costs.

Follow the cardinality sign reversal numerically

Suppose the common coefficient is \(c=-2\), and the selected local costs obey

The recursive cost sum is at most \(-18\), which is \(c\cdot9\), where nine is the covered length. Shifted subadditivity and positive-time nonpositivity give

Coverage gives \(6\le9\). Since \(c\le0\), multiplying by \(c\) reverses the comparison:

Consequently \(X_{14}(\omega)\le-12=c|B|\). The marked-card theorem is not claiming that six selected intervals exist. It uses three selected intervals covering six marks, nine covered positions, and one sign-aware multiplication step.

In Lean, the relevant proof first obtains a natural-number inequality from card_le_coveredLength_of_covers. The statement is moved into \(\mathbb R\) with exact_mod_cast. Only then does mul_le_mul_of_nonpos_left apply the hypothesis hc : c ≤ 0. Keeping those stages separate makes the reversal visible to the reader and the elaborator.

Why the ambient horizon is \(H+m\)

The marked-start horizon controls starts, not endpoints. If \(j\lt H\) and \(0\lt\ell(j)\le m\), then

The inequality is strict because \(j\le H-1\) when \(H\gt0\). The packing type itself only promises endpoints at most its horizon; the selector provenance proves the stronger strict endpoint bound.

Using horizon \(H\) would reject a legal marked start near its right edge. Using an unbounded ambient horizon would erase a finite quantity required by the later process inequality. The explicit \(H+m\) is a clean uniform choice: it gives the strict endpoint bound above while keeping the degenerate \(H=m=0\) case free of truncated subtraction. A sharper positive-horizon encoding could use \(H+m-1\), but that refinement is not needed here.

The empty case remains informative. If \(H=m=0\), the selector exists and returns an empty packing of horizon zero. The combinatorics are valid. A later process inequality at that horizon is not valid unless time zero is separately controlled.

Disjointness turns union size into covered length

The shifted containment theorem shows every recovered interval lies inside its ambient shifted horizon. The shifted pairwise theorem shows every earlier right endpoint is at most every later left endpoint. Mapping this endpoint relation to Set.Ico gives pairwise set disjointness.

The exact cardinality proof then follows the recursive representation. The current interval contributes exactly its length. It is disjoint from the tail covered set because every tail position begins at or beyond the current right endpoint. Mathlib’s disjoint-union cardinality theorem combines the two sizes (finite-set cardinality). Thus

If \(P\) covers \(B\), finite-set monotonicity gives

Coverage of a nonempty marked set also proves that the packing has nonzero interval count. An empty packing covers no positions. This small lemma is the bridge later used to obtain strict finite summation.

From per-marked-start costs to recursive interval costs

For a map \(T\), process \(X\), sample \(\omega\), and coefficient \(c\), the packing cost is

This display is explanatory. Lean defines the sum recursively so that every tail is evaluated at the correctly shifted sample. It is not a sum of the one-step values \(X_1\) over all covered positions.

The predicates EveryIntervalCostLE and EveryIntervalCostLT mirror that recursion. Their empty branch is True. At a cons node they assert a weak or strict linear bound for the current selected interval and recur at the shifted sample.

The two offset bridge theorems are the key interface between selector and dynamics. A SelectedFromFrom certificate identifies the current absolute start and prescribed length. Natural-iterate addition aligns the recursively shifted sample with that absolute start. The public zero-offset bridges then state:

• weak bounds at every marked start imply EveryIntervalCostLE for the selected packing;
• strict bounds at every marked start imply EveryIntervalCostLT.

The strict predicate implies the weak predicate pointwise. Summing weak bounds works for every packing, including empty. Summing strict bounds needs a nonzero interval count.

The finite subadditive packing inequality

Suppose \(X\) is shifted-subadditive and nonpositive at every positive horizon. For a packing \(P\) inside \(N\ne0\), RMT-21 proves

The direction can feel surprising. The selected interval costs may be negative. Every uncovered positive gap also has nonpositive cost, so deleting those gap terms makes the right side larger and preserves an upper bound.

The induction must avoid manufacturing a time-zero term. It treats three places carefully:

1. If the initial gap is zero, do not split it off.
2. If the terminal tail is zero, stop at the final selected interval rather than splitting a zero tail.
3. If the recursive rest contains another positive-length interval, its horizon is positive even when its leading gap is zero.

This is why the raw theorem assumes only positive-horizon nonpositivity. It does not impose \(X_0=0\) or even \(X_0\le0\).

For a nonempty packing, positive horizon follows from the selected positive-length interval. The companion theorem therefore replaces the explicit \(N\ne0\) premise by nonzero interval count.

Combining the process inequality with weak or strict interval-cost summation gives bounds by covered length:

for weak local estimates, and a strict version for nonempty \(P\).

Weak for every marked set, strict only when marks exist

Coverage gives \(|B|\le L\), where \(L\) is selected covered length. If \(c\le0\), multiplication reverses this inequality:

That sign premise is essential. It is the finite algebra that turns a lower bound on selected length into an upper bound on a negative process value.

The universal covering theorem is weak:

It accepts the empty marked set, but still requires \(N\ne0\). The end-to-end greedy version uses \(N=H+m\) and exposes exactly that horizon premise.

The strict theorem has a different boundary:

It requires \(B\) to be nonempty. Coverage then forces a nonempty packing, which supplies both horizon positivity and at least one strict summand. The end-to-end strict greedy theorem consequently needs no separate \(H+m\ne0\) premise.

The empty-set counterexample

Let \(X_n=0\) at every positive time and let \(B=\varnothing\). Every strict per-mark hypothesis is true because there is no marked \(j\). The greedy packing is empty and both its cost and marked cardinality are zero. A universal strict conclusion would demand \(0\lt0\), which is false.

This counterexample is not a corner to smooth over. It fixes the API: weak for all finite marked sets, strict under marked.Nonempty.

Proof dependencies versus wrapper baggage

The raw packing and process theorems use no measurable space, measure, integrability, probability, or ergodicity. The public candidate wrappers are methods on a stronger bundled object, so their receiver still carries finite horizon integrability and a measure. The proof projects only shifted subadditivity.

The centered-process wrapper additionally uses the already checked facts that orbit-majorant centering preserves shifted subadditivity and is nonpositive at positive horizons. It needs no time-zero normalization and no additional measure-preservation witness.

The matrix-cocycle wrapper takes the cocycle directly. The cocycle already stores a preserved base map, but the proof consumes only finite algebra and the centered log-positive observable’s subadditivity and sign. It does not require the separate generator-integrability package. Empty matrix dimension remains legal.

The current wrappers stop at the packing-sum inequality. The generic marked-card and greedy theorems can be instantiated with the centered cocycle observable without adding a separate wrapper for every composition.

The complete source-order tour

The following map covers all sixty-seven named declarations in the frozen 1,131-line source. Items 30 and 56 through 67 are private. The compiled anonymous examples after item 67 exercise the public surface and boundary models.

Items 1–7: the indexed packing and interval-list decoder

1. OrderedNatIntervalPacking is the horizon-indexed empty/cons representation.
2. intervalCount counts selected intervals.
3. coveredLength sums selected lengths.
4. intervalsFrom decodes endpoints from an absolute offset.
5. intervals is the zero-offset decoder.
6. length_intervalsFrom proves shifted decoding preserves count.
7. length_intervals is the public zero-offset count identity.

Items 8–18: covered positions, coverage, and cardinality

8. coveredFinsetFrom recursively unions shifted half-open finite intervals.
9. coveredFinset starts that decoder at zero.
10. mem_coveredFinsetFrom_iff_exists_interval equates shifted covered membership with membership in one decoded interval.
11. mem_coveredFinset_iff_exists_interval is the public zero-offset equivalence.
12. mem_coveredFinsetFrom_bounds puts every covered point inside the shifted horizon.
13. card_coveredFinsetFrom proves exact shifted union cardinality.
14. card_coveredFinset identifies public covered cardinality with covered length.
15. coveredFinset_subset_range contains every covered point below the horizon.
16. Covers defines coverage as marked-set inclusion.
17. intervalCount_ne_zero_of_covers_of_nonempty turns nonempty coverage into nonempty packing.
18. card_le_coveredLength_of_covers is the marked-count bridge.

Items 19–23: interval order and disjointness

19. intervalsFrom_inside proves shifted start, positive length, and endpoint containment.
20. intervalsFrom_pairwise proves chronological endpoint order.
21. intervals_pairwise specializes order to offset zero.
22. intervals_pairwiseDisjoint_Ico converts order to pairwise disjoint half-open sets.
23. intervals_inside gives the public nonempty/contained endpoint statement.

Items 24–31: selected provenance and the greedy selector

24. SelectedFromFrom recursively certifies absolute selected starts and prescribed lengths.
25. SelectedFrom is its zero-offset public form.
26. SelectedFromFrom.mono widens eligible starts along a finite-set inclusion.
27. SelectedFromFrom.intervalsFrom_chosen exposes provenance for every shifted decoded interval.
28. SelectedFrom.intervals_chosen exposes it at offset zero.
29. SelectedFrom.interval_end_lt_enlargedHorizon proves strict endpoint slack from marked-start and length bounds.
30. exists_orderedPacking_covering_from is the private offset strong-induction selector.
31. exists_orderedPacking_covering returns a packing at \(H+m\) with both coverage and provenance.

Items 32–43: packing costs and local-cost transport

32. cost recursively adds selected process costs at absolute starts.
33. coveredLength_le_horizon bounds selected length by ambient length.
34. horizon_pos_of_intervalCount_ne_zero derives positive horizon from a nonempty packing.
35. EveryIntervalCostLE is the recursive weak local-cost predicate.
36. EveryIntervalCostLT is the strict predicate.
37. EveryIntervalCostLT.le weakens every strict local estimate.
38. SelectedFromFrom.everyIntervalCostLE transports weak marked estimates at an arbitrary offset.
39. SelectedFromFrom.everyIntervalCostLT transports strict marked estimates at an arbitrary offset.
40. SelectedFrom.everyIntervalCostLE is the zero-offset weak bridge.
41. SelectedFrom.everyIntervalCostLT is the zero-offset strict bridge.
42. cost_le_mul_coveredLength sums weak local estimates.
43. cost_lt_mul_coveredLength sums strict estimates for a nonempty packing.

Items 44–51: process, covered-length, marked-card, and greedy bounds

44. le_cost_of_add_le_nonpos is the raw positive-horizon packing inequality.
45. le_cost_of_add_le_nonpos_of_nonempty derives horizon positivity internally.
46. le_mul_coveredLength_of_add_le_nonpos is the weak covered-length process bound.
47. lt_mul_coveredLength_of_add_le_nonpos is its strict nonempty counterpart.
48. le_mul_card_of_add_le_nonpos_of_covers combines weak cost, coverage, and \(c\le0\).
49. lt_mul_card_of_add_le_nonpos_of_covers combines strict cost with nonempty marked coverage.
50. le_mul_card_of_greedy_cover composes selection, provenance, coverage, and weak per-mark estimates. It retains \(H+m\ne0\).
51. lt_mul_card_of_greedy_cover is the strict end-to-end theorem. Nonempty marks imply a positive enlarged horizon.

Items 52–55: project wrappers

52. IsIntegrableSubadditiveProcessCandidate.le_orderedIntervalPackingSum exposes the raw packing sum on a candidate receiver.
53. IsIntegrableSubadditiveProcessCandidate.le_mul_coveredLength_of_orderedIntervalPacking exposes the weak covered-length form.
54. IsIntegrableSubadditiveProcessCandidate.centeredProcess_le_orderedIntervalPackingSum specializes to the orbit-majorant-centered process.
55. DiscreteMatrixCocycle.centeredLogPlusNormObservable_le_orderedIntervalPackingSum specializes directly to the centered cocycle observable.

Items 56–67: private boundary witnesses

56. positiveAtZeroProcess equals one at time zero and a negative linear value later.
57. positiveAtZeroProcess_add_le proves its shifted subadditivity.
58. positiveAtZeroProcess_nonpos proves only positive-horizon nonpositivity.
59. positiveAtZeroCandidate packages the witness over the zero measure.
60. emptyPositivePacking is an empty packing at positive horizon.
61. fullTerminalPacking selects one interval ending exactly at its horizon.
62. abuttingPacking selects two adjacent intervals with zero intermediate gap.
63. packingWithOuterGaps retains both an initial and terminal gap.
64. unitAbuttingPacking selects three singleton intervals that abut.
65. packingWithIntermediateGap selects two singleton intervals separated by a positive internal gap.
66. longChoice assigns a longer interval at start zero and unit length elsewhere.
67. longCoverPacking covers two marked starts with one selected interval, showing that marked cardinality can be strictly smaller than covered length.

Boundary cases are part of the theorem

Empty marked set

The selector returns an empty packing and both Covers and SelectedFrom hold vacuously. The weak greedy theorem is useful at positive enlarged horizon and says \(X_{H+m}\le0\). The strict theorem is not available because marked.Nonempty is false.

Empty packing at positive horizon

The raw inequality reduces to positive-horizon nonpositivity: \(X_N\le0=\operatorname{cost}(P)\). This is valid and useful.

Empty packing at horizon zero

The private witness has \(X_0=1\). The empty packing cost is zero. Therefore

This countermodel refutes the version of the raw theorem with its horizon premise deleted.

Singleton intervals

unitAbuttingPacking contains \([0,1)\), \([1,2)\), and \([2,3)\). Each interval has one natural position. This is the direct regression test for the strict-endpoint inconsistency in the motivating inclusive display.

Abutting intervals

abuttingPacking contains \([0,2)\) and \([2,5)\). Their endpoint and start are equal, but their intersection is empty. Requiring a positive gap would reject a legal packing and break the leftmost selector when the next uncovered mark lies exactly at the prior endpoint.

Endpoint at the horizon

fullTerminalPacking contains \([0,3)\) in horizon three. Generic packing containment permits endpoint equality. The selector’s stronger endpoint theorem is strict only because its ambient horizon includes the extra \(m\) slack.

Zero gaps and outer gaps

An initial gap of zero must not create an \(X_0\) summand. A positive outer gap may be split and discarded by nonpositivity. A terminal gap of zero is handled without a time-zero sign premise.

Zero length bound

If \(m=0\), a nonempty marked set cannot satisfy \(0\lt\ell(j)\le m\). The empty marked set still produces a packing. The weak process theorem then needs \(H\ne0\), exactly as its explicit enlarged-horizon premise says.

Empty matrix dimension

The cocycle smoke test instantiates the final wrapper with index type Empty. No positive matrix dimension has leaked into this finite algebra.

How Lean executes the finite proof

Let the type eliminate geometric side conditions

Induction on the packing immediately exposes a prefix gap, positive selected length, and recursively valid tail. There is no separate proof record to unpack at every step.

Carry absolute offsets explicitly

Relative gaps are convenient constructors. Process costs and marked-start hypotheses use absolute orbit positions. The From definitions and theorems carry an offset until a zero-offset wrapper closes the public API.

Use strong induction on remaining old horizon

The selector does not decrease by exactly one. After selecting a length- \(\ell\) interval, it recurses on the tail beginning at \(j+\ell\). Strong induction states exactly the needed decreasing relation.

Use the finite minimum, then filter

Finset.min’ chooses the leftmost mark. Filtering by \(j+\ell\le k\) retains exactly the starts that are not covered by the current half-open interval. SelectedFromFrom.mono widens the recursive certificate from this filtered set back to the original marked set.

Normalize natural iterates at the cost bridge

The recursive packing has already shifted the sample. The per-mark hypothesis is written at an absolute exponent. Function.iterate_add_apply and commutativity of natural addition identify the two forms (function iteration).

Let omega own endpoint arithmetic

The proof obligations are linear natural-number inequalities and equalities: tail horizons, endpoint containment, strict decrease, and reconstruction of \(H+m\). The omega tactic handles those Presburger facts after the semantic cases have been chosen.

Let linarith delete signed gaps

Subadditivity supplies a sum containing a gap term. Positive-horizon nonpositivity bounds that term by zero. linarith performs only the final ordered-ring combination.

Cast cardinalities before reversing multiplication

Coverage begins in natural numbers. The process bound lives in real numbers. The proof casts \(|B|\le L\) to the reals, then applies multiplication by a nonpositive coefficient on the left. This is the only reason the marked-card theorems require \(c\le0\).

Common wrong turns

Using closed intervals in Lean

Closed intervals double-count a shared endpoint. The selector and cardinality proof are designed around half-open intervals.

Requiring a positive gap

Pairwise disjoint half-open intervals may abut. A strict gap rejects valid output and contradicts the leftmost filter.

Requiring length at least two

Positive natural length includes one. The strict endpoint chain in the source display is not a valid reason to remove singleton intervals.

Treating Covers as provenance

Coverage alone does not say where a selected interval began or which length function it obeys. Per-mark cost transport requires SelectedFrom.

Treating SelectedFrom as coverage

A packing can select legitimate marked intervals and still omit other marks. The greedy theorem returns both predicates.

Demanding the original horizon \(H\)

A legal interval beginning at \(H-1\) may extend beyond \(H\). The uniform bound on length gives the enlarged horizon \(H+m\).

Dropping the horizon premise from the weak greedy theorem

When \(H=m=0\) and marks are empty, the selector exists but positive-horizon nonpositivity says nothing about \(X_0\).

Claiming a strict theorem for empty marks

Strict per-mark hypotheses are vacuous on the empty set. The desired strict conclusion can reduce to \(0\lt0\).

Forgetting that \(c\le0\)

Coverage gives a lower bound on selected length. It becomes the desired upper bound only after multiplication reverses direction.

Reading packing cost as an orbit sum of \(X_1\)

Each summand is a variable-horizon process value at one selected start. It is not a Birkhoff sum unless additional equality is proved.

Discarding zero gaps with nonpositivity

The sign premise applies only at nonzero horizons. The proof branches around zero gaps instead.

Calling the selector optimal or canonical

The theorem proves existence of a leftmost construction with coverage and provenance. It proves no minimum number of intervals, maximum covered length, or uniqueness.

Calling coverage a density estimate

The result is a finite cardinality inequality for a supplied finite marked set. No limiting density exists in the statement.

Calling this Kingman’s theorem

The module proves a finite ingredient used in one proof strategy. It contains no limit, almost-everywhere quantifier, expectation, or invariant function.

What interval packing still does not prove

RMT-21 proves none of the following:

1. a lower or upper asymptotic density of marked starts;
2. a maximal inequality;
3. a finite or pointwise Birkhoff ergodic theorem;
4. a mean ergodic theorem;
5. Kingman’s subadditive ergodic theorem;
6. almost-sure or almost-everywhere convergence;
7. convergence in probability or in \(L^1\);
8. interchange of a limit and an integral;
9. an invariant-integral identity;
10. ergodicity of \(T\) or any power of \(T\);
11. a probability-space normalization;
12. a measure estimate for a marked event;
13. independence or stationarity of selected intervals;
14. uniqueness, maximality, or optimality of the selected packing;
15. a Vitali covering theorem or a Riesz covering lemma;
16. a signed logarithmic cocycle observable;
17. a top or lower Lyapunov exponent;
18. a singular-value growth theorem;
19. an exterior-power cocycle;
20. an invariant Oseledets filtration or splitting.

The final two wrappers remain finite statements about the project’s log-positive expansion envelope. They do not recover contraction clipped by that observable.

Exercises with solutions

Exercise 1: decode one cons node

Let the offset be five, the gap two, and the length three. What interval is emitted?

Solution. The start is \(5+2=7\) and the endpoint is \(7+3=10\), so the half-open interval is \([7,10)\).

Exercise 2: identify the terminal gap

What constructor records a terminal gap of four after the last selected interval?

Solution. The recursive rest is .empty 4. Empty retains a horizon even though it selects nothing.

Exercise 3: permit abutment

Are \([2,5)\) and \([5,8)\) disjoint?

Solution. Yes. The first excludes five and the second includes it. Their endpoint order is \(5\le5\).

Exercise 4: permit a singleton

How many natural positions lie in \([4,5)\)?

Solution. Exactly one, namely four. Its positive length is one.

Exercise 5: separate the decoders

What does the interval list remember that the covered finite set forgets?

Solution. It remembers ordered interval boundaries. The finite union only remembers which positions are covered.

Exercise 6: recover interval count

Why does length_intervals need no disjointness theorem?

Solution. It counts list nodes, not union positions. Each cons emits one pair and recurses.

Exercise 7: recover covered cardinality

Why does card_coveredFinset need disjointness?

Solution. Cardinality of a union is additive only when overlaps are absent.

Exercise 8: distinguish coverage

Can one long interval that starts outside \(B\) satisfy Covers B?

Solution. Yes, if it contains every mark. Coverage alone is not provenance.

Exercise 9: distinguish provenance

Can a SelectedFrom packing omit a marked start?

Solution. Yes. The predicate constrains selected intervals but does not require every eligible mark to be covered.

Exercise 10: combine the predicates

What two facts does the greedy selector return?

Solution. P.Covers marked and P.SelectedFrom marked length.

Exercise 11: find the leftmost mark

If \(B=\{2,3,7\}\) and \(\ell(2)=3\), which marks are removed after selecting at two?

Solution. The interval is \([2,5)\), so starts two and three are covered. Seven remains.

Exercise 12: see abutment in the filter

If the first interval is \([2,5)\), does a mark at five survive?

Solution. Yes. The filter retains starts at least five. A subsequent interval may abut the first.

Exercise 13: prove induction decreases

Why is the recursive old-horizon tail shorter after selecting a positive interval?

Solution. The new origin lies at \(j+\ell(j)\), strictly to the right of the selected start because \(\ell(j)\gt0\).

Exercise 14: explain the crossing branch

Why can recursion stop when \(j+\ell(j)\) passes the old horizon end?

Solution. Every marked start is still below the old end and at least the leftmost \(j\), so it lies inside the selected interval.

Exercise 15: justify the enlarged endpoint

From \(j\lt H\) and \(\ell(j)\le m\), show \(j+\ell(j)\lt H+m\).

Solution. Natural arithmetic gives \(j+1\le H\), hence \(j+\ell(j)\lt H+m\) using positive-length and bound arithmetic. This is the fact discharged by omega.

Exercise 16: compare endpoint theorems

Why does generic intervals_inside permit endpoint \(N\), while the selector endpoint theorem gives a strict bound below \(H+m\)?

Solution. A generic packing may fill its horizon exactly. The selector’s target horizon includes uniform extra slack \(m\) beyond the start horizon.

Exercise 17: count covered marks

If \(B\subseteq P.coveredFinset\), why is \(|B|\le P.coveredLength\)?

Solution. Finite-set inclusion gives \(|B|\le|P.coveredFinset|\), and exact cardinality identifies the latter with covered length.

Exercise 18: derive nonempty packing

Why does a packing covering nonempty \(B\) have nonzero interval count?

Solution. An empty packing has empty covered finite set and cannot contain a witness from \(B\).

Exercise 19: read one cost term

For interval \([j,j+\ell)\), which process value enters the cost?

Solution. \(X_\ell(T^j\omega)\).

Exercise 20: reject a pointwise interpretation

Is that term equal to \(\sum_{r\lt\ell}X_1(T^{j+r}\omega)\)?

Solution. Not in general. Subadditivity supplies only an inequality unless the process is additive.

Exercise 21: align recursive offsets

Why does the cost bridge use function-iterate addition?

Solution. The tail sample has already been shifted by earlier gaps and intervals. The theorem identifies that nested shift with the absolute selected start named by SelectedFromFrom.

Exercise 22: sum weak bounds on empty packing

What does cost_le_mul_coveredLength become?

Solution. \(0\le c\cdot0\), hence \(0\le0\).

Exercise 23: try to sum strict bounds on empty packing

What false conclusion would result?

Solution. \(0\lt0\). This is why nonzero interval count is explicit.

Exercise 24: discard a positive gap

If subadditivity yields \(X_N\le A+X_g\) with \(g\ne0\), what sign fact removes the gap?

Solution. \(X_g\le0\), so \(A+X_g\le A\).

Exercise 25: handle a zero gap

Why not use the same sign fact when \(g=0\)?

Solution. The premise controls only nonzero horizons. Lean instead avoids splitting off that gap.

Exercise 26: test the time-zero witness

What are the process value and empty packing cost at horizon zero?

Solution. The private witness has process value one and packing cost zero, so the desired inequality fails.

Exercise 27: retain the positive empty case

What happens for an empty packing at horizon four under the same witness?

Solution. \(X_4=-4\le0\), so the raw inequality is valid.

Exercise 28: reverse the count inequality

Suppose \(|B|\le L\) and \(c=-2\). Which way does multiplication go?

Solution. \(-2L\le-2|B|\).

Exercise 29: locate the coefficient premise

Which theorem family needs \(c\le0\): covered-length or marked-card?

Solution. Marked-card. Covered-length uses no comparison between \(L\) and another cardinality.

Exercise 30: audit the weak greedy boundary

Why does le_mul_card_of_greedy_cover retain \(H+m\ne0\)?

Solution. Empty marks can produce an empty horizon-zero packing, and no positive-time sign premise controls \(X_0\).

Exercise 31: audit the strict greedy boundary

Why can lt_mul_card_of_greedy_cover omit the horizon premise?

Solution. Nonempty marks plus coverage force at least one selected positive-length interval, hence a positive horizon.

Exercise 32: construct the empty strict counterexample

Take a process identically zero at positive times and no marks. Why are all strict local hypotheses true?

Solution. They are universally quantified over the empty marked set, so there is no counterexample. The global strict conclusion is still false.

Exercise 33: audit wrapper integrability

Does the candidate-facing packing-sum proof use the candidate’s integrability field?

Solution. No. The receiver carries it, but the proof projects only add_le and takes nonpositivity separately.

Exercise 34: audit preservation

Does the centered-process packing theorem require a new preservation witness?

Solution. No. It is pointwise finite algebra once the centered subadditivity and sign theorems are available.

Exercise 35: audit matrix dimension

Why is no nonempty index premise needed?

Solution. The centered log-positive observable’s finite algebra is already valid for the empty matrix index, and the packing layer is scalar.

Exercise 36: name the next missing bridge

What must be proved before this finite marked-card inequality becomes a Kingman theorem?

Solution. One still needs exact measurable marked events, finite-measure and stationarity interfaces, a pointwise Birkhoff theorem or another density mechanism, limit and integral control, and the argument identifying the liminf. RMT-21 supplies none of those automatically.

Reproducibility and audit ledger

From the repository root:

source "$HOME/.elan/env"
cd formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomCocycles/SubadditiveIntervalPacking.lean
lake build NonlinearDynamics.Random.RandomCocycles.SubadditiveIntervalPacking
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Random/RandomCocycles.lean
lake env lean -DwarningAsError=true NonlinearDynamics/Random.lean
lake env lean -DwarningAsError=true NonlinearDynamics.lean
cd ..
python3 scripts/check_teaching_source_hygiene.py
make site-check

The public-surface audit should include:

import NonlinearDynamics

open NonlinearDynamics.Random.RandomCocycles

#check OrderedNatIntervalPacking
#check OrderedNatIntervalPacking.intervals_pairwiseDisjoint_Ico
#check OrderedNatIntervalPacking.exists_orderedPacking_covering
#check OrderedNatIntervalPacking.SelectedFrom.everyIntervalCostLE
#check OrderedNatIntervalPacking.SelectedFrom.everyIntervalCostLT
#check OrderedNatIntervalPacking.le_cost_of_add_le_nonpos
#check OrderedNatIntervalPacking.le_mul_card_of_greedy_cover
#check OrderedNatIntervalPacking.lt_mul_card_of_greedy_cover
#check IsIntegrableSubadditiveProcessCandidate.centeredProcess_le_orderedIntervalPackingSum
#check DiscreteMatrixCocycle.centeredLogPlusNormObservable_le_orderedIntervalPackingSum

The integrated repository module is 1,131 lines with SHA-256 732187ce77b5efa14df3a992f194d5dce4dfc8d9f5fa6dbaf658c5ed41ef4f4d. That hash records the exact source audited for this chapter; the repository module is the present authority. Its warning-fatal leaf check and the aggregator/root builds pass. The axiom audit reports only Lean and Mathlib’s standard logical dependencies, with no sorry, admit, unsafe declaration, or custom axiom.

This article publishes as an open working note with draft: false and retains pro_reviewed: false. Automated checks do not replace human mathematical, source, accessibility, and editorial review.

The next ridge

RMT-20 supplied the finite phase-averaged upper mechanism. RMT-21 now supplies the complementary finite interval-packing mechanism: choose bounded favorable intervals, retain an ordered disjoint cover of all marked starts, and turn their local estimates into a marked-cardinality process bound.

The next dependency is not another repackaging theorem. It is the analytic infrastructure that makes the marked set large along typical orbits and connects finite inequalities to limits. That work must state exact measurable events, probability or finite-measure assumptions, measure preservation, integrability, stationarity, maximal or Birkhoff machinery, almost-everywhere quantifiers, and limit-identification steps. The current module does not allow any one of those assumptions to be inferred from notation.

The immediate successor, Convergence Without Existence: Birkhoff Events and Ergodic Rigidity in Lean, supplies the first event-level bridge. It proves that convergence of one-step Birkhoff averages is an exactly invariant measurable or null-measurable event, then derives conditional null-or-conull and probability-zero-or-one laws. It supplies no convergence existence, marked-set density or frequency, maximal inequality, pointwise Birkhoff theorem, or Kingman theorem. Those analytic inputs remain the next ridge between this finite packing and asymptotic subadditive dynamics.

For matrix cocycles, the observable remains log-positive and therefore clips contraction. Signed Lyapunov exponents, singular-value rates, exterior powers, and Oseledets splittings remain separate future layers.

References

The links below were checked on 2026-07-21. The pinned Mathlib 4.32.0 checkout at commit 81a5d257c8e410db227a6665ed08f64fea08e997 is the exact authority for upstream theorem names used by the frozen proof.

Mathlib contributors. Finite interval definitions, with the pinned definitions and membership theorem. These declarations define Finset.Ico and identify its members with the half-open endpoint inequalities used by the packing decoder.

Mathlib contributors. Natural-number finite intervals, with the pinned range and cardinality laws. These laws identify Finset.range H with the half-open interval from zero and compute the size of a natural Ico.

Mathlib contributors. Finite-set cardinality, with the pinned disjoint-union laws. RMT-21 uses these declarations to add interval and recursive-tail cardinalities only after proving disjointness.

Lean contributors. Lean 4 list pairwise source, Lean 4.32.0. The recursive pairwise_cons characterization matches the source-order proof of endpoint separation.

Mathlib contributors. Function iteration, with the pinned iterate laws. The addition law aligns 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 finite packed-process inequality as equation (6). Page 3 describes choosing the leftmost blue interval and deleting candidates whose starts it covers. The notes use inclusive integer intervals. Their displayed strict start-to-end chain excludes length one although the next paragraph allows \(1\le k\le m\). RMT-21 translates the argument to half-open intervals, admits singleton and abutting selections, and separately repairs the empty-set strict boundary. These notes motivate the finite construction; they are not an upstream Lean theorem or the primary source for Kingman’s asymptotic theorem.

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 conceptually algorithmic decomposition of a finite integer interval into selected bounded intervals and singleton classes. It is related proof lineage, but it neither states nor replaces RMT-21’s exact Covers and SelectedFrom 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. RMT-21 proves only finite combinatorics and a finite process inequality.

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