Mathematical Physics

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route (C1 Formal Proofs, §3). Points are arranged in Steiner triple systems, and each point of each line is given one of three roles. The model's claim is that the role postulates alone force the number of points to be exactly seven. This mission proves that claim.

What this mission does NOT prove.

• Not that the system is the Fano plane. It proves the point count is $7$. That every Steiner triple system on $7$ points is the Fano plane up to relabelling is a classical result, but it is not formalized here.
• Not the modelling premise. Why lines have three points, and why there are three roles, is an input of the model, not derived here.
• Not the later steps from the Fano plane to the octonions, and from there to the node size $n = 3$ and $\mathfrak{u}(3)$.

Two corrections to C1 §3 built into this mission.

• At least one point is required. The empty system — no points, no lines — satisfies every condition vacuously and has $0$ points, so C1 Theorem 3.6 as stated is false for it. The goal carries the hypothesis $0 < n$. This is proved (in Lean, locally): the empty system is a Steiner triple system with a role colouring, so the statement without $0 < n$ is false.
• C1 Theorem 3.3(a) is not used. Its condition "any two lines meet" does not force $7$ points: it also holds for a single triple ($3$ points) and a single point, where there is no pair of lines to fail. This mission uses the role postulates instead.

Setting

Fix a natural number $n$ and take the points $\{0, \dots, n-1\}$. A Steiner triple system is a family of subsets, called lines, such that

1. every line has exactly $3$ points, and
2. every pair of distinct points lies on exactly one line.

A role colouring assigns to each point $x$ and line $\ell$ a role $\rho(x, \ell) \in \{0, 1, 2\}$ such that

1. the three points of a line get three different roles;
2. completeness: every point takes every role at least once, on some line through it;
3. minimality: every point takes every role at most once — two different lines through $x$ give $x$ different roles.

In Lean these are RolesForceSeven.STS n and RolesForceSeven.RoleColouring S role, with points Fin n and lines Finset (Fin n).

Formalization targets

Goal: the role postulates force exactly seven points

$$n \ge 1,\ \text{a Steiner triple system on } n \text{ points with a role colouring} \;\Longrightarrow\; n = 7 .$$

This is RolesForceSeven.roles_force_seven. It asserts the point count only.

Milestones

1. M1 (replication count). In any Steiner triple system, every point lies on exactly $r$ lines with $2r + 1 = n$.
2. M2 (three lines per point). Under a role colouring, every point lies on exactly $3$ lines.

Corollaries

• A — the Fano plane has a role colouring. The Fano plane on $\{0, \dots, 6\}$, with lines $\{i, i+1, i+3\}$ modulo $7$, admits a role colouring. Without this the goal could be vacuously true.
• B — AG(2, 3) is excluded (C1 Corollary 3.7): no Steiner triple system on $9$ points has a role colouring.

Significance

The result itself. It turns the model's role postulates into a precise count: whatever the Steiner triple system, if it carries a role colouring and has a point, it has exactly seven points. Corollary A shows the conditions are satisfiable, and Corollary B rules out the next Steiner triple system, AG(2, 3), explicitly.

Formalizing it. The C1 statement omits the non-emptiness hypothesis and is false for the empty system; the formal statement makes the hypothesis explicit and shows it is needed. The numerical check (Fano plane: $48$ role colourings; AG(2, 3): $0$; single triple: $0$) is replaced by a proof for every $n$.

Numerical cross-check

system	points	lines through each point	role colourings
Fano plane	7	3	48
AG(2, 3)	9	4	0
single triple	3	1	0
empty system	0	—	vacuous (all conditions hold)

Difficulty

Moderate. The central step is the replication count: the lines through a point $x$ must be shown to cover every other point exactly once, two at a time, which is a double-counting argument over the pairs through $x$. The role postulates then fix the replication number at three. The Fano plane corollary is a finite check.

Formalization scope

• Points are Fin n; lines are finite sets of points, with no ambient geometry assumed.
• The role function is total, Fin n → Finset (Fin n) → Fin 3; only its values on pairs $x \in \ell$ with $\ell$ a line matter.
• Completeness and minimality are both hypotheses; the goal uses both.
• $0 < n$ is necessary: without it the empty system is a counterexample (proved).
• The conclusion is the number $7$, not an isomorphism with the Fano plane.

Selected references

• Wikipedia, Steiner system (Steiner triple systems, replication number). https://en.wikipedia.org/wiki/Steiner_system
• Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
• Wikipedia, Octonion (Fano plane mnemonic for the multiplication of imaginary units). https://en.wikipedia.org/wiki/Octonion

Motivation

Whether the quantization of the gravitational field is observable is a long-standing question at the interface of general relativity and quantum theory. In his 2013 talk Is a Graviton Detectable? (doi:10.1142/S0217751X1330041X), Freeman Dyson examined three families of hypothetical single-graviton detectors and estimated, for each, why it fails: LIGO-type interferometers (Sec. 3), atoms absorbing a graviton by the gravitoelectric effect (Secs. 4–5), and Gertsenshtein photon–graviton conversion in a magnetic field (Secs. 6–7).

Most of the paper consists of order-of-magnitude physical estimates. A part of it, however, consists of precise mathematical statements: exact algebraic consequences of the stated physical relations, and one genuine analytic inequality about the quadrupole factor $Q$ that controls the graviton absorption cross-section of a bound particle. This mission collects those statements.

Setting

Sections 3. Let $c, G, \hbar > 0$ be the speed of light, Newton's constant and the reduced Planck constant. The Planck length is $L_p = (G\hbar/c^3)^{1/2}$ (Eq. (5)). A gravitational wave of strain amplitude $f$ and angular frequency $\omega$ has energy density $E = \frac{c^2}{32\pi G}\omega^2 f^2$ (Eq. (2)); a single graviton of frequency $\omega$ has energy density at most $E_s = \hbar\omega^4/c^3$ (Eq. (3)).

Section 4. For an electron bound in a state with zero angular momentum about the $z$-axis, with real wave function $f(s,z)$ in cylindrical coordinates ($s>0$ the distance from the $z$-axis), let $f' = \partial f/\partial s$ and define

$$Q = \frac{\int_{\mathbb R}\int_0^\infty s^3 [f']^2\, ds\, dz}{2\int_{\mathbb R}\int_0^\infty s\, f^2\, ds\, dz} \qquad \text{(Eq. (16))}.$$

The s-state of Eq. (19) is $f = r^{-n} e^{-r/R}$ with $r = \sqrt{s^2+z^2}$.

Sections 6–7. For a transverse magnetic field $B$, the mixing length is $L = 2c^2/(G^{1/2}B)$ (Eq. (29)) and the photon-to-graviton conversion probability over a distance $D$ is $P = \sin^2(D/L)$ (Eq. (28)). Vacuum nonlinearity slows the photon by the fraction $g = k\alpha B^2/(360\pi^2 H_c^2)$ (Eq. (36)), where $\alpha$ is the fine-structure constant and $H_c$ the critical field, giving the coherence length $L_c = c/(g\omega)$ (Eq. (37)).

Formalization targets

Goal — Eq. (18)

For every nonzero, normalizable axially symmetric wave function with finite $\int s^3 [f']^2$,

$$Q > \tfrac12 .$$

Milestones

• Eq. (17): $\int\!\!\int s^3\,[f' + f/s]^2\, ds\,dz > 0$ (see the note on the sign below).
• Eq. (20): for the s-state (19), $Q = \frac45\left(1 - \frac n6\right)$.
• Eqs. (4), (6): equating (2) and (3) gives $f = (32\pi)^{1/2} L_p\omega/c$, and with $D = c/\omega$, $\delta = fD = (32\pi)^{1/2}L_p$.
• Eq. (8): free mirrors with $M\delta^2 \ge \hbar T$, $T \ge D/c$, $\delta = L_p$ satisfy $D \le GM/c^2$.
• Eq. (10): clamped mirrors with $\delta^2 \ge \hbar D/(Ms)$, $\delta = L_p$, $s < c$ satisfy $GM/c^2 \ge (c/s)D > D$.
• Eqs. (28)–(30): $P \le GB^2D^2/(4c^4)$, with asymptotic equality as $D \to 0^+$.
• Eq. (37): for $k = 4$, $L_c = 90\pi^2 c H_c^2/(\alpha B^2\omega)$.
• Eqs. (38)–(39): if $D \le L_c$ then $P \le 2025\pi^4 G H_c^4/(\alpha^2 c^2 B^2\omega^2)$ (the symbolic form of $P \le 10^{36}/(B^2\omega^2)$).

Significance

Eq. (18) is what allows Dyson to conclude that the averaged absorption cross-section $4\pi^2L_p^2 Q$ (Eq. (14)) is, for every bound particle, of the order of the Planck area; together with Eq. (20) it shows $Q$ is of order unity for tightly bound s-states. The Section 3 bounds are the precise algebraic content of the argument that measuring distances to Planck accuracy forces the apparatus inside its own Schwarzschild radius. The Section 7 bounds are the algebraic content of the argument that vacuum birefringence limits Gertsenshtein conversion.

None of these statements has, to our knowledge, a machine-checked proof. Eq. (18) is a weighted Hardy-type inequality on the half line with sharp constant, applied slice by slice; formalizing it produces reusable one-dimensional weighted Hardy inequalities. Eq. (20) requires explicit Gamma-function integrals in cylindrical coordinates.

Difficulty

For Eq. (18) the difficulty is analytic: the inequality must hold for all admissible $f$, including functions that are not compactly supported and may be singular on the $z$-axis, and it is strict although its sharp constant is not attained. Boundary terms of the integration by parts behind Eq. (17) must be controlled using only the integrability assumptions. The printed Eq. (17) has the sign $f' - f/s$; with that sign the integral is trivially positive and does not imply Eq. (18). The mission uses $f' + f/s$, the sign under which (17) implies (18). The algebraic milestones are elementary.

Formalization scope

All quantities are real. $f : \mathbb R \to \mathbb R \to \mathbb R$ is a function of $(s,z)$; $f'$ is deriv in the first variable; integrals are Lebesgue integrals over the half plane $\{s > 0\}\times\mathbb R$. The admissible class for Eqs. (17)–(18) is: $f(\cdot,z)$ differentiable at every $s>0$, $s f^2$ and $s^3[f']^2$ integrable on the half plane, and $f$ not almost-everywhere zero there. These hypotheses rule out the degenerate reading $Q = 0/0$ (Lean's division returns $0$). Eq. (20) requires $R > 0$ and $n < 3/2$, the range in which the integrals in Eq. (16) converge. Physical constants are arbitrary positive reals; numerical cgs values (e.g. Eqs. (5), (21), (31)) are not formalized. The heuristic parts of the paper (Bohr–Rosenfeld argument, the sum rule (14), astrophysical source estimates, neutrino backgrounds) are out of scope.

Selected references

• F. Dyson, Is a Graviton Detectable?, Int. J. Mod. Phys. A 28 (2013) 1330041. https://doi.org/10.1142/S0217751X1330041X
• T. Rothman and S. Boughn, Can gravitons be detected?, Found. Phys. 36 (2006) 1801. https://doi.org/10.1007/s10701-006-9081-9
• M. E. Gertsenshtein, Wave resonance of light and gravitational waves, Sov. Phys. JETP 14 (1962) 84.

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) aims to obtain all three factors of the Standard Model gauge structure — $U(1)$, $SU(2)$ and $SU(3)$ — from a single linear-algebra statement applied at three node sizes. A node carrying $n$ oscillator pairs has a $2n$-dimensional real state space with a complex structure $J$. Within the model, the couplings that do no net work (passive couplings) are the symmetric matrices, and those that respect $J$ are the ones commuting with it. The claim is that the couplings satisfying both conditions form a real vector space of dimension exactly $n^2$, which is the dimension of the unitary Lie algebra $\mathfrak{u}(n)$ (Unitary group):

node size $n$	admissible dimension	Lie algebra
1	1	$\mathfrak{u}(1)$
2	4	$\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$
3	9	$\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$

The dimension count has so far been checked numerically for $n = 1, \dots, 5$ only, giving $1, 4, 9, 16, 25$. A machine-checked proof covers every $n$, and it is the claim a physicist examining the model would check first.

What this mission does NOT prove. This mission proves the linear algebra: symmetric matrices commuting with $J$ form a space of dimension $n^2$. It does not prove the physics step that passivity forces a coupling to be symmetric. That step is a separate premise of the model, and a completed mission must not be read as establishing it.

Setting

Fix a natural number $n$. Consider real $2n \times 2n$ matrices, with rows and columns indexed by two copies of $\{0, \dots, n-1\}$, so that each matrix is written in $2 \times 2$ block form with $n \times n$ blocks:

$$W = \begin{pmatrix} A & B \\ C & D \end{pmatrix}.$$

Let $I$ be the $n \times n$ identity matrix and define the standard complex structure

$$J = \begin{pmatrix} 0 & -I \\ I & 0 \end{pmatrix},$$

which satisfies $J^2 = -1$. In the Lean development this matrix is PassivityUn.stdJ n, and the index type is PassivityUn.Blk n, the disjoint union of two copies of Fin n.

Two real linear subspaces of the $4n^2$-dimensional space of such matrices are defined:

1. symm n: the symmetric matrices, $W^{\mathsf T} = W$;
2. commJ n: the matrices commuting with $J$, $WJ = JW$.

The admissible coupling class admissible n is their intersection:

$$\mathcal{A}_n = \{\, W \in \mathbb{R}^{2n \times 2n} : W^{\mathsf T} = W \ \text{and}\ WJ = JW \,\}.$$

Formalization targets

Goal: the admissible class has dimension $n^2$

$$\dim_{\mathbb{R}} \mathcal{A}_n = n^2 \qquad \text{for every } n \in \mathbb{N}.$$

This is PassivityUn.admissible_finrank. It asserts the exact dimension for all $n$ at once, not for a particular node size.

Milestones

1. M1. $J \cdot J = -1$, so $J$ is a complex structure.
2. M2. A block matrix $\begin{pmatrix} A & B \\ C & D \end{pmatrix}$ commutes with $J$ exactly when $D = A$ and $B = -C$.
3. M3. A block matrix $\begin{pmatrix} A & -B \\ B & A \end{pmatrix}$ is symmetric exactly when $A^{\mathsf T} = A$ and $B^{\mathsf T} = -B$.
4. M4. The dimension counts of symmetric and antisymmetric $n \times n$ matrices add to $n^2$: $\tfrac{n(n+1)}{2} + \tfrac{n(n-1)}{2} = n^2$.

Significance

The result itself. The goal identifies the admissible coupling class with the real form of the $n \times n$ Hermitian matrices, the space whose dimension is that of $\mathfrak{u}(n)$ (Hermitian matrix). Applied at $n = 1, 2, 3$ it gives the dimensions $1$, $4$ and $9$, which the Shape Zero model matches with $\mathfrak{u}(1)$, $\mathfrak{u}(2) = \mathfrak{u}(1) \oplus \mathfrak{su}(2)$ and $\mathfrak{u}(3) = \mathfrak{u}(1) \oplus \mathfrak{su}(3)$. Without a proof for general $n$, the model rests on a finite numerical check.

Formalizing it. The underlying fact is standard linear algebra, a special case of the correspondence between real matrices commuting with a complex structure and complex-linear maps (Linear complex structure). No machine-checked statement of this exact dimension count was found in the platform library. The mission produces a verified, general-$n$ statement whose hypotheses are fully explicit, and it separates the verified linear algebra from the unverified physical premise.

Difficulty

Every step is standard linear algebra, so the difficulty is in the formal bookkeeping rather than the mathematics. The dimension of a subspace defined by equations is not computed by any Mathlib tactic. It has to be obtained by exhibiting an explicit linear equivalence with spaces of known dimension, and that requires moving between the $2n \times 2n$ matrix indexed by a disjoint union and its four $n \times n$ blocks. Checking small cases numerically, as has already been done, does not extend to a statement about every $n$.

Formalization scope

• Matrices are real (ℝ), not complex. The complex structure enters only through the fixed real matrix $J$.
• Matrices are indexed by Fin n ⊕ Fin n (PassivityUn.Blk n) rather than Fin (2n), so that block decomposition via Mathlib's Matrix.fromBlocks is direct. The first copy of Fin n indexes the upper/left blocks.
• Each condition is defined as the kernel of a linear map: symmetry as the kernel of $W \mapsto W^{\mathsf T} - W$, and commuting with $J$ as the kernel of $W \mapsto WJ - JW$. Both are therefore subspaces by construction, with no hand-written closure proofs.
• Dimension is Module.finrank ℝ. The ambient space is finite-dimensional, so the convention that finrank of an infinite-dimensional space is $0$ never applies.
• The case $n = 0$ is included, and there the statement reads $0 = 0$. This is not a trivialization: the claim is quantified over all $n$, and every $n \ge 1$ is a nontrivial instance.
• M4 is stated with natural-number division and truncated subtraction. Both are exact here, because $n(n \pm 1)$ is always even and $n \cdot (n - 1) = 0$ when $n = 0$.

The development needs only Mathlib's block matrices, transpose, linear maps and finrank. The block-characterization lemmas (M2, M3) are reusable for any statement relating real matrices commuting with $J$ to complex matrices. Contributions are welcome on the milestones and on the assembling isomorphism.

Selected references

• B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
• Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
• Wikipedia, Linear complex structure. https://en.wikipedia.org/wiki/Linear_complex_structure
• Wikipedia, Hermitian matrix. https://en.wikipedia.org/wiki/Hermitian_matrix
• Mathlib, Mathlib.Data.Matrix.Block (block matrices, Matrix.fromBlocks). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Block.html

Motivation

The g-factor of a particle, nucleus or atom is the dimensionless number that measures its magnetic moment in units of the moment a classical particle with the same charge and angular momentum would have. Because it is both measured and computed to very high precision, small discrepancies between measured and predicted g-factors are used as tests of the Standard Model; the electron g-factor is known to about two parts in $10^{13}$, and the muon g-factor has for two decades shown a several-standard-deviation tension between experiment and theory.

This mission formalizes the mathematical content of the Wikipedia article g-factor (physics): the definitions it gives, the elementary identities it states between them, and the numerical claims it makes about the experimental data.

Setting

All vectors live in $\mathbb R^3$, written as functions $\{0,1,2\}\to\mathbb R$, with component $2$ playing the role of the $z$ component.

• Dirac particle. For charge $e$, mass $m$, spin angular momentum $\mathbf S$ and g-factor $g$, the spin magnetic moment is $\boldsymbol\mu = g\,\frac{e}{2m}\,\mathbf S$ (diracMagneticMoment).
• Nuclear magneton convention. With $\mu_N = \frac{e\hbar}{2m_p}$ (nuclearMagneton), the moment of a nucleon or nucleus with spin $\mathbf I$ is $\boldsymbol\mu = g\,\frac{\mu_N}{\hbar}\,\mathbf I$ (nuclearMagneticMoment).
• Bohr magneton $\mu_B = \frac{e\hbar}{2m_e}$ (bohrMagneton) and electron orbital moment $\boldsymbol\mu_L = -g_L\frac{\mu_B}{\hbar}\mathbf L$ (electronOrbitalMagneticMoment).
• Classical point charges. For finitely many point particles with charges $q_i$, masses $m_i$, positions $\mathbf r_i$ and velocities $\mathbf v_i$, the magnetic moment is $\boldsymbol\mu = \sum_i \frac{q_i}{2}\,\mathbf r_i\times\mathbf v_i$ (classicalMagneticMoment) and the angular momentum is $\mathbf L = \sum_i m_i\,\mathbf r_i\times\mathbf v_i$ (classicalAngularMomentum).

Formalization targets

Goal: the classical baseline has $g = 1$

The article defines the g-factor as the ratio of a particle's magnetic moment to the one "expected of a classical particle of the same charge and angular momentum", and says $g_L = 1$ "by a quantum-mechanical argument analogous to the derivation of the classical magnetogyric ratio". The goal makes that classical baseline precise: for a system whose charge-to-mass ratio is the same for every particle ($q_i = \kappa m_i$, $m_i>0$), with total charge $Q=\sum_i q_i$ and total mass $M=\sum_i m_i$,

$$\boldsymbol\mu \;=\; 1\cdot\frac{Q}{2M}\,\mathbf L .$$

Milestones

1. The two forms of the nuclear-magneton formula agree: $g\frac{\mu_N}{\hbar}\mathbf I = g\frac{e}{2m_p}\mathbf I$.
2. For a particle of proton mass, the Dirac-particle and nuclear-magneton definitions assign the same g-factor.
3. The $z$ component of the electron orbital moment is $-g_L\mu_B m_\ell$, which equals $-\mu_B m_\ell$ when $g_L=1$.
4. The E821 muon result differs from the quoted theoretical prediction by between $3.4$ and $3.5$ combined standard deviations.
5. The relative standard uncertainties in the article's CODATA table round to the values printed there.

Significance

The goal is the statement that fixes the normalization of every g-factor in the article: it says that a classical body with uniform charge-to-mass ratio has gyromagnetic ratio exactly $Q/(2M)$, i.e. $g=1$, so any deviation from $1$ (such as $g_e\approx-2$) is a genuinely non-classical effect. The milestones pin down the conventions (Dirac versus nuclear magneton, sign conventions for the electron orbital moment) and check the numerical claims the article makes from its data. None of these results is new; the contribution is a machine-checked, convention-explicit record of them.

Difficulty

The mathematics is elementary. The work is in the conventions: division by a mass or by $\hbar$ is total in Lean and returns $0$ at $0$, so positivity of masses and of $\hbar$ must be carried explicitly, and the numerical milestones must be stated with the exact decimal values of the source rather than rounded ones.

Formalization scope

• Vectors are Fin 3 → ℝ; the cross product is Mathlib's crossProduct. Component index 2 is the $z$ axis.
• Physical constants are free real parameters; no numerical value of $e$, $\hbar$ or any mass is fixed. Where the source's formula divides by a quantity, the statement assumes it nonzero or positive.
• Uncertainties written as $x(\text{dd})$ in the article are read as a standard uncertainty in the last two digits of $x$; the E821 milestone combines the experimental and theoretical uncertainties in quadrature, which is the standard convention but is not spelled out in the article.
• Not formalized: the finite-nuclear-mass formula $g_L = 1 - 1/M$ and the Landé factor $g_J$, which the article quotes from other sources without derivation.

Selected references

• Wikipedia, g-factor (physics). https://en.wikipedia.org/wiki/G-factor_(physics)
• G. W. Bennett et al. (Muon g−2 Collaboration), Final report of the E821 muon anomalous magnetic moment measurement at BNL, Phys. Rev. D 73, 072003 (2006). https://doi.org/10.1103/PhysRevD.73.072003
• NIST, CODATA Internationally recommended values of the fundamental physical constants. https://physics.nist.gov/cuu/Constants/

Motivation

Since the 2019 revision of the SI, every unit in the system is fixed by assigning exact numerical values to seven defining constants: the caesium hyperfine transition frequency $\Delta\nu_{\mathrm{Cs}}$, the speed of light $c$, the Planck constant $h$, the elementary charge $e$, the Boltzmann constant $k$, the Avogadro constant $N_{\mathrm A}$ and the luminous efficacy $K_{\mathrm{cd}}$. Six of the seven base units — every one except the mole — therefore carry $\Delta\nu_{\mathrm{Cs}}$ in their definition, and the caesium standard is the anchor of the whole system. The first caesium clock was built by Louis Essen and Jack Parry in 1955 (Nature 176, 280); the caesium frequency was tied to the ephemeris second by Markowitz, Hall, Essen and Parry in 1958 (Phys. Rev. Lett. 1, 105); the 13th CGPM adopted the caesium definition of the second in 1967, the CIPM added the "atom at rest at $0\ \mathrm K$" qualification in 1997, the metre was redefined in terms of $c$ and the second in 1983, and the 26th CGPM fixed the present constant-based system in 2018, effective 2019 (Resolution 1 (2018)).

The audience for this mission is anyone who relies on those conversion factors being right: metrology, unit-aware computation, and formal libraries that want a machine-checked statement of what the SI actually fixes, rather than a table copied by hand.

Setting

All seven defining constants are exact decimal numbers, hence exact rationals:

$$\Delta\nu_{\mathrm{Cs}} = 9\,192\,631\,770,\qquad c = 299\,792\,458,\qquad h = 6.626\,070\,15\times10^{-34},$$ $$e = 1.602\,176\,634\times10^{-19},\qquad k = 1.380\,649\times10^{-23},$$ $$N_{\mathrm A} = 6.022\,140\,76\times10^{23},\qquad K_{\mathrm{cd}} = 683,$$

each understood as the numerical value of the constant in its SI unit (hertz, metres per second, joule seconds, coulombs, joules per kelvin, reciprocal moles, lumens per watt).

From these one forms the four parameters of the caesium-133 hyperfine transition radiation:

$$\Delta t_{\mathrm{Cs}} = \frac{1}{\Delta\nu_{\mathrm{Cs}}},\qquad \Delta\lambda_{\mathrm{Cs}} = \frac{c}{\Delta\nu_{\mathrm{Cs}}},\qquad \Delta E_{\mathrm{Cs}} = h\,\Delta\nu_{\mathrm{Cs}},\qquad \Delta M_{\mathrm{Cs}} = \frac{\Delta E_{\mathrm{Cs}}}{c^{2}},$$

its period, wavelength, photon energy and photon mass equivalent. The optical units bring in one further radiation, of frequency $\nu_{\mathrm{opt}} = 5.4\times10^{14}$ Hz, with period $t_{\mathrm{opt}} = 1/\nu_{\mathrm{opt}}$, wavelength $\lambda_{\mathrm{opt}} = c/\nu_{\mathrm{opt}}$, photon energy $E_{\mathrm{opt}} = h\,\nu_{\mathrm{opt}}$ and luminous energy per photon $K_{\mathrm{cd}}\,E_{\mathrm{opt}}$.

Formalization targets

Goal — the seven base units in the defining constants

$$\begin{aligned} 1\ \mathrm s &= \frac{9\,192\,631\,770}{\Delta\nu_{\mathrm{Cs}}}, & 1\ \mathrm m &= \frac{9\,192\,631\,770}{299\,792\,458}\,\frac{c}{\Delta\nu_{\mathrm{Cs}}},\\[2pt] 1\ \mathrm{kg} &= \frac{8.987\,551\,787\,368\,1764\times10^{40}}{6.091\,102\,297\,113\,866\,55}\, \frac{h\,\Delta\nu_{\mathrm{Cs}}}{c^{2}}, & 1\ \mathrm A &= \frac{10^{9}}{1.472\,821\,982\,686\,006\,218}\,e\,\Delta\nu_{\mathrm{Cs}},\\[2pt] 1\ \mathrm K &= \frac{13.806\,49}{6.091\,102\,297\,113\,866\,55}\,\frac{h\,\Delta\nu_{\mathrm{Cs}}}{k}, & 1\ \mathrm{mol} &= \frac{6.022\,140\,76\times10^{23}}{N_{\mathrm A}},\\[2pt] 1\ \mathrm{cd} &= \frac{10^{11}}{3.824\,339\,691\,519\,516\,481\,631\,301\,046\,05}\, h\,\Delta\nu_{\mathrm{Cs}}^{2}\,K_{\mathrm{cd}}. & & \end{aligned}$$

Each line is the assertion that the displayed expression has numerical value exactly $1$.

Milestones

The radiation parameters ($\Delta t_{\mathrm{Cs}}$ and the 1967 definition of the second; $\Delta\lambda_{\mathrm{Cs}}$ and the claim that it lies between $3.26$ and $3.27$ cm; $\Delta E_{\mathrm{Cs}} = 6.091\,102\,297\,113\,866\,55\times10^{-24}$ J; $\Delta M_{\mathrm{Cs}}$); the individual base-unit relations for the kilogram, ampere, kelvin and candela; the derived units of energy, power, force, pressure and absorbed dose; the electromagnetic units, including $1\ \Omega$ as an exact multiple of $h/e^{2}$; the optical units and the parameters of the $540$ THz radiation; the katal; and finally the dependence statement: the formulas for the mole and the coulomb return the same value whatever the caesium frequency, while those for the second, metre, kilogram, ampere, kelvin and candela separate distinct positive frequencies.

Significance

What the results give is a machine-checked transcription of the exact arithmetic content of the 2019 SI: every coefficient in the table of base and derived units, checked against the defining constants rather than against another table. Downstream, a unit-conversion or dimensional-analysis development can cite these identities instead of re-deriving or re-typing sixteen-digit decimals, where a single transposed digit is a silent error.

What formalizing adds is faithfulness checking, not new mathematics. Every statement in this mission is a true identity between exact rational numbers; none of them is open in the mathematical sense.

Difficulty

This mission is arithmetically easy on purpose, and that should be stated plainly: each target is an equality between explicit rational numbers, and a solver who unfolds the constants and normalizes the arithmetic will close it. There is no analytic content, no limit, no inequality beyond the two decimal bounds on $\Delta\lambda_{\mathrm{Cs}}$.

The real failure mode is transcription. The coefficients carry up to $51$ significant digits (the pascal), they are quotients of two decimals rather than single numbers, and the source displays several of them in a layout where a numerator and a denominator can easily be swapped. A statement that is off in the last digit is false, not approximately true, and is the kind of defect this mission exists to exclude.

Formalization scope

Every quantity is modelled as an element of $\mathbb Q$: the numerical value of the physical quantity in the corresponding SI unit. Dimensions are not tracked. A clause such as "$1\ \mathrm{kg} = \alpha\, h\,\Delta\nu_{\mathrm{Cs}}/c^{2}$" is formalized as the numerical identity $\alpha\, h\,\Delta\nu_{\mathrm{Cs}}/c^{2} = 1$, the unit bookkeeping being carried in the prose only; a development that wants dimensional safety must add a dimension layer on top. Decimal literals are exact rationals, not floating-point numbers, and no real-number approximation enters.

The statements are closed identities between explicit rationals, so none of them can be vacuous: each is either true or false, with no hypothesis to satisfy and no quantifier to exploit. The one quantified statement — the dependence of the unit formulas on the caesium frequency — ranges over all positive rationals and asserts non-equality in six cases and equality in two.

The definition layer is a single file of exact rational constants and the caesium radiation parameters; it is reusable by any later unit-related development. Contributions that would extend the mission usefully: a dimension-tracking layer over these constants, and the pre-2019 definitions (the krypton-86 metre, the IPK kilogram, the triple-point kelvin) stated in the same style for comparison.

Selected references

• Bureau International des Poids et Mesures, Resolution 1 of the 26th CGPM (2018) — https://www.bipm.org/en/committees/cg/cgpm/26-2018/resolution-1
• L. Essen, J. V. L. Parry, "An Atomic Standard of Frequency and Time Interval: A Caesium Resonator", Nature 176 (1955) 280–282 — https://doi.org/10.1038/176280a0
• W. Markowitz, R. Hall, L. Essen, J. Parry, "Frequency of Cesium in Terms of Ephemeris Time", Physical Review Letters 1 (1958) 105 — https://doi.org/10.1103/PhysRevLett.1.105
• "Caesium standard", Wikipedia, revision 1328818072 — https://en.wikipedia.org/w/index.php?title=Caesium_standard&oldid=1328818072

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

The Avogadro constant $N_A$ is the conversion factor between an amount of substance and a number of elementary entities (atoms, molecules, ions, ion pairs). Since the 2019 revision of the SI it is a defining constant with the exact value $N_A = 6.02214076\times10^{23}\ \mathrm{mol}^{-1}$; the pure number $N_0 = 6.02214076\times10^{23}$ is called the Avogadro number. Before 2019 the mole was instead defined as the amount of substance in 12 grams of carbon-12, so $N_0$ was a measured quantity: the number of carbon-12 atoms in 12 g, equivalently the number of daltons in a gram, $N_0 = \mathrm{g}/\mathrm{Da}$. The two definitions agree to within the experimental uncertainty of the dalton, but no longer by fiat.

The relations that carry this content — $n(X) = N(X)/N_A$, $M(X) = m(X)\,N_A$, $V_m = v\,N_A$, $n_a = 1/N_A$, and the crystal/unit-cell count used by the Avogadro Project's X-ray crystal density measurements on silicon-28 spheres — are stated in every chemistry course and used without further comment. They are elementary, but they are also exactly the kind of unit-bookkeeping that is easy to state loosely and easy to get wrong by a factor, and they have no machine-checked formulation.

Setting

Fix a common positive scale for masses, volumes and amounts, and record on it three units: a mass unit $\mathrm{g}$ (gram), a second mass unit $\mathrm{Da}$ (dalton), and an amount unit $\mathrm{mol}$ (mole), each a strictly positive real number. Write

$$N_0 = 6.02214076\times10^{23}, \qquad N_A = \frac{N_0}{\mathrm{mol}} .$$

For a sample containing $N$ entities, its amount of substance is $n = N/N_A$; for an entity of mass $m$, the molar mass is $M = m\,N_A$; for an entity occupying volume $v$, the molar volume is $V_m = v\,N_A$; the elementary amount is $n_a = 1/N_A$. For a crystal of volume $V$ whose unit cell has volume $v_{\text{cell}} > 0$ and contains $k$ entities, the number of entities in the crystal is $k\,V/v_{\text{cell}}$.

All of these are modelled as real numbers; units appear as positive real parameters rather than as a dimension system, so every statement below is an identity between real numbers that holds for every admissible choice of $\mathrm{g}$, $\mathrm{Da}$, $\mathrm{mol}$.

Formalization targets

Goal — the gram-to-dalton ratio

Under the pre-2019 definition of the mole, let $m_{\mathrm{C}} > 0$ be the mass of one carbon-12 atom, let $N$ satisfy $N\,m_{\mathrm{C}} = 12\,\mathrm{g}$ (a mole of carbon-12 weighs 12 grams), and let the dalton be one twelfth of the mass of a carbon-12 atom, $\mathrm{Da} = m_{\mathrm{C}}/12$. Then

$$N = \frac{\mathrm{g}}{\mathrm{Da}} .$$

That is: the Avogadro number under the old definition is exactly the number of daltons in a gram. The goal fixes no numerical value — it asserts the shape of the relation, and so survives any revision of the measured value of the dalton.

Milestones

The six milestone lemmas are the remaining relations the source states: the inversion $n(X)\,N_A = N(X)$; the 2019 statement $M(X)\cdot\mathrm{mol} = N_0\,m(X)$; the elementary-amount identity $1\,\mathrm{mol} = N_0\,n_a$; the pre-2019 numerical coincidence that a particle of mass $12\,\mathrm{Da}$ has molar mass exactly $12\,\mathrm{g}/\mathrm{mol}$ when $N_A = (\mathrm{g}/\mathrm{Da})\,\mathrm{mol}^{-1}$; the worked numerical example that a water molecule occupies about $0.030\ \mathrm{nm}^3$ when the molar volume of water is $18\ \mathrm{mL}/\mathrm{mol}$; and the crystal/unit-cell amount relation.

Significance

The result itself is not new mathematics: each identity is one line of algebra once the model is fixed. What the mission produces is the model — a single, audited Lean formulation of amount of substance, molar mass, molar volume, the elementary amount, and the crystal count, in which the pre-2019 and post-2019 definitions of the mole can both be stated and compared, and in which the one place where the two definitions differ (the dalton is measured, the Avogadro number is fixed) is visible rather than hidden in a convention. That layer is reusable by any later formalization that needs to convert between microscopic and molar quantities, including the X-ray crystal density determination of $N_A$ from silicon-28 lattice measurements.

Status honesty: everything stated here is standard, textbook-level content, and all seven statements have been checked to be provable in the model as formalized. The mission's value is the faithful encoding and the audited definition layer, not the difficulty of the proofs.

Difficulty

The proofs are elementary real algebra; the difficulty is entirely in the statements. Two traps recur. First, division in Lean is total, so an identity such as $n = N/N_A$ carries no information at $N_A = 0$ and can be satisfied vacuously; every statement here therefore either derives positivity from the unit data or takes the nondegeneracy hypothesis explicitly. Second, it is easy to write a unit relation that is true only for one choice of units — for instance, conflating the numerical value $N_0$ with the dimensional constant $N_A = N_0/\mathrm{mol}$ — and such a statement still compiles. Readers auditing this proposal should check each statement against both failure modes.

Formalization scope

Units are positive real parameters bundled in a structure carrying $\mathrm{g}, \mathrm{Da}, \mathrm{mol}$ together with proofs of their positivity; there is no dimension-tracking type system. Amounts, masses, volumes and entity counts are real numbers (the crystal's entities-per-cell count is a natural number). The Avogadro number is the exact rational $602214076\times10^{15}$, so the numerical milestone is a genuine rational-arithmetic bound, not a floating-point approximation. The water example is stated as a strict two-sided bound, $0.0298\ \mathrm{nm}^3 < v < 0.0300\ \mathrm{nm}^3$, so that it cannot be satisfied by a rounded value.

A trivializing formalization is ruled out as follows: no statement is of the form "some quantity exists", every statement quantifies over an arbitrary admissible unit system, and the goal's hypotheses are simultaneously satisfiable (take $\mathrm{g} = 1$, $m_{\mathrm{C}} = 12/N$ for any $N > 0$), so the goal is not vacuous.

Contributions welcome: a dimension-typed refinement of the unit layer, and the X-ray crystal density relation $N_A = n M/(\rho a^3)$ for a cubic lattice, which the source describes only qualitatively and which is deliberately not claimed here.

Selected references

• Wikipedia, Avogadro constant. https://en.wikipedia.org/wiki/Avogadro_constant (the uploaded snapshot is the source of record for this mission).
• Bureau International des Poids et Mesures, The International System of Units (SI), 9th edition, 2019. https://www.bipm.org/en/publications/si-brochure

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 gravitational constant $G$ is the proportionality constant in Newton's law of universal gravitation and, through the Einstein gravitational constant $\kappa = 8\pi G/c^4$, in the Einstein field equations. It is the least precisely known of the fundamental constants: the CODATA-recommended value is $G = 6.674\,30(15)\times 10^{-11}\ \mathrm{m^3\,kg^{-1}\,s^{-2}}$, a relative standard uncertainty of $2.2\times 10^{-5}$, and published high-precision measurements since the 1980s have at times been mutually exclusive. Everything that is known about $G$ is known through a small number of algebraic identities that convert a measurable quantity - a surface acceleration, a mean density, an orbital period - into a value of $G$. Those identities, not the measurements, are what can be formalized, and they are what this mission collects.

The identities themselves are classical: the inverse-square law dates to Newton's Principia (1687), the notation $G$ to C. V. Boys in the 1890s, and the first laboratory determination to the Cavendish experiment of 1798, which reported a mean Earth density of $5.448(33)\ \mathrm{g\,cm^{-3}}$ - equivalent to $G = 6.74(4)\times 10^{-11}$ in modern units, about $1\%$ above the modern value. The route from "mean density of the Earth" to "value of $G$" is exactly one of the identities below.

Setting

All quantities are real numbers; no dimensional type discipline is imposed, and units are handled explicitly where they matter (see Formalization scope).

For a gravitational constant $G$, point masses $m_1, m_2$ and a centre-to-centre distance $r$, the Newtonian force is

$$F(G, m_1, m_2, r) = \frac{G\,m_1 m_2}{r^2}.$$

For a spherically symmetric body of mass $M$ and radius $R$, the surface gravity ("small $g$", as opposed to "big $G$") is

$$g(G, M, R) = \frac{G M}{R^2},$$

the ball volume is $V(r) = \tfrac{4}{3}\pi r^3$, and the mean density is $\rho(M,R) = M / V(R)$.

A circular orbit of radius $r$ and period $P$ about a mass $M$ is the condition that the centripetal acceleration equals the gravitational acceleration:

$$r > 0,\qquad P > 0,\qquad \left(\frac{2\pi}{P}\right)^2 r = \frac{G M}{r^2}.$$

The Einstein gravitational constant is $\kappa(G,c) = 8\pi G/c^4$.

Formalization targets

Goal - $G$ from an orbit

For $G > 0$, $M > 0$ and a circular orbit of radius $r$ and period $P$ about $M$,

$$G \;=\; \frac{3\pi\,V(r)}{P^2 M},\qquad V(r) = \tfrac{4}{3}\pi r^3.$$

This is the article's statement that $G$ is fixed by the period of an orbit and the volume it encloses. It is the weakest stable form of the orbital identity: no numerical value of $G$, no unit system, and no choice of body are hard-coded into it.

Supporting levels

The milestone list refines the goal into the chain the source uses: the "big $G$ / small $g$" relation, its mean-density form (the Schiehallion-Cavendish route), $P^2 = 4\pi^2 r^3/(GM)$, Kepler's third law for circular orbits, the grazing-satellite form $P^2 = 3\pi/(G\rho)$, the relation to $\kappa$, and the SI $\leftrightarrow$ cgs conversion of the recommended numerical value.

Significance

The result itself. The identities in this mission are the bridge between what an experiment measures and the number reported for $G$: the mean-density form is what turns the Schiehallion and Cavendish results into values of $G$; the orbital form is what makes the product $GM$ (the standard gravitational parameter, known far more accurately than either factor) the quantity celestial mechanics actually uses; the $\kappa$ relation is what carries the Newtonian constant into general relativity.

Formalizing it. No claim here is open mathematics - each target is a consequence of real-field algebra, and the mission's contribution is a single, faithful, reusable Lean vocabulary for elementary Newtonian gravitation (force, surface gravity, mean density, circular orbits) together with machine-checked statements of the identities the literature quotes informally. The mission is a formalization task, not a research task, and it is presented as such.

Difficulty

The mathematical content is elementary; the difficulty is entirely in faithfulness, and it has two specific sources.

First, division in Lean's real numbers is total: $x/0 = 0$. Several of these identities are therefore true but empty at degenerate arguments unless positivity hypotheses are stated, and conversely it is easy to over-hypothesize and end up proving a weaker claim than the source states. Each statement below fixes a particular choice, and that choice is the thing to audit.

Second, the SI/cgs target is a claim about units, which have no primitive representation here. It is stated in a model where each unit symbol is a real scale factor constrained by the relations between the systems; the honest reading of that target is "the two printed numerical values denote the same quantity given $1\ \mathrm{m} = 100\ \mathrm{cm}$, $1\ \mathrm{kg} = 1000\ \mathrm{g}$ and $1\ \mathrm{dyn} = 1\ \mathrm{g\,cm\,s^{-2}}$", and nothing stronger.

Formalization scope

Everything is over $\mathbb{R}$. The definition layer is a single definition item providing newtonForce, surfaceGravity, ballVolume, meanDensity, einsteinConstant, the predicate IsCircularOrbit, and the numerical constant gravitationalConstantSI $= 6.674\,30\times 10^{-11}$; every theorem in the mission is phrased through those, so the definition layer is the part that must be audited first.

The orbit condition is stated as a predicate on $(G, M, r, P)$ carrying $r>0$ and $P>0$, rather than as a derived function, so that no target is vacuous: for every $G>0$, $M>0$ and $r>0$ there is a $P$ satisfying it, so the hypotheses of the orbital targets are satisfiable, and the targets are not true merely for want of instances. No target is stated as an existence claim that a witness construction could trivialize.

Units are modelled as real scale factors rather than by a dimensional type system; a solver who wants a genuinely dimension-typed treatment is welcome to contribute it as a separate development, but the target here is the scale-factor statement.

A complete development needs nothing beyond Mathlib's ordered-field and Real.pi API. The definition layer is intended to be reusable by any later mission on Newtonian gravitation, orbital mechanics, or unit conversion.

Selected references

• Wikipedia, Gravitational constant, https://en.wikipedia.org/wiki/Gravitational_constant (the mission's source text).
• E. Tiesinga, P. J. Mohr, D. B. Newell, B. N. Taylor, CODATA recommended values of the fundamental physical constants: 2018, Rev. Mod. Phys. 93, 025010 (2021), https://doi.org/10.1103/RevModPhys.93.025010.
• H. Cavendish, Experiments to determine the density of the Earth, Phil. Trans. R. Soc. London 88, 469-526 (1798), https://doi.org/10.1098/rstl.1798.0022.

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