Circle-invariant normal coordinates linearize a bifurcate Killing boost

In a surface slice chart choose its smooth tangent basis $E_1,E_2$, put $h_{ij}=g(E_i,E_j)$, and write $h^{ij}$ for the inverse matrix. Since $h$ is positive definite, its determinant is positive and its inverse is smooth by the adjugate formula. For $V\in TM{\mathrm{\mid }}_S$, define $PV={\sum }_{i,j=1}^2{h}^{ij}g(V,E_j)E_i$. Direct pairing with $E_k$ gives $g(PV,E_k)=g(V,E_k)$, and $P$ is the identity on $TS$. Thus $V-PV\in NS$ and $TS\cap NS=\{0\}$ by positive definiteness. These two characterizations uniquely determine $P$, so the chartwise smooth projections agree on overlaps and give $TM{\mathrm{\mid }}_S=TS\oplus NS$, with $NS=\ker P$ a smooth rank-two normal bundle. Set $n=N{\mathrm{\mid }}_S-P(N{\mathrm{\mid }}_S)$. Orthogonality yields $g(n,n)=g(N,N)-g(PN,PN)<0$ and $g(n,N)=g(n,n)<0$. Therefore $n$ is a globally defined smooth future timelike normal field, constructed without assuming a normal frame.

Average and normalize the field $n$ from step 1.1 using [F1], obtaining the smooth invariant future unit normal $e_0$. Write $B(v)={\mathrm{\nabla }}_{v}K$ on $NS$ and set $e_1={\kappa }^{-1}B(e_0)$. In any local future/outward orthonormal normal basis $(f_0,f_1)$, write $e_0=\cosh a{f}_0+\sinh a{f}_1$. The assumed boost matrix then gives $e_1=\sinh a{f}_0+\cosh a{f}_1$, which is outward, unit spacelike and orthogonal to $e_0$. The formula for $e_1$ proves smoothness. The connected circle preserves the normal-plane orientation and $e_0$, so it preserves the unique outward unit normal orthogonal to $e_0$, namely $e_1$. Changing a future/outward orthonormal basis in a Lorentzian two-plane is a Lorentz boost, which commutes with the positive-rate boost matrix; thus the stated $B$ matrix is unchanged in this frame. Apply [F2] to obtain a uniform tube.

To justify [F3]'s equivariance, differentiate the pullback metric along a Killing flow: its derivative is the pullback of ${\mathcal{L}}_{K}g=0$, so it is an isometry. Pulling back the connection preserves its two defining conditions; uniqueness identifies the pulled-back connection with the original one. Uniqueness of its geodesics gives ${\varphi }_s^K{\exp }_y(w)={\exp }_y(d{\varphi }_s^{K}w)$ where defined. The fixed-point differential boost from [F1] therefore gives the claimed exact boost formula in $(u,v)$. The same argument for $Z$, with its invariant frame, gives its base-only action. Differentiating the hyperbolic-coordinate change proves $K={\mathrm{\partial }}_{\tau }$, and the other two vector-field formulas follow.