All missions

Motivation

A coupling constant is the number that fixes the strength of an interaction: in the modern formulation it is the parameter weighting the interaction part of a Lagrangian against its kinetic part. In a quantum field theory such a parameter is not constant. Probing a process at a higher energy resolves more of the virtual activity that dresses the interaction, and the value one measures depends on the energy scale $\mu$ at which the measurement is made. This scale dependence is called the running of the coupling, and it is the organising phenomenon behind two of the best-known qualitative facts about the Standard Model: the electromagnetic coupling grows with energy ($\alpha \approx 1/137$ at low energy, $\alpha \approx 1/127$ at the $Z$ mass, about 90 GeV) and apparently diverges at a finite energy — the Landau pole — while the strong coupling decreases logarithmically at high energy, the asymptotic freedom found by Gross, Politzer and Wilczek and recognised by the 2004 Nobel Prize.

The source treats the running through the beta function, defined there by

$$\beta(g) \;=\; \mu\,\frac{\partial g}{\partial \mu} \;=\; \frac{\partial g}{\partial \ln \mu},$$

and through the one-loop strong coupling

$$\alpha_s(k^2) \;\approx\; \frac{1}{\beta_0 \ln(k^2/\Lambda^2)} .$$

Everything in this mission is the mathematics of those two formulas: an autonomous scalar ordinary differential equation in the logarithm of the energy, and the behaviour of its solutions according to the sign of the one-loop coefficient.

Setting

Write $\mu > 0$ for the energy scale of a process and $g$, or $\alpha$, for a real-valued coupling as a function of that scale. The beta function in the energy scale is the logarithmic derivative used by the source,

$$\beta(g)(\mu) \;=\; \mu \cdot \frac{d g}{d \mu}(\mu),$$

a function of $\mu$ built from $g$; a theory whose beta function vanishes identically is scale-invariant, since its coupling then takes the same value at every scale.

A coupling is said to be one-loop running with coefficient $b$ on a set $S$ of scales when it satisfies, at every $\mu \in S$,

$$\mu \, \frac{d\alpha}{d\mu}(\mu) \;=\; b \, \alpha(\mu)^2 ,$$

equivalently $d\alpha/d\mu = b\,\alpha^2/\mu$. Here $b < 0$ is the asymptotically free sign (QCD) and $b > 0$ the sign the source attributes to QED. The equation is the one-loop truncation written in $\mu$ rather than in $t = \ln \mu$: both forms appear in the source, and the first milestone is precisely their agreement.

The one-loop strong coupling with one-loop coefficient $\beta_0 > 0$ and QCD scale $\Lambda > 0$ is the explicit function

$$\alpha(Q) \;=\; \frac{1}{\beta_0 \ln(Q^2/\Lambda^2)}, \qquad Q > \Lambda ,$$

the formula the source quotes for $\alpha_s(k^2)$. It is defined by an existing platform definition, which this mission reuses rather than restates.

Formalization targets

Goal — the running dichotomy in the energy scale

For every reference scale $\mu_0 > 0$ and every positive reference value $\alpha_0$ of the coupling at that scale:

$$b<0:\quad \alpha(\mu) \;=\; \frac{\alpha_0}{1 - b\,\alpha_0 \ln(\mu/\mu_0)} \ \ (\mu \ge \mu_0), \qquad \alpha(\mu) \xrightarrow[\mu \to \infty]{} 0 ;$$ $$b>0:\quad \text{no coupling obeys } \mu\,\frac{d\alpha}{d\mu} = b\,\alpha^2 \text{ on all of } \Big[\mu_0,\ \mu_0 e^{1/(b\alpha_0)}\Big] \text{ with } \alpha(\mu_0)=\alpha_0 .$$

The negative-coefficient half is asymptotic freedom together with the uniqueness of the solution; the positive-coefficient half is the Landau pole, stated as the non-existence of any solution up to the pole scale rather than as a divergence of one chosen formula. The pole scale $\mu_0 e^{1/(b\alpha_0)}$ is the one the one-loop equation itself predicts.

Supporting levels

The milestones below range from the definitional identity $\mu\,\partial_\mu g = \partial_{\ln \mu} g$, through the three qualitative readings of the sign of $\beta$ that the source states in words (vanishing beta function means scale invariance; positive beta function means the coupling grows with energy; negative means it falls), to the identification of the quoted QCD formula as an exact solution of the one-loop equation and the determination of $\Lambda$ from a single measured value.

Significance

The dichotomy is the mathematical content of two physical statements that the source presents side by side. Asymptotic freedom is what makes perturbative QCD predictive at high energy; the Landau pole is the reason the source warns that the perturbative beta function cannot be trusted at strong coupling, since the one-loop equation has no solution reaching the pole scale at all. Formalizing the uniqueness half also pins down what "the" running coupling means: the explicit formula is not merely one solution of the renormalization-group equation but the only one through a given data point.

An earlier public mission on the same source ("Coupling Constant: One-Loop Running, Asymptotic Freedom and the Landau Pole") formalized the one-loop flow in the logarithmic variable $t = \ln\mu$ with a cubic beta function $\beta(g) = b\,g^3$, and its statements are proved. This mission is stated in the other variable the source uses — the energy scale $\mu$ itself, with the quadratic one-loop equation for $\alpha$ — and adds the parts of the source that the earlier mission does not cover: the defining identity between the two forms of the beta function, the sign-to-monotonicity statements for an arbitrary (not necessarily one-loop) coupling, the explicit pole scale, and the determination of the QCD scale $\Lambda$ from a measurement. Where the earlier mission already settles a statement in the quoted formula's variables, this proposal references the published theorem instead of restating it.

Difficulty

The equation is elementary, and the difficulty is entirely in what the statements quantify over. The negative-coefficient half asserts that every function satisfying the equation on $[\mu_0,\infty)$ is the explicit one, so it needs a uniqueness argument for a nonlinear scalar ordinary differential equation rather than a verification that a formula works; the substitution $u = 1/\alpha$ that makes the equation linear is legitimate only while $\alpha$ is known not to vanish, which is part of what has to be proved. The positive-coefficient half is a non-existence statement on a closed interval reaching the pole, so no local solution can be extended to it; the naive attempt — differentiate the explicit formula and observe that it blows up — proves nothing about the other candidate solutions.

Formalization scope

Couplings are total functions $\mathbb{R} \to \mathbb{R}$, and every statement restricts to the scales it is about: the positive half-line for the beta-function statements, $(\Lambda,\infty)$ for the explicit QCD formula, $[\mu_0,\infty)$ or a closed interval for the one-loop flow. Outside those ranges nothing is claimed — in particular at $Q \le \Lambda$, where the logarithm in the quoted formula vanishes or is negative and the reciprocal returns a junk value. Differentiability is a hypothesis where it is needed, written as a two-sided derivative at each scale of the set, so that a statement cannot be satisfied by a one-sided artefact at an endpoint. The one-loop property is phrased as an exact differential equation, never as an asymptotic approximation, and the Landau-pole milestone is a non-existence claim rather than a divergence claim, so it cannot be discharged by exhibiting a formula with a singularity.

A complete development needs the mean value theorem, Gronwall- or uniqueness-type arguments for scalar ordinary differential equations, and the standard logarithm and exponential API; the uniqueness lemma for $\dot u = b u^2$ and the reciprocal substitution are reusable beyond this mission. Contributions of a general scalar-ODE uniqueness lemma, usable by both this mission and the earlier one, are especially welcome.

Selected references

• Wikipedia, Coupling constant, revision 1354339557. https://en.wikipedia.org/w/index.php?title=Coupling_constant&oldid=1354339557
• A. Deur, S. J. Brodsky, G. F. de Téramond, The QCD running coupling, Progress in Particle and Nuclear Physics 90 (2016) 1-74. https://arxiv.org/abs/1604.08082
• ATLAS Collaboration, A precise determination of the strong-coupling constant from the recoil of Z bosons with the ATLAS experiment at $\sqrt{s} = 8$ TeV, 2023. https://arxiv.org/abs/2309.12986
• P. A. Zyla et al. (Particle Data Group), Review of Particle Physics - Chapter 9, Quantum Chromodynamics, PTEP 2020 (8). https://doi.org/10.1093/ptep/ptaa104

Motivation

The Polyakov action is the standard action for the worldsheet of a bosonic string. It was introduced by Deser and Zumino and independently by Brink, Di Vecchia and Howe in 1976, and is associated with Polyakov after he used it to quantize the string in 1981. Its value over the Nambu–Goto (area) action is that it is quadratic in the embedding fields, which makes quantization tractable, while being classically equivalent to the area action. This mission formalizes the classical facts collected in the Wikipedia article Polyakov action.

Setting

A string sweeps out a two-dimensional worldsheet with coordinates $\sigma=(\tau,\sigma)$. Its embedding in a $D$-dimensional target is $X^\mu(\sigma)$; the target carries a metric $g_{\mu\nu}(X)$, and the worldsheet carries an independent (auxiliary) metric $h_{ab}(\sigma)$ with inverse $h^{ab}$ and determinant $h$. With the induced metric $G_{ab}=g_{\mu\nu}(X)\partial_aX^\mu\partial_bX^\nu$ and string tension $T$, the Polyakov and Nambu–Goto actions are

$$S_P=\frac T2\int d^2\sigma\,\sqrt{-h}\,h^{ab}G_{ab},\qquad S_{NG}=T\int d^2\sigma\,\sqrt{-\det G_{ab}} .$$

The stress–energy tensor is $T_{ab}=T\big(G_{ab}-\tfrac12h_{ab}h^{cd}G_{cd}\big)$. Signature convention: timelike $+$, spacelike $-$.

Formalization targets

Goal: on-shell equivalence with Nambu–Goto

If the auxiliary metric satisfies its equation of motion $T_{ab}=0$ (with $h^{cd}G_{cd}\ge0$), then

$$S_P=S_{NG}.$$

Milestones

1. Poincaré invariance of the target: translations $X\to X+b$ (exact) and infinitesimal Lorentz transformations $X\to X+\varepsilon\,\omega X$ (to $O(\varepsilon^2)$), for a constant target metric.
2. Worldsheet diffeomorphism invariance and Weyl invariance $h\to\Lambda h$.
3. Tracelessness of the stress–energy tensor, $T^a{}_a=0$.
4. The variations $\delta\sqrt{-h}=-\frac12\sqrt{-h}h_{ab}\delta h^{ab}$ and $\delta S/\delta h^{ab}=\frac T2\sqrt{-h}\,(G_{ab}-\frac12h_{ab}h^{cd}G_{cd})$.
5. On shell, $\det G=\frac14h\,(h^{cd}G_{cd})^2$.
6. Conformal gauge: $S=\frac T2\int(\dot X^2-X'^2)$, the constraints $\dot X\cdot X'=0$, $\dot X^2+X'^2=0$, the wave equation $\Box X^\mu=0$, and its light-cone solution $X=X_+(\tau+\sigma)+X_-(\tau-\sigma)$.

Significance

These are the classical foundations of bosonic string theory: the symmetries (Poincaré, diffeomorphism, Weyl) are what make the conformal gauge reachable, and the equivalence with Nambu–Goto justifies using the quadratic action. All statements are textbook results; the work here is to formalize them with explicit hypotheses (differentiability, integrability, positivity of $h^{cd}G_{cd}$) that the physics presentation leaves implicit.

Difficulty

The algebraic statements are $2\times2$ matrix identities. The diffeomorphism invariance needs the change-of-variables formula; the infinitesimal Lorentz statement needs care with integrability; the wave-equation milestone needs the fundamental lemma of the calculus of variations; and the light-cone solution is d'Alembert's theorem.

Formalization scope

Worldsheet $=\mathbb R^2$ (coordinates Fin 2 → ℝ, index $0=\tau$), target $=\mathbb R^D$. Actions are Bochner integrals over a region $U\subseteq\mathbb R^2$. The inverse metric is Mathlib's matrix inverse. Quantization, Virasoro operators, the Liouville action and string boundary conditions are out of scope.

Selected references

• Wikipedia, Polyakov action, revision 1292212311.
• S. Deser, B. Zumino, A complete action for the spinning string, Phys. Lett. B 65 (1976) 369–373.
• L. Brink, P. Di Vecchia, P. Howe, A locally supersymmetric and reparametrization invariant action for the spinning string, Phys. Lett. B 65 (1976) 471–474.
• A. M. Polyakov, Quantum geometry of bosonic strings, Phys. Lett. B 103 (1981) 207–210.

Motivation

Whether the many-worlds (Everett) interpretation of quantum mechanics is local in the sense of Bell is a recurring question in the foundations of physics. A number of authors have argued that Everett's theory escapes Bell-type nonlocality theorems because it drops the assumption that each measurement has a single outcome. A. Drezet's paper arXiv:2306.07794 (2023) argues against this claim by revisiting the Greenberger–Horne–Zeilinger (GHZ) nonlocality theorem, which, unlike Bell's inequality, uses only probability-one (perfect) correlations. Its central mathematical step, stated in Section II, is that no locally causal beable model can reproduce the quantum predictions for the GHZ state. The paper's argument is that this step makes no assumption about completeness or hidden variables, and so applies to Everett's theory as well.

Timeline:

• 1964–1976: J. S. Bell introduces Bell inequalities and, in "The theory of local beables" (1976), the notion of local causality phrased with beables $\lambda$ (collected in Speakable and Unspeakable in Quantum Mechanics, 2004).
• 1989: Greenberger, Horne and Zeilinger give a nonlocality proof for three spin-½ particles that uses no inequality ("Going beyond Bell's theorem").
• 2015: L. Vaidman discusses the GHZ argument in the many-worlds setting ("Bell inequality and Many-Worlds interpretation").
• 2023: Drezet's paper, the source of this mission.

Setting

Three spin-½ particles are sent to three distant observers, Alice, Bob and Charlie. Each one measures the spin of their particle along a direction $\hat n_j \in \{\hat x, \hat y\}$ and records an outcome $\alpha, \beta, \gamma \in \{+1, -1\}$. The particles are prepared in the GHZ state

$$|\psi\rangle = \tfrac{1}{\sqrt 2}\big(|{+z}\rangle_1|{+z}\rangle_2|{+z}\rangle_3 - |{-z}\rangle_1|{-z}\rangle_2|{-z}\rangle_3\big),$$

and quantum mechanics predicts the joint outcome probabilities through the Born rule, $P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3,\psi) = |\langle \alpha_{\hat n_1},\beta_{\hat n_2},\gamma_{\hat n_3}|\psi\rangle|^2$. Here $|a_{\hat n}\rangle$ denotes the eigenvector of $\sigma_{\hat n}$ with eigenvalue $a$. In Lean this is bornProb n₁ n₂ n₃ α β γ.

A locally causal (Bell-local) model consists of

• a space $\Lambda$ of beables with a probability distribution $\rho(\lambda)$ that does not depend on the settings (Eq. (18), statistical independence), and
• local response probabilities $P_j(\alpha\mid\lambda,\hat n_j)$, where party $j$'s outcome depends only on $\lambda$ and its own setting (Eq. (17)).

Such a model predicts

$$P(\alpha,\beta,\gamma\mid\hat n_1,\hat n_2,\hat n_3) = \int_\Lambda P_1(\alpha\mid\lambda,\hat n_1)\,P_2(\beta\mid\lambda,\hat n_2)\,P_3(\gamma\mid\lambda,\hat n_3)\,d\rho(\lambda).$$

In Lean the model is a LocalCausalModel Λ and its prediction is M.predict. The beables are arbitrary: $\lambda$ may be a hidden variable, or the quantum state itself as in the Beltrametti–Bugajski representation, Eq. (15).

Formalization targets

Goal (Section II, Eqs. (10)–(27))

No locally causal model reproduces the quantum predictions on the four GHZ settings $(\hat x,\hat x,\hat x)$, $(\hat x,\hat y,\hat y)$, $(\hat y,\hat x,\hat y)$, $(\hat y,\hat y,\hat x)$:

$$\neg\Big(\forall\,\text{GHZ settings } \hat n,\ \forall \alpha,\beta,\gamma:\ P^{\mathrm{model}}(\alpha,\beta,\gamma\mid\hat n) = P^{\mathrm{Born}}(\alpha,\beta,\gamma\mid\hat n,\psi)\Big).$$

Milestones

1. Eqs. (2)–(5). $\sigma_x^{(1)}\sigma_x^{(2)}\sigma_x^{(3)}|\psi\rangle = -|\psi\rangle$, and the three $\sigma_x\sigma_y\sigma_y$-type operators fix $|\psi\rangle$.
2. Born probabilities (Section III, Eqs. (30)–(32)). For $(\hat x,\hat x,\hat x)$ each outcome triple has probability $1/4$ if $\alpha\beta\gamma=-1$ and $0$ otherwise. For the other three GHZ settings the same holds with $\alpha\beta\gamma=+1$.
3. Eqs. (10)–(13). No assignment $A_j, B_j \in\{\pm1\}$ satisfies all four GHZ constraints.
4. Eqs. (19)–(27). If a product of three probability distributions on $\{\pm1\}$ vanishes off the set $\{\alpha\beta\gamma = s\}$, then each factor is a point mass, and the three atoms multiply to $s$.
5. Section II, summary (ii). A locally causal model that reproduces the GHZ predictions is, for $\rho$-almost every $\lambda$, deterministic, with values satisfying (10)–(13).
6. Section III (B). Local causality implies non-signalling.
7. Eq. (29). Quantum non-signalling for the GHZ state, with Alice's marginal $P_1(\pm1\mid\hat x,\psi)=\tfrac12$.
8. Appendix 3, Eqs. (39)–(45). Keeping Eq. (17) but letting the beable density depend on the settings (a "superdeterministic" model) does reproduce the GHZ predictions.

Significance

The goal theorem is the mathematical core of the paper's conclusion that any beable account of the GHZ correlations, including one where $\lambda$ is just the quantum state, violates Bell's local causality. Milestones 6–8 formalize the paper's separation of notions of locality: non-signalling holds both in quantum mechanics and in every locally causal model, so it cannot tell them apart; and dropping statistical independence (Eq. (18)) is enough to reproduce the correlations. The GHZ theorem itself has been known since 1989. As far as the drafter is aware it has no machine-checked formalization on this platform, and this mission provides one, stated for general measurable beable spaces.

Difficulty

The combinatorial core (milestone 3) is a parity argument. The substance lies in the steps that connect it to probability: showing that perfect correlations force determinism almost surely when $\rho$ is an arbitrary probability measure (null sets, measurability, integrals of nonnegative functions), and computing the Born probabilities exactly in Lean from explicit matrices and eigenvectors.

Formalization scope

• Outcomes are elements of ℤˣ (exactly $\{+1,-1\}$). Settings form a two-element type Setting with values x and y. Qubit index 0 is $|{+z}\rangle$ and index 1 is $|{-z}\rangle$. Three-qubit operators are Kronecker products.
• A LocalCausalModel Λ has a probability measure ρ on a measurable space Λ and measurable response functions P j λ n α with values in $[0,1]$ that sum to one over $\alpha$. The fixed state $\psi$ is left implicit. Predictions are Bochner integrals, and all integrands are bounded and measurable.
• The goal quantifies over all such models on all measurable spaces. Its hypothesis is the equality of all $4\times 8$ predicted and Born probabilities. Because it uses the actual Born probabilities rather than an arbitrary list of constraints, it cannot hold vacuously.
• Needed infrastructure: finite-dimensional matrix computations over $\mathbb C$ with $\sqrt2$, and basic measure theory (a.e. vanishing of nonnegative integrands).

Selected references

• A. Drezet, An Elementary Proof That Everett's Quantum Multiverse Is Nonlocal: Bell-Locality and Branch-Symmetry in the Many-Worlds Interpretation, arXiv:2306.07794, 2023. https://arxiv.org/abs/2306.07794
• D. M. Greenberger, M. A. Horne, A. Zeilinger, Going beyond Bell's theorem, in Bell's Theorem, Quantum Theory and Conceptions of the Universe, Kluwer, 1989, pp. 69–72. https://arxiv.org/abs/0712.0921
• J. S. Bell, Speakable and Unspeakable in Quantum Mechanics, 2nd ed., Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511815676

Motivation

In emergent gravity proposals, spacetime and gravity are macroscopic descriptions of an underlying quantum system. In Verlinde (2016) it is argued that in de Sitter space (a universe with positive dark energy) the entanglement entropy has, besides the usual area-law part, a thermal volume-law part, and that matter displaces this volume-law entropy. The elastic response of the medium to this displacement produces an extra gravitational pull, which the paper proposes as the origin of the effects usually ascribed to dark matter in galaxies and clusters.

The physical derivation is heuristic, but it ends in explicit mathematical relations between the baryonic (visible) mass profile $M_B(r)$ and the apparent dark matter mass profile $M_D(r)$ of a spherically symmetric, isolated system. The central one is the integral relation (7.40),

$$\int_0^r \frac{G\,M_D(r')^2}{r'^2}\,dr' = \frac{M_B(r)\,a_0\,r}{6},$$

where $G$ is Newton's constant and $a_0 = cH_0$ is the Hubble acceleration scale. For a point mass it reproduces Milgrom's empirical acceleration relation and the baryonic Tully-Fisher relation $v_f^4 = a_M G M_B$ with $a_M = a_0/6$.

Setting

All quantities are real numbers or real functions of the radius $r>0$. $G>0$ and $a_0>0$ are constants. $M_B(r)$ and $M_D(r)$ are the baryonic and apparent dark masses inside radius $r$. The Newtonian accelerations are $g_B(r) = GM_B(r)/r^2$ and $g_D(r) = GM_D(r)/r^2$ (7.42). The averaged density inside radius $r$ is $\bar\rho(r) = 3M(r)/(4\pi r^3)$ (7.45), and the slope parameter is $\beta(r) = -\,d\log\bar\rho/d\log r = -r\bar\rho'(r)/\bar\rho(r)$ (7.46). A local density $\rho$ gives $M(r) = \int_0^r \rho(r')\,4\pi r'^2\,dr'$ (7.39).

The paper also uses two purely mathematical facts about elastic strain in $d-1$ spatial dimensions: a bound (7.30) on the largest principal strain of a traceless symmetric strain tensor, and the integration-by-parts identity (7.31) between the squared Hessian and the squared Laplacian.

Formalization targets

Goal: Milgrom relation for a central point mass (7.43)

If $M_B>0$ is constant and (7.40) holds for every $r>0$, then for every $r>0$

$$g_D(r) = \sqrt{a_M\, g_B(r)}, \qquad a_M = \frac{a_0}{6}.$$

Milestones

• (4.44) the strain-squared integral outside a spherical inclusion: $\int_{c}^{\infty} (c/V)^2\,dV = c$.
• (7.30) $\varepsilon^2 \le \frac{d-2}{d-1}\sum_{ij}\varepsilon'^2_{ij}$ for a traceless symmetric $\varepsilon'$ with eigenvalue $\varepsilon$.
• (7.31) $\int (\nabla_i\nabla_j\chi)^2\,dV = \int (\nabla^2\chi)^2\,dV$.
• (7.47) $\bar\rho_D(r)^2 = (4-\beta_B(r))\,\frac{a_0\,\bar\rho_B(r)}{8\pi G r}$ for a general baryonic profile.
• (7.48) $\rho_D(r) = (1-\tfrac13\beta_D(r))\,\bar\rho_D(r)$.
• (7.51) $\Omega_D^2 = \tfrac43\,\Omega_B$ when (7.47) is applied at the Hubble radius with $\beta_B = 0$.

Significance

The point-mass relation (7.43) is what connects the paper to the observed flat rotation curves and the baryonic Tully-Fisher law; (7.47) is its extension to extended mass profiles, which the paper uses to discuss galaxy clusters. The formal content checked here is the mathematics that turns the stated relation (7.40) into these observable consequences, plus the two elasticity lemmas used on the way to (7.40). The physical steps that lead to (7.40) (the entropy-displacement picture, the elastic interpretation, the identification (7.35)) are not mathematical statements and are outside the scope of this mission. None of these relations is known to have been machine-checked before.

Difficulty

The algebra is short once one may differentiate; the work is in the analysis. (7.40) is an integral identity with a singular weight $1/r'^2$ at the origin, so recovering pointwise information requires the fundamental theorem of calculus on $(0,\infty)$ with only continuity there, and care with integrability at $0$. (7.31) is a double integration by parts in $\mathbb R^n$ that must be justified for the chosen decay class. (7.30) needs the spectral theorem for symmetric matrices, or an equivalent argument.

Formalization scope

All statements live in the namespace Verlinde2016. Radial profiles are functions $\mathbb R\to\mathbb R$, with hypotheses only on $(0,\infty)$. The integral in (7.40) is Lean's interval integral over $[0,r]$; since it would be $0$ for a non-integrable integrand, the positivity of the right-hand side forces integrability. Continuity of $M_D$ (and of densities) on $(0,\infty)$ is taken as a standing physical convention. In (7.31) the paper's condition that "$\chi$ falls off rapidly enough" is formalized as $\chi$ smooth with compact support. Spatial dimension is $d-1$ in (7.30); (7.40)–(7.51) use $d=4$ as in Section 7.2. Definitions: avgDensity, slopeParam, partialDeriv.

Selected references

• E. Verlinde, Emergent Gravity and the Dark Universe, SciPost Phys. 2, 016 (2017). https://arxiv.org/abs/1611.02269
• M. Milgrom, A modification of the Newtonian dynamics as a possible alternative to the hidden mass hypothesis, Astrophys. J. 270 (1983) 365. https://doi.org/10.1086/161130

Motivation

Liouville field theory is a two-dimensional conformal field theory whose classical equation of motion generalizes Liouville's equation. It is one of the few interacting conformal field theories with a continuous spectrum that has been solved: its three-point function on the sphere is given by the DOZZ formula (Dorn–Otto 1994; Zamolodchikov–Zamolodchikov 1996), proved rigorously from a probabilistic construction of the path integral by Kupiainen–Rhodes–Vargas (2017), with the conformal bootstrap established by Guillarmou–Kupiainen–Rhodes–Vargas (2020). It appears in two-dimensional quantum gravity, non-critical string theory, and log-correlated random energy models.

This mission is the first in a series following the Wikipedia article on Liouville field theory. It formalizes the kinematic layer of the theory: the algebraic relations between the coupling constant, the background charge, the central charge, the conformal dimensions and the reflection coefficient, on which every later statement (the spectrum, the DOZZ formula, the bootstrap) is phrased.

Setting

Fix a complex number $b$, the coupling constant. Define

• the background charge $Q = b + \dfrac1b$;
• the central charge $c = 1 + 6Q^2$;
• the conformal dimension of the primary field with momentum $\alpha \in \mathbb C$, $\ \Delta(\alpha) = \alpha(Q - \alpha)$;
• the reflection coefficient with normalization parameter $\lambda$,

$$R_P = \pm\,\lambda^{-2iP}\,\frac{\Gamma(2ibP)\,\Gamma(2ib^{-1}P)}{\Gamma(-2ibP)\,\Gamma(-2ib^{-1}P)},$$

with sign $+1$ if $c \in (-\infty,1)$ and $-1$ otherwise.

Two symmetries act on these data: the reflection $\alpha \to Q - \alpha$ and the duality $b \to 1/b$. The spectrum of the theory is the set of dimensions $\Delta \in \frac{c-1}{24} + \mathbb R_+$, parametrized by momenta $\alpha = \frac Q2 + iP$, $P \in \mathbb R_+$.

Formalization targets

Goal: the spectrum parametrization

For every $b \in \mathbb C$, the map $P \mapsto \Delta\left(\frac Q2 + iP\right)$ is a bijection

$$[0,\infty) \;\xrightarrow{\ \sim\ }\; \frac{c-1}{24} + [0,\infty) \subset \mathbb C.$$

Milestones

1. Reflection invariance: $\Delta(Q-\alpha) = \Delta(\alpha)$.
2. Duality: $c$ and $\Delta$ are invariant under $b \to 1/b$.
3. Marginality: for $b \ne 0$, $b(Q - b) = 1 \iff Q = b + 1/b$.
4. Dimension in terms of momentum: $\Delta\left(\frac Q2 + iP\right) = \frac{c-1}{24} + P^2$.
5. Imaginary coupling: real nonzero $\beta = ib$ produce exactly the real central charges $c \le 1$.
6. Reflection relation consistency: $R_P R_{-P} = 1$ for $\lambda \ne 0$ and $2ibP, 2ib^{-1}P \notin \mathbb Z$.

Significance

These identities are the dictionary between the parameters used in the physics literature ($b$, $Q$, $c$, $\alpha$, $P$, $\Delta$) and fix the conventions for later missions in the series: the DOZZ formula, the pole structure of correlation functions, and the reflection and duality covariance of structure constants are all stated in these variables. None of these statements is open; the value of the mission is a vetted, reusable definition layer with machine-checked consistency of the conventions.

Difficulty

The individual statements are elementary algebra over $\mathbb C$, together with the non-vanishing of the Gamma function away from its poles. The care needed is in conventions: total functions in Lean ($0^{-1} = 0$, principal-branch complex powers, Gamma at its poles) must be handled by explicit hypotheses exactly where the source implicitly excludes degenerate values.

Formalization scope

All quantities are complex-valued functions of $b \in \mathbb C$, defined in the namespace LiouvilleFieldTheory. $1/b$ is Lean's inverse (so $b = 0$ gives junk values $Q = 0$, $c = 1$; statements that need $b \ne 0$ assume it). $\mathbb R_+$ is taken to be $[0,\infty)$. The condition $c \in (-\infty,1)$ is encoded as $\operatorname{Im} c = 0 \wedge \operatorname{Re} c < 1$. $\lambda^{-2iP}$ is the principal-branch complex power. The analytic content of the article (Virasoro representations, conformal blocks, the special function $\Upsilon_b$, the path integral, the DOZZ formula) is out of scope for this mission.

Selected references

• Wikipedia, Liouville field theory, revision 1376996606. https://en.wikipedia.org/w/index.php?title=Liouville_field_theory&oldid=1376996606
• S. Ribault, Conformal field theory on the plane, 2014. https://arxiv.org/abs/1406.4290
• H. Dorn, H.-J. Otto, Two and three point functions in Liouville theory, Nucl. Phys. B 429 (1994). https://arxiv.org/abs/hep-th/9403141
• A. Zamolodchikov, Al. Zamolodchikov, Conformal bootstrap in Liouville field theory, Nucl. Phys. B 477 (1996). https://arxiv.org/abs/hep-th/9506136
• A. Kupiainen, R. Rhodes, V. Vargas, Integrability of Liouville theory: proof of the DOZZ formula, 2017. https://arxiv.org/abs/1707.08785
• C. Guillarmou, A. Kupiainen, R. Rhodes, V. Vargas, Conformal bootstrap in Liouville theory, 2020. https://arxiv.org/abs/2005.11530

Why barycenters of histograms matter

A barycenter summarizes several objects by minimizing a weighted sum of distances to them. For probability histograms, ordinary coordinatewise averages depend strongly on how the bins are labeled. Optimal transport instead lets mass move between bins and charges for those moves through a cost matrix. The resulting Wasserstein barycenter can reflect the geometry of the bins: nearby bins can exchange mass at a lower cost than distant ones. Peyré and Cuturi use this construction in their treatment of variational transport problems, including shape interpolation and the representation of a measure as a barycenter of other measures. The finite histogram problem in this mission is the entropically regularized version developed in §9.2 of their textbook.

The computational question is how to connect three ways of describing the same solution: a histogram that is the barycenter, transport matrices coupling it to the inputs, and vectors of dual potentials. Proposition 9.1 on p. 530 identifies the dual potentials behind the scaling factors of the optimal transport matrices. This is the second proposition numbered 9.1 in the chapter; the one on p. 519 concerns derivatives with respect to histograms.

Finite histogram setting

There are $S$ input histograms. Source $s$ has $n_s$ bins and a probability vector $b_s$, while the barycenter has $n$ bins. The real matrix $C_s\in\mathbb R^{n\times n_s}$ gives the cost of transporting a unit of mass from barycenter bin $i$ to input bin $j$. A weight vector $\lambda\in\Sigma_S$ has nonnegative entries summing to one; $\Sigma_k$ denotes the probability simplex on $k$ bins. The unregularized barycenter problem (9.10) minimizes $\sum_s\lambda_s L_{C_s}(a,b_s)$ over $a\in\Sigma_n$, where $L_{C_s}$ is the minimum transport cost with marginals $a$ and $b_s$.

For a regularization parameter $\varepsilon>0$, the entropic transport cost $L^\varepsilon_{C_s}(a,b_s)$ minimizes $\langle C_s,P_s\rangle-\varepsilon H(P_s)$ over nonnegative coupling matrices $P_s$ with row marginal $a$ and column marginal $b_s$. Here $\langle C_s,P_s\rangle=\sum_{i,j}C_{s,ij}P_{s,ij}$ and $H(P_s)=\sum_{i,j}(-P_{s,ij}\log P_{s,ij}+P_{s,ij})$, with $0\log0=0$. The Gibbs kernel is $K_{s,ij}=e^{-C_{s,ij}/\varepsilon}$.

The book also writes the regularized barycenter as a weighted KL projection. Its variables are the matrices $(P_s)_s$; each matrix has column marginal $b_s$, and every matrix has the same row marginal. That shared row marginal is $a$, so the optimization can be expressed without carrying $a$ as a separate variable. The generalized matrix divergence is $\mathrm{KL}(P_s\mid K_s)=\sum_{i,j}[P_{s,ij}\log(P_{s,ij}/K_{s,ij})-P_{s,ij}+K_{s,ij}]$, using the continuous value at $P_{s,ij}=0$. See (9.15)–(9.17) in Peyré and Cuturi.

Formalization targets

The goal is Proposition 9.1 on p. 530. The dual variables are row potentials $f_s\in\mathbb R^n$ and column potentials $g_s\in\mathbb R^{n_s}$. They maximize

$$\sum_s\lambda_s\left[\langle g_s,b_s\rangle-\varepsilon\sum_{i,j}e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon}\right] \quad\text{subject to}\quad \sum_s\lambda_s f_s=0.$$

The theorem asserts that the primal and dual optima are attained, that every optimal primal family and every optimal dual family satisfy

$$P_{s,ij}=e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon},$$

and that the dual maximum is the minimum value of the entropic barycenter objective (9.15). The milestone targets are the scalar and matrix versions of the KL conjugate (9.22), followed by the closed form maximizer of one $g_s$ block, corresponding to the update (9.18). These statements retain the source's finite matrix setting and are listed in the order in which their concepts enter the dual formulation.

What the result supplies

The scaling formula turns the optimal couplings into a product of a row factor, a fixed positive kernel, and a column factor. It identifies those factors with exponentials of dual potentials and gives a constrained maximization problem whose value is the entropic barycenter cost. Thus a solver can reason about the couplings, the barycenter marginal, or the potentials while referring to one theorem that connects them. The book uses the same variables to describe the iterative scaling updates on pp. 529–531 and later illustrates barycenters of shapes and surface measures; those applications depend on interpreting the matrix factors correctly. Peyré and Cuturi give the mathematical proposition and its argument. A complete Lean proof of the proposition and its supporting KL identities is the work this mission calls for; the statements here are draft targets rather than machine-checked solutions.

Where the difficulty lies

The potential program is a constrained optimization problem, while the transport problem constrains nonnegative matrices by two kinds of marginals. Equality of their optimum values must preserve the normalization constants in generalized KL. The exponential form alone does not establish that a proposed matrix has the required marginals, nor does a feasible matrix alone identify dual potentials. In addition, the assertion concerns every optimizer: a choice of zero source weight would leave that source's coupling unconstrained by the objective, and a zero target entry would put a logarithmic column update on the boundary. These are substantive edge cases of the formulas, not merely notation.

Formalization scope

Lean uses Fin S, Fin n, and Fin (n_s) for the finite index sets; these are zero based versions of the book's one based indices. Histograms and potentials are real vectors, costs and couplings are real matrices, and the Gibbs kernel is defined entrywise. The theorem requires $S,n,n_s>0$, $\varepsilon>0$, strictly positive weights $\lambda_s$ that sum to one, and strictly positive input histograms $b_s$ that each sum to one. The strict positivity of weights and input entries is an explicit restriction beyond (9.15)–(9.21), needed for a statement about every optimizer and finite logarithmic potentials. Entropy uses $0\log0=0$ on nonnegative couplings. The shared row marginal is constructed by the constraints on the $P_s$; it is not a free histogram unrelated to them.

The definition layer includes finite matrix pairing, entropy, generalized KL, the Gibbs kernel, feasibility, and primal and dual objective functions. The KL conjugate identities and the block optimizer are separate theorem targets so they can be reused in other entropic transport developments. The main theorem asserts primal and dual attainment as well as their relationship; it does not assume strong duality or an optimal scaling as an input. The page has slips in the dimensions of the marginal equations and a missing subscript on $K$ in (9.17); the Lean statements use the dimensions specified by $P_s\in\mathbb R^{n\times n_s}$. The optional cost-gradient Proposition 9.2 on pp. 519–520 and the $f_s$ block update (9.19)–(9.20) lie outside this proposal.

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. DOI: 10.1561/2200000073.

Motivation

Optimal transport compares two distributions by finding the least expensive way to move mass between them. For finite histograms, the resulting linear program is precise but its optimal coupling can be sparse. In applications where the coupling represents traffic, matching, or a differentiable loss, a sparse plan may be undesirable or expensive to compute repeatedly. Peyré and Cuturi describe how adding an entropy term selects a diffuse coupling and leads to matrix scaling algorithms that can be used on large finite problems (Peyré and Cuturi, 2019, Chapter 4).

The entropic dual gives a second view of the same regularized problem. Its variables are real vectors attached to the two marginal constraints. Unlike the ordinary Kantorovich dual, the objective has no explicit feasibility constraints and is smooth. This permits calculations in the log domain, which the book introduces because direct scaling with exponentials can suffer from numerical overflow or underflow when the regularization parameter is small relative to the costs (Peyré and Cuturi, 2019, §4.4). This mission targets the exact relationship between the regularized minimum, the smooth dual maximum, and the scaling factors.

Setting

Fix positive integers $n,m$. A histogram $a\in\Sigma_n$ is a vector with nonnegative entries summing to one; $b\in\Sigma_m$ is defined similarly. Strict positivity is required for the attained dual maximum and log-domain updates; the primal scaling and Kantorovich-feasibility statements also cover zero-entry histograms. A coupling $P\in U(a,b)$ is an $n\times m$ matrix with nonnegative entries, row sums $a$, and column sums $b$. A real matrix $C$ assigns cost $C_{ij}$ to each transfer from row $i$ to column $j$, and $\langle C,P\rangle=\sum_{i,j}C_{ij}P_{ij}$ is its transport cost.

The book uses the entropy $H(P)=-\sum_{i,j}P_{ij}(\log P_{ij}-1)$, with $0\log0=0$. For $\varepsilon>0$, the regularized cost is $L_C^\varepsilon(a,b)=\min_{P\in U(a,b)}\{\langle C,P\rangle-\varepsilon H(P)\}$. The Gibbs kernel has entries $K_{ij}=\exp(-C_{ij}/\varepsilon)$. Given potentials $f\in\mathbb R^n$ and $g\in\mathbb R^m$, the smooth dual objective is $Q(f,g)=\langle f,a\rangle+\langle g,b\rangle-\varepsilon\sum_{i,j}e^{f_i/\varepsilon}K_{ij}e^{g_j/\varepsilon}$. These are the finite-dimensional objects of (4.1), (4.2), and (4.30) in the source (Peyré and Cuturi, 2019, pp. 425, 428, 448).

Formalization targets

Attained entropic duality

The goal is Proposition 4.4. There are an optimal coupling $P$ and potentials $(f,g)$ at which the dual reaches its maximum, with the common value

$$L_C^\varepsilon(a,b) =\langle C,P\rangle-\varepsilon H(P) =\max_{f',g'} Q(f',g').$$

For every maximizing pair $(f',g')$, the same optimal coupling satisfies

$$P_{ij}=e^{f'_i/\varepsilon}K_{ij}e^{g'_j/\varepsilon}.$$

Thus the dual potentials determine the scaling vectors $u=e^{f'/\varepsilon}$ and $v=e^{g'/\varepsilon}$ in (4.12). The maximum is an attained maximum of a real function, as stated in the book, rather than an unrestricted real infimum or supremum that might take a default value on a bad input (Peyré and Cuturi, 2019, Proposition 4.4).

Supporting results

The milestones follow the source's statements. Proposition 4.3 gives existence, uniqueness, and the Gibbs scaling of the primal optimizer. Remark 4.21 gives the two partial-gradient formulas and the closed log-domain block updates. Proposition 4.5 states that an entropic dual maximizer is a feasible pair of ordinary Kantorovich potentials, so its linear objective is bounded above by the unregularized cost $L_C(a,b)$ (Peyré and Cuturi, 2019, pp. 432, 449, 452–453).

Significance

The equality establishes that the matrix scaling variables and the dual potentials describe the same optimal coupling. It lets a computation based on scaling be interpreted as maximizing a smooth objective, and it gives exact marginal-error expressions through the dual gradients. Feasible Kantorovich potentials obtained at the optimum also provide a lower bound on the ordinary transport cost. These statements explain why log-domain updates represent the same mathematical problem as entropic transport, even when direct exponentiation is numerically fragile (Peyré and Cuturi, 2019, §§4.4–4.5).

The results are established in the textbook; the open work here is their Lean formalization. A completed development would provide reusable finite coupling, entropy, Gibbs-kernel, and smooth-dual interfaces, together with the existence and differentiability results needed to connect them. It would also distinguish a primal optimum, a dual maximum, and a feasible potential without relying on informal convention. The mission does not assert that these textbook results are new, and no machine-checked proof of these exact statements is claimed here.

Difficulty

The unconstrained dual objective has a symmetry: shifting every coordinate of $f$ by one constant and every coordinate of $g$ by its negative leaves the value unchanged. Consequently, the set of maximizers is not bounded in the ordinary product space. Positivity of the marginals matters for attaining a maximum with finite real potentials; if a marginal entry is zero, the corresponding potential can escape toward negative infinity. On the primal side, the entropy formula must be valid at zero entries even though optimality links it to strictly positive exponential scalings. The formal argument must connect these boundary conventions and the finite-dimensional optimization statements without turning the maximum into a junk real supremum (Peyré and Cuturi, 2019, Proposition 4.4 and Remark 4.21).

Formalization scope

The Lean development represents indices by Fin n and Fin m, matrices by Matrix (Fin n) (Fin m) ℝ, and histograms by Mathlib's stdSimplex. Positive dimensions and $\varepsilon>0$ appear throughout. Strictly positive marginal entries are required for the attained dual maximum and log-domain updates; the other statements permit zero entries. The book assumes positive weights for discrete measures in Remark 2.1; the marginal positivity is also required for the attained dual maximum and the logarithmic updates. The cost matrix itself may have arbitrary real entries. Entropy uses Real.negMulLog, which implements $0\log0=0$ on the nonnegative couplings where it is applied.

The primal optimum is a predicate on a coupling and its objective, rather than a chosen matrix. The unregularized $L_C$ is a real infimum used only when simplex marginals make its feasible set nonempty and bounded. The dual objective is a finite sum. Its gradients are stated as one-variable derivatives in each coordinate, and each block update is characterized as the unique maximizer with the other block fixed. The complete development needs Mathlib's finite sums, real exponential and logarithm, calculus, finite-dimensional topology, and optimization facts. Contributions that establish these shared interfaces or the four milestone statements are in scope.

Propositions 4.7 and 4.8 are excluded from this proposal because their printed bounds compare a dual linear objective with $L_C^\varepsilon$ where the accompanying arguments instead support a comparison with the unregularized $L_C$; (4.47) also has a sign discrepancy. The milestone list therefore avoids encoding a false inequality (Peyré and Cuturi, 2019, pp. 453–454).

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6), 2019, pp. 355–607. DOI: 10.1561/2200000073.

Motivation

A scattered subspace is an $\mathbb F_q$-subspace $U$ of an $\mathbb F_{q^n}$-vector space $V$ that meets every one-dimensional $\mathbb F_{q^n}$-subspace of $V$ in an $\mathbb F_q$-subspace of dimension at most one. Scattered subspaces produce scattered linear sets in projective spaces over finite fields, and through them two-intersection sets, two-weight codes, translation caps and maximum rank distance (MRD) codes. Blokhuis and Lavrauw (Geom. Dedicata 2000) proved that a scattered subspace of $V(r,q^n)$ has dimension at most $rn/2$, and constructions of that dimension are known whenever $rn$ is even (see Bartoli, Giulietti, Marino, Polverino 2018 and the references there).

Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) replace "one-dimensional" by "$h$-dimensional". The resulting $h$-scattered subspaces interpolate between scattered subspaces ($h=1$) and subspaces meeting every hyperplane in small dimension ($h=r-1$), which Sheekey and Van de Voorde (Des. Codes Cryptogr. 2020) showed to be equivalent to MRD codes with an idealiser isomorphic to $\mathbb F_{q^n}$. For the new notion the paper proves an upper bound on the dimension (Theorem 2.3) and shows that the bound is attained when $h+1$ divides $r$ (Theorem 2.6). This mission is the attainment half.

Setting

Let $\mathbb F_q\subseteq\mathbb F_{q^n}$ be finite fields, so $n=[\mathbb F_{q^n}:\mathbb F_q]$, and let $V=V(r,q^n)$ be an $r$-dimensional $\mathbb F_{q^n}$-vector space with $r\ge1$. Every $\mathbb F_{q^n}$-space is also an $\mathbb F_q$-space of dimension $rn$. For an integer $h$ with $0<h\le r-1$, an $\mathbb F_q$-subspace $U\le V$ is $h$-scattered (Definition 1.1) if

1. $U$ spans $V$ over $\mathbb F_{q^n}$, $\langle U\rangle_{\mathbb F_{q^n}}=V$, and
2. $\dim_{\mathbb F_q}(S\cap U)\le h$ for every $h$-dimensional $\mathbb F_{q^n}$-subspace $S$ of $V$.

An $h$-scattered subspace of largest possible $\mathbb F_q$-dimension is maximum $h$-scattered. Theorem 2.3 of the paper says that an $h$-scattered $U$ either has dimension $r$ and defines a subgeometry (an $\mathbb F_q$-basis of $U$ is an $\mathbb F_{q^n}$-basis of $V$), or satisfies

$$\dim_{\mathbb F_q}U\le\frac{rn}{h+1}.\tag{1}$$

Two building blocks appear in the statements. If $V=V_1\oplus\dots\oplus V_t$ with $V_i=V(r_i,q^n)$ and $U_i\le V_i$ are $\mathbb F_q$-subspaces, then $U=U_1\oplus\dots\oplus U_t$ is the direct sum of the $U_i$. For $r\le n$ the Gabidulin-type subspace of $\mathbb F_{q^n}^{\,r}$ is

$$G_r=\{(x,x^{q},x^{q^2},\dots,x^{q^{r-1}}) : x\in\mathbb F_{q^n}\},$$

the image of an $\mathbb F_q$-linear map, since $x\mapsto x^{q^j}$ fixes $\mathbb F_q$.

Formalization targets

Goal: Theorem 2.6 (p. 7)

If $h\ge1$, $h+1$ divides $r$ and $n\ge h+1$, then $V(r,q^n)$ contains an $\mathbb F_q$-subspace $U$ that is maximum $h$-scattered and satisfies

$$\dim_{\mathbb F_q}U=\frac{rn}{h+1}.$$

Milestones, in the order the paper uses them

• Proposition 2.1 (p. 3): for $h>1$, every $h$-scattered subspace is $i$-scattered for all $0<i<h$.
• Theorem 2.3 (p. 4): the dichotomy above, subgeometry or bound (1).
• Theorem 2.4 (p. 6): if $U_i$ is $h_i$-scattered in $V_i$, then $U_1\oplus\dots\oplus U_t$ is $\min_i h_i$-scattered in $V_1\oplus\dots\oplus V_t$.
• Theorem 2.4, second sentence (p. 6): if every $U_i$ is $h$-scattered with $\dim_{\mathbb F_q}U_i=r_in/(h+1)$, then the direct sum is $h$-scattered of dimension $rn/(h+1)$.
• Example 2.5 (p. 7): for $2\le r\le n$, $G_r$ is maximum $(r-1)$-scattered of dimension $n$.

Significance

Together with Theorem 2.3, the goal settles the largest dimension of an $h$-scattered subspace of $V(r,q^n)$ whenever $h+1\mid r$ and $n\ge h+1$: it is exactly $rn/(h+1)$. The subspaces it produces are the input of the paper's Delsarte duality (Theorem 3.3), which turns maximum $h$-scattered subspaces of $V(r,q^n)$ reaching bound (1) into maximum $(n-h-2)$-scattered subspaces of $V(rn/(h+1)-r,q^n)$ and so gives constructions also when $h+1\nmid r$. The direct-sum theorem is also of independent use: it extends the direct-sum construction for scattered linear sets of Bartoli, Giulietti, Marino and Polverino to every $h$, and Example 2.5 gives the subspace counterpart of Gabidulin codes.

All results in this mission are proved in the paper. To our knowledge none of them has a machine-checked proof; no formal library contains scattered subspaces, linear sets or Gabidulin-type subspaces. The remaining work is formalizing the paper's arguments: the counting of roots of linearized polynomials behind Example 2.5, the Grassmann-formula and quotient-space argument of Theorem 2.4, and the bound (1) of Theorem 2.3, which the companion mission on the dimension bound states as its goal.

Difficulty

The construction itself is short; the work lies in the three ingredients. The obvious approach to Theorem 2.4 fails: an $h$-dimensional $\mathbb F_{q^n}$-subspace $W$ of $V_1\oplus V_2$ need not be the sum of its intersections with $V_1$ and $V_2$, so the intersection $W\cap U$ cannot be bounded summand by summand. Example 2.5 needs that a nonzero $q$-polynomial $\sum_{j<r}a_jx^{q^j}$ has at most $q^{r-1}$ roots in $\mathbb F_{q^n}$, and the root set is an $\mathbb F_q$-subspace. Maximality is not a property of a single subspace: it quantifies over every $h$-scattered subspace of $V$ and so needs the full upper bound of Theorem 2.3, including the case $n<h+1$ handled there by Proposition 2.1.

Formalization scope

$\mathbb F_q$ is a finite field F, $\mathbb F_{q^n}$ a finite field K with Algebra F K, so $q=$ Fintype.card F and $n=$ Module.finrank F K. $V$ is a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V), and $r=$ Module.finrank K V. An $\mathbb F_q$-subspace is a Submodule F V; its intersection with an $\mathbb F_{q^n}$-subspace S is S.restrictScalars F ⊓ U.

Conventions the statements commit to:

• The range $0<h<r$ and the spanning condition are part of IsHScattered; without the range every spanning subspace would be $h$-scattered for $h\ge r$.
• Every quotient $rn/(h+1)$ is multiplied out, as $(h+1)\dim_{\mathbb F_q}U=rn$ or $\le rn$; no natural-number division is used.
• The direct sum in Theorem 2.4 is external: $V=\prod_{i<t}V_i$ ((i : Fin t) → V i) and $U=$ Submodule.pi Set.univ U. The minimum $h=\min_i h_i$ is given by $h\le h_i$ for all $i$ and $h=h_i$ for some $i$. The second part of Theorem 2.4 assumes $t\ge1$.
• Example 2.5 is stated on Fin r → K, with $G_r$ the range of the F-linear map $x\mapsto(x^{q^j})_{j<r}$, and assumes $r\ge2$ so that $(r-1)$-scattered is within Definition 1.1's range.
• The goal assumes $r\ge1$: $h+1$ divides $0$, but the zero space has no $h$-scattered subspace. The upper end $h<r$ follows from $h+1\mid r$.
• "Defines a subgeometry" in Theorem 2.3 is: some subset of $U$ spans $U$ over $\mathbb F_q$ and is an $\mathbb F_{q^n}$-basis of $V$.

The goal is not satisfied by a small subspace: both the dimension equality $(h+1)\dim_{\mathbb F_q}U=rn$ and maximality among all $h$-scattered subspaces of $V$ are part of its conclusion.

Results the paper cites without a number (the Blokhuis–Lavrauw bound for $h=1$, the direct-sum theorem for scattered linear sets) are not items. Theorem 2.3 is restated here because the maximality in Theorem 2.6 rests on it; it duplicates the goal of the companion mission. Useful infrastructure beyond this mission: roots of linearized polynomials over finite fields, dimension formulas for subspaces under restriction of scalars, and direct sums of $h$-scattered subspaces. Contributions on any milestone are welcome, and the goal can be closed from the milestones alone.

Selected references

• B. Csajbók, G. Marino, O. Polverino, F. Zullo, Generalising the scattered property of subspaces, arXiv:1906.10590v2, 2020; Combinatorica 41 (2021). https://arxiv.org/abs/1906.10590, https://doi.org/10.1007/s00493-020-4347-y
• A. Blokhuis, M. Lavrauw, Scattered spaces with respect to a spread in PG(n, q), Geom. Dedicata 81 (2000), 231–243. https://doi.org/10.1023/A:1005283806897
• D. Bartoli, M. Giulietti, G. Marino, O. Polverino, Maximum scattered linear sets and complete caps in Galois spaces, Combinatorica 38 (2018), 255–278. https://doi.org/10.1007/s00493-016-3531-6
• J. Sheekey, G. Van de Voorde, Rank-metric codes, linear sets, and their duality, Des. Codes Cryptogr. 88 (2020), 655–675. https://doi.org/10.1007/s10623-019-00703-z

Motivation

The discrete optimal transport problem of Kantorovich asks for the cheapest way to move a probability histogram $\mathbf a$ onto a histogram $\mathbf b$ when moving a unit of mass from $i$ to $j$ costs $\mathbf C_{i,j}$. Its optimal couplings are vertices of a polytope and are typically sparse: they rely on a few routes. Two communities have reasons to blur them. In transportation planning, observed traffic is more diffuse than linear-programming predictions, which led to the "gravity" model of Wilson (1969) and Erlander (1980), as recounted in Peyré and Cuturi, §4.1. In machine learning and statistics, adding an entropy term to the objective turns the linear program into a strictly convex problem that Sinkhorn's matrix-scaling algorithm solves at scale (Cuturi, 2013).

Every use of the entropic problem raises the same question: what does the regularized solution approximate? Chapter 4 of Peyré and Cuturi's Computational Optimal Transport answers it in Proposition 4.1 for the two extreme regimes of the regularization strength $\varepsilon$.

Timeline. Cominetti and San Martín (1994) studied the convergence of entropic penalties for linear programs, including first-order expansions near $\varepsilon = 0$ and $\varepsilon = +\infty$. Peyré and Cuturi (2019) record the transport case as Proposition 4.1, with a short compactness proof.

Setting

Fix sizes $n, m \ge 1$. A histogram is a vector of the probability simplex $\Sigma_n = \{\mathbf a \in \mathbb R^n_+ : \sum_i \mathbf a_i = 1\}$. Given $\mathbf a \in \Sigma_n$, $\mathbf b \in \Sigma_m$, the set of couplings is

$$\mathbf U(\mathbf a,\mathbf b) = \{\mathbf P \in \mathbb R_+^{n\times m} : \mathbf P\mathbb 1_m = \mathbf a,\ \mathbf P^\top\mathbb 1_n = \mathbf b\},$$

nonnegative matrices with row sums $\mathbf a$ and column sums $\mathbf b$. For a cost matrix $\mathbf C \in \mathbb R^{n\times m}$ write $\langle \mathbf C, \mathbf P\rangle = \sum_{i,j}\mathbf C_{i,j}\mathbf P_{i,j}$. The Kantorovich problem is $\mathrm L_{\mathbf C}(\mathbf a,\mathbf b) = \min_{\mathbf P \in \mathbf U(\mathbf a,\mathbf b)}\langle \mathbf C,\mathbf P\rangle$.

The discrete entropy of a coupling is

$$\mathbf H(\mathbf P) = -\sum_{i,j}\mathbf P_{i,j}(\log \mathbf P_{i,j} - 1),$$

with $0\log 0 = 0$. For $\varepsilon > 0$ the entropic problem is

$$\mathrm L^\varepsilon_{\mathbf C}(\mathbf a,\mathbf b) = \min_{\mathbf P\in\mathbf U(\mathbf a,\mathbf b)}\langle \mathbf P,\mathbf C\rangle - \varepsilon\mathbf H(\mathbf P),$$

whose unique minimizer is $\mathbf P_\varepsilon$. The maximum-entropy optimal coupling $\mathbf P^\star_0$ is the optimal coupling of the Kantorovich problem with the largest entropy. The Gibbs kernel is $\mathbf K_{i,j} = e^{-\mathbf C_{i,j}/\varepsilon}$ and the Kullback–Leibler divergence between matrices is $\mathrm{KL}(\mathbf P|\mathbf K) = \sum_{i,j}\mathbf P_{i,j}\log(\mathbf P_{i,j}/\mathbf K_{i,j}) - \mathbf P_{i,j} + \mathbf K_{i,j}$.

In Lean these are couplings, frob and IsOptimalCoupling in CompOT.Assignment, and entropy, entObjective, IsEntropicOptimal, IsMaxEntropyOptimal, gibbs and klMat in CompOT.EntropicLimit.

Formalization targets

Goal: Proposition 4.1

For $\mathbf a\in\Sigma_n$, $\mathbf b \in \Sigma_m$ and any cost matrix $\mathbf C$,

$$\mathbf P_\varepsilon \xrightarrow{\varepsilon\to 0^+} \mathbf P^\star_0,\qquad \mathrm L^\varepsilon_{\mathbf C}(\mathbf a,\mathbf b)\xrightarrow{\varepsilon\to 0^+}\mathrm L_{\mathbf C}(\mathbf a,\mathbf b),\qquad \mathbf P_\varepsilon\xrightarrow{\varepsilon\to+\infty}\mathbf a\otimes\mathbf b = (\mathbf a_i\mathbf b_j)_{i,j}.$$

Milestones

1. For $\varepsilon > 0$, problem (4.2) has a unique optimal solution (§4.1, p. 425).
2. The maximum-entropy optimal coupling (4.3) exists and is unique (proof of Proposition 4.1, p. 426).
3. The sandwich (4.5): for an optimal $\mathbf P$ and $\varepsilon>0$, $0 \le \langle\mathbf C,\mathbf P_\varepsilon\rangle - \langle \mathbf C,\mathbf P\rangle \le \varepsilon(\mathbf H(\mathbf P_\varepsilon) - \mathbf H(\mathbf P))$.
4. $\mathbf a \otimes \mathbf b$ is the unique maximizer of $\mathbf H$ on $\mathbf U(\mathbf a,\mathbf b)$ (p. 426).
5. (4.7): $\mathbf P_\varepsilon$ is the KL projection of the Gibbs kernel onto $\mathbf U(\mathbf a,\mathbf b)$ (p. 428).

Significance

The result. Proposition 4.1 justifies the entropic regularization as an approximation scheme: for small $\varepsilon$ the regularized plan converges to an exact optimal plan, and specifically to a canonical one, the most diffuse among all optimal couplings, so the limit does not depend on any tie-breaking. The value $\mathrm L^\varepsilon_{\mathbf C}$ converges to the transport cost, which is what makes Sinkhorn-based estimates of transport distances meaningful. For large $\varepsilon$ the plan becomes the independent coupling $\mathbf a\otimes\mathbf b$, which explains the interpolation between optimal transport and maximum mean discrepancy studied later in the book. The KL projection identity (4.7) is the starting point of Sinkhorn's algorithm, so this mission also supplies the bridge to the next missions of the series.

Formalizing it. The proposition is a known result with a complete proof in the source; the work is formalizing it in Lean 4 with Mathlib. To our knowledge none of these statements, nor the discrete entropic transport problem itself, has a machine-checked proof in Mathlib or on the platform. A formal proof also pins down the convention for zero entries, on which the statement silently depends.

Difficulty

The obvious argument passes to the limit in the optimality of $\mathbf P_\varepsilon$, but this only shows that limit points are optimal for the Kantorovich problem; it does not identify which optimal coupling is the limit when the optimal set is a face of the polytope rather than a vertex. Identifying it requires a second-order argument at the level of the entropy, and the convergence of the whole family (not just a subsequence) rests on the uniqueness of the maximum-entropy optimal coupling, which in turn needs strict concavity of $\mathbf H$ on a set that may contain matrices with zero entries, where the logarithm is singular. Existence and uniqueness of $\mathbf P_\varepsilon$ face the same boundary issue: the minimizer may a priori sit on the boundary of the polytope.

Formalization scope

Indices are 0-based (Fin n, Fin m); histograms are functions Fin n → ℝ in Mathlib's stdSimplex; matrices are Matrix (Fin n) (Fin m) ℝ with the product topology, so convergence is entrywise. Entropy uses $0\log 0 = 0$ (Real.negMulLog); the book's remark that $\mathbf H = -\infty$ at a zero entry is not used, since it would contradict the continuity of $\mathbf H$ invoked in the book's proof and make (4.3) degenerate. Optimality is expressed by predicates (a minimizer over $\mathbf U(\mathbf a,\mathbf b)$), never by a real infimum, so no junk value of an empty infimum appears. The limit $\varepsilon \to 0$ is taken from the right. The values $\mathrm L^\varepsilon_{\mathbf C}$ and $\mathrm L_{\mathbf C}$ appear as the objectives at $\mathbf P_\varepsilon$ and $\mathbf P^\star_0$.

In the goal, $\mathbf P_\varepsilon$ and $\mathbf P^\star_0$ are given by hypotheses (any family solving (4.2) for every $\varepsilon > 0$, any solution of (4.3)). This is not a vacuous formalization: milestones 1 and 2 assert that such objects exist and are unique, so the hypotheses are satisfiable and determine them. Standing assumptions are exactly those of the book: $\mathbf a \in \Sigma_n$, $\mathbf b \in \Sigma_m$, $\varepsilon > 0$; no positivity of $\mathbf a$, $\mathbf b$ or $\mathbf C$ is assumed.

A complete development needs: compactness of the transport polytope, continuity and strict concavity of $x \mapsto -x\log x$ on $[0,\infty)$, and the Gibbs inequality on finite sums. These are reusable for the Sinkhorn and entropic-duality missions of this series. Proofs of any milestone are welcome independently.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (§4.1, pp. 425–430)
• R. Cominetti and J. San Martín, Asymptotic analysis of the exponential penalty trajectory in linear programming, Mathematical Programming 67(1–3):169–187, 1994. https://doi.org/10.1007/BF01582220
• M. Cuturi, Sinkhorn Distances: Lightspeed Computation of Optimal Transport, NeurIPS 2013. https://arxiv.org/abs/1306.0895
• A. G. Wilson, The use of entropy maximizing models, in the theory of trip distribution, mode split and route split, Journal of Transport Economics and Policy, 108–126, 1969 (bibliography of Peyré and Cuturi). https://doi.org/10.1561/2200000073
• S. Erlander, Optimal Spatial Interaction and the Gravity Model, Vol. 173, Springer-Verlag, 1980 (bibliography of Peyré and Cuturi). https://doi.org/10.1561/2200000073