Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck pending
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Continuity and strict monotonicity of the chronological volume functions in a globally hyperbolic manifold

Statement

Assume Countable Choice and Dependent Choice (The Axiom of Countable Choice (ACω), The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain) for the absolutely continuous causal-curve calculus and the supplied causal results used below. Let (M,g,N) be a globally hyperbolic time-oriented smooth Lorentzian four-manifold (Chronology, causality, strong causality, global hyperbolicity and time functions clause (c)) and let μ be the finite volume measure of Existence of a positive smooth volume density of total mass one on a smooth Lorentzian four-manifold, with μ(M)=1, μ(O)>0 for every nonempty open O and μ(E)=0 for every chart-Lebesgue-null Borel set E. Then:

(a) for every sequence pk→p in M, the indicator functions 1I−(pk) converge μ-almost everywhere to 1I−(p), and μ(I−(pk))⟶μ(I−(p)), with the same statement for I+;

(b) the maps p↦μ(I−(p)) and p↦μ(I+(p)) are continuous on M;

(c) J−(p)=I−(p)‾ and μ(J−(p))=μ(I−(p)) for every p, and dually J+(p)=I+(p)‾ and μ(J+(p))=μ(I+(p));

(d) if p≪q then μ(I−(p))<μ(I−(q)),μ(I+(p))>μ(I+(q)).

Facts & Assumptions

Given: A globally hyperbolic (M,g,N), the volume measure μ, a point p∈M and a sequence pk→p.

[L1]

(M,g,N) is strongly causal; hence no nonconstant future causal curve has equal endpoints: a nonconstant closed causal curve through x has an image point y≠x. Take the open neighborhood U=M∖{y} of x (the manifold is Hausdorff). For every V with x∈V⊆U, the closed curve starts and ends in V but passes through y∉U, violating the strong-causality requirement (Chronology, causality, strong causality, global hyperbolicity and time functions clauses (b) and (c)).

[L2]

The causal relation is closed and J±(K) is closed for every compact K (In a globally hyperbolic manifold the causal relation is closed and truncated causal cones over compact sets are compact clauses (a) and (b)).

[L3]

Openness of chronology: I±(x) is open and the set {(y,z):y≪z} is open (Openness of the chronological future and past, openness of the chronological relation, and closure of future and past sets clauses (a) and (b)). Transitivity of ≤ and ≪ (Chart independence, concatenation, reparametrization and transitivity for causal curves clauses (d) and (f)). Push-up: a≪b, b≤c implies a≪c, and dually (The push-up rule: p << q and q <= r imply p << r, together with the timelike-piece criterion clauses (a) and (b)).

[L4]

I−(p) is a past set: if x≪y∈I−(p) then x≪p by transitivity, so I−(I−(p))⊆I−(p); it is open by [L3]. The boundary of the open past set I−(p) is an achronal boundary in the sense of Future sets, past sets, achronal boundaries and their elementary properties clause (b) (apply that definition in the time reverse), hence is μ-null by Achronal boundaries are locally Lipschitz graphs, topological hypersurfaces and null for smooth volume densities clause (d), whose hypotheses and conclusion are invariant under reversing the time orientation; moreover J−(p)=I−(p)‾, because J−(p) is closed by [L2], contains I−(p), and every x∈J−(p) is a limit of points x′∈I−(p): choose x′ on a past timelike geodesic segment through x ([L5]), so that x′≪x≤p, and apply push-up to get x′≪p.

[L5]

Through every point x there are past and future timelike geodesic segments: for every sufficiently small ε>0 the points exp⁡x(−εNx) and exp⁡x(εNx) are defined and satisfy exp⁡x(−εNx)≪x≪exp⁡x(εNx) (Observers, rest spaces and the spatial projection at an event, The geodesic initial-value problem and the exponential map of the metric-selected connection clauses (a) and (d), Covariant differentiation along curves: metric pairing, parallel transport and geodesic speed clause 3, Causal curves, chronological and causal reachability, and inextendibility clause (b)).

[L6]

Dominated convergence: if ∣fk∣≤g with ∫g<∞ and fk→f almost everywhere, then ∫fk→∫f; here μ(M)=1 so the constant 1 is integrable (Dominated convergence, Existence of a positive smooth volume density of total mass one on a smooth Lorentzian four-manifold clause (a)).

Proof

technique · direct
1.1L3given

(Pointwise lower bound.) If q∈I−(p), that is, q≪p, then by openness of the chronological relation [L3] there is k0 with q≪pk for all k≥k0; hence 1I−(pk)(q)=1 eventually and lim inf⁡k1I−(pk)(q)≥1=1I−(p)(q).

1.2L2given

(Pointwise upper bound outside J−(p).) If q∉J−(p), that is, q≰p, then q∉I−(pk) for all sufficiently large k: otherwise q≪pkj for infinitely many j, so q≤pkj, and closedness of the causal relation [L2] applied to pkj→p gives q≤p, a contradiction. Hence lim sup⁡k1I−(pk)(q)≤1J−(p)(q).

2.1step 1.1step 1.2L4L6given

(Almost-everywhere convergence.) By steps 1.1 and 1.2, for every q the limit of the indicators exists and equals 1I−(p)(q) whenever q∈I−(p) or q∉J−(p); the exceptional set is J−(p)∖I−(p)⊆∂I−(p), which is μ-null by [L4]. Hence 1I−(pk)→1I−(p) μ-almost everywhere. Since all indicators are bounded by the μ-integrable constant 1, dominated convergence [L6] gives μ(I−(pk))→μ(I−(p)). The same argument in the time reverse gives the statement for I+.

3.1step 2.1

(Continuity.) Clause (b) is the sequential characterization of continuity of p↦μ(I±(p)), since the limits are the values at the limit point for every sequence pk→p; it is clause (a) read as a statement about all sequences.

3.2L4L5step 2.1

(Closures and measure of the closed cones.) J−(p)=I−(p)‾ and both have equal μ-measure by [L4], because J−(p)=I−(p)‾=I−(p)∪∂I−(p) with the boundary null; dually for J+(p).

4.1step 3.2L1L2L3given

(Strict monotonicity.) Let p≪q and choose a future timelike curve λ:[0,1]→M with λ(0)=p, λ(1)=q; put r:=λ(1/2), so that p≪r≪q by transitivity [L3]. If x≪p then x≪q, so I−(p)⊆I−(q). The point r lies in I−(q) but not in J−(p): otherwise r≤p together with p≪r would give a nonconstant closed future causal curve through p (concatenating a timelike curve from p to r with a causal curve from r to p), contradicting [L1]. Since J−(p) is closed [L2], the open set I−(q)∖J−(p) containing r has positive μ-measure; by additivity and monotonicity of μ, μ(I−(q))≥μ(I−(p))+μ(I−(q)∖J−(p))>μ(I−(p)). Dually, I+(q)⊆I+(p) and r∈I+(p)∖J+(q) is an interior point of an open subset of I+(p)∖I+(q), so μ(I+(q))<μ(I+(p)).

5.1step 2.1step 3.1step 3.2step 4.1∎

(Conclusion.) Clauses (a), (b), (c), and (d) follow respectively from steps 2.1, 3.1, 3.2, and 4.1.

Remarks

  • The role of global hyperbolicity. Strong causality is used only to exclude closed causal curves (step 4.1) and closedness of the causal relation (steps 1.2 and 5.1) is used to keep the limit-superior set inside J−(p). Neither the Cauchy property nor compactness of the diamonds is used directly, and both conclusions remain true for causally simple spacetimes; the global-hyperbolic setting is the one supplied by the previous items of this page.

  • Why almost everywhere is enough. The volume functions are integrals of indicators, so pointwise convergence on a full-measure set suffices; the exceptional set J−(p)∖I−(p) is exactly the achronal boundary of I−(p), which is a local Lipschitz graph and hence null for μ.

  • Use. Clauses (a)-(c) enter the proof that the volume time function is continuous in The Geroch volume function: a continuous strictly increasing time function whose levels are Cauchy sets, and clause (d) supplies its strict monotonicity.

Depends on

Dependency tree · 2 levels

Sources