The fibre cells decorrelate under the hyperbolic stroke

Category: 7-SigmaLayer. BACKLOG #118(i), the hypothesis #118(ii), #130 and #144 consumed; R-019; consumed by FibreRelaxation.lean (#147).

Every finite-horizon theorem of FibreFiniteHorizon.lean, FibreHorizonDivergence.lean and FibreCellUniform.lean took finite-horizon correlation decay of the cell indicators as a hypothesis, #118(i), recorded as a genuine mathematical question about the cat map on indicator functions. This file proves it, and then states what the corpus's rate theorems become once their hypothesis is a theorem.

The identification

A fibre cell fibreCell m ⁻¹' {(k, l)} is a product of two circle cells, and a circle cell is the open grid arc (k/(m+1), (k+1)/(m+1)) up to its two endpoints (★ circCell_ind_ae_eq_arcIndR, from FibreCellUniform.lean's sandwich). So on Σ, almost everywhere for μL, ★★ fibreCellInd_ae_eq_rectIndR: the cell indicator is the indicator of a rectangle of arcs on the fibre, exactly the observable Mathlib/Dynamics/CatMapMixing.lean decorrelates. Decay transfers across almost-everywhere equality of the observable (HasCorrelationDecay.congr_ae, through measure preservation of the stroke) and lifts from the fibre to Σ along the second projection (HasCorrelationDecay.liftSnd, the base carrying mass 1).

The results

• ★★★ fibreStroke_hasCorrelationDecay_fibreCellInd: every fibre cell's indicator has exponentially decaying correlations under the hyperbolic stroke, with the explicit summable envelope catRectEnv (4 · 2^{-⌊(n−2)/3⌋} from lag 2). #118(i), discharged for the corpus's hyperbolic fibre map.
• ★★★ integral_birkhoffAverage_fibreCellInd_sub_sq_le_hyperbolic: the finite-horizon equilibration of a cell, unconditionally: the mean-square deviation of its time-averaged occupation from 1/(m+1)² is at most 130/T at horizon T; and ★★★ tendsto_integral_birkhoffAverage_fibreCellInd_sub_sq_hyperbolic, the L² convergence of the time averages with no hypothesis.
• ★★★ abs_integral_fibreCellInd_iterate_mul_sub_le: two cells decorrelate at step n: the joint occupation of c' after n strokes and of c now is within catRectEnv n of 1/(m+1)⁴. This is instantaneous (mixing), not a time average.
• ★★★ abs_stepWeight_sub_le and ★★★ klDiv_stepLaw_le: the law at step n of a coarse-grained initial density approaches the uniform cell law, in relative entropy, at the rate of the envelope. For a density ∑ w_c 1_c constant on the cells, nonnegative and normalised, the cell law after n strokes (stepLaw, a probability measure on the cells) satisfies klDiv (stepLaw n) (uniform) ≤ (m+1)⁸ · catRectEnv n², through the chi-squared bound of ChiSquare.lean. This is R-019's second clause, the distribution approaches Haar, stated at step n in klDiv, with a rate in the cell count, for the hyperbolic fibre map and every initial distribution coarse-grained on the same grid. Together with the monotone clause of FibreCoarseArrow.lean (#18) it is the relaxation statement Track B asked for, on this map.

Honest scope

• The map is the available hyperbolic witness, not a derived de-isolation dynamics. catStroke is MovingFibreWitness.lean's cat map on the fibre, offered there as an available hyperbolic fibre map and not wired into a ConstraintDynamics. That the physical de-isolation flow acts on the fibre by a hyperbolic map is the A5/D1 residue (Posit 1, BACKLOG #19); nothing here derives it. What is proved is: given that map, the fibre relaxes, with these rates.
• Initial densities coarse-grained on the grid. cellDensity is constant on the (m+1)² cells. A density that is a finite combination of indicators of arbitrary rectangles of arcs is covered by the same Category-1 pair bound; a general L² density is FibreRelaxation.lean (#147): convergence with no rate, by the strong mixing of the cat map on L²(T²). The rate is what this file adds, and it is for the coarse-grained class. The relaxation H-theorem for the fibre stays on the map identification. RESIDUE(R-019)
• The constants are polynomial in the cell count, (m+1)⁸ in the divergence bound, from (m+1)² cells each deviating by at most (m+1)² · catRectEnv n, and the envelope is not sharp (see the Category-1 file). The exponential rate in n is what matters, and the first-passage question #118(iii) was not needed for it.
• Unchanged: nothing here is about the translation kFlow, which relaxation_requires_hyperbolic_fibre shows cannot decorrelate; the typicality posits are untouched.

References: specs/BACKLOG.md #118, #18, #130, #144, #147; specs/residues.tsv R-019; Mathlib/Dynamics/CatMapMixing.lean; SigmaLayer/FibreFiniteHorizon.lean; SigmaLayer/FibreHorizonDivergence.lean; SigmaLayer/FibreCellUniform.lean; SigmaLayer/MovingFibreWitness.lean.

A fibre cell is a rectangle of arcs, almost everywhere

theorem CSD.SigmaLayer.unitRep_eq_rep : MeasureTheory.unitRep = RecordLayer.rep

The representative used by the Category-1 arcs is the record layer's rep.

@[reducible, inline]

noncomputable abbrev CSD.SigmaLayer.gridLo (m : ℕ) (k : Fin (m + 1)) : ℝ

The left endpoint of the k-th grid arc.

Equations

• CSD.SigmaLayer.gridLo m k = ↑↑k / (↑m + 1)

@[reducible, inline]

noncomputable abbrev CSD.SigmaLayer.gridHi (m : ℕ) (k : Fin (m + 1)) : ℝ

The right endpoint of the k-th grid arc.

Equations

• CSD.SigmaLayer.gridHi m k = (↑↑k + 1) / (↑m + 1)

theorem CSD.SigmaLayer.gridLo_nonneg (m : ℕ) (k : Fin (m + 1)) : 0 ≤ gridLo m k

theorem CSD.SigmaLayer.gridLo_lt_gridHi (m : ℕ) (k : Fin (m + 1)) : gridLo m k < gridHi m k

theorem CSD.SigmaLayer.gridHi_le_one (m : ℕ) (k : Fin (m + 1)) : gridHi m k ≤ 1

theorem CSD.SigmaLayer.volume_rep_preimage_singleton (t : ℝ) : MeasureTheory.volume (RecordLayer.rep ⁻¹' {t}) = 0

The rep-preimage of a single point of the circle is null.

theorem CSD.SigmaLayer.circCell_ind_ae_eq_arcIndR (m : ℕ) (k : Fin (m + 1)) : (fun (x : AddCircle 1) => if circCell m x = k then 1 else 0) =ᵐ[MeasureTheory.volume] MeasureTheory.arcIndR (gridLo m k) (gridHi m k)

★ A circle cell is its open grid arc up to a null set: the two indicators differ only at the two endpoints of the arc.

theorem CSD.SigmaLayer.fibreCellInd_eq_mul_ite {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (p : LF4.KSigma N) : fibreCellInd m c p = (if circCell m p.2.1 = c.1 then 1 else 0) * if circCell m p.2.2 = c.2 then 1 else 0

The cell indicator on Σ factors through the fibre as a product of two circle tests.

theorem CSD.SigmaLayer.fibreCellInd_ae_eq_rectIndR {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : fibreCellInd m c =ᵐ[LF4.kMuL p₀] fun (p : LF4.KSigma N) => MeasureTheory.rectIndR (gridLo m c.1) (gridHi m c.1) (gridLo m c.2) (gridHi m c.2) p.2

★★ A fibre cell is a rectangle of grid arcs on the fibre, almost everywhere for μL.

Transport from the fibre to Σ

theorem CSD.SigmaLayer.fsMeasure_univ_eq_one {N : ℕ} (p₀ : LF4.CPN N) : (Matrix.UnitaryGroup.fsMeasure p₀) Set.univ = 1

theorem CSD.SigmaLayer.integral_snd_kMuL {N : ℕ} (p₀ : LF4.CPN N) (h : LF4.KTorus → ℝ) : ∫ (p : LF4.KSigma N), h p.2 ∂LF4.kMuL p₀ = ∫ (y : LF4.KTorus), h y

Integrating a function of the fibre coordinate against μL integrates it against Haar on the fibre: the base carries total mass 1.

theorem CSD.SigmaLayer.fibreStroke_iterate {N : ℕ} (u : ℕ) (p : LF4.KSigma N) : fibreStroke^[u] p = (p.1, catStroke^[u] p.2)

theorem CSD.SigmaLayer.HasCorrelationDecay.liftSnd {N : ℕ} (p₀ : LF4.CPN N) {g : LF4.KTorus → ℝ} {ε : ℕ → ℝ} (hg : MeasureTheory.HasCorrelationDecay MeasureTheory.volume catStroke g ε) : MeasureTheory.HasCorrelationDecay (LF4.kMuL p₀) fibreStroke (fun (p : LF4.KSigma N) => g p.2) ε

Decay of a fibre observable lifts to Σ along the second projection.

theorem CSD.SigmaLayer.HasCorrelationDecay.congr_ae {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {Φ : X → X} {f g : X → ℝ} {ε : ℕ → ℝ} (hΦ : MeasureTheory.MeasurePreserving Φ μ μ) (hfg : f =ᵐ[μ] g) (hg : MeasureTheory.HasCorrelationDecay μ Φ g ε) : MeasureTheory.HasCorrelationDecay μ Φ f ε

Decay transfers across almost-everywhere equality of the observable.

theorem CSD.SigmaLayer.fibreStroke_hasCorrelationDecay_fibreCellInd {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : MeasureTheory.HasCorrelationDecay (LF4.kMuL p₀) fibreStroke (fibreCellInd m c) MeasureTheory.catRectEnv

★★★ The fibre cells decorrelate exponentially under the hyperbolic stroke. This is the hypothesis every finite-horizon theorem of FibreFiniteHorizon.lean consumed, now proved for the corpus's hyperbolic fibre map.

The finite-horizon theorems, unconditional

theorem CSD.SigmaLayer.sum_range_catRectEnv_le (T : ℕ) : ∑ u ∈ Finset.range T, MeasureTheory.catRectEnv u ≤ 65

The envelope's partial sums are bounded by 65.

theorem CSD.SigmaLayer.integral_birkhoffAverage_fibreCellInd_sub_sq_le_hyperbolic {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) {T : ℕ} (hT : 0 < T) : ∫ (p : LF4.KSigma N), (birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p - ((↑m + 1) ^ 2)⁻¹) ^ 2 ∂LF4.kMuL p₀ ≤ 130 / ↑T

★★★ Finite-horizon equilibration of a fibre cell, unconditionally: at horizon T the mean-square deviation of the cell's time-averaged occupation from 1/(m+1)² is at most 130 / T.

theorem CSD.SigmaLayer.tendsto_integral_birkhoffAverage_fibreCellInd_sub_sq_hyperbolic {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : 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 time-averaged occupation of every fibre cell converges in L² to its Haar value, with no hypothesis.

The law at step n: two cells, then a coarse-grained density

theorem CSD.SigmaLayer.integral_rectIndR_grid {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : ∫ (y : LF4.KTorus), MeasureTheory.rectIndR (gridLo m c.1) (gridHi m c.1) (gridLo m c.2) (gridHi m c.2) y = ((↑m + 1) ^ 2)⁻¹

The mean of a grid rectangle on the fibre is 1/(m+1)².

theorem CSD.SigmaLayer.abs_integral_fibreCellInd_iterate_mul_sub_le {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c c' : Fin (m + 1) × Fin (m + 1)) (n : ℕ) : |∫ (p : LF4.KSigma N), fibreCellInd m c' (fibreStroke^[n] p) * fibreCellInd m c p ∂LF4.kMuL p₀ - ((↑m + 1) ^ 2)⁻¹ * ((↑m + 1) ^ 2)⁻¹| ≤ MeasureTheory.catRectEnv n

★★★ Two fibre cells decorrelate at step n: the joint occupation of c' after n strokes and c now is within catRectEnv n of the product 1/(m+1)⁴. This is the instantaneous (mixing) statement, not a time average.

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

A density on Σ that is constant on the fibre cells: the coarse-grained initial distributions of Track B.

Equations

• CSD.SigmaLayer.cellDensity m w p = ∑ c : Fin (m + 1) × Fin (m + 1), w c * CSD.SigmaLayer.fibreCellInd m c p

theorem CSD.SigmaLayer.measurable_cellDensity {N : ℕ} (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) : Measurable (cellDensity m w)

theorem CSD.SigmaLayer.abs_cellDensity_le {N : ℕ} (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) (p : LF4.KSigma N) : |cellDensity m w p| ≤ ∑ c : Fin (m + 1) × Fin (m + 1), |w c|

noncomputable def CSD.SigmaLayer.stepWeight {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : ℝ

The mass the coarse-grained density puts on the cell c' after n strokes.

Equations

• CSD.SigmaLayer.stepWeight p₀ m w n c' = ∫ (p : CSD.LF4.KSigma N), CSD.SigmaLayer.fibreCellInd m c' (CSD.SigmaLayer.fibreStroke^[n] p) * CSD.SigmaLayer.cellDensity m w p ∂CSD.LF4.kMuL p₀

theorem CSD.SigmaLayer.integrable_fibreCellInd_iterate_mul {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c c' : Fin (m + 1) × Fin (m + 1)) (n : ℕ) : MeasureTheory.Integrable (fun (p : LF4.KSigma N) => fibreCellInd m c' (fibreStroke^[n] p) * fibreCellInd m c p) (LF4.kMuL p₀)

theorem CSD.SigmaLayer.stepWeight_eq_sum {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : stepWeight p₀ m w n c' = ∑ c : Fin (m + 1) × Fin (m + 1), w c * ∫ (p : LF4.KSigma N), fibreCellInd m c' (fibreStroke^[n] p) * fibreCellInd m c p ∂LF4.kMuL p₀

The step weight is the w-combination of the pair occupations.

theorem CSD.SigmaLayer.abs_stepWeight_sub_le {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : |stepWeight p₀ m w n c' - (∑ c : Fin (m + 1) × Fin (m + 1), w c) * (((↑m + 1) ^ 2)⁻¹ * ((↑m + 1) ^ 2)⁻¹)| ≤ (∑ c : Fin (m + 1) × Fin (m + 1), |w c|) * MeasureTheory.catRectEnv n

★★★ The law at step n of a coarse-grained density approaches the uniform cell law at the rate of the envelope: each cell's mass is within (∑|w|) · catRectEnv n of its limit (∑ w) / (m+1)⁴.

The step-n law as a measure on the cells, and its divergence from uniform

theorem CSD.SigmaLayer.sum_fibreCellInd {N : ℕ} (m : ℕ) (q : LF4.KSigma N) : ∑ c : Fin (m + 1) × Fin (m + 1), fibreCellInd m c q = 1

Exactly one cell contains any point: the cell indicators sum to 1.

theorem CSD.SigmaLayer.integrable_fibreCellInd {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : MeasureTheory.Integrable (fibreCellInd m c) (LF4.kMuL p₀)

theorem CSD.SigmaLayer.integrable_fibreCellInd_iterate_mul_cellDensity {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : MeasureTheory.Integrable (fun (p : LF4.KSigma N) => fibreCellInd m c' (fibreStroke^[n] p) * cellDensity m w p) (LF4.kMuL p₀)

theorem CSD.SigmaLayer.stepWeight_nonneg {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {w : Fin (m + 1) × Fin (m + 1) → ℝ} (hw : ∀ (c : Fin (m + 1) × Fin (m + 1)), 0 ≤ w c) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : 0 ≤ stepWeight p₀ m w n c'

theorem CSD.SigmaLayer.sum_stepWeight {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) (n : ℕ) : ∑ c' : Fin (m + 1) × Fin (m + 1), stepWeight p₀ m w n c' = ∫ (p : LF4.KSigma N), cellDensity m w p ∂LF4.kMuL p₀

The step weights sum to the mass of the density.

theorem CSD.SigmaLayer.integral_cellDensity {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) : ∫ (p : LF4.KSigma N), cellDensity m w p ∂LF4.kMuL p₀ = (∑ c : Fin (m + 1) × Fin (m + 1), w c) * ((↑m + 1) ^ 2)⁻¹

The mass of a coarse-grained density is (∑ w) / (m+1)².

noncomputable def CSD.SigmaLayer.stepLaw {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (w : Fin (m + 1) × Fin (m + 1) → ℝ) (n : ℕ) : MeasureTheory.Measure (Fin (m + 1) × Fin (m + 1))

The law at step n of the coarse-grained density, as a measure on the cells: the step weights placed at the cells.

Equations

• CSD.SigmaLayer.stepLaw p₀ m w n = ∑ c' : Fin (m + 1) × Fin (m + 1), ENNReal.ofReal (CSD.SigmaLayer.stepWeight p₀ m w n c') • MeasureTheory.Measure.dirac c'

theorem CSD.SigmaLayer.stepLaw_real_apply {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {w : Fin (m + 1) × Fin (m + 1) → ℝ} (hw : ∀ (c : Fin (m + 1) × Fin (m + 1)), 0 ≤ w c) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : (stepLaw p₀ m w n).real {c'} = stepWeight p₀ m w n c'

theorem CSD.SigmaLayer.isProbabilityMeasure_stepLaw {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {w : Fin (m + 1) × Fin (m + 1) → ℝ} (hw : ∀ (c : Fin (m + 1) × Fin (m + 1)), 0 ≤ w c) (hnorm : ∑ c : Fin (m + 1) × Fin (m + 1), w c = (↑m + 1) ^ 2) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (stepLaw p₀ m w n)

The step law of a normalised nonnegative density is a probability measure.

theorem CSD.SigmaLayer.klDiv_stepLaw_le {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {w : Fin (m + 1) × Fin (m + 1) → ℝ} (hw : ∀ (c : Fin (m + 1) × Fin (m + 1)), 0 ≤ w c) (hnorm : ∑ c : Fin (m + 1) × Fin (m + 1), w c = (↑m + 1) ^ 2) (n : ℕ) : InformationTheory.klDiv (stepLaw p₀ m w n) (ProbabilityTheory.uniformOn Set.univ) ≤ ENNReal.ofReal ((↑m + 1) ^ 8 * MeasureTheory.catRectEnv n ^ 2)

★★★ The divergence of the step-n law from the uniform cell law decays exponentially: for a nonnegative density constant on the cells and normalised to mass 1, klDiv (stepLaw n) (uniform) ≤ (m+1)⁸ · catRectEnv n². This is R-019's second clause at step n — the instantaneous, relative-entropy statement, not a time average — for the hyperbolic fibre map and every initial distribution coarse-grained on the same grid.