All missions

Motivation

Runtime monitoring checks a running system against a specification by inspecting its trace of events as it is produced. Policies on data, such as "every published report was approved within the last 10 days" or "each value stored in in reaches out within 5 time units", quantify over data values and constrain the time between events. Metric first-order temporal logic (MFOTL) expresses such policies: it extends first-order logic with past and future temporal operators that carry intervals of allowed time differences.

Basin, Klaedtke, Müller and Zălinescu (J. ACM 62(2), Article 15, 2015) give a monitor for MFOTL properties $\square\Phi$ with $\Phi$ bounded. It allows negation and quantification over the infinite domain $\mathbb N$ without restriction, because every relation it manipulates is represented by a finite automaton: the input structures are automatic structures. The paper implements it in the prototype tool MonPoly-Reg (§6). Its correctness rests on Theorem 3.9: the monitor reports exactly the violations of $\Phi$, at every time point.

Setting

A signature $S=(C,R,\iota)$ has finitely many constants and predicates with arities. Formulas are built from $t\approx t'$ and $r(t_1,\dots,t_{\iota(r)})$ by $\neg$, $\vee$, $\exists x$ and the temporal operators $\bullet_I$ (previous), $\circ_I$ (next), $\mathsf S_I$ (since) and $\mathsf U_I$ (until), where $I=[b,b')$ is a nonempty interval of $\mathbb N$ with $b'\in\mathbb N\cup\{\infty\}$. A formula is bounded if every $\mathsf U_I$ in it has $b'<\infty$.

A temporal structure $(\bar{\mathcal D},\bar\tau)$ assigns to each time point $i\in\mathbb N$ relations $r^{\mathcal D_i}\subseteq\mathbb N^{\iota(r)}$ and a time stamp $\tau_i\in\mathbb N$; constants are rigid, $\tau_0\le\tau_1\le\cdots$, and $\bar\tau$ exceeds every bound. Satisfaction $(\bar{\mathcal D},\bar\tau,v,i)\models\varphi$ is Definition 2.2; for example $\psi\,\mathsf U_I\,\psi'$ holds at $i$ if $\psi'$ holds at some $j\ge i$ with $\tau_j-\tau_i\in I$ and $\psi$ holds at all $k\in[i,j)$. For $\varphi$ with free variables $x_1<\dots<x_n$, the satisfying set is

$$\varphi^{(\bar{\mathcal D},\bar\tau,i)}=\{\bar d\in\mathbb N^n\mid(\bar{\mathcal D},\bar\tau,v[\bar x\mapsto\bar d],i)\models\varphi\ \text{for some }v\}.$$

A domain representation is a regular language $\mathcal L$ over a finite alphabet with a surjection $\nu:\mathcal L\to\mathbb N$ whose equality relation is regular. A relation $A\subseteq\mathbb N^k$ is regular if the words $u_1\otimes\cdots\otimes u_k$ (the letter-by-letter convolution, padded with $\#$) with $(\nu(u_1),\dots,\nu(u_k))\in A$ form a regular language.

The monitor $\mathsf M_\Phi$ (Fig. 2) reads $(\mathcal D_0,\tau_0),(\mathcal D_1,\tau_1),\dots$ one element per loop iteration. It extends each $\mathcal D_j$ to $\hat{\mathcal D}_j$ with auxiliary relations $p_\alpha$ (and $r_\alpha$, $s_\alpha$ for since and until) for every temporal subformula $\alpha$, built incrementally by the constructions of §3.4 once a list $Q$ of pending triples $(\alpha,j,S)$ says that enough of the future has been read. When $\hat{\mathcal D}_i$ is complete it outputs the set $(\neg\hat\Phi)^{\hat{\mathcal D}_i}$ with $\tau_i$, where $\hat\Phi$ is $\Phi$ with each top-level temporal subformula $\alpha$ replaced by the atom $p_\alpha(\bar x)$.

Formalization targets

Goal: Theorem 3.9

For every input satisfying the restrictions of §3.1 and every bounded $\Phi$:

$$\text{(i)}\quad (n,O,t)\ \text{output by line 9}\ \Longrightarrow\ O=(\neg\Phi)^{(\bar{\mathcal D},\bar\tau,n)},\ O\ \text{regular},\ t=\tau_n;$$ $$\text{(ii)}\quad \forall n\in\mathbb N,\quad n=0\ \text{or some output at index }n-1\text{ occurs},$$

where each output is followed by line 11 setting $i$ to the next index. This records counter values reached inside the while loop, including values that may never appear at a loop entry. Part (ii) excludes the vacuous reading of (i).

Milestones

1. Lemma 3.4: $\hat\varphi^{\hat{\mathcal D}_i}=\varphi^{(\bar{\mathcal D},\bar\tau,i)}$ once the auxiliary relations of $\mathit{tsub}(\varphi)$ are correct, and regularity is preserved.
2. Lemmas 3.5–3.8: the constructions for $\bullet_I$, $\circ_I$, $\mathsf S_I$ and bounded $\mathsf U_I$ produce regular relations equal to the satisfying sets, with the stated characterizations of $r_\alpha$ and $s_\alpha$.
3. Observations (1)–(3) of the proof of Theorem 3.9 on the list $Q$ and the counter $i$.
4. The claim that line 7 can always be executed, in the form: if $(\alpha,j,\emptyset)\in Q_k$ then the build stores $p_\alpha^{\hat{\mathcal D}_j}=\alpha^{(\bar{\mathcal D},\bar\tau,j)}$, which is regular.

Significance

Theorem 3.9 makes $\mathsf M_\Phi$ a sound and complete monitor for the safety fragment $\square\Phi$, $\Phi$ bounded: every violation at every time point is reported, nothing else is, and every output is a finitely represented (regular) set even though it may be infinite. It covers unrestricted negation and quantification, which finite-relation monitors (§4 of the paper) cannot handle. The incremental constructions of §3.4 are the template reused by later MFOTL monitors.

The paper gives a mathematical proof of its monitor's correctness. This mission asks for a Lean proof that checks the MFOTL semantics, automatic relations over $\mathbb N$, and the correctness of this particular monitor, including the until construction whose printed version is defective (see Formalization scope).

Difficulty

Two parts are hard. The regularity claims need the fundamental property of automatic structures: first-order definable relations are regular, which requires closure of padded convolution languages under Boolean operations, cylindrification, permutation of tracks and projection, the last with removal of trailing padding. The arithmetic constraints of the since and until constructions additionally need successor and offset relations definable from $\prec$.

The scheduling argument is the other part. Correctness of a build at $(\alpha,j)$ requires that every input relation, at time points up to $j+\ell_j$ for until, was built before and not discarded since. Following only the syntax of $\alpha$ does not settle this: a needed relation for a subformula at a later time point may be built in the same iteration as $\alpha$'s.

Formalization scope

The domain is $\mathbb N$, as §3.1 assumes. Relations are sets of lists of natural numbers, ordered by the sorted free variables. Interval upper bounds are in $\mathbb N_\infty$; intervals carry the proof that they are nonempty. The representation $(\mathcal L,\nu)$ is a single parameter shared by the hypothesis "every $r^{\mathcal D_i}$ is regular" and the regularity claims of the conclusions; it is never chosen existentially. The binary predicate $\prec$ interpreted as $<$ is a hypothesis.

Two hypotheses on $\Phi$ besides boundedness are the paper's own "without loss of generality" assumptions: each temporal subformula occurs once in $\Phi$ (§3.6), and the direct subformulas of each $\mathsf S_I$, $\mathsf U_I$ subformula have the same free variables (§3.4; achieved by padding with $x\approx x$, as in §3.5). No other restriction is placed on $\Phi$.

The printed until construction (§3.4.4) is repaired: the guard of $U_r$ is "$\bar a\in\hat\beta^{\hat{\mathcal D}_{i+k}}$ for all $\ell_{i-1}\le k\le\ell_i$", since the printed guard empties $r_\alpha$ in the paper's own example of §3.5; $U_s$ keeps only tuples with $j'\ge1$, since otherwise a $\gamma$-witness at time point $i-1$ survives to time point $i$ when $\tau_i=\tau_{i-1}$; and time-stamp equations are encoded additively. Lemma 3.8(i) reads $\bar a\in\mathbb N^n$ and adds $j\le\ell_i$. "Effectively computable" in Theorem 3.9(i) is not formalized. Part (ii) uses the output at index $n-1$ as the record of the line-11 increment to $n$; for $n=0$, the counter is initialized by line 2. Loop-entry states alone can skip counter values reached within one iteration.

The monitor is a state machine whose builds and outputs are computed only from its store of relations; it never consults the satisfaction relation or satisfying sets. A formalization in which line 7 reads the semantics would turn Theorem 3.9(i) into a restatement of Lemma 3.4, and is ruled out. A build whose input is missing stores nothing, so a monitor that silently fails would violate (ii).

Contributions welcome: the theory of automatic relations (reusable beyond this mission), the semantic halves of Lemmas 3.4–3.8, and the scheduling invariants.

Selected references

• D. Basin, F. Klaedtke, S. Müller, E. Zălinescu, Monitoring metric first-order temporal properties, J. ACM 62(2), Article 15, 2015. https://doi.org/10.1145/2699444

Motivation

A set-valued predictor returns, for each input $x$, a set of plausible responses rather than a single guess. Such sets are used wherever a model's output feeds a decision with asymmetric costs: a medical classifier that lists every diagnosis it cannot rule out, a segmentation model that marks every pixel that may belong to a tumour, a protein-structure predictor that reports a range of distances. Bates, Angelopoulos, Lei, Malik and Jordan, Distribution-Free, Risk-Controlling Prediction Sets (J. ACM 68(6), 2021), calibrate a nested family of such predictors $\{\mathcal T_\lambda\}$ so that a chosen loss is controlled with high probability, without distributional assumptions.

Calibration says nothing about which family to calibrate. Any nested family can be made risk-controlling; families differ in how large their sets are, and large sets are uninformative. §4 of the paper asks which family is best in the population: which predictor achieves a given risk with the smallest expected set size. For a weighted miscoverage loss (Theorem 7, §4.2) the answer thresholds a weighted conditional density, in the spirit of the optimality results of Sadinle, Lei and Wasserman (2019) for classification. Theorem 8 (§4.3) extends the answer to every loss of integral form. This mission formalizes Theorem 8.

Setting

Let $(X, Y)$ take values in $\mathcal X \times \mathcal Y$ with law $P$, marginal $P_X$, and conditional law $\kappa(x)$ of $Y$ given $X = x$. Prediction sets are subsets of a measurable space $\mathcal Z$ (in the paper's examples $\mathcal Z = \mathcal Y$). A set-valued predictor is a map $\mathcal T : \mathcal X \to 2^{\mathcal Z}$.

Fix a finite measure $\mu$ on $\mathcal Z$ and a nonnegative cost $\ell : \mathcal Y \times \mathcal Z \to [0, \infty)$; $\ell(y, z)$ is the cost of leaving $z$ out of the prediction set when the true response is $y$. The loss of a set $\mathcal S$ is the total cost of what it leaves out,

$$L(y; \mathcal S) = \int_{z \in \mathcal S^c} \ell(y, z)\, d\mu(z),$$

and the risk of a predictor is $R(\mathcal T) = \mathbb E[L(Y; \mathcal T(X))]$ (§2.1). Larger sets have smaller loss. The conditional expected cost of omitting $z$ at $x$ is

$$\mathbb E[\ell(Y; z) \mid X = x] = \int \ell(y, z)\, d\kappa(x)(y),$$

and for $\lambda < 0$ the threshold predictor of display (11) is

$$\mathcal T_\lambda(x) = \{z \in \mathcal Z : \mathbb E[\ell(Y; z) \mid X = x] \ge -\lambda\}.$$

It includes exactly the points whose omission is expected to cost at least $-\lambda$. The size of a set is its $\mu$-measure, $|\mathcal S| = \mu(\mathcal S)$, and the expected size of a predictor is $\mathbb E[|\mathcal T(X)|] = \int \mu(\mathcal T(x))\, dP_X(x)$.

In Lean: setLoss μ ℓ y S, risk P μ ℓ T, condLoss κ ℓ x z, thresholdSet κ ℓ lam x and expSize P μ T in the namespace RiskControl.Optimal.

Formalization targets

Goal: Theorem 8

For every $\lambda < 0$ and every set-valued predictor $\mathcal T'$ (with measurable graph),

$$R(\mathcal T') \le R(\mathcal T_\lambda) \implies \mathbb E\big[|\mathcal T_\lambda(X)|\big] \le \mathbb E\big[|\mathcal T'(X)|\big].$$

No constant is involved; the statement is uniform over $\ell$, $\mu$, $P$ and $\mathcal T'$.

Milestones: the steps of the proof (p. 27)

1. Moving the conditional expectation inside the $\mu$-integral: for a predictor $\mathcal A$ with measurable graph, $\mathbb E[\int_{\mathcal A(X)} \ell(Y; z)\, d\mu(z)] = \mathbb E[\int_{\mathcal A(X)} \mathbb E[\ell(Y; z) \mid X]\, d\mu(z)]$.
2. From the risk comparison to the set differences:

$$\mathbb E\Big[\int_{\mathcal T'(X) \setminus \mathcal T_\lambda(X)} \mathbb E[\ell(Y; z) \mid X]\, d\mu\Big] \ge \mathbb E\Big[\int_{\mathcal T_\lambda(X) \setminus \mathcal T'(X)} \mathbb E[\ell(Y; z) \mid X]\, d\mu\Big].$$

3. From costs to sizes: $\mathbb E|\mathcal T'(X) \setminus \mathcal T_\lambda(X)| \ge \mathbb E|\mathcal T_\lambda(X) \setminus \mathcal T'(X)|$.
4. From set differences to sets: $\mathbb E|\mathcal A(X) \setminus \mathcal B(X)| \le \mathbb E|\mathcal B(X) \setminus \mathcal A(X)|$ implies $\mathbb E|\mathcal A(X)| \le \mathbb E|\mathcal B(X)|$.

Significance

The result. Theorem 8 identifies the population-optimal shape of a set-valued predictor for every loss that charges for omitted points through a nonnegative cost and a finite measure. It justifies building nested families by thresholding an estimate of the conditional expected cost: if the estimate were exact, no other predictor with the same or smaller risk could have smaller sets on average. It contains the weighted-miscoverage case (Theorem 7) when $\mathcal Y$ is discrete and $\mu$ is counting measure, and it covers losses for which no such special case exists, such as costs that depend on the distance between $z$ and $y$.

Formalizing it. The proof on p. 27 is a chain of eight displays. A machine-checked version settles the measure-theoretic points the chain passes over: the conditional expectation inside an integral over a random set, the cancellation of possibly infinite terms, and the range of $\lambda$. To our knowledge no formal proof of Theorem 8 or of the Neyman–Pearson-type optimality results it generalizes for set predictors exists in Lean or Mathlib.

Difficulty

The natural reading of the proof subtracts the quantity $\mathbb E\int_{\mathcal Z} \mathbb E[\ell(Y; z) \mid X]\, d\mu(z)$ from both sides of the risk comparison to pass from complements to sets. Nothing in the setting makes this quantity finite, so that step is not valid as written, and a proof that follows the displays literally breaks there. The theorem itself does not need finiteness of $\ell$, and no such hypothesis is in scope.

The other obstacle is measure-theoretic bookkeeping. The conditional expectation $\mathbb E[\ell(Y; z) \mid X]$ is indexed by a point $z$ of a second space, and must be a jointly measurable function of $(x, z)$ before it can be integrated over the random set $\mathcal T(X)$; here it is given by a regular conditional distribution, and every integral over $\mathcal T(x)$ needs the measurability of the graph of $\mathcal T$.

Formalization scope

• Spaces and measures. $\mathcal X, \mathcal Y, \mathcal Z$ are arbitrary measurable spaces; $P$ is a probability measure on $\mathcal X \times \mathcal Y$; $\mu$ is a finite measure on $\mathcal Z$; $\ell$ takes values in $[0, \infty)$ and is jointly measurable.
• Conditional law. $\mathbb E[\ell(Y; z) \mid X = x]$ is $\int \ell(y, z)\, d\kappa(x)(y)$ for a Markov kernel $\kappa$ with $P = P_X \otimes \kappa$, which is exactly the statement that $\kappa$ is a regular conditional distribution of $Y$ given $X$. Such a kernel exists, for instance, when $\mathcal Y$ is standard Borel; the formalization does not assume this. The threshold predictor is built from the same $\kappa$ and the same $\ell$ as the risk; neither is a free object.
• Integrals. Every integral is a lower Lebesgue integral with values in $[0, \infty]$; no integrability hypothesis is made, and an infinite risk is $+\infty$.
• Range of $\lambda$ (correction of the print). The paper states Theorem 8 for $\lambda \in \Lambda \subset (-\infty, 0]$. At $\lambda = 0$ it is false: with $\ell \equiv 0$ and $\mu(\mathcal Z) > 0$, $\mathcal T_0(x) = \mathcal Z$ and $\mathcal T' \equiv \emptyset$ both have risk $0$, but $\mathbb E|\mathcal T'(X)| = 0 < \mu(\mathcal Z)$. The proof divides by $-\lambda$. Theorem 8 and its milestones are posed for $\lambda < 0$.
• Set size (correction of the print). p. 13 describes $|\cdot|$ as Lebesgue or counting measure, a sentence written for Theorem 7. In Theorem 8 the proof measures sets with the measure $\mu$ of the loss, and $|\cdot| = \mu$ throughout.
• Measurable graphs. The competing predictor $\mathcal T'$ is required to have a measurable graph $\{(x, z) : z \in \mathcal T'(x)\}$; otherwise its risk and expected size are not integrals of measurable functions. The page leaves this implicit. The graph of $\mathcal T_\lambda$ is measurable by construction.
• Not a trivialization. The goal is stated about the threshold sets (11) built from the given $\ell$, $\mu$ and $\kappa$, for every competing predictor; it does not assume any of the intermediate inequalities, and its hypotheses are satisfiable (for instance $\ell \equiv 1$, $\lambda = -1/2$, where $\mathcal T_\lambda(x) = \mathcal Z$).

The development needs Mathlib's composition of a measure with a kernel, Tonelli's theorem for kernels and lower integrals over sections of a measurable set. Lemmas about expected $\mu$-sizes of random sets (milestone 4) and about moving a kernel integral inside a set integral (milestone 1) are reusable beyond this mission. Proofs of the milestones, and of the goal by other routes, are welcome.

Selected references

• S. Bates, A. Angelopoulos, L. Lei, J. Malik, M. I. Jordan, Distribution-Free, Risk-Controlling Prediction Sets, Journal of the ACM 68(6), 2021. arXiv:2101.02703v3. https://arxiv.org/abs/2101.02703 — Theorem 8, p. 13; proof p. 27.
• M. Sadinle, J. Lei, L. Wasserman, Least Ambiguous Set-Valued Classifiers With Bounded Error Levels, Journal of the American Statistical Association 114(525), 2019. https://doi.org/10.1080/01621459.2017.1395341

Motivation

A trained classifier or regressor returns a point prediction, but many uses of machine learning need a prediction set: a set of plausible labels together with a guarantee about how often, or how badly, it misses the truth. Medical imaging, protein structure prediction and multi-label classification are examples where a user wants a set whose expected loss is bounded, not just a best guess. Bates, Angelopoulos, Lei, Malik and Jordan (arXiv:2101.02703, J. ACM 68(6), 2021) give a procedure that wraps any black-box predictor and returns sets whose risk is controlled, with no assumption on the data distribution beyond i.i.d. calibration data.

The procedure generalizes split conformal prediction (Vovk, Gammerman and Shafer, 2005) and the tolerance regions of Wilks (1941), which control only the probability of missing the label, to an arbitrary monotone loss on sets (false-negative rate, coverage of a segmentation mask, a hierarchical loss). This mission formalizes its central guarantee, Theorem 1 (p. 5), together with the abstract form Theorem A.1 (p. 26) from which the paper derives it.

Setting

Let $(X, Y)$ be a random pair in $\mathcal X \times \mathcal Y$ with law $P$, and let $\mathcal Z$ be a set of labels. A set-valued predictor is a map $\mathcal T : \mathcal X \to 2^{\mathcal Z}$. The paper considers a family $\{\mathcal T_\lambda\}_{\lambda \in \Lambda}$ indexed by a closed set $\Lambda \subseteq \mathbb R \cup \{\pm\infty\}$ that is nested:

$$\lambda_1 < \lambda_2 \implies \mathcal T_{\lambda_1}(x) \subseteq \mathcal T_{\lambda_2}(x). \tag{1}$$

A loss on sets $L(y, S) \ge 0$ is required to decrease as the set grows:

$$S \subseteq S' \implies L(y, S) \ge L(y, S'). \tag{2}$$

The risk of $\mathcal T_\lambda$ is $R(\lambda) = \mathbb E[L(Y, \mathcal T_\lambda(X))]$, and the section assumes some $\lambda_{\max} \in \Lambda$ with $R(\lambda_{\max}) = 0$.

A risk-controlling prediction set at levels $(\alpha, \delta)$ (Definition 1, p. 2) is a data-dependent predictor $\mathcal T$ with $R(\mathcal T) \le \alpha$ with probability at least $1 - \delta$.

Given an i.i.d. calibration sample $D = ((X_1, Y_1), \dots, (X_n, Y_n))$, a pointwise upper confidence bound is a function $\widehat R^+(\lambda) = \widehat R^+(D, \lambda)$ with

$$P\big(R(\lambda) \le \widehat R^+(\lambda)\big) \ge 1 - \delta \quad \text{for each fixed } \lambda. \tag{3}$$

UCB calibration selects

$$\hat\lambda = \inf\big\{\lambda \in \Lambda : \widehat R^+(\lambda') < \alpha \ \ \forall \lambda' \in \Lambda,\ \lambda' \ge \lambda\big\}. \tag{4}$$

In Lean, the risk is RiskControl.UCB.risk P L T lam, the calibration set of (4) for one realization r of $\widehat R^+$ is calSet Λ r α, and $\hat\lambda$ is lambdaHat Λ r α.

Formalization targets

Goal: Theorem 1 (p. 5)

In the setting above, if (3) holds for every $\lambda \in \Lambda$ and $R$ is continuous on $\Lambda$, then

$$P^n\big(R(\mathcal T_{\hat\lambda}) \le \alpha\big) \ge 1 - \delta .$$

Nothing is assumed of $\widehat R^+$ beyond (3); $\alpha$ and $\delta$ are arbitrary reals.

Milestones

1. Monotone risk (§2.1, pp. 4–5): (1) and (2) make $R$ nonincreasing on $\Lambda$.
2. The failure point (proof of Theorem A.1, p. 26, corrected): $\lambda^\dagger = \sup\{\lambda \in \Lambda : R(\lambda) > \alpha\}$ lies in $\Lambda$ and $R(\lambda^\dagger) \ge \alpha$.
3. Failure implies a low bound at $\lambda^\dagger$ (p. 26, corrected): deterministically, $R(\hat\lambda) > \alpha$ implies $\widehat R^+(\lambda^\dagger) < \alpha$.
4. Theorem A.1 (p. 26): for any continuous nonincreasing $R : \Lambda \to \mathbb R$ and any $\widehat R^+$ satisfying (3) on an abstract probability space, $P(R(\hat\lambda) \le \alpha) \ge 1 - \delta$.

Significance

Theorem 1 turns a confidence bound for one fixed parameter into a guarantee for a parameter chosen from the data. No uniform convergence over $\Lambda$ is needed, so any concentration inequality for a mean (Hoeffding, Bentkus, the betting bound of Waudby-Smith and Ramdas) yields a calibration procedure immediately; the paper's Theorems 2–5 and 9–10 are of exactly this form, and the later Learn-then-Test and conformal risk control frameworks build on the same template.

The result is proved in the paper; nothing here is open. What the mission adds is a machine-checked version of an argument whose printed form has a gap. The printed proof of Theorem A.1 introduces $\lambda^* = \inf\{\lambda \in \Lambda : R(\lambda) \le \alpha\}$ and asserts $R(\lambda^*) = \alpha$ "by continuity", which is false when $\Lambda$ is not an interval. Finite grids, the usual choice of $\Lambda$ in practice, are not intervals. The theorem remains true, and milestones 2 and 3 state the corrected steps. No formalization of risk-controlling prediction sets or of conformal prediction is known to exist in Lean or on this platform.

Difficulty

The obvious argument applies the confidence bound at $\hat\lambda$; that fails because $\hat\lambda$ depends on the data, so (3) says nothing at $\lambda = \hat\lambda$. The proof must find one deterministic point at which a failure of calibration forces a failure of (3). The paper's choice $\lambda^*$ works only when $R$ attains the value $\alpha$ on $\Lambda$; on $\Lambda = \{0, 1\}$ with $R(0) = 1$, $R(1) = 0$, $\alpha = 1/2$ and the exact bound $\widehat R^+ = R$, the event $\{\widehat R^+(\lambda^*) < \alpha\}$ has probability one, so the printed last step does not bound anything. The second difficulty is boundary behaviour: $\Lambda$ may contain $\pm\infty$, the infimum in (4) may be over an empty set, and the calibration set need not contain its own infimum.

Formalization scope

• $\Lambda$ is a closed subset of EReal (the extended reals with the order topology); $\lambda$ is only compared, never added. Continuity of $R$ is in the subspace topology of $\Lambda$.
• Set-valued predictions are Set 𝒵, i.e. $\mathcal Y' = 2^{\mathcal Z}$ (the paper uses $2^{\mathcal Y}$ for most of its examples).
• The risk is the published definition WassersteinDRO.Duality.nominalRisk, a Bochner integral. Because a non-integrable integrand integrates to $0$ in Lean, Theorem 1 assumes $(x, y) \mapsto L(y, \mathcal T_\lambda(x))$ is $P$-integrable for every $\lambda \in \Lambda$.
• The standing assumptions of §2.1 are hypotheses of Theorem 1: $\Lambda$ closed, (1) on $\Lambda$, (2), $L \ge 0$, and $R(\lambda_{\max}) = 0$ for some $\lambda_{\max} \in \Lambda$. The monotonicity of $R$ is not assumed in Theorem 1; it is milestone 1. Theorem A.1 assumes it, as printed.
• The i.i.d. sample is Fin n → 𝒳 × 𝒴 under the product measure $P^n$. $\widehat R^+$ is an arbitrary real function of the sample and of $\lambda$; an infinite bound is represented by any value $\ge \alpha$.
• "With probability at least $1 - \delta$" is written as a failure probability at most $\delta$, measured as an outer measure; no measurability of $\widehat R^+$ or $\hat\lambda$ is assumed. For a measurable event this is the page's statement.
• $\hat\lambda$ is an infimum in EReal, so $\inf \emptyset = +\infty$ as on the page. Since $+\infty$ need not belong to $\Lambda$, the failure event is "the set in (4) is nonempty and $R(\hat\lambda) > \alpha$"; when the set is nonempty, $\hat\lambda \in \Lambda$. When it is empty the procedure certifies nothing, and the natural output is $\mathcal T_{\lambda_{\max}}$, of risk $0$.
• Corrections of the print: Theorem A.1's conclusion reads $P(R(\lambda) \le \alpha)$, stated here with $\hat\lambda$; the proof's point $\lambda^*$ and the claim $R(\lambda^*) = \alpha$ are replaced by $\lambda^\dagger = \sup\{\lambda \in \Lambda : R(\lambda) > \alpha\}$ and $R(\lambda^\dagger) \ge \alpha$, which coincide with the page for an interval $\Lambda$.
• A formalization that assumes $R$ monotone in Theorem 1, quantifies over $\widehat R^+$ inside the event, takes a real-valued infimum (which is $0$ on unbounded sets) or drops the integrability guard would state a different theorem; the statement here does none of these.

Needed infrastructure is small: closed subsets of EReal and their infima and suprema (IsClosed.sInf_mem, IsClosed.sSup_mem), continuity within a set, monotonicity of the Bochner integral, and monotonicity of outer measure. Proofs of the milestones are welcome individually; the deterministic milestones 2 and 3 are reusable for every UCB-calibration theorem of the paper.

Selected references

• S. Bates, A. Angelopoulos, L. Lei, J. Malik, M. I. Jordan, Distribution-Free, Risk-Controlling Prediction Sets, J. ACM 68(6), 2021; arXiv:2101.02703v3. https://arxiv.org/abs/2101.02703
• V. Vovk, A. Gammerman, G. Shafer, Algorithmic Learning in a Random World, Springer, 2005. https://doi.org/10.1007/b106715
• S. S. Wilks, Determination of sample sizes for setting tolerance limits, Ann. Math. Statist. 12(1), 1941. https://doi.org/10.1214/aoms/1177731788
• I. Waudby-Smith, A. Ramdas, Estimating means of bounded random variables by betting, arXiv:2010.09686, 2020. https://arxiv.org/abs/2010.09686

Motivation

Trained neural networks are increasingly embedded inside optimization models: to verify that a classifier is robust to small input perturbations, to optimize over a learned surrogate of an expensive system, or to choose decisions whose outcome is predicted by a network. When the network uses rectified linear units (ReLU), each neuron $y=\max\{0,\,w\cdot x+b\}$ is piecewise linear, and the whole network can be written exactly as a mixed-integer program (MIP) with one binary variable per neuron. How fast a branch-and-bound solver closes such a model depends on how tight the linear-programming relaxation of each neuron's formulation is.

Anderson, Huchette, Tjandraatmadja and Vielma (arXiv:1811.08359v2, the IPCO 2019 extended abstract) gave a formulation (6) of a single ReLU neuron over a box that uses only the original variables and one binary variable, and is ideal: its LP relaxation has integral extreme points (Proposition 1, p. 6). The price is an exponential family of inequalities (6b), one for every subset $I$ of the support of $w$. The present mission formalizes their Proposition 2: each of these inequalities is facet-defining, so no member of the family can be dropped without weakening the relaxation. A longer journal version of the work, with different numbering, appeared later (arXiv:1811.01988); this mission follows the extended abstract.

Setting

Fix $\eta\in\mathbb N$, a weight vector $w\in\mathbb R^\eta$, a bias $b\in\mathbb R$, and bounds $L,U\in\mathbb R^\eta$ with $L_i<U_i$ for every $i$ (§1.3, p. 4). Write $f(x)=w\cdot x+b$ and $[L,U]=\{x : L\le x\le U\}$. The sign-adjusted bounds are

$$\breve L_i=\begin{cases}L_i & w_i\ge 0\\ U_i & w_i<0\end{cases},\qquad \breve U_i=\begin{cases}U_i & w_i\ge 0\\ L_i & w_i<0\end{cases},$$

so that $M^+(f)=w\cdot\breve U+b$ and $M^-(f)=w\cdot\breve L+b$ are the maximum and minimum of $f$ over $[L,U]$. The support is $\operatorname{supp}(w)=\{i : w_i\neq 0\}$. Strict activity means $M^-(f)<0<M^+(f)$: the neuron is neither always off nor always on over the box. The paper assumes it throughout (§1.3).

Formulation (6) (p. 6) consists of the points $(x,y,z)$ with

$$\begin{aligned} &y\ge w\cdot x+b, &&\text{(6a)}\\ &y\le\sum_{i\in I}w_i\bigl(x_i-\breve L_i(1-z)\bigr)+\Bigl(b+\sum_{i\notin I}w_i\breve U_i\Bigr)z\quad\forall I\subseteq\operatorname{supp}(w), &&\text{(6b)}\\ &(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}. &&\text{(6c)} \end{aligned}$$

In Lean, form6 w b L U is this set, and relax6 w b L U is its LP relaxation ($0\le z\le1$ in place of $z\in\{0,1\}$). The right-hand side of (6b) for the subset $I$ is rhs6b w b L U I x z.

An inequality $g\le0$ is facet-defining for a set $P$ when it holds on $P$, its face $F=P\cap\{g=0\}$ is nonempty, and $\dim F=\dim P-1$, the dimension of a set being that of its affine hull. The paper uses this standard notion without defining it.

Formalization targets

Goal: Proposition 2 (p. 6)

Under $L<U$ and strict activity, for every $I\subseteq\operatorname{supp}(w)$, the inequality (6b) for $I$ is facet-defining for

$$P=\operatorname{conv}\{(x,y,z) : (x,y,z)\text{ satisfies (6a)–(6c)}\}.$$

The page states the result as "Each inequality in (6b) is facet-defining", and adds right after the proof line: "We require the assumption of strict activity above, as introduced in Section 1.3."

Milestones (App. A.2, p. 15)

1. For some $\varepsilon>0$, the $\eta+2$ points $p^0=(\breve L,0,0)$, $p^1=(\breve U,f(\breve U),1)$, $\tilde p^i=(\breve L+\varepsilon\sigma_ie^i,0,0)$ for $i\notin I$, and $\tilde p^i=(\breve U-\varepsilon\sigma_ie^i,f(\breve U-\varepsilon\sigma_ie^i),1)$ for $i\in I$ are feasible with respect to (6) and satisfy (6b) for $I$ at equality; here $\sigma_i=\pm1$ is the sign of $w_i$ (with $\sigma_i=1$ when $w_i=0$).
2. For every $\varepsilon>0$ these $\eta+2$ points are affinely independent.

Significance

The result. Proposition 1 shows that (6) is ideal; Proposition 2 shows it cannot be made smaller: removing any single inequality (6b) produces a strictly weaker relaxation. Since the family has $2^{|\operatorname{supp}(w)|}$ members, this is what justifies the paper's practical recommendation to start from the big-$M$ formulation and separate inequalities of (6b) on demand (Proposition 3, p. 7) rather than to search for a smaller ideal description in the same variables. The facet structure also gives the geometric picture the paper describes after Proposition 2: each facet is the convex combination of an $(\eta-|I|)$-dimensional face at $z=0$ and an $|I|$-dimensional face at $z=1$.

Formalizing it. The result is proved in the paper, in a half-page appendix; it has not been machine-checked. The formalization adds two things. First, the proof is written for $w\ge0$ "without loss of generality by appropriately interchanging $+$ and $-$"; the Lean statements are for every sign pattern, including zero weights. Second, the appendix exhibits $\eta+2$ affinely independent points on the face, which bounds the face dimension from below; the statement that the face has dimension exactly one less than the polyhedron also needs the polyhedron to be full-dimensional and the face to lie in a proper hyperplane, steps the extended abstract leaves implicit and a complete proof must supply.

Difficulty

The arithmetic in each step is elementary. The work lies in the bookkeeping: choosing a single $\varepsilon$ that keeps every perturbed point inside the box and on the correct side of $f=0$ (this is exactly where strict activity enters), checking the perturbed points against all $2^{|\operatorname{supp}(w)|}$ inequalities of (6b) and not only the one for $I$, and turning a row-reduction argument on an $(\eta+1)\times(\eta+2)$ matrix into a statement about AffineIndependent and finrank of a vectorSpan in Lean. The natural shortcut, proving only that $\eta+2$ affinely independent tight points exist, is not Proposition 2: it says nothing about the dimension of the polyhedron itself.

Formalization scope

Inputs are Fin η → ℝ (indices $0,\dots,\eta-1$ for the paper's $1,\dots,\eta$); a point $(x,y,z)$ is p : (Fin η → ℝ) × ℝ × ℝ with p.1 = x, p.2.1 = y, p.2.2 = z. $M^\pm(f)$ are given by their closed forms $w\cdot\breve U+b$ and $w\cdot\breve L+b$. In (6b), "$i\notin I$" ranges over all indices outside $I$, zero weights included; $I$ ranges over subsets of $\operatorname{supp}(w)$, as on the page.

Every goal and milestone keeps the standing assumptions of §1.3, $L_i<U_i$ for all $i$ and strict activity, except the affine-independence milestone, which holds without them and is stated without them (a stronger statement). No other hypothesis is added. Strict activity excludes $\eta=0$, so no nonemptiness assumption on the index set is needed.

IsFacetDefining P g is the standard notion: validity, a nonempty face, and $\dim F+1=\dim P$ with dimensions the finrank of the vectorSpan. The equation is written with $+1$ on the left so that no natural-number subtraction can make the empty set or a point a facet. The polyhedron is the convex hull of the points of (6), not the set form6 itself (which is not convex, since $z\in\{0,1\}$); by Proposition 1 it equals the LP relaxation relax6, but the statement does not depend on that.

The shared objects of this paper (the ReLU graph, $\breve L$, $\breve U$, $M^\pm$, support, strict activity, formulation (6), ideality) come from the shared definitions module ReluMIP.Ideal.Setting, common to the companion mission on Proposition 1; this mission's own definitions module adds form6, IsFacetDefining, the sign inward, and the indexed family facetPts of the $\eta+2$ points. The facet notion and the affine-independence argument are reusable for other facet proofs of polyhedra in product spaces. Proofs of the milestones, of the goal, and of the full-dimensionality step are all welcome.

Selected references

• R. Anderson, J. Huchette, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, IPCO 2019, LNCS 11480, pp. 27–42; preprint arXiv:1811.08359v2, 2019. https://arxiv.org/abs/1811.08359v2
• R. Anderson, J. Huchette, W. Ma, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, Mathematical Programming 183 (2020), 3–39. https://doi.org/10.1007/s10107-020-01474-5
• G. L. Nemhauser, L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0
• J. P. Vielma, Mixed integer linear programming formulation techniques, SIAM Review 57 (2015), 3–57. https://doi.org/10.1137/130915303

Motivation

Neutrinos are the only Standard Model fermions whose masses, mixing and electromagnetic properties are still largely unknown. The review of Giunti and Studenikin (Rev. Mod. Phys. 87, 531 (2015)) collects the theory of neutrino masses and mixing, the general structure of neutrino electromagnetic form factors for Dirac and Majorana neutrinos, and the dynamics of neutrino spin and flavor in electromagnetic fields and matter. Most of the review is phenomenology (experimental bounds, astrophysical estimates), but a core of it consists of exact mathematical statements about finite-dimensional unitary matrices, Hermitian matrices and two-level linear Schrödinger equations. Those exact statements are what this mission targets.

Timeline of the results formalized here:

• 1957–1968: Pontecorvo; Maki, Nakagawa and Sakata introduce neutrino mixing and oscillations.
• 1957: Case; Radicati and Touschek observe that Majorana neutrinos cannot have diagonal magnetic or electric dipole moments.
• 1971: Cisneros proposes spin precession $\nu_{eL}\to\nu_{eR}$ of solar neutrinos in a magnetic field.
• 1978: Wolfenstein writes the evolution equation of neutrino flavor in matter; 1985: Mikheev and Smirnov identify its resonance (MSW effect).
• 1986: Okun, Voloshin and Vysotsky; Voloshin and Vysotsky show that matter suppresses spin precession.

Setting

A mixing matrix is a unitary $n\times n$ complex matrix $U$ whose rows are labelled by flavors $\ell$ and whose columns are labelled by massive states $k$ with masses $m_k$. For a neutrino of energy $E>0$ that has travelled a distance $L$, the plane-wave transition probability (Eqs. (2.35)–(2.36)) is

$$P_{\nu_\ell\to\nu_{\ell'}}(L,E)=\Bigl|\sum_k U^*_{\ell k}\,e^{-i m_k^2 L/(2E)}\,U_{\ell' k}\Bigr|^2 .$$

In the Lean development this is oscProb U m L E l l'. The standard parametrization $U^{\mathrm D}(\vartheta_{12},\vartheta_{13},\vartheta_{23},\delta_{13})$ of Eq. (2.27) and the Majorana phase matrix $D^{\mathrm M}=\operatorname{diag}(1,e^{i\lambda_{21}},e^{i\lambda_{31}})$ of Eq. (2.28) are diracMixing and majoranaPhases; the two-neutrino rotation matrix of Eq. (2.38) is twoFlavorMixing.

In matter of constant electron density, the $\nu_e$–$\nu_a$ amplitudes $(\varphi_e,\varphi_a)$ obey $i\,\tfrac{d}{dx}\varphi=\mathrm H\varphi$ with the effective Hamiltonian of Eq. (2.46) (mswHamiltonian), built from the vacuum squared-mass difference $\Delta m^2$, the mixing angle $\vartheta$ and the charged-current potential $V_{\rm CC}$ with $A_{\rm CC}=2EV_{\rm CC}$. The effective squared-mass difference $\Delta m^2_{\rm M}$ of Eq. (2.53) and effective angle $\vartheta_{\rm M}$ of Eq. (2.54) are mswDeltaM2 and mswMixingAngle.

Electromagnetic form-factor matrices $\mathbb f_\Omega$ ($\Omega=Q,M,E,A$: charge, magnetic, electric, anapole) are Hermitian $N\times N$ complex matrices in the space of massive neutrinos; for Majorana neutrinos they are in addition antisymmetric ($\Omega=Q,M,E$) or symmetric ($\Omega=A$), Eqs. (3.66)–(3.68).

Finally, the helicity amplitudes $(\psi_L,\psi_R)$ of an ultrarelativistic Dirac neutrino with magnetic moment $\mu$ in a transverse field $B_\perp$ and matter potential $V$ obey $i\,\tfrac{d}{dx}\psi=\begin{pmatrix}V&\mu B_\perp\\ \mu B_\perp&0\end{pmatrix}\psi$ (Eqs. (6.23), (6.28); spinFlavorHamiltonian), with energy splitting $\Delta E_{\rm M}=\sqrt{V^2+(2\mu B_\perp)^2}$ (Eq. (6.31); spinFlavorEnergySplitting).

Formalization targets

Goal: the general vacuum oscillation probability, Eq. (2.37)

For every unitary $U$, all masses $m_k$, every $L$ and every $E>0$,

$$P_{\nu_\ell\to\nu_{\ell'}}=\delta_{\ell\ell'}-4\sum_{k>j}\operatorname{Re}\bigl(U^*_{\ell k}U_{\ell' k}U_{\ell j}U^*_{\ell' j}\bigr)\sin^2\!\Bigl(\frac{\Delta m^2_{kj}L}{4E}\Bigr)-2\sum_{k>j}\operatorname{Im}\bigl(U_{\ell k}U^*_{\ell j}U^*_{\ell' k}U_{\ell' j}\bigr)\sin\!\Bigl(\frac{\Delta m^2_{kj}L}{2E}\Bigr),$$

with $\Delta m^2_{kj}=m_k^2-m_j^2$. The number $n$ of massive states is left free (the paper uses $n=3$, and $n>3$ with sterile neutrinos, Sec. II.F).

Milestones

1. Eqs. (2.26)–(2.28): $U^{\mathrm D}$ and $U^{\mathrm D}D^{\mathrm M}$ are unitary.
2. Eq. (2.39): two-neutrino transition probability $\sin^2 2\vartheta\,\sin^2(\Delta m^2L/4E)$.
3. Eq. (2.40): two-neutrino survival probability $1-\sin^2 2\vartheta\,\sin^2(\Delta m^2L/4E)$.
4. Eqs. (2.50)–(2.54): $U_{\rm M}^T\mathrm H U_{\rm M}=\operatorname{diag}(-\Delta m^2_{\rm M},\Delta m^2_{\rm M})/4E$.
5. Eq. (2.57): MSW transition probability at constant density $\sin^2 2\vartheta_{\rm M}\sin^2(\Delta m^2_{\rm M}x/4E)$.
6. Eqs. (3.66)–(3.70): Majorana form-factor matrices — antisymmetric Hermitian matrices are purely imaginary with vanishing diagonal; symmetric Hermitian matrices are real.
7. Eqs. (3.71)–(3.72): three-flavor antisymmetric Hermitian form factors are $i\sum_j\epsilon^{fij}\tilde{\mathbb f}^j$ with a real vector $\tilde{\mathbb f}$.
8. Eq. (6.27): spin precession in a transverse field, $P_{\nu_L\to\nu_R}(x)=\sin^2\bigl(\int_0^x\mu B_\perp\bigr)$.
9. Eq. (6.34): spin precession in matter, $P_{\nu_L\to\nu_R}(x)=\sin^2 2\xi\,\sin^2(\tfrac12\Delta E_{\rm M}x)$ with $\sin 2\xi=2\mu B_\perp/\Delta E_{\rm M}$.

Significance

Eq. (2.37) is the formula used in essentially every analysis of oscillation data; its two-neutrino specializations (2.39)–(2.40) and the matter formula (2.57) are the standard fitting functions for reactor, accelerator and solar experiments. The Majorana constraints (3.67)–(3.70) are the precise statement behind the claim that a measured diagonal magnetic moment would rule out Majorana neutrinos (under CPT). The spin-precession formulas (6.27) and (6.34) underlie the astrophysical bounds on neutrino magnetic moments.

All targets are established results with textbook derivations; none is open. What the mission adds is machine-checked versions with every convention (sign of the phase, ordering $k>j$, ranges of angles, boundary conditions of the Schrödinger equation) fixed explicitly. Related vacuum-oscillation statements from a different source already exist on the platform under the LipariNeutrino namespace; the present drafts are self-contained and follow this paper's notation and equation numbering.

Difficulty

The algebraic targets require careful bookkeeping of complex conjugation and of the unitarity relations $UU^\dagger=U^\dagger U=1$ inside double sums over $k>j$. The dynamical targets (2.57), (6.27), (6.34) are statements about every solution of a linear ODE with a given initial value, so a solution in closed form is not enough: uniqueness of solutions of the (for (6.27), non-autonomous) linear system must also be established in Lean.

Formalization scope

• Flavor and mass indices are Fin n; two-neutrino indices 0,1 stand for $(\nu_e,\nu_a)$, $(\nu_L,\nu_R)$ or $(\nu_1,\nu_2)$.
• Masses $m_k$ are arbitrary reals and enter only through $m_k^2$.
• Unitarity is membership in Matrix.unitaryGroup.
• The evolution equations are encoded as HasDerivAt φ (-(I • H.mulVec (φ x))) x for all real $x$, i.e. $\varphi'=-i\mathrm H\varphi$, with initial value $(1,0)$.
• $\vartheta_{\rm M}$ is defined as half the argument of $(\Delta m^2\cos2\vartheta-2EV_{\rm CC})+i\,\Delta m^2\sin2\vartheta$, which realizes Eq. (2.54) without the division-by-zero at resonance; $\sin 2\xi=2\mu B_\perp/\Delta E_{\rm M}$ is inlined, with Lean's convention $0/0=0$ in the degenerate case $V=\mu B_\perp=0$.
• The source's angle ranges ($0\le\vartheta\le\pi/2$, $0\le\delta_{13}<2\pi$) and $E>0$ are kept as hypotheses.

Useful reusable infrastructure: uniqueness for linear ODEs in $\mathbb C^2$, closed-form exponentials of $2\times2$ real symmetric matrices, and algebraic lemmas for unitary matrices.

Selected references

• C. Giunti and A. Studenikin, Neutrino electromagnetic interactions: A window to new physics, Rev. Mod. Phys. 87, 531 (2015). https://doi.org/10.1103/RevModPhys.87.531
• C. Giunti and C. W. Kim, Fundamentals of Neutrino Physics and Astrophysics, Oxford University Press (2007).
• L. Wolfenstein, Neutrino oscillations in matter, Phys. Rev. D 17, 2369 (1978). https://doi.org/10.1103/PhysRevD.17.2369

Motivation

C. Baumgarten's essay How to (Un-) Quantum Mechanics (arXiv:1810.06981, v2 2025) argues that much of the mathematical formalism usually presented as specifically "quantum" — Heisenberg's equation of motion, commutators, eigenvalue problems, the real Pauli and Dirac algebras — already follows from classical linear Hamiltonian mechanics on an abstract phase space. The physical and philosophical claims of the paper are outside the scope of a formalization, but its argument rests on a compact chain of linear-algebra facts stated in Sections IV–VI (pp. 13–20). This mission formalizes exactly that chain, so that the mathematical part of the argument can be checked independently of its interpretation.

Setting

Fix a number $n \ge 0$ of degrees of freedom. A phase-space vector is $\psi = (q_1,p_1,\dots,q_n,p_n)^T \in \mathbb R^{2n}$. The symplectic unit matrix is the Kronecker product

$$\gamma_0 = \mathbf 1_n \otimes \eta_0, \qquad \eta_0 = \begin{pmatrix}0 & 1\\ -1 & 0\end{pmatrix}.$$

A real $2n\times 2n$ matrix is Hamiltonian if it equals $\gamma_0 A$ with $A$ symmetric, skew-Hamiltonian if it equals $\gamma_0 B$ with $B$ skew-symmetric, and symplectic if $M\gamma_0M^T = \gamma_0$.

Linear Hamiltonian motion is $\dot\psi = H\psi$ with $H$ Hamiltonian (the paper's Eq. 35, coming from the quadratic Hamiltonian $\tfrac12\psi^TA\psi$). A matrix of second moments $\Sigma(\tau)$ (in the paper an average $\langle\psi\psi^T\rangle$) then evolves by

$$\dot\Sigma = H\Sigma + \Sigma H^T \qquad\text{(Eq. 40)},$$

and the autocorrelation matrix is $S = \Sigma\gamma_0^T$.

Target

The goal theorem combines the conclusions drawn on pp. 16–17: for $H$ Hamiltonian and $\Sigma$ a symmetric solution of Eq. (40), the autocorrelation matrix satisfies, for every time $\tau$,

$$\chi_{S(\tau)} = \chi_{S(0)} \qquad\text{and}\qquad \operatorname{Tr}\big(S(\tau)^{2k+1}\big) = 0 \ \ (k \in \mathbb N),$$

where $\chi$ is the characteristic polynomial: "the eigenvalues are constants of motion" (after Eq. 51) together with Eq. (48).

The milestones follow the paper's own steps, in order:

1. pairing $\pm\lambda$ of eigenvalues of skew-symmetric matrices, and a vanishing eigenvalue in odd size (p. 13);
2. conservation of $H$ under $\dot\psi = J\nabla H$ with $J$ skew (Eqs. 26–28);
3. identities of $\gamma_0$ and the transpose rules for (skew-)Hamiltonian matrices (Eqs. 33, 36, 54);
4. $\exp(H\tau)\psi_0$ solves $\dot\psi = H\psi$ (Eq. 49);
5. Heisenberg's equation $\dot S = [H,S]$ for second moments (Eq. 42);
6. the Lax invariants $\operatorname{Tr}(S^k)$ (Eq. 47) and tracelessness of odd powers (Eq. 48);
7. symplecticity of $\exp(H\tau)$ and $S(\tau) = M(\tau)S(0)M(-\tau)$ (Eqs. 50–51);
8. the dimension counts $n(2n+1)$ and $n(2n-1)$ (Eqs. 55–56) and the (anti-)commutator table (Eq. 57);
9. the matrix Euler formulas for the real Pauli matrices (Eq. 66).

Significance

The result itself. Each statement is classical linear algebra or linear ODE theory; the paper uses them to argue that Heisenberg's equation and the spectral description of observables arise from second moments of a classical Hamiltonian ensemble. A checked version separates what is a theorem from what is interpretation, and pins down the hypotheses (for example, that only symmetry of $A$ is needed for Eq. 48, not positive definiteness).

Formalizing it. None of these statements is new mathematics; the work is to formalize them in the paper's notation ($\gamma_0 = \mathbf 1_n\otimes\eta_0$, entrywise matrix derivatives, the matrix exponential) so that they can be reused for later parts of the paper, such as the real Dirac algebra of Sec. VII–VIII.

Difficulty

Most milestones are short calculations. The two steps needing real infrastructure are (i) the uniqueness of solutions of the linear matrix ODE $\dot S = [H,S]$, needed to identify $S(\tau)$ with $\exp(H\tau)S(0)\exp(-H\tau)$, and (ii) the dimension counts, which require an explicit basis or an isomorphism with symmetric/skew-symmetric matrices. Going through the Lax invariants alone gives only the traces of powers of $S$, and recovering the characteristic polynomial from them needs Newton's identities; the similarity form of Eq. (51) gives the conservation of the characteristic polynomial directly.

Formalization scope

Everything is over $\mathbb R$. Matrices are indexed by pairs $(i,b)$, $i<n$, $b\in\{0,1\}$, so that $\gamma_0$ is literally a Kronecker product; $n = 0$ is allowed. Time derivatives of matrix-valued functions are entrywise HasDerivAt; $\exp$ is Mathlib's power-series NormedSpace.exp. A Hamiltonian matrix is $\gamma_0A$ with $A$ symmetric (no definiteness); $\Sigma$ is any symmetric solution of Eq. (40) — positivity is not assumed because it is not used. Eigenvalues of real skew-symmetric matrices are taken over $\mathbb C$. "Number of linearly independent elements" is the dimension of the real span. No statement is vacuous: all hypotheses are satisfied, for example, by $H = \gamma_0$ and $\Sigma \equiv \mathbf 1$.

All statements share the definition file UnQM_phase_space and the namespace UnQuantumMechanics.

Selected references

• C. Baumgarten, How to (Un-) Quantum Mechanics, arXiv:1810.06981v2 [physics.gen-ph], 2025. https://arxiv.org/abs/1810.06981
• P. D. Lax, Integrals of nonlinear equations of evolution and solitary waves, Comm. Pure Appl. Math. 21 (1968), 467–490. https://doi.org/10.1002/cpa.3160210503

Motivation

The virial theorem relates the long-time average of the total kinetic energy of a bound system of particles to the average of the virial $-\frac12\sum_k \mathbf F_k\cdot\mathbf r_k$ of the forces acting on them. It gives the average kinetic energy of systems too complicated to solve exactly, such as stars, planetary systems, galaxies and galaxy clusters. Fritz Zwicky used it to infer the existence of unseen matter, and it enters the derivation of the Chandrasekhar limit for white dwarfs. It does not depend on the notion of temperature and holds for systems that are not in thermal equilibrium.

Timeline (as recounted in the source article):

• 1772: Lagrange's identity appears in Lagrange's Essay on the Problem of Three Bodies.
• Jacobi generalizes the identity to $n$ bodies.
• 1870: Clausius, lecture On a Mechanical Theorem Applicable to Heat: the mean vis viva of a system equals its virial.
• Later development by Maxwell, Rayleigh, Poincaré, Chandrasekhar, Fermi, Ledoux, Bader and Parker; quantum versions sketched in 1926 and proved by Finkelstein (1928) and Fock (1930).

Setting

$N$ point particles move in $\mathbb R^3$. Particle $k$ has a constant mass $m_k$, position $r_k(t)$, velocity $v_k(t)=\dot r_k(t)$ and momentum $p_k=m_kv_k$; the net force on it is $F_k=\dot p_k$. The kinetic energy is $T=\frac12\sum_km_k\|v_k\|^2$, the moment of inertia is $I=\sum_km_k\|r_k\|^2$, and

$$G=\sum_{k=1}^Np_k\cdot r_k .$$

The time average over a duration $\tau$ is $\langle f\rangle_\tau=\frac1\tau\int_0^\tau f(t)\,dt$.

When forces come from pair potentials $V_{jk}$ depending only on the distance $r_{jk}=\|r_k-r_j\|$, the force of $j$ on $k$ is $F_{jk}=-\nabla_{r_k}V_{jk}(r_{jk})$, $F_k=\sum_jF_{jk}$, and the total potential energy is $V_{\mathrm{TOT}}=\sum_k\sum_{j<k}V_{jk}(r_{jk})$. Power-law potentials are $V_{jk}=\alpha_{jk}r_{jk}^n$; gravity is $n=-1$.

Formalization targets

Goal: the virial theorem

For a motion with $\dot r_k=v_k$, $\dot p_k=F_k$ (continuous forces) that is bounded (positions and velocities bounded for $t\ge0$),

$$\lim_{\tau\to\infty}\Big(2\langle T\rangle_\tau+\sum_{k=1}^N\langle F_k\cdot r_k\rangle_\tau\Big)=0 .$$

Milestones

1. $\frac12\,\dot I=G$.
2. $\dot G=2T+\sum_kF_k\cdot r_k$.
3. With Newton's third law, $\sum_kF_k\cdot r_k=\sum_k\sum_{j<k}F_{jk}\cdot(r_k-r_j)$.
4. Potential pair forces are central: $F_{jk}=-\frac{V_{jk}'(r_{jk})}{r_{jk}}(r_k-r_j)$.
5. Potential pair forces satisfy $F_{jk}=-F_{kj}$.
6. $\sum_kF_k\cdot r_k=-\sum_k\sum_{j<k}V'_{jk}(r_{jk})\,r_{jk}$.
7. Power law: $\sum_kF_k\cdot r_k=-nV_{\mathrm{TOT}}$.
8. Power law: $\dot G=2T-nV_{\mathrm{TOT}}$.
9. Lagrange's identity ($n=-1$): $\frac12\ddot I=2T+V_{\mathrm{TOT}}$.
10. $\langle\dot G\rangle_\tau=\frac{G(\tau)-G(0)}{\tau}=2\langle T\rangle_\tau+\sum_k\langle F_k\cdot r_k\rangle_\tau$.
11. Bounded motion: $\langle\dot G\rangle_\tau\to0$.
12. Power-law virial theorem: $\langle T\rangle_\tau-\frac n2\langle V_{\mathrm{TOT}}\rangle_\tau\to0$ for bounded collision-free motion.

Significance

The theorem turns boundedness of a motion into a quantitative relation between averaged energies, without solving the equations of motion; with $n=-1$ it gives $\langle T\rangle=-\frac12\langle V_{\mathrm{TOT}}\rangle$ for self-gravitating systems, the relation used for mass estimates of galaxy clusters. The result is classical and proved in the literature. This mission formalizes the standard derivation: the calculus identities for $I$ and $G$, the pair-force algebra under Newton's third law, the gradient computation for distance potentials, and the averaging argument.

Difficulty

The mathematics is elementary; the work lies in the formal infrastructure: product rules for inner products of vector-valued trajectories, the gradient of $y\mapsto V(\|y-x\|)$ in $\mathbb R^3$, re-indexing a double sum over ordered pairs into a sum over $j<k$, and the fundamental theorem of calculus for $\int_0^\tau\dot G$ with the required integrability. A tempting oversimplification is to assume that $\langle T\rangle_\tau$ and $\langle F\cdot r\rangle_\tau$ converge individually; bounded motion does not guarantee this, so the targets are stated as limits of the combined expression.

Formalization scope

Space is EuclideanSpace ℝ (Fin 3) and particles are indexed by Fin N. Trajectories are functions $\mathbb R\to\mathbb R^3$; the equations of motion are hypotheses HasDerivAt (r k) (v k t) t and HasDerivAt (fun s => m k • v k s) (F k t) t. Masses are constant real numbers. Time averages are $\tau^{-1}\int_0^\tau$ (interval integral). Pair forces are defined with Mathlib's gradient, with $F_{kk}=0$. Power-law coefficients $\alpha_{jk}$ may depend on the pair (symmetric), which contains the article's single constant $\alpha$. Real powers are Real.rpow; collision-freeness is assumed wherever pair distances enter. Boundedness is imposed only for $t\ge0$. The hypotheses are satisfiable (for instance by a uniform circular two-body motion), so no target holds vacuously.

Selected references

• Wikipedia, Virial theorem. https://en.wikipedia.org/wiki/Virial_theorem
• R. Clausius, On a mechanical theorem applicable to heat, Philosophical Magazine, Series 4, 40 (1870), 122–127.