For y = ( m , u , v , w ) ∈ R 4 y=(m,u,v,w)\in\mathbb R^4 y = ( m , u , v , w ) ∈ R 4 , define
K ( u , v , w ) = u 2 + v 2 + w 2 − 2 ( u v + v w + w u ) , κ = u ( v + w − u ) , K(u,v,w)=u^2+v^2+w^2-2(uv+vw+wu),\qquad \kappa=u(v+w-u), K ( u , v , w ) = u 2 + v 2 + w 2 − 2 ( uv + v w + w u ) , κ = u ( v + w − u ) ,
F m = − v 2 + w 2 + u ( v − w ) − m κ , F u = 1 2 ( 1 − m 2 − ( v − w ) 2 + u 2 ) 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, F m = − v 2 + w 2 + u ( v − w ) − mκ , F u = 2 1 ( 1 − m 2 − ( v − w ) 2 + u 2 ) u ,
F v = ( m − 1 − κ ) v , F w = ( − m − 1 − κ ) w , F = ( F m , F u , F v , F w ) , F_v=(m-1-\kappa)v,\qquad F_w=(-m-1-\kappa)w,\qquad
F=(F_m,F_u,F_v,F_w), F v = ( m − 1 − κ ) v , F w = ( − m − 1 − κ ) w , F = ( F m , F u , F v , F w ) ,
and E ( m , v ) = ( m − 1 ) 2 + v 2 E(m,v)=(m-1)^2+v^2 E ( m , v ) = ( m − 1 ) 2 + v 2 .
Write r ( m , v ) = ( m − 1 ) 2 + v 2 r(m,v)=\sqrt{(m-1)^2+v^2} r ( m , v ) = ( m − 1 ) 2 + v 2 and define
g ( R , v ) = R 2 − v 2 , d ( R , u , v , w ) = g ( R , v ) + u ( v + w − u ) , g(R,v)=\sqrt{R^2-v^2},\qquad d(R,u,v,w)=g(R,v)+u(v+w-u), g ( R , v ) = R 2 − v 2 , d ( R , u , v , w ) = g ( R , v ) + u ( v + w − u ) ,
f R = − u ( v + w − u ) R − g ( R , v ) ( u − w ) 2 / R d , f_R=\frac{-u(v+w-u)R-g(R,v)(u-w)^2/R}{d}, f R = d − u ( v + w − u ) R − g ( R , v ) ( u − w ) 2 / R ,
a s = 2 g ( R , v ) − R 2 + 2 v w − w 2 + u 2 2 d , a w = g ( R , v ) − 2 − u ( v + w − u ) d . a_s=\frac{2g(R,v)-R^2+2vw-w^2+u^2}{2d},\qquad
a_w=\frac{g(R,v)-2-u(v+w-u)}d. a s = 2 d 2 g ( R , v ) − R 2 + 2 v w − w 2 + u 2 , a w = d g ( R , v ) − 2 − u ( v + w − u ) .
The exit clock rate is ω ( y ) = 1 − m + u ( v + w − u ) \omega(y)=1-m+u(v+w-u) ω ( y ) = 1 − m + u ( v + w − u ) , and its field is
F log ( y ) = F ( y ) / ω ( y ) F_{\log}(y)=F(y)/\omega(y) F l o g ( y ) = F ( y ) / ω ( y ) . Division and square roots have their total
real-valued Lean meanings.
For Y = ( R , u , w ) Y=(R,u,w) Y = ( R , u , w ) define E v ( Y ) = ( f R , a s u , a w w ) E_v(Y)=(f_R,a_su,a_ww) E v ( Y ) = ( f R , a s u , a w w ) , evaluated at ( R , u , v , w ) (R,u,v,w) ( R , u , v , w ) .
The coordinate maps are Q ( m , u , v , w ) = ( r ( m , v ) , u , w ) Q(m,u,v,w)=(r(m,v),u,w) Q ( m , u , v , w ) = ( r ( m , v ) , u , w ) and
Q v − 1 ( R , u , w ) = ( 1 − g ( R , v ) , u , v , w ) Q_v^{-1}(R,u,w)=(1-g(R,v),u,v,w) Q v − 1 ( R , u , w ) = ( 1 − g ( R , v ) , u , v , w ) .
For a curve Y ( s ) Y(s) Y ( s ) set
M i ( Y , t ) = exp ∫ 0 t a i ( Y 0 ( s ) , Y 1 ( s ) , e − s , Y 2 ( s ) ) d s ( i = s , w ) . M_i(Y,t)=\exp\int_0^t a_i(Y_0(s),Y_1(s),e^{-s},Y_2(s))\,ds
\quad(i=s,w). M i ( Y , t ) = exp ∫ 0 t a i ( Y 0 ( s ) , Y 1 ( s ) , e − s , Y 2 ( s )) d s ( i = s , w ) .
Let R α , b , A , D \mathcal R_{\alpha,b,A,D} R α , b , A , D consist of the states satisfying
7 / 4 ≤ R ≤ 17 / 4 , ∣ u ∣ , ∣ w ∣ ≤ 1 / 100 , ∣ u ∣ + ∣ w ∣ ≤ A b , ∣ R − ( 2 + 2 α ) ∣ ≤ D b . 7/4\leq R\leq17/4,\quad |u|,|w|\leq1/100,\quad
|u|+|w|\leq Ab,\quad |R-(2+2\alpha)|\leq Db. 7/4 ≤ R ≤ 17/4 , ∣ u ∣ , ∣ w ∣ ≤ 1/100 , ∣ u ∣ + ∣ w ∣ ≤ A b , ∣ R − ( 2 + 2 α ) ∣ ≤ D b .
Put
B ( α , b , A , D , T ) = [ 10 ( α + D b ) + 100 ( A b ) 2 ] T + 100 A b + 5 , B(\alpha,b,A,D,T)=[10(\alpha+Db)+100(Ab)^2]T+100Ab+5, B ( α , b , A , D , T ) = [ 10 ( α + D b ) + 100 ( A b ) 2 ] T + 100 A b + 5 ,
L ( η , α , J ) = log ( 1 / η ) + J log ( 1 / α ) . L(\eta,\alpha,J)=\log(1/\eta)+J\log(1/\alpha). L ( η , α , J ) = log ( 1/ η ) + J log ( 1/ α ) .
Define
H 0 = ( 2 − g ( R , v ) ) 2 + v 2 , d 0 = ( u − w ) 2 − 2 v ( u + w ) , H_0=(2-g(R,v))^2+v^2,\quad d_0=(u-w)^2-2v(u+w), H 0 = ( 2 − g ( R , v ) ) 2 + v 2 , d 0 = ( u − w ) 2 − 2 v ( u + w ) ,
e = d 0 [ 1 + ( R 2 − 4 + d 0 ) / H 0 ] , σ v ( R , u , w ) = ( R 2 + e − 2 ) / 2. e=d_0[1+(R^2-4+d_0)/H_0],\qquad
\sigma_v(R,u,w)=(\sqrt{R^2+e}-2)/2. e = d 0 [ 1 + ( R 2 − 4 + d 0 ) / H 0 ] , σ v ( R , u , w ) = ( R 2 + e − 2 ) /2.
Put
H 0 , R = 2 ( g − 2 ) R / g , e R = d 0 [ 2 R / H 0 − ( R 2 − 4 + d 0 ) H 0 , R / H 0 2 ] , H_{0,R}=2(g-2)R/g,\quad
e_R=d_0[2R/H_0-(R^2-4+d_0)H_{0,R}/H_0^2], H 0 , R = 2 ( g − 2 ) R / g , e R = d 0 [ 2 R / H 0 − ( R 2 − 4 + d 0 ) H 0 , R / H 0 2 ] ,
e w a l l = 1 + ( R 2 − 4 + 2 d 0 ) / H 0 . e_{\rm wall}=1+(R^2-4+2d_0)/H_0. e wall = 1 + ( R 2 − 4 + 2 d 0 ) / H 0 .
If 0 < α ≤ 1 0<\alpha\leq1 0 < α ≤ 1 ,
b ≤ α / 10000 b\leq\alpha/10000 b ≤ α /10000 , ∣ R − ( 2 + 2 α ) ∣ ≤ α / 10000 |R-(2+2\alpha)|\leq\alpha/10000 ∣ R − ( 2 + 2 α ) ∣ ≤ α /10000 ,
∣ u ∣ + ∣ w ∣ ≤ b |u|+|w|\leq b ∣ u ∣ + ∣ w ∣ ≤ b , and 0 ≤ v ≤ α / 100 0\leq v\leq\alpha/100 0 ≤ v ≤ α /100 , then
2 < R ≤ 5 , 2 < g ( R , v ) ≤ 5 , v 2 < R 2 , α 2 ≤ H 0 , 2<R\leq5,\quad2<g(R,v)\leq5,\quad v^2<R^2,\quad
\alpha^2\leq H_0, 2 < R ≤ 5 , 2 < g ( R , v ) ≤ 5 , v 2 < R 2 , α 2 ≤ H 0 ,
∣ d 0 ∣ ≤ α 2 / 1000 , ∣ R 2 − 4 + d 0 ∣ ≤ 22 α , H 0 + d 0 > 0 , R 2 − 4 + d 0 > 0. |d_0|\leq\alpha^2/1000,\quad |R^2-4+d_0|\leq22\alpha,\quad
H_0+d_0>0,\quad R^2-4+d_0>0. ∣ d 0 ∣ ≤ α 2 /1000 , ∣ R 2 − 4 + d 0 ∣ ≤ 22 α , H 0 + d 0 > 0 , R 2 − 4 + d 0 > 0.