Finite-horizon equilibration of the fibre cells

Category: 7-SigmaLayer. BACKLOG #118(ii) — the one clause of R-019's convergence half that row calls "plausibly a brick".

#18 proved the monotone decrease and showed it is not the content of relaxation: it holds for the translation, which provably cannot decorrelate. #118 split what is left into three, and only (ii) was priced as a brick — the finite-horizon statement, conditional on HasCorrelationDecayUpTo rather than on asymptotic mixing. This is that statement, on the fibre.

• fibreCellInd — a cell's indicator as a bounded observable on Σ, with ★ integral_fibreCellInd identifying its space average as the Haar cell law's mass at that cell, which is what makes the conclusion a statement about the coarse-grained law;
• ★★★ integral_birkhoffAverage_fibreCellInd_sub_sq_le — at horizon T, the mean-square deviation of a cell's time-averaged occupation from its Haar value is at most (2/T)·Σ_{u<T} ε u;
• ★★★ integral_sum_birkhoffAverage_fibreCellInd_sub_sq_le — summed over all (m+1)² cells, which is the row's "rate in terms of the cell count m": the bound carries a factor (m+1)²;
• ★★★ tendsto_integral_birkhoffAverage_fibreCellInd_sub_sq — with a summable envelope the deviation tends to 0, which is the convergence #118 asks for, in the finite-horizon reading.

What this is and is not

⚠️ It is time-averaged, not instantaneous — and that is the real finding. The Cesàro estimate controls the Birkhoff average over [0, T), so what equilibrates here is a cell's time-averaged occupation. R-019 asks for the law at step n to approach Haar, which is a mixing statement, not an ergodic one. So the finite-horizon escape buys an ergodic conclusion and leaves the mixing one untouched: it is genuinely weaker than R-019, exactly as #118 recorded, and no amount of sharpening the envelope closes that gap.

⚠️ The hypothesis is assumed, not derived. Whether the fibre's cell indicators satisfy HasCorrelationDecayUpTo is #118(i), a genuine mathematical question: the corpus has decay for the single observable catObs (catStroke_hasCorrelationDecay, finitely supported), and extending it to indicators is a statement about the cat map's spectral gap on indicator functions, which nothing here supplies. Everything below travels with its hypothesis.

⚠️ The cell count costs (m+1)². The summed bound degrades quadratically in the fineness of the coarse-graining, so a finite-horizon statement at fixed horizon is not uniform in m. R-019's "rate set by the cell size" would need the envelope itself to improve with m, and that is not available.

⚠️ Not the klDiv form. R-019's second clause is about relative entropy. Since the Haar cell law is uniform on these cells, klDiv ≤ χ² would convert the bound above at the cost of one more factor (m+1)² — but it needs the time-averaged occupations packaged as a measure, measurably in the base point, which is a restatement rather than new mathematics and is #130.

⚠️ Not a Track B prediction. Nothing here exhibits a fibre out of equilibrium returning to it, and the translation comparison of #18 still applies: this theorem's hypothesis is what distinguishes the maps, not its conclusion.

References: FibreCoarseArrow.lean (#18, fibreCell, fibreStroke), CorrelationDecay.lean (HasCorrelationDecayUpTo, the Cesàro estimate), KahlerFlowFiniteHorizon.lean (the same hypothesis for kFlow, where Dirichlet obstructs it), MovingFibreWitness.lean (relaxation_requires_hyperbolic_fibre); specs/BACKLOG.md #118, #18, #130; specs/residues.tsv R-019.

A cell's indicator as an observable

noncomputable def CSD.SigmaLayer.fibreCellInd {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (p : LF4.KSigma N) : ℝ

The indicator of one fibre cell, as a bounded real observable on Σ.

Equations

• CSD.SigmaLayer.fibreCellInd m c p = (CSD.SigmaLayer.fibreCell m ⁻¹' {c}).indicator (fun (x : CSD.LF4.KSigma N) => 1) p

theorem CSD.SigmaLayer.measurableSet_fibreCell_preimage {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : MeasurableSet (fibreCell m ⁻¹' {c})

theorem CSD.SigmaLayer.measurable_fibreCellInd {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : Measurable (fibreCellInd m c)

theorem CSD.SigmaLayer.abs_fibreCellInd_le {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (p : LF4.KSigma N) : |fibreCellInd m c p| ≤ 1

theorem CSD.SigmaLayer.integral_fibreCellInd {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : ∫ (p : LF4.KSigma N), fibreCellInd m c p ∂LF4.kMuL p₀ = ((InformationTheory.coarseLaw (LF4.kMuL p₀) (fibreCell m)) {c}).toReal

★ The space average is the Haar cell law's mass at the cell — which is what makes the estimates below statements about the coarse-grained law rather than about an arbitrary observable.

The finite-horizon estimate on the fibre

theorem CSD.SigmaLayer.measurable_fibreStroke {N : ℕ} : Measurable fibreStroke

The stroke is measurable, which the Cesàro estimate needs.

theorem CSD.SigmaLayer.integral_iterate_fibreCellInd {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (t : ℕ) : ∫ (p : LF4.KSigma N), fibreCellInd m c (fibreStroke^[t] p) ∂LF4.kMuL p₀ = ∫ (p : LF4.KSigma N), fibreCellInd m c p ∂LF4.kMuL p₀

The space average is stationary along the stroke, because the stroke preserves kMuL.

theorem CSD.SigmaLayer.integral_birkhoffAverage_fibreCellInd_sub_sq_le {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) {ε : ℕ → ℝ} {T : ℕ} (hdec : MeasureTheory.HasCorrelationDecayUpTo (LF4.kMuL p₀) fibreStroke (fibreCellInd m c) ε T) (hT : 0 < T) : ∫ (p : LF4.KSigma N), (birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p - ((InformationTheory.coarseLaw (LF4.kMuL p₀) (fibreCell m)) {c}).toReal) ^ 2 ∂LF4.kMuL p₀ ≤ 2 * (↑T)⁻¹ * ∑ u ∈ Finset.range T, ε u

★★★ Finite-horizon equilibration of one cell. At horizon T, the mean-square deviation of the cell's time-averaged occupation from its Haar value is at most (2/T)·Σ_{u<T} ε u.

The hypothesis is finite-horizon decay for that cell's indicator, which is #118(i) and is assumed here.

theorem CSD.SigmaLayer.integral_sum_birkhoffAverage_fibreCellInd_sub_sq_le {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ε : ℕ → ℝ} {T : ℕ} (hdec : ∀ (c : Fin (m + 1) × Fin (m + 1)), MeasureTheory.HasCorrelationDecayUpTo (LF4.kMuL p₀) fibreStroke (fibreCellInd m c) ε T) (hT : 0 < T) : ∑ c : Fin (m + 1) × Fin (m + 1), ∫ (p : LF4.KSigma N), (birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p - ((InformationTheory.coarseLaw (LF4.kMuL p₀) (fibreCell m)) {c}).toReal) ^ 2 ∂LF4.kMuL p₀ ≤ (↑m + 1) ^ 2 * (2 * (↑T)⁻¹ * ∑ u ∈ Finset.range T, ε u)

★★★ The rate in the cell count. Summed over all (m+1)² cells under a common envelope the bound carries a factor (m+1)²: a finite-horizon statement at fixed horizon is not uniform in the fineness of the coarse-graining.

The convergence, under a summable envelope

theorem CSD.SigmaLayer.tendsto_integral_birkhoffAverage_fibreCellInd_sub_sq {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) {ε : ℕ → ℝ} (hdec : MeasureTheory.HasCorrelationDecay (LF4.kMuL p₀) fibreStroke (fibreCellInd m c) ε) (hsum : Summable ε) : Filter.Tendsto (fun (T : ℕ) => ∫ (p : LF4.KSigma N), (birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p - ((InformationTheory.coarseLaw (LF4.kMuL p₀) (fibreCell m)) {c}).toReal) ^ 2 ∂LF4.kMuL p₀) Filter.atTop (nhds 0)

★★★ The convergence #118 asks for, in the finite-horizon reading. With asymptotic decay and a summable envelope the time-averaged occupation of a cell converges in L² to its Haar value.

This is the honest target #118(ii) named: equilibration conditional on decay, time-averaged, with the hypothesis doing the work.