\section{Introduction}
\label{sec:introduction}

The vacuum Bianchi IX equations describe a spatially homogeneous universe
whose anisotropic geometry undergoes repeated transitions as a singularity
is approached. In the description of Belinskii, Khalatnikov and
Lifshitz~\cite{BKL}, these transitions are organized into eras. Each era
contains a finite number of epochs, and the succession of eras is governed
by continued fractions. The statistical theory developed by Khalatnikov,
Lifshitz, Khanin, Shchur and Sinai~\cite{KLKSS} predicts that the inverse
era parameter has density
\[
  \frac{1}{\log 2}\frac{1}{1+x},\qquad 0<x<1.
\]
Establishing this law for the differential equations requires control of
both individual trajectories and the measure of the initial data that
produce them.

We prove this statistical law for eras defined by transverse events of the
exact vacuum Bianchi IX flow. The exceptional initial data form one
invariant Borel set that is null on every smooth transverse section
and in the four-dimensional phase space.
The result includes the frequencies of all finite blocks of era lengths,
their tail distribution, and the divergence of their arithmetic mean.
Thus arbitrarily long eras occur along a typical trajectory, and their
contribution prevents the mean number of transitions per era from
settling to a finite value. Joint frequencies also retain correlations
between successive eras.
Theorem~\ref{thm:main} gives the precise statement after the event convention
has been specified.

The main difficulty occurs near the three Taub points of the Kasner
circle. An era may contain arbitrarily many transitions. The two small
curvature variables may have arbitrarily different sizes, and the time
between successive transitions need not remain bounded. Estimates on a
fixed compact part of the Kasner circle therefore do not control the
statistical problem. Moreover, closeness to the Mixmaster attractor does
not determine how initial volume is distributed among the possible
symbolic itineraries. Both issues enter the proof.

\subsection{Relation to earlier work}

Ringstr\"om's attractor theorem~\cite{Ringstrom} established the approach of
generic Bianchi IX solutions to the union of the vacuum type I and type II
states. Brehm~\cite{Brehm} developed estimates near the Taub spaces and
proved further results on attraction and particle horizons. We use the
consequence of his IX classification that every positive-wall solution
outside the Taub subspaces has vanishing pairwise curvature products.
This input is stated in Proposition~\ref{prop:attractor}.

The passage from attraction to asymptotic statistics has been articulated
by Heinzle and Uggla~\cite{HU}. Their formulation separates the dynamics
of the Kasner map from assertions about the exact Bianchi IX equations.
Liebscher, H\"arterich, Webster and Georgi~\cite{LHWG} constructed families
of solutions approaching a periodic heteroclinic cycle, with a method
extending to chains uniformly separated from the Taub points.
B\'eguin~\cite{Beguin} obtained nonperiodic shadowing families for
Kasner points in closed forward-invariant sets without periodic points.
Reiterer and Trubowitz~\cite{RT} treated chains with unbounded continued
fraction digits subject to a growth condition. B\'eguin and
Dutilleul~\cite{BD} subsequently obtained a precise geometric description
of shadowing families and proved that their union has positive
four-dimensional Lebesgue measure. Their Theorems~1.5 and~1.9 establish
this measure statement for unions of shadowing families over sets of
Kasner parameters of positive measure.

Our result determines era statistics on a set of full transverse measure
in the exact IX phase space. The proof estimates the distribution of
actual era itineraries directly. The local comparison with continued
fractions is combined with a global argument that brings almost every
orbit into a statistical set on a fixed section. This also makes it
possible to choose the exceptional set independently of the initial
section and the observation function.

The sampling convention matters. Damour and Lecian~\cite{DL} analyze
invariant measures and correlations for cosmological billiards, including
the effects of retaining or identifying the spatial axis labels. Here each
era receives equal weight, and the recorded scalar quantities are
unchanged by an overall renaming of the axes. We define these quantities
at specified crossings of the exact solution, so the statistical
statement includes the existence and ordering of the events being counted.

\subsection{The mechanism of the proof}

The proof has three main tasks: transfer Gauss statistics to perturbed
returns, construct complete era returns with estimates uniform near
Taub, and bring almost every initial condition into their statistical
domain. The first task separates comparison of observations from
control of the measure of initial data.

For the comparison, if an era has length
$k$ and terminal phase $y$, its initial phase is close to
$g_k(y)=(k+y)^{-1}$. Two consecutive ideal inverse branches contract by at
least a factor of four. Consequently, an error tending to zero in the
inverse recurrence produces an asymptotically identical Gauss orbit.
Section~\ref{sec:comparison} establishes this comparison while keeping the
digits fixed. Continuous observations can then be transferred without
crossing the discontinuities of the forward Gauss map.

To control the measure of the coding, we use suitable curves
of small transverse amplitude. The exact era branches have summable
distortion and summable losses of parameter length. For every finite word,
the measure of the initial points carrying that word is bounded by a
constant times the length of its Gauss cylinder. This bound passes to
Borel sets of codes and makes the coding measure absolutely continuous.
Birkhoff's theorem, first applied to the countable family of cylinders,
then supplies one typical set for all the desired observations.
Sections~\ref{sec:gauss-statistics} and~\ref{sec:coding-measure} develop
these measure estimates and the statistical transfer.

Sections~\ref{sec:curvature-cores}--\ref{sec:terminal-connections}
give the local estimates. They are organized around the loss of
transverse amplitude through each curvature core.
That loss controls the phase error and its derivative. Summing the losses
over an era avoids a bound that grows with the number of cores. A
terminal connection produces a smaller amplitude for the next era, so
the estimates can be iterated even when the era lengths are unbounded.
Section~\ref{sec:complete-era-returns} combines the passages into actual
era returns and applies the statistical transfer.

To reach general initial data, we use radial families on small sections
near the Taub points, constructed in
Sections~\ref{sec:small-section-entrance}--\ref{sec:slow-passage}.
Their returns reach the local statistical construction. Angular families
complete the coverage near zero shear in
Section~\ref{sec:angular-coverage}. The points left outside these
entrance selections have finite flux for a density equivalent to the
natural section density. The first return strictly increases this flux.
Section~\ref{sec:flux-and-capture} proves that almost every recurrent
point eventually leaves the excluded set.

Recurrence follows from a separate use of the local statistics.
They exclude almost every trajectory that eventually stays away from
all Taub points. The attractor input and deep Taub visits then give the
section crossings needed for capture. Transport of the resulting null
sets along the flow produces one invariant exceptional set, valid on
every transverse section. These global steps and the final
proof of Theorem~\ref{thm:main} occupy
Section~\ref{sec:global-era-statistics}.

All results and proofs in this article have been formalized in Lean~4;
see \hyperref[sec:data-availability]{\textcolor{blue}{Data availability}}.