Lens-shaped vs globally hyperbolic The theorem of uniqueness of solutions of first order, quasilinear, symmetric hyperbolic systems is naturally formulated in terms of so-called lens-shaped domains. Roughly, a domain is lens-shaped if it is bounded by two spacelike surfaces that are compact deformations of each other. Of course, for quasilinear systems, the notion of spacelike surface depends on some fixed solution. The theorem essentially states that any two solutions that agree on either boundary of a lens-shaped domain also agree on its interior. This result is described in more detail for example in the monographs on hyperbolic PDEs by John and Lax.
It appears to me that the notion of a lens-shaped domain is very close to the notion of a (partial) Cauchy development. However, in the literature that I am familiar with (mostly relativity and field theory on curved spacetimes), the Cauchy development is defined differently. Namely, given a spacelike surface $S$, its Cauchy development $D(S)$ is the maximal globally hyperbolic domain for which $S$ is a Cauchy surface (is intersected exactly once by every inextensible timelike curve). So these two notions are dual to each other; one is defined using spacelike surfaces and the other using timelike curves, again provided that both timelike and spacelike are defined with respect to some fixed solution.
I think that the two notions should coincide. (I have a rough sketch of an argument that might establish the equivalence, but am allowing for the possibility that some technical issues might spoil the result.) Unfortunately, I've yet to see this addressed in any of the references I'm familiar with. So, my question is the following.

Are the following statements true? And where could either proofs or counter examples be found in the literature?
(a) A lens-shaped domain is globally hyperbolic (has a Cauchy surface).
(b) Given a spacelike surface $S$, its Cauchy development $D(S)$ coincides with the union of all lens-shaped domains bounded by compact deformations of $S$.

 A: Christodoulou actually doesn't give the complete proof (which is why I said a proof needs to be extracted). Here let me give a proof of the geometric fact (the connection with the analysis will have to be made via suitable definitions of space-like and time-like). 
Fix a smooth manifold $M$. A causal structure $\mathcal{C}$ on $M$ is the ordered pair of two open subsets $(C,C') \subset TM\times T^*M$ with the following properties


*

*For any point $p\in M$, $C_p := C \cap T_pM$ is an open convex cone in $T_pM$. Similarly $C'_p$ is an open convex cone in $T^*_pM$. 

*For any $v\in C_p$ and $\xi\in C'_p$, we have $\xi(v) > 0$


A vector $v\in C_p$ is said to be future time-like. A hyperplane $S\subset T_pM$ is said to be space-like if there exists $\xi\in C'_p$ such that $\xi|_S \equiv 0$. A vector is said to be space-like if it lies in a space-like hyperplane. (Claim: the set of space-like vectors is an open set.)
Denote by $(C'_p)^*$ the convex dual of $C'_p$. That is:
$$ T_pM \supset (C'_p)^* := \{ w : \xi(w) > 0 \quad \forall \xi\in C'_p\} $$ 
So by definition we assumed $C\subset (C'_p)^*$. This in particular implies that the set of space-like and time-like vectors are disjoint. (Note that we allow the possibility that a vector is neither space-like nor time-like: that is if $w\in (C'_p)^* \setminus C_p$.) 
(Note that this definition of time-like and space-like corresponds to what gives good energy estimates.)
We take the following definitions:
Defn A lens-shaped domain $D\subset M$ based on $\Sigma$ is the image of a smooth map $\Phi: \Sigma\times (-1,1) \to M$ where $\Sigma\subset M$ is a compact, codimension 1 submanifold with boundary, with the property that 


*

*$\Phi(\cdot,0):\Sigma\to\Sigma$ is the identity map.

*$\Phi(x,t) = \Phi(x,s)$ for any $x\in\partial\Sigma$, $t,s\in (-1,1)$. 

*for any fixed $s\in (-1,1)$, $\Phi(\Sigma, s)$ is a space-like hypersurface.  

*away from $\partial\Sigma\times (-1,1)$, $\Phi$ is a diffeomorphism.


(the last condition I think is technical. One may be able to remove it. But for proving energy estimates, this induced foliation is used in the Gronwall inequality, so we might as well keep it.)
Now, a curve $\gamma\subset M$ is said to be causal if $T\gamma \subset \overline{ (C')^* \cup -(C')^*}$. 
Defn A globally hyperbolic development of $\Sigma$ is a subset $I\subset M$ such that for any inextensible causal curve $\gamma$


*

*$\gamma \cap I$ has at most one connected component

*if $\gamma\cap I\neq \emptyset$, then $\gamma$ intersects the interior of $\Sigma$.  


Note that by the definition $\partial\Sigma$ cannot be in $I$. 
Rmrk If in the definition of causal curve we use $C$ instead of $(C')^*$, the number of admissible curves $\gamma$ decreases, and so would give a looser definition. 

Prop A lens shaped domain $D(\Sigma)\setminus \partial\Sigma$ is a globally hyperbolic development $I(\Sigma)$. 
Proof Using that $\Phi$ restricts to a diffeomorphism, $\gamma\cap D(\Sigma)\setminus\partial\Sigma$ lifts to a curve $\tilde\gamma$ in the interior of $\Sigma\times(-1,1)$. Let $\tilde\gamma_0$ be a connected component. If the desired conclusion were to not hold, WLOG we can assume that the infimum of the projection onto $(-1,1)$ of $\tilde\gamma_0$ is not $t_m > -1$. That $\gamma$ is causal implies that $\tilde\gamma$ is transveral to the constant time surfaces, and so along the curve the projection is monotonic. Hence by inextendibility of $\gamma$ one can continuously extend $\tilde\gamma_0$ to intersect $\partial\Sigma\times\{t_m\}$. But this implies that $\gamma$ intersects $\partial\Sigma$ with $T\gamma$ there being space-like, a contradiction. 

Off the top of my head I don't have a good proof for the reverse implication. There are two problems involved: to properly develop causal relations and be able to take limits seems to require dealing with $C^0$ but piecewise smooth curves, and with this developed one can indeed connect the notion of a development to Leray's notion of global hyperbolicity (see, e.g. O'Neill Semi-Riemannian Geometry; the proofs there if suitably modified should also work to show that a development in the sense of time-like curves is globally hyperbolic). The problem then is to bring this notion back to the notion of lens-shaped spaces. Presumeably this was already done by Leray, since he was able to prove well-posedness of hyperbolic equations on such domains. 
But what I want to emphasize again here is that any possible dual implications must use the set $(C')^*$ to define causal curves, and not $C$ (the set of "globally hyperbolic domains defined relative to $C$" is strictly bigger than that for $(C')^*$, if the two are not equal). On the other hand, $C$ constitutes the natural set of "time-like" vectors with regards to which we can use Garding's inequality to get energy estimates. So one must be careful with the definitions to say that the two notions agree. 
A: After scrutinizing the literature some more, I've concluded that, in the case when the causal structure as defined in Willie's answer comes from a Lorentzian metric, the answer to my question has been available for some time and more recently in the general case.
The main point of confusion, and the reason I did not realize this sooner, is that that the property of a domain being lens-shaped is usually expressed in different terms. Namely, for a Lorentzian manifold $M$, the property of being lens-shaped is equivalent to the existence of a smooth Cauchy time function $f$ (it increases along every future directed timelike curve, the image of the composition of each such curve with $f$ is the whole real line $({-\infty},\infty)$ and each level set is a Cauchy surface diffeomorphic to $S$). In other words, the spacetime smoothly and causally factors as $M\cong \mathbb{R}\times S$. Adding a boundary to compactify $S$, if necessary, and rescaling $f$ to make sure its range is $({-1},1)$, it is easy to see that this factorization (or splitting) is equivalent to the property of being lens-shaped, as defined precisely in Willie's answer.
So, the answer part (a) of my question is subsumed by the well known equivalence of global hyperbolicity of $M$ (as defined in terms of timelike curves) to the existence of the smooth causal splitting $M\cong \mathbb{R}\times S$, with $S$ diffeomorphic to a Cauchy surface of $M$. Part (b) is then answered by noting that both $D(S)$ and the union of all lens-shaped domains are maximal under the respective conditions of global hyperbolicity and being lens-shaped and again using the fact that these conditions are equivalent.
Now, the smooth causal splitting property was first established by Geroch (JMP, 1970), though only for Lorentzian manifolds and the splitting was only show to be topological. Again for Lorentzian manifolds, the smoothness was established more recently by Bernal and Sánchez (CMP, 2003). Finally, for more general causal structures as defined by Willie's answer, smooth causal splitting was established very recently by Fathi and Siconolfi (Math Proc CPS, 2011), incidentally using quite different methods from the previous work.
The information above definitely answers my original question. However, if I could, I would mark this answer as correct jointly with the one given earlier by Willie, as it certainly helped greatly.
