The fibre flow has no finite-horizon escape either

Category: 3-CSD. This closes Q12-d's route 2 for the corpus's own fibre flow.

W1 (KahlerFlowNoMixing.lean) kills the asymptotic mixing hypothesis for every flow the corpus defines. The escape the scoping doc recommends is Q12-d route 2: weaken mixing to finite-horizon decorrelation (MeasureTheory.HasCorrelationDecayUpTo), on the physical grounds that a real environment decorrelates on a timescale rather than asymptotically, and that a unitary flow on a large space can decorrelate for a long time before it recurs.

★★ exists_lag_le_envelope says that escape is not available to kFlow. The reason is quantitative recurrence: Dirichlet's approximation theorem (AddCircle.exists_norm_nsmul_le) returns j • sh to within 1/(n+1) of the identity at some lag j ≤ n, for every shift. So the correlation is back near its lag-zero value 1/2 at a lag bounded by a number depending only on how close you want to get — and, crucially, not on the horizon. Enlarging T buys nothing, because the return has already happened well inside it.

What is uniform, and why that is the point

The lag bound n depends on δ alone: not on the shift sh, not on the base point p₀, and not on the horizon T. Route 2's physical picture is "a big system wanders for a long time before coming back". A torus shift has no such room — Dirichlet caps the return time — and the theorem says so with a bound that is blind to every parameter one might hope to tune.

⚠️ Scope

• This is about kFlow, not about finite-horizon decorrelation in general. Route 2's engine (blockPop_timeAverage_le_of_finiteHorizon) is untouched and still correct; what is ruled out is instantiating its antecedent on the Kähler fibre shift. A flow with genuine room to wander is exactly what the corpus does not have.
• It is a statement about the fibre observable. A different observable could have smaller variance, but not zero — fibreObs_variance_ne — and the argument only needs the return.
• Nothing here says CSD cannot have a de-isolation flow with finite-horizon decorrelation. It says no flow currently in the corpus is one, which — with W1 — leaves Q12-d with no route that the corpus's present Σ-vocabulary can supply.

Reference: specs/q12-fibre-mechanism-scoping.md (Q12-d route 2, W1); specs/equilibration-arc-plan.md (E4/E6); specs/future-work.md.

The character's modulus of continuity at the identity

noncomputable def CSD.LF4.charDev (x : MeasureTheory.Circ) : ℝ

The first character's deviation from 1, on the circle. shiftDev is this read off the first fibre angle.

Equations

• CSD.LF4.charDev x = ‖(fourier 1) x - 1‖

@[simp]

theorem CSD.LF4.charDev_apply (x : MeasureTheory.Circ) : charDev x = ‖(fourier 1) x - 1‖

@[simp]

theorem CSD.LF4.charDev_zero : charDev 0 = 0

theorem CSD.LF4.continuous_charDev : Continuous charDev

theorem CSD.LF4.shiftDev_eq_charDev (v : KTorus) : shiftDev v = charDev v.1

theorem CSD.LF4.exists_charDev_lt {δ : ℝ} (hδ : 0 < δ) : ∃ (η : ℝ), 0 < η ∧ ∀ (x : MeasureTheory.Circ), ‖x‖ < η → charDev x < δ

The modulus of continuity at the identity: a small shift moves the character little.

Dirichlet: every shift returns, at a lag that does not depend on the shift

theorem CSD.LF4.exists_dirichlet_lag {δ : ℝ} (hδ : 0 < δ) : ∃ (n : ℕ), 0 < n ∧ ∀ (sh : KTorus), ∃ (j : ℕ), 1 ≤ j ∧ j ≤ n ∧ shiftDev (j • sh) < δ

★ The Dirichlet lag. For any δ > 0 there is a bound n — depending on δ alone — such that every shift sh returns within δ of the identity, as the character sees it, at some lag j ≤ n.

Uniformity in sh is what Dirichlet's theorem gives and what the finite-horizon argument needs: there is no shift, however finely tuned, whose first near-return can be pushed past n.

The finite-horizon no-go

theorem CSD.LF4.exists_lag_le_envelope {N : ℕ} {δ : ℝ} (hδ : 0 < δ) : ∃ (n : ℕ), 0 < n ∧ ∀ (p₀ : CPN N) (sh : KTorus) (ε : ℕ → ℝ) (T : ℕ), n < T → MeasureTheory.HasCorrelationDecayUpTo (kMuL p₀) (kFlow sh) fibreObs ε T → ∃ (j : ℕ), 1 ≤ j ∧ j ≤ n ∧ 1 / 2 - δ ≤ ε j

★★ Finite-horizon decorrelation fails for the fibre flow too, and the horizon cannot help.

For every δ > 0 there is a lag bound n — depending on δ alone — such that on any horizon T > n, a finite-horizon envelope for kFlow sh must already exceed 1/2 − δ at some lag in [1, n]. The bound is blind to the shift, to the base point, and to T.

This is Q12-d route 2 closed for kFlow. The escape's picture is a system that wanders long enough to decorrelate before recurring; Dirichlet caps the wandering, so a torus shift never gets the room.

theorem CSD.LF4.exists_lag_envelope_ge_quarter {N : ℕ} : ∃ (n : ℕ), 0 < n ∧ ∀ (p₀ : CPN N) (sh : KTorus) (ε : ℕ → ℝ) (T : ℕ), n < T → MeasureTheory.HasCorrelationDecayUpTo (kMuL p₀) (kFlow sh) fibreObs ε T → ∃ (j : ℕ), 1 ≤ j ∧ j ≤ n ∧ 1 / 4 ≤ ε j

★★ The same statement with a number in it: there is a lag n such that no horizon past n admits an envelope smaller than 1/4 throughout [1, n].