Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
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.

Truncated wave cones: convexity, piecewise C1 presentation and outward normals

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Let n≥1, c>0, x0∈Rn, t0>0 and 0<t1<t2<t0. In space-time Rn+1 with coordinates (x,t) (Euclidean, so (0,−1) and (0,1) below have zero space part) put

K(t1,t2):={(x,t):t1<t<t2, ∣x−x0∣<c(t0−t)}.

Then:

(i) K(t1,t2) is a nonempty open bounded convex set (A convex subset of Rm contains every line segment between two of its points);

(ii) it has the finite piecewise C1 presentation of Specified finite piecewise C1 boundary presentations whose non-edge faces are the bottom disk B‾c(t0−t1)(x0)×{t1}, the top disk B‾c(t0−t2)(x0)×{t2} and the lateral frustum L:={(x,t):∣x−x0∣=c(t0−t), t1≤t≤t2}, the edge set being the two boundary circles Sc(t0−t1)(x0)×{t1} and Sc(t0−t2)(x0)×{t2};

(iii) the corresponding outward unit normals are (0,−1) on the bottom disk, (0,1) on the top disk, and νlat(x,t)=(x−x0∣x−x0∣, c)/1+c2 at points of L;

(iv) the closed backward cone K−(x0,t0)={(x,t):0≤t≤t0, ∣x−x0∣≤c(t0−t)} is compact and convex, and K(t1,t2) is its interior intersected with the slab {t1<t<t2}.

All statements are also true at c=1, and n=1 is the characteristic trapezium.

Facts & Assumptions

Given: ACω; n≥1, c>0, x0∈Rn, t0>0 and 0<t1<t2<t0; the Euclidean structure of The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn on Rn+1; the function φ:Rn+1→R, φ(x,t):=∣x−x0∣+ct.

[F1]

A finite piecewise C1 presentation of a nonempty bounded open Ω consists of compact faces covering its boundary, each a compact Borel subset of a regular C1 hypersurface patch, together with a compact edge set E, and it requires: Sj∩E surface-null in each face, the edge set to contain the relative face boundaries and all overlaps, the boundary to be locally a single C1 graph with Ω on one side off E, and each face to carry its actual outward unit normal off E. (Specified finite piecewise C1 boundary presentations)

[F2]

On a compact embedded C1 hypersurface the chart integral is a finite Borel measure independent of the charts; in graph coordinates X(y)=(y,h(y)) its density is 1+∣Dh(y)∣2, and on a one-sided domain boundary the outward unit normal agrees on chart overlaps. (Chart and partition independence of surface measure)

[F4]

For every real α the function s↦sα is differentiable on (0,∞) with derivative αsα−1. (Continuity and derivatives of positive-base real powers)

[F5]

Chain rule: D(G∘H)(a)=DG(H(a))∘DH(a) for composable totally differentiable maps. (The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a))

[F6]

Finite sums and products of Ck Euclidean maps are Ck, and composites of composable Ck maps are Ck. (Ck Euclidean maps are closed under componentwise algebra and composition)

[F7]

For n≥1 and r>0, ∣Br∣=ωn−1rn/n, with 0<ωn−1<∞ (Sphere and ball measures scale in Rn). Consequently every positive-radius sphere has Lebesgue measure zero: for 0<ε<r, it lies in Br+ε∖Br−ε, whose measure is ωn−1((r+ε)n−(r−ε)n)/n; monotonicity and finite additivity bound its measure by this quantity, and letting ε↓0 gives zero.

[F8]

A Lipschitz self-map of Rn carries λn-null sets to λn-null sets, under ACω. (A Lipschitz self-map of Rn carries Lebesgue null sets to Lebesgue null sets)

[F9]

A subset U⊆Rm is convex when (1−t)x+ty∈U for all x,y∈U and t∈[0,1]. (A convex subset of Rm contains every line segment between two of its points)

Proof

1.1givenF3F9algebra

The function φ is convex: for p=(x,t), q=(y,s)∈Rn+1 and λ∈[0,1], writing u:=(1−λ)(x−x0) and v:=λ(y−x0), the triangle inequality and absolute homogeneity of the Euclidean norm [F3] give ∣u+v∣≤(1−λ)∣x−x0∣+λ∣y−x0∣, while c((1−λ)t+λs)=(1−λ)ct+λcs by linearity, so φ((1−λ)p+λq)≤(1−λ)φ(p)+λφ(q); consequently K(t1,t2)={φ<ct0}∩{t1<t<t2} is convex, because both sets are convex: for {φ<ct0} this is the inequality just proved applied to two points with values below ct0, and the slab is defined by two affine conditions [F9].

2.1givenstep 1.1F3algebra

Basic topological properties: K(t1,t2) is open since [F3] gives ∣∣x−x0∣−∣y−x0∣∣≤∣x−y∣, so φ and the coordinate t are continuous and the half-lines (t1,t2) and (−∞,ct0) are open; it is nonempty because (x0,(t1+t2)/2) has φ=0+c(t1+t2)/2<ct0 and lies in the slab; it is bounded because every point has t1<t<t2 and ∣x−x0∣<c(t0−t)<ct0. This is (i).

3.1givenstep 2.1algebra

The boundary decomposition: ∂K(t1,t2)=Db∪Dt∪L with Db:=B‾c(t0−t1)(x0)×{t1}, Dt:=B‾c(t0−t2)(x0)×{t2} and L as in the statement; the only overlaps are Db∩L=Sc(t0−t1)(x0)×{t1} and Dt∩L=Sc(t0−t2)(x0)×{t2}, and Db∩Dt=∅. Indeed ∂{φ<ct0}⊆{φ=ct0} and ∂{t1<t<t2}⊆{t=t1}∪{t=t2}, and K is the intersection of these three open sets, so a boundary point of K lies in one of the three level sets; conversely a point p=(x,t) with φ(p)=ct0 and t∈(t1,t2) (a point of L) has p+δ(x−x0,c)∉K and p−δ(x−x0,c)∈K for small δ>0, while a point with t=t1 and ∣x−x0∣<c(t0−t1) has p−δet∉K and p+δet∈K, and at a rim point ∣x−x0∣=c(t0−t1), t=t1, the points (x0+t0−t1−2εt0−t1(x−x0), t1+ε) lie in K for 0<ε<min⁡((t0−t1)/2,t2−t1), since their spatial radius is c(t0−t1−2ε)<c(t0−t1−ε), and tend to p; at a top rim point (x,t2) the points (x,t2−ε) lie in K for 0<ε<t2−t1 and tend to it, while the interior of the top disk is approached vertically.

4.1F4F5F6step 3.1algebra

Each face is a compact Borel subset of a regular C1 hypersurface patch: Db and Dt are closed balls in the hyperplanes {t=ti}, which are graphs of the constant (hence C1) functions over Rn with nonvanishing gradient of (x,t)↦t; the lateral face lies in the graphic hypersurface {(y,h(y)):y∈O} where O:=Rn∖{x0} and h(y):=t0−∣y−x0∣/c, which is C1 because y↦⟨y−x0,y−x0⟩ is a finite sum of products of the C1 coordinate functions [F6], the square root is differentiable on (0,∞) with derivative 12s−1/2 [F4], and the chain rule [F5] applies on the open set where the inner value is positive, namely O.

5.1F1F2F7F8F10step 3.1step 4.1

The presentation is verified with E:=(Sc(t0−t1)(x0)×{t1})∪(Sc(t0−t2)(x0)×{t2}): the three faces are closed bounded Borel subsets, hence compact by [F10], of regular C1 patches by step 4.1 and cover ∂K by step 3.1; E⊂∂K is compact and contains the relative boundaries of the faces in their patches (the rim circles of the two disks and the two boundary circles of the annulus {c(t0−t2)≤∣y−x0∣≤c(t0−t1)} parametrizing L) and all pairwise overlaps, which by step 3.1 are exactly the two rim circles; off E the boundary is locally a single C1 graph with K on one side, namely t=ti over a small ball in the interior of each disk with K on the side t>t1, respectively t<t2, and t=h(y) over a small ball in O for interior points of L, with K locally {t<h(y)} by the definition of K; and Sj∩E is surface-null in each face: on a disk the surface measure is n-dimensional Lebesgue measure transported by the graph chart [F2], whose rim is a sphere of positive radius, null by [F7] and [F8] applied to the homothety z↦x0+rz (and for n=1 a two-point set), while on L the graph density is the constant 1+1/c2 because ∣Dh∣=1/c on O, so a Borel subset of L is surface-null exactly when its y-projection is λn-null [F2], and the projection of E∩L is the union of two positive-radius spheres, null by [F7] and [F8]. Thus K(t1,t2) has the specified finite piecewise C1 presentation with faces Db,Dt,L and edge set E: this is (ii).

5.2givenF2step 4.1algebra

The outward normals: on the bottom disk the region lies locally in {t>t1}, so the outward unit normal is (0,−1); on the top disk it is (0,1); on L the field ∇φ=((x−x0)/∣x−x0∣,c) is continuous and nonvanishing near L because ∣x−x0∣=c(t0−t)≥c(t0−t2)>0 there, K is locally the side {φ<ct0} and L⊆{φ=ct0}, so the outward unit normal is ∇φ/∣∇φ∣=((x−x0)/∣x−x0∣,c)/1+c2, using the outward-normal convention for one-sided graph boundaries [F2] and the gradient of The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case. This is (iii).

6.1step 1.1step 2.1F9F10algebra∎

The closed cone: K−={φ≤ct0}∩{t≥0}∩{t≤t0} is closed because φ is continuous, bounded because 0≤t≤t0 and ∣x−x0∣≤ct0, and thus compact by [F10], and convex because the sublevel set is convex by the inequality of step 1.1 and the two half-spaces are convex [F9]; its interior is {0<t<t0, φ<ct0}: the inclusion ⊇ is openness of the right-hand set inside K−, and conversely a point with φ=ct0 is not interior, since for z:=(x0,0) with φ(z)=0<ct0 the points r(σ):=z+σ(p−z), σ>1, satisfy p=1σr(σ)+(1−1σ)z, so convexity gives φ(p)≤1σφ(r(σ))+(1−1σ)φ(z) and hence φ(r(σ))≥ct0+(σ−1)(ct0−φ(z))>ct0, with r(σ)→p as σ↓1; a point with t=0 or t=t0 is not interior because p−δet, respectively p+δet, lies outside K− for every δ>0. Intersecting int⁡K− with the slab {t1<t<t2}⊆{0<t<t0} gives exactly K(t1,t2), which is (iv).

Remarks

The outward normals of (iii) supply the geometric data used in The energy identity on a truncated wave cone.

Depends on

Used by

Dependency tree · two levels

88 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources