Finite-Horizon Log-Positive Cocycle Integrability

Begin with four states and one exact ledger

Take four base states

and let the base map move one place clockwise:

Put mass \(1/4\) at each state. This is a probability measure because the four masses add to one. The map \(T\) preserves it because \(T\) merely permutes four equally weighted points. Every subset is an event and every real-valued function is measurable on this finite discrete space.

Now use one-dimensional matrices. At the four states, choose the positive generator values

Regarded as \(1\times1\) complex matrices, their operator norms are just their absolute values. Each is a power of two:

We will measure logarithms in units of \(\log2\). This removes numerical approximations without changing any inequality:

The positive logarithm keeps only the positive part,

Therefore the one-step observable, again in units of \(\log2\), is

The contractions \(1/2\) and \(1/4\) contribute zero. The expansions \(2\) and \(4\) contribute one and two.

Because the measure is uniform, the integral is the ordinary average:

This number is finite. In this example the explicit one-step integrability hypothesis is true.

Compute the two-step cocycle before bounding it

For a generator-presented one-sided cocycle,

Multiplying powers of two adds their signed exponents. Taking positive log afterward keeps the positive part of that total. The four exact calculations are:

So

The theorem does not compute \(P_2\) from an average. It first constructs the pointwise orbit budget

Its four values in \(\log2\)-units are

Thus

At every state,

The inequality is strict at all four states in this example. Positive parts do not add exactly: a later expansion can cancel an earlier contraction in the signed product, while \(S_2\) has already clipped the contraction to zero.

At horizon four, every orbit sees all four signed exponents. Their sum is zero, so \(P_4=0\) everywhere. But every orbit sum is \(S_4=(0+1+0+2)\log2=3\log2\). A useful majorant need not be sharp.

What the measure-theory words mean here

The finite ledger is already a complete small model of the vocabulary.

• A measurable space specifies which subsets count as events. Here every subset of \(\Omega\) is an event.
• A measure assigns nonnegative mass to events. Here the mass of a set is the number of its points divided by four.
• A probability measure has total mass one. That is why the integral above can also be called an expectation.
• A measurable function respects the selected events. Every function out of this finite discrete space does.
• A real function is integrable when its absolute size has finite integral. A finite list of finite values with finite weights is automatically integrable.
• A null set has mass zero. Because every point here has positive mass, the only null set is the empty set.
• A claim holding almost everywhere may fail on a null set. In this finite example that means it holds everywhere.

For a function \(f:\Omega\to\mathbb R\), the integral is the weighted sum

For integrability one inserts absolute values:

The target observable \(P_k\) is nonnegative, so \(|P_k|=P_k\). This small identity is exactly the final step used by the Lean proof.

A measure need not be a probability measure

The target module accepts an arbitrary raw measure \(\mu\). To see the difference, give each of the same four states mass \(2\). The total mass is \(8\), not \(1\). The one-step integral in \(\log2\)-units becomes

It is still finite, so \(P_1\) is integrable. But \(6\log2\) is not an expectation under that unnormalized measure. “Integral” is the correct general word; “expectation” is reserved for a probability measure.

Measure preservation also has a precise job. It says that moving all mass through \(T\) does not change the measure. Consequently, if \(P_1\) is already integrable, then each shifted function

is integrable. Preservation transports an existing fact. It does not turn an arbitrary measurable function into an integrable one.

The explicit hypothesis can genuinely fail

Finite spaces hide heavy tails. Move to the countable space \(\Omega=\mathbb N\), keep the identity base \(T(n)=n\), and put geometric probability mass

at atom \(n\). The masses sum to one. The identity map preserves them, and every function is measurable for the discrete measurable structure.

Choose a one-dimensional expanding generator with norm

Then

Every atom contributes exactly the same amount to the integral:

Therefore the first \(N\) atoms already contribute \(N/2\), and

This is not merely a large finite sample. The algebra proves every summand is \(1/2\), so the partial integrals are unbounded. Probability normalization, ordinary measurability, and measure preservation are all present, yet HasIntegrableGeneratorLogPlus is false.

The opposite sign is a wrong-level near miss

Replace the generator norm by

Now every norm is at most one, so \(P_1(n)=0\). The RMT-15 hypothesis holds because the positive-log observable is identically zero. But the signed logarithm has magnitude \(2^n\), and its weighted absolute integral again contains \(1/2\) at every atom. The inverse norm has the same expanding tail.

This does not contradict RMT-15. Positive log deliberately erased the contraction before integrability was discussed. A later project module checks this geometric contraction model as a counterexample separating forward positive-log integrability from inverse-tail and signed-real-log integrability. The target module makes neither stronger claim.

Choose a route up

Learning objectives

By the summit, you should be able to compute the four-state ledger without a calculator; explain why a finite weighted list is integrable; distinguish a raw integral from an expectation; produce the geometric heavy-tail counterexample; explain what positive log erases; read seven Lean bridges token by token; run the bounded Std worksheet; derive the orbit-sum majorant; reconstruct the pullback and domination proof; audit all sixteen public declarations; and state which probability, tail, uniform-time, ergodic, and Lyapunov conclusions remain outside the file.

In Lean: seven bridges from the ledger to the theorem

All seven bridges below belong to NonlinearDynamics.Random.RandomCocycles.LogPlusIntegrability. The human sentence, paper formula, and Lean expression say the same thing at three levels.

Bridge one: define the real nonnegative envelope

C.logPlusNormObservable k ω : ℝ

The companion theorem C.logPlusNormObservable_nonneg k ω supplies \(0\le P_k(\omega)\).

Bridge two: split a finite history

C.logPlusNormObservable_add_le m k ω

Bridge three: add the shifted one-step costs

C.orbitLogPlusSum k ω

Bridge four: append the newest term

C.orbitLogPlusSum_succ k

Bridge five: the orbit sum dominates pointwise

C.logPlusNormObservable_le_orbitLogPlusSum k ω

Bridge six: name the missing analytic assumption

C.HasIntegrableGeneratorLogPlus

Bridge seven: propagate to every fixed horizon

hC.integrable_logPlusNormObservable k

Check the exact project interface

import NonlinearDynamics.Random.RandomCocycles.LogPlusIntegrability

open NonlinearDynamics.Random.RandomCocycles

#print DiscreteMatrixCocycle.logPlusNormObservable
#check DiscreteMatrixCocycle.logPlusNormObservable_nonneg
#check DiscreteMatrixCocycle.logPlusNormObservable_zero
#check DiscreteMatrixCocycle.logPlusNormObservable_one
#check DiscreteMatrixCocycle.measurable_logPlusNormObservable
#check DiscreteMatrixCocycle.logPlusNormObservable_add_le
#check DiscreteMatrixCocycle.logPlusNormObservable_eq_zero_of_isEmpty
#print DiscreteMatrixCocycle.orbitLogPlusSum
#check DiscreteMatrixCocycle.orbitLogPlusSum_zero
#check DiscreteMatrixCocycle.orbitLogPlusSum_succ
#check DiscreteMatrixCocycle.measurable_orbitLogPlusSum
#check DiscreteMatrixCocycle.logPlusNormObservable_le_orbitLogPlusSum
#print DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_at_base_iterate
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_orbitLogPlusSum
#check DiscreteMatrixCocycle.HasIntegrableGeneratorLogPlus.integrable_logPlusNormObservable

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

Type the ledgers yourself with Lean and Std

The project theorem uses Mathlib matrices, measures, iterates, and Bochner integrability. The arithmetic that motivates it is much smaller. The following worksheet imports only Std, represents logarithms by their exact coefficients, and checks the finite and geometric ledgers without compiling Mathlib.

Create a scratch directory outside formalization/. Save the exact block below as FiniteHorizonLogPlusIntegrabilityTutorial.lean:

import Std

namespace FiniteHorizonLogPlusIntegrabilityTutorial

/-
The four generator norms are powers of two:

  state       0     1     2     3
  norm       1/2    2    1/4    4
  exponent    -1    1     -2    2

All logarithms below are measured in units of log 2.  This keeps every
calculation exact while preserving the positive-log arithmetic.
-/

def exponentAt (state : Nat) : Int :=
  match state % 4 with
  | 0 => -1
  | 1 => 1
  | 2 => -2
  | _ => 2

def base (state : Nat) : Nat :=
  (state + 1) % 4

def positivePart (z : Int) : Nat :=
  z.toNat

def oneStepPositive (state : Nat) : Nat :=
  positivePart (exponentAt state)

def signedExponent (state horizon : Nat) : Int :=
  (List.range horizon).foldl
    (fun total j => total + exponentAt (state + j)) 0

def horizonPositive (state horizon : Nat) : Nat :=
  positivePart (signedExponent state horizon)

def orbitBudget (state horizon : Nat) : Nat :=
  ((List.range horizon).map
    (fun j => oneStepPositive (state + j))).sum

structure HorizonLedger where
  start : Nat
  signedExponent : Int
  horizonPositive : Nat
  orbitBudget : Nat
  deriving Repr, DecidableEq

def ledgerAt (horizon start : Nat) : HorizonLedger :=
  { start := start
    signedExponent := signedExponent start horizon
    horizonPositive := horizonPositive start horizon
    orbitBudget := orbitBudget start horizon }

def horizonTwoLedger : List HorizonLedger :=
  (List.range 4).map (ledgerAt 2)

def horizonFourLedger : List HorizonLedger :=
  (List.range 4).map (ledgerAt 4)

def fairMean (values : List Nat) : Rat :=
  (values.sum : Rat) / values.length

def oneStepMean : Rat :=
  fairMean ((List.range 4).map oneStepPositive)

def horizonTwoMean : Rat :=
  fairMean ((List.range 4).map (fun state => horizonPositive state 2))

def horizonTwoBudgetMean : Rat :=
  fairMean ((List.range 4).map (fun state => orbitBudget state 2))

/-
The same four atoms with raw mass 2 each have total mass 8.  Their integral
is still finite, but it is not an expectation until the measure is normalized.
-/

def rawMassTwoOneStepIntegral : Nat :=
  2 * ((List.range 4).map oneStepPositive).sum

/-
Near miss on the countable probability space Nat:

  mass at n                 = 1 / 2^(n+1)
  generator norm           = exp (-(2^n))
  positive log             = 0
  missing negative magnitude = 2^n

Each missing-tail contribution is exactly 1/2, so its partial sums grow
without bound even though the positive-log integral is zero.
-/

def tailWeight (n : Nat) : Rat :=
  1 / (2 ^ (n + 1) : Nat)

def missingNegativeMagnitude (n : Nat) : Nat :=
  2 ^ n

def missingTailContribution (n : Nat) : Rat :=
  tailWeight n * missingNegativeMagnitude n

def missingTailPartialSum (count : Nat) : Rat :=
  ((List.range count).map missingTailContribution).sum

def forwardPositivePartialSum (count : Nat) : Rat :=
  ((List.range count).map (fun _ => (0 : Rat))).sum

/-
Flipping the sign in the exponent gives the expanding generator
exp (2^n).  Then the very same contributions belong to the positive log,
so the RMT-15 one-step hypothesis itself fails.
-/

def expandingPositiveContribution (n : Nat) : Rat :=
  tailWeight n * missingNegativeMagnitude n

def expandingPositivePartialSum (count : Nat) : Rat :=
  ((List.range count).map expandingPositiveContribution).sum

structure TailLedger where
  atom : Nat
  weight : Rat
  positiveLog : Nat
  missingNegativeMagnitude : Nat
  weightedMissingTail : Rat
  deriving Repr, DecidableEq

def tailLedger (count : Nat) : List TailLedger :=
  (List.range count).map fun n =>
    { atom := n
      weight := tailWeight n
      positiveLog := 0
      missingNegativeMagnitude := missingNegativeMagnitude n
      weightedMissingTail := missingTailContribution n }

#eval (List.range 4).map exponentAt
#eval (List.range 4).map oneStepPositive
#eval horizonTwoLedger
#eval horizonFourLedger
#eval [oneStepMean, horizonTwoMean, horizonTwoBudgetMean]
#eval rawMassTwoOneStepIntegral
#eval (List.range 6).map missingTailContribution
#eval (List.range 6).map missingTailPartialSum
#eval (List.range 6).map forwardPositivePartialSum
#eval (List.range 6).map expandingPositivePartialSum

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

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

example : horizonTwoLedger =
    [ { start := 0, signedExponent := 0,
        horizonPositive := 0, orbitBudget := 1 },
      { start := 1, signedExponent := -1,
        horizonPositive := 0, orbitBudget := 1 },
      { start := 2, signedExponent := 0,
        horizonPositive := 0, orbitBudget := 2 },
      { start := 3, signedExponent := 1,
        horizonPositive := 1, orbitBudget := 2 } ] := by
  native_decide

example : horizonTwoLedger.all
    (fun row => decide (row.horizonPositive ≤ row.orbitBudget)) := by
  native_decide

example : horizonFourLedger.map
    (fun row => (row.horizonPositive, row.orbitBudget)) =
      [(0, 3), (0, 3), (0, 3), (0, 3)] := by
  native_decide

example : oneStepMean = 3 / 4 := by native_decide
example : horizonTwoMean = 1 / 4 := by native_decide
example : horizonTwoBudgetMean = 3 / 2 := by native_decide
example : rawMassTwoOneStepIntegral = 6 := by native_decide

example : (List.range 6).map missingTailContribution =
    [1 / 2, 1 / 2, 1 / 2, 1 / 2, 1 / 2, 1 / 2] := by
  native_decide

example : missingTailPartialSum 8 = 4 := by native_decide
example : forwardPositivePartialSum 8 = 0 := by native_decide
example : expandingPositivePartialSum 8 = 4 := by native_decide

end FiniteHorizonLogPlusIntegrabilityTutorial

Open a terminal in that scratch directory and type:

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

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

[-1, 1, -2, 2]
[0, 1, 0, 2]
[{ start := 0, signedExponent := 0, horizonPositive := 0, orbitBudget := 1 },
 { start := 1, signedExponent := -1, horizonPositive := 0, orbitBudget := 1 },
 { start := 2, signedExponent := 0, horizonPositive := 0, orbitBudget := 2 },
 { start := 3, signedExponent := 1, horizonPositive := 1, orbitBudget := 2 }]
[{ start := 0, signedExponent := 0, horizonPositive := 0, orbitBudget := 3 },
 { start := 1, signedExponent := 0, horizonPositive := 0, orbitBudget := 3 },
 { start := 2, signedExponent := 0, horizonPositive := 0, orbitBudget := 3 },
 { start := 3, signedExponent := 0, horizonPositive := 0, orbitBudget := 3 }]
[(3 : Rat)/4, (1 : Rat)/4, (3 : Rat)/2]
6
[(1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2, (1 : Rat)/2]
[0, (1 : Rat)/2, 1, (3 : Rat)/2, 2, (5 : Rat)/2]
[0, 0, 0, 0, 0, 0]
[0, (1 : Rat)/2, 1, (3 : Rat)/2, 2, (5 : Rat)/2]

The first two lines are the signed exponents and their positive parts. The next two ledgers give horizons two and four. The three rational means are \(3/4\), \(1/4\), and \(3/2\); the raw mass-two integral is \(6\). The next line shows six identical geometric contributions of \(1/2\). The final three lines show their partial sums: the missing contraction tail grows as \(N/2\), the contraction’s forward positive log stays zero, and the expanding positive tail again grows as \(N/2\).

native_decide does not estimate these values. It evaluates exact integer and rational computations and produces a proof term checked by Lean’s kernel. The worksheet models logarithms by exact coefficients; it does not reimplement Mathlib’s analytic logarithm, matrix norm, measure, or Integrable predicate. Those authoritative interfaces remain the full project check above.

Why the finite-horizon propagation works

Return to the general setting. Fix:

• a base type \(\Omega\) with a measurable-space structure;
• a finite matrix index type \(\iota\) with decidable equality;
• an arbitrary measure \(\mu\) on \(\Omega\); and
• a bundled DiscreteMatrixCocycle μ.

The cocycle stores a measurable generator \(A\), a measurable measure-preserving base map \(T\), and the newest-factor-left finite product

The predecessor module defines

using the maximum absolute row-sum matrix norm and proves

Positive log keeps only expansion

The target defines

as an ordinary real number. For nonnegative norm inputs:

The first three cases collapse to one value. This is why \(P_k\) is an upper integrability envelope, not the predecessor’s zero-faithful extended log norm and not a signed growth rate.

Mathlib proves that Real.posLog is continuous, hence measurable. Composing it with the predecessor’s measurable norm observable gives measurable_logPlusNormObservable.

At time zero, the cocycle value is the identity. In nonempty matrix dimension its norm is one; in empty dimension its norm is zero. Positive log sends both to zero, so

without a Nonempty ι assumption. In empty dimension every matrix value has norm zero and every \(P_k\) is identically zero.

Finite-time subadditivity

Pass the norm split through the monotone positive logarithm:

The first inequality uses norm nonnegativity and positive-log monotonicity. The second is Mathlib’s product inequality Real.posLog_mul. It is an inequality rather than an equality because clipping can discard negative logarithms before addition.

Induct to the one-step orbit budget

Define

The empty sum is zero and

Now induct on \(k\). The base case is \(P_0=0=S_0\). For the successor, finite-time subadditivity at the split \(k+1\) gives

Apply the induction hypothesis \(P_k\le S_k\), commute the two real summands, and recognize \(S_{k+1}\). Therefore

for every state, not merely almost everywhere.

Transport, add, dominate

Assume

The bundled cocycle proves that every natural iterate \(T^j\) is measure-preserving. Mathlib’s pullback theorem transports the assumption to

There are only \(k\) such terms in \(S_k\). Finite sums of integrable functions are integrable, so \(S_k\) is integrable. No independence, identical-distribution assumption, infinite series, or convergence theorem is needed.

Finally, \(P_k\) is measurable, \(P_k\ge0\), and \(P_k\le S_k\). Hence

Mathlib’s dominated-integrability method Integrable.mono’ therefore proves \(P_k\) integrable.

The complete sixteen-declaration map

The file exposes exactly sixteen public declarations in source order.

The ambient assumptions are a measurable base type, a finite matrix index type with decidable equality, and an arbitrary measure. There is no global Nonempty ι, probability, finite-measure, sigma-finite, ergodic, invertible-base, or independence assumption.

The bundled cocycle receiver still carries its base-preservation and measurability fields even when an early pointwise theorem does not consume them. That packaging should not be mistaken for additional theorem-specific hypotheses.

Edge cases worth keeping visible

Horizon zero

The conclusion theorem retains the one-step hypothesis even at \(k=0\), because it is stated uniformly for every natural \(k\). But \(P_0=0\) is integrable without that hypothesis. A separate zero-only theorem could omit it; the current declaration instead presents one uniform interface.

Empty matrix dimension

When \(\iota\) is empty, every square matrix is the unique empty matrix and its selected norm is zero. The positive-log observable is identically zero at every horizon. This is why the target’s time-zero theorem needs no inhabited coordinate type even though the predecessor’s norm-one theorem does.

Zero measure

Under the zero measure, every suitably measurable finite real function is integrable because all integrals vanish. The theorem allows this degenerate case. It does not silently normalize the measure.

Pointwise versus almost everywhere

The cocycle inequality \(P_k\le S_k\) is pointwise. The final Mathlib integrability interface asks only for an almost-everywhere norm bound, so the proof converts the stronger statement into the weaker form automatically.

Finite horizons versus one uniform bound

For each fixed \(k\), the sum \(S_k\) has finitely many integrable terms. This does not exhibit one integrable random variable dominating \(P_k\) for all \(k\), and it does not justify exchanging a limit with an integral.

Exercises from foothill to summit

Foothill

1. Recompute the four one-step positive-log coefficients.
2. Multiply the four horizon-two scalar pairs and recover \(P_2/\log2=(0,0,0,1)\).
3. Compute \(S_2/\log2=(1,1,2,2)\).
4. Verify all four pointwise inequalities \(P_2\le S_2\).
5. Replace uniform masses by \(1/10,2/10,3/10,4/10\). Decide whether the same clockwise cycle preserves the new probability measure.
6. Give each state raw mass two and explain why the word “expectation” is no longer appropriate.

Ridge

7. Expand \(S_3(\omega)\) with all three base iterates visible.
8. Derive \(S_{k+1}=S_k+P_1\circ T^k\) from a finite range.
9. Prove \(P_k\le S_k\) by induction on paper.
10. In the expanding geometric model, prove the masses sum to one.
11. Prove every weighted positive-log contribution is \(1/2\).
12. Explain why an identity base is measure preserving but does not create integrability.
13. Change the sign of the geometric exponent and distinguish the forward positive tail from the missing signed tail.

Summit

14. Translate Integrable.mono’ into measurability, an integrable majorant, and an almost-everywhere norm bound.
15. Audit all sixteen declarations against their exact assumptions.
16. Explain why no independence hypothesis appears in the finite-sum proof.
17. State an additional hypothesis that would control the inverse-generator positive log.
18. State what probability and asymptotic assumptions would be needed before invoking a precise subadditive ergodic theorem.
19. Explain why an integrable \(P_k\) does not make the predecessor’s extended-real log norm integrable.
20. Design a derivative-cocycle interface for a nonlinear random dynamical system and list the chain-rule and measurability facts it would require.

Reproduce the chapter

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

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

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

Summit: what has and has not been proved

The checked result is finite and exact: one existing integrability fact for the expanding one-step envelope propagates through preserved pullbacks, finite addition, and pointwise domination to every fixed horizon.

Where to continue

Integrated Log-Positive Cocycle Growth and Its Deterministic Fekete Limit is the immediate successor. It integrates these finite-horizon envelopes and uses a deterministic Fekete argument. It still does not turn RMT-15 into a samplewise ergodic or Lyapunov theorem.

Finite-Time Norm and Extended-Log-Norm Observables for Matrix Cocycles is the immediate predecessor. It develops the maximum absolute row-sum norm and the zero-faithful extended log norm whose contraction and collapse data the present positive envelope discards.

Generator-Presented One-Sided Discrete Matrix Cocycles supplies the base orbit, measure-preserving natural iterates, and exact later-block-left product law.

The log-positive integrability envelope glossary entry is the compact companion for the clipping and majorization strategy.

References

Mathlib contributors. The positive part of the logarithm, Mathlib 4 documentation. This official source defines Real.posLog and records its nonnegativity, endpoint values, continuity, monotonicity on nonnegative inputs, and product inequality.

Mathlib contributors. Bochner integrability, Mathlib 4 documentation. The pinned local source supplies the exact MeasurePreserving.integrable_comp_of_integrable, integrable_finsetSum, and Integrable.mono’ interfaces used by the target.

Mathlib contributors. Measure-preserving maps, Mathlib 4 documentation. RMT-13 packages natural-iterate preservation for the cocycle base.

Harry Furstenberg and Harry Kesten. Products of Random Matrices, The Annals of Mathematical Statistics 31(2), 457–469, 1960. This primary source motivates logarithmic growth of random matrix products. RMT-15 proves none of its asymptotic conclusions.

J. F. C. Kingman. The ergodic theory of subadditive stochastic processes, Journal of the Royal Statistical Society: Series B 30(3), 499–510, 1968. The target supplies only a finite-time integrability layer, not the hypotheses or conclusion of the subadditive ergodic theorem.

V. I. Oseledets. A multiplicative ergodic theorem. Characteristic Ljapunov exponents of dynamical systems, Transactions of the Moscow Mathematical Society 19 (1968), 197–231. This is an asymptotic destination; the present module proves no exponent, spectrum, filtration, or splitting.

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