Prove2Me

Survivor states, physical arrival schedules and complete era sequences

Definition
BianchiIX_PhysicalEraData

by trppppp · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

bianchi-ix-era-statisticsdynamical-systems

For real variables p,s,a,b,cp,s,a,b,c, set

K=a2+b2+c2−2(ab+bc+ca),S=p2+s2,C=S+K.K=a^2+b^2+c^2-2(ab+bc+ca),\qquad S=p^2+s^2,\qquad C=S+K.

The shear components and wall rates are

P=Kp−2a2+b2+c2+ab−2bc+ac,P=Kp-2a^2+b^2+c^2+ab-2bc+ac, Q=Ks+3(−b2+c2+ab−ac),Q=Ks+\sqrt{3}(-b^2+c^2+ab-ac), r1=−S+2p,r2=−S−p+3s,r3=−S−p−3s.r_1=-S+2p,\qquad r_2=-S-p+\sqrt{3}s,\qquad r_3=-S-p-\sqrt{3}s.

These functions define the normalized vacuum Bianchi IX vector field (P,Q,r1a,r2b,r3c)(P,Q,r_1a,r_2b,r_3c). For y=(m,u,v,w)∈R4y=(m,u,v,w)\in\mathbb R^4, define

K(u,v,w)=u2+v2+w2−2(uv+vw+wu),κ=u(v+w−u),K(u,v,w)=u^2+v^2+w^2-2(uv+vw+wu),\qquad \kappa=u(v+w-u), Fm=−v2+w2+u(v−w)−mκ,Fu=12(1−m2−(v−w)2+u2)u,F_m=-v^2+w^2+u(v-w)-m\kappa,\qquad F_u=\tfrac12(1-m^2-(v-w)^2+u^2)u, Fv=(m−1−κ)v,Fw=(−m−1−κ)w,F=(Fm,Fu,Fv,Fw),F_v=(m-1-\kappa)v,\qquad F_w=(-m-1-\kappa)w,\qquad F=(F_m,F_u,F_v,F_w),

and E(m,v)=(m−1)2+v2E(m,v)=(m-1)^2+v^2.

For x=(p,s,a,b,c)x=(p,s,a,b,c), put

ψ(p,z)=3 z1+p,Π(x)=(ψ(p,s),ψ(p,a),ψ(p,b),ψ(p,c)).\psi(p,z)=\frac{\sqrt3\,z}{1+p},\qquad \Pi(x)=(\psi(p,s),\psi(p,a),\psi(p,b),\psi(p,c)).

For y=(m,u,v,w)y=(m,u,v,w), set D(y)=3+m2+K(u,v,w)D(y)=3+m^2+K(u,v,w) and

ΞA(y)=(A−1,Am3,Au3,Av3,Aw3),Ξ(y)=Ξ6/D(y)(y).\Xi_A(y)=\left(A-1,\frac{Am}{\sqrt3},\frac{Au}{\sqrt3}, \frac{Av}{\sqrt3},\frac{Aw}{\sqrt3}\right),\qquad \Xi(y)=\Xi_{6/D(y)}(y).

Write N(x)=(P,Q,r1a,r2b,r3c)N(x)=(P,Q,r_1a,r_2b,r_3c) for the normalized vector field and C(x)=C(p,s,a,b,c)\mathcal C(x)=C(p,s,a,b,c) for its constraint.

The normalized and projective state spaces are R5\mathbb R^5 and R4\mathbb R^4 with their finite-product norms. The maps Π,Ξ,D,F\Pi,\Xi,D,F act on these state spaces.

Define the core radius, angle, and clock factor by

r(m,v)=(m−1)2+v2,θ(m,v)=arsinh⁡1−mv,d(r,u,w)=1−(u−w)2r2.r(m,v)=\sqrt{(m-1)^2+v^2},\qquad \theta(m,v)=\operatorname{arsinh}\frac{1-m}{v},\qquad d(r,u,w)=1-\frac{(u-w)^2}{r^2}.

For y=(m,u,v,w)y=(m,u,v,w), write ry=r(m,v)r_y=r(m,v), θy=θ(m,v)\theta_y=\theta(m,v), and dy=d(ry,u,w)d_y=d(r_y,u,w). All quotients use the total convention x/0=0x/0=0.

The core state space is R3\mathbb R^3 with coordinates Y=(r,u,p)Y=(r,u,p). Define

η(m,u,v,w)=(r(m,v),u,vw),ιz(r,u,p)=(1−rtanh⁡z,u,rcosh⁡z,pr/cosh⁡z).\eta(m,u,v,w)=(r(m,v),u,vw),\qquad \iota_z(r,u,p)=\left(1-r\tanh z,u,\frac r{\cosh z}, \frac p{r/\cosh z}\right).

For fixed (z,Y)(z,Y) put v=r/cosh⁡zv=r/\cosh z, w=p/vw=p/v, d=d(r,u,w)d=d(r,u,w), and define

V(z,Y)=(−κ(u,v,w)−tanh⁡z (u−w)2/rd,u[−r/2+tanh⁡z+w/cosh⁡z+(u2−w2)/(2r)]d,−2p(1+κ(u,v,w))rd).\mathcal V(z,Y)=\left( \frac{-\kappa(u,v,w)-\tanh z\,(u-w)^2/r}{d},\quad \frac{u[-r/2+\tanh z+w/\cosh z+(u^2-w^2)/(2r)]}{d},\quad \frac{-2p(1+\kappa(u,v,w))}{rd}\right).

For real kk, put εk=1/(10000k)\varepsilon_k=1/(10000k) and define

Kk={(m,u,v,w):∣E(m,v)−k2∣≤1/8,v≥1,0≤u≤εk,0≤vw≤εk}.\mathcal K_k=\{(m,u,v,w): |E(m,v)-k^2|\leq1/8,\quad v\geq1, \quad0\leq u\leq\varepsilon_k,\quad0\leq vw\leq\varepsilon_k\}.

Write X=R5X=\mathbb R^5, Y=R4Y=\mathbb R^4, and let αx,t0\alpha_{x,t_0} be the maximal solution of α′=N(α)\alpha'=N(\alpha) with initial value xx at t0t_0 and domain Imax⁡(x,t0)I_{\max}(x,t_0). Put

Jx,t0(t)=dxαx,t0(t),Ψt0(y,t)=Π(αΞ(y),t0(t)),J_{x,t_0}(t)=d_x\alpha_{x,t_0}(t),\qquad \Psi_{t_0}(y,t)=\Pi(\alpha_{\Xi(y),t_0}(t)), Jy,t0(t)=dΠαΞ(y),t0(t)∘JΞ(y),t0(t)∘dΞy.\mathcal J_{y,t_0}(t)=d\Pi_{\alpha_{\Xi(y),t_0}(t)} \circ J_{\Xi(y),t_0}(t)\circ d\Xi_y.

Write G(y)=6F(y)/D(y)G(y)=6F(y)/D(y), λ(y)=6rydy/D(y)\lambda(y)=6r_yd_y/D(y), and Sk(R,U,P)=(R,kU,P)S_k(R,U,P)=(R,kU,P). Define

Pyξ=dηyξ−dθyξ V(θy,η(y)),Wy,t0,w(t)=PΨt0(y,t)(Jy,t0(t)w).\mathcal P_y\xi=d\eta_y\xi-d\theta_y\xi\,\mathcal V(\theta_y,\eta(y)), \qquad \mathcal W_{y,t_0,w}(t)= \mathcal P_{\Psi_{t_0}(y,t)}(\mathcal J_{y,t_0}(t)w).

The entrance parametrization and radial exit factor are

e(k,u,w)=(1+k2−1,u,1,w),e(k,u,w)=(1+\sqrt{k^2-1},u,1,w), fy=V(θy,η(y))0,cy=−tanh⁡θy,hy=cy+fy/ry,ρy=cy/hy.f_y=\mathcal V(\theta_y,\eta(y))_0,\qquad c_y=-\tanh\theta_y, \qquad h_y=c_y+f_y/r_y,\qquad \rho_y=c_y/h_y.

For projective initial data yy, put

Ay,t0(t)=1+(αΞ(y),t0(t))0.A_{y,t_0}(t)=1+(\alpha_{\Xi(y),t_0}(t))_0.

Coordinates of three-vectors are indexed by 0,1,20,1,2; projective coordinates are indexed by m,u,v,wm,u,v,w.

For Y∈R3Y\in\mathbb R^3, put xY=Ξ(e(Y))x_Y=\Xi(e(Y)), βY(t)=Ψ0(e(Y),t)\beta_Y(t)=\Psi_0(e(Y),t), and

HY={t>0:t∈Imax⁡(xY,0), (βY(t))v=1},T(Y)=inf⁡HY,F(Y)=η(βY(T(Y))).H_Y=\{t>0:t\in I_{\max}(x_Y,0),\ (\beta_Y(t))_v=1\}, \qquad T(Y)=\inf H_Y,\qquad F(Y)=\eta(\beta_Y(T(Y))).

The infimum uses the total real-order convention. Write Valid⁡(Y)\operatorname{Valid}(Y) when T(Y)T(Y) is the least element of HYH_Y, every t∈[0,T(Y)]t\in[0,T(Y)] lies in Imax⁡(xY,0)I_{\max}(x_Y,0) with Ae(Y),0(t)>0A_{e(Y),0}(t)>0, the active wall is strictly above one for 0<t<T(Y)0<t<T(Y), and

dgαxY,0(T(Y))N(αxY,0(T(Y)))<0,g(x)=(Π(x))v.dg_{\alpha_{x_Y,0}(T(Y))}N(\alpha_{x_Y,0}(T(Y)))<0, \qquad g(x)=(\Pi(x))_v.

All vector and operator norms below use the finite-product supremum norm. For real variables p,s,a,b,cp,s,a,b,c, set

K=a2+b2+c2−2(ab+bc+ca),S=p2+s2,C=S+K.K=a^2+b^2+c^2-2(ab+bc+ca),\qquad S=p^2+s^2,\qquad C=S+K.

The shear components and wall rates are

P=Kp−2a2+b2+c2+ab−2bc+ac,P=Kp-2a^2+b^2+c^2+ab-2bc+ac, Q=Ks+3(−b2+c2+ab−ac),Q=Ks+\sqrt{3}(-b^2+c^2+ab-ac), r1=−S+2p,r2=−S−p+3s,r3=−S−p−3s.r_1=-S+2p,\qquad r_2=-S-p+\sqrt{3}s,\qquad r_3=-S-p-\sqrt{3}s.

These functions define the normalized vacuum Bianchi IX vector field (P,Q,r1a,r2b,r3c)(P,Q,r_1a,r_2b,r_3c). For y=(m,u,v,w)∈R4y=(m,u,v,w)\in\mathbb R^4, define

K(u,v,w)=u2+v2+w2−2(uv+vw+wu),κ=u(v+w−u),K(u,v,w)=u^2+v^2+w^2-2(uv+vw+wu),\qquad \kappa=u(v+w-u), Fm=−v2+w2+u(v−w)−mκ,Fu=12(1−m2−(v−w)2+u2)u,F_m=-v^2+w^2+u(v-w)-m\kappa,\qquad F_u=\tfrac12(1-m^2-(v-w)^2+u^2)u, Fv=(m−1−κ)v,Fw=(−m−1−κ)w,F=(Fm,Fu,Fv,Fw),F_v=(m-1-\kappa)v,\qquad F_w=(-m-1-\kappa)w,\qquad F=(F_m,F_u,F_v,F_w),

and E(m,v)=(m−1)2+v2E(m,v)=(m-1)^2+v^2.

For x=(p,s,a,b,c)x=(p,s,a,b,c), put

ψ(p,z)=3 z1+p,Π(x)=(ψ(p,s),ψ(p,a),ψ(p,b),ψ(p,c)).\psi(p,z)=\frac{\sqrt3\,z}{1+p},\qquad \Pi(x)=(\psi(p,s),\psi(p,a),\psi(p,b),\psi(p,c)).

For y=(m,u,v,w)y=(m,u,v,w), set D(y)=3+m2+K(u,v,w)D(y)=3+m^2+K(u,v,w) and

ΞA(y)=(A−1,Am3,Au3,Av3,Aw3),Ξ(y)=Ξ6/D(y)(y).\Xi_A(y)=\left(A-1,\frac{Am}{\sqrt3},\frac{Au}{\sqrt3}, \frac{Av}{\sqrt3},\frac{Aw}{\sqrt3}\right),\qquad \Xi(y)=\Xi_{6/D(y)}(y).

Write N(x)=(P,Q,r1a,r2b,r3c)N(x)=(P,Q,r_1a,r_2b,r_3c) for the normalized vector field and C(x)=C(p,s,a,b,c)\mathcal C(x)=C(p,s,a,b,c) for its constraint.

The normalized and projective state spaces are R5\mathbb R^5 and R4\mathbb R^4 with their finite-product norms. The maps Π,Ξ,D,F\Pi,\Xi,D,F act on these state spaces.

The projective vector field in normalized time is

G(y)=6D(y)F(y).G(y)=\frac6{D(y)}F(y).

Write X=R5X=\mathbb R^5, Y=R4Y=\mathbb R^4, and let αx,t0\alpha_{x,t_0} be the maximal solution of α′=N(α)\alpha'=N(\alpha) with initial value xx at t0t_0 and domain Imax⁡(x,t0)I_{\max}(x,t_0). Put

Jx,t0(t)=dxαx,t0(t),Ψt0(y,t)=Π(αΞ(y),t0(t)),J_{x,t_0}(t)=d_x\alpha_{x,t_0}(t),\qquad \Psi_{t_0}(y,t)=\Pi(\alpha_{\Xi(y),t_0}(t)), Jy,t0(t)=dΠαΞ(y),t0(t)∘JΞ(y),t0(t)∘dΞy.\mathcal J_{y,t_0}(t)=d\Pi_{\alpha_{\Xi(y),t_0}(t)} \circ J_{\Xi(y),t_0}(t)\circ d\Xi_y.

Put c=u(v+w−u)c=u(v+w-u), s(m,u,v,w)=m−1−cs(m,u,v,w)=m-1-c, b(m,u,v,w)=(1−m2−(v−w)2+u2)/2b(m,u,v,w)=(1-m^2-(v-w)^2+u^2)/2, D(m,u,v,w)=3+m2+K(u,v,w)D(m,u,v,w)=3+m^2+K(u,v,w), and r(m,v)=(m−1)2+v2r(m,v)=\sqrt{(m-1)^2+v^2}.

Define

Cμ={(m,u,v,w):∣−m−μ∣≤1/2, 0≤u≤1/10000, 0≤v,w≤1},\mathcal C_\mu=\{(m,u,v,w):|-m-\mu|\leq1/2, \ 0\leq u\leq1/10000,\ 0\leq v,w\leq1\}, ω−(y)=s(−ym,yu,yv,yw),H(y)=F(y)/ω−(y).\omega_-(y)=s(-y_m,y_u,y_v,y_w),\qquad H(y)=F(y)/\omega_-(y).

For a normalized trajectory write

β(t)=Π(αx,t0(t)),A(t)=1+(αx,t0(t))0,I=Imax⁡(x,t0).\beta(t)=\Pi(\alpha_{x,t_0}(t)),\quad A(t)=1+(\alpha_{x,t_0}(t))_0, \quad I=I_{\max}(x,t_0).

For p=(μ,u,w)∈R3p=(\mu,u,w)\in\mathbb R^3, set e(p)=(−μ,u,1,w)e(p)=(-\mu,u,1,w), xp=Ξ(e(p))x_p=\Xi(e(p)), and

T−(p)=inf⁡{t>0:t∈Imax⁡(xp,0), (Ψ0(e(p),t))w=1},P−(p)=Ψ0(e(p),T−(p)).T_-(p)=\inf\{t>0:t\in I_{\max}(x_p,0),\ (\Psi_0(e(p),t))_w=1\}, \qquad P_-(p)=\Psi_0(e(p),T_-(p)).

Let V−(p)V_-(p) mean that this infimum is a least element, the full interval [0,T−(p)][0,T_-(p)] lies in the maximal domain with positive AA, the growing wall is below one before the endpoint, and its normalized-time derivative is strictly positive at the endpoint. The infimum has its total real-order meaning.

Write e+(R,u,w)=(1+R2−1,u,1,w)e_+(R,u,w)=(1+\sqrt{R^2-1},u,1,w), e−(R,u,w)=(1−R2−1,u,1,w)e_-(R,u,w)=(1-\sqrt{R^2-1},u,1,w), p−(R,u,w)=(R2−1−1,u,w)p_-(R,u,w)=(\sqrt{R^2-1}-1,u,w), and R(m,u,v,w)=(−m,u,w,v)\mathcal R(m,u,v,w)=(-m,u,w,v). The physical connection coordinates are

C(p)=((−P−(p)0−1)2+1,P−(p)1,P−(p)2).\mathscr C(p)=\left(\sqrt{(-P_-(p)_0-1)^2+1},P_-(p)_1,P_-(p)_2\right).

Below TT denotes the canonical core return time from e+e_+ and F(Y)=η(Ψ0(e+(Y),T(Y)))F(Y)=\eta(\Psi_0(e_+(Y),T(Y))) its radial and wall coordinates. Let R(Y)=C(p−(Y))\mathscr R(Y)=\mathscr C(p_-(Y)), tr(Y)=T−(p−(Y))t_r(Y)=T_-(p_-(Y)), G=R∘FG=\mathscr R\circ F, and tG(Y)=T(Y)+tr(F(Y))t_G(Y)=T(Y)+t_r(F(Y)). A cone direction at YY has d0=1d_0=1, ∣d1∣≤Y1|d_1|\leq\sqrt{Y_1}, ∣d2∣≤Y2|d_2|\leq\sqrt{Y_2}. For a map HH with positive output walls, its positive cone property means dH(Y)ddH(Y)d has positive radial component and ∣(dH(Y)d)i∣≤H(Y)i(dH(Y)d)0|(dH(Y)d)_i|\leq\sqrt{H(Y)_i}(dH(Y)d)_0 for i=1,2i=1,2. For real variables p,s,a,b,cp,s,a,b,c, set

K=a2+b2+c2−2(ab+bc+ca),S=p2+s2,C=S+K.K=a^2+b^2+c^2-2(ab+bc+ca),\qquad S=p^2+s^2,\qquad C=S+K.

The shear components and wall rates are

P=Kp−2a2+b2+c2+ab−2bc+ac,P=Kp-2a^2+b^2+c^2+ab-2bc+ac, Q=Ks+3(−b2+c2+ab−ac),Q=Ks+\sqrt{3}(-b^2+c^2+ab-ac), r1=−S+2p,r2=−S−p+3s,r3=−S−p−3s.r_1=-S+2p,\qquad r_2=-S-p+\sqrt{3}s,\qquad r_3=-S-p-\sqrt{3}s.

These functions define the normalized vacuum Bianchi IX vector field (P,Q,r1a,r2b,r3c)(P,Q,r_1a,r_2b,r_3c). For y=(m,u,v,w)∈R4y=(m,u,v,w)\in\mathbb R^4, define

K(u,v,w)=u2+v2+w2−2(uv+vw+wu),κ=u(v+w−u),K(u,v,w)=u^2+v^2+w^2-2(uv+vw+wu),\qquad \kappa=u(v+w-u), Fm=−v2+w2+u(v−w)−mκ,Fu=12(1−m2−(v−w)2+u2)u,F_m=-v^2+w^2+u(v-w)-m\kappa,\qquad F_u=\tfrac12(1-m^2-(v-w)^2+u^2)u, Fv=(m−1−κ)v,Fw=(−m−1−κ)w,F=(Fm,Fu,Fv,Fw),F_v=(m-1-\kappa)v,\qquad F_w=(-m-1-\kappa)w,\qquad F=(F_m,F_u,F_v,F_w),

and E(m,v)=(m−1)2+v2E(m,v)=(m-1)^2+v^2.

For x=(p,s,a,b,c)x=(p,s,a,b,c), put

ψ(p,z)=3 z1+p,Π(x)=(ψ(p,s),ψ(p,a),ψ(p,b),ψ(p,c)).\psi(p,z)=\frac{\sqrt3\,z}{1+p},\qquad \Pi(x)=(\psi(p,s),\psi(p,a),\psi(p,b),\psi(p,c)).

For y=(m,u,v,w)y=(m,u,v,w), set D(y)=3+m2+K(u,v,w)D(y)=3+m^2+K(u,v,w) and

ΞA(y)=(A−1,Am3,Au3,Av3,Aw3),Ξ(y)=Ξ6/D(y)(y).\Xi_A(y)=\left(A-1,\frac{Am}{\sqrt3},\frac{Au}{\sqrt3}, \frac{Av}{\sqrt3},\frac{Aw}{\sqrt3}\right),\qquad \Xi(y)=\Xi_{6/D(y)}(y).

Write N(x)=(P,Q,r1a,r2b,r3c)N(x)=(P,Q,r_1a,r_2b,r_3c) for the normalized vector field and C(x)=C(p,s,a,b,c)\mathcal C(x)=C(p,s,a,b,c) for its constraint.

The normalized and projective state spaces are R5\mathbb R^5 and R4\mathbb R^4 with their finite-product norms. The maps Π,Ξ,D,F\Pi,\Xi,D,F act on these state spaces.

The projective vector field in normalized time is

G(y)=6D(y)F(y).G(y)=\frac6{D(y)}F(y).

Write X=R5X=\mathbb R^5, Y=R4Y=\mathbb R^4, and let αx,t0\alpha_{x,t_0} be the maximal solution of α′=N(α)\alpha'=N(\alpha) with initial value xx at t0t_0 and domain Imax⁡(x,t0)I_{\max}(x,t_0). Put

Jx,t0(t)=dxαx,t0(t),Ψt0(y,t)=Π(αΞ(y),t0(t)),J_{x,t_0}(t)=d_x\alpha_{x,t_0}(t),\qquad \Psi_{t_0}(y,t)=\Pi(\alpha_{\Xi(y),t_0}(t)), Jy,t0(t)=dΠαΞ(y),t0(t)∘JΞ(y),t0(t)∘dΞy.\mathcal J_{y,t_0}(t)=d\Pi_{\alpha_{\Xi(y),t_0}(t)} \circ J_{\Xi(y),t_0}(t)\circ d\Xi_y.

For Y=(k,u,w)∈R3Y=(k,u,w)\in\mathbb R^3, define

e−(Y)=(1−k2−1,u,1,w),xY=Ξ(e−(Y)),βY(t)=Ψ0(e−(Y),t),g(x)=(Π(x))v.e_-(Y)=(1-\sqrt{k^2-1},u,1,w),\quad x_Y=\Xi(e_-(Y)),\quad \beta_Y(t)=\Psi_0(e_-(Y),t),\quad g(x)=(\Pi(x))_v.

For any real height η\eta, put

Hη,Y={t>0:t∈Imax⁡(xY,0), g(αxY,0(t))=η},H_{\eta,Y}=\{t>0:t\in I_{\max}(x_Y,0),\ g(\alpha_{x_Y,0}(t))=\eta\}, Tη(Y)=inf⁡Hη,Y,Pη(Y)=βY(Tη(Y)).T_\eta(Y)=\inf H_{\eta,Y},\qquad P_\eta(Y)=\beta_Y(T_\eta(Y)).

The infimum uses the total real-order convention. Let TailValid⁡η(Y)\operatorname{TailValid}_\eta(Y) mean that Tη(Y)T_\eta(Y) is the least element of Hη,YH_{\eta,Y}, and, writing T=Tη(Y)T=T_\eta(Y), that

t∈Imax⁡(xY,0),1+(αxY,0(t))0>0(0≤t≤T),t\in I_{\max}(x_Y,0),\quad 1+(\alpha_{x_Y,0}(t))_0>0 \quad(0\leq t\leq T), g(αxY,0(t))>η(0≤t<T),g(\alpha_{x_Y,0}(t))>\eta\quad(0\leq t<T), dgαxY,0(t)N(αxY,0(t))<0,∣(Π(αxY,0(t)))w∣<1/2(0≤t≤T).dg_{\alpha_{x_Y,0}(t)}N(\alpha_{x_Y,0}(t))<0,\quad |(\Pi(\alpha_{x_Y,0}(t)))_w|<1/2\quad(0\leq t\leq T).

All vector and operator norms use the finite-product supremum norms.

For y∈R4y\in\mathbb R^4, put xy=Ξ(y)x_y=\Xi(y),

T+(y)=inf⁡{t>0:t∈Imax⁡(xy,0), (Ψ0(y,t))v=1},P+(y)=Ψ0(y,T+(y)).T_+(y)=\inf\{t>0:t\in I_{\max}(x_y,0),\ (\Psi_0(y,t))_v=1\}, \qquad P_+(y)=\Psi_0(y,T_+(y)).

Let V+(y)V_+(y) mean that this infimum is a least element, the full interval [0,T+(y)][0,T_+(y)] lies in the maximal domain with 1+(αxy,0(t))0>01+(\alpha_{x_y,0}(t))_0>0, the active wall is below one before the endpoint, and its normalized-time derivative is strictly positive throughout the interval. The infimum has its total real-order meaning.

For y=(m,u,v,w)y=(m,u,v,w) define the cyclic chart by

H(y)=(m+1)2+K(u,v,w),A(y)=(1−4(m+1)/H,4v/H,4w/H,4u/H).H(y)=(m+1)^2+K(u,v,w),\qquad \mathcal A(y)=(1-4(m+1)/H,4v/H,4w/H,4u/H).

Its normalized symmetry is

A(p,s,a,b,c)=((−p+3s)/2,(−3p−s)/2,b,c,a).A(p,s,a,b,c)=((-p+\sqrt3s)/2,(-\sqrt3p-s)/2,b,c,a).

Put zh(Y)=A(Ph(Y))z_h(Y)=\mathcal A(P_h(Y)) and

T(h,Y)=Th(Y)+T+(zh(Y)),P(h,Y)=P+(zh(Y)),xYc=AΞ(e−(Y)).\mathcal T(h,Y)=T_h(Y)+T_+(z_h(Y)),\qquad \mathcal P(h,Y)=P_+(z_h(Y)),\qquad x_Y^c=A\Xi(e_-(Y)).

Write r(m,v)=(m−1)2+v2r(m,v)=\sqrt{(m-1)^2+v^2} and g∗(x)=(Π(x))vg_*(x)=(\Pi(x))_v.

In the era formulas below, FF denotes the core return map and G=R∘FG=\mathscr R\circ F its composition with reflection. For Z=(R,u,w)Z=(R,u,w) use the natural height h∗(Z)=η((R−2)/2)Jh_*(Z)=\eta((R-2)/2)^J and define S∗(Z)=P(h∗(Z),Z)S_*(Z)=\mathcal P(h_*(Z),Z), R∗(Z)=r(S∗(Z)0,S∗(Z)2)R_*(Z)=r(S_*(Z)_0,S_*(Z)_2), Q∗(Z)=2/R∗(Z)Q_*(Z)=2/R_*(Z) and t∗(Z)=T(h∗(Z),Z)t_*(Z)=\mathcal T(h_*(Z),Z). The complete era maps are

Zm=F∘Gm,Sm=S∗∘Zm,Rm=R∗∘Zm,Pm=2/Rm.Z_m=F\circ G^m,\qquad S_m=S_*\circ Z_m,\qquad R_m=R_*\circ Z_m,\qquad P_m=2/R_m.

For a graph Γ=(U,W)\Gamma=(U,W) write Γ[r]=(r,U(r),W(r))\Gamma[r]=(r,U(r),W(r)), ϕm(r)=Pm(Γ[r])\phi_m(r)=P_m(\Gamma[r]), km(r)=Rm(Γ[r])k_m(r)=R_m(\Gamma[r]), um(r)=Sm(Γ[r])1u_m(r)=S_m(\Gamma[r])_1, wm(r)=Sm(Γ[r])3w_m(r)=S_m(\Gamma[r])_3. Let Inv⁡a,b(f)\operatorname{Inv}_{a,b}(f) denote Lean's total choice inverse invFunOn⁡f [a,b]\operatorname{invFunOn}f\,[a,b]. For a=2(m+1+β)a=2(m+1+\beta), b=2(m+2−β)b=2(m+2-\beta), define

gm=Inv⁡a,b(ϕm),hm(y)=2/gm(y).g_m=\operatorname{Inv}_{a,b}(\phi_m),\qquad h_m(y)=2/g_m(y).

Write γn(y)=1/(n+y)\gamma_n(y)=1/(n+y) for the Gauss inverse branch. The retained phase set is HN=⋃m<N(hm(1−2β),hm(2β))\mathcal H_N=\bigcup_{m<N}(h_m(1-2\beta),h_m(2\beta)).

Write x(Y)=Ξ(e+(Y))x(Y)=\Xi(e_+(Y)), Φts(x)=αx,s(t)\Phi^s_t(x)=\alpha_{x,s}(t) and I(x,s)I(x,s) for its maximal domain. Set Yj=GjXY_j=G^jX, Z=F(Ym)Z=F(Y_m), Nm(X)=(Rm(X),Sm(X)1,Sm(X)3)N_m(X)=(R_m(X),S_m(X)_1,S_m(X)_3), and

dm(X)=∑j<mtG(Yj)+T(Ym)+t∗(Z).d_m(X)=\sum_{j<m}t_G(Y_j)+T(Y_m)+t_*(Z).

The six axis frames realize all permutations of the normalized walls and diagonal shears. Write LmL_m for the frame obtained by mm swaps followed by the cyclic permutation. The event itinerary Im(X)\mathcal I_m(X) has the following meaning. For j≤mj\le m, the radius of YjY_j exceeds two, the entry is an upward unit-wall crossing, its core first return is valid, and its endpoint is e−(F(Yj))e_-(F(Y_j)). For j<mj<m the exit radius exceeds four, and the first positive unit-wall hit in the swapped chart reaches e+(Yj+1)e_+(Y_{j+1}), the reflection of the endpoint at time tG(Yj)t_G(Y_j). The final exit has radius strictly between two and four. In the cycled exit chart its first positive unit-wall hit occurs at t∗(Z)t_*(Z), has state S∗(Z)S_*(Z) and positive event rate. Finally ⌊X0/2⌋=m+1\lfloor X_0/2\rfloor=m+1.

For a budget cap bb define Am(b)A_m(b) by the conditions on (B,X)(B,X)

0<B≤b,m<⌊B−σ⌋,X1,X2>0,X1+X2≤B,m+1+Bσ≤X0/2≤m+2−Bσ.0<B\le b,\quad m<\lfloor B^{-\sigma}\rfloor,\quad X_1,X_2>0,\quad X_1+X_2\le B,\quad m+1+B^\sigma\le X_0/2\le m+2-B^\sigma.

The selected domain Dm(b)D_m(b) additionally requires 2Bσ<Pm(X)<1−2Bσ2B^\sigma<P_m(X)<1-2B^\sigma; the budget return is Fm(B,X)=(B4/3,Nm(X))\mathcal F_m(B,X)=(B^{4/3},N_m(X)). In a small-budget assertion there exists 0<δ≤1/400000<\delta\le1/40000 such that for every 0<η≤δ0<\eta\le\delta, J∈NJ\in\mathbb N with J≥20J\ge20, 0<σ<10<\sigma<1 and 2Jσ<12J\sigma<1, the stated constants can be chosen.

Let pp be a budget and core state surviving all selected returns at cap bb. Its successive digits are ana_n, its transported states are XnX_n, its phases are yn=2/(Xn)0y_n=2/(X_n)_0, and mn=an−1m_n=a_n-1. Put

dn=dmn(Xn),sn=∑j<ndj,A0=1,An+1=LmnAn.d_n=d_{m_n}(X_n),\qquad s_n=\sum_{j<n}d_j,\qquad A_0=1,\quad A_{n+1}=L_{m_n}A_n.

Frame indices use the chosen composition on the six labels. For restart data w=((i,s),(B,X))w=((i,s),(B,X)), let tn=s+snt_n=s+s_n and let PnP_n denote the frame with index chosen for AnQiA_n Q_i, where QiQ_i is the initial frame of label ii. A restart witness for xx requires s>0s>0, s∈I(x,0)s\in I(x,0) and a survivor with initial data (B,X)(B,X), full era statistics, and entry e+(X)=Π(QiΦs0(x))e_+(X)=\Pi(Q_i\Phi^0_s(x)).

A physical era sequence consists of complete event blocks on a single constraint-one orbit with the stated statistics, increasing positive times tending to infinity, matching next states, times and frames, and an actual preceding block ending at its first entrance.

Definition code
import Definitions.Def_BianchiIX_Dynamics_CoreAngle
import Definitions.Def_BianchiIX_EraCodingData
import Mathlib.Analysis.Calculus.ParametricIntervalIntegral
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Topology.Order.Compact
import Mathlib.MeasureTheory.Integral.DominatedConvergence
import Mathlib.Data.Fin.VecNotation
import Mathlib.Analysis.Calculus.Deriv.Pi
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Analysis.Calculus.ImplicitContDiff
import Mathlib.Tactic.NormNum
import Mathlib.Analysis.Calculus.Deriv.Pow
import Mathlib.Analysis.Calculus.Deriv.Mul
import Mathlib.Analysis.Calculus.Deriv.Add
import Mathlib.Analysis.Real.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.FunProp
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
import Mathlib.Tactic.FieldSimp
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.Analysis.ODE.ExistUnique
import Mathlib.Analysis.Calculus.FDeriv.Partial
import Mathlib.Topology.Order.IntermediateValue
import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.Deriv.Inv
import Mathlib.Tactic.LinearCombination
import Mathlib.Analysis.SpecialFunctions.Arcosh
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
import Mathlib.Analysis.Calculus.Deriv.MeanValue
import Mathlib.Tactic.Module
import Mathlib.Analysis.SpecialFunctions.Arsinh
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Data.Matrix.Mul
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.ODE.Gronwall
import Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
import Mathlib.Tactic.GCongr
import Mathlib.Analysis.Calculus.Deriv.Slope
import Mathlib.Topology.Order.OrderClosed
import Mathlib.Tactic.Positivity
import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
import Mathlib.Topology.MetricSpace.Thickening
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.LinearAlgebra.Determinant
import Mathlib.Topology.Instances.Matrix
import Mathlib.LinearAlgebra.Matrix.Trace
import Mathlib.Analysis.Calculus.FDeriv.Analytic
import Mathlib.Topology.Algebra.Module.Determinant
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Topology.Order.ProjIcc
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Analysis.Normed.Operator.Basic
import Mathlib.LinearAlgebra.Matrix.Notation
import Mathlib.Analysis.Calculus.ContDiff.Deriv
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
import Mathlib.Topology.MetricSpace.Cauchy
import Mathlib.Analysis.Calculus.ContDiff.Comp
import Mathlib.Analysis.Calculus.Deriv.Comp
import Mathlib.Analysis.Calculus.UniformLimitsDeriv
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
import Mathlib.Analysis.Calculus.ParametricIntegral
import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.Calculus.FDeriv.Comp
import Mathlib.Algebra.Order.Floor.Ring
import Mathlib.Analysis.Calculus.FDeriv.Mul
import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib.Data.List.Induction
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Algebra.Order.Floor.Semiring
import Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
import Mathlib.Topology.Algebra.InfiniteSum.Order
import Mathlib.Data.PNat.Basic
import Mathlib.Data.Rat.Floor
import Mathlib.NumberTheory.Real.Irrational
import Mathlib.Order.OrderIsoNat
import Mathlib.MeasureTheory.Group.MeasurableEquiv
import Mathlib.MeasureTheory.Measure.Regular
import Mathlib.MeasureTheory.Function.JacobianOneDim
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
import Mathlib.MeasureTheory.Function.Floor
import Mathlib.Dynamics.Ergodic.Ergodic
import Mathlib.Dynamics.BirkhoffSum.Average
import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.MeasureTheory.Measure.WithDensity
import Mathlib.Dynamics.Ergodic.MeasurePreserving
import Mathlib.Analysis.Asymptotics.SpecificAsymptotics
import Mathlib.Topology.UniformSpace.HeineCantor
import Mathlib.Dynamics.BirkhoffSum.NormedSpace
import Mathlib.MeasureTheory.Integral.Bochner.Set
import Mathlib.Analysis.Normed.Group.Tannery
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Definitions.Def_BianchiIX_Dynamics_Normalized
import Definitions.Def_BianchiIX_Dynamics_AxisMaps
import Definitions.Def_BianchiIX_Dynamics_AxisSymmetry
import Definitions.Def_BianchiIX_AxisAndOrbitData
import Mathlib.Analysis.InnerProductSpace.PiL2
import Definitions.Def_BianchiIX_Dynamics_ProjectiveState
import Definitions.Def_BianchiIX_Dynamics_MaximalFlow
import Definitions.Def_BianchiIX_Statistics_EraStatistics
import Definitions.Def_BianchiIX_Dynamics_CoreEntryDifferential
import Mathlib.Topology.Order.MonotoneConvergence
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Definitions.Def_BianchiIX_TerminalConeData
import Definitions.Def_BianchiIX_EraReturnData
import Mathlib.Order.Interval.Set.Monotone

section

noncomputable section

namespace BianchiIX

open Set MeasureTheory

local instance _root_.BianchiIX.instMeasurableSpaceListPNat_bianchiIX : MeasurableSpace (List ℕ+) := ⊤

namespace EraSurvivor

variable {η σ Bcap : ℝ} {J : ℕ}

def budgetState (p : eraSurvivorDomain η J σ Bcap) (n : ℕ) : ℝ × CoreAngleState :=
  eraPrefixState η J (word p n) p.val

def state (p : eraSurvivorDomain η J σ Bcap) (n : ℕ) : CoreAngleState := (budgetState p n).2



















end EraSurvivor
end BianchiIX

end
end

section

section
noncomputable section
open BianchiIX

private theorem BianchiIX.axisCycle_shears (x : NormalizedState) :
    normalizedShears (axisCycle x) = ![normalizedShears x 1, normalizedShears x 2, normalizedShears x 0] := by
  have hs : (Real.sqrt 3) ^ 2 = 3 := Real.sq_sqrt (by norm_num)
  ext i
  fin_cases i <;> dsimp [normalizedShears, axisCycle] <;> ring_nf <;> norm_num [hs] <;> ring

end
end

section
noncomputable section
open BianchiIX

private theorem BianchiIX.axisSwap_shears (x : NormalizedState) :
    normalizedShears (axisSwap x) = ![normalizedShears x 0, normalizedShears x 2, normalizedShears x 1] := by
  ext i
  fin_cases i <;> dsimp [normalizedShears, axisSwap] <;> ring

end
end

section
noncomputable section
open BianchiIX

private theorem BianchiIX.axisOrder_bijective : ∀ i, Function.Bijective (axisOrder i) := by decide

end
end

section
noncomputable section
open BianchiIX

private theorem BianchiIX.axisFrame_apply (i : Fin 6) (x : NormalizedState) :
    (axisFrame i).map x =
      ![x, axisCycle x, axisCycle (axisCycle x), axisSwap x,
        axisSwap (axisCycle x), axisSwap (axisCycle (axisCycle x))] i := by
  fin_cases i <;> rfl

end
end

section
noncomputable section
open BianchiIX

private theorem BianchiIX.axisFrame_walls (i : Fin 6) (x : NormalizedState) :
    normalizedWalls ((axisFrame i).map x) = fun j => normalizedWalls x (axisOrder i j) := by
  rw [axisFrame_apply]
  fin_cases i <;> ext j <;> fin_cases j <;> rfl

end
end

section
noncomputable section
open BianchiIX

private theorem BianchiIX.axisFrame_shears (i : Fin 6) (x : NormalizedState) :
    normalizedShears ((axisFrame i).map x) = fun j => normalizedShears x (axisOrder i j) := by
  rw [axisFrame_apply]
  fin_cases i
  · ext j
    fin_cases j <;> rfl
  · change normalizedShears (axisCycle x) = _
    rw [axisCycle_shears]
    ext j
    fin_cases j <;> rfl
  · change normalizedShears (axisCycle (axisCycle x)) = _
    simp only [axisCycle_shears]
    ext j
    fin_cases j <;> rfl
  · change normalizedShears (axisSwap x) = _
    rw [axisSwap_shears]
    ext j
    fin_cases j <;> rfl
  · change normalizedShears (axisSwap (axisCycle x)) = _
    simp only [axisSwap_shears, axisCycle_shears]
    ext j
    fin_cases j <;> rfl
  · change normalizedShears (axisSwap (axisCycle (axisCycle x))) = _
    simp only [axisSwap_shears, axisCycle_shears]
    ext j
    fin_cases j <;> rfl

end
end

section
noncomputable section
open BianchiIX

private theorem BianchiIX.normalizedState_ext_shears_walls {x y : NormalizedState}
    (hs : normalizedShears x = normalizedShears y) (hw : normalizedWalls x = normalizedWalls y) : x = y := by
  have h₀ := congrFun hs 0
  have h₁ := congrFun hs 1
  change -2 * x 0 = -2 * y 0 at h₀
  change x 0 - Real.sqrt 3 * x 1 = y 0 - Real.sqrt 3 * y 1 at h₁
  have hx₀ : x 0 = y 0 := by linarith
  have hx₁ : x 1 = y 1 := mul_left_cancel₀ (Real.sqrt_ne_zero'.mpr (by norm_num : (0 : ℝ) < 3))
    (by linarith : Real.sqrt 3 * x 1 = Real.sqrt 3 * y 1)
  ext i
  fin_cases i
  · exact hx₀
  · exact hx₁
  · exact congrFun hw 0
  · exact congrFun hw 1
  · exact congrFun hw 2

end
end

section
noncomputable section
open BianchiIX

private theorem BianchiIX.axisFrame_comp (i j : Fin 6) :
    ∃ k : Fin 6, ∀ x : NormalizedState,
      (axisFrame i).map ((axisFrame j).map x) = (axisFrame k).map x := by
  let σ : Equiv.Perm (Fin 3) := Equiv.ofBijective (axisOrder i) (axisOrder_bijective i)
  let τ : Equiv.Perm (Fin 3) := Equiv.ofBijective (axisOrder j) (axisOrder_bijective j)
  obtain ⟨k, hk⟩ := axisOrder_covers (σ.trans τ)
  refine ⟨k, fun x => normalizedState_ext_shears_walls ?_ ?_⟩
  · ext l
    simp only [axisFrame_shears, hk]
    rfl
  · ext l
    simp only [axisFrame_walls, hk]
    rfl

end
end


noncomputable section

namespace BianchiIX

namespace EraSurvivor

variable {η σ Bcap : ℝ} {J : ℕ}

def duration (p : eraSurvivorDomain η J σ Bcap) (n : ℕ) : ℝ :=
  eraReturnTime η J (digits p n).natPred (state p n)

def elapsedTime (p : eraSurvivorDomain η J σ Bcap) (n : ℕ) : ℝ :=
  ∑ j ∈ Finset.range n, duration p j

def frame (p : eraSurvivorDomain η J σ Bcap) : ℕ → Fin 6
  | 0 => 0
  | n + 1 => (axisFrame_comp (eraReturnFrame (digits p n).natPred) (frame p n)).choose













end EraSurvivor



end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

/-- Physical frame, elapsed time, budget, and actual core state. -/
abbrev CoreRestartData := (Fin 6 × ℝ) × (ℝ × CoreAngleState)

def CoreRestartWitness (η : ℝ) (J : ℕ) (σ Bcap : ℝ) (x : NormalizedState)
    (w : CoreRestartData) : Prop :=
  0 < w.1.2 ∧ w.1.2 ∈ normalizedMaxDomain x 0 ∧
    ∃ p : eraSurvivorDomain η J σ Bcap, p.val = w.2 ∧
      EraStatistics (EraSurvivor.digits p) (EraSurvivor.phase p) ∧
      coreRadiusEntry p.val.2 = toProjectiveState ((axisFrame w.1.1).map (normalizedMaxCurve x 0 w.1.2))









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology

namespace EraSurvivor

variable {η σ Bcap : ℝ} {J : ℕ}

def physicalTime (w : CoreRestartData) (p : eraSurvivorDomain η J σ Bcap) (n : ℕ) : ℝ :=
  elapsedTime p n + w.1.2

def physicalFrame (w : CoreRestartData) (p : eraSurvivorDomain η J σ Bcap) (n : ℕ) : Fin 6 :=
  (axisFrame_comp (frame p n) w.1.1).choose

end EraSurvivor



end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set Filter
open scoped Topology

/-- Complete eras on one original physical trajectory, including the terminal connection before the first era. -/
structure PhysicalEraSequence (η : ℝ) (J : ℕ) (x : NormalizedState)
    (K : ℕ → ℕ+) (Y : ℕ → CoreAngleState) (t : ℕ → ℝ) (a : ℕ → Fin 6) : Prop where
  constraint : stateConstraint x = 1
  statistics : EraStatistics K (fun n => 2 / Y n 0)
  time_positive : ∀ n, 0 < t n
  time_strictMono : StrictMono t
  time_unbounded : Tendsto t atTop atTop
  entrance : ∀ n, fromProjectiveState (coreRadiusEntry (Y n)) =
    (axisFrame (a n)).map (normalizedMaxCurve x 0 (t n))
  block : ∀ n, EraEventItinerary η J (K n).natPred (Y n)
  next_state : ∀ n, coreRadiusEntry (Y (n + 1)) = terminalNaturalState η J
    (eraCoreExit (K n).natPred (Y n))
  next_time : ∀ n, t (n + 1) = eraReturnTime η J (K n).natPred (Y n) + t n
  next_frame : ∀ n z, (axisFrame (a (n + 1))).map z =
    (axisFrame (eraReturnFrame (K n).natPred)).map ((axisFrame (a n)).map z)
  preceding_terminal : ∃ m X s i, EraEventItinerary η J m X ∧ 0 < s ∧ s < t 0 ∧
    fromProjectiveState (coreRadiusEntry X) = (axisFrame i).map (normalizedMaxCurve x 0 s) ∧
    t 0 = eraReturnTime η J m X + s ∧
    coreRadiusEntry (Y 0) = terminalNaturalState η J (eraCoreExit m X) ∧
    ∀ z, (axisFrame (a 0)).map z = (axisFrame (eraReturnFrame m)).map ((axisFrame i).map z)

namespace EraSurvivor









end EraSurvivor

namespace PhysicalEraSequence
















end PhysicalEraSequence
end BianchiIX

end
end
Source
https://github.com/l46430640-del/ERA-STATISTICS-FORMAL/tree/d74c241819f896ab8d050b21ace80c8e90eabd9e/BianchiIX

View graph