The Kähler fibre flow cannot mix either

Category: 3-CSD. This closes the second half of W1 (specs/q12-fibre-mechanism-scoping.md), and it is the Q12-w brick that scoping doc lists.

W1 claims that no flow the corpus defines can supply the mixing hypothesis E4 needs. It was half a theorem. The unitary base action was proved (CSD.Thermo.not_hasCorrelationDecay_blockPop_of_unitary); the T² fibre shift kFlow was asserted by analogy — "the identical argument applies" — and kProjectedFlow is id, which is the periodic case. ★★ not_hasCorrelationDecay_kFlow supplies the missing half, so W1 is now a theorem across every flow the corpus has.

What made it cheap

MeasureTheory.not_hasCorrelationDecay_of_compactAddGroup — the general statement extracted from the unitary proof — does the work, and to_additive is what lets the same proof cover a multiplicative group action and an additive torus shift. Three inputs remain:

• kFlow_iterate — iterating the shift n times is shifting by n • sh, which is the hpow the general theorem asks for;
• abs_fibreCorr_sub_le — a uniform modulus. The exact correlation is not needed: shifting moves the observable by Re((e(v) − 1)·e(x)), so the correlation moves by at most ‖e(v) − 1‖, which is continuous and vanishes at 0. That is continuousAt_correlation_of_abs_sub_le_add's hypothesis, and it dodges every Fubini argument;
• integral_fibreObs and integral_fibreObs_sq — the variance, which does need the product structure, but only through Measure.map_fst_prod / Measure.map_snd_prod and integral_map.

The observable fibreObs is cos 2π of the first fibre angle, reused from MeasureTheory.circObs. It was built as the witness observable for the doubling map (E5); here it plays the opposite role, certifying that the fibre flow's correlations cannot decay. Same function, opposite verdict — the difference is entirely in the map.

⚠️ What this does and does not close

It closes the statement of W1: the corpus's Σ-dynamics is compact-group translation throughout, and compact-group translation cannot mix. It does not say CSD cannot have a mixing de-isolation flow — it says no such flow is currently in the corpus, and that any escape must leave compact-group translations. Q12-d's route 2 (finite-horizon decorrelation, MeasureTheory.HasCorrelationDecayUpTo) is untouched by this and remains the recommended escape: this theorem kills the asymptotic antecedent only.

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

noncomputable def CSD.LF4.fibreObs {N : ℕ} (p : KSigma N) : ℝ

The fibre observable: cos 2π of the first T² angle, as a function on Σ.

Reused from MeasureTheory.circObs, which the E5 witness built for the doubling map. It is the simplest observable that sees the fibre and averages to zero.

Equations

• CSD.LF4.fibreObs p = MeasureTheory.circObs p.2.1

@[simp]

theorem CSD.LF4.fibreObs_apply {N : ℕ} (p : KSigma N) : fibreObs p = MeasureTheory.circObs p.2.1

theorem CSD.LF4.measurable_fibreObs {N : ℕ} : Measurable fibreObs

theorem CSD.LF4.abs_fibreObs_le_one {N : ℕ} (p : KSigma N) : |fibreObs p| ≤ 1

theorem CSD.LF4.kFlow_iterate {N : ℕ} (sh : KTorus) (n : ℕ) (p : KSigma N) : (kFlow sh)^[n] p = kFlow (n • sh) p

Iterating the shift is shifting by the multiple — the hpow hypothesis of MeasureTheory.not_hasCorrelationDecay_of_compactAddGroup.

The fibre marginal, and the variance it gives

theorem CSD.LF4.map_fibreCoord {N : ℕ} (p₀ : CPN N) : MeasureTheory.Measure.map (fun (p : KSigma N) => p.2.1) (kMuL p₀) = MeasureTheory.volume

Σ's first fibre angle is uniform: the pushforward of μL along it is Lebesgue on the circle.

Both projections are probability-measure marginals, so this is Measure.map_snd_prod followed by Measure.map_fst_prod.

theorem CSD.LF4.integral_fibreCoord {N : ℕ} (p₀ : CPN N) {F : MeasureTheory.Circ → ℝ} (hF : Measurable F) (hbd : ∀ (z : MeasureTheory.Circ), |F z| ≤ 1) : ∫ (p : KSigma N), F p.2.1 ∂kMuL p₀ = ∫ (z : MeasureTheory.Circ), F z

Integrals of fibre functions reduce to integrals on the circle.

theorem CSD.LF4.integral_fibreObs {N : ℕ} (p₀ : CPN N) : ∫ (p : KSigma N), fibreObs p ∂kMuL p₀ = 0

theorem CSD.LF4.integral_fibreObs_sq {N : ℕ} (p₀ : CPN N) : ∫ (p : KSigma N), fibreObs p * fibreObs p ∂kMuL p₀ = 1 / 2

theorem CSD.LF4.fibreObs_variance_ne {N : ℕ} (p₀ : CPN N) : ∫ (p : KSigma N), fibreObs p * fibreObs p ∂kMuL p₀ ≠ (∫ (q : KSigma N), fibreObs q ∂kMuL p₀) ^ 2

The fibre observable has nonzero variance: ⟨f²⟩ = 1/2 while ⟨f⟩ = 0.

The modulus, and the no-go

noncomputable def CSD.LF4.shiftDev (v : KTorus) : ℝ

The deviation of a shift from the identity, as the character sees it.

Equations

• CSD.LF4.shiftDev v = ‖(fourier 1) v.1 - 1‖

@[simp]

theorem CSD.LF4.shiftDev_apply (v : KTorus) : shiftDev v = ‖(fourier 1) v.1 - 1‖

theorem CSD.LF4.continuous_shiftDev : Continuous shiftDev

@[simp]

theorem CSD.LF4.shiftDev_zero : shiftDev 0 = 0

theorem CSD.LF4.abs_fibreCorr_sub_le {N : ℕ} (p₀ : CPN N) (v : KTorus) : |∫ (p : KSigma N), fibreObs p * fibreObs (kFlow v p) ∂kMuL p₀ - ∫ (p : KSigma N), fibreObs p * fibreObs p ∂kMuL p₀| ≤ shiftDev v

★ The correlation moves by at most shiftDev v. Shifting the fibre replaces the character e(x) by e(v)·e(x), so the observable moves by Re((e(v) − 1)·e(x)), whose size is ‖e(v) − 1‖ because characters have modulus one. The uniform bound then integrates directly.

This is what makes the exact correlation unnecessary — continuity at 0 is all the general no-go asks for.

theorem CSD.LF4.not_hasCorrelationDecay_kFlow {N : ℕ} (p₀ : CPN N) (sh : KTorus) {ε : ℕ → ℝ} (hsum : Summable ε) : ¬MeasureTheory.HasCorrelationDecay (kMuL p₀) (kFlow sh) fibreObs ε

★★ W1's missing half: the Kähler fibre flow cannot have decaying correlations.

For any base point and any shift sh, the fibre observable has no summable decay envelope along kFlow sh. With CSD.Thermo.not_hasCorrelationDecay_blockPop_of_unitary for the base action and HasCorrelationDecay.integral_mul_self_eq_of_periodic for kProjectedFlow = id, every flow the corpus defines is now covered by a theorem, which is what W1 asserted and half-proved.

⚠️ Read it as a limitation on the route, not on CSD. Mixing systems exist — MeasureTheory.circ_hasCorrelationDecay is one — and they are precisely the ones that are not compact-group translations. What is ruled out is deriving the first-passage race from asymptotic mixing of any dynamics the corpus currently has; the finite-horizon escape (MeasureTheory.HasCorrelationDecayUpTo, Q12-d route 2) is untouched.