[proofplan] The proof has two independent parts. The support statement is exactly the assumed local domain-of-dependence estimate applied to the solution $u$ with cone vertex $(t_0,y_0)$. The microlocal statement uses only the retarded properly supported Fourier integral representation, the wave front mapping theorem for Fourier integral operators, and the stated bicharacteristic speed bound; the strict hyperbolicity and well-posedness hypotheses are the structural assumptions behind those inputs. The closed inequalities are obtained by integrating the speed bound on the full time interval of the smooth bicharacteristic base projection. [/proofplan]

[step:Apply the domain-of-dependence estimate to the closed coordinate cone]Set $x_0:=\varphi(y_0)$ and define \begin{align*} K:=\overline D_c(t_0,y_0). \end{align*} By hypothesis, $K$ is compactly contained in $J\times O$. The assumed vanishing of the source gives \begin{align*} Pu=f=0\quad\text{in }\mathcal{D}'(\operatorname{int}_{J\times O}K), \end{align*} and the assumed vanishing of the Cauchy traces gives \begin{align*} \gamma_k u=g_k=0\quad\text{in }\mathcal{D}'(\{y\in O:|\varphi(y)-x_0|<ct_0\}) \end{align*} for every $0\leq k\leq m-1$. Therefore the local domain-of-dependence property, applied with $w=u$, $h=f$, $t_*=t_0$, and $x_*=x_0$, gives an open neighbourhood $U\subset J\times O$ of $(t_0,y_0)$ such that $u=0$ in the energy sense on $U$. Since energy-class vanishing implies distributional vanishing by the same hypothesis, $u=0$ in $\mathcal{D}'(U)$.[/step]

[guided]We first isolate the part of the theorem that is not microlocal. The relevant compact cone is \begin{align*} K:=\overline D_c(t_0,y_0) =\{(s,y)\in[0,t_0]\times O:|\varphi(y)-\varphi(y_0)|\leq c(t_0-s)\}. \end{align*} This is exactly the cone appearing in the assumed domain-of-dependence principle with $t_*=t_0$ and $x_*=\varphi(y_0)$. The compact-containment hypothesis required by that principle is part of the theorem statement: $K$ is compactly contained in $J\times O$. Now we verify the two vanishing hypotheses of the domain-of-dependence principle for the choice $w=u$ and $h=f$. Since $Pu=f$, the assumption \begin{align*} f=0\quad\text{in }\mathcal{D}'(\operatorname{int}_{J\times O}\overline D_c(t_0,y_0)) \end{align*} is precisely the required statement that $h=0$ in the interior of $K$. Likewise, for each integer $k$ with $0\leq k\leq m-1$, the trace identity $\gamma_k u=g_k$ and the hypothesis \begin{align*} g_k=0\quad\text{in }\mathcal{D}'(\{y\in O:|\varphi(y)-\varphi(y_0)|<ct_0\}) \end{align*} give the required vanishing of the $k$th Cauchy trace on the open initial ball at time $0$. All hypotheses of the assumed local domain-of-dependence estimate are therefore satisfied. It follows that $u$ vanishes in the energy sense on some open neighbourhood $U\subset J\times O$ of $(t_0,y_0)$. The domain-of-dependence hypothesis also states that this energy vanishing implies distributional vanishing, so $u=0$ in $\mathcal{D}'(U)$.[/guided]

[step:Use the retarded parametrix to reduce wave front membership to canonical-relation images]Fix a nonzero covector $\eta\in T^*_{(t_0,y_0)}(J\times O)$ and suppose \begin{align*} ((t_0,y_0),\eta)\in\operatorname{WF}(u). \end{align*} By the microlocal parametrix hypothesis, choose a properly supported order-zero pseudodifferential cutoff $A$ on $J\times O$ whose principal symbol is elliptic at $((t_0,y_0),\eta)$, and choose properly supported input pseudodifferential cutoffs $B$ on $J\times O$ and $B_k$ on $O$ supported in the microlocal coordinate neighbourhood where the retarded representation is valid. The hypothesis on localized parametrices gives, microlocally near $((t_0,y_0),\eta)$, \begin{align*} Au=AEBf+\sum_{k=0}^{m-1}AE_kB_k g_k+R, \end{align*} where $R$ is smooth microlocally near $((t_0,y_0),\eta)$. The operators $AEB$ and $AE_kB_k$ are properly supported Fourier integral operators in the twisted operator convention; by the statement hypotheses their closed conic canonical relations are contained in $C_E$ and $C_k$, respectively. Since $A$ is elliptic at $((t_0,y_0),\eta)$ and $R$ contributes no wave front direction there, the assumed membership of $((t_0,y_0),\eta)$ in $\operatorname{WF}(u)$ forces this covector to occur in the wave front set of the localized right-hand side. The wave front set of a finite sum is contained in the union of the wave front sets of its summands. Hence $((t_0,y_0),\eta)$ belongs to $\operatorname{WF}(AEBf)$ or to $\operatorname{WF}(AE_kB_k g_k)$ for at least one $k$ with $0\leq k\leq m-1$. Applying [citetheorem:TEMP-47] to these localized properly supported Fourier integral operators is legitimate because the operators are properly supported, their canonical relations are closed conic canonical relations in the convention of the theorem, and the covectors under consideration are nonzero. The theorem first gives input covectors in $\operatorname{WF}(Bf)$ or $\operatorname{WF}(B_k g_k)$. Since properly supported pseudodifferential cutoffs do not create wave front set, we have \begin{align*} \operatorname{WF}(Bf)\subset\operatorname{WF}(f) \end{align*} and, for each $0\leq k\leq m-1$, \begin{align*} \operatorname{WF}(B_k g_k)\subset\operatorname{WF}(g_k). \end{align*} Thus the theorem gives the following alternatives. Either there exist $(s,z)\in J\times O$ and $\zeta\in T^*_{(s,z)}(J\times O)\setminus 0$ such that \begin{align*} ((s,z),\zeta)\in\operatorname{WF}(f) \end{align*} and \begin{align*} (((t_0,y_0),\eta),((s,z),\zeta))\in C_E, \end{align*} or there exist $k\in\{0,\dots,m-1\}$, $z\in O$, and $\zeta\in T^*_zO\setminus 0$ such that \begin{align*} (z,\zeta)\in\operatorname{WF}(g_k) \end{align*} and \begin{align*} (((t_0,y_0),\eta),(z,\zeta))\in C_k. \end{align*}[/step]

[guided]We now turn the microlocal representation into a statement about where singularities can come from. Fix a nonzero covector $\eta\in T^*_{(t_0,y_0)}(J\times O)$ and assume \begin{align*} ((t_0,y_0),\eta)\in\operatorname{WF}(u). \end{align*} The representation is only asserted microlocally near $((t_0,y_0),\eta)$, so we first localize it. Choose an output microlocal cutoff $A$ elliptic at $((t_0,y_0),\eta)$ and input cutoffs $B$ and $B_k$ supported in the coordinate neighbourhood where the retarded representation is valid. After these cutoffs are inserted, the localized representation has the form \begin{align*} Au=AEBf+\sum_{k=0}^{m-1}AE_kB_k g_k+R \end{align*} microlocally near $((t_0,y_0),\eta)$, where $R$ is smooth microlocally there. The localized operators are properly supported Fourier integral operators. Their canonical relations are contained in the originally stated relations $C_E$ and $C_k$, because microlocal cutoffs can only restrict a canonical relation, not create new branches. The smooth remainder cannot contribute to the wave front direction at $((t_0,y_0),\eta)$, and ellipticity of $A$ at that covector preserves the detected singularity. Therefore this covector must come from one of the finitely many localized Fourier integral operator terms. The wave front set of a finite sum is contained in the union of the wave front sets of its summands, so $((t_0,y_0),\eta)$ lies in $\operatorname{WF}(AEBf)$ or in $\operatorname{WF}(AE_kB_k g_k)$ for at least one integer $k$ with $0\leq k\leq m-1$. We may now apply [citetheorem:TEMP-47]. Its hypotheses are satisfied because the localized operators are properly supported Fourier integral operators, their canonical relations are closed conic canonical relations in the twisted operator convention used in the theorem, and the input and output covectors are nonzero. The theorem first locates the input singularity in the wave front set after the input cutoff: for the source term it gives a point of $\operatorname{WF}(Bf)$, and for the $k$th initial term it gives a point of $\operatorname{WF}(B_k g_k)$. This is enough because $B$ and $B_k$ are properly supported pseudodifferential operators, and pseudodifferential operators cannot create wave front set: \begin{align*} \operatorname{WF}(Bf)\subset\operatorname{WF}(f) \end{align*} and \begin{align*} \operatorname{WF}(B_k g_k)\subset\operatorname{WF}(g_k). \end{align*} For the source operator $E$, the theorem therefore gives a point $(s,z)\in J\times O$ and a nonzero covector $\zeta\in T^*_{(s,z)}(J\times O)$ such that \begin{align*} ((s,z),\zeta)\in\operatorname{WF}(f) \end{align*} and \begin{align*} (((t_0,y_0),\eta),((s,z),\zeta))\in C_E. \end{align*} For an initial-data operator $E_k$, the same theorem gives a point $z\in O$ and a nonzero covector $\zeta\in T^*_zO$ such that \begin{align*} (z,\zeta)\in\operatorname{WF}(g_k) \end{align*} and \begin{align*} (((t_0,y_0),\eta),(z,\zeta))\in C_k. \end{align*} These are the only possible microlocal sources of the wave front direction under consideration.[/guided]

[step:Integrate the bicharacteristic speed bound for source terms]Assume the first alternative from the preceding step occurs. By the retarded time-oriented hypothesis on $C_E$, the time coordinate of the source point satisfies $0\leq s\leq t_0$, and there are a branch $j$ and curves \begin{align*} x:[s,t_0]\to V \end{align*} and \begin{align*} \xi:[s,t_0]\to\mathbb{R}^n_0 \end{align*} such that $x(s)=\varphi(z)$, $x(t_0)=x_0$, and \begin{align*} \frac{dx}{dr}(r)=-\partial_\xi\lambda_j(r,x(r),\xi(r)) \end{align*} for every $r\in[s,t_0]$. Since the lifted bicharacteristic is a smooth Hamiltonian integral curve, its base projection $x:[s,t_0]\to V\subset\mathbb{R}^n$ is $C^1$, hence absolutely continuous. The velocity hypothesis gives \begin{align*} \left|\frac{dx}{dr}(r)\right|\leq c \end{align*} for every $r\in[s,t_0]$. By the fundamental estimate for absolutely continuous curves in Euclidean space, \begin{align*} |\varphi(z)-x_0|\leq \int_s^{t_0}\left|\frac{dx}{dr}(r)\right|\,d\mathcal{L}^1(r). \end{align*} Using the bound on the integrand gives \begin{align*} |\varphi(z)-x_0|\leq \int_s^{t_0}c\,d\mathcal{L}^1(r)=c(t_0-s). \end{align*} Therefore \begin{align*} (s,z)\in\overline D_c(t_0,y_0). \end{align*} This proves the first asserted microlocal alternative with the required closed cone condition.[/step]

[guided]Now we explain why the canonical relation cannot bring a source singularity from outside the closed backward cone. Suppose that the source-term alternative given by the Fourier integral operator mapping theorem holds. Thus there are $(s,z)\in J\times O$ and a nonzero covector $\zeta\in T^*_{(s,z)}(J\times O)$ such that \begin{align*} ((s,z),\zeta)\in\operatorname{WF}(f) \end{align*} and \begin{align*} (((t_0,y_0),\eta),((s,z),\zeta))\in C_E. \end{align*} The retarded hypothesis on $C_E$ supplies the geometric information behind this relation. It says first that $0\leq s\leq t_0$, so the source point is not advanced in time. It also says that the relation is generated by a lifted bicharacteristic over one characteristic branch $\tau=\lambda_j(t,x,\xi)$. In local coordinates, the base projection is a curve \begin{align*} x:[s,t_0]\to V \end{align*} with $x(s)=\varphi(z)$ and $x(t_0)=\varphi(y_0)$. There is also a covector curve \begin{align*} \xi:[s,t_0]\to\mathbb{R}^n_0 \end{align*} such that the base velocity is \begin{align*} \frac{dx}{dr}(r)=-\partial_\xi\lambda_j(r,x(r),\xi(r)). \end{align*} Because this curve is the base projection of a smooth lifted Hamiltonian bicharacteristic, $x:[s,t_0]\to V\subset\mathbb{R}^n$ is $C^1$ and therefore absolutely continuous. The speed assumption is exactly the finite-propagation ingredient. Since \begin{align*} |\partial_\xi\lambda_j(r,x(r),\xi(r))|\leq c \end{align*} for every $r\in[s,t_0]$, the velocity equation implies \begin{align*} \left|\frac{dx}{dr}(r)\right|\leq c \end{align*} for every $r\in[s,t_0]$. Applying the fundamental estimate for an absolutely continuous Euclidean curve to the map $x:[s,t_0]\to\mathbb{R}^n$ gives \begin{align*} |x(s)-x(t_0)|\leq \int_s^{t_0}\left|\frac{dx}{dr}(r)\right|\,d\mathcal{L}^1(r). \end{align*} Substituting $x(s)=\varphi(z)$ and $x(t_0)=\varphi(y_0)$ gives \begin{align*} |\varphi(z)-\varphi(y_0)|\leq \int_s^{t_0}\left|\frac{dx}{dr}(r)\right|\,d\mathcal{L}^1(r). \end{align*} Using the pointwise velocity bound inside the integral yields \begin{align*} |\varphi(z)-\varphi(y_0)|\leq \int_s^{t_0}c\,d\mathcal{L}^1(r)=c(t_0-s). \end{align*} This is the closed cone inequality, including the boundary case. Hence \begin{align*} (s,z)\in\overline D_c(t_0,y_0). \end{align*} So every source singularity that can reach $((t_0,y_0),\eta)$ through $C_E$ must be based in the closed local backward cone.[/guided]

[step:Integrate the bicharacteristic speed bound for Cauchy data]Assume the second alternative from the parametrix step occurs for some $k\in\{0,\dots,m-1\}$. By the retarded time-oriented hypothesis on $C_k$, there are a branch $j$ and curves \begin{align*} x:[0,t_0]\to V \end{align*} and \begin{align*} \xi:[0,t_0]\to\mathbb{R}^n_0 \end{align*} such that $x(0)=\varphi(z)$, $x(t_0)=x_0$, and \begin{align*} \frac{dx}{dr}(r)=-\partial_\xi\lambda_j(r,x(r),\xi(r)). \end{align*} Since this lifted bicharacteristic is a smooth Hamiltonian integral curve, its base projection $x:[0,t_0]\to V\subset\mathbb{R}^n$ is $C^1$, hence absolutely continuous. The velocity bound gives \begin{align*} \left|\frac{dx}{dr}(r)\right|\leq c \end{align*} for every $r\in[0,t_0]$. Therefore \begin{align*} |\varphi(z)-x_0|\leq \int_0^{t_0}\left|\frac{dx}{dr}(r)\right|\,d\mathcal{L}^1(r)\leq \int_0^{t_0}c\,d\mathcal{L}^1(r)=ct_0. \end{align*} Thus $z$ lies in the closed initial ball \begin{align*} \{y\in O:|\varphi(y)-x_0|\leq ct_0\}. \end{align*} This proves the second asserted microlocal alternative with the required closed initial-ball condition.[/step]

[guided]The Cauchy-data case is the same geometric estimate with starting time fixed at $0$. Suppose the initial-data alternative from the Fourier integral operator mapping step occurs for an integer $k$ satisfying $0\leq k\leq m-1$. Thus there are $z\in O$ and a nonzero covector $\zeta\in T_z^*O$ such that \begin{align*} (z,\zeta)\in\operatorname{WF}(g_k) \end{align*} and \begin{align*} (((t_0,y_0),\eta),(z,\zeta))\in C_k. \end{align*} The retarded time-oriented hypothesis on $C_k$ says that this canonical-relation element is generated by a lifted bicharacteristic over one branch $\tau=\lambda_j(t,x,\xi)$. Its base projection starts at the initial hypersurface and ends at the target point. Therefore there are maps \begin{align*} x:[0,t_0]\to V \end{align*} and \begin{align*} \xi:[0,t_0]\to\mathbb{R}^n_0 \end{align*} such that $x(0)=\varphi(z)$, $x(t_0)=x_0$, and \begin{align*} \frac{dx}{dr}(r)=-\partial_\xi\lambda_j(r,x(r),\xi(r)) \end{align*} for every $r\in[0,t_0]$. Because the lifted curve is a smooth Hamiltonian integral curve, the coordinate base curve $x:[0,t_0]\to\mathbb{R}^n$ is $C^1$ and hence absolutely continuous. The speed bound applies along this whole curve. Since \begin{align*} |\partial_\xi\lambda_j(r,x(r),\xi(r))|\leq c \end{align*} for every $r\in[0,t_0]$, the velocity equation gives \begin{align*} \left|\frac{dx}{dr}(r)\right|\leq c \end{align*} for every $r\in[0,t_0]$. The fundamental estimate for absolutely continuous curves in Euclidean space then gives \begin{align*} |x(0)-x(t_0)|\leq \int_0^{t_0}\left|\frac{dx}{dr}(r)\right|\,d\mathcal{L}^1(r). \end{align*} Substituting $x(0)=\varphi(z)$ and $x(t_0)=x_0$ yields \begin{align*} |\varphi(z)-x_0|\leq \int_0^{t_0}\left|\frac{dx}{dr}(r)\right|\,d\mathcal{L}^1(r). \end{align*} Using the pointwise bound by $c$ inside the integral gives \begin{align*} |\varphi(z)-x_0|\leq \int_0^{t_0}c\,d\mathcal{L}^1(r)=ct_0. \end{align*} Thus the Cauchy-data base point must lie in the closed initial ball \begin{align*} \{y\in O:|\varphi(y)-x_0|\leq ct_0\}. \end{align*} This proves the second microlocal alternative with the required closed-ball condition.[/guided]

[step:Conclude that branches outside the closed backward region do not contribute] Combining the Fourier integral operator mapping step with the two integrated speed estimates gives the asserted dichotomy for every nonzero covector $\eta\in T^*_{(t_0,y_0)}(J\times O)$ with $((t_0,y_0),\eta)\in\operatorname{WF}(u)$. In the source case, the contributing base point must lie in $\overline D_c(t_0,y_0)$. In the Cauchy-data case, the contributing base point must lie in the closed initial ball \begin{align*} \{z\in O:|\varphi(z)-x_0|\leq ct_0\}. \end{align*} Consequently, any retarded canonical-relation branch whose base projection begins strictly outside the corresponding closed region cannot be responsible for a wave front direction of $u$ over $(t_0,y_0)$. This is exactly the stated equivalent formulation. [/step]