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
- Absolute and Conditional Convergence; Rearrangement; Products
- Areas of Elementary Plane Figures
- Binary Operations, Monoids, Groups and Subgroups
- Causal kernels, gauge and point fields after wave existence
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Em Elementary Mathematical Prerequisites
- Em Expanded Analysis Prerequisites
- Em Wave Equation Prerequisites
- Euclidean Surface Measure, Divergence, and Green Identities
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Harmonic Functions and Mean Values in Rn
- Hausdorff via the Diagonal
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper Integrals
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Densities and Radon Volume on Manifolds
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Normed and Banach Spaces
- Norming and Separation under Hahn–Banach
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Partial Differential Equations and Characteristics
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Radon Measures and the Riesz Markov Kakutani Theorem
- Regular Surfaces and Surface Integrals
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Simple Field Extensions and the Construction of the Complex Numbers
- Smooth Partitions of Unity and Exhaustions
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Divergence Theorem and Classical Stokes
- The Exponential Function
- The Fundamental Theorems of Calculus
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Lebesgue and Riemann Integrals Compared
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Maximal Function and Lebesgue Differentiation
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Wave Energy, Finite Propagation and Huygens' Principle
- Wave Equation Representation Formulas
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 , where the root is and the pair reduces to , , , , and checks that the kernel's retarded-history integral then reproduces the time-independent Poisson kernel 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 : for , and one has , the gauge transform is , 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
Explicit checks of the causal wave kernel, the gauge conventions and the static retarded limit
Example
Assume (The Axiom of Countable Choice ()). 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 (so ), , 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 the root is , , , , , , so the potentials and fields are , , , . Thus the retarded formulas reduce exactly to the Coulomb field with the convention , and the kernel's explicit retarded-history integral reproduces the time-independent Poisson kernel : for a static spatial source define . Indeed the retarded time is and evaluating the static source there leaves 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 take and . Then and , . The quadratic function satisfies : indeed and , so . Its gauge transform is , which satisfies and has the same fields: and . 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 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 solves the homogeneous wave equation, which is why both may be used.
(iii) Sharpness of the kernel support at the apex. For a nonnegative with one has , so and the apex is not an artefact of the definition; the same computation with a bump near , , shows that every point of the cone is in the support.
Facts & Assumptions
Given: The countable-choice hypothesis, the constants , the static trajectory , the pair , , the gauge function , the kernel of the retarded-wave-kernel item, and a static source .
For and with there is exactly one retarded root of , with and equality exactly on the worldline; a trajectory gives a root off the worldline (Global existence, uniqueness and differentiability of the retarded root).
In the setting of that item, , , and the fields , 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).
For the kernel and , is well defined and for a nonnegative test the pairing is the displayed integral; (The retarded wave kernel is a distribution supported on the cone, solves the point-wave equation, and convolves to the retarded solution).
For a potential pair, , , , , and the gauge transform is (Scalar-vector potential pairs, gauge transformation, Lorenz divergence and the wave expression).
Under , if is a potential pair on a slab, then there is a gauge function with zero Cauchy data and , the gauge transform preserves and and is in Lorenz gauge, and differences of functions with the same -image satisfy (Gauge reachability of Lorenz gauge by the free-space wave solution, with field invariance).
, and for ; divergence and curl are linear and computed from the first partial derivatives (The Laplacian of a function and of a vector field, Divergence and curl of a vector field, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case, Sums, scalar multiples, products and quotients: , , , and when , The curl of the gradient of a function vanishes, Divergence and curl are linear and satisfy the scalar product rules).
Under 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 exactly when it vanishes almost everywhere, Euclidean balls have positive finite Lebesgue measure, Monotonicity and nonnegative homogeneity of the nonnegative integral).
Compact subsets of are bounded and closed (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line), and for a compact set inside an open set there is a smooth compact cutoff equal to one near it (Test function cutoffs and euclidean localization).
The Euclidean norm and inner product are those of The Euclidean inner product on , and regularity is componentwise ( Euclidean maps and diffeomorphisms).
The Axiom of Countable Choice (The Axiom of Countable Choice ()).
Verification
Static specialization (i). With the root equation reads , whose unique solution is ; then , , , , , , and . By [F2] the potentials are and (since ), and the field formulas give and , using .
Static Poisson kernel (i). Let , fix a compact observation region and note that for and in the support of the retarded time stays in a bounded interval; choose a smooth nonnegative time cutoff equal to one on that interval with compact support, and put , which agrees with the time-independent extension of on the contributing region. By [F3], on , since equals one at the retarded times and the static source does not depend on time; the remaining integral is finite: is bounded with compact support, the polar formula bounds its absolute integral on by , and on the remaining compact support one has , giving an upper bound 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.
The gauge transformation (ii). For and : , so ; ; . For : , and with , so . Since , the gauge transform is , whose divergence is and whose curl vanishes because it is the gradient of by the curl-of-gradient theorem; hence and , and the transformed pair is in Lorenz gauge. This instantiates clauses (b) and (c) of [F5] with a nonzero constant and a gauge function that does not have the zero Cauchy data of the existence construction; by clause (d) of [F5], for the zero-data solution of , so the two are compatible.
Sharpness at the apex (iii). Let with . By continuity and there are and with whenever . On that ball is nonnegative and bounded below by , 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, ; [F8] supplies such nonnegative bumps supported in every prescribed neighbourhood of the origin, so this nonvanishing proves . For and a nonnegative bump positive at with support in a small ball, continuity gives on a neighbourhood of , while there, and the same computation gives , 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. enters only through the polar formula and the positivity criteria of [F7] and through the kernel item [F3]; the algebraic computations are choice-free.