A non-vacuity witness for HasCorrelationDecay

Category: 1-Mathlib. The equilibration arc's E5(a) (specs/equilibration-arc-plan.md): E4 is a conditional, so somebody must show its antecedent is satisfiable at all — otherwise the whole arc is a theorem about the empty set.

Why the witness has to look like this

HasCorrelationDecay with a summable envelope forces the correlations to converge to ⟨f⟩², so there is no way to cheat by choosing ε large. Two consequences pin the shape of any witness:

• HasCorrelationDecay.integral_mul_self_eq_of_periodic — a periodic map forces ⟨f²⟩ = ⟨f⟩², i.e. an a.e. constant observable.
• Every measure-preserving map of a finite or countable probability space is periodic on its support (mass is preserved and the atoms have positive mass), so no atomic space carries a witness.

So a genuine witness needs a non-atomic space and a genuinely non-periodic map. The doubling map on the circle is the minimal such object, and this file uses it.

The construction, and why it needs no Fourier analysis

Circ = ℝ ⧸ ℤ with its normalized Haar measure, doubling x = 2x, and the observable circObs x = Re e^{2πix} = cos 2πx. Every correlation is computed by the sign-flip argument already used throughout Q24, not by integration:

• rotating by 2^{-(s+1)} sends 2^s x ↦ 2^s x + 1/2, and circObs is odd under the half-turn, so the s-factor flips sign;
• the same rotation sends 2^t x ↦ 2^t x + 2^{t-s-1}, an integer, hence unchanged, so for s < t the t-factor is fixed.

The integrand is therefore odd under a measure-preserving translation, so its integral is zero: correlations vanish exactly, at every lag ≥ 1. The same trick with a quarter-turn (which exchanges real and imaginary parts) gives ⟨circObs²⟩ = 1/2 with no integral evaluated either — the quarter-phase move of Q24's phaseFlip.

What is proved

• ★★ circ_hasCorrelationDecay — the antecedent holds with the finitely-supported envelope ε = fun u => if u = 0 then 1 else 0, which is circ_summable;
• ★ integral_circObs_sq — ⟨circObs²⟩ = 1/2, and integral_circObs — ⟨circObs⟩ = 0;
• ★★ circ_nontrivial — hence ⟨f²⟩ ≠ ⟨f⟩²: the witness is not the trivial constant observable, which is exactly what non-vacuity requires;
• ★ doubling_not_periodic — a free corollary, and a consistency check on the no-go: the doubling map cannot be periodic, since it carries a non-constant observable with decay.

⚠️ Honest scope

• This witnesses the engine, not CSD. It says HasCorrelationDecay is satisfiable; it says nothing about whether any Σ-flow satisfies it. Indeed CSD.Thermo.not_hasCorrelationDecay_blockPop_of_periodic shows periodic Σ-flows cannot.
• The witness is a classical chaotic map, deliberately: the point is that the antecedent is a real condition met by real systems, not that the circle models a Σ.

Reference: specs/equilibration-arc-plan.md (E5); specs/future-work.md.

The circle, the doubling map, and the observable

@[reducible, inline]

abbrev MeasureTheory.Circ : Type

The circle ℝ ⧸ ℤ with its normalized Haar measure.

Equations

• MeasureTheory.Circ = AddCircle 1

instance MeasureTheory.instIsProbabilityMeasureCircVolume : IsProbabilityMeasure volume

noncomputable def MeasureTheory.doubling : Circ → Circ

The doubling map x ↦ 2x, the standard non-periodic measure-preserving map.

Equations

• MeasureTheory.doubling x = 2 • x

noncomputable def MeasureTheory.circObs : Circ → ℝ

The witness observable cos 2πx, written as the real part of the first character.

Equations

• MeasureTheory.circObs x = ((fourier 1) x).re

noncomputable def MeasureTheory.halfTurn : Circ

The half-turn, under which circObs is odd.

Equations

• MeasureTheory.halfTurn = ↑(1 / 2)

noncomputable def MeasureTheory.quarterTurn : Circ

The quarter-turn, which exchanges the real and imaginary parts of the character.

Equations

• MeasureTheory.quarterTurn = ↑(1 / 4)

theorem MeasureTheory.doubling_iterate (u : ℕ) (x : Circ) : doubling^[u] x = 2 ^ u • x

theorem MeasureTheory.measurable_doubling : Measurable doubling

theorem MeasureTheory.fourier_arg_add (x y : Circ) : (fourier 1) (x + y) = (fourier 1) x * (fourier 1) y

theorem MeasureTheory.norm_fourier_one (x : Circ) : ‖(fourier 1) x‖ = 1

theorem MeasureTheory.measurable_circObs : Measurable circObs

theorem MeasureTheory.abs_circObs_le_one (x : Circ) : |circObs x| ≤ 1

theorem MeasureTheory.integrable_circObs : Integrable circObs volume

The two turns

theorem MeasureTheory.fourier_halfTurn : (fourier 1) halfTurn = -1

theorem MeasureTheory.fourier_quarterTurn : (fourier 1) quarterTurn = Complex.I

theorem MeasureTheory.circObs_add_halfTurn (x : Circ) : circObs (x + halfTurn) = -circObs x

circObs is odd under the half-turn — the engine of every vanishing below.

theorem MeasureTheory.circObs_add_quarterTurn (x : Circ) : circObs (x + quarterTurn) = -((fourier 1) x).im

Under the quarter-turn the observable becomes (minus) the imaginary part.

theorem MeasureTheory.measurePreserving_rot (a : Circ) : MeasurePreserving (fun (x : Circ) => x + a) volume volume

The rotation that flips one factor and fixes the other

noncomputable def MeasureTheory.flipPoint (s : ℕ) : Circ

The rotation used at a pair of times s < t: by 2^{-(s+1)}.

Equations

• MeasureTheory.flipPoint s = ↑(↑(2 ^ (s + 1)))⁻¹

theorem MeasureTheory.doubling_iterate_add_flipPoint (s : ℕ) (x : Circ) : doubling^[s] (x + flipPoint s) = doubling^[s] x + halfTurn

It sends 2^s x to 2^s x + 1/2, so the s-factor flips sign.

theorem MeasureTheory.doubling_iterate_add_flipPoint_of_lt {s t : ℕ} (hst : s < t) (x : Circ) : doubling^[t] (x + flipPoint s) = doubling^[t] x

It fixes 2^t x whenever t > s, because 2^t / 2^{s+1} is then a whole number.

★ The correlations, all by symmetry

theorem MeasureTheory.integrable_circObs_iterate (t : ℕ) : Integrable (fun (x : Circ) => circObs (doubling^[t] x)) volume

theorem MeasureTheory.integrable_circObs_pair (s t : ℕ) : Integrable (fun (x : Circ) => circObs (doubling^[s] x) * circObs (doubling^[t] x)) volume

theorem MeasureTheory.integral_circObs_iterate (t : ℕ) : ∫ (x : Circ), circObs (doubling^[t] x) = 0

★ The mean is zero at every time, by the half-turn.

theorem MeasureTheory.integral_circObs : ∫ (x : Circ), circObs x = 0

theorem MeasureTheory.integral_circObs_pair_of_lt {s t : ℕ} (hst : s < t) : ∫ (x : Circ), circObs (doubling^[s] x) * circObs (doubling^[t] x) = 0

★★ The correlations vanish exactly at every nonzero lag. For s < t the rotation by 2^{-(s+1)} flips the s-factor and fixes the t-factor, so the integrand is odd.

★★ The witness

noncomputable def MeasureTheory.circEnv : ℕ → ℝ

The envelope: everything is exact after lag zero.

Equations

• MeasureTheory.circEnv u = if u = 0 then 1 else 0

theorem MeasureTheory.circ_summable : Summable circEnv

theorem MeasureTheory.circ_hasCorrelationDecay : HasCorrelationDecay volume doubling circObs circEnv

★★ The antecedent is satisfiable. The doubling map on the circle, with the observable cos 2πx, has correlation decay with a finitely-supported envelope.

★ Non-vacuity: the observable is not constant

theorem MeasureTheory.integrable_circObs_sq : Integrable (fun (x : Circ) => circObs x * circObs x) volume

theorem MeasureTheory.integrable_fourierIm_sq : Integrable (fun (x : Circ) => ((fourier 1) x).im * ((fourier 1) x).im) volume

theorem MeasureTheory.integral_circObs_sq : ∫ (x : Circ), circObs x * circObs x = 1 / 2

★ ⟨circObs²⟩ = 1/2 — by the quarter-turn, which exchanges the real and imaginary parts, plus |e^{2πix}| = 1. No integral is evaluated.

theorem MeasureTheory.circ_nontrivial : ∫ (x : Circ), circObs x * circObs x ≠ (∫ (y : Circ), circObs y) ^ 2

★★ The witness is non-trivial: ⟨f²⟩ ≠ ⟨f⟩², so circObs is not a.e. constant. This is what makes circ_hasCorrelationDecay a genuine non-vacuity certificate rather than a restatement of "constants have no correlations".

theorem MeasureTheory.doubling_not_periodic : ¬∃ (k : ℕ), 0 < k ∧ doubling^[k] = id

★ A free corollary, and a consistency check on the no-go. The doubling map is not periodic — if it were, the periodic no-go would force circObs to be constant, contradicting circ_nontrivial.