Functional Analysis

Motivation

Recursive potentials can define tree norms with controlled midpoint behavior. The central question is whether that control forces an asymptotically uniformly convex renorming. The pinned manuscript supplies the research context.

Setting

The encoded constructions include root-sum and zero-root completions, finite tree heads, aggregation spaces and variable-exponent coordinate models. Two least nonnegative potential fields determine the norms.

Formalization target

The selected goal is OAI.ComparatorModel.RecursivePotentials.main. Its central assertion is

$$\overline\delta(t)\geq t^3/128\qquad(0<t<1).$$

The theorem states (its proof is admitted with sorry) that the defined proposition MainClaim holds. MainClaim asserts that there exist constructions, over index types in universe 0, of the finite rooted tree head structure, the tree-vector spaces, the zero-root tree-vector spaces, the aggregation-vector spaces, and their l^p-coordinate models, such that eleven statements about completions of finite-support vectors on rooted trees hold simultaneously. These comprise: (1) completion statements saying that the root-sum tree space for the sequence tree and for the joined tree, and the zero-root space for the joined tree, are complete, infinite-dimensional, with continuous coordinates extending the vector coordinates, continuous potential fields P and Q extending the finite-tree ones, norm equal to P+Q at the root (or both P and Q at the root in the zero-root case, where the root coordinate vanishes), and with norm-nonincreasing idempotent coordinate projections onto initial subtrees having finite-dimensional range, closed finite-codimensional tails and approximation of tail elements by vectors vanishing on the head, and that XZero and XJoined are reflexive; (2) a main statement giving the lower bound t^3/128 on the averaged modulus of XSigma and XJoined for 0<t<1, a cubic-type uniform convexity inequality (‖x+z‖+‖x-z‖)/2 ≥ ‖x‖+‖z‖^3/(8(2‖x‖+‖z‖)^2) for x supported on a head and z vanishing there, and that no equivalent norm on XSigma, XZero or XJoined has the AUC property (positive modulus at every positive t); (3) positivity of the averaged modulus of XSigma at every positive radius t; (4) a separation statement for XJoined: for each ε>0 there is η in (0,1), equal to min(1/2, logarithmicGamma(2, ε/16)) when ε≤2, such that if ‖x±z_n‖≤1 for all n and the z_n are pairwise at distance at least ε, then ‖x‖≤1-η; (5) properties of the variable-exponent l^2-sum of height-h tree spaces with exponents 1+1/h, namely completeness, reflexivity, separable dual, a root-sum functional ν (nonnegative, definite, subadditive, absolutely homogeneous) bounded above and below by explicit multiples of the l^p norm, dense finitely supported vectors, and finite-rank projections; (6) a recursive characterization of the l^p-model potentials by least pairs, with ν equal to the root P plus Q; (7) for every equivalent norm A on the variable space, the modulus at lower/upper vanishes; (8) the absence of any equivalent AUC norm there; (9) a sixth-power stability inequality and (10) a cubic stability inequality for admissible heads, with explicit constants; and (11) a weak-tail estimate: if x and a weakly null sequence y_j with ‖y_j‖≥ε, 0<ε≤1, satisfy ‖x±y_j‖≤1, then ‖x‖≤θ(ε)<1.

Significance and status

The published MainClaim is an eleven-part package, not only the displayed midpoint inequality. Its additional completion, separation, stability, weak-tail and no-AUC assertions remain part of the goal. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The bundled target must coordinate completion, continuous coordinate maps, finite-head approximations, reflexivity and uniform estimates across several related spaces.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Midpoint convexity from two recursive potentials, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Independent positive multipliers on a branching tree generate concrete subspaces of real L1. Their asymptotic geometry can distinguish midpoint estimates from AUC renormability. The pinned manuscript supplies the research context.

Setting

A nonconstant positive multiplier has probability law μ, mean one and finite second moment. Path products are multiplied along nonempty prefixes, and their L1 classes generate a closed real span.

Formalization target

The selected goal is OAI.IndependentProducts.main_general. Its central assertion is

$$\dim\operatorname{productSpan}(\mu)=\infty,\qquad\neg\exists\text{ equivalent AUC norm}.$$

The theorem states that, for any Borel measure μ on ℝ satisfying the multiplier hypotheses, the closed real L¹ span of the path products is infinite-dimensional, and no equivalent norm on it is AUC. The hypotheses say that μ is a probability measure, almost every value is positive, μ is not almost surely equal to any constant, its mean is 1, and the identity function has a finite second moment (is in L²). Vertices are finite lists of positive integers, a sample assigns a real number to each nonroot vertex, and the product measure is the infinite product of independent copies of μ, one per nonroot vertex. The path product of a vertex v multiplies the sample values at the nonempty prefixes of v, and is 1 for the root. productSpan(μ) is the topological closure, in L¹ of the product measure, of the real linear span of the classes equal almost everywhere to some path product. The theorem concludes first that productSpan(μ) is not finite-dimensional over ℝ. Second, for every seminorm N on productSpan(μ) that is an equivalent norm, meaning there are constants 0<a≤b with a‖x‖≤N(x)≤b‖x‖ for all x, N fails the AUC property, which requires that, for every t>0, the one-sided asymptotic modulus of N at t is strictly positive. That modulus is the infimum over N-unit vectors x of the supremum over closed finite-codimension subspaces F of the infimum of N(x+ty)−1 over y in F with N(y)=1. The statement is given as an admitted theorem without proof.

Significance and status

The selected general target asserts infinite dimension and absence of AUC renormings. Specific exponential and Gaussian-square midpoint estimates are separate published targets, retained as additional references. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The obstruction must work for every admissible multiplier distribution and every equivalent norm, rather than only a particular exponential example.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.IndependentProducts.main_exponential (Open).
• OAI.IndependentProducts.main_gaussian_12 (Open).
• OAI.IndependentProducts.main_gaussian_24 (Open).

Selected references

• OpenAI, Independent products in real L1: asymptotic midpoint convexity without AUC renormings, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

Uniform discreteness places a lower bound on distances between points. The target tests whether that metric simplicity forces uniformly bounded finite-rank approximation in the associated Lipschitz-free space. The pinned manuscript supplies the research context.

Setting

The free space is the closed real span of point evaluations in the dual of Lipschitz functions vanishing at a base point. Approximation and bounded approximation retain their distinct operator-norm quantifiers.

Formalization target

The selected goal is OAI.DiscreteFree.source_endpoints. Its central assertion is

$$\mathrm{AP}(\mathcal F(M))\quad\land\quad\forall\Lambda\geq1,\ \neg\mathrm{BAP}_\Lambda(\mathcal F(M)).$$

The theorem states that two propositions hold together, both about the Lipschitz-free space FreeSpace(o) of a pointed metric space (M,o), which is the closed linear span, inside the dual of the Banach space Lip0(o) of real Lipschitz functions vanishing at o (normed by the supremum of the slopes |f(x)-f(y)|/d(x,y)), of the point evaluations; delta(o,a) denotes the evaluation at a. The first, BlockStatement, says that for every natural number p ≥ 1 there exist a countable metric space M and a base point o with all distinct points at distance at least 1 and all distances at most 300p²+150p+5, together with a finite set A of M containing o, such that every bounded linear operator T on FreeSpace(o) of finite rank and norm at most p moves some delta(o,a) with a in A by at least 1/2, that is ‖T(delta(o,a))-delta(o,a)‖ ≥ 1/2. The second, MainStatement, says there exist a countable metric space M and a point o such that distinct points are at distance at least 1, M is unbounded, M is not a proper space, FreeSpace(o) has the approximation property (finite-rank bounded operators approximate the identity uniformly on every compact set to within any ε>0), and yet for every Λ ≥ 1 FreeSpace(o) fails the bounded approximation property with constant Λ, meaning the approximating finite-rank operators cannot all be chosen with norm at most Λ. The theorem is stated with sorry, so no proof is asserted here.

Significance and status

The selected conjunction includes quantitative block obstructions and an unbounded, nonproper, uniformly discrete example. The quantitative real-ℓ1 renorming target is retained as an additional reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Compact-set approximation must remain possible while every candidate uniform norm bound fails. The finite block obstruction must survive in one countable space.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

• OAI.DiscreteFree.real_l1_quantitative_renorming (Open).

Selected references

• OpenAI, A uniformly discrete counterexample to bounded approximation in Lipschitz-free spaces, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

The separable quotient problem asks whether every infinite-dimensional Banach space admits a separable infinite-dimensional quotient. The selected statement isolates a negative result under the continuum hypothesis. The pinned manuscript supplies the research context.

Setting

A quotient is encoded as a surjective bounded linear map between Banach spaces over the same scalar field. The target considers both real and complex scalars.

Formalization target

The selected goal is OAI.SeparableQuotient.negative_main. Its central assertion is

$$\mathrm{CH}\quad\Longrightarrow\quad\neg\mathrm{SQ}(\mathbb R)\land\neg\mathrm{SQ}(\mathbb C).$$

The theorem states that, under the continuum hypothesis CH (the defined proposition that the cardinality of ℝ equals ℵ₁), the separable quotient assertion fails over both the real and the complex numbers, at any universe level u. Here SQ over a scalar field 𝕜 (ℝ or ℂ) asserts that every complete normed space X over 𝕜 in Type u that is not finite-dimensional has a separable quotient in the following sense: there exist a complete, separable, infinite-dimensional normed space Y over 𝕜, also in Type u, and a bounded 𝕜-linear map T from X to Y that is surjective. The conclusion is the conjunction of ¬SQ(ℝ) and ¬SQ(ℂ), so for each field there is an infinite-dimensional Banach space with no such bounded surjection onto an infinite-dimensional separable Banach space. The statement is admitted without proof in the source.

Significance and status

CH is an explicit assumption. The published goal does not state relative consistency, a positive model, or the complete independence assertion in the manuscript title. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The obstruction must rule out every bounded surjection onto every separable infinite-dimensional target space, rather than one proposed quotient.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

• OpenAI, Relative independence of the separable quotient problem, preprint, 2026. Manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

Motivation

The determinant of a nonsingular integer matrix has absolute value at least one. The source examines the proposed counterpart for integer matrices over group rings, where the determinant is defined by an operator trace. The source is OpenAI's September 2026 manuscript.

Setting

The left regular operator associated to a group-ring matrix acts on $\ell^2(G)^n$ by finite convolution. Its Fuglede–Kadison determinant in the invertible case is the exponential of half the real trace of the logarithm of its positive square.

Formalization targets

$$\exists A\in M_n(\mathbb Z[G]),\quad A\text{ invertible over }\mathbb Q[G],\quad 0<\det_{\mathcal N(G)}(T_A)<1.$$

The defined proposition MainStatement holds, i.e. there exist a group G that is finitely generated, an integer n ≥ 1, an n×n matrix A with entries in the integral group ring ℤ[G], and a bounded ℂ-linear operator T on the Hilbert space l²(G)^n (square-summable complex functions on Fin n × G) such that four conditions hold. First, the image of A in the rational group ring ℚ[G] (obtained by applying the integer-to-rational map to every coefficient) is an invertible matrix over ℚ[G]. Second, T is exactly the left-regular operator of A, meaning (Tξ)(i,h) = Σ_j Σ_g a_{ij}(g) ξ(j, g⁻¹h), where a_{ij}(g) ∈ ℤ is the coefficient of g in the entry A_{ij}. Third, T is invertible as a bounded operator on l²(G)^n. Fourth, its Fuglede–Kadison determinant fkDet(T) = exp(Re tr(log(T*T))/2) satisfies 0 < fkDet(T) < 1, where tr(S) = Σ_i ⟨e_i, S e_i⟩ is the unnormalized trace summing over the basis vectors e_i supported at the identity element of G in component i, and log is the continuous functional calculus logarithm.

The goal is OAI.GroupRingDeterminant.main.

Significance

The goal gives a square-matrix obstruction with both a rational group-ring inverse and a bounded operator inverse. This keeps the logarithm in the invertible setting. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

The trace logarithm is not an ordinary finite-dimensional determinant polynomial. The algebraic matrix and bounded regular operator must be shown to match exactly before the determinant estimate is meaningful.

Formalization scope

The group is finitely generated and $n\ge1$. Lean uses complex square-summable functions on Fin n × G, the unnormalized matrix trace, and continuous functional calculus for the logarithm. Invertibility is explicit on both the rational matrix and the operator.

The shared definitions are supplied by GroupRingDeterminant. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, A Counterexample to the Group-Ring Determinant Conjecture, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation

A norm is uniformly convex when midpoints of far-apart unit vectors are pushed strictly inside the unit ball. In infinite-dimensional Banach spaces the useful notions are asymptotic: one asks for a gain only in directions taken from a subspace of finite codimension, chosen after the center is fixed. Two such notions are compared here. Asymptotic uniform convexity (AUC) asks for growth of $\|x+ty\|$ in every far-out unit direction $y$; asymptotic midpoint uniform convexity (AMUC) asks only that the average of $\|x+ty\|$ and $\|x-ty\|$ grows. These properties control nonlinear embeddings (for instance of countably branching diamond graphs) and are standard tools in the asymptotic geometry of Banach spaces.

Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) asked whether AMUC and AUC are equivalent up to renorming. Baudier (2026) answered no, using subspaces of $L^1$ whose unit ball is compact in measure and the Daugavet-property example of Kadets and Werner. This mission asks for the exact values of both moduli in that setting.

Timeline

• 1980. Bourgain and Rosenthal construct a subspace of $L^1$ whose unit ball is relatively compact in measure but which fails the Radon–Nikodym property (doi:10.1007/BF02762868).
• 1983. Brézis and Lieb prove their splitting identity for pointwise convergent sequences in $L^p$ (doi:10.1090/S0002-9939-1983-0699419-3).
• 2000. Kadets, Shvidkoy, Sirotkin and Werner give the slice characterization of the Daugavet property (arXiv:math/9709216); Shvydkoy gives its weak-open form (doi:10.1006/jfan.2000.3626).
• 2004. Kadets and Werner refine the Bourgain–Rosenthal construction to obtain a space with the Schur and Daugavet properties (doi:10.1090/S0002-9939-03-07278-2).
• 2016. Dilworth et al. introduce AMUC and ask whether it is equivalent to AUC up to renorming (doi:10.1016/j.jmaa.2015.11.061).
• 2026. Baudier proves AMUC for measure-compact subspaces of $L^1$ and deduces a negative answer via the Kadets–Werner space (arXiv:2609.21283).

The source of this mission is an OpenAI preprint dated September 27, 2026, which computes both moduli exactly.

Setting

All spaces are real. For a Banach space $X$ with norm $N$, let $\operatorname{cof}(X)$ be its closed linear subspaces of finite codimension. For $N(x)=1$ and $t>0$,

$$H_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)\ge1}}\Bigl(\frac{N(x+ty)+N(x-ty)}2-1\Bigr),\qquad D_N(x,t)=\sup_{F\in\operatorname{cof}(X)}\ \inf_{\substack{y\in F\\ N(y)=1}}\bigl(N(x+ty)-1\bigr).$$

The averaged midpoint modulus $\widehat\delta_N(t)$ and the one-sided modulus $\overline\delta_N(t)$ are the infima of $H_N(x,t)$ and $D_N(x,t)$ over unit $x$. $N$ is AUC if $\overline\delta_N(t)>0$ for all $t>0$. A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ with $a,b>0$.

A space has the Daugavet property if $\|I+T\|=1+\|T\|$ for every rank-one bounded operator $T$. On a probability space $(\Omega,\mathbb P)$, convergence in measure is given by the metric

$$d(f,g)=\inf\{a>0:\ \mathbb P(|f-g|>a)<a\}.$$

A set is totally bounded in measure if for each $\varepsilon>0$ it is covered by finitely many $d$-balls of radius $\varepsilon$.

Formalization targets

Goal: Theorem 1.1

Let $E$ be an infinite-dimensional closed subspace of $L^1(\Omega,\mathbb P)$, $\mathbb P$ a probability measure, whose unit ball is totally bounded in measure and whose norm has the Daugavet property. Then for every unit $x\in E$ and $t>0$

$$H_E(x,t)=\max\{t/2,\ t-1\},\qquad D_E(x,t)=\max\{0,\ t-2\},$$

so $\widehat\delta_E(t)=\max\{t/2,t-1\}$ and $\overline\delta_E(t)=\max\{0,t-2\}$, and $E$ admits no equivalent AUC norm. Lean: OAI.ExactModuli.exact_main (open on the platform).

Milestone: Theorem 6.1 (Kadets–Werner construction)

On $([0,1]^{\mathbb N},\lambda^{\mathbb N})$ there is an infinite-dimensional closed subspace $E\subseteq L^1$ whose unit ball is totally bounded in measure and which has the Daugavet slice property. Lean: OAI.ExactModuli.kadets_werner_existence. The proposal also carries OAI.ExactModuli.exact_example, the combination of the two theorems for this space.

Significance

The formulas show how far apart the two moduli can be: the averaged modulus grows linearly from $0$, while the one-sided modulus vanishes on the whole interval $(0,2]$. They refine Baudier's qualitative AMUC statement and linear lower bound into exact curves at every unit center, and the renorming clause shows that no equivalent norm can repair the one-sided modulus. Together with Theorem 6.1, they give a concrete space realizing the separation.

The results are proved in an OpenAI preprint; they have not been peer reviewed, and no machine-checked proof exists. The Daugavet slice characterization, Bourgain's lemma on slices and weak neighborhoods (Lemma 3.2), and the construction itself are reusable pieces of Banach space theory that a formalization would supply.

Difficulty

The lower bound for $H_E$ must hold uniformly over all directions in some finite-codimensional subspace, while the hypothesis only says that the unit ball is compact in a weak metric. A compactness argument along subsequences (Baudier's route via Brézis–Lieb) gives positivity but not the exact constant. The upper bounds need directions in a prescribed finite-codimensional subspace that are almost at distance $2$ from $x$; the Daugavet property supplies such vectors only in weak neighborhoods, and they must then be corrected into the subspace. The renorming clause must handle an arbitrary equivalent norm, for which neither formula is available.

Formalization scope

• Cofinite F is a closed submodule with finite-dimensional quotient. H, D, averagedModulus, oneSidedModulus follow the displayed sup/inf order; H ranges over $N(y)\ge1$, D over $N(y)=1$.
• EquivalentNorm N is a Seminorm with two-sided comparison constants $a,b>0$; AUC N is positivity of oneSidedModulus N t for every $t>0$.
• Daugavet X quantifies over rank-one operators written as ell.smulRight v.
• measureDistance is the metric $d$ on Lp ℝ 1 μ; MeasurePrecompactBall μ E requires finite $\varepsilon$-nets (centers in $L^1$) of the unit ball of $E$; μ is a probability measure.
• kwMeasure is the product of Lebesgue measures on $\mathbb N\to[0,1]$.
• The moduli are real-valued sSup/sInf; for infinite-dimensional $E$ the relevant sets are nonempty and bounded, so the junk values are not used.

A full development needs the Daugavet slice characterization (Lemma 3.1), Bourgain's lemma (Lemma 3.2), the weak-neighborhood diameter-two property (Lemma 3.3), $L^1$ truncation estimates, and the Kadets–Werner iteration (Lemmas 6.2–6.3). Formalizations of these lemmas are welcome.

Selected references

• OpenAI, Exact asymptotic moduli in a Daugavet subspace of $L^1$, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exact-asymptotic-moduli-in-a-Daugavet-subspace-of-L1-September-27-2026/manuscript.pdf
• F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• V. Kadets, D. Werner, A Banach space with the Schur and the Daugavet property, Proc. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0002-9939-03-07278-2
• J. Bourgain, H. P. Rosenthal, Martingales valued in certain subspaces of $L^1$, Israel J. Math., 1980. https://doi.org/10.1007/BF02762868
• V. M. Kadets, R. V. Shvidkoy, G. G. Sirotkin, D. Werner, Banach spaces with the Daugavet property, Trans. Amer. Math. Soc., 2000. https://arxiv.org/abs/math/9709216
• R. V. Shvydkoy, Geometric aspects of the Daugavet property, J. Funct. Anal., 2000. https://doi.org/10.1006/jfan.2000.3626
• H. Brézis, E. Lieb, A relation between pointwise convergence of functions and convergence of functionals, Proc. Amer. Math. Soc., 1983. https://doi.org/10.1090/S0002-9939-1983-0699419-3

Motivation

In a uniformly convex space, if $x$ is nearly as long as $R$ and both $x+y$ and $x-y$ have length at most $R$, then the displacement $y$ must be short. The set of such displacements,

$$\mathcal L(x,R)=\{y:\ \|x+y\|\le R,\ \|x-y\|\le R\},$$

is a symmetric lens. In infinite dimensions the right question is asymptotic: is $y$ short after discarding finitely many directions? Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016) characterized asymptotic midpoint uniform convexity (AMUC) through the measure of noncompactness of such lenses. AMUC is the property that, together with asymptotic uniform convexity (AUC), governs which countably branching graphs embed into a Banach space with bounded distortion.

This mission asks for an explicit lens estimate in two James-type tree spaces, with a bound depending only on the squared-radius deficit $R^2-\|x\|^2$ of the center and holding for every displacement simultaneously after one finite set of coordinates is removed.

Timeline

• 1974. James introduces the square-sum norm over disjoint segments of a tree (doi:10.1090/S0002-9904-1974-13580-9).
• 1985. Ghoussoub and Maurey study $G_\delta$-embeddings in Hilbert space (doi:10.1016/0022-1236(85)90039-4); the coordinate predual $B_\infty$ used here is the Ghoussoub–Maurey–Schachermayer construction as presented by Banakh (2000).
• 2001. Girardi proves AUC of the canonical predual and of the full dual of the binary James tree space (doi:10.4064/sm147-2-2).
• 2016. Dilworth et al. introduce AMUC and characterize it by lenses (doi:10.1016/j.jmaa.2015.11.061).
• 2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of countably branching diamonds (arXiv:1612.01984).
• 2021. Perreau asks whether the canonical predual of the countably branching James tree space is AMUC (Question 6 of arXiv:2104.10494).
• 2026. Baudier shows that AMUC does not imply AUC renormability, via the Kadets–Werner modification of the Bourgain–Rosenthal space (arXiv:2609.21283).

The source of this mission is an OpenAI preprint dated September 27, 2026.

Setting

All scalars are real.

Finite-height forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the tree of words of length at most $h$, ordered by extension (the root is the empty word). The forest $\mathcal F$ is the disjoint union of one copy $\{h\}\times T_h$ for each $h\ge1$. Write $a\preceq b$ if $a$ is an ancestor of $b$ in the same component. A segment is a nonempty interval $[a,b]=\{v: a\preceq v\preceq b\}$. For finitely supported $u$ put $u(S)=\sum_{v\in S}u(v)$ and

$$\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.$$

Let $J$ be the completion of $(c_{00}(\mathcal F),\rho)$ and $X=J^*$ with the dual norm. Coordinate evaluation gives functionals $e_v^*\in X$.

Infinite tree. Let $T_\infty=\mathbb N^{<\omega}$ (all finite words, root included), $J_\infty$ the completion for the same norm, and $B_\infty=\overline{\operatorname{span}}\{e_v^*\}\subset J_\infty^*$, closed in the dual norm.

A finite set $H$ of vertices is ancestral if it contains all ancestors of its elements. On either space,

$$P_Hx=\sum_{v\in H}x(e_v)\,e_v^*,\qquad Q_Hx=x-P_Hx.$$

Formalization targets

Goal: Theorem 1.1

For $Y\in\{X,\ B_\infty\}$, every finite ancestral $H$, every $x,y\in Y$ with $x=P_Hx$, and every $R\ge0$ with $\|x+y\|\le R$ and $\|x-y\|\le R$,

$$\|Q_Hy\|\ \le\ 2\sqrt{R^2-\|x\|^2}.$$

The Lean statement OAI.SegmentLenses.midpoint_lens_main is the conjunction of the two cases. It is open on the platform. The displacement $y$ may have a nonzero head $P_Hy$; only its tail is controlled.

Significance

The estimate is uniform over the lens: one finite head $H$ controls every admissible displacement, which is exactly what is needed when a single center has infinitely many approximate midpoints. As a consequence (Corollary 7.1 of the source) both given norms are AMUC with $\widehat\delta(t)\ge(\sqrt{1+t^2/4}-1)/2$, while Proposition 9.1 shows that neither space admits an equivalent AUC norm. In particular the infinite-height case answers Perreau's question for the specified real norm on $B_\infty$, and the finite-height forest gives a reflexive space separating AMUC from AUC renormability. A companion preprint uses this theorem to force distortion $D^2\ge1+k/4$ for depth-$k$ countably branching diamonds.

The result is proved only in the OpenAI preprint; it is not peer reviewed and has no machine-checked proof. Formalizing it would certify the cancellation analysis that drives the constant $2$.

Difficulty

The natural attempt is to represent a nearly norming functional for the center as a convex combination of disjoint segment functionals and read off the tail. The obstacle is cancellation: two atoms leaving the head $H$ through the same vertex can have segment sums of opposite sign, and a naive estimate loses all control. The bound must also hold for every displacement with the same $H$, so compactness arguments that choose $H$ after $y$ do not suffice, and an independent radial approach in the source gives only the weaker $(\sqrt2+\sqrt6)\sqrt{R(R-\|x\|)}$.

Formalization scope

• Vertices: ForestVertex is the subtype of pairs $(h,w)$ with $1\le h$ and $|w|\le h$; InfiniteVertex := List ℕ. Ancestry is equality of heights plus List.IsPrefix (resp. prefix only).
• Segments: IsInterval ancestor S asserts $S=[a,b]$ with $a\preceq b$, so segments are nonempty. A test family is a finite set of pairwise disjoint segments, and segmentSeminorm is the supremum of the Euclidean norms of the vectors of segment sums.
• Spaces: X := StrongDual ℝ (UniformSpace.Completion (Test ForestVertex)); BInfinite is the closed span of the coordinate functionals inside the full dual of the infinite-tree completion, carrying the subspace (dual) norm.
• head H x = ∑ v ∈ H, x(e_v) • e_v^* and tail H x = x - head H x; ancestrality is Ancestral.
• Trivialization check: $R\ge0$ is required as in the source, and since $\|x\|\le R$ follows from the lens condition, the square root argument is never negative.

A full development needs the James segment norm, its completion and dual, contractivity of coordinate projections, the $\ell_2$ decomposition of the tail over descendant cones (Lemma 2.2), and the atomic description of finite head balls (Section 4). This infrastructure is shared with the other missions in the same family. Formalizations of Lemma 2.1, Lemma 2.2, Corollary 7.1 and Proposition 9.1 are welcome as supporting results.

Selected references

• OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
• M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
• Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494
• F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
• F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
• N. Ghoussoub, B. Maurey, $G_\delta$-embeddings in Hilbert space, J. Funct. Anal., 1985. https://doi.org/10.1016/0022-1236(85)90039-4

Motivation

Uniform convexity of a norm says that the midpoint of two far-apart points of the unit sphere lies strictly inside the ball. In infinite dimensions there is an asymptotic version: one only asks for a gain in directions that lie far out, that is, inside some closed subspace of finite codimension. Asymptotic uniform convexity and its relatives control the large-scale geometry of a Banach space, and in particular which infinite graphs can be embedded into the space with bounded distortion.

Two such properties are compared here. Asymptotic uniform convexity (AUC) demands a gain in every far-out direction separately; asymptotic midpoint uniform convexity (AMUC), introduced by Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov (2016), only asks for a gain when a direction and its opposite are tested together. Every AUC norm is AMUC. The question is how far apart the two notions are, both up to renorming and in terms of metric embeddings of the countably branching diamond graphs $D_k$.

Timeline

• 1974. James introduces the square-sum norm over disjoint segments of a tree (the James tree space) (doi:10.1090/S0002-9904-1974-13580-9).
• 2001. Girardi proves that the coordinate predual and the full dual of the binary James tree space are AUC (doi:10.4064/sm147-2-2).
• 2004 and 2009. Lee and Naor obtain quantitative $L_p$ distortion bounds for finite binary diamonds; Johnson and Schechtman relate diamond embeddings to super-reflexivity (doi:10.1007/s00039-004-0473-8, doi:10.1142/S1793525309000114).
• 2016. Dilworth et al. define AMUC and construct an AMUC norm on $\ell_2$ that is not AUC (doi:10.1016/j.jmaa.2015.11.061).
• 2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang show that an equivalent AMUC norm prevents uniform embeddings of the countably branching diamonds, and that for reflexive spaces with unconditional asymptotic structure, failure of AUC renormability forces uniform diamond embeddings (arXiv:1612.01984).
• 2018 and 2021. Swift extends the embedding construction to countably branching bundle graphs under the same hypotheses (arXiv:1710.00877); Perreau treats duals of separable spaces with weak-star unconditional asymptotic structure (arXiv:2104.10494).
• 2025. Baudier and Lancien record, as Problem 39 of their monograph, whether the diamond implication holds for general reflexive spaces (arXiv:2512.00817).
• 2026. Baudier shows that AMUC renormability does not imply AUC renormability, using the Kadets–Werner modification of the Bourgain–Rosenthal space, which is not reflexive (arXiv:2609.21283).

The source of this mission, an OpenAI preprint dated September 27, 2026, gives a reflexive example that separates the two notions and answers the reflexive diamond question negatively.

Setting

All spaces are real. For a Banach space $Y$ with norm $N$, let $\operatorname{cof}(Y)$ be the closed subspaces of finite codimension. For $t>0$,

$$\overline\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\bigl(N(x+ty)-1\bigr),$$ $$\widehat\delta_N(t)=\inf_{N(x)=1}\ \sup_{F\in\operatorname{cof}(Y)}\ \inf_{y\in F,\ N(y)=1}\Bigl(\tfrac{N(x+ty)+N(x-ty)}{2}-1\Bigr).$$

$N$ is AUC if $\overline\delta_N(t)>0$ for every $t>0$, and AMUC if $\widehat\delta_N(t)>0$ for every $t>0$. A norm $N$ is equivalent to $\|\cdot\|$ if $a\|x\|\le N(x)\le b\|x\|$ for some $0<a\le b$.

The forest. For $h\ge1$ let $T_h=\mathbb N^{\le h}$ be the rooted tree of words of length at most $h$, ordered by extension. The forest $\mathcal F$ is the disjoint union of one copy of $T_h$ for every $h\ge1$. A segment is an interval $[a,b]$ of an ancestral chain. For a finitely supported $u:\mathcal F\to\mathbb R$,

$$\rho(u)=\sup\Bigl\{\Bigl(\sum_{i=1}^m u(S_i)^2\Bigr)^{1/2} : S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\},\qquad u(S)=\sum_{v\in S}u(v).$$

Let $J$ be the completion and $X=J^*$ with the dual norm.

Diamonds. $D_0$ is one edge; $D_{k+1}$ replaces every edge of $D_k$ by countably many internally disjoint two-edge paths. With the shortest-path metric $d_k$, a map $f:D_k\to X$ has distortion at most $C$ if some scale $s>0$ gives $s\,d_k(u,v)\le\|f(u)-f(v)\|\le Cs\,d_k(u,v)$ for all $u,v$.

Formalization targets

Goal: Theorem 1.1

$$X\ \text{is infinite dimensional, separable and reflexive, and admits no equivalent AUC norm;}$$ $$\widehat\delta_X(t)\ \ge\ \sqrt{1+t^2/12}-1\quad(t>0);$$ $$\text{every embedding of }D_k\text{ into }X\text{ has distortion}\ \ge\ \sqrt{1+k/12}\quad(k\ge0).$$

The Lean statement OAI.ForestSpace.main_theorem is the conjunction of these six clauses. It is open on the platform.

Significance

The theorem separates AMUC from AUC renormability inside the reflexive class, which Baudier's 2026 example (non-reflexive) does not. Because AMUC is a property of the given norm while the diamond obstruction is invariant under renorming, the theorem also shows that, for general reflexive spaces, failure of AUC renormability does not force the countably branching diamonds to embed uniformly. This answers Problem 39 of Baudier–Lancien negatively and shows that the unconditional asymptotic structure hypothesis in the 2017 embedding theorem cannot simply be dropped. The quantitative modulus and distortion bounds are explicit, not merely positivity statements.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. A formal proof would certify the full construction, including reflexivity of $J^*$ for a non-locally-finite forest and the square-sum distortion recursion.

Difficulty

Two points are delicate. First, reflexivity: the classical James tree space is not reflexive, and here reflexivity comes from using trees of finite but unbounded height together with countable branching; the full dual $J^*$, not the coordinate completion, is the space. Second, the midpoint estimate: a segment test may cross from a finite ancestral set to its complement, and simply adding norming tests for the two parts produces uncontrolled positive cross terms. Non-renormability, by contrast, must be proved for every equivalent norm at once, so it cannot be read off from any computation with the given norm.

Formalization scope

• The space is FullDual Vertex := StrongDual ℝ (J Vertex), where J V is the UniformSpace.Completion of TestVector V (finitely supported functions with norm rho). Vertex packs a height $h\ge1$ and a word in $\mathbb N^*$ of length $\le h$; the order is equality of heights plus prefix order.
• Segments are finite order-convex chains (IsSegment); the empty segment is allowed and contributes zero.
• Reflexive is surjectivity of the canonical map NormedSpace.inclusionInDoubleDual, not an abstract isomorphism with the bidual.
• EquivalentNorm E α β stores a Seminorm with explicit constants $0<\alpha\le\beta$; the lower bound makes it a norm. The non-renormability clause quantifies over all such structures.
• aucModulus and averageModulus take the inf/sup/inf order above, with sInf/sSup over real sets; for an infinite-dimensional space these sets are nonempty and bounded, so the Lean defaults are not triggered.
• Diamond.diamond k iterates the edge replacement starting from one edge; distances are SimpleGraph.dist of the undirected graph, and EmbeddingBound is the scaled bi-Lipschitz condition above.

A complete development needs the James-type segment norm, its completion and dual, coordinate projections onto ancestral sets, and graph distances on the diamonds. The segment-norm and diamond infrastructure is shared with the other missions of this family. Contributions formalizing Lemma 2.1 (structure and reflexivity), Lemma 3.2 (bounded trees exclude AUC renorming), Lemma 4.1 (paired head–tail estimate) and Lemma 5.1 (lens lemma) are welcome.

Selected references

• OpenAI, Asymptotic midpoint uniform convexity and unbounded diamond distortion in a reflexive tree space, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Asymptotic-midpoint-uniform-convexity-and-unbounded-diamond-distortion-in-a-reflexive-tree-space-September-27-2026/manuscript.pdf
• S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
• F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
• F. P. Baudier, G. Lancien, Asymptotic and nonlinear geometries of Banach spaces and their interactions, Cours Spécialisés, SMF, 2026. https://arxiv.org/abs/2512.00817
• F. P. Baudier, The Kadets–Werner modification of Bourgain–Rosenthal space is asymptotically midpoint uniformly convex, preprint, 2026. https://arxiv.org/abs/2609.21283
• R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
• M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2
• A. Swift, A coding of bundle graphs and their embeddings into Banach spaces, Mathematika, 2018. https://arxiv.org/abs/1710.00877
• Y. Perreau, On the embeddability of countably branching bundle graphs into dual spaces, preprint, 2021. https://arxiv.org/abs/2104.10494

Motivation

Free probability treats bounded self-adjoint operators $X_1,\dots,X_n$ in a tracial von Neumann algebra as noncommuting random variables, and the free analogue of independence is freeness. Voiculescu introduced two candidate analogues of Shannon entropy for such tuples. The microstates free entropy $\chi(X)$ measures how large the set of matrix tuples imitating the joint moments of $X$ is (Voiculescu 1994). The nonmicrostates free entropy $\chi^*(X)$ is built instead from free Fisher information, by integrating along the addition of free semicircular noise (Voiculescu 1998). The two agree for a single variable, and whether they agree in general is part of Voiculescu's unification problem (Voiculescu 2002, Sections 3.5 and 3.8). Guionnet stated the finite-entropy formulation explicitly: does $\chi(X)>-\infty$ imply $\chi(X)=\chi^*(X)$? (Guionnet 2004, Conjecture 7.1).

The question matters because $\chi$ carries the strongest structural consequences for von Neumann algebras (it is the tool behind results such as Ge's theorem that free group factors are prime, Ge 1996), while $\chi^*$ is far more computable. Equality would let analytic computations of $\chi^*$ transfer to $\chi$.

This mission asks for a machine-checked proof of Theorem 1.1 of an OpenAI preprint dated September 25, 2026 (source), which claims a tuple with $-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty$. The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 1991 — Voiculescu proves asymptotic freeness of independent GUE matrices (Invent. Math. 1991), the random-matrix input behind microstates.
• 1994 — Voiculescu defines the microstates free entropy $\chi$ (Invent. Math. 1994); Speicher develops the noncrossing cumulant calculus (Math. Ann. 1994).
• 1996 — Ge uses microstates entropy to prove that $L(F_2)$ is prime (PNAS 1996).
• 1998 — Voiculescu defines free Fisher information via conjugate variables and the nonmicrostates entropy $\chi^*$ (Invent. Math. 1998).
• 2002–2004 — Voiculescu's survey lists the unification problem (Bull. LMS 2002); Guionnet states the finite-entropy equality conjecture (Probab. Surv. 2004).
• 2003 — Biane, Capitaine and Guionnet prove $\chi\le\chi^*$ in general (Invent. Math. 2003).
• 2017–2020 — Equality is established for regular convex potentials by Dabrowski (arXiv:1604.06420) and Jekel (Anal. PDE 2020).
• 2024 — Jekel and Pi give an elementary proof of $\chi\le\chi^*$, including the conditional version (Doc. Math. 2024).
• 2026 — The OpenAI preprint claims a strict gap with both entropies finite (Theorem 1.1, p. 2).

Setting

Let $M$ be a von Neumann algebra with a faithful normal tracial state $\tau$, and $X=(X_1,\dots,X_n)$ a tuple of self-adjoint elements of $M$.

Microstates. For $R>0$, $m\in\mathbb N$, $\varepsilon>0$ and a matrix size $d$, let $\Gamma_R(X;m,d,\varepsilon)$ be the set of $n$-tuples of self-adjoint $d\times d$ complex matrices with operator norms at most $R$ whose normalized traces $d^{-1}\mathrm{Tr}$ of all words of length $\le m$ are within $\varepsilon$ of the corresponding $\tau$-moments of $X$. Volume is Lebesgue measure for the unnormalized Hilbert–Schmidt inner product. Then

$$\chi_R(X)=\inf_{m,\varepsilon}\ \limsup_{d\to\infty}\Bigl[d^{-2}\log\mathrm{Vol}\,\Gamma_R(X;m,d,\varepsilon)+\tfrac n2\log d\Bigr],\qquad \chi(X)=\sup_{R>0}\chi_R(X).$$

Free Fisher information. Vectors $\xi_1,\dots,\xi_n$ in the $L^2(\tau)$-closure of polynomials in $X$ are conjugate variables if $\tau(\xi_i P(X))=(\tau\otimes\tau)((\partial_iP)(X))$ for every noncommutative polynomial $P$, where $\partial_i$ is the free difference quotient. Then $\Phi^*(X)=\sum_i\|\xi_i\|_2^2$, or $+\infty$ if no conjugate variables exist.

Nonmicrostates entropy. With $S=(S_1,\dots,S_n)$ a standard free semicircular family free from $X$,

$$\chi^*(X)=\frac n2\log(2\pi e)+\frac12\int_0^\infty\Bigl(\frac n{1+s}-\Phi^*(X+\sqrt s\,S)\Bigr)\,ds .$$

Formalization targets

Goal: Theorem 1.1 (p. 2)

There exist $n\ge2$ and a bounded self-adjoint tuple $X$ in a von Neumann algebra with faithful normal tracial state such that

$$-\infty<\chi(X)\le\chi^*(X)-\tfrac12<\infty .$$

The Lean goal OAI.FiniteEntropySeparation.main asserts exactly this, with the semicircular family $S$ required to lie in the same algebra.

Significance

The result itself. The theorem answers the finite-entropy equality question negatively: finiteness of $\chi$ does not force $\chi=\chi^*$, so the matrix-approximation and Fisher-information definitions are genuinely different invariants even in the finite regime. Known equality results therefore cannot be extended by finiteness alone; any equality theorem must use structure such as convexity of a potential. The preprint notes that it does not settle the question for each fixed small number of variables.

Formalizing it. No formal definitions of free entropy, free Fisher information or free semicircular systems are known to exist in a proof assistant. A complete development would formalize both entropies, the comparison $\chi\le\chi^*$ in the form needed, Gaussian asymptotic freeness, cumulant calculus and matrix-volume estimates, all reusable across free probability.

Difficulty

Both entropies are hard to compute for any non-free tuple, and the gap must survive two limits that interact badly: the $\limsup$ over matrix size in $\chi$ and the integral over noise time in $\chi^*$. The preprint's tuple couples free semicirculars with a commuting discrete variable $Y$ that creates spectral blocks; after perturbing by small semicircular noise, $\chi$ is finite (Lemma 4.2, p. 9). The analytic side needs a Fisher-information bound in terms of higher cumulants (Proposition 3.2, p. 6), which makes $\chi^*$ nearly Gaussian at a suitable noise scale, while the matrix side must show that microstates, after GUE evolution, retain detectable block structure that independent GUE matrices of the same variances lack (Lemma 6.1, p. 12). Matching the two requires a finite-time entropy-production comparison along one fixed sequence of matrix laws (Lemma 5.1, p. 10); a naive application of $\chi\le\chi^*$ loses exactly the deficit being sought.

Formalization scope

• The algebra is a VonNeumannAlgebra H on a complex Hilbert space $H$; the trace is a vector state given by a unit vector that is tracial on $M$ and separating for $M$ (so the state is faithful and normal).
• $X$ and $S$ are Fin n-indexed self-adjoint elements of $M$. FreeStandardNoise requires each $S_i$ to have the semicircle moments (Catalan numbers) and the unital algebras generated by $X$ and by each $S_i$ to be free.
• Conjugate systems are vectors in the closed span of word vectors satisfying the derivative-moment identities; free Fisher information is an infimum in ℝ≥0∞, equal to $\infty$ when no conjugate system exists.
• $\chi^*$ is an EReal built from the positive and negative parts of the integrand as lower Lebesgue integrals over $(0,\infty)$.
• $\chi$ uses explicit real coordinates for Hermitian matrices that make the Euclidean volume equal to Hilbert–Schmidt volume, matrix sizes $d+1$ to avoid $d=0$, and EReal logarithms (volume zero gives $-\infty$).
• The finiteness conditions are part of the conclusion, so a degenerate witness with $\chi=-\infty$ or $\chi^*=\infty$ does not satisfy the goal.

Selected references

• OpenAI, A finite-entropy separation of microstates and nonmicrostates free entropy, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-finite-entropy-separation-of-microstates-and-nonmicrostates-free-entropy-September-25-2026/paper.pdf
• D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. II, Invent. Math. 118 (1994), 411–440. https://doi.org/10.1007/BF01231539
• D. Voiculescu, The analogues of entropy and of Fisher's information measure in free probability theory. V, Invent. Math. 132 (1998), 189–227. https://doi.org/10.1007/s002220050222
• D. Voiculescu, Free entropy, Bull. London Math. Soc. 34 (2002), 257–278. https://doi.org/10.1112/S0024609301008992
• A. Guionnet, Large deviations and stochastic calculus for large random matrices, Probab. Surv. 1 (2004), 72–172. https://doi.org/10.1214/154957804100000033
• P. Biane, M. Capitaine, A. Guionnet, Large deviation bounds for matrix Brownian motion, Invent. Math. 152 (2003), 433–459. https://doi.org/10.1007/s00222-002-0281-4
• D. Jekel, J. Pi, An elementary proof of the inequality χ ≤ χ for conditional free entropy*, Doc. Math. 29 (2024), 1085–1124. https://doi.org/10.4171/DM/969
• D. Jekel, An elementary approach to free entropy theory for convex potentials, Anal. PDE 13 (2020), 2289–2374. https://doi.org/10.2140/apde.2020.13.2289
• D. Voiculescu, Limit laws for random matrices and free products, Invent. Math. 104 (1991), 201–220. https://doi.org/10.1007/BF01245072

Motivation

A closed subspace $\mathcal M$ of a Hilbert space $H$ is hyperinvariant for a bounded operator $S$ if $A\mathcal M\subseteq\mathcal M$ for every operator $A$ commuting with $S$. The hyperinvariant subspace problem asks whether every bounded nonscalar operator on an infinite-dimensional separable complex Hilbert space has a nonzero proper closed hyperinvariant subspace. It is a strengthening of the invariant subspace problem, closely tied to the theory of transitive operator algebras: $S$ has no such subspace exactly when its commutant $\{S\}'$ is transitive. A related classical question asks whether every unital transitive operator algebra is strongly dense in $B(H)$; Arveson's density theorem gives a positive answer when the algebra contains a maximal abelian self-adjoint subalgebra.

Timeline

• 1967. Arveson proves that a transitive algebra containing a maximal abelian self-adjoint subalgebra is strongly dense in $B(H)$ (doi:10.1215/S0012-7094-67-03467-9).
• 1972. Douglas and Pearcy relate hyperinvariant subspaces to transitive algebras (doi:10.1307/mmj/1029000793).
• 1981–1982. Domar describes translation-invariant subspaces of weighted $\ell^p$ and $L^p$ spaces (doi:10.7146/math.scand.a-11926); Grabiner studies unicellular shifts.
• 1999. Atzmon and Sodin construct completely indecomposable bilateral weighted shifts with spectrum the unit circle, leaving open whether they have proper hyperinvariant subspaces (doi:10.1006/jfan.1999.3454).
• 2005. Dykema observes that hyperinvariant subspaces of an operator in a von Neumann algebra have projections in that algebra (doi:10.1007/s00208-005-0669-8).
• 2025–2026. A preprint of Kérchy and Pearcy claiming an equivalence between the invariant and hyperinvariant problems is withdrawn after a counterexample to its Theorem 3 (arXiv:2503.13005); Kérchy studies hyperinvariant subspaces of operators containing unilateral shifts (doi:10.1007/s11785-026-02038-9).

The source of this mission is an OpenAI preprint dated September 27, 2026. A companion OpenAI preprint of the same date reaches the same existence conclusion through invariant projections in an irrational-rotation factor, by a different construction.

Setting

Let $H$ be a complex Hilbert space and $B(H)$ its bounded operators. For $S\in B(H)$:

• the commutant is $\{S\}'=\{A\in B(H):AS=SA\}$, a unital subalgebra of $B(H)$;
• $\{S\}'$ is transitive if the only closed subspaces $\mathcal M$ with $A\mathcal M\subseteq\mathcal M$ for all $A\in\{S\}'$ are $\{0\}$ and $H$;
• $S$ is norm-quasinilpotent if $\|S^n\|^{1/n}\to0$;
• the strong operator topology on $B(H)$ is the topology of pointwise norm convergence: $A_\lambda\to A$ iff $A_\lambda x\to Ax$ for every $x\in H$.

Formalization targets

Goal: Corollary 1.2

For every infinite-dimensional separable complex Hilbert space $H$ there is $S\in B(H)$ with

$$S\neq0,\qquad \lim_{n\to\infty}\|S^n\|^{1/n}=0,\qquad \{S\}'\ \text{transitive},\qquad \{S\}'\neq B(H),\qquad \{S\}'\ \text{strongly closed}.$$

The Lean statement OAI.BackwardIntertwiners.direct_algebra_corollary is open on the platform. The family statement OAI.Hyperinvariant.main_theorem asserts the same proposition and is included as a reference item.

Significance

Corollary 1.2 gives a negative answer to the hyperinvariant subspace problem on every separable infinite-dimensional Hilbert space, and its commutant is a proper, strongly closed, unital transitive algebra, so it also answers negatively whether every unital transitive operator algebra is strongly dense in $B(H)$. The construction behind it (Theorem 1.1) is explicit: a weighted shift over the 2-adic odometer whose fibres have only coordinate-tail invariant subspaces, an explicit bound $\|S^n\|\le\exp(-10\lfloor(n+1)^2/4\rfloor)$, and a bounded commuting operator moving those tails backward. The operator does have many ordinary invariant subspaces, so the invariant subspace problem itself is untouched.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

Weighted shifts have rich lattices of invariant subspaces, so one must first pin down the invariant subspaces of each fibre (a quadratic weighted-translation criterion in the style of Domar) and then find enough operators in the commutant to destroy every candidate. Multiplication operators and the shift alone leave every fixed tail $L^2(X;K_{\ge h})$ invariant. The essential step is a bounded operator commuting with $S$ that moves tails backward across fibres; this requires opposite logarithmic drifts of the weights at the two ends of the bilateral sequence and one measurable normalization valid on the whole base. Arveson's theorem cannot be used, since the multiplier algebra has infinite multiplicity and is not maximal abelian.

Formalization scope

• H is any type with [InnerProductSpace ℂ H] [CompleteSpace H] [SeparableSpace H] and ¬FiniteDimensional ℂ H; the claim is existential in T : H →L[ℂ] H.
• commutant T is Subalgebra.centralizer ℂ {T}; TransitiveCommutant T quantifies over closed Submodules invariant under every A with A * T = T * A.
• Quasinilpotence is Tendsto (fun n => ‖T ^ n‖ ^ (1 / n)) atTop (𝓝 0) (the $n=0$ term is irrelevant to the limit).
• The strong operator topology is TopologicalSpace.induced from the pointwise (product) topology on functions H → H.

A complete development needs vector-valued $L^2$ spaces over the 2-adic integers with Haar measure, weighted shifts and their invariant subspaces, measurable fields of projections, and transport to an arbitrary separable Hilbert space by a unitary. Contributions formalizing Theorem 1.1 (the construction), Lemma 2.1 (weighted translation criterion), Proposition 4.3 (a bounded backward intertwiner) and Lemma 5.1 (strict descent) are welcome.

Selected references

• OpenAI, Backward intertwiners and a transitive commutant, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Backward-intertwiners-and-a-transitive-commutant-September-27-2026/paper.pdf
• OpenAI, Invariant-projection counterexamples for every irrational rotation, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Invariant-projection-counterexamples-for-every-irrational-rotation-September-27-2026/paper.pdf
• W. B. Arveson, A density theorem for operator algebras, Duke Math. J., 1967. https://doi.org/10.1215/S0012-7094-67-03467-9
• R. G. Douglas, C. Pearcy, Hyperinvariant subspaces and transitive algebras, Michigan Math. J., 1972. https://doi.org/10.1307/mmj/1029000793
• Y. Domar, Translation invariant subspaces of weighted $l^p$ and $L^p$ spaces, Math. Scand., 1981. https://doi.org/10.7146/math.scand.a-11926
• A. Atzmon, M. Sodin, Completely indecomposable operators and a uniqueness theorem of Cartwright–Levinson type, J. Funct. Anal., 1999. https://doi.org/10.1006/jfan.1999.3454
• K. Dykema, Hyperinvariant subspaces for some B-circular operators, Math. Ann., 2005. https://doi.org/10.1007/s00208-005-0669-8
• L. Kérchy, C. Pearcy, Hyperinvariant subspaces of block-triangular operators on Hilbert space, withdrawn preprint, 2025. https://arxiv.org/abs/2503.13005

Motivation

A representation $\pi$ of a group $G$ by bounded invertible operators on a Hilbert space is uniformly bounded if $\sup_g\|\pi(g)\|<\infty$, and unitarizable if after a change of inner product it becomes unitary, i.e. some bounded invertible $S$ makes every $S\pi(g)S^{-1}$ unitary. Unitary representations are the ones harmonic analysis knows how to decompose, so it matters which groups have only unitarizable uniformly bounded representations. Day and Dixmier showed in 1950 that every amenable group (one with an invariant mean) has this property, and Dixmier asked whether the converse holds. Dixmier's unitarizability problem has driven work in operator algebras, $\ell^2$-invariants and measured group theory for seven decades.

Timeline

• 1947. Sz.-Nagy proves that an invertible operator with uniformly bounded powers is similar to a unitary.
• 1950. Day and Dixmier prove that amenable groups are unitarizable; Dixmier asks whether the converse holds (doi:10.2307/1990358).
• 1955. Ehrenpreis and Mautner give nonunitarizable uniformly bounded representations of $\mathrm{SL}_2(\mathbb R)$ (doi:10.1073/pnas.41.4.231); Følner gives his finite-set criterion for amenability (doi:10.7146/math.scand.a-10442).
• 1986. Pytlik and Szwarc construct explicit nonunitarizable families for free groups, settling all groups containing $F_2$ (doi:10.1007/BF02392596).
• 1998. Pisier characterizes amenability by a quantitative similarity bound with exponent $<3$ (The similarity degree of an operator algebra, Algebra i Analiz, 1998).
• 2009. Epstein and Monod use invariant random forests to prove nonunitarizability for residually finite groups with positive first $\ell^2$-Betti number (doi:10.1093/imrn/rnp090); Osin obtains nonunitarizable groups without free subgroups.
• 2010. Monod and Ozawa prove that the wreath products $A\wr G$ with $A$ infinite abelian are unitarizable exactly when $G$ is amenable (doi:10.1016/j.jfa.2009.06.029), using the Gaboriau–Lyons theorem (doi:10.1007/s00222-009-0187-5).
• 2018–2025. Gerasimova, Gruber, Monod and Thom relate unitarizability to Cheeger constants (doi:10.1016/j.jfa.2019.108457); Alpeev and Vergara obtain further cases.

The source of this mission, an OpenAI preprint dated September 23, 2026, answers Dixmier's question affirmatively for all discrete groups.

Setting

Let $G$ be a discrete group. $G$ is amenable if there is a linear functional $m$ on the bounded functions $G\to\mathbb C$ with $m(1)=1$, $m(f)\ge0$ for $f\ge0$, and $m(L_gf)=m(f)$, where $(L_gf)(x)=f(g^{-1}x)$.

A representation is a homomorphism $\pi:G\to\mathcal B(\mathcal K)$ into bounded operators on a complex Hilbert space $\mathcal K$ (each $\pi(g)$ is then invertible). It is similar to a unitary representation if there is a bounded invertible $S$ with $S\pi(g)S^{-1}$ unitary for every $g$. $G$ is unitarizable if every uniformly bounded representation on every complex Hilbert space is similar to a unitary representation; the similarity may depend on the representation.

Formalization targets

Milestone: countable case

Every countable nonamenable $G$ has a representation on a separable Hilbert space with $\sup_g\|\pi(g)\|\le101$ that is not similar to a unitary representation.

Goal: Theorem 1.1

$$G\ \text{amenable}\iff G\ \text{unitarizable},$$

and for nonamenable $G$ and every $\varepsilon>0$ there is $\pi$ with $\sup_g\|\pi(g)\|\le1+\varepsilon$ not similar to a unitary representation, on a separable space when $G$ is countable. The Lean statement OAI.Dixmier.current_main_theorem is open on the platform.

Significance

Theorem 1.1 characterizes amenability of discrete groups by a purely Hilbert-space property, without any quantitative bound on similarities, and shows that nonunitarizable representations can be chosen with uniform bound arbitrarily close to $1$. Earlier results produced witnesses for groups with free subgroups, for residually finite groups with positive $\ell^2$-Betti number, or for wreath-product extensions of $G$; the theorem gives a witness for every nonamenable $G$ itself. The paper also derives a consequence for group C$^*$-algebras using a companion similarity result.

The result is proved in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists. The amenable direction (Day–Dixmier averaging) is classical and a natural first formalization step; the converse needs the paper's new operator construction.

Difficulty

A witness must be one representation for which no similarity exists, with no a priori control of the condition number of a putative unitarizer; quantitative criteria such as Pisier's do not apply. Nonamenable groups need not contain free subgroups and need not be residually finite, so the earlier free-group, random-forest and $\ell^2$-Betti routes do not cover them. The paper builds bounded operator cocycles with no bounded implementer, which requires operators whose conjugation differences under translation are uniformly bounded while their distance from the translation commutant tends to infinity.

Formalization scope

• Amenability is stated for G with the discrete topology, using G →ᵇ ℂ for $\ell^\infty(G)$; positivity is required on functions with nonnegative real values.
• Representations are monoid homomorphisms G →* (H →L[ℂ] H) with [InnerProductSpace ℂ H] [CompleteSpace H]; SimilarToUnitary π asks for S : H ≃L[ℂ] H with $\|S\pi(g)S^{-1}x\|=\|x\|$ for all $g,x$.
• Unitarizability quantifies over Hilbert spaces in universe max u v, and the witness is built there; since the theorem holds for every v, this covers all Hilbert spaces.
• Separability of the witness is required only for countable G, as in the paper.

A complete development needs bounded operator cocycles and triangular representations, Hilbert direct sums, Hilbert–Schmidt estimates, Følner's criterion, induction of representations from subgroups, and invariant means. Contributions formalizing the Day–Dixmier direction, Proposition 2.2 (direct-sum obstruction) and Lemma 5.1 (induction from a subgroup) are welcome.

Selected references

• OpenAI, Unitarizability implies amenability for discrete groups, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Unitarizability-Implies-Amenability-for-Countable-Groups-September-23-2026/paper.pdf
• M. M. Day, Means for the bounded functions and ergodicity of the bounded representations of semi-groups, Trans. Amer. Math. Soc., 1950. https://doi.org/10.2307/1990358
• J. Dixmier, Les moyennes invariantes dans les semi-groupes et leurs applications, Acta Sci. Math. (Szeged), 1950.
• G. Pisier, Are unitarizable groups amenable?, preprint, 2004. https://arxiv.org/abs/math/0405282
• I. Epstein, N. Monod, Nonunitarizable representations and random forests, IMRN, 2009. https://doi.org/10.1093/imrn/rnp090
• N. Monod, N. Ozawa, The Dixmier problem, lamplighters and Burnside groups, J. Funct. Anal., 2010. https://doi.org/10.1016/j.jfa.2009.06.029
• D. Gaboriau, R. Lyons, A measurable-group-theoretic solution to von Neumann's problem, Invent. Math., 2009. https://doi.org/10.1007/s00222-009-0187-5
• T. Pytlik, R. Szwarc, An analytic family of uniformly bounded representations of free groups, Acta Math., 1986. https://doi.org/10.1007/BF02392596
• M. Gerasimova, D. Gruber, N. Monod, A. Thom, Asymptotics of Cheeger constants and unitarisability of groups, J. Funct. Anal., 2020. https://doi.org/10.1016/j.jfa.2019.108457

Motivation

Thompson's group $F$ consists of the increasing piecewise linear homeomorphisms of $[0,1]$ with finitely many pieces, dyadic rational breakpoints, and slopes that are integer powers of $2$. It is finitely presented, has strong topological finiteness properties, and appears across group theory, dynamics and logic. Whether $F$ is amenable, i.e. whether its bounded functions admit a translation-invariant mean, is one of the best-known open questions about a single explicit group. It is a natural test case because the two classical routes to deciding amenability both fail: $F$ contains no nonabelian free subgroup (Brin–Squier 1985), so the free-subgroup obstruction is unavailable, yet $F$ is not elementary amenable (Cannon–Floyd–Parry 1996, Theorem 4.10). Geoghegan conjectured in 1979 that $F$ is nonamenable. The problem has attracted claimed resolutions in both directions, several later withdrawn or found to contain errors.

This mission asks for a formal proof of nonamenability as stated in an OpenAI preprint dated September 23, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1929–1957 — Von Neumann and Day develop invariant means and amenability (Fund. Math. 1929; Illinois J. Math. 1957); Følner's criterion (Math. Scand. 1955).
• 1965–1973 — Thompson introduces $F$; an early published construction is McKenzie–Thompson (1973).
• 1979 — Geoghegan conjectures that $F$ is nonamenable (recorded in Cannon–Floyd–Parry 1996, p. 227).
• 1984–1985 — Brown and Geoghegan: $F$ is $\mathrm{FP}_\infty$ (Invent. Math. 1984); Brin and Squier: no nonabelian free subgroups (Invent. Math. 1985).
• 2009–2013 — Shavgulidze's amenability claim (arXiv:0906.0107) and Moore's identification of its errors (arXiv:1102.0747); Moore's tower lower bounds for Følner functions (GGD 2013) and Ramsey characterization of amenability (Fund. Math. 2013); Moore's later amenability manuscript is withdrawn (arXiv:1209.2063).
• 2017 — Haagerup and Olesen: $C^*$-simplicity of $T$ would imply nonamenability of $F$ (JFA 2017).
• 2021–2026 — Akhmedov's nonamenability claim via height functions (arXiv:1310.4395v3); Guba's density estimates (J. Comb. Algebra 2025; J. Algebra 2026).

Setting

A homeomorphism $f$ of $[0,1]$ is a dyadic PL map if there are dyadic rationals $0=x_0<x_1<\dots<x_k=1$ and integers $e_i$ such that on each $[x_{i-1},x_i]$, $f(x)=f(x_{i-1})+2^{e_i}(x-x_{i-1})$. The group $F$ is the set of increasing dyadic PL homeomorphisms of $[0,1]$, with multiplication $hg=h\circ g$, regarded as a discrete group. Let $\ell^\infty(F;\mathbb R)$ be the bounded real functions on $F$. A left-invariant mean is a linear functional $M:\ell^\infty(F;\mathbb R)\to\mathbb R$ with $M(\mathbf 1)=1$, $M(\varphi)\ge0$ whenever $\varphi\ge0$, and $M(g\mapsto\varphi(hg))=M(\varphi)$ for every $h\in F$. $F$ is amenable if such a mean exists.

Formalization targets

Goal: Theorem 1.1 (p. 1)

Thompson's group $F$ is not amenable: there is no positive, normalized, left-invariant mean on $\ell^\infty(F;\mathbb R)$.

Significance

The result itself. It settles Geoghegan's conjecture and the amenability problem for $F$. Because $F$ has no free subgroups, $F$ becomes a finitely presented, torsion-free example of a nonamenable group without free subgroups. Through companion results the preprint derives that $F$ has uniformly bounded representations that are not unitarizable (Corollary 3.1, p. 7) and that Bernoulli percolation on every Cayley graph of $F$ has a nonuniqueness phase (Corollary 3.2, p. 8). The proof is short (Section 2) and uses an infinite-dimensional fixed-point phenomenon: the Benyamini–Sternfeld theorem that the unit ball of an infinite-dimensional Hilbert space admits a Lipschitz self-map moving every point by at least a fixed $\delta>0$ (Lemma 1.2, p. 2; Proc. AMS 1983).

Formalizing it. Given the length of the published argument, this is a realistic target for a complete formal proof of a result that had been open for over forty years. It needs the dyadic-partition model of $F$, the Følner criterion (forward direction), and a Lipschitz map on a Hilbert ball with no approximate fixed points (Appendix A of the preprint constructs one on $L^2([0,1];\mathbb R^2)$ with $\delta=1/2$). The Følner direction from invariant means to Følner sets is reusable infrastructure for amenability in Mathlib.

Difficulty

Neither standard obstruction applies: there is no free subgroup to produce a paradoxical decomposition, and no structural closure property shows amenability. Følner sets, if they existed, would have to grow extremely fast (Moore's tower bounds), so explicit counting is ineffective. The preprint's argument converts approximate invariance of a finite set $A\subset F$ into an approximate fixed point of a Lipschitz map on a Hilbert ball, via recursively defined Hilbert-valued colours of dyadic partitions. The delicate points are exact covariance of normalized restrictions under the group action (equation (2.2), p. 4) and controlling the diagonal and nested pairs in the correlation expansion, which yields a uniform lower bound on the relative boundary of every finite set (Proposition 2.3, p. 5).

Formalization scope

• UnitInterval is Set.Icc (0:ℝ) 1; an element of F is a homeomorphism of it that is StrictMono and has a DyadicPLWitness: finitely many strictly increasing dyadic knots from $0$ to $1$ and integer exponents with the affine formula on each piece.
• The goal asserts that some group structure on F exists whose multiplication is composition ((h * g) x = h (g x)); since multiplication is fixed, this structure is unique.
• InvariantMean F is a real-linear functional on lp (fun _ : F => ℝ) ∞ that is positive, sends the constant $1$ to $1$, and is invariant under leftPull h, $\varphi\mapsto(g\mapsto\varphi(hg))$; the goal is ¬ Nonempty (InvariantMean F).
• No generating set, Følner constant or boundary bound is fixed in the statement, so the goal is stable under improved constants.

Selected references

• OpenAI, Thompson's group F is nonamenable, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Thompsons-group-F-is-nonamenable-September-23-2026/paper.pdf
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, Enseign. Math. (2) 42 (1996), 215–256. https://www.imo.universite-paris-saclay.fr/~emmanuel.breuillard/Cannon.pdf
• M. G. Brin, C. C. Squier, Groups of piecewise linear homeomorphisms of the real line, Invent. Math. 79 (1985), 485–498. https://doi.org/10.1007/BF01388519
• K. S. Brown, R. Geoghegan, An infinite-dimensional torsion-free $\mathrm{FP}_\infty$ group, Invent. Math. 77 (1984), 367–381. https://doi.org/10.1007/BF01388451
• Y. Benyamini, Y. Sternfeld, Spheres in infinite-dimensional normed spaces are Lipschitz contractible, Proc. Amer. Math. Soc. 88 (1983), 439–445. https://doi.org/10.1090/S0002-9939-1983-0699410-7
• E. Følner, On groups with full Banach mean value, Math. Scand. 3 (1955), 243–254. https://doi.org/10.7146/math.scand.a-10442
• J. T. Moore, Amenability and Ramsey theory, Fund. Math. 220 (2013), 263–280. https://doi.org/10.4064/fm220-3-6
• J. T. Moore, Fast growth in the Følner function for Thompson's group F, Groups Geom. Dyn. 7 (2013), 633–651. https://doi.org/10.4171/GGD/201
• U. Haagerup, K. K. Olesen, Non-inner amenability of the Thompson groups T and V, J. Funct. Anal. 272 (2017), 4838–4852. https://doi.org/10.1016/j.jfa.2017.02.003
• M. M. Day, Amenable semigroups, Illinois J. Math. 1 (1957), 509–544. https://doi.org/10.1215/ijm/1255380675

Motivation

Edit distance $\mathrm{ED}(x,y)$, the least number of single-symbol insertions, deletions and substitutions turning $x$ into $y$, is the standard distance on strings. Embedding strings into $\ell_1$ with small distortion would make edit distance amenable to the fast nearest-neighbour and sketching tools available for $\ell_1$, so the least achievable distortion is a central quantity in metric embedding theory. A single insertion shifts every later symbol, yet cyclically shifting a word costs only two edits; this tension between position and alignment is what makes edit distance hard to embed.

This preprint gives two independent constructions of binary word sets whose least $\ell_1$ distortion is $\exp(\Omega(\sqrt{\log d\log\log d}))$, two binary coding arguments that transfer large-alphabet constructions to binary, and a complete histogram embedding attaining the matching upper scale. Together they determine the exponential scale of the distortion.

Background

• 1966, 1974. Levenshtein introduces insertion/deletion codes; Wagner and Fischer describe alignments by increasing traces.
• 1995. Linial, London and Rabinovich develop finite metric embeddings into $\ell_1$.
• 1999. Schulman and Zuckerman construct asymptotically good codes for insertions and deletions.
• 2003. Andoni, Deza, Gupta, Indyk and Raskhodnikova give binary sets with $\ell_1$ distortion approaching $3/2$.
• 2006. Khot and Naor prove a $(\log d)^{1/2 - o(1)}$ lower bound by Fourier analysis of cuts.
• 2007. Ostrovsky and Rabani prove the upper bound $\exp(O(\sqrt{\log d\log\log d}))$ for fixed-length binary strings.
• 2009. Krauthgamer and Rabani prove an $\Omega(\log d)$ lower bound.
• 2026. The OpenAI preprint Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance (dated September 27, 2026), a companion to Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, proves the results below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

For a finite alphabet $\Sigma$ with $|\Sigma| \ge 2$ and an integer $d \ge 1$, let $\Sigma^{\le d}$ be the words of length at most $d$, including the empty word. For an injective $f : \Sigma^{\le d} \to \ell_1$,

$$\mathrm{dist}(f) = \Big(\max_{x\ne y}\frac{\|f(x)-f(y)\|_1}{\mathrm{ED}(x,y)}\Big)\Big(\max_{x\ne y}\frac{\mathrm{ED}(x,y)}{\|f(x)-f(y)\|_1}\Big), \qquad E_\Sigma(d) = \inf_f \mathrm{dist}(f).$$

The longest common subsequence $\mathrm{LCS}(x,y)$ and the deficit $r_L(x,y) = L - \mathrm{LCS}(x,y)$ for words of length $L$ are used in the coding results. A binary substitution $c : \Sigma \to \{0,1\}^w$ replaces each letter by a codeword.

In Lean (OAI.FiniteCircle), editDistance is the least script length, lcs and deficit are as above, optimalDistortion is the infimum of distortion over injective maps into lp (fun _ : ℕ => ℝ) 1, E α d is the least distortion of words of length at most $d$, and maskWord, excludedWord are the two finite-circle constructions with prime-period parameters.

Formalization targets

Goal: finiteCircle_fullMain

The conjunction of the paper's main statements, with common absolute constants:

• Theorem 1.1. For $d \ge d_0$ and every finite $\Sigma$ with $|\Sigma| \ge 2$,

$$\exp\big(c\sqrt{\log d\log\log d}\big) \le E_\Sigma(d) \le \exp\big(C\sqrt{\log d\log\log d}\big),$$

and the same bounds for $\sup_{|\Sigma| \ge 2} E_\Sigma(d)$.

• Lower constructions (Sections 5–7): for each $d \ge d_0$, both the mask construction and the excluded-prime construction, encoded in binary, give a set of words of one common length $n \le d$ with least distortion at least $\exp(c\sqrt{\log d\log\log d})$.
• Theorem 4.1 (two binary substitutions): for every alphabet of $A \ge 2$ letters there are codes $c : \Sigma \to \{0,1\}^w$ with $w = O(\log 2A)$ and $a\,w\,r_L(x,y) \le r_{wL}(c(x),c(y)) \le w\,r_L(x,y)$ for equal-length words, $\mathrm{ED}(c(x),c(y)) \le w\,\mathrm{ED}(x,y)$, plus the local separation property each construction needs.
• Theorem 8.1 (uniform upper bound): a deterministic finite-dimensional map $F$ with $\mathrm{ED}(x,y) \le \|F(x)-F(y)\|_1 \le \exp(C\sqrt{\log d\log\log d})\,\mathrm{ED}(x,y)$.

Significance

The result. The lower bounds reach the Ostrovsky–Rabani scale, so the order of $\log E_\Sigma(d)$ is $\sqrt{\log d\log\log d}$; this improves the previous $\Omega(\log d)$ lower bound to $\exp(\Omega(\sqrt{\log d\log\log d}))$. The histogram embedding gives an explicit, alphabet-uniform upper bound including all shorter words.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. Unlike the companion paper, the upper bound here is proved in full (Section 8) rather than imported, so the goal is self-contained relative to the preprint. The edit-distance and distortion definitions are reusable across the edit-distance missions.

Difficulty

Lower bounds for edit distance must control every increasing matching of the two words, including matchings crossing the row boundaries used to construct them. A cheap translation of phases moves row lists at low edit cost, while a simultaneous half-turn at every leaf must be expensive; proving the latter for arbitrary alignments, and then showing that every $\ell_1$ image must distort one of these comparisons, requires combining a combinatorial separation estimate with a Fourier argument on the finite phase space that forces large total frequency.

Formalization scope

• Words are List α with Fintype α; the domain $\Sigma^{\le d}$ is a subtype by length; the empty word is included.
• distortion uses sSup over finite sets of ratios; optimalDistortion is sInf over injective maps into $\ell_1(\mathbb N)$; exponentScale d = sqrt(log d · log log d) with natural logarithms.
• The lower witnesses fix the paper's constructions (prime assignments MaskPrimes, ExcludedPrimes, depth parameters) and require a common positive length $n \le d$.
• UniformUpper asks for a map into Fin M → ℝ with the $\ell_1$ norm written as a finite sum.

The goal is not vacuous: a set with one element would have least distortion $0$, so witnesses must be nontrivial, and both bounds are required uniformly.

Needed infrastructure: LCS and alignment combinatorics, cut decompositions of finite $\ell_1$ metrics, Fourier analysis on finite cyclic groups, prime counting estimates, and random partition arguments for the upper bound. Contributions toward any component are welcome.

Selected references

• OpenAI, Finite-Circle Obstructions, Binary Codes, and Histogram Embeddings for Edit Distance, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-Circle-Obstructions-Binary-Codes-and-Histogram-Embeddings-for-Edit-Distance-September-27-2026/paper.pdf
• OpenAI, Edit Distance in $\ell_1$: Matching Bounds up to Constants in the Exponent, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/main/preprints/Edit-Distance-in-l1-Matching-Bounds-up-to-Constants-in-the-Exponent-September-27-2026/paper.pdf
• R. Ostrovsky, Y. Rabani, Low distortion embeddings for edit distance, J. ACM 54(5), 2007. https://doi.org/10.1145/1284320.1284322
• R. Krauthgamer, Y. Rabani, Improved lower bounds for embeddings into $L_1$, SIAM J. Comput. 38(6), 2009.
• S. Khot, A. Naor, Nonembeddability theorems via Fourier analysis, Math. Ann. 334(4), 2006. https://doi.org/10.1007/s00208-005-0745-0
• A. Andoni, M. Deza, A. Gupta, P. Indyk, S. Raskhodnikova, Lower bounds for embedding edit distance into normed spaces, SODA 2003.
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2), 1995. https://doi.org/10.1007/BF01200757
• L. J. Schulman, D. Zuckerman, Asymptotically good codes correcting insertions, deletions, and transpositions, IEEE Trans. Inform. Theory 45(7), 1999. https://doi.org/10.1109/18.796406
• V. I. Levenshtein, Binary codes capable of correcting deletions, insertions, and reversals, Soviet Physics Doklady 10(8), 1966.
• R. A. Wagner, M. J. Fischer, The string-to-string correction problem, J. ACM 21(1), 1974. https://doi.org/10.1145/321796.321811

Motivation

A metric space is doubling if every ball can be covered by a bounded number of balls of half the radius. Every subset of a finite-dimensional Euclidean space is doubling, so doubling is a necessary condition for a metric space to embed bi-Lipschitzly into some $\mathbb R^k$. Whether it is also sufficient, for subsets of Hilbert space, is the Lang–Plaut problem. It sits at the meeting point of metric geometry and algorithm design: doubling is a standard notion of "intrinsic dimension" for data, and a positive answer would mean that intrinsically low-dimensional Euclidean data can always be represented in a bounded number of coordinates with bounded distortion.

Timeline

• 1983. Assouad proves that every doubling metric space embeds bi-Lipschitzly into some $\mathbb R^k$ after snowflaking, i.e. after replacing the distance $d$ by $d^\alpha$ with $0<\alpha<1$ (doi:10.24033/bsmf.1997).
• 2001. Lang and Plaut ask whether every doubling subset of Hilbert space admits a bi-Lipschitz embedding into a finite-dimensional Euclidean space (Question 2.4) (doi:10.1023/A:1012093209450).
• 2003. Gupta, Krauthgamer and Lee independently pose the question for algorithmic dimension reduction (doi:10.1109/SFCS.2003.1238226).
• 2012. Naor and Neiman bound the target dimension in Assouad's theorem independently of the snowflake exponent near $1$ (doi:10.4171/RMI/706).
• 2014. Lafforgue and Naor construct, for $p>2$, a doubling subset of $L_p$ with no bi-Lipschitz embedding into any $\mathbb R^k$ (doi:10.1007/s10711-013-9924-4).
• 2015. Bartal, Gottlieb and Neiman obtain obstructions for doubling subsets of $\ell_p$ via Laakso-type configurations (doi:10.1137/140977655); Gottlieb and Krauthgamer embed snowflakes of finite Hilbert subsets with distortion close to one (doi:10.1007/s00454-015-9707-9).
• 2017. Schioppa announces a negative answer for $\ell_2$ and later withdraws the preprint (arXiv:1703.10265).
• 2021. Baudier, Świȩcicki and Swift give an elementary proof of the fixed-set theorem for $\ell_q$, $q>2$ (doi:10.1016/j.jmaa.2021.125407).

The Hilbert case ($p=2$) remained open. The source of this mission, an OpenAI preprint dated September 25, 2026, claims a negative answer.

Setting

A metric space $(X,d)$ is doubling with constant at most $\lambda$ if for every $x\in X$ and $r>0$, the ball of radius $r$ about $x$ is covered by at most $\lambda$ balls of radius $r/2$ with centers in $X$. A map $f:X\to\mathbb R^k$ is a bi-Lipschitz embedding with distortion at most $D$ if some scale $a>0$ satisfies

$$a\,d(x,y)\ \le\ \|f(x)-f(y)\|\ \le\ D\,a\,d(x,y)\qquad(x,y\in X).$$

Real $\ell_2$ is the Hilbert space of square-summable real sequences indexed by $\mathbb N$; subsets carry the induced distance.

Formalization targets

Corollary 6 (milestone)

There is a universal $\Lambda$ such that every infinite-dimensional real Banach space $B$ contains a compact set $K_B$ with doubling constant at most $\Lambda$ that admits no bi-Lipschitz embedding into any finite-dimensional real normed space at any finite distortion.

Goal: Theorem 1

$$\exists\, S\subset\ell_2:\quad S\ \text{is doubling with constant}\ \le 76800,\ \text{and}\ \forall k\ge1,\ S\ \text{admits no bi-Lipschitz embedding into}\ \mathbb R^k.$$

The set is fixed once, independently of $k$ and of the distortion. The Lean statement OAI.DoublingHilbert.main is open on the platform. The constant $76800=300\cdot16^2$ comes from the paper's covering count; any finite universal constant would answer the Lang–Plaut problem, but the Lean goal records the paper's value.

Significance

The theorem answers the Lang–Plaut problem negatively: there is no function of the doubling constant alone that bounds both the dimension and the distortion for doubling subsets of Hilbert space. It extends the Lafforgue–Naor and Bartal–Gottlieb–Neiman obstructions from $p>2$ to the Hilbert case, which is the case of most interest for applications. By Gaussian isometric embedding the same metric space sits in every $L_p[0,1]$, $1\le p<\infty$ (Corollary 5), and by Dvoretzky's theorem a compact version sits in every infinite-dimensional Banach space (Corollary 6). Assouad's theorem shows that any snowflake of the set does embed, so the obstruction is specific to the original distance.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A previous announced proof of this statement (Schioppa, 2017) was withdrawn, which makes an independent formal verification particularly informative.

Difficulty

Doubling gives covering control at every scale, and Assouad's theorem shows that any loss in the exponent of the metric removes the obstruction, so a counterexample must be sharp at the level of exact Lipschitz bounds. The $p>2$ constructions rely on uniform convexity estimates of $L_p$ that degenerate at $p=2$, and Hilbert space has the most symmetric geometry available, so the standard Laakso and diamond-type obstructions do not transfer. The set must also be chosen before the target dimension and distortion, so a single set has to defeat every $k$ and every $D$ simultaneously.

Formalization scope

• The ambient space is RealL2 := lp (fun _ : ℕ => ℝ) 2; $S$ is a Set RealL2 with the subspace metric.
• DoublingAtMost S bound: for each $x\in S$ and $r>0$ there is a Finset of at most bound centers in $S$ such that every $y\in S$ with $d(y,x)<r$ satisfies $d(y,c)<r/2$ for some center (open balls; centers in $S$).
• AdmitsBiLipschitzEmbedding S k: there are $f:S\to$ EuclideanSpace ℝ (Fin k), $a>0$ and $D\ge1$ with the two-sided bound above.
• For Corollary 6, CompactBanach.main quantifies over all complete real normed spaces that are not finite-dimensional and all finite-dimensional real normed targets, with the doubling constant $\Lambda$ chosen before $B$.

A complete development needs Hilbert direct sums, the explicit strip-colored set, covering estimates, a.e. differentiability of Lipschitz maps on open subsets of $\mathbb R^2$ (Rademacher), and a Euclidean packing bound. Rademacher's theorem and packing estimates are reusable well beyond this mission. Contributions formalizing Proposition 2 (the doubling bound) are a natural first step.

Selected references

• OpenAI, A doubling Hilbert subset with no finite-dimensional bi-Lipschitz embedding, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-doubling-Hilbert-subset-with-no-finite-dimensional-bi-Lipschitz-embedding-September-25-2026/main.pdf
• U. Lang, C. Plaut, Bilipschitz embeddings of metric spaces into space forms, Geom. Dedicata, 2001. https://doi.org/10.1023/A:1012093209450
• P. Assouad, Plongements lipschitziens dans $\mathbb R^n$, Bull. Soc. Math. France, 1983. https://doi.org/10.24033/bsmf.1997
• A. Gupta, R. Krauthgamer, J. R. Lee, Bounded geometries, fractals, and low-distortion embeddings, FOCS 2003. https://doi.org/10.1109/SFCS.2003.1238226
• A. Naor, O. Neiman, Assouad's theorem with dimension independent of the snowflaking, Rev. Mat. Iberoam., 2012. https://doi.org/10.4171/RMI/706
• V. Lafforgue, A. Naor, A doubling subset of $L_p$ for $p>2$ that is inherently infinite dimensional, Geom. Dedicata, 2014. https://doi.org/10.1007/s10711-013-9924-4
• Y. Bartal, L.-A. Gottlieb, O. Neiman, On the impossibility of dimension reduction for doubling subsets of $\ell_p$, SIAM J. Discrete Math., 2015. https://doi.org/10.1137/140977655
• F. P. Baudier, K. Świȩcicki, A. Swift, No dimension reduction for doubling subsets of $\ell_q$ when $q>2$ revisited, J. Math. Anal. Appl., 2021. https://doi.org/10.1016/j.jmaa.2021.125407

Motivation

The Johnson–Lindenstrauss lemma (1984) says that any $n$ points of a Hilbert space can be placed in $O_D(\log n)$-dimensional Euclidean space with distortion at most any prescribed $D>1$. This dimension reduction is used throughout analysis, geometry and algorithm design. Johnson and Lindenstrauss also asked what analogues hold in other Banach spaces. For the spaces $L_p$ with $p\ne2$ the question splits into several versions: whether one needs the map to be linear, whether one discretizes a whole subspace or only a finite set, and whether the target is a coordinate space $\ell_p^d$ with the same exponent. This mission concerns the finite-set, coordinate-target, nonlinear version: how many coordinates $d$ are needed so that every $n$-point subset of $L_p$ embeds into $\ell_p^d$ with distortion at most $D$?

Timeline

• 1958. Lamperti characterizes equality in the $p$-parallelogram inequality, the tool behind exact-embedding lower bounds (doi:10.2140/pjm.1958.8.459).
• 1984. Johnson and Lindenstrauss prove the Hilbert-space lemma and ask for analogues in other spaces (doi:10.1090/conm/026/737400).
• 1987 and 2011. Schechtman's finite-set estimates for $p<2$ improve from $O_D(n\log n)$ coordinates to $O_{p,D}(n)$ (numdam, arXiv:1110.2148).
• 1989 and 1995. Bourgain–Lindenstrauss–Milman and Talagrand discretize whole $r$-dimensional subspaces of $L_p$ by linear maps (doi:10.1007/BF02392835, doi:10.1007/978-3-0348-9090-8_26); applied to $n$ points this gives dimension polynomial in $n$.
• 1990. Ball proves that exact embeddings need at most $\binom n2$ coordinates and that quadratic order is necessary for $1\le p<2$ (doi:10.1016/S0195-6698(13)80131-X).
• 2004–2005. Brinkman–Charikar and Lee–Naor show that dimension reduction fails in $\ell_1$ even for nonlinear maps (doi:10.1145/1089023.1089026, doi:10.1007/s00039-004-0473-8); Lee–Mendel–Naor show that linear maps can require dimension linear in $n$ when $p\ne2$ (doi:10.1016/j.ejc.2004.07.002).
• 2018. Naor surveys metric dimension reduction and the coordinate-target question (arXiv:1809.02376).
• 2026. Naor and Ren show that for $p>2$ the dimension cannot be $O_{p,D}(\log n)$ (arXiv:2609.01079).

The source of this mission, an OpenAI preprint dated September 23, 2026, claims that for every fixed $1<p<\infty$, $p\ne2$, and $D>1$ the dimension is $n^{o(1)}$.

Setting

All spaces are real. Fix $1<p<\infty$, an integer $n\ge2$ and $D\ge1$. Let $d_p(n,D)$ be the least integer $d$ such that for every measure space and every $n$ distinct points $x_1,\dots,x_n\in L_p$ there are $y_1,\dots,y_n\in\mathbb R^d$ and a scale $s>0$ with

$$s\,\|x_i-x_j\|_p\ \le\ \|y_i-y_j\|_{\ell_p^d}\ \le\ D\,s\,\|x_i-x_j\|_p\qquad(1\le i,j\le n).$$

The map $x_i\mapsto y_i$ is arbitrary, not required to be linear. Put

$$\gamma(p)=\begin{cases}2-p,&1<p<2,\\ 1-2/p,&2<p<\infty.\end{cases}$$

Formalization targets

Goal: Theorem 1.1

For fixed $1<p<\infty$, $p\ne2$:

$$\forall D>1\ \exists C_{p,D}\ \forall n\ge2:\quad \frac{\log n}{\log(1+2D)}\ \le\ d_p(n,D)\ \le\ \exp\bigl(C_{p,D}(\log n)^{\gamma(p)}\bigr);$$ $$\Bigl\lfloor\tfrac{n-1}{4}\Bigr\rfloor^2\ \le\ d_p(n,1)\ \le\ \binom n2\qquad(n\ge9);$$ $$\lim_{n\to\infty}\frac{\log d_p(n,D)}{\log n}=\begin{cases}0,&D>1,\\ 2,&D=1.\end{cases}$$

Since $\gamma(p)<1$, the upper bound is $n^{o(1)}$. The Lean statement OAI.SubpolynomialLp.source_main is open on the platform.

Significance

For $p\ne2$ the best previous finite-set bounds were polynomial in $n$ (linear for $p<2$), and for $p>2$ logarithmic dimension is impossible. The theorem places $d_p(n,D)$ at $n^{o(1)}$ for every fixed $D>1$, in contrast with exact embeddings, where the dimension is of order $n^2$. Thus the exponent $\lim \log d_p/\log n$ jumps from $2$ at $D=1$ to $0$ for every $D>1$. The upper exponent and the logarithmic lower bound are not claimed to be optimal. The theorem is existential; no embedding algorithm is asserted.

The result is claimed in an OpenAI preprint and has not been peer reviewed; no machine-checked proof exists. A formal proof would include a probabilistic construction (stable laws, Poisson sampling, Rosenthal-type moment inequalities), an electrical-flow localization estimate, and a convex-separation argument.

Difficulty

Linear maps cannot work: fixed-distortion linear maps on some $L_p$ configurations need dimension proportional to $n$ when $p\ne2$. Subspace discretization theorems apply to the span of the points, which has dimension up to $n-1$, so they also give only polynomial bounds. The Johnson–Lindenstrauss approach relies on Gaussian rotation invariance, which has no analogue in $L_p$. One needs a single random scalar map whose increments have nearly equal normalized $p$-th moments simultaneously for all $\binom n2$ pairs, with relative (not additive) error control.

Formalization scope

• coordinateDistance p y z is $(\sum_a |y_a-z_a|^p)^{1/p}$ on Fin d → ℝ.
• GoodDimension p n D d quantifies over every measure space (Ω, mΩ, μ) in a fixed universe and every injective x : Fin n → Lp ℝ (ENNReal.ofReal p) μ; the target is Fin d → ℝ with the $\ell_p$ distance and a scale $s>0$.
• dimension p n D is the sInf of the good dimensions in ℕ. The goal also asserts that this infimum is good, so the default value of sInf ∅ cannot make the bounds trivial.
• gamma p is as above; the exact-embedding lower bound uses natural-number division, i.e. the floor.
• The limit is a Tendsto statement along n : ℕ for each $D\ge1$.

A complete development needs $L_p$ spaces, $p$-stable random variables, Poisson sampling and moment inequalities, effective resistance and electrical flows on complete graphs, and Carathéodory's theorem for the exact-embedding upper bound. Contributions formalizing the exact-embedding bounds (Ball's upper bound and the antipodal lower bound) and the weighted moment criterion are welcome.

Selected references

• OpenAI, Subpolynomial dimension reduction in $L_p$, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Subpolynomial-dimension-reduction-in-Lp-September-23-2026/paper.pdf
• W. B. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26, 1984. https://doi.org/10.1090/conm/026/737400
• K. Ball, Isometric embedding in $l_p$-spaces, European J. Combin., 1990. https://doi.org/10.1016/S0195-6698(13)80131-X
• G. Schechtman, Dimension reduction in $L_p$, $0<p<2$, preprint, 2011. https://arxiv.org/abs/1110.2148
• B. Brinkman, M. Charikar, On the impossibility of dimension reduction in $\ell_1$, J. ACM, 2005. https://doi.org/10.1145/1089023.1089026
• J. R. Lee, M. Mendel, A. Naor, Metric structures in $L_1$: dimension, snowflakes, and average distortion, European J. Combin., 2005. https://doi.org/10.1016/j.ejc.2004.07.002
• A. Naor, Metric dimension reduction: a snapshot of the Ribe program, Proc. ICM 2018. https://arxiv.org/abs/1809.02376
• A. Naor, K. Ren, A threshold phenomenon for embeddings of Euclidean snowflakes and impossibility of dimension reduction, preprint, 2026. https://arxiv.org/abs/2609.01079
• O. Gurel-Gurevich, A. Nachmias, S. Sachdeva, A tight bound on localization of electrical flows, preprint, 2026. https://arxiv.org/abs/2605.24130