The fibre torus does admit a mixing map — the wall is about the map, not about Σ

Category: 3-CSD. Q12-d brick (i).

W1 and its finite-horizon companion say no flow the corpus defines can decorrelate. It is easy to read that as "Σ cannot mix", and that reading is wrong. ★★ torusDouble_hasCorrelationDecay exhibits a map of the corpus's own fibre T² whose correlations are exactly zero at every nonzero lag — the strongest possible decay, with a finitely supported envelope.

Why this escapes W1, precisely

not_hasCorrelationDecay_of_compactGroup rules out flows Ψ U whose iterates are the powers of an element of a compact group. kFlow is such a flow: it translates the torus, and translations are the compact group T² acting on itself, so Dirichlet-style recurrence applies and the correlations must come back.

torusDouble is the doubling endomorphism y ↦ 2y, not a translation. Its iterates are y ↦ 2ⁿ y, powers in the multiplicative monoid ℕ — discrete and non-compact. There is no compact group for the recurrence lemma to bite on, and in fact the correlations do not merely fail to recur: they vanish outright.

So the obstruction W1 records is a fact about the class of maps the corpus chose, not about the ontic space. Σ is unchanged here: KTorus is the fibre the Kähler instance already has.

⚠️ What this does and does not settle

• It does not replace kFlow. kFlow is the phase translation — free evolution — and it is correct that a phase translates. torusDouble is a candidate for the de-isolation map, which is what Q12-d asks for and which the corpus does not otherwise have.
• ⚠️ torusDouble is not invertible. That is a real limitation: a symplectic/Hamiltonian Σ-flow would be, so this is a witness that the mixing half of Q12-d is satisfiable on T², not yet a physically admissible de-isolation dynamics. The invertible case is a hyperbolic toral automorphism ([[2,1],[1,1]], the cat map): the character argument is the same shape, and the extra cost is Haar-invariance of a toral automorphism, which Mathlib does not provide.
• ⚠️ Mixing is not the race. Even with a mixing fibre map, Q12-d needs first-passage times to be exponential at moment-map rates. That link — hitting times of small sets in mixing systems are asymptotically exponential — is Galves–Schmitt/Abadi, rated research-grade and not upstream in W2. That, not Σ's vocabulary, is what actually blocks Q12-d.

The proof is free

torusObs reads only the first angle and torusDouble acts coordinatewise, so every correlation collapses to the corresponding one-dimensional integral and E5's witness (MeasureTheory.circ_hasCorrelationDecay) supplies the answer. The second factor integrates out through Measure.map_fst_prod. Nothing about the doubling map is re-proved.

Reference: specs/q12-fibre-mechanism-scoping.md (Q12-d, W1, W2); specs/equilibration-arc-plan.md (E5, the witness reused here); specs/future-work.md.

noncomputable def CSD.LF4.torusDouble : KTorus → KTorus

The doubling endomorphism of the fibre torus, y ↦ 2y in both angles.

A toral endomorphism, not a translation — which is exactly why W1 does not reach it.

Equations

• CSD.LF4.torusDouble = Prod.map MeasureTheory.doubling MeasureTheory.doubling

noncomputable def CSD.LF4.torusObs (y : KTorus) : ℝ

The fibre observable on the torus: cos 2π of the first angle. Same function as fibreObs, read on the fibre alone rather than on all of Σ.

Equations

• CSD.LF4.torusObs y = MeasureTheory.circObs y.1

@[simp]

theorem CSD.LF4.torusObs_apply (y : KTorus) : torusObs y = MeasureTheory.circObs y.1

theorem CSD.LF4.torusDouble_iterate (u : ℕ) (y : KTorus) : torusDouble^[u] y = (MeasureTheory.doubling^[u] y.1, MeasureTheory.doubling^[u] y.2)

@[simp]

theorem CSD.LF4.torusObs_torusDouble_iterate (u : ℕ) (y : KTorus) : torusObs (torusDouble^[u] y) = MeasureTheory.circObs (MeasureTheory.doubling^[u] y.1)

The second angle integrates out

theorem CSD.LF4.map_fst_torus : MeasureTheory.Measure.map Prod.fst MeasureTheory.volume = MeasureTheory.volume

theorem CSD.LF4.integral_torus_fst {F : MeasureTheory.Circ → ℝ} (hF : Measurable F) (hbd : ∀ (z : MeasureTheory.Circ), |F z| ≤ 1) : ∫ (y : KTorus), F y.1 = ∫ (x : MeasureTheory.Circ), F x

Integrals of functions of the first angle collapse to the circle.

theorem CSD.LF4.integral_torusObs_pair (s t : ℕ) : ∫ (y : KTorus), torusObs (torusDouble^[s] y) * torusObs (torusDouble^[t] y) = ∫ (x : MeasureTheory.Circ), MeasureTheory.circObs (MeasureTheory.doubling^[s] x) * MeasureTheory.circObs (MeasureTheory.doubling^[t] x)

theorem CSD.LF4.integral_torusObs : ∫ (y : KTorus), torusObs y = 0

The witness

theorem CSD.LF4.torusDouble_hasCorrelationDecay : MeasureTheory.HasCorrelationDecay MeasureTheory.volume torusDouble torusObs MeasureTheory.circEnv

★★ The corpus's fibre torus carries a map whose correlations vanish exactly.

torusDouble has MeasureTheory.circEnv as a decay envelope — 1 at lag zero and 0 at every other lag. That is not merely decay, it is exact decorrelation at every nonzero lag.

Read against not_hasCorrelationDecay_kFlow: the same fibre, the same observable, opposite verdicts. The difference is entirely that kFlow translates and torusDouble does not, which is precisely the hypothesis not_hasCorrelationDecay_of_compactGroup needs and torusDouble fails to meet. W1 constrains the choice of map, not the ontic space.

theorem CSD.LF4.torusDouble_summable : Summable MeasureTheory.circEnv

The envelope is summable, so the witness meets the hypothesis E4's engine actually takes.

theorem CSD.LF4.torusObs_variance_ne : ∫ (y : KTorus), torusObs y * torusObs y ≠ (∫ (z : KTorus), torusObs z) ^ 2

Non-trivial: the observable is not almost everywhere constant, so this is a genuine witness rather than the degenerate case that HasCorrelationDecay.integral_mul_self_eq_of_recurrent forces on every compact-group flow.

Kac on the same map

theorem CSD.LF4.kac_doubling {A : Set MeasureTheory.Circ} (hA : MeasurableSet A) (hApos : MeasureTheory.volume A ≠ 0) : ∑' (n : ℕ), MeasureTheory.volume (A ∩ {x : MeasureTheory.Circ | ↑n < MeasureTheory.returnTime MeasureTheory.doubling A x}) = 1

★★ Kac's formula on the mixing fibre map, which is also the non-vacuity check for MeasureTheory.tsum_measure_lt_returnTime: its hypotheses (ergodic, measure-preserving, positive measure) are satisfiable, and satisfied by the very map brick (i) exhibits.

The content: a fibre cell of measure b is returned to on average every 1/b steps. That is the rate content of the record layer's race, derived from the dynamics rather than posited — and it is regime-correct, holding for any cell of positive measure rather than only for rare ones.

⚠️ It gives the rates, not the exponential law. See the Q12-d row.