Prove2Me

Exact era inverse trees, survivors and a common typical domain

Definition
BianchiIX_EraCodingData

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)).

A curve Γ=(U,W)\Gamma=(U,W) is admissible at budget BB if, for every r>2r>2, U(r),W(r)>0U(r),W(r)>0, U(r)+W(r)≤BU(r)+W(r)\leq B, both functions are C1C^1 at rr, and ∣U′(r)∣≤U(r)|U'(r)|\leq\sqrt{U(r)}, ∣W′(r)∣≤W(r)|W'(r)|\leq\sqrt{W(r)}. For an arbitrary graph, define its successor walls by

Um+=Ekm,uma,b; 2/(1−2β), 1/β,Wm+=Ekm,wma,b; 2/(1−2β), 1/β,U_m^+=\mathfrak E_{k_m,u_m}^{a,b;\,2/(1-2\beta),\,1/\beta},\qquad W_m^+=\mathfrak E_{k_m,w_m}^{a,b;\,2/(1-2\beta),\,1/\beta},

where E\mathfrak E is the canonical amplitude extension after composing with the choice inverse of kmk_m, with slope um′/km′u_m'/k_m' or wm′/km′w_m'/k_m'. The one-step property at (η,J,σ,B,C)(\eta,J,\sigma,B,C) consists of the following. Put β=Bσ\beta=B^\sigma, N=⌊1/β⌋NN=\lfloor1/\beta\rfloor_{\mathbb N}, Kβ=[2β,1−2β]K_\beta=[2\beta,1-2\beta]. One has 0<β<1/1600<\beta<1/160. For every m<Nm<N, hmh_m is strictly decreasing on KβK_\beta, and for y∈Kβy\in K_\beta,

1m+2<hm(y)<1m+1,ϕm(2/hm(y))=y,hm is C1 at y,hm′(y)<0,\frac1{m+2}<h_m(y)<\frac1{m+1},\quad \phi_m(2/h_m(y))=y, \quad h_m\text{ is }C^1\text{ at }y,\quad h_m'(y)<0, ∣hm(y)−γm+1(y)∣≤CB/(m+1)2,∣log⁡∣hm′(y)∣∣γm+1′(y)∣∣≤5CB.|h_m(y)-\gamma_{m+1}(y)|\leq CB/(m+1)^2,\quad \left|\log\frac{|h_m'(y)|}{|\gamma_{m+1}'(y)|}\right|\leq5C\sqrt B.

The successor (Um+,Wm+)(U_m^+,W_m^+) is admissible at budget B4/3B^{4/3} and, with r=2/hm(y)r=2/h_m(y), satisfies km(r)=2/yk_m(r)=2/y, Um+(2/y)=um(r)U_m^+(2/y)=u_m(r), Wm+(2/y)=wm(r)W_m^+(2/y)=w_m(r). The retained branch intervals are pairwise disjoint and λ((0,1)∖HN)≤10Bσ\lambda((0,1)\setminus\mathcal H_N)\leq10B^\sigma. For B∈RB\in\mathbb R and m∈Nm\in\mathbb N, define

Mm(B)=B(4/3)m,M_m(B)=B^{(4/3)^m},

where the outer power is the real power.

For a state (B,X)(B,X) let Fm(B,X)=(B4/3,(Rm(X),Sm(X)1,Sm(X)3))\mathcal F_m(B,X)=(B^{4/3},(R_m(X),S_m(X)_1,S_m(X)_3)). Its selected domain Dm(Bcap)D_m(B_{\rm cap}) is defined by

0<B≤Bcap,m<⌊B−σ⌋N,X1,X2>0,X1+X2≤B,0<B\leq B_{\rm cap},\quad m<\lfloor B^{-\sigma}\rfloor_{\mathbb N}, \quad X_1,X_2>0,\quad X_1+X_2\leq B, 2(m+1+Bσ)≤X0≤2(m+2−Bσ),2Bσ<Pm(X)<1−2Bσ.2(m+1+B^\sigma)\leq X_0\leq2(m+2-B^\sigma),\quad 2B^\sigma<P_m(X)<1-2B^\sigma.

For positive-digit words define D∅D_\varnothing to be the whole state space and Daw=Da−1(Bcap)∩Fa−1−1DwD_{a w}=D_{a-1}(B_{\rm cap})\cap\mathcal F_{a-1}^{-1}D_w. The survivor domain is D∞=⋂n⋃∣w∣=nDwD_\infty=\bigcap_n\bigcup_{|w|=n}D_w. For p∈D∞p\in D_\infty, choose its compatible words wnw_n and digits ana_n with wn+1=wnanw_{n+1}=w_n a_n. Let yn(p)=2/(Fwn(p))X,0y_n(p)=2/(\mathcal F_{w_n}(p))_{X,0} and let π(a)\pi(a) be the continued-fraction code. The common typical domain is

D={p∈D∞:π(a(p))∈BG},\mathcal D=\{p\in D_\infty:\pi(a(p))\in\mathcal B_G\},

where BG\mathcal B_G is the set of points with all Gauss cylinder frequencies. For a curve of budget BB, set TΓ={x∈(0,1):(B,Γ[2/x])∈D}\mathcal T_\Gamma=\{x\in(0,1):(B,\Gamma[2/x])\in\mathcal D\}. The curve family begins at Γ\Gamma and uses its successor for retained digits; other descendants use the constant pair (Mn+1(B)/2,Mn+1(B)/2)(M_{n+1}(B)/2,M_{n+1}(B)/2). At a word of length nn, its inverse branch for digit aa is ha−1h_{a-1}, with β=Mn(B)σ\beta=M_n(B)^\sigma, on (2β,1−2β)(2\beta,1-2\beta) if a−1<⌊1/β⌋Na-1<\lfloor1/\beta\rfloor_{\mathbb N}, and has empty domain otherwise. These branches and supplied one-step properties define an inverse tree. Its realization states that each branch edge agrees with Fa−1\mathcal F_{a-1} and that its image is exactly the selected domain on that curve.

Finite prefix states are the ordered compositions of the selected forward maps. Finite prefix domains impose selection at each step. The survivor digits are chosen from the unique compatible prefix words. The code, phase sequence, common typical domain and its pullback to each admissible curve use these same choices.

Definition code
import Definitions.Def_BianchiIX_Statistics_GaussInverse
import Definitions.Def_BianchiIX_Analysis_AmplitudeSequence
import Definitions.Def_BianchiIX_EraReturnData
import Definitions.Def_BianchiIX_Statistics_BranchTree
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 Definitions.Def_BianchiIX_Dynamics_CoreAngle
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
import Mathlib.MeasureTheory.Function.Floor
import Definitions.Def_BianchiIX_Statistics_GaussCoding
import Definitions.Def_BianchiIX_Statistics_GaussTypical
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

section

section
noncomputable section
open BianchiIX
open Set MeasureTheory
open scoped ENNReal
open EraCurve

private theorem BianchiIX.EraCurve.StepEstimates.branch_image_open {Γ : EraCurve} {η σ B C : ℝ} {J : ℕ}
    (H : Γ.StepEstimates η J σ B C) (m : ℕ) (hm : m < ⌊1 / B ^ σ⌋₊) :
    eraInverseBranch η J m (B ^ σ) Γ.U Γ.W '' Ioo (2 * B ^ σ) (1 - 2 * B ^ σ) =
      Ioo (eraInverseBranch η J m (B ^ σ) Γ.U Γ.W (1 - 2 * B ^ σ))
        (eraInverseBranch η J m (B ^ σ) Γ.U Γ.W (2 * B ^ σ)) := by
  have hc : ContinuousOn (eraInverseBranch η J m (B ^ σ) Γ.U Γ.W)
      (Icc (2 * B ^ σ) (1 - 2 * B ^ σ)) :=
    fun y hy => ((H.branch m hm).2 y hy).2.2.1.continuousAt.continuousWithinAt
  exact hc.image_Ioo_of_strictAntiOn (by linarith [H.beta_small]) (H.branch m hm).1

end
end


noncomputable section

namespace BianchiIX

open Set MeasureTheory
open scoped ENNReal

def eraTreeDomain (σ B : ℝ) (w : List ℕ+) (a : ℕ+) : Set ℝ :=
  if a.natPred < ⌊1 / (eraAmplitude B w.length) ^ σ⌋₊ then
    Ioo (2 * (eraAmplitude B w.length) ^ σ) (1 - 2 * (eraAmplitude B w.length) ^ σ)
  else ∅

theorem mem_eraTreeDomain {σ B y : ℝ} {w : List ℕ+} {a : ℕ+} :
    y ∈ eraTreeDomain σ B w a ↔ a.natPred < ⌊1 / (eraAmplitude B w.length) ^ σ⌋₊ ∧
      y ∈ Ioo (2 * (eraAmplitude B w.length) ^ σ) (1 - 2 * (eraAmplitude B w.length) ^ σ) := by
  unfold eraTreeDomain
  split_ifs <;> simp_all

namespace EraCurve

def treeBranch (Γ : EraCurve) (η : ℝ) (J : ℕ) (σ B : ℝ) (w : List ℕ+) (a : ℕ+) : ℝ → ℝ :=
  eraInverseBranch η J a.natPred ((eraAmplitude B w.length) ^ σ)
    (Γ.family η J σ B w).U (Γ.family η J σ B w).W

theorem treeBranch_image_of_retained {Γ : EraCurve} {η σ B C : ℝ} {J : ℕ} {w : List ℕ+}
    (H : (Γ.family η J σ B w).StepEstimates η J σ (eraAmplitude B w.length) C)
    (a : ℕ+) (ha : a.natPred < ⌊1 / (eraAmplitude B w.length) ^ σ⌋₊) :
    Γ.treeBranch η J σ B w a '' eraTreeDomain σ B w a =
      Ioo (Γ.treeBranch η J σ B w a (1 - 2 * (eraAmplitude B w.length) ^ σ))
        (Γ.treeBranch η J σ B w a (2 * (eraAmplitude B w.length) ^ σ)) := by
  rw [eraTreeDomain, if_pos ha]
  exact H.branch_image_open a.natPred ha

def inverseTree (Γ : EraCurve) (η : ℝ) (J : ℕ) (σ B C : ℝ)
    (H : ∀ w : List ℕ+, (Γ.family η J σ B w).StepEstimates η J σ (eraAmplitude B w.length) C) :
    InverseBranchTree where
  root := Ioo 0 1
  branch := Γ.treeBranch η J σ B
  domain := eraTreeDomain σ B
  root_open := isOpen_Ioo
  domain_open := by intro w a; unfold eraTreeDomain; split_ifs <;> first | exact isOpen_Ioo | exact isOpen_empty
  branch_continuous := by
    intro w a y hy
    obtain ⟨ha, hy⟩ := mem_eraTreeDomain.mp hy
    exact (((H w).branch a.natPred ha).2 y ⟨hy.1.le, hy.2.le⟩).2.2.1.continuousAt.continuousWithinAt
  branch_injective := by
    intro w a x hx y hy hxy
    obtain ⟨ha, hx⟩ := mem_eraTreeDomain.mp hx
    obtain ⟨_, hy⟩ := mem_eraTreeDomain.mp hy
    exact ((H w).branch a.natPred ha).1.injOn ⟨hx.1.le, hx.2.le⟩ ⟨hy.1.le, hy.2.le⟩ hxy
  branch_disjoint := by
    intro w a b hab
    by_cases ha : a.natPred < ⌊1 / (eraAmplitude B w.length) ^ σ⌋₊
    · by_cases hb : b.natPred < ⌊1 / (eraAmplitude B w.length) ^ σ⌋₊
      · rw [treeBranch_image_of_retained (H w) a ha, treeBranch_image_of_retained (H w) b hb]
        exact (H w).branch_disjoint (Finset.mem_range.mpr ha) (Finset.mem_range.mpr hb)
          (fun he => hab (PNat.natPred_injective he))
      · have hd : eraTreeDomain σ B w b = ∅ := by rw [eraTreeDomain, if_neg hb]
        rw [hd, image_empty]
        simp
    · have hd : eraTreeDomain σ B w a = ∅ := by rw [eraTreeDomain, if_neg ha]
      rw [hd, image_empty]
      simp









end EraCurve



end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set

def eraPrefixState (η : ℝ) (J : ℕ) : List ℕ+ → (ℝ × CoreAngleState) → ℝ × CoreAngleState
  | [] => id
  | a :: w => eraPrefixState η J w ∘ eraBudgetReturn η J a.natPred

def eraPrefixDomain (η : ℝ) (J : ℕ) (σ Bstar : ℝ) : List ℕ+ → Set (ℝ × CoreAngleState)
  | [] => univ
  | a :: w => eraSelectedInputs η J σ Bstar a.natPred ∩
      eraBudgetReturn η J a.natPred ⁻¹' eraPrefixDomain η J σ Bstar w

def eraSurvivorDomain (η : ℝ) (J : ℕ) (σ Bstar : ℝ) : Set (ℝ × CoreAngleState) :=
  ⋂ n : ℕ, ⋃ w : {w : List ℕ+ // w.length = n}, eraPrefixDomain η J σ Bstar w.val

















end BianchiIX

end
end

section

section
noncomputable section
open BianchiIX
open Set

private theorem BianchiIX.eraInputSelection_disjoint {σ Bstar : ℝ} {m n : ℕ} (hmn : m ≠ n) :
    Disjoint (eraInputSelection σ Bstar m) (eraInputSelection σ Bstar n) := by
  apply disjoint_left.mpr
  intro p hm hn
  have hβ : 0 < p.1 ^ σ := Real.rpow_pos_of_pos hm.1.1 _
  have hrm := hm.2.2.2.2.2
  have hrn := hn.2.2.2.2.2
  rcases lt_or_gt_of_ne hmn with h | h
  · have hcast : (m : ℝ) + 1 ≤ n := by exact_mod_cast (Nat.succ_le_of_lt h)
    linarith [hrm.2, hrn.1]
  · have hcast : (n : ℝ) + 1 ≤ m := by exact_mod_cast (Nat.succ_le_of_lt h)
    linarith [hrn.2, hrm.1]

end
end

section
noncomputable section
open BianchiIX
open Set

private theorem BianchiIX.eraSelectedInputs_disjoint (η : ℝ) (J : ℕ) (σ Bstar : ℝ) {m n : ℕ} (hmn : m ≠ n) :
    Disjoint (eraSelectedInputs η J σ Bstar m) (eraSelectedInputs η J σ Bstar n) :=
  (eraInputSelection_disjoint hmn).mono (fun _ h => h.1) (fun _ h => h.1)

end
end

section
noncomputable section
open BianchiIX
open Set

private theorem BianchiIX.mem_eraPrefixDomain_append (η : ℝ) (J : ℕ) (σ Bstar : ℝ)
    (v w : List ℕ+) (p : ℝ × CoreAngleState) :
    p ∈ eraPrefixDomain η J σ Bstar (v ++ w) ↔
      p ∈ eraPrefixDomain η J σ Bstar v ∧ eraPrefixState η J v p ∈ eraPrefixDomain η J σ Bstar w := by
  induction v generalizing p with
  | nil => simp [eraPrefixDomain, eraPrefixState]
  | cons a v ih =>
    simp only [List.cons_append, eraPrefixDomain, mem_inter_iff, mem_preimage, eraPrefixState,
      Function.comp_apply, ih]
    exact and_assoc.symm

end
end

section
noncomputable section
open BianchiIX
open Set

private theorem BianchiIX.eraPrefixDomain_unique (η : ℝ) (J : ℕ) (σ Bstar : ℝ) {v w : List ℕ+}
    (hlen : v.length = w.length) {p : ℝ × CoreAngleState}
    (hv : p ∈ eraPrefixDomain η J σ Bstar v) (hw : p ∈ eraPrefixDomain η J σ Bstar w) : v = w := by
  induction v generalizing w p with
  | nil => exact (List.length_eq_zero_iff.mp hlen.symm).symm
  | cons a v ih =>
    cases w with
    | nil => simp at hlen
    | cons b w =>
      have hab : a = b := by
        by_contra hne
        have hd := eraSelectedInputs_disjoint η J σ Bstar
          (fun he => hne (PNat.natPred_injective he))
        exact Set.disjoint_left.mp hd hv.1 hw.1
      subst b
      exact congrArg (List.cons a) (ih (Nat.succ.inj hlen) hv.2 hw.2)

end
end


noncomputable section

namespace BianchiIX

open Set

namespace EraSurvivor

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

private theorem exists_word (p : eraSurvivorDomain η J σ Bstar) (n : ℕ) :
    ∃ w : List ℕ+, w.length = n ∧ p.val ∈ eraPrefixDomain η J σ Bstar w := by
  obtain ⟨w, hw⟩ := mem_iUnion.mp (mem_iInter.mp p.property n)
  exact ⟨w.val, w.property, hw⟩

def word (p : eraSurvivorDomain η J σ Bstar) (n : ℕ) : List ℕ+ := (exists_word p n).choose

theorem word_length (p : eraSurvivorDomain η J σ Bstar) (n : ℕ) : (word p n).length = n :=
  (exists_word p n).choose_spec.1

theorem mem_word_domain (p : eraSurvivorDomain η J σ Bstar) (n : ℕ) :
    p.val ∈ eraPrefixDomain η J σ Bstar (word p n) := (exists_word p n).choose_spec.2



private theorem exists_next_digit (p : eraSurvivorDomain η J σ Bstar) (n : ℕ) :
    ∃ a : ℕ+, word p (n + 1) = word p n ++ [a] := by
  have hl := word_length p (n + 1)
  have hp := mem_word_domain p (n + 1)
  generalize word p (n + 1) = w at hl hp ⊢
  induction w using List.reverseRecOn with
  | nil => simp at hl
  | append_singleton w a _ =>
    have hw : w = word p n := eraPrefixDomain_unique η J σ Bstar
      (by simpa [word_length] using hl)
      ((mem_eraPrefixDomain_append η J σ Bstar w [a] p.val).mp hp).1 (mem_word_domain p n)
    exact ⟨a, congrArg (fun v => v ++ [a]) hw⟩

def digits (p : eraSurvivorDomain η J σ Bstar) (n : ℕ) : ℕ+ := (exists_next_digit p n).choose









def code (p : eraSurvivorDomain η J σ Bstar) : ℝ := gaussCode (digits p)



def typicalDomain (η : ℝ) (J : ℕ) (σ Bstar : ℝ) : Set (ℝ × CoreAngleState) :=
  Subtype.val '' {p : eraSurvivorDomain η J σ Bstar | code p ∈ gaussCylinderTypicalSet}







end EraSurvivor



end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set

namespace EraCurve

def treeState (Γ : EraCurve) (η : ℝ) (J : ℕ) (σ B : ℝ) (w : List ℕ+) (x : ℝ) : ℝ × CoreAngleState :=
  (eraAmplitude B w.length, (Γ.family η J σ B w).state (2 / x))



/-- Agreement of the selected forward return with every edge of an inverse tree. -/
structure Realization (Γ : EraCurve) (η : ℝ) (J : ℕ) (σ B Bcap : ℝ) (T : InverseBranchTree) : Prop where
  root : T.root = Ioo 0 1
  step : ∀ w a y, y ∈ T.domain w a →
    eraBudgetReturn η J a.natPred (Γ.treeState η J σ B w (T.branch w a y)) =
      Γ.treeState η J σ B (w ++ [a]) y
  selected : ∀ w a x, Γ.treeState η J σ B w x ∈ eraSelectedInputs η J σ Bcap a.natPred ↔
    x ∈ T.branch w a '' T.domain w a



namespace Realization












end Realization
end EraCurve
end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set

namespace EraSurvivor

def phase {η σ Bcap : ℝ} {J : ℕ} (p : eraSurvivorDomain η J σ Bcap) (n : ℕ) : ℝ :=
  2 / (eraPrefixState η J (word p n) p.val).2 0

def curveTypicalSet (Γ : EraCurve) (η : ℝ) (J : ℕ) (σ B Bcap : ℝ) : Set ℝ :=
  Ioo 0 1 ∩ (fun x => (B, Γ.state (2 / x))) ⁻¹' typicalDomain η J σ Bcap

end EraSurvivor

namespace EraCurve.Realization
















end EraCurve.Realization
end BianchiIX

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

View graph