Prove2Me

Radial entrance coordinates and exact connection phase response

Definition
BianchiIX_EntrancePhaseResponseData

by trppppp · Nov 5, 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.

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 i=0,1i=0,1 put j(0)=1j(0)=1, j(1)=3j(1)=3, and define

mi(η,Y)=exp⁡(log⁡(1+(xY)0)−log⁡(1+(αxY,0(Tη(Y)))0)+∫0Tη(Y)rj(i)(αxY,0(t)) dt).m_i(\eta,Y)=\exp\left(\log(1+(x_Y)_0) -\log(1+(\alpha_{x_Y,0}(T_\eta(Y)))_0) +\int_0^{T_\eta(Y)}r_{j(i)}(\alpha_{x_Y,0}(t))\,dt\right).

Let R(m,u,v,w)=(−m,u,w,v)\mathcal R(m,u,v,w)=(-m,u,w,v).

On the invariant plane with zero active wall, use y=(m,u,w)∈R3y=(m,u,w)\in\mathbb R^3, the inclusion ι(m,u,w)=(m,u,0,w)\iota(m,u,w)=(m,u,0,w) and the restriction πs(m,u,v,w)=(m,u,w)\pi_s(m,u,v,w)=(m,u,w). Define

f(y)=(mu2−(m+1)uw+w2,1−m2−w2+u22u,−(m+1+uw−u2)w),f(y)=\left(mu^2-(m+1)uw+w^2, \frac{1-m^2-w^2+u^2}{2}u,-(m+1+uw-u^2)w\right), Δ(y)=3+m2+(u−w)2,fo(y)=6f(y)/Δ(y).\Delta(y)=3+m^2+(u-w)^2,\qquad f_o(y)=6f(y)/\Delta(y).

Write J=dfJ=df, H=d2fH=d^2f, Jo=dfoJ_o=df_o, Ho=d2foH_o=d^2f_o for their explicit Jacobian and Hessian expressions. The denominator derivatives are dΔ=(2m,2(u−w),2(w−u))d\Delta=(2m,2(u-w),2(w-u)) and d2Δ(v,z)=2v0z0+2(v1−v2)(z1−z2)d^2\Delta(v,z)=2v_0z_0+2(v_1-v_2)(z_1-z_2). The exact original-time boundary flow and its projected variation are

Φ(y,t)=πsΨ0(ιy,t),L(y,t)=πsJιy,0(t)ι.\Phi(y,t)=\pi_s\Psi_0(\iota y,t),\qquad L(y,t)=\pi_s\mathcal J_{\iota y,0}(t)\iota.

For a fixed scale KK, set ΦK(y,s)=Φ(y,Ks)\Phi_K(y,s)=\Phi(y,Ks), LK(y,s)=L(y,Ks)L_K(y,s)=L(y,Ks) and QK(y,s)=dyLK(y,s)Q_K(y,s)=d_yL_K(y,s). For directions v,zv,z, define

SK(y,s;v,z)=K[Ho(ΦK)(LKv,LKz)+Jo(ΦK)QK(v,z)].S_K(y,s;v,z)=K\left[H_o(\Phi_K)(L_Kv,L_Kz)+J_o(\Phi_K)Q_K(v,z)\right].

All vector norms are sup norms, and operator norms are induced by them. Write b(y)=∣u∣+∣w∣b(y)=|u|+|w|, E(y)=e512b(y)E(y)=e^{512b(y)}, vs=(v1,v2)v_s=(v_1,v_2), and

H(y;v,z)=b(y)∥v∥∥z∥+∥vs∥∥z∥+∥v∥∥zs∥,\mathcal H(y;v,z)=b(y)\|v\|\|z\|+\|v_s\|\|z\|+\|v\|\|z_s\|, B2(y)=192b(y)(40000E(y)3)+10000E(y)2.B_2(y)=192b(y)(40000E(y)^3)+10000E(y)^2.

The closed boundary region is Sc={(m,u,0,w):∣m−c∣≤1/10, ∣u∣,∣w∣≤1/100}\mathcal S_c=\{(m,u,0,w):|m-c|\leq1/10,\ |u|,|w|\leq1/100\}. The boundary projection P(m,u,w)P(m,u,w) is the limit of Φ(m,u,w;t)0\Phi(m,u,w;t)_0 as t→∞t\to\infty, using the total limit convention of the formal definitions.

Define

Ek={(m,u,v,w):m≥1, ∣r(m,v)−k∣≤k/100, 0≤u,w≤1/10000, 0≤v≤1},\mathcal E_k=\{(m,u,v,w):m\geq1,\ |r(m,v)-k|\leq k/100, \ 0\leq u,w\leq1/10000,\ 0\leq v\leq1\},

and ω+(m,u,v,w)=s(m,u,v,w)\omega_+(m,u,v,w)=s(m,u,v,w). 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 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 p(y)=P(m,u,w)p(y)=P(m,u,w), ρ(y)=(p(y)−1)2+v2\rho(y)=\sqrt{(p(y)-1)^2+v^2}, ω(y)=m−1−u(v+w−u)\omega(y)=m-1-u(v+w-u), and χ(y)=(ρ(y),u,v,w)\chi(y)=(\rho(y),u,v,w). Write pi=∂ipp_i=\partial_i p. The inverse differential Jχ(y)J_\chi(y) preserves the last three coordinates and has first row

(ρ(p−1)p0,−p1p0,−v(p−1)p0,−p3p0).\left(\frac{\rho}{(p-1)p_0},-\frac{p_1}{p_0}, -\frac{v}{(p-1)p_0},-\frac{p_3}{p_0}\right).

An admissible local inverse ψ\psi at yy is C2C^2 at χ(y)\chi(y), maps χ(y)\chi(y) to yy, has derivative Jχ(y)J_\chi(y) there, and is a two-sided inverse to χ\chi on neighborhoods of these points. For a scalar function ff, write ∂ˉif=d(f∘ψ)χ(y)ei\bar\partial_i f=d(f\circ\psi)_{\chi(y)}e_i. The radial coefficients and drift are

N(y)=m−1−u(w−u)−(p−1)p0,B(y)=N(y)ρω,N(y)=m-1-u(w-u)-(p-1)p_0,\qquad B(y)=\frac{N(y)}{\rho\omega}, A(y)=(p−1)((1−m)p0+w(p1−p3))−v2−12(p−1)vp1ρω,G(y)=uvA(y)+v2B(y).A(y)=\frac{(p-1)((1-m)p_0+w(p_1-p_3))-v^2 -\tfrac12(p-1)vp_1}{\rho\omega},\qquad G(y)=uvA(y)+v^2B(y).

Set

S(y)=(p−1)((p−m)−(m−1)(p0−1))+(p−1)w(p1−p3)−12(p−1)vp1,H(y)=p−1−(m−1)p0,S(y)=(p-1)((p-m)-(m-1)(p_0-1))+(p-1)w(p_1-p_3) -\tfrac12(p-1)vp_1,\quad H(y)=p-1-(m-1)p_0, N2(y)=(1−L−2)u2+(−1+4L−2)uw−w2/L2,L=m+1,N_2(y)=(1-L^{-2})u^2+(-1+4L^{-2})uw-w^2/L^2,\qquad L=m+1, Re(y)=Rq(m,u,w),N4(y)=−Re−(m−1)∂0Re−(p−m)(p0−1),E(y)=ρ(y)−r(m,v).R_e(y)=R_q(m,u,w),\quad N_4(y)=-R_e-(m-1)\partial_0R_e-(p-m)(p_0-1),\quad E(y)=\rho(y)-r(m,v).

Here

Rq(m,u,w)=P(m,u,w)−[m+mu2m2−1−2uwm+1+w22(m+1)].R_q(m,u,w)=P(m,u,w)- \left[m+\frac{mu^2}{m^2-1}-\frac{2uw}{m+1}+\frac{w^2}{2(m+1)}\right].

The logarithmic wall rates are

as=1−m2−(v−w)2+u22ω,aw=−1−2(1+u(v+w−u))ω.a_s=\frac{1-m^2-(v-w)^2+u^2}{2\omega},\qquad a_w=-1-\frac{2(1+u(v+w-u))}{\omega}.

Let Dχf=df JχD_\chi f=df\,J_\chi, define

c(y)=(DχG e0,uDχG e1,wDχG e3),c(y)=(D_\chi G\,e_0,uD_\chi G\,e_1,wD_\chi G\,e_3), Ak(y)=(uDχas e1(w/k2)Dχas e3k2uDχaw e1wDχaw e3),\mathcal A_k(y)= \begin{pmatrix}uD_\chi a_s\,e_1&(w/k^2)D_\chi a_s\,e_3\\ k^2uD_\chi a_w\,e_1&wD_\chi a_w\,e_3\end{pmatrix},

and ℓk(y)=(log⁡u,k2log⁡w)\ell_k(y)=(\log u,k^2\log w). All vector and operator norms use the sup norm.

For C,A≥0C,A\geq0 define

SC,A,x,y(c)=∣c1∣∣x∣+∣c2∣∣y∣+CA(∣c1∣+∣c2∣),S_{C,A,x,y}(c)=|c_1||x|+|c_2||y|+CA(|c_1|+|c_2|), KC,l(c)=(C+1)(∣c0∣+l(∣c1∣+∣c2∣)).K_{C,l}(c)=(C+1)(|c_0|+l(|c_1|+|c_2|)).

The logarithmic active-wall field is F/ωF/\omega, its observable is log⁡v\log v, and its original-time rate is 6ω/D6\omega/D. The tangent projection at fixed relative active-wall clock is

Πclk(y,h,ζ)=h−(h2/y2−ζ)F(y)/ω(y).\Pi_{\rm clk}(y,h,\zeta)=h-(h_2/y_2-\zeta)F(y)/\omega(y).

Applied to the exact flow differential, it uses ζ=h2/y2\zeta=h_2/y_2 at the initial point. Radial input variations first apply JχJ_\chi. The wall tangent is (h1/u,k2h3/w)(h_1/u,k^2h_3/w); the radial source column is (Dχase0,k2Dχawe0)(D_\chi a_s e_0,k^2D_\chi a_w e_0). The two column envelopes are the sums of the absolute entries of Ak\mathcal A_k. The weighted phase coefficient is (c0,c1,c2/k2)(c_0,c_1,c_2/k^2), and its feedback rate is ∣c0∣+l(∣c1∣+∣c2∣/k2)|c_0|+l(|c_1|+|c_2|/k^2). For the reflected finite-tail entry eη(Y)=RPη(Y)e_\eta(Y)=\mathcal R P_\eta(Y), define

Fη=ρ∘eη,F^η(Y)=r(P+(eη(Y))0,P+(eη(Y))2),Dη=F^η−Fη.F_\eta=\rho\circ e_\eta,\quad \widehat F_\eta(Y)=r(P_+(e_\eta(Y))_0,P_+(e_\eta(Y))_2),\quad D_\eta=\widehat F_\eta-F_\eta.

Its radial entrance coordinates are χ(eη(Y))=(Fη(Y),Y1m0(η,Y),Y2m1(η,Y),η)\chi(e_\eta(Y))=(F_\eta(Y),Y_1m_0(\eta,Y),Y_2m_1(\eta,Y),\eta).

Definition code
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.SpecialFunctions.Arsinh
import Mathlib.Analysis.SpecialFunctions.Sqrt
import Mathlib.Tactic.FieldSimp
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.Deriv.Prod
import Mathlib.Analysis.Calculus.MeanValue
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.FunProp
import Mathlib.Analysis.Calculus.Deriv.Inv
import Mathlib.Tactic.LinearCombination
import Mathlib.Analysis.SpecialFunctions.Arcosh
import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
import Mathlib.Analysis.Calculus.Deriv.MeanValue
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv
import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
import Mathlib.Analysis.ODE.ExistUnique
import Mathlib.Analysis.Calculus.FDeriv.Partial
import Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
import Definitions.Def_BianchiIX_Dynamics_ProjectiveState
import Definitions.Def_BianchiIX_Dynamics_EntranceRegion
import Mathlib.Topology.Instances.Real.Lemmas
import Mathlib.Tactic.GCongr
import Mathlib.Analysis.Calculus.Deriv.Slope
import Mathlib.Topology.Order.OrderClosed
import Mathlib.Analysis.SpecialFunctions.Log.Deriv
import Definitions.Def_BianchiIX_Dynamics_ProjectiveFlowVariation
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Module
import Definitions.Def_BianchiIX_CompactPhaseExpansionData
import Mathlib.Analysis.ODE.Gronwall
import Mathlib.Data.Matrix.Mul
import Mathlib.Topology.Order.IntermediateValue
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.ParametricIntervalIntegral
import Mathlib.Topology.Order.Compact
import Mathlib.MeasureTheory.Integral.DominatedConvergence
import Mathlib.Topology.Order.ProjIcc
import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff
import Definitions.Def_BianchiIX_Dynamics_CoreAngle
import Definitions.Def_BianchiIX_Dynamics_CoreTailMultipliers
import Mathlib.Analysis.Calculus.ImplicitContDiff
import Mathlib.Algebra.BigOperators.Fin
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
import Mathlib.Analysis.SpecialFunctions.Log.Basic
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.Calculus.Deriv.Pi
import Definitions.Def_BianchiIX_Algebra_CoreAngle
import Definitions.Def_BianchiIX_Dynamics_CompactConnectionReturn
import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
import Mathlib.Analysis.Calculus.ParametricIntegral
import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
import Definitions.Def_BianchiIX_StableProjectionRefinementData
import Definitions.Def_BianchiIX_Analysis_ConnectionAmplitudeDifferential
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
import Mathlib.Analysis.SpecialFunctions.Pow.Real

section

noncomputable section

namespace BianchiIX

open Set MeasureTheory

def coupledVariationSource (C A x y : ℝ) (c : Fin 3 → ℝ) : ℝ :=
  |c 1| * |x| + |c 2| * |y| + C * A * (|c 1| + |c 2|)

def coupledVariationFeedback (C l : ℝ) (c : Fin 3 → ℝ) : ℝ :=
  (C + 1) * (|c 0| + l * (|c 1| + |c 2|))



end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

def entranceLogField (y : ProjectiveState) : ProjectiveState :=
  (entranceClockRate y)⁻¹ • projectiveField y

def entranceLogClock (y : ProjectiveState) : ℝ := Real.log (y 2)

def entranceOriginalClockRate (y : ProjectiveState) : ℝ :=
  (6 / projectiveStateDenom y) * entranceClockRate y

















end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set Filter
open scoped Topology

/-- Tangent at fixed log(V/V_entry); zeta is the initial logarithmic wall variation. -/
def entranceClockProjection (y v : ProjectiveState) (ζ : ℝ) : ProjectiveState :=
  v - (v 2 / y 2 - ζ) • entranceLogField y





def entranceProjectedFlowVariation (y : ProjectiveState) (t₀ t : ℝ) (w : ProjectiveState) :
    ProjectiveState := entranceClockProjection (projectiveOriginalFlow y t₀ t)
      (projectiveFlowDifferential y t₀ t w) (w 2 / y 2)







end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

def entranceWeakNumerator (y : ProjectiveState) : ℝ :=
  y 0 - 1 - y 1 * (y 3 - y 1) - (entranceStablePhase y - 1) * entranceStablePartial y 0

def entranceRadialStrongCoefficient (y : ProjectiveState) : ℝ :=
  ((entranceStablePhase y - 1) * ((1 - y 0) * entranceStablePartial y 0 +
    y 3 * (entranceStablePartial y 1 - entranceStablePartial y 3)) - y 2 ^ 2 -
    (1 / 2) * (entranceStablePhase y - 1) * y 2 * entranceStablePartial y 1) /
      (entranceStableRadius y * entranceClockRate y)

def entranceRadialWeakCoefficient (y : ProjectiveState) : ℝ :=
  entranceWeakNumerator y / (entranceStableRadius y * entranceClockRate y)

def entranceStrongRemainder (y : ProjectiveState) : ℝ :=
  (entranceStablePhase y - 1) * ((entranceStablePhase y - y 0) -
    (y 0 - 1) * (entranceStablePartial y 0 - 1)) +
  (entranceStablePhase y - 1) * y 3 * (entranceStablePartial y 1 - entranceStablePartial y 3) -
  (1 / 2) * (entranceStablePhase y - 1) * y 2 * entranceStablePartial y 1











end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX




def entranceStrongBracket (y : ProjectiveState) : ℝ :=
  entranceStablePhase y - 1 - (y 0 - 1) * entranceStablePartial y 0





















end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

def entranceRadialCoordinates (y : ProjectiveState) : ProjectiveState :=
  ![entranceStableRadius y, y 1, y 2, y 3]

def entranceRadialDifferential (y : ProjectiveState) : ProjectiveState →L[ℝ] ProjectiveState :=
  ContinuousLinearMap.pi ![fderiv ℝ entranceStableRadius y, ContinuousLinearMap.proj 1,
    ContinuousLinearMap.proj 2, ContinuousLinearMap.proj 3]

def entranceRadialInverseDifferential (y : ProjectiveState) : ProjectiveState →L[ℝ] ProjectiveState :=
  ContinuousLinearMap.pi ![
    (entranceStableRadius y / ((entranceStablePhase y - 1) * entranceStablePartial y 0)) • ContinuousLinearMap.proj 0 -
    (entranceStablePartial y 1 / entranceStablePartial y 0) • ContinuousLinearMap.proj 1 -
    (y 2 / ((entranceStablePhase y - 1) * entranceStablePartial y 0)) • ContinuousLinearMap.proj 2 -
    (entranceStablePartial y 3 / entranceStablePartial y 0) • ContinuousLinearMap.proj 3,
    ContinuousLinearMap.proj 1, ContinuousLinearMap.proj 2, ContinuousLinearMap.proj 3]













end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology

structure EntranceRadialInverseAt (y : ProjectiveState) (Ψ : ProjectiveState → ProjectiveState) : Prop where
  apply_base : Ψ (entranceRadialCoordinates y) = y
  contDiffAt : ContDiffAt ℝ 2 Ψ (entranceRadialCoordinates y)
  hasFDerivAt : HasFDerivAt Ψ (entranceRadialInverseDifferential y) (entranceRadialCoordinates y)
  left_inverse : ∀ᶠ z in 𝓝 y, Ψ (entranceRadialCoordinates z) = z
  right_inverse : ∀ᶠ z in 𝓝 (entranceRadialCoordinates y), entranceRadialCoordinates (Ψ z) = z















end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set Filter Metric
open scoped Topology

def compactConnectionCoordinates (η : ℝ) (Y : CoreAngleState) : ProjectiveState :=
  ![compactConnectionFinitePhase η Y, Y 1 * coreTailMultiplier η Y 0,
    Y 2 * coreTailMultiplier η Y 1, η]









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology

def compactConnectionPhase (η : ℝ) (Y : CoreAngleState) : ℝ :=
  coreRadius (compactConnectionState η Y 0) (compactConnectionState η Y 2)

def compactConnectionError (η : ℝ) (Y : CoreAngleState) : ℝ :=
  compactConnectionPhase η Y - compactConnectionFinitePhase η Y





end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

def entranceRadiusCorrection (y : ProjectiveState) : ℝ :=
  entranceStableRadius y - coreRadius (y 0) (y 2)









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology



local instance entranceStableOperatorGroup : NormedAddCommGroup (StableState →L[ℝ] ℝ) :=
  ContinuousLinearMap.toNormedAddCommGroup
local instance entranceStableOperatorSpace : NormedSpace ℝ (StableState →L[ℝ] ℝ) := inferInstance





end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX


local instance entranceOperatorSpace : NormedSpace ℝ (ProjectiveState →L[ℝ] ℝ) := inferInstance









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology



local instance entranceQuarticStableOperatorGroup : NormedAddCommGroup (StableState →L[ℝ] ℝ) :=
  ContinuousLinearMap.toNormedAddCommGroup
local instance entranceQuarticStableOperatorSpace : NormedSpace ℝ (StableState →L[ℝ] ℝ) := inferInstance

def entranceQuarticRemainder (y : ProjectiveState) : ℝ := stableQuadraticRemainder (stableRestriction y)









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

def entranceStrongLogRate (y : ProjectiveState) : ℝ := connectionStrongClockRate (y 0) (y 1) (y 2) (y 3)

def entranceWeakLogRate (y : ProjectiveState) : ℝ := connectionWeakClockRate (y 0) (y 1) (y 2) (y 3)









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

def entranceWeakQuadratic (y : ProjectiveState) : ℝ :=
  (1 - 1 / (y 0 + 1) ^ 2) * y 1 ^ 2 + (-1 + 4 / (y 0 + 1) ^ 2) * y 1 * y 3 - y 3 ^ 2 / (y 0 + 1) ^ 2

def entranceWeakRemainder (y : ProjectiveState) : ℝ :=
  -entranceQuarticRemainder y - (y 0 - 1) * fderiv ℝ entranceQuarticRemainder y (Pi.single 0 1) -
    (entranceStablePhase y - y 0) * (entranceStablePartial y 0 - 1)









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology

def entranceRadialDrift (y : ProjectiveState) : ℝ :=
  y 1 * y 2 * entranceRadialStrongCoefficient y + y 2 ^ 2 * entranceRadialWeakCoefficient y







end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology

def entranceRadialDriftDifferential (y : ProjectiveState) : ProjectiveState →L[ℝ] ℝ :=
  (fderiv ℝ entranceRadialDrift y).comp (entranceRadialInverseDifferential y)

def entranceRadialVariationCoefficients (y : ProjectiveState) : Fin 3 → ℝ :=
  ![entranceRadialDriftDifferential y (Pi.single 0 1),
    y 1 * entranceRadialDriftDifferential y (Pi.single 1 1),
    y 3 * entranceRadialDriftDifferential y (Pi.single 3 1)]













end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

def entranceStrongLogDifferential (y : ProjectiveState) : ProjectiveState →L[ℝ] ℝ :=
  (fderiv ℝ entranceStrongLogRate y).comp (entranceRadialInverseDifferential y)

def entranceWeakLogDifferential (y : ProjectiveState) : ProjectiveState →L[ℝ] ℝ :=
  (fderiv ℝ entranceWeakLogRate y).comp (entranceRadialInverseDifferential y)

def entranceWallWeightedMatrix (k : ℝ) (y : ProjectiveState) : Matrix (Fin 2) (Fin 2) ℝ :=
  !![y 1 * entranceStrongLogDifferential y (Pi.single 1 1),
      y 3 / k ^ 2 * entranceStrongLogDifferential y (Pi.single 3 1);
    k ^ 2 * y 1 * entranceWeakLogDifferential y (Pi.single 1 1),
      y 3 * entranceWeakLogDifferential y (Pi.single 3 1)]

def entranceWallWeightedColumn (k : ℝ) (y : ProjectiveState) (j : Fin 2) : ℝ :=
  |entranceWallWeightedMatrix k y 0 j| + |entranceWallWeightedMatrix k y 1 j|















end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set MeasureTheory

def entranceWallRadialSource (k : ℝ) (y : ProjectiveState) : Fin 2 → ℝ :=
  ![entranceStrongLogDifferential y (Pi.single 0 1), k ^ 2 * entranceWeakLogDifferential y (Pi.single 0 1)]





end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set MeasureTheory

def entrancePhaseFeedbackRate (k l : ℝ) (y : ProjectiveState) : ℝ :=
  |entranceRadialVariationCoefficients y 0| +
    l * (|entranceRadialVariationCoefficients y 1| + |entranceRadialVariationCoefficients y 2| / k ^ 2)





end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Filter
open scoped Topology

def entranceWallTangent (k : ℝ) (y v : ProjectiveState) : Fin 2 → ℝ :=
  ![v 1 / y 1, k ^ 2 * (v 3 / y 3)]













end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set MeasureTheory

def entranceLogWalls (k : ℝ) (y : ProjectiveState) : Fin 2 → ℝ :=
  ![Real.log (y 1), k ^ 2 * Real.log (y 3)]









end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set MeasureTheory

def entranceWeightedPhaseCoefficients (k : ℝ) (y : ProjectiveState) : Fin 3 → ℝ :=
  ![entranceRadialVariationCoefficients y 0, entranceRadialVariationCoefficients y 1,
    entranceRadialVariationCoefficients y 2 / k ^ 2]







end BianchiIX

end
end

section

noncomputable section

namespace BianchiIX

open Set

def entranceRadialClockVariation (y : ProjectiveState) (t₀ t : ℝ) (d : ProjectiveState) : ProjectiveState :=
  entranceProjectedFlowVariation y t₀ t (entranceRadialInverseDifferential y d)















end BianchiIX

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

View graph