Alphabeta Math
Pipeline-generated
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.

Causal kernels, gauge and point fields after wave existence — Examples

1 · Prerequisites

2 · Summary

The companion page records three explicit mathematical checks of the conventions and hypotheses used on em-causal-wave-kernel-prerequisites; all of them carry domain: mathematics and make no empirical claim.

Explicit checks of the causal wave kernel, the gauge conventions and the static retarded limit first specializes the retarded point formulas of Retarded potentials of a point history as the retarded convolution of the point sources, and the off-worldline Lienard-Wiechert fields to the static history z≡0, where the root is s=t−∣x∣/c and the pair reduces to φ=C/∣x∣, A=0, E=Cx/∣x∣3, B=0, and checks that the kernel's retarded-history integral then reproduces the time-independent Poisson kernel 1/(4π∣x−y∣) on each compact observation region once the static source is cut off in time. Second, it performs an explicit Lorenz-gauge transformation in an instance where the Lorenz divergence is the nonzero constant G=1: for φ≡0, A=(x1,0,0) and χ=−∣x∣2/6 one has Wχ=1=G, the gauge transform is Tχ(φ,A)=(0,((2/3)x1,−x2/3,−x3/3)), its Lorenz divergence vanishes and the fields are unchanged, which is the point where the lemma's clause (d) about differences of solutions enters because the explicit gauge function does not carry the zero Cauchy data of the existence construction. Third, it verifies the sharpness of the kernel support at the cone apex and at every nonzero cone point by a nonnegative-test computation, matching the support statement of The retarded wave kernel is a distribution supported on the cone, solves the point-wave equation, and convolves to the retarded solution.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)Open item page →

Explicit checks of the causal wave kernel, the gauge conventions and the static retarded limit

Example

Assume ACω (The Axiom of Countable Choice (ACω)). The following are explicit mathematical checks of the conventions and hypotheses of the items on this page; no measurement, physical field identification or empirical claim is made.

(i) Static specialization. Take z≡0 (so v∗=0), q∈R, ε0>0 in the setting of Retarded potentials of a point history as the retarded convolution of the point sources, and the off-worldline Lienard-Wiechert fields. Then for x≠0 the root is s=t−∣x∣/c, r=∣x∣, n=x/∣x∣, β=0, κ=1, β˙=0, so the potentials and fields are φ=C/∣x∣, A=0, E=C x/∣x∣3, B=0. Thus the retarded formulas reduce exactly to the Coulomb field with the convention C=q/(4πε0), and the kernel's explicit retarded-history integral reproduces the time-independent Poisson kernel 1/(4π∣x−y∣): for a static spatial source h∈Cc∞(R3) define u(x,t):=14π∫R3h(y)∣x−y∣ dy. Indeed the retarded time is t−∣x−y∣/c and evaluating the static source there leaves h(y) unchanged. This finite integral is the extension of the compact spacetime-source formula by source-time cutoffs on each compact observation region; a time-independent nonzero source is not itself compactly supported in spacetime.

(ii) Explicit Lorenz-gauge transformation. On Ω=R3×R take φ≡0 and A(x,t)=(x1,0,0). Then G(φ,A)=div⁡A=1 and E=−∂tA=0, B=curl⁡A=0. The quadratic function χ(x,t):=−∣x∣2/6 satisfies Wχ=G: indeed ∂t2χ=0 and Δχ=−1, so Wχ=c−2⋅0−(−1)=1=G. Its gauge transform is Tχ(φ,A)=(0, ((2/3)x1,−x2/3,−x3/3)), which satisfies G(Tχ(φ,A))=23−13−13=0 and has the same fields: E(Tχ(φ,A))=0=E(φ,A) and B(Tχ(φ,A))=0=B(φ,A). This checks clauses (b) and (c) of Gauge reachability of Lorenz gauge by the free-space wave solution, with field invariance in an instance where G is a nonzero constant and where the gauge function does not have the zero Cauchy data used in the existence construction of that lemma; by its clause (d), the difference of this χ and the zero-data solution of Wχ=G solves the homogeneous wave equation, which is why both may be used.

(iii) Sharpness of the kernel support at the apex. For a nonnegative ψ∈D(R3×R) with ψ(0,0)>0 one has ⟨K,ψ⟩=14π∫ψ(y,∣y∣/c)∣y∣−1dy>0, so (0,0)∈supp⁡K and the apex is not an artefact of the definition; the same computation with a bump near (y0,∣y0∣/c), y0≠0, shows that every point of the cone is in the support.

Facts & Assumptions

Given: The countable-choice hypothesis, the constants c,q,ε0,C, the static trajectory z≡0, the pair φ≡0, A(x,t)=(x1,0,0), the gauge function χ=−∣x∣2/6, the kernel K of the retarded-wave-kernel item, and a static source h∈Cc∞(R3).

[F1]

For c>0 and C1 z with ∣z′∣≤v∗<c there is exactly one retarded root s of t−s=∣x−z(s)∣/c, with s≤t and equality exactly on the worldline; a Ck trajectory gives a Ck root off the worldline (Global existence, uniqueness and differentiability of the retarded root).

[F2]

In the setting of that item, φ=C/(κr), A=βφ/c, and the fields E=−∇φ−∂tA, B=curl⁡A obey the displayed Lienard-Wiechert formulas; the pairings against the kernel satisfy the exact retarded-convolution identities (Retarded potentials of a point history as the retarded convolution of the point sources, and the off-worldline Lienard-Wiechert fields).

[F3]

For the kernel K and h∈Cc∞(R3×R), (K∗h)(x,t)=∫h(y,t−∣x−y∣/c)(4π∣x−y∣)−1dy is well defined and for a nonnegative test ψ the pairing ⟨K,ψ⟩ is the displayed integral; supp⁡K=C (The retarded wave kernel is a distribution supported on the cone, solves the point-wave equation, and convolves to the retarded solution).

[F4]

For a potential pair, E=−∇φ−∂tA, B=curl⁡A, G=div⁡A+c−2∂tφ, W=c−2∂t2−Δ, and the gauge transform is Tχ(φ,A)=(φ−∂tχ,A+∇χ) (Scalar-vector potential pairs, gauge transformation, Lorenz divergence and the wave expression).

[F5]

Under ACω, if (φ,A) is a C∞ potential pair on a slab, then there is a C∞ gauge function χ with zero Cauchy data and Wχ=G(φ,A), the gauge transform preserves E and B and is in Lorenz gauge, and differences of functions with the same W-image satisfy W(χ1−χ2)=0 (Gauge reachability of Lorenz gauge by the free-space wave solution, with field invariance).

[F7]

Under ACω the polar formula holds for nonnegative Borel functions, a nonnegative measurable function has zero integral exactly when it vanishes almost everywhere, Euclidean balls have positive finite measure, and nonnegative integrals are monotone and scale (Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma, A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere, Euclidean balls have positive finite Lebesgue measure, Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F9]

The Euclidean norm and inner product are those of The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn, and Ck regularity is componentwise (Ck Euclidean maps and diffeomorphisms).

[A1]

The Axiom of Countable Choice ACω (The Axiom of Countable Choice (ACω)).

Verification

technique · direct
1.1givenF1F2F4F6F9

Static specialization (i). With z≡0 the root equation reads t−s=∣x∣/c, whose unique solution is s=t−∣x∣/c; then R=x, r=∣x∣, n=x/∣x∣, β=0, N=0, κ=1, D=∣x∣ and β˙=0. By [F2] the potentials are φ=C/∣x∣ and A=0 (since β=0), and the field formulas give E=C(1−0)(n−0)/(1⋅∣x∣2)=Cx/∣x∣3 and B=n×E/c=(C/c)(n×n)/∣x∣2=0, using n×n=0.

1.2givenF3F7F8A1

Static Poisson kernel (i). Let h∈Cc∞(R3), fix a compact observation region Q0⊆R3×R and note that for (x,t)∈Q0 and y in the support of h the retarded time s=t−∣x−y∣/c stays in a bounded interval; choose a smooth nonnegative time cutoff σ equal to one on that interval with compact support, and put h#(x,t):=σ(t)h(x)∈Cc∞(R3×R), which agrees with the time-independent extension of h on the contributing region. By [F3], (K∗h#)(x,t)=∫h#(y,t−∣x−y∣/c)(4π∣x−y∣)−1dy=14π∫h(y)/∣x−y∣ dy on Q0, since σ equals one at the retarded times and the static source does not depend on time; the remaining integral is finite: h is bounded with compact support, the polar formula bounds its absolute integral on B1(x) by ∥h∥∞∫B1(x)∣x−y∣−1dy<∞, and on the remaining compact support one has ∣x−y∣−1≤1, giving an upper bound ∥h∥∞ times a finite ball volume. This is the stated extension of the compact spacetime-source formula by source-time cutoffs; the uncut static source is not compactly supported in spacetime.

1.3givenF4F5F6F9

The gauge transformation (ii). For φ≡0 and A=(x1,0,0): div⁡A=∂1x1=1, so G=1; curl⁡A=0; E=−∂tA=0. For χ=−∣x∣2/6: ∂t2χ=0, and Δχ=−16Δ∣x∣2=−1 with Δ∣x∣2=6, so Wχ=c−2⋅0−(−1)=1=G. Since ∇χ=(−x1/3,−x2/3,−x3/3), the gauge transform is Tχ(φ,A)=(0−∂tχ, A+∇χ)=(0,((2/3)x1,−x2/3,−x3/3)), whose divergence is 23−13−13=0 and whose curl vanishes because it is the gradient of 13x12−16x22−16x32 by the curl-of-gradient theorem; hence E(Tχ(φ,A))=−∇0−∂t(0,…)=0=E(φ,A) and B(Tχ(φ,A))=0=B(φ,A), and the transformed pair is in Lorenz gauge. This instantiates clauses (b) and (c) of [F5] with a nonzero constant G and a gauge function that does not have the zero Cauchy data of the existence construction; by clause (d) of [F5], W(χ−χ0)=1−1=0 for the zero-data solution χ0 of Wχ0=1, so the two are compatible.

2.1givenF3F7F8A1∎

Sharpness at the apex (iii). Let 0≤ψ∈D(R3×R) with ψ(0,0)>0. By continuity and ψ(0,0)>0 there are a>0 and δ>0 with ψ(y,∣y∣/c)≥a whenever ∣y∣<δ. On that ball y↦ψ(y,∣y∣/c)/∣y∣ is nonnegative and bounded below by a/∣y∣, so by the polar formula and the positivity of the integral of a nonnegative measurable function that is positive on a set of positive measure, ⟨K,ψ⟩=14π∫ψ(y,∣y∣/c)∣y∣−1dy≥a4π∫Bδ∣y∣−1dy=a4π⋅σ(S2)δ22>0; [F8] supplies such nonnegative bumps supported in every prescribed neighbourhood of the origin, so this nonvanishing proves (0,0)∈supp⁡K. For y0≠0 and a nonnegative bump ψ positive at (y0,∣y0∣/c) with support in a small ball, continuity gives ψ(y,∣y∣/c)≥a>0 on a neighbourhood of y0, while ∣y∣−1≥1/(2∣y0∣) there, and the same computation gives ⟨K,ψ⟩>0, so every such cone point lies in the support in accordance with the support computation of [F3]. Both computations use only nonnegative tests, and no factorization of an arbitrary test into radial and time factors is assumed.

Remarks

  • Consistency, not evidence. These are internal consistency checks of conventions and hypotheses; they neither prove any physical field identification nor test any model against observation.

  • Choice accounting. ACω enters only through the polar formula and the positivity criteria of [F7] and through the kernel item [F3]; the algebraic computations are choice-free.

Sources