Analysis

Motivation

In quantum mechanics an observable is a self-adjoint operator $A$ on a complex Hilbert space $\mathfrak H$, and the dynamics is the Schrödinger equation $i\,\tfrac{d}{dt}\psi(t) = H\psi(t)$. In finite dimensions the solution is the matrix exponential $e^{-itH}\psi(0)$, computed by diagonalizing $H$. The operators of physics (the Laplacian, Schrödinger operators with Coulomb potentials, position and momentum) are unbounded, defined only on a dense subspace, and have no eigenbasis in general. The spectral theorem is the substitute for diagonalization in this setting: it expresses every self-adjoint operator as an integral of the identity function against a family of orthogonal projections, and so gives meaning to $f(A)$ for every Borel function $f$, in particular to $e^{-itA}$ and to the spectral projections $\chi_\Omega(A)$.

The theorem goes back to Hilbert (bounded symmetric forms, 1906) and was extended to unbounded self-adjoint operators by von Neumann (1929/30), Stone (1932) and Riesz. This mission follows the treatment in G. Teschl, Mathematical Methods in Quantum Mechanics (AMS Graduate Studies in Mathematics 99, 2009), Section 3.1: projection-valued measures, their functional calculus for bounded and unbounded functions, and the spectral theorem obtained from resolvents through the Herglotz representation of Borel transforms.

Setting

Let $\mathfrak H$ be a complex Hilbert space, with inner product $\langle\cdot,\cdot\rangle$ conjugate linear in the first argument, and let $\mathfrak L(\mathfrak H)$ be the bounded operators on it. An (unbounded) operator $A$ is a linear map defined on a subspace $\mathfrak D(A) \subseteq \mathfrak H$; $A \subseteq B$ means $B$ extends $A$. $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A^* = A$, domains included.

The resolvent set of $A$ is the set of $z \in \mathbb{C}$ for which $A - z : \mathfrak D(A) \to \mathfrak H$ is a bijection with bounded inverse, and the spectrum is its complement, $\sigma(A) = \mathbb{C} \setminus \rho(A)$.

A projection-valued measure assigns to every Borel set $\Omega \subseteq \mathbb{R}$ an orthogonal projection $P(\Omega) = P(\Omega)^* = P(\Omega)^2$ such that $P(\mathbb{R}) = \mathbb{I}$ and, for pairwise disjoint Borel sets $\Omega_n$, $\sum_n P(\Omega_n)\psi = P(\bigcup_n \Omega_n)\psi$ for every vector $\psi$ (strong, not norm, $\sigma$-additivity). Each $\psi$ gives the spectral measure $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$, a finite Borel measure of total mass $\|\psi\|^2$, and by polarization the complex measures $\mu_{\varphi,\psi}(\Omega) = \langle\varphi, P(\Omega)\psi\rangle$.

For a bounded Borel function $f$ the operator $P(f) = \int f(\lambda)\,dP(\lambda) \in \mathfrak L(\mathfrak H)$ is the bounded operator with $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for all $\psi$. For an arbitrary Borel function $f$ it is the operator with domain

$$\mathfrak D_f = \Big\{\psi \in \mathfrak H \;\Big|\; \int_{\mathbb{R}} |f(\lambda)|^2\, d\mu_\psi(\lambda) < \infty\Big\}$$

and $\langle\psi, P(f)\psi\rangle = \int f\,d\mu_\psi$ for $\psi \in \mathfrak D_f$. An operator $T$ is normal if it is densely defined, $\mathfrak D(T) = \mathfrak D(T^*)$ and $\|T\psi\| = \|T^*\psi\|$ on $\mathfrak D(T)$.

Formalization targets

Goal: the spectral theorem (Theorem 3.7)

For every self-adjoint operator $A$ in $\mathfrak H$ there is a unique projection-valued measure $P_A$ with

$$A = \int_{\mathbb{R}} \lambda\, dP_A(\lambda),$$

an equality of operators including their domains. Uniqueness is among projection-valued measures, compared on Borel sets.

Milestones

• Theorem 3.1. For a projection-valued measure $P$, the map $f \mapsto P(f)$ from bounded Borel functions (sup norm) to $\mathfrak L(\mathfrak H)$ is a unital $C^*$-algebra homomorphism of norm one, $\langle P(g)\varphi, P(f)\psi\rangle = \int g^* f\, d\mu_{\varphi,\psi}$, and $P(f_n) \to P(f)$ strongly when $f_n \to f$ pointwise with $\sup_\lambda |f_n(\lambda)|$ bounded.
• Theorem 3.2. For every Borel $f$, the operator $P(f)$ with $\mathfrak D(P(f)) = \mathfrak D_f$ exists, is normal, and $P(f)^* = P(f^*)$.
• Lemma 3.5. $\alpha P(f) + \beta P(g) \subseteq P(\alpha f + \beta g)$ with domain $\mathfrak D_{|f|+|g|}$, and $P(f)P(g) \subseteq P(fg)$ with domain $\mathfrak D_g \cap \mathfrak D_{fg}$.
• Theorem 3.8. For self-adjoint $A$, $\sigma(A) = \{\lambda \in \mathbb{R} \mid P_A((\lambda-\varepsilon, \lambda+\varepsilon)) \ne 0 \text{ for all } \varepsilon > 0\}$.
• Corollary 3.9. $P_A(\sigma(A)) = \mathbb{I}$ and $P_A(\mathbb{R} \cap \rho(A)) = 0$.

A further supporting statement (not a milestone) records that $\mu_\psi$ is a finite measure with $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle = \|P(\Omega)\psi\|^2$.

Significance

The result itself. The spectral theorem is the foundation of the rest of the book and of mathematical quantum mechanics generally. Stone's theorem and the time evolution $e^{-itA}$, the min-max principle, the RAGE theorem, the decomposition of the spectrum into absolutely continuous, singular continuous and pure point parts, Weyl's theorem on essential spectra and scattering theory are all statements about $f(A)$ or $P_A(\Omega)$. Theorem 3.8 identifies the spectrum with the support of $P_A$, which is what makes spectral questions accessible to measure theory.

Formalizing it. The result is classical and fully proved in the literature. Mathlib has the continuous functional calculus for bounded normal elements of $C^*$-algebras and the finite-dimensional spectral theorem, but no projection-valued measures, no spectral integral of unbounded functions, and no spectral theorem for unbounded operators (LinearPMap). On Prove2Me the related published material is bounded or finite-dimensional (for example diagonalization of self-adjoint endomorphisms and the Fuglede–Putnam theorem). A formal proof here supplies the object $f(A)$ that every later mission of this series currently has to take as data.

Difficulty

The obvious route through the bounded case fails. For bounded self-adjoint $A$ one can build $f(A)$ from polynomials by the sup norm on $\sigma(A)$ and extend by monotone limits; for unbounded $A$ there are no polynomials in $A$ defined on a common useful domain and no sup-norm estimate. The standard reductions (the Cayley transform $(A-i)(A+i)^{-1}$, or the bounded resolvent $(A-z)^{-1}$) produce bounded normal operators whose spectral measures must then be transported back, and the domain $\mathfrak D(A)$ must be recovered exactly as $\mathfrak D_\lambda$; getting the domains right, not just the formulas on a core, is where unbounded arguments usually break. Beyond the domain issue, the projections $P_A(\Omega)$ are not given by any formula in $A$ that Mathlib can evaluate: they have to be recovered from resolvent data, which in the book's development requires the Herglotz representation of Borel transforms and the Stieltjes inversion formula for finite measures, neither of which is in Mathlib. Uniqueness is also not automatic: it requires that a projection-valued measure is determined by the operator $\int \lambda\, dP(\lambda)$ alone.

Formalization scope

$\mathfrak H$ is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is not assumed, since none of the stated results or their proofs in the book need it. Operators are LinearPMaps H →ₗ.[ℂ] H; self-adjointness is Mathlib's IsSelfAdjoint, which includes density. A projection-valued measure is a function Set ℝ → (H →L[ℂ] H) constrained on Borel sets only (IsProjValuedMeasure); uniqueness in the goal compares values on Borel sets. The spectral measure spectralMeasure P ψ is built with Measure.ofMeasurable from $\Omega \mapsto \|P(\Omega)\psi\|^2$. The spectral integral spectralIntegral P f is the operator with domain $\mathfrak D_f$ and quadratic form $\int f\,d\mu_\psi$ (the predicate IsSpectralIntegral), selected by choice; its existence for Borel $f$ is part of the milestone for Theorem 3.2, not an assumption. The bounded calculus boundedSpectralIntegral is characterized the same way in $\mathfrak L(\mathfrak H)$. The spectrum is the resolvent-based TeschlQM.Spectral.spectrum of Section 2.4, not Mathlib's spectrum ℂ of a Banach algebra element. In Theorems 3.8 and 3.9, $P_A$ enters as a projection-valued measure P with the hypothesis A = spectralIntegral P (fun x => x), which by the goal's uniqueness is exactly $P_A$.

Nothing is taken as data that the book derives. In particular the goal is not stated for "a projection-valued measure with $A = \int\lambda\,dP$" given as a hypothesis, and $P_A$ is not defined by choosing such a measure: the goal quantifies existentially and uniquely over projection-valued measures, with self-adjointness of $A$ as the only hypothesis.

Lemma 3.4 (spectral bases), Lemma 3.6 (the family $P_A(\Omega)$ built from the Herglotz representation) and the results of Sections 3.2–3.3 are not stated. A complete development needs finite Borel measures and $L^2$ spaces (in Mathlib), the Herglotz representation and Stieltjes inversion (the subject of the next mission of this series), and the adjoint theory of LinearPMap. The projection-valued measure and spectral-integral layer is reusable by every later mission of the series. Contributions of any milestone, of general lemmas about IsProjValuedMeasure (finite additivity, $P(\Omega_1)P(\Omega_2) = P(\Omega_1 \cap \Omega_2)$, monotonicity), and of alternative proofs of the goal are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009, Chapter 3. https://doi.org/10.1090/gsm/099
• J. von Neumann, Allgemeine Eigenwerttheorie Hermitescher Funktionaloperatoren, Mathematische Annalen 102 (1930), 49–131. https://doi.org/10.1007/BF01782338
• M. H. Stone, Linear Transformations in Hilbert Space and Their Applications to Analysis, AMS Colloquium Publications 15, 1932. https://doi.org/10.1090/coll/015
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Academic Press, 1980, Chapters VII–VIII. https://doi.org/10.1016/B978-0-12-585050-6.X5001-4

Motivation

In one complex variable every open set is the natural domain of some holomorphic function. In several variables this fails: by the Hartogs phenomenon, every function holomorphic on some domains extends to a strictly larger one. The domains that are "natural", the domains of holomorphy, are characterised by a convexity condition on the domain. Since the work of Levi (1910), Hartogs, Oka and Cartan–Thullen (1932), the way to state that condition intrinsically has been pseudoconvexity. The tool that makes it work is the plurisubharmonic function, the complex analogue of a convex function.

This mission formalizes the part of that theory that needs no partial differential equations: harmonic, subharmonic and plurisubharmonic functions; smoothing of plurisubharmonic functions; the characterizations of Hartogs pseudoconvexity; and the Cartan–Thullen theorem. The source is §2.4–2.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), pp. 78–103.

Timeline, as the book presents it:

• Hartogs (1906) found the extension phenomenon.
• Levi (1910) found the boundary condition now called Levi pseudoconvexity.
• Cartan and Thullen (1932) proved that domains of holomorphy are exactly the holomorphically convex domains.
• Oka (1942–1953), Bremermann and Norguet (1954) solved the Levi problem: every pseudoconvex domain is a domain of holomorphy. The book states this result (its Theorem 2.6.2) but does not prove it.

Setting

Throughout, $\mathbb{C}^n$ carries the Euclidean norm $\|z\| = (|z_1|^2 + \dots + |z_n|^2)^{1/2}$. A domain is a nonempty connected open set. For $K, U \subset \mathbb{C}^n$, $K \subset\subset U$ means that $K$ is relatively compact in $U$: its closure is compact and contained in $U$.

Harmonic and subharmonic functions (one variable). A $C^2$ function $f$ on an open $U \subset \mathbb{C}$ is harmonic if $\nabla^2 f = 0$. A function $f : U \to \mathbb{R} \cup \{-\infty\}$ is subharmonic if it is upper-semicontinuous and, for every disc $B_r(a)$ with $\overline{B_r(a)} \subset U$ and every $g$ continuous on $\overline{B_r(a)}$ and harmonic inside it, $f \le g$ on $\partial B_r(a)$ implies $f \le g$ on $B_r(a)$.

Plurisubharmonic functions. For $U \subset \mathbb{C}^n$ open, $f : U \to \mathbb{R} \cup \{-\infty\}$ is plurisubharmonic if it is upper-semicontinuous and $\xi \mapsto f(a + b\xi)$ is subharmonic on $\{\xi : a + b\xi \in U\}$ for all $a, b \in \mathbb{C}^n$.

Hulls and convexity. For a class $\mathcal{F}$ of extended-real functions on $U$ and $K \subset U$, the hull is

$$\widehat{K} = \{x \in U : f(x) \le \sup_{y \in K} f(y) \text{ for all } f \in \mathcal{F}\}.$$

$U$ is convex with respect to $\mathcal{F}$ if $K \subset\subset U$ implies $\widehat{K} \subset\subset U$. For $\mathcal{F} = \{|f| : f \in \mathcal{O}(U)\}$ this is holomorphic convexity, with hull $\widehat{K}_U$.

Hartogs pseudoconvexity. $f : U \to \mathbb{R}$ is an exhaustion function if $\{z \in U : f(z) < r\} \subset\subset U$ for every $r$. A domain is Hartogs pseudoconvex if it admits a continuous plurisubharmonic exhaustion function.

Analytic discs. A closed analytic disc is a nonconstant holomorphic $\varphi : \mathbb{D} \to \mathbb{C}^n$ that extends continuously to $\overline{\mathbb{D}}$. Its image is $\Delta = \varphi(\mathbb{D})$ and its boundary is $\partial\Delta = \varphi(\partial\mathbb{D})$.

Formalization targets

Goal: Theorem 2.5.6

For a domain $U \subsetneq \mathbb{C}^n$ with $\rho(z) = \operatorname{dist}(z, \partial U)$, the following are equivalent:

$$\text{(i) } -\log\rho \text{ is plurisubharmonic};\quad \text{(ii) } U \text{ is Hartogs pseudoconvex};$$ $$\text{(iii) } U \text{ is convex w.r.t. plurisubharmonic functions on } U;\quad \text{(iv) } \textstyle\bigcup_\alpha \partial\Delta_\alpha \subset\subset U \Rightarrow \bigcup_\alpha \Delta_\alpha \subset\subset U$$

for every collection of closed analytic discs $\Delta_\alpha \subset U$.

Milestones

• Proposition 2.4.3. A continuous $f$ is harmonic iff it has the mean-value property. An upper-semicontinuous $f$ is subharmonic iff $f(a) \le \frac{1}{2\pi}\int_0^{2\pi} f(a + re^{i\theta})\,d\theta$ whenever $\overline{\Delta_r(a)} \subset U$.
• Proposition 2.4.7. Finite suprema of subharmonic functions are subharmonic, and so are arbitrary suprema that are finite and upper-semicontinuous.
• Proposition 2.4.9. A $C^2$ function is plurisubharmonic iff its complex Hessian $[\partial^2 f/\partial\bar z_k \partial z_\ell]$ is positive semidefinite.
• Theorem 2.4.10. Every plurisubharmonic $f$ is the pointwise limit of smooth plurisubharmonic $f_\epsilon \ge f$ on $U_\epsilon = \{z \in U : \operatorname{dist}(z, \partial U) > \epsilon\}$.
• Theorem 2.5.2 (Kontinuitätssatz, second version): (iii) implies (iv).
• Lemma 2.5.7. Hartogs pseudoconvexity is a local property of the boundary.
• Theorem 2.4.12 (Radó): a continuous function holomorphic off its zero set is holomorphic.
• Theorem 2.6.3 (Cartan–Thullen): for a domain $U \subsetneq \mathbb{C}^n$, being a domain of holomorphy, $\operatorname{dist}(K, \partial U) = \operatorname{dist}(\widehat{K}_U, \partial U)$ for all $K \subset\subset U$, and holomorphic convexity are equivalent.

Significance

The result. Theorem 2.5.6 makes pseudoconvexity checkable. Condition (i) involves one explicitly given function of the domain's geometry. Condition (iv) involves only families of discs. Condition (ii) is the form the Levi problem and Hörmander's $L^2$ theory need. From these equivalences one gets, for example, that intersections and increasing unions of pseudoconvex domains are pseudoconvex, that pseudoconvexity is a biholomorphic invariant, and, with Lemma 2.5.7, that it is a local boundary property. In the smooth case that local property is Levi pseudoconvexity (Theorem 2.5.8, chapter III of this series). Cartan–Thullen supplies the other half of the picture for domains of holomorphy.

Formalizing it. All of these results are classical and proved in the book, apart from routine steps left as exercises. As far as is known, none of them is formalized in any proof assistant. Mathlib has harmonic functions (InnerProductSpace.HarmonicOnNhd) and the circle average, but no subharmonic or plurisubharmonic functions, no hulls and no pseudoconvexity. The Prove2Me corpus holds a one-variable subharmonic definition based on the sub-mean-value property and the one-directional mean-value property of harmonic functions; neither is the book's definition or statement. The mission would give Lean a first library of plurisubharmonic functions in $\mathbb{C}^n$, with the definition matching the textbook.

Difficulty

The obvious route to (iv) ⇒ (i) of the goal would show $-\log\rho$ is plurisubharmonic by computing a complex Hessian (Proposition 2.4.9). That fails: $\rho$ is in general not even differentiable, so no Hessian is available. Several other steps also need measure theory with extended-real values. The sub-mean-value property requires Lebesgue integrals of upper-semicontinuous functions that may equal $-\infty$ on large sets. Smoothing requires convolution of such functions with a mollifier, and pointwise convergence in $[-\infty, \infty)$. Suprema of families lose upper semicontinuity in general, which is why Proposition 2.4.7 carries that hypothesis. In Cartan–Thullen, holomorphic convexity alone must produce a holomorphic function on $U$ that extends across no boundary point. Nothing in the hypothesis supplies such a function directly.

Formalization scope

• $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n), so balls, $\rho(z)$ = Metric.infDist z (frontier U), $U_\epsilon$ and $\operatorname{dist}(K, \partial U)$ are all Euclidean, as in the book. They are not sup-norm polydisc quantities.
• Functions with values in $\mathbb{R} \cup \{-\infty\}$ are EReal-valued with $+\infty$ excluded on $U$. Upper semicontinuity is UpperSemicontinuousOn for the order of EReal.
• Hulls take suprema in EReal, and holomorphic hulls in $[0, \infty]$, so no supremum takes a junk value. Set distances are infima in $[0, \infty]$ (Metric.infEDist).
• The circle mean in Proposition 2.4.3 (ii) is the Lebesgue integral of the positive part minus that of the negative part.
• Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there.
• A domain is IsOpen U ∧ IsConnected U. Relative compactness is compact closure contained in $U$.
• Harmonic and subharmonic functions are defined only on open subsets of $\mathbb{C} = \mathbb{R}^2$. The book defines them on $\mathbb{R}^n$, but only uses $n = 2$. This is the one restriction of scope.
• A collection of analytic discs is a set of parametrizing maps, and $\Delta_\alpha = \varphi_\alpha(\mathbb{D})$ as in Definition 1.4.5.
• Definitions 1.4.5 and 2.1.1 are restated locally in the namespace LeblSCV.Pseudoconvex.

Several trivializing formalizations are ruled out. Plurisubharmonicity is not defined through the Hessian condition, so the mission does not reduce to $C^2$ functions. Nor is it defined by the sub-mean-value property, which would make Proposition 2.4.3 (ii) a tautology. $\rho$ is not the sup-norm distance. Suprema, infima and integrals are nowhere allowed to default to $0$ on empty, unbounded or non-integrable input.

A complete development needs:

• mean values of upper-semicontinuous functions and the Poisson integral on discs (Theorem 2.4.2, not a milestone);
• convolution with a radial mollifier on $\mathbb{C}^n$;
• Cauchy estimates on polydiscs.

The subharmonic and plurisubharmonic layer is reusable beyond this mission. Chapters on the Levi problem, the $\bar\partial$-problem and Bergman kernels would all build on it. Proofs of the smaller milestones, and alternative arguments for the goal, are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026. https://www.jirka.org/scv/scv.pdf
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland Mathematical Library 7, 1990 (the book's reference [H] for the Levi problem).
• H. Cartan and P. Thullen, "Zur Theorie der Singularitäten der Funktionen mehrerer komplexen Veränderlichen: Regularitäts- und Konvergenzbereiche", Mathematische Annalen 106 (1932), 617–647.

Motivation

Heavy-traffic and fluid approximations for open queueing networks are obtained by writing the queue-content process as a deterministic function of a simpler netput process (arrivals minus potential service, corrected for routing) and then transferring a functional limit theorem for the netput through that function. The function is the multidimensional reflection map of Harrison and Reiman (Harrison and Reiman 1981), extended from continuous paths to paths with jumps by Reiman (Reiman 1984). The transfer works only if the map is continuous, and quantitative bounds on the approximation error require it to be Lipschitz with a known modulus.

Chen and Whitt (Chen and Whitt 1993) use this map to derive diffusion approximations for networks whose servers are subject to interruptions. Before doing so, Section 2 of the paper supplies "explicit Lipschitz bounds" for the map in the uniform topology: a bound in the Harrison–Reiman scaling (Proposition 2.1) and a new bound that depends on the routing matrix only through its powers (Proposition 2.3).

Timeline. Harrison and Reiman (1981) proved existence, uniqueness and continuity of the map on continuous paths for a routing matrix of spectral radius less than one. Reiman (1984) extended it to paths with jumps. Chen and Mandelbaum (Leontief systems, RBV's and RBM's, 1991, cited in the paper as [4]) noted that a minor extension of the argument makes the map Lipschitz on $D([0,T],\mathbb R^n)$ with the uniform topology. Chen and Whitt (1993, Section 2) made the Lipschitz constants explicit.

Setting

Fix a dimension $n$ and an $n\times n$ matrix $Q$ whose transpose $Q^{\mathsf t}$ is substochastic: all entries of $Q$ are nonnegative and every column sum of $Q$ is at most $1$. Assume also $Q^k \to 0$ as $k\to\infty$. With Markovian routing, $Q^{\mathsf t}$ is the routing matrix of an open network of $n$ queues.

Vectors $c\in\mathbb R^n$ carry the norm $\|c\| = \sum_j |c_j|$, and matrices carry the maximum absolute column sum $\|P\| = \max_j \sum_i |P_{ij}|$ (Eq. (2.5)). $D([0,T],\mathbb R^n)$ is the space of paths that are right-continuous with left limits on $[0,T]$. For a path $x$, $|x|\in\mathbb R^n$ is the vector of coordinatewise sup norms, $|x|_j = \sup_{0\le t\le T}|x_j(t)|$, and $\|x\| = \big\||x|\big\| = \sum_j \sup_{t}|x_j(t)|$.

The reflection of $x \in D$ is the pair $(y,z) = (\psi(x),\phi(x))$ with $y \in D$ and

$$z = x + (I-Q)\,y \ge 0, \qquad y_j \text{ nondecreasing},\ y_j(0) = 0, \qquad \int_0^T z_j(t)\,dy_j(t) = 0 \quad (1\le j\le n).$$

The last condition says that $y_j$ increases only when $z_j = 0$. In queueing terms, $z$ is the vector of queue contents and $y$ the cumulative idleness. The operator $\pi_x(y) = (Qy - x)^{\uparrow}\vee 0$, where $f^{\uparrow}(t) = \sup_{0\le s\le t} f(s)$ coordinatewise, has the reflection as its fixed point (Eq. (2.4)). Write $\gamma = \|Q^n\|$.

Formalization targets

Goal: Proposition 2.3

For all $x_1,x_2\in D$ with reflections $(\psi(x_i),\phi(x_i))$,

$$|\psi(x_1)-\psi(x_2)| \le (I-Q)^{-1}|x_1-x_2| \quad\text{componentwise},\tag{2.9}$$ $$\|\psi(x_1)-\psi(x_2)\| \le \|(I-Q)^{-1}\|\,\|x_1-x_2\| \le \sum_{k=0}^\infty \|Q^k\|\,\|x_1-x_2\| \le \frac{n}{1-\gamma}\|x_1-x_2\|,\tag{2.10}$$ $$\|\phi(x_1)-\phi(x_2)\| \le \big(1+\|I-Q\|\,\|(I-Q)^{-1}\|\big)\|x_1-x_2\| \le \Big(1+\frac{2n}{1-\gamma}\Big)\|x_1-x_2\|.\tag{2.11}$$

The constants are those of the paper. The goal fixes nothing beyond the standing assumptions on $Q$.

Milestones

1. Existence and uniqueness of the reflection for $x\in D$ with $x(0)\ge0$ (Section 2, p. 337).
2. Eq. (2.4): given (2.1)–(2.2), the complementarity condition (2.3) is equivalent to $y = \pi_x(y)$.
3. $\gamma = \|Q^n\| < 1$ (p. 338).
4. Proposition 2.2: $\|\pi_x^k(y_1)-\pi_x^k(y_2)\| \le \|Q^k|y_1-y_2|\| \le \|y_1-y_2\|$ for $k\ge1$, the factor $\gamma$ for $k\ge n$, and $\pi_x^k(y_1)\to\psi(x)$.
5. Proposition 2.1: for $Q^* = \Lambda^{-1}Q\Lambda$ with $\Lambda$ diagonal and $\|Q^*\| = \alpha<1$, the moduli $\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\psi$ and $1 + \|I-Q\|\|\Lambda\|\|\Lambda^{-1}\|/(1-\alpha)$ for $\phi$.
6. Remark (2.1): for $n=1$, $Q=0$ the bounds are attained.
7. Remark (2.2): for two queues in series, (2.10) gives modulus $2$, while (2.7) gives at best $4$ (every modulus $\ge 4$ is attained, $4$ at $z = 1/2$).

Significance

Proposition 2.3 makes the queue-content and idleness processes of an open network Lipschitz functions of the netput, in the uniform norm, with a modulus computed from the routing matrix alone. Combined with the fact that Lipschitz continuity in the uniform topology passes to the Skorohod $J_1$ and $M_1$ topologies (Section 2 of the paper), it is what turns a functional central limit theorem for arrival and service processes into a heavy-traffic limit for the network. The paper uses it in exactly this way in Sections 3–4. Explicit moduli also yield rates: an error of order $\varepsilon$ in the netput produces an error of at most $n\varepsilon/(1-\gamma)$ in the idleness process.

On the formal side, the results are proved in the paper, but neither the reflection map nor $D([0,T],\mathbb R^n)$ has a machine-checked development in Mathlib or on this platform. The mission would provide a reusable definition of the oblique reflection map with a Lebesgue–Stieltjes complementarity condition, its fixed-point characterization, and certified Lipschitz constants, as a foundation for any later formal heavy-traffic limit.

Difficulty

The componentwise bound (2.9) is short once the fixed-point form of the map is available. The difficulty lies in the infrastructure beneath it. The fixed-point characterization (2.4) is a one-dimensional Skorokhod-problem argument carried out coordinatewise for paths with jumps, where the complementarity condition must be handled through Lebesgue–Stieltjes measures. A jump of $y_j$ is allowed at a time where $z_j = 0$ even if $z_j$ was positive just before. Existence needs the iterates $\pi_x^k(0)$ to converge in $D$ and the limit to satisfy (2.1)–(2.3). The explicit constants involve $(I-Q)^{-1}$, $\sum_k\|Q^k\|$ and $\gamma = \|Q^n\|<1$. The last inequality is a combinatorial fact about transient substochastic matrices. It does not follow from $\|Q\|\le1$.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, and $\|P\|$ is the maximum absolute column sum. Paths are functions ℝ → Fin n → ℝ, of which only the restriction to $[0,T]$ matters. Membership in $D([0,T],\mathbb R^n)$ is the predicate IsCadlagOn T x: right-continuous on $[0,T)$, left limits on $(0,T]$, and (redundantly) bounded on $[0,T]$. The reflection is the predicate IsReflection Q T x y z. Every theorem is stated for all pairs satisfying it, so no choice function and no junk value are involved. Condition (2.3) is encoded as "the Lebesgue–Stieltjes measure $dy_j$ of $\{t\in[0,T]: z_j(t)>0\}$ is zero". For $z\ge0$ this is equivalent to $\int_0^T z_j\,dy_j=0$. $\pi_x^k$ is Nat.iterate, $(I-Q)^{-1}$ is Mathlib's matrix inverse (invertible under the standing assumptions), and $\sum_k\|Q^k\|$ is a tsum stated together with its summability.

Corrections and conventions, each disclosed in the item concerned:

• The norm (2.6). The page prints $\|x\| = \sup_t\sum_j|x_j(t)|$. Under that norm Propositions 2.1 and 2.3 are false for $n\ge2$. With $Q=0$, $n=2$, $T=1$, $x_1\equiv0$ and $x_2 = (-\mathbf 1_{[0.1,0.2)}, -\mathbf 1_{[0.3,0.4)})$, one gets $\|x_1-x_2\|=1$ but $\psi(x_2) = (\mathbf 1_{[0.1,1]},\mathbf 1_{[0.3,1]})$ has norm $2$. The paper's proofs are valid for $\|x\| = \sum_j\sup_t|x_j(t)|$, which is used throughout. In dimension one the two norms coincide.
• (2.8) prints $\phi(x_1)-\phi(x_1)$. The formalization states $\phi(x_1)-\phi(x_2)$.
• (2.2)–(2.3) print the index range $1\le j\le J$. The dimension is $n$.
• $x(0)\ge0$ is added to the existence item. Conditions (2.1)–(2.2) force $z(0)=x(0)$, so no reflection exists otherwise. The Lipschitz bounds are stated for all solution pairs and are vacuous exactly when some $x_i(0)$ has a negative coordinate.
• Proposition 2.1 assumes only that $\Lambda$ is diagonal with nonzero entries. All quantities depend on $|\Lambda|$, so this covers the positive scaling of Harrison and Reiman.
• Eq. (2.4) keeps the standing assumptions on $Q$ as on the page, although the equivalence does not use them.

A trivializing formalization would read (2.3) through a Bochner integral, which is $0$ for non-integrable integrands, or take suprema over unbounded families. The measure-zero encoding and the boundedness built into IsCadlagOn rule both out. A sorry-free check shows that Remark (2.1)'s jump example satisfies IsReflection.

Welcome contributions: a general API for càdlàg paths on $[0,T]$ (boundedness, measurability, running suprema), the one-dimensional Skorokhod lemma for càdlàg paths, and the Neumann series for transient substochastic matrices. All of these are reusable beyond this mission.

Selected references

• H. Chen and W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
• J. M. Harrison and M. I. Reiman, Reflected Brownian motion on an orthant, Annals of Probability 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994428
• M. I. Reiman, Open queueing networks in heavy traffic, Mathematics of Operations Research 9 (1984) 441–458. https://doi.org/10.1287/moor.9.3.441
• H. Chen and A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Annals of Probability 19 (1991) 1463–1519. https://doi.org/10.1214/aop/1176990220

From conditional motion to a marginal probability path

Flow matching models a changing probability distribution using a time-dependent velocity field. A conditional model specifies a density and a velocity separately for each conditioning point. The mathematical question is whether those conditional descriptions determine a velocity for the mixture distribution. This mission concerns the continuity-equation formulation of Theorem 1 of Lipman, Chen, Ben-Hamu, Nickel, and Le, Flow Matching for Generative Modeling (ICLR 2023). The source is arXiv:2210.02747v2, Section 3.1 and Appendix A.

Densities, velocities, and probability flux

Fix a natural number $d$ and let $E=\mathbb R^d$. The conditioning distribution $Q$ is a Borel probability measure on $E$. At time $t$, position $x$, and conditioning point $z$, write $\rho(t,x,z)$ for the conditional density and $v(t,x,z)\in E$ for the conditional velocity. The variable $x$ is integrated against Lebesgue measure; $z$ is integrated against $Q$. These roles remain distinct even though both variables take values in the same space.

The conditional flux is $F(t,x,z)=\rho(t,x,z)v(t,x,z)$. The marginal density, marginal flux, and marginal velocity are defined by

$$p(t,x)=\int_E\rho(t,x,z)\,dQ(z),\qquad J(t,x)=\int_E F(t,x,z)\,dQ(z),\qquad u(t,x)=p(t,x)^{-1}J(t,x).$$

These definitions express equations (6) and (8) using a probability measure rather than a data-density function. This representation also allows discrete conditioning distributions. Every conditional density is strictly positive and normalized on $0\leq t\leq1$, jointly measurable in $(x,z)$, and integrable in $z$ at each fixed $(t,x)$.

The divergence of a differentiable vector field is the sum of the diagonal entries of its derivative. A density and velocity satisfy the classical continuity equation when their flux is spatially differentiable and the density has time derivative equal to minus that divergence.

Formalization targets

The goal asserts that $p(t,\cdot)$ is a positive probability density for every $t\in[0,1]$ and that

$$\partial_t p(t,x)+\operatorname{div}_x\bigl(p(t,x)u(t,x)\bigr)=0\qquad(0<t<1,\ x\in E).$$

The hypotheses require the conditional continuity equation for $Q$-almost every conditioning point, at each interior time and spatial point. They also specify a sufficient local domination package for differentiation under the integral. This is an explicit classical interpretation of the regularity qualification in the proof of Theorem 1.

Four supporting targets isolate the mathematical assertions used by this formulation: the probability-density property of equation (6); time differentiation under the conditioning integral; spatial divergence under the conditioning integral; and the velocity/flux identity corresponding to equation (8). The source contains these equations and operations rather than separately numbered supporting lemmas, so the milestone titles identify the relevant equation or proof passage.

What completing the formalization provides

The deliverable is a checked interface for passing from a measurable family of conditional continuity equations to the continuity equation of its mixture. It records which variables are differentiated, which measure is used for averaging, where positivity is needed, and which assumptions justify each analytic operation. The time and spatial differentiation lemmas are stated for general measures and integrands, making them reusable outside this particular probability model.

The mathematical result is already proved in the cited paper. The uploaded theorem items are open formalization targets, with explicit proof placeholders. Successful local compilation checks their types and imports; it does not establish their conclusions. The definition module contains no proof placeholders.

Analytic obligations

Pointwise differentiability of every conditional function does not by itself justify differentiating an integral over the conditioning variable. The regularity predicates therefore require a neighborhood independent of that variable, an integrable bound for the derivative norm throughout that neighborhood, and almost-everywhere measurability of the integrand and derivative. Time and space receive separate predicates because their derivatives take values in different spaces.

There is also a distinction between density normalization in $x$ and integrability in $z$ at a fixed position. The formal assumptions record both. A probability measure on the conditioning space does not make every measurable function integrable. These conditions prevent the totalized Bochner integral from silently supplying a default value where an intended integral fails to exist.

Formalization scope

Space is represented by Fin d → ℝ, with its standard finite-product Borel structure and Lebesgue measure. Its norm is the standard product norm used by mathlib. All finite dimensions, including dimension zero, are included. Time-dependent functions are defined on all real times, while density assumptions apply on the closed unit interval and derivative conclusions apply on its interior. No endpoint time derivative is asserted.

The regularity package is one sufficient realization of the source's Leibniz-rule assumption, not a claim to the weakest possible hypotheses. Conditional continuity equations may hold almost everywhere in the conditioning variable; their exceptional sets may depend on the fixed time and position. Spatial differentiability of the marginal flux is part of the conclusion, so the equation cannot be satisfied merely through the default value of an undefined derivative.

The target is the PDE formulation. It does not assert existence of a global ODE flow, uniqueness of transported measures, or equality with a flow pushforward. Those require a separate transport development. It also asserts no endpoint approximation to a data distribution and no theorem about optimization, neural networks, or Gaussian paths. No marginal continuity equation or differentiation–integration interchange is assumed as an input.

Required infrastructure consists of Bochner integration, finite-dimensional differentiation, finite sums of derivative coordinates, and product-measure integration. Contributions may prove the supporting targets or the goal directly while preserving their statements and the distinction between classical PDE and flow-transport claims.

Selected references

• Yaron Lipman, Ricky T. Q. Chen, Heli Ben-Hamu, Maximilian Nickel, and Matt Le. Flow Matching for Generative Modeling. ICLR 2023. arXiv:2210.02747v2, Section 2, Section 3.1, Theorem 1, equations (6), (8), and (26), and Appendix A's proof of Theorem 1.
• mathlib contributors. ParametricIntegral.lean, revision 0df444a360eaa60ab8c11dca51a86af692955474. Differentiation under the integral.

Motivation

Two different numbers describe the output of a lamp. Radiant flux $\Phi_e$ is the power it radiates, in watts. Luminous flux $\Phi_v$ is how much of that radiation the standard human eye registers, in lumens — a weighted integral of the radiated power in which each wavelength is counted according to the sensitivity of the eye at that wavelength. Their ratio

$$K \;=\; \frac{\Phi_v}{\Phi_e}$$

is the luminous efficacy of radiation, measured in lumens per watt: it says what fraction of the radiated power is usable for illumination. Photometry is built on this pair of quantities. The lumen and the candela are defined from the watt through exactly such a weighting, with the SI defining constant $K_{\mathrm{cd}} = 683$ lm/W fixing the scale at the frequency $540 \times 10^{12}$ Hz, and every efficiency figure quoted for a lamp — a tungsten filament at $15$ lm/W, a white LED above $100$ lm/W — is a statement about this ratio or its wall-plug variant.

The basic structural fact of the subject is that this ratio is bounded. Since the eye's sensitivity curve is normalized to a maximum of $1$, no source, however designed, can exceed the maximum spectral luminous efficacy: $683.002$ lm/W under photopic (daylight, cone) vision, and about $1700$ lm/W under scotopic (dark-adapted, rod) vision. Those two numbers are the ceilings against which every lighting technology is measured, and they are what this mission formalizes.

Setting

Wavelengths are real numbers (nanometres). A spectral radiant flux distribution of a source is modelled as a finite Borel measure $\mu$ on the wavelength axis: $\mu(A)$ is the power, in watts, that the source radiates at wavelengths in $A$. Its radiant flux is the total mass

$$\Phi_e \;=\; \mu(\mathbb{R}).$$

A luminosity function (luminous efficiency function) with peak at $\lambda_0$ is a measurable $V : \mathbb{R} \to \mathbb{R}$ with

$$0 \le V(\lambda) \le 1 \quad \text{for all } \lambda, \qquad V(\lambda_0) = 1 .$$

For photopic vision the CIE 1924 curve $V$ peaks at $\lambda_0 = 555$ nm; the scotopic curve $V'$ peaks at $\lambda_0 = 507$ nm. The development assumes only the normalization above, never a specific tabulated curve, so every statement holds for the photopic curve, the scotopic curve, and any other normalized weighting.

Given a maximum spectral luminous efficacy $K_{\max}$ — the value $K_m = 683.002$ lm/W for photopic vision, $1700$ lm/W for scotopic vision — the spectral luminous efficacy is $K(\lambda) = K_{\max} V(\lambda)$ and the luminous flux is

$$\Phi_v \;=\; \int_{\mathbb{R}} K(\lambda) \, \mathrm{d}\mu(\lambda) \;=\; K_{\max} \int_{\mathbb{R}} V \,\mathrm{d}\mu .$$

The luminous efficacy of radiation is $K = \Phi_v / \Phi_e$, the dimensionless luminous efficiency is $K / K_{\max}$, and the luminous efficacy of a source (overall, or wall-plug, efficacy) is $\Phi_v / P$, where $P$ is the total input power the source consumes — electrical, chemical or other — of which the radiated part is $\Phi_e \le P$.

Modelling the spectrum as a measure rather than as a density is what makes the two halves of the target statement expressible at once. A spectrum with a spectral radiant flux density $\Phi_{e,\lambda}$ is the measure $\mathrm{d}\mu = \Phi_{e,\lambda} \, \mathrm{d}\lambda$, for which the formulas above reduce to the usual integrals

$$\Phi_v = K_{\max}\int V(\lambda)\, \Phi_{e,\lambda} \,\mathrm{d}\lambda, \qquad \Phi_e = \int \Phi_{e,\lambda} \,\mathrm{d}\lambda ;$$

an ideal monochromatic source at $\lambda_0$, which has no density with respect to wavelength, is the point mass $\delta_{\lambda_0}$.

Formalization targets

Goal — the photopic ceiling is attained at $683.002$ lm/W

$$683.002 \;=\; \max\left\{\, \frac{K_m \int V \,\mathrm{d}\mu}{\mu(\mathbb{R})} \;:\; \mu \text{ finite}, \ \mu(\mathbb{R}) > 0 \,\right\}, \qquad K_m = 683.002 \text{ lm/W}.$$

This is a maximum, not a supremum: the assertion is both that no spectral radiant flux distribution exceeds $683.002$ lm/W and that some distribution — the monochromatic source at $555$ nm — attains it exactly.

Scotopic counterpart

$$1700 \;=\; \max\left\{\, \frac{1700 \int V' \,\mathrm{d}\mu}{\mu(\mathbb{R})} \;:\; \mu \text{ finite}, \ \mu(\mathbb{R}) > 0 \,\right\}$$

for a scotopic luminosity function $V'$ with $V'(507) = 1$.

Supporting statements

$\Phi_v \ge 0$; $\Phi_v \le K_{\max}\Phi_e$; $0 \le K \le K_{\max}$; luminous efficiency in $[0,1]$; the point mass at the peak realizes $K = K_{\max}$; the reduction of $K$ to the integral formula for a spectrum with a density; invariance of $K$ under rescaling the spectrum; $\Phi_v / P \le K$ when $\Phi_e \le P$; and $K = 0$ for a source radiating only where $V$ vanishes.

Significance

The ceiling is the reference point for the whole of lighting efficiency: quoted luminous efficiencies are efficacies divided by $683.002$ lm/W, so "$37\%$" for a truncated $5800$ K black body and "$2\%$" for a tungsten filament are statements about the distance to this bound. The supporting statements are the facts that make such comparisons well posed — that the efficacy depends only on the shape of the spectrum and not on the wattage, that the wall-plug efficacy of a device is never better than the efficacy of its radiation, and that power radiated outside the response band is pure loss.

Formalizing the material produces a small, reusable measure-theoretic layer for photometric and, more generally, for weighted-average quantities: a bounded weight integrated against a finite measure, normalized by the total mass, with the extreme value attained at a point mass. Nothing here is open mathematics; the value of the mission is a machine-checked model in which the definitions of the International Electrotechnical Vocabulary are stated once and the standard consequences are derived from them, rather than each being asserted in prose.

Difficulty

The mathematical content is elementary — the ceiling is the inequality $\int V \,\mathrm{d}\mu \le \mu(\mathbb{R})$ for $0 \le V \le 1$ — and the work is in the modelling. Three points need care.

First, attainment. On the space of $L^1$ densities the value $683.002$ lm/W is a supremum that is never attained: for the actual CIE curve the set $\{V = 1\}$ is a single point, hence Lebesgue-null, so a density supported there is zero almost everywhere and has no radiant flux at all. A formalization restricted to densities would either have to weaken the goal to a supremum or state an attainment claim that is vacuously true. Measures avoid this: the monochromatic source is the point mass $\delta_{555}$.

Second, division. Efficacy is a quotient, and the quotient of a real by zero is a junk value; every statement about $K$ therefore carries the hypothesis $\Phi_e > 0$, which is also the physically meaningful one.

Third, integrability. The luminous flux is a Bochner integral, which returns $0$ for a non-integrable integrand; the mission's hypotheses ($V$ measurable and bounded, $\mu$ finite) are what rule this degeneracy out.

Formalization scope

The wavelength axis is all of $\mathbb{R}$, with Lebesgue measure where a density is used; no restriction to positive wavelengths or to a visible band is imposed, since the luminosity function already performs the restriction. A spectral radiant flux distribution is a finite Borel measure; the finiteness hypothesis is carried as a typeclass assumption and the positivity of the radiant flux as an explicit one. The luminosity function is assumed measurable with values in $[0,1]$ and equal to $1$ at its peak, and nothing more: no continuity, no unimodality, no tabulated values. The maximum spectral luminous efficacy appears as an explicit parameter $K_{\max}$, so that the photopic constant $683.002$ and the scotopic constant $1700$ are instances of the same statements rather than separate developments. Units are not represented in the types: all quantities are plain real numbers, and lumens per watt appears only in the prose.

The goal is stated as "$683.002$ is the greatest element of the set of achievable efficacies", which rules out the two trivializing readings: a bare upper bound (true of any number above the ceiling) and an attainment claim over a class of spectra that is empty or null.

A complete development needs Mathlib's measure theory and Bochner integration only: finite measures, withDensity, Dirac measures, and monotonicity of the integral. The resulting definitions are reusable for any normalized weighted average of a finite measure, and contributions extending the model — mesopic weighting, black-body spectra and the efficacy figures computed from them, or the CIE curve as tabulated data — are welcome.

Selected references

• International Electrotechnical Commission, International Electrotechnical Vocabulary, entries 845-21-089 (luminous efficacy of a source) and 845-21-090 (luminous efficacy of radiation), electropedia.org.
• Bureau International des Poids et Mesures, Principles Governing Photometry, 2nd edition, 2019, p. 10, bipm.org — the value $683.002$ lm/W.
• ISO/CIE, ISO 23539:2005 Photometry — The CIE system of physical photometry, iso.org.
• T. W. Murphy, "Maximum spectral luminous efficacy of white light", Journal of Applied Physics 111 (2012) 104909, arXiv:1309.7039.
• Wikipedia, Luminous efficacy, en.wikipedia.org/wiki/Luminous_efficacy — the source material for this mission.

Motivation

A black body is an idealized body that absorbs all radiation falling on it and, when held at a fixed absolute temperature $T$, re-emits radiation whose spectrum depends on $T$ alone. At the end of the nineteenth century two incompatible descriptions of that spectrum were on the table. Wien's distribution law (1896) fitted the measurements at short wavelengths and high temperatures but failed at long wavelengths. The formula Rayleigh obtained from classical equipartition, later the Rayleigh-Jeans law, reproduced the long-wavelength data and grew without bound at short wavelengths - the failure Ehrenfest named the ultraviolet catastrophe in 1911.

Planck's 1900 formula fits at every frequency. He reached it by refusing to treat the vibrational energy of the oscillators as a continuous quantity, writing it instead as an integer multiple of an energy element $\varepsilon = h\nu$; the constant $h$ entered physics as the proportionality factor in that hypothesis. Fitting black-body data, Planck obtained $h \approx 6.55\times10^{-34}\ \mathrm{J\,s}$, within about $1.2\%$ of the value $h = 6.626\,070\,15\times10^{-34}\ \mathrm{J\,s}$ that today defines the SI.

What makes Planck's formula the successful one is not only that it fits the data. It contains both classical laws: it degenerates to Rayleigh-Jeans at low frequency and to Wien's law at high frequency, and unlike Rayleigh-Jeans it has a finite total emission. This mission formalizes those four statements - two limits and two integrability claims - about the spectral radiance function itself.

Setting

Fix three positive real parameters: the Planck constant $h$, the speed of light $c$, and the Boltzmann constant $k_B$. They are kept as variables rather than numerical constants, so every statement is a theorem about the functional form, valid in any system of units. Let $T > 0$ be an absolute temperature.

Per unit frequency $\nu$, Planck's law gives the spectral radiance

$$B_\nu(\nu, T) \;=\; \frac{2h\nu^3/c^2}{\exp\!\left(\dfrac{h\nu}{k_B T}\right) - 1},$$

which is the function planckFreq of the already-published definition bundle BlackbodyRadiation_planck. That bundle also provides the dimensionless shape function

$$g_n(x) \;=\; \frac{x^n}{e^x - 1}, \qquad n \in \mathbb{N},$$

in terms of which $B_\nu(\nu,T) = \dfrac{2k_B^3T^3}{h^2c^2}\, g_3\!\left(\dfrac{h\nu}{k_BT}\right)$.

Two further functions are introduced by this mission. The Rayleigh-Jeans spectral radiance, the classical equipartition prediction,

$$B^{\mathrm{RJ}}_\nu(\nu, T) \;=\; \frac{2\nu^2 k_B T}{c^2},$$

and Wien's distribution law, the short-wavelength approximation,

$$B^{\mathrm{W}}_\nu(\nu, T) \;=\; \frac{2h\nu^3}{c^2}\,\exp\!\left(-\frac{h\nu}{k_B T}\right).$$

Write $x = h\nu/(k_B T)$ for the dimensionless frequency. All three radiances are positive on $\nu > 0$; the two comparisons below are stated as ratios, which is the precise form of "agrees with, in this regime".

Formalization targets

Goal

For all $h, c, k_B, T > 0$, all four of the following hold simultaneously:

$$\lim_{\nu \to 0^+} \frac{B_\nu(\nu,T)}{B^{\mathrm{RJ}}_\nu(\nu,T)} = 1, \qquad \lim_{\nu \to \infty} \frac{B_\nu(\nu,T)}{B^{\mathrm{W}}_\nu(\nu,T)} = 1,$$ $$B_\nu(\cdot,T) \in L^1\big((0,\infty)\big), \qquad B^{\mathrm{RJ}}_\nu(\cdot,T) \notin L^1\big((0,\infty)\big).$$

The goal asserts only the shape of the truth - ratios tending to $1$ and membership or non-membership in $L^1$ - and fixes no constant, so it is not invalidated by any sharper rate or by the exact value of the total emission.

Milestones

The four conjuncts are milestones in their own right, together with the two shape-function limits that drive them:

$$\lim_{x \to 0^+} \frac{x}{e^x - 1} = 1, \qquad \lim_{x \to \infty} \frac{e^x}{e^x - 1} = 1 .$$

Significance

The result itself. The two limits are the sense in which Planck's law reproduces Wien's law for short wavelengths and the empirical long-wavelength formula, which is the criterion Planck was working to when he introduced $h$; the non-integrability of $B^{\mathrm{RJ}}_\nu$ is the ultraviolet catastrophe, stated exactly rather than as an asymptotic remark; and the integrability of $B_\nu$ is what makes the total emitted power

• the Stefan-Boltzmann law - a well-defined finite number in the first place. In Lean this last point is not cosmetic: the Bochner integral of a non-integrable function is defined and equal to $0$, so an integral identity such as $\int_0^\infty \pi B_\nu \, d\nu = \sigma T^4$ carries no information until integrability is known separately. This mission supplies that missing side condition for the Stefan-Boltzmann statements already on the platform (CODATA2022.blackbody_exitance_eq_stefanBoltzmann, CODATA2022.bose_einstein_integral_cube), both of which are Open.

Formalizing it. The physics has been settled for over a century; none of it is open mathematics. What is missing is machine-checked statements: the platform's existing black-body development (BlackbodyRadiation_planck, and the mission Planck's Law and Wien's Displacement Law) covers the peak of the spectrum and the exact radiation constants, but not the two classical regimes, and not integrability. The limit and integrability lemmas about $x^n/(e^x-1)$ produced here are reusable for any later work on Bose-Einstein integrals, the Debye model, or the Stefan-Boltzmann constant.

Difficulty

The obvious argument for each limit is a one-line asymptotic expansion, and the obvious argument for integrability is "the integrand decays exponentially". Neither survives contact with a formal proof as stated. The ratio $B_\nu/B^{\mathrm{RJ}}_\nu$ equals $x/(e^x-1)$ only after cancelling $\nu^2$, $c^2$ and $2$, which requires those factors to be nonzero - so the algebraic reduction is valid on a punctured neighbourhood, and must be transported to the limit through a congruence-along-a-filter step rather than by rewriting the function globally. At $\nu = 0$ the ratio is a $0/0$ junk value, which is exactly why the limit is taken within $(0,\infty)$.

For integrability the difficulty is at the two ends at once: near $0$ the integrand is $O(\nu^2)$ but the defining expression is a quotient whose denominator vanishes, and near $\infty$ the exponential decay has to be turned into a dominating integrable function rather than a limit statement. Non-integrability of $B^{\mathrm{RJ}}_\nu$ must be derived from unboundedness of $\int_0^R \nu^2 d\nu$, not asserted from the divergence of the integral, since an unproved-integrability integral in Lean silently evaluates to $0$.

Formalization scope

Everything is over $\mathbb{R}$ with the Lebesgue (volume) measure; $L^1$ membership is MeasureTheory.IntegrableOn ... (Set.Ioi 0) volume, which includes measurability. One-sided limits are filters: $\nu \to 0^+$ is the neighbourhood filter of $0$ restricted to $(0,\infty)$, and $\nu\to\infty$ is Filter.atTop. The three physical parameters and the temperature are explicit real arguments, each carrying its own strict positivity hypothesis; no statement is quantified over a possibly empty set of parameters, and every hypothesis $h,c,k_B,T>0$ is satisfiable, so nothing here is vacuous.

The radiance functions are total: division by zero yields $0$ in Lean, so $B_\nu(0,T) = 0$ and the comparison ratios are $0/0 = 0$ at $\nu = 0$. That is harmless for the limits, which are taken strictly inside $(0,\infty)$, and it is why the integrability statements are on $(0,\infty)$ rather than on $[0,\infty)$. The comparisons are deliberately stated as ratios tending to $1$ rather than as differences tending to $0$: the latter would be a weaker claim, and near $\nu=0$ it would be satisfied by functions that are not asymptotically equal.

Contributions welcome beyond the milestones: the corresponding statements in the wavelength parameterization, quantitative error bounds on the two approximations, and the integrability of $g_n$ on $(0,\infty)$ for general $n$, which would close the remaining gap in the Stefan-Boltzmann chain.

Selected references

• Max Planck, Ueber das Gesetz der Energieverteilung im Normalspectrum, Annalen der Physik 4 (1901) 553-563. https://doi.org/10.1002/andp.19013090310
• Planck constant, Wikipedia. https://en.wikipedia.org/wiki/Planck_constant
• Planck's law, Wikipedia. https://en.wikipedia.org/wiki/Planck%27s_law

Motivation

The encyclopedic account of the speed of light makes two claims that look physical but whose content is mathematical. First, invariance: "the speed of light in vacuum is the same for all observers, no matter their relative velocity", so that light travels at $c$ "regardless of the motion of the source or the inertial reference frame of the observer". Second, unattainability: $c$ "is the upper limit for the speed at which information, matter, or energy can travel through space", and "particles with nonzero rest mass can be accelerated to approach $c$ but can never reach it". The supporting apparatus quoted in the same source is likewise mathematical: the Lorentz factor $\gamma$, which "diverges to infinity as $v$ approaches $c$"; the Lorentz interval, in which spatial and temporal differences "are combined with a negative sign"; and the kinetic energy $(\gamma-1)mc^2$, from which the source concludes that "it would take an infinite amount of energy to accelerate an object with mass to the speed of light".

This mission isolates that mathematical core, in one spatial dimension, over the real numbers, and asks for machine-checked proofs of it. Nothing here depends on the numerical value $c = 299\,792\,458\ \mathrm{m\,s^{-1}}$: every statement is proved for an arbitrary parameter $c > 0$, which is the sense in which the source's claims are structural rather than metrological.

Setting

Fix a real constant $c > 0$, the invariant speed. Work in one spatial dimension, with a spatial coordinate $x \in \mathbb{R}$ and a time coordinate $t \in \mathbb{R}$; speeds are real numbers, and a speed $v$ is called subluminal when $|v| < c$.

Four objects are used throughout, written in the prose exactly as in the mission's Lean development.

Relativistic velocity addition. For speeds $u, v$,

$$u \oplus_c v \;=\; \frac{u+v}{1 + \dfrac{uv}{c^{2}}}.$$

Lorentz factor. For a speed $v$,

$$\gamma_c(v) \;=\; \frac{1}{\sqrt{1 - \dfrac{v^{2}}{c^{2}}}}.$$

Lorentz interval and Lorentz boost. The interval of an event $(x,t)$ is

$$I_c(x,t) \;=\; c^{2}t^{2} - x^{2},$$

and the boost of velocity $v$ sends the event $(x,t)$ to

$$B_c^{\,v}(x,t) \;=\; \Bigl(\gamma_c(v)\,(x - vt),\ \gamma_c(v)\,\bigl(t - \tfrac{vx}{c^{2}}\bigr)\Bigr).$$

Relativistic kinetic energy. For rest mass $m$ and speed $v$,

$$K_c(m,v) \;=\; \bigl(\gamma_c(v) - 1\bigr)\,m\,c^{2}.$$

Formalization targets

Goal

For every $c > 0$ and every rest mass $m > 0$, all three of the following hold:

$$\forall v,\ |v| < c \ \Longrightarrow\ c \oplus_c v = c;$$ $$\forall u, v,\ |u| < c \ \text{and}\ |v| < c \ \Longrightarrow\ |u \oplus_c v| < c;$$ $$\forall E \in \mathbb{R},\ \exists v,\ 0 < v < c \ \text{and}\ E < K_c(m,v).$$

The three conjuncts are, in order, the invariance of light speed under a change of inertial frame, the fact that composing subluminal speeds never reaches $c$, and the unboundedness of the energy required to approach $c$. The goal deliberately asserts only the shape of the claims — no rate of divergence, no numerical constant — so it is not invalidated by any sharper quantitative statement a solver may prove separately.

Milestones

The milestone list decomposes the goal along the four notions above: interval preservation under a boost, invariance of $c$ under composition, closure of the subluminal range under composition, divergence of $\gamma_c$ at $c$, and unboundedness of kinetic energy below $c$.

Significance

The three conjuncts of the goal are what make $c$ a limit rather than merely a large speed. Closure of $\{|v| < c\}$ under $\oplus_c$ says that no finite chain of subluminal boosts produces a luminal speed; invariance says that the boundary of that range is fixed by every boost; the energy statement says that the boundary is not approached at finite cost. Interval preservation is the geometric statement behind them: a boost is an isometry of the quadratic form $c^2t^2 - x^2$, so the light cone $c^2t^2 = x^2$ is frame-independent.

These results are classical and have been standard since the 1905 formulation of special relativity; nothing in this mission is mathematically open. What the mission produces is the machine-checked version and a small reusable layer of one-dimensional relativistic kinematics: a search for declarations mentioning "Lorentz" in the Mathlib revision used for the drafting check returned none, so the definitions here are contributed rather than reused. The statements are stated for an arbitrary $c > 0$, so they can be reused at $c = 1$ (natural units) without restatement.

Difficulty

The algebraic milestones are short once the right nonvanishing facts are in hand, and the obvious first attempt — clear denominators and call a ring normalizer — fails on all of them for the same reason: the denominators $1 + uv/c^2$, $c$, and $1 - v^2/c^2$ must first be shown nonzero, and each of those facts needs the hypothesis $|v| < c$, not merely $c \neq 0$. For velocity addition the usable identities are

$$c\Bigl(1 + \tfrac{uv}{c^{2}}\Bigr) \pm (u+v) = \frac{(c \pm u)(c \pm v)}{c},$$

whose positivity is where the strict inequality comes from.

The analytic milestone is the one that is not formal manipulation: $\gamma_c$ must be shown to tend to $+\infty$ along the punctured left neighbourhood of $c$, which requires the inner expression to be shown positive, not merely convergent to $0$, on a neighbourhood — the one-sided filter is essential, since $\gamma_c$ takes a junk value beyond $c$ (see below).

Formalization scope

All quantities are real; there is no vector or manifold structure, and spacetime is $\mathbb{R}^2$ presented as a pair of coordinates $(x,t)$. The invariant speed $c$ is a parameter with hypothesis $c > 0$; the numerical SI value is never used. The definitions are total functions, so two junk-value conventions are fixed and must be respected when reading the statements:

• $\gamma_c(v)$ uses the real square root, which is $0$ on negative arguments; hence $\gamma_c(v) = 0$ whenever $|v| \ge c$, rather than being undefined or infinite. Every statement about $\gamma_c$ therefore carries an explicit subluminality or one-sided-limit hypothesis.
• $u \oplus_c v$ is a quotient, and division by zero yields $0$; the hypotheses $|u| < c$, $|v| < c$ are what exclude the vanishing denominator.

No statement in the mission is vacuous: each hypothesis set is satisfiable, e.g. by $c = 1$, $u = v = 1/2$, $m = 1$, and the goal quantifies over all $c > 0$ and all $m > 0$.

A complete development needs only Mathlib's real analysis: Real.sqrt, field-simplification and positivity reasoning, and one-sided neighbourhood filters for the divergence milestone. The definition layer (velocity addition, Lorentz factor, interval, boost, kinetic energy) is reusable beyond this mission — natural follow-ups, welcome as contributions, are the associativity and group structure of $\oplus_c$, the rapidity parametrization $v = c\tanh\theta$, time dilation and length contraction, and the composition law for boosts.

Note on the read-backs attached to this proposal

The read-backs attached to the draft items of this proposal are not blind and not independent: they were written by the same agent that drafted the Lean statements, at the explicit instruction of the proposal owner, with full sight of the source material and of the intended meaning. They should be read as an author's restatement, not as independent testimony, and they do not provide the error-catching value of an independent audit.

Selected references

• Speed of light, Wikipedia (source material supplied for this mission), sections "Invariance of $c$ and the Lorentz factor", "Synthesis of space and time", and "Mass and massless particles". https://en.wikipedia.org/wiki/Speed_of_light
• A. Einstein, Zur Elektrodynamik bewegter Körper, Annalen der Physik 17 (1905), 891–921. https://doi.org/10.1002/andp.19053221004