\documentclass[11pt,a4paper]{amsart}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{amsmath,amssymb,mathtools}
\usepackage{graphicx}
\usepackage{placeins}
\usepackage{xcolor}
\usepackage[margin=30mm]{geometry}
\usepackage[hidelinks]{hyperref}
\hypersetup{bookmarksdepth=2}
\numberwithin{equation}{section}
\allowdisplaybreaks[1]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\newcommand{\R}{\mathbb R}
\newcommand{\N}{\mathbb N}
\newcommand{\M}{\mathcal M_{+++}}
\newcommand{\Z}{\mathcal Z}
\newcommand{\dd}{\,d}
\newcommand{\Dt}{\mathop{\mathrm D_t}\nolimits}
\newcommand{\Pin}{P_{\mathrm{in}}}
\newcommand{\ind}{\mathbf 1}
\DeclareMathOperator{\Leb}{Leb}
\DeclareMathOperator{\dist}{dist}
\DeclareMathOperator{\Lip}{Lip}
\title{Era statistics for the vacuum Bianchi IX flow}
\author{Yi-kun Li}
\address{State Key Laboratory of Radio Astronomy and Technology,
Xinjiang Astronomical Observatory, CAS, 150 Science 1-Street,
Urumqi 830011, China}
\address{College of Astronomy and Space Science,
University of Chinese Academy of Sciences, No.1 Yanqihu East Road,
Beijing 101408, China}
\email{\href{mailto:liyikun@xao.ac.cn}{liyikun@xao.ac.cn}}
\urladdr{\href{https://orcid.org/0009-0003-4143-2141}{0009-0003-4143-2141}}
\date{}
\begin{document}
\raggedbottom
\begin{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.
\end{abstract}
\maketitle
% Put the author affiliations and contact details on the title page.
\makeatletter
\begingroup
\renewcommand{\emailaddrname}{\textit{Corresponding author}}
\renewcommand{\urladdrname}{\textit{ORCID}}
\@setaddresses
\endgroup
\global\let\addresses\@empty
\makeatother
\clearpage
\setcounter{tocdepth}{2}
\begingroup
\linespread{0.93}\selectfont
\tableofcontents
\endgroup
\clearpage
\input{sections/introduction}
\input{sections/flow-and-eras}
\section{Continued fractions and statistical transfer}
\label{sec:statistical-transfer}

The statistical argument needs two properties of the exact returns:
their phases follow perturbed inverse Gauss branches, and the measure
of each finite itinerary is controlled by its Gauss cylinder.
We first prove what these properties imply. This identifies the value,
derivative and measure estimates that the subsequent dynamics must provide.

\input{sections/phase-comparison}
\input{sections/gauss-statistics}
\input{sections/coding-measure}
\section{Passage through a curvature core}
\label{sec:curvature-cores}

A core is the part of a curvature transition between the upward and
downward crossings of the active wall. Its transverse contraction
controls the error accumulated before the next core. We establish the
actual passage, its ordinary initial-data derivatives, and the invariant
directions needed to iterate curves of entrance states.

\input{sections/core-passage}
\input{sections/core-variation}
\input{sections/core-multipliers}
\input{sections/core-uniform}
\section{Reflections at large radius}
\label{sec:large-reflections}

After a nonterminal core the two active axes exchange roles.
At large radius the resulting connection may take a long time.
The estimates below retain the small wall factors throughout that
interval, so that both the phase error and its derivatives remain
controlled by transverse amplitude.

\input{sections/connection-passage}
\input{sections/connection-variation}
\input{sections/connection-cone}
\section{Reflections at bounded radius}
\label{sec:bounded-reflections}

The bounded range completes the reflection estimates down to the
terminal threshold. Here a finite outgoing passage and a possibly long
incoming passage are joined through the single-wall geometry.
The stable boundary phase organizes their derivatives; the final result
combines this range with the large-radius estimate.

\input{sections/compact-connection-passage}
\input{sections/stable-boundary-phase}
\input{sections/stable-phase-derivatives}
\input{sections/entrance-phase-transport}
\input{sections/entrance-variation}
\input{sections/entrance-physical-radius}
\input{sections/compact-connection-phase}
\input{sections/reflection-uniform}
\section{The terminal connection}
\label{sec:terminal-connections}

At the last core of an era, a cyclic change of axes replaces the
reflection. The new reciprocal radius is the bounded phase that enters
the next inverse branch. We determine this phase and its derivatives,
together with the transverse contraction needed at the next entrance.

\input{sections/terminal-passage}
\input{sections/terminal-variation}
\input{sections/terminal-phase-value}
\input{sections/terminal-single-phase}
\input{sections/terminal-physical-phase}
\input{sections/terminal-cone}
\section{Complete era returns and their statistics}
\label{sec:complete-era-returns}

The core and connection estimates now form an entire era return.
Their errors are summed against transverse losses, giving constants
independent of the number of cores. At each entrance we retain the
branches whose radii and wall amplitudes satisfy the estimates for
another return. Iterating this selection gives a set of entrances
with an infinite itinerary. The coding measure estimate then yields
the statistics of these itineraries in
Theorem~\ref{thm:era-graph-statistics}.
We recover their complete events in the original time and estimate
the measure left outside this construction along entrance families.

\input{sections/era-accumulation}
\input{sections/era-phase}
\input{sections/era-output}
\input{sections/era-intervals}
\input{sections/era-branches}
\input{sections/era-successors}
\input{sections/era-selected-return}
\input{sections/era-tree-statistics}
\input{sections/era-original-time}
\input{sections/era-radial-families}
\section{Transport from a small physical section}
\label{sec:small-section-entrance}

The next three sections construct a return from a small transverse
section near Taub to the entrance graphs of
Theorem~\ref{thm:era-graph-statistics}. Where shear dominates the two
weak walls, varying the shear supplies a radial parameter. The return
must preserve a nonzero phase derivative, control the transverse
slopes, and leave only a small measure of parameters outside the
statistical set. The resulting statement is
Theorem~\ref{thm:common-shear-statistical-loss}, extended to both shear
signs in Proposition~\ref{prop:signed-shear-return}.

The two wall orderings require different waiting times. We first let
the dominant wall decay and follow the orbit through the remaining
core to the next entrance. For the other ordering, an additional slow
interval reduces the wall that would otherwise be too large.
Both constructions use the same transverse event on their overlap.
Their measure bounds will be integrated against section flux in
Section~\ref{sec:flux-and-capture}. The purpose of that integration
is capture: a set of finite flux cannot retain a positive measure of
recurrent points under a strictly expanding return.

Initial-data derivatives are taken in the ambient coordinate charts.
On closed parameter intervals they are the restrictions of derivatives
on the open neighborhoods supplied by the flow and transverse event
maps. Prescribed waiting times are held fixed when differentiating
at a fixed scale; derivatives of arrival times are included when an
endpoint is defined by an event.

\input{sections/small-section-transport}
\input{sections/small-section-nonlinear}
\input{sections/small-section-radial}
\input{sections/small-section-projection}
\section{From a remaining core to the next entrance}
\label{sec:remaining-core-entrance}

The section transport can end inside a core, or just before its upward
entrance. In both cases we follow the orbit to the same downward exit
and then to the next entrance. The estimates retain the moving initial
angle and the small wall product. They give the monotone phase and
transverse slope bounds used in
Theorem~\ref{thm:positive-shear-statistical-loss}, which establishes
statistical entrance families for positive shear with the second
weak wall sufficiently small.

\input{sections/small-section-partial-core}
\input{sections/partial-core-variation}
\input{sections/partial-core-multipliers}
\input{sections/partial-core-connection}
\input{sections/entrance-common-return}
\input{sections/entrance-radial-direction}
\input{sections/small-section-return-phase}
\input{sections/small-section-statistical-families}
\section{Slow passage and both weak-wall orderings}
\label{sec:slow-passage}

The other ordering of the weak walls can require a longer wait before
the next core. We first control the phase and its derivative during
this slow interval. The endpoint then enters the core construction
of Section~\ref{sec:remaining-core-entrance}.
Identifying the two returns on their overlap gives one entrance map
for both wall orderings. Reflection of the axes supplies the other
sign of shear. The final statistical estimate thus covers either
choice of the smaller wall, with constants independent of their ratio.

\input{sections/small-section-slow-decay}
\input{sections/small-section-slow-variation}
\input{sections/small-section-slow-radius}
\input{sections/small-section-delayed-projection}
\input{sections/small-section-delayed-directions}
\input{sections/small-section-delayed-entrance}
\input{sections/small-section-delayed-core}
\input{sections/small-section-delayed-return}
\input{sections/small-section-delayed-output}
\input{sections/small-section-common-return}
\input{sections/small-section-common-statistics}
\input{sections/small-section-signed-return}
\section{Section flux and capture}
\label{sec:flux-and-capture}

The statistical construction leaves an excluded set of finite section
flux. We choose a density for which every positive-time return strictly
increases flux. The recurrent points that stay excluded forever form
a set of finite flux, mapped injectively into itself by the first
return. Strict expansion forces this set to be null. This argument
gives the capture theorem below. We establish its ingredients first
in the region where shear dominates the weak walls.

\input{sections/small-section-flux}
\input{sections/small-section-finite-failure}
\input{sections/strict-volume-expansion}
\input{sections/arrival-flux-transport}
\input{sections/measurable-first-returns}
\input{sections/capture-by-expanding-returns}
\input{sections/small-section-shear-region}
\section{Angular directions and coverage of the section}
\label{sec:angular-coverage}

The shear families cover the region where both weak walls are small
compared with the shear. Near zero shear, we instead vary the larger
weak wall while fixing the ratio of shear to that wall. These angular
families retain a nonzero phase derivative at zero shear.
Their returns and flux estimates complete the coverage in
Theorem~\ref{thm:whole-small-section-statistics}.

\input{sections/angular-reference-phase}
\input{sections/angular-core-coordinates}
\input{sections/angular-projected-phase}
\input{sections/angular-remaining-core}
\input{sections/angular-actual-return}
\input{sections/angular-statistical-families}
\input{sections/angular-failure-flux}
\input{sections/whole-small-section}
\section{Recurrence and global era statistics}
\label{sec:global-era-statistics}

It remains to establish the recurrence required for capture and to make
one choice valid for all physical initial sections. Uniform avoidance
of Taub would force bounded era digits, a null possibility by the local
statistics. Deep Taub visits give repeated crossings of a fixed finite
section family. We combine these crossings with capture and then
transport a single exceptional set along the flow.

\input{sections/compact-phase-exclusion}
\input{sections/late-wall-entrance}
\input{sections/late-physical-core}
\input{sections/taub-recurrence-in-measure}
\input{sections/deep-taub-crossings}
\input{sections/recurrent-axis-sections}
\input{sections/measurable-statistical-entrances}
\input{sections/global-statistical-capture}
\input{sections/proof-of-statistical-theorem}
\section*{Acknowledgments}
OpenAI AI tools were used to explore possible proof strategies,
implement the Lean~4 formalization, and polish the manuscript.
During formalization, these tools suggested proof approaches that
facilitated formal verification. These approaches were incorporated
into the manuscript to keep the written and formalized proofs consistent.
The author checked the assumptions and conclusions of the formalization
and takes responsibility for both the manuscript and the formalized results.

\section*{Statements and Declarations}
\noindent\textbf{Funding.} No funding was received for this research.

\noindent\textbf{Competing interests.} The author has no relevant financial
or non-financial interests to disclose.

\section*{Data availability}
\label{sec:data-availability}
All mathematical results and proofs established in this article,
starting from the normalized vacuum Bianchi IX equations, have been
formalized in Lean~4. The formalization retains exactly two explicit
literature hypotheses: Birkhoff's pointwise ergodic theorem in its
probability-space form~\cite[Corollary~10.1.2]{Walkden}, and the decay
of curvature-wall products obtained from Brehm's attractor
theorems~\cite[Theorems~2--3, pp.~44--45]{Brehm}.
The complete source code and verification instructions are publicly
available at
\url{https://github.com/l46430640-del/ERA-STATISTICS-FORMAL}.
\input{references}
\end{document}