HEXAGONbeta

Era statistics for the vacuum Bianchi IX flow

A mix of human-written and AI-generated textHuman understanding: no partsmath-ph — Mathematical Physicsmath.DS — Dynamical Systems

Contributed by Yi-kun Li ↗

Version 1 / Nov 06, 2026 / CC BY 4.0

Abstract

We prove the Gauss statistical law for eras of the exact vacuum Bianchi IX flow with zero cosmological constant. Eras are defined by transverse events along the solution, and their lengths count curvature transitions. Along almost every trajectory, the era phases have the Gauss distribution and every finite block of era lengths has its Gauss frequency. The tail decays inversely with era length; the limiting truncated mean grows logarithmically with the cutoff, while the full mean diverges. One invariant Borel exceptional set is null on every smooth transverse section and in the four-dimensional constraint manifold. The proof combines estimates for exact return branches with absolute continuity of their coding measure. Transverse contraction controls the accumulated phase error within each era, uniformly over unbounded era lengths and arbitrarily unequal small curvature variables. A density with strictly expanding section flux then forces almost every recurrent orbit to enter a statistical set on a small section.

Author comments: The Lean 4 formalization is also available on GitHub: https://github.com/l46430640-del/ERA-STATISTICS-FORMAL

Provenance statement

I used OpenAI AI tools to explore and develop proof strategies, implement the formalization in Lean 4, and draft and revise the manuscript. During formalization, the tools suggested alternative arguments that were easier to verify in Lean. The manuscript follows those arguments so that the written and formal proofs agree. The main theorem is machine-checked with two explicit inputs from the literature: Birkhoff’s pointwise ergodic theorem and a consequence of Brehm’s attractor theorem for vacuum Bianchi IX solutions. I checked the assumptions and conclusions of the Lean formalization and am confident that the proof as a whole is sound. Given the length of the manuscript, I have not personally verified every detail of the written proof. I used several AI tools to cross-check the manuscript as thoroughly as possible.

Formalizations

Tools used

OpenAI
Codex
OpenAI
ChatGPT

References

  1. V. A. Belinskii, I. M. Khalatnikov and E. M. Lifshitz, Oscillatory approach to a singular point in the relativistic cosmology , Advances in Physics 19 (1970), 525--573. https://doi.org/10.1080/00018737000101171.DOI
  2. F. Béguin and T. Dutilleul, Chaotic dynamics of spatially homogeneous spacetimes , Communications in Mathematical Physics 399 (2023), 737--927. https://doi.org/10.1007/s00220-022-04583-8.DOI
  3. F. Béguin, Aperiodic oscillatory asymptotic behavior for some Bianchi spacetimes , Classical and Quantum Gravity 27 (2010), 185005. https://doi.org/10.1088/0264-9381/27/18/185005.DOI
  4. B. Brehm, Bianchi VIII and IX vacuum cosmologies: Almost every solution forms particle horizons and converges to the Mixmaster attractor , preprint (2016), arXiv:1606.08058v1 (https://arxiv.org/abs/1606.08058v1).arXiv
  5. T. Damour and O. M. Lecian, Statistical properties of cosmological billiards , Physical Review D 83 (2011), 044038. https://doi.org/10.1103/PhysRevD.83.044038.DOI
  6. J. M. Heinzle and C. Uggla, Mixmaster: Fact and belief , Classical and Quantum Gravity 26 (2009), 075016. https://doi.org/10.1088/0264-9381/26/7/075016.DOI
  7. I. M. Khalatnikov, E. M. Lifshitz, K. M. Khanin, L. N. Shchur and Ya. G. Sinai, On the stochasticity in relativistic cosmology , Journal of Statistical Physics 38 (1985), 97--114. https://doi.org/10.1007/BF01017851.DOI
  8. S. Liebscher, J. Härterich, K. Webster and M. Georgi, Ancient dynamics in Bianchi models: Approach to periodic cycles , Communications in Mathematical Physics 305 (2011), 59--83. https://doi.org/10.1007/s00220-011-1248-3.DOI
  9. H. Ringström, The Bianchi IX attractor , Annales Henri Poincaré 2 (2001), 405--500. https://doi.org/10.1007/PL00001041. arXiv:gr-qc/0006035 (https://arxiv.org/abs/gr-qc/0006035).arXivDOI
  10. M. Reiterer and E. Trubowitz, The BKL conjectures for spatially homogeneous spacetimes , preprint (2010), arXiv:1005.4908v2 (https://arxiv.org/abs/1005.4908v2).arXiv
Show all 11 referencesShow fewer references
  1. C. Walkden, Ergodic Theory , lecture notes, University of Manchester, Corollary 10.1.2, p. 89. Online lecture notes (https://personalpages.manchester.ac.uk/staff/Charles.Walkden/ergodic-theory/ergodic_theory.pdf).link

Version history

  1. v1 · 257 pagesSubmitted by Yi-kun LiThe Lean 4 formalization is also available on GitHub: https://github.com/l46430640-del/ERA-STATISTICS-FORMALCurrentNov 06, 2026