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 oscillator media and passivity — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Continuity and the Sharp Fundamental Theorem of Calculus
- Analyticity of Holomorphic Functions; Liouville and Morera
- Arc Length and Rectifiable Curves
- Areas of Elementary Plane Figures
- Banach-Space Differential Calculus and Banach Manifolds
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Linear Operators and Quotient Spaces
- Bounded Variation and the Riemann–Stieltjes Integral
- Causal oscillator media and passivity
- Cm Math Central
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Coordinate and Path Transport
- Complex Differentiability and the Cauchy–Riemann Equations
- Complex Lp Spaces and Test-Function Conventions
- Complex Norms and Realification
- Complexification, Realification and Real Structures
- Connectedness
- 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
- Contour Integration
- 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
- Differentiation of Monotone Functions and the Vitali Covering Theorem
- Discrete de Rham complexes and edge-element foundations
- 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 Causal Response And Radiation Prerequisites
- Em Elementary Mathematical Prerequisites
- Em Expanded Analysis Prerequisites
- Euclidean Surface Measure, Divergence, and Green Identities
- Exterior Powers, Orientation and Hodge Duality
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite Dimensional Normed Spaces and Riesz Lemma
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fubini and Change of Variables
- Fundamental Trigonometric Identities
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Goursat's Theorem and Cauchy's Theorem in a Convex Domain
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hausdorff via the Diagonal
- Hereditary and Productive Behaviour of the Separation Axioms
- Hilbert Space Geometry and Riesz Representation
- Homotopy and Homotopy Equivalence
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Line Integrals and the Gradient Theorem
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Lorentz Transformations
- Manifolds with Boundary Collars and Orientations
- Material response and stationary interfaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- 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
- Orthonormal Bases, Parseval and Fourier Series
- Outer Measure and the Caratheodory Extension Theorem
- Partitions of Unity and Paracompactness
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Primitives and postulates
- 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
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Simply Connected Plane Domains: the Grand Equivalence
- Sine, Cosine, and the Definition of Pi
- Smooth Manifolds and Smooth Maps
- Spacetime Primitives
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- Tensor Fields Exterior Algebra and Differential Forms
- Tensor Products of Modules
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- 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 Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Radon Nikodym Theorem and Lebesgue Decomposition
- 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 ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vacuum waves and polarization
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Derivatives and Sobolev Spaces
- Weak fields, boundary power and dissipative uniqueness
- Worldlines And Clocks
2 · Summary
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
Phase and group speeds are not causal fronts
An exact narrowband dispersion calculation for one passive, damped Lorentz medium at a specified frequency. It shows that the local derivative of the real wave-number phase can be negative in this lossy model; it assigns no signal-front speed, energy velocity, empirical observation or universal group-velocity bound.
Statement
Take the finite Lorentz response with , , one oscillator in F m s, and damping in s, where is an angular frequency in s. For angular frequency in s, let ; its relative absolute permittivity is
For each , define to be the dimensionless square root of with positive real and positive imaginary parts, and define the complex wave number in m for a harmonic field with spatial factor , where is in m, is in m s, and is the propagation direction. Use standard right-handed Cartesian coordinates and let , . Fix a real amplitude in V m and, with the real-part plane-wave convention, explicitly extended here to complex , define the fields
These are real maps . Set and
the harmonic particular displacement response specified by the Lorentz susceptibility theorem. This is a formal source-free transverse bulk mode; no boundary condition or finite-energy property is asserted. The imaginary part of gives attenuation along . Define the narrowband group-delay derivative per unit length to be in s m; it is a local derivative of phase with respect to angular frequency. For a real temporal signal , define its support by ; if this support is nonempty and bounded below, its front time is . The nonzero harmonic histories at each fixed spatial point are eternal and have support , hence have no front time. At , the group-delay derivative is negative. This derivative does not by itself determine a pulse's support front, which is a property of its full time-dependent signal.
Statement references
Analytic susceptibility and dispersion restrictions
Real plane-wave fields encoded by complex amplitudes
Declared material-closure branches: linear nondispersive Ohmic response and the causal memory branch
The macroscopic Maxwell equations in terms of D, H and the free sources
Framework-local SI units, the vacuum constants and the exact/measured status of their values
Facts & Assumptions
Given: Countable Choice and Dependent Choice, the one-oscillator Lorentz closure with the parameter choices in the Statement, the SI relation , and the source-free homogeneous transverse Maxwell branch. Use complex amplitudes only as the standard encoding of real harmonic fields.
Countable Choice and Dependent Choice are carried by the analytic-response supplier used for the passive Lorentz susceptibility (The Axiom of Countable Choice (), The axiom of dependent choice: a relation in which every element is related to something admits an -indexed chain, Analytic susceptibility and dispersion restrictions).
In the material rest frame, the absolute oscillator susceptibility is and the absolute permittivity is ; with the oscillator response is causal and has the stated analytic transfer under the integrable-kernel hypotheses (Analytic susceptibility and dispersion restrictions).
For zero free sources, the smooth macroscopic Maxwell equations are , , and , with the constitutive quantities of the material model (The macroscopic Maxwell equations in terms of D, H and the free sources, clause (b); Declared material-closure branches: linear nondispersive Ohmic response and the causal memory branch).
The SI constants satisfy with (Framework-local SI units, the vacuum constants and the exact/measured status of their values, clause (a)).
Every positive real number has a unique positive square root; the product rule and total-derivative chain rule hold under the displayed smooth rational functions (Square roots exist: a unique with ; the positives are , Sums, scalar multiples, products and quotients: , , , and when , The chain rule for total derivatives: ).
The coordinate identity holds for real vectors and extends to complex vectors because both sides are polynomial in their coordinates; all complex dot and cross products here are extended complex-bilinearly (The vector triple product identity , The Euclidean inner product on ).
The complex exponential is defined by its everywhere-convergent power series and has derivative itself; the chain rule differentiates its real-linear spatial and temporal phase (The complex exponential by its power series, The complex exponential is entire and its complex derivative is itself, The chain rule for total derivatives: ).
The plane-wave definition uses the real-part encoding , on ; this Statement specifies its extension to complex , defines the resulting real field maps, and uses complex-bilinear dot and cross products (Real plane-wave fields encoded by complex amplitudes).
Verification
At a real frequency , set and substitute the temporal factor and spatial factor of the Statement into [A2]; [F5] differentiates these phases, and [F6] fixes the real-field encoding, extended to this complex wavevector. The two curl equations give and , with . For a transverse amplitude , [F4] gives . Since , ; [F1] and the definition of imply on the selected square-root branch. Conversely, for this root take , and . Then and . Also , so the divergence amplitudes of and vanish. Thus the fields in the Statement realize the source-free transverse harmonic mode. As , attenuates along .
At , , hence . Write the selected root as with . Equating real and imaginary parts gives and , hence and . For general , write ; rationalization gives . Put . Then , so and both and are positive. Define and . These satisfy and ; since , , so . For any other root with , the same equations imply , hence and , ; positivity gives , . The rational functions are continuous for ; the positive square root is continuous at each positive , since for . Applying this to and to the positive arguments proves that , hence , are continuous near . Therefore , and the difference quotient identity gives . Set . Viewing as , the real product rule applied to gives . Thus at , and gives , since and .
From and , the chain and product rules give . At , this is negative by step 1.2 and . Thus the conventional narrowband group-delay derivative is negative for this lossy causal model at that frequency. Its value does not give the support-front time of a pulse, which depends on the full time-domain signal; no front-speed or universal group-speed claim follows.
Matter energy survives zero instantaneous polarization
A single allowed oscillator state in the undamped Lorentz model. It illustrates the model's positive kinetic material-energy term when the instantaneous polarization vanishes; it reports no experiment and makes no claim beyond the stated constitutive model.
Statement
In the one-oscillator Lorentz model, take an undamped oscillator with in F m s and in s. At a time , compare two allowed states with the same instantaneous fields , , , polarization , and therefore displacement : in the first state set , and in the second set for any fixed nonzero real vector in A m. The second state has oscillator energy density in J m, while the first has zero oscillator energy. Thus the instantaneous pair alone does not determine the full stored energy in this dispersive model.
Statement references
Facts & Assumptions
Given: Countable Choice, one undamped Lorentz oscillator with , ; its state at consists of and ; take and at that instant.
The adopted oscillator model permits the initial polarization and polarization-velocity state and uses (Finite Lorentz oscillator closure).
For this undamped Lorentz state, the material energy density is , added to the positive electromagnetic field energy (Augmented energy and passive absorption, Lorentz branch).
The Euclidean squared norm is positive for every nonzero vector: when (The Euclidean inner product on ).
Countable Choice is an explicit hypothesis of the finite-energy oscillator theorem used here (The Axiom of Countable Choice (), Augmented energy and passive absorption).
Verification
In the first state , so [F1] gives zero oscillator energy. In the second state , so [F1] gives by [F2] and . Both states have and , hence the same , and both have ; they therefore have identical instantaneous data but different total stored energies.
The comparison is between allowed model states at one time; it is not an observed outcome or a claim about microscopic material energy. Hence the full oscillator energy is not a function of the instantaneous pair alone.
Sources
- David Tong, Electromagnetism, University of Cambridge Part II Mathematical Tripos lecture notes (236-page complete text)
- Niklas Beisert, Elektrodynamik, ETH Zurich 2024 FS complete lecture script
- MIT OpenCourseWare 6.007, Electromagnetic Energy: From Motors to Lasers, Lecture 22: Interaction of atoms and EM waves (Lorentz oscillator)