Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Risk measures quantify the danger of an uncertain cost by a single number. The axiomatic theory of coherent and convex risk measures (Artzner, Delbaen, Eber and Heath, Coherent measures of risk, 1999; Föllmer and Schied, Convex measures of risk and trading constraints, 2002) is static: the risk is evaluated once, with no information beyond what is known at time zero. Multistage stochastic optimization and dynamic risk management need risk evaluated conditionally: at time 1 part of the uncertainty has been resolved, and the risk of a time-2 cost should be a function of what is known at time 1.
Ruszczyński and Shapiro, in Conditional risk mappings (preprint of February 21, 2004; journal version Mathematics of Operations Research 31(3), 2006), extend their earlier static theory (Optimization of convex risk functions, Math. Oper. Res. 31(3), 2006) to this conditional setting. They define conditional risk mappings by three axioms, derive a pointwise conjugate duality, and show that positively homogeneous conditional risk mappings are, under regularity conditions, suprema of countably many conditional expectations. The last result explains the word conditional: the conditional expectation is the prototype, and every positively homogeneous conditional risk mapping is a worst case over a countable family of them.
Let be a set with -algebras ; is the information available when risk is evaluated. Let be a real vector space of -measurable functions , and a subspace of -measurable ones. Let be a real vector space of finite signed measures on with , and pair them by
Both spaces carry locally convex topologies that are compatible with this pairing: the continuous linear functionals on each space are exactly the pairings with elements of the other. Two standing conditions hold throughout: (C) if is not a nonnegative measure, some nonnegative has ; (C′) for every .
A conditional risk mapping is a map with, writing :
Costs are minimised: smaller is better. All inequalities hold at every , not almost surely. is positively homogeneous if for , and lower semicontinuous if each is.
The conjugate is and the risk envelope is . denotes the probability measures in , and those with for all . A map is weakly* -measurable if every is -measurable. For such a selection of , the operator acts on . Assumption (K): is compact, and every such maps into itself with a closed graph. Finally, is the conditional probability of given if each is -measurable and for , ; then .
If is separable, (K) holds and is a positively homogeneous, lower semicontinuous conditional risk mapping, then there are probability measures , , with
each conditional expectation being the integral against a weakly* -measurable conditional probability of .
Corollary 1 (p. 10, singleton envelopes give a conditional expectation) and Proposition 2 (p. 7, for nonnegative -step functions ) are included as further statements.
Theorem 2 identifies the positively homogeneous conditional risk mappings with suprema of conditional expectations. It is the conditional analogue of the representation of a coherent risk measure as a worst-case expectation over a set of probability measures. It shows that the axioms (A1)–(A3), stated at every , are the right abstraction of "conditional": nothing beyond conditional expectations and a supremum is needed to generate them. Theorem 1, the pointwise duality on which it rests, is what makes conditional risk mappings usable in multistage problems. Its envelope form (3.8) is what the paper's composition results and dynamic programming equations in §5–§7 manipulate.
The results are proved in the paper, partly by reference: the duality of Theorem 1 by applying the authors' earlier unconditional theorem "verbatim" at each , Lemma 1 through a measurable-selection theorem, and Theorem 2 through Kakutani's fixed-point theorem. None of them is formalized. A formalization would check these deferred steps. In particular the passage, in the proof of Lemma 1, from a dense subset of to all of uses only lower semicontinuity of , and whether that suffices in every separable paired space is open to scrutiny.
Theorem 1 needs the Fenchel–Moreau theorem in a general locally convex space, paired through integrals against signed measures. Mathlib's convex duality is mostly finite-dimensional or normed, and the extended-real bookkeeping of conjugates is delicate. The main obstacle is Lemma 1. The envelope can be uncountable, and choosing countably many selections that are simultaneously measurable in and exhaust the supremum for every requires a measurable-selection theorem for multifunctions with values in , a space that need not be metrizable. The obvious argument fixes a dense sequence , picks -optimal measures for each , and passes to general by semicontinuity. As written, that last step appears to need more than the proof supplies: approximation of by uniformly over the chosen needs more than lower semicontinuity of . The fixed-point step needs a Kakutani-type theorem in a locally convex space, which Mathlib does not provide.
and are abstract real vector spaces with their own topologies (instances of IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ), realised by injective linear maps into and into Mathlib's SignedMeasure Ω. They are not subspaces of with the pointwise topology. The ambient MeasurableSpace Ω is ; is a structure field. The pairing is , and integrability against is a field, so no integral takes a junk value. Compatibility includes continuity of both pairings as well as the representation of continuous functionals. The paper's space is not modelled; no statement uses it.
Committed conventions:
EReal;IsLUB), never sSup on ;Two hypotheses are added where the page relies on them implicitly. is nonempty in the goal, Corollary 1 and the fixed-point milestone. for every is assumed in the goal, Proposition 3 and Corollary 1, because the paper derives measurability of from weak* measurability.
The goal cannot be satisfied by an almost-everywhere version of a conditional expectation chosen separately for each , which would allow itself as a "version". Each is integration against one kernel that is a conditional probability of . The goal mentions no selection, fixed point or Kakutani; appears only inside (K).
Contributions are welcome on all of the following:
All three are reusable beyond this mission.
Stochastic models of covariance matrices need processes that stay in the cone of positive semidefinite matrices. Wishart processes (Bru, 1991) and their extensions underlie multivariate stochastic-volatility and term-structure models in finance (see §1 of Cuchiero et al. for the literature). They are used because their Laplace transforms are explicit: they are exponential-affine in the initial state, and their exponents solve matrix Riccati equations. Cuchiero, Filipović, Mayerhofer and Teichmann (arXiv:0910.0137, Ann. Appl. Probab. 2011) classify all such affine processes on the cone. Theorem 2.4 of that paper says that affine processes on correspond one-to-one to admissible parameter sets. This mission formalizes the converse direction of that correspondence: every admissible parameter set is realized by exactly one affine process.
Timeline:
Let be the real symmetric matrices with , let be the positive semidefinite cone, and let be its interior. Write when . A time-homogeneous, possibly killed Markov process on with transition kernels is affine if it is stochastically continuous and
for functions and .
An admissible parameter set (Definition 2.3) consists of the following:
These data define the operator (2.12),
with . They also define the functions and of (2.16)–(2.17), which drive the generalized Riccati equations , and , .
For every admissible parameter set there is a transition family and there are exponents such that:
Together with the necessity direction (companion mission I in this series), the goal makes admissibility an exact characterization. Every admissible parameter set, including those with jumps of infinite activity and state-dependent killing, defines a well-posed Markov model on . Its Laplace transform is then given by the Riccati flow, which is what makes the model computationally tractable. The intermediate results are reusable on their own:
The theorem is proved in the paper; it is not formalized anywhere. No formal library contains affine processes, generalized Riccati equations on matrix cones, quasi-monotone comparison theorems or martingale problems with jumps. Formalizing them requires all of that infrastructure.
The obvious route is to solve the Riccati equation (2.15) on by Picard iteration and to show invariance of the cone from the inward-pointing condition. That route fails because need not be Lipschitz at : the integral term can have unbounded derivative there (Remark 5.4). Standard invariance theorems therefore do not apply. Instead, quasi-monotonicity keeps the solution away from the boundary.
The obvious construction of the process is also blocked. Stroock's existence and uniqueness theory for martingale problems needs and a uniformly elliptic diffusion part, and neither holds on the cone, where the diffusion degenerates at the boundary. Existence must go through regularized operators with bounded smooth coefficients, then tightness in the Skorokhod space of and a limit. Uniqueness in law comes from the Riccati solutions. The killing terms and are added last.
Conventions committed to in Lean:
Fin d → Fin d → ℝ, with and its norm.∃!.EthierKurtz.HasCadlagPaths).Trivializing formalizations are excluded:
∃! over transition families would be false at negative times, so uniqueness is stated for .Needed infrastructure, reusable beyond this mission: matrix calculus on (square roots, spectral derivatives), comparison theorems for quasi-monotone ODEs, analytic dependence of ODE solutions, tightness in Skorokhod space, and martingale problems on locally compact spaces. Contributions are welcome at any of these levels, as are alternative proofs of the milestones.
The Lasso is the standard estimator for high-dimensional linear regression: from noisy linear measurements of an unknown vector , with possibly much larger than , it minimizes the empirical squared error plus an penalty. Its theoretical guarantees are usually stated as sparsity oracle inequalities: the prediction error of the Lasso is bounded by the best trade-off, over all candidate vectors , between the approximation error of and a term proportional to the number of nonzero components of .
Before this paper, such inequalities for the Lasso carried a leading constant strictly larger than in front of the approximation error. The inequalities of Bunea, Tsybakov and Wegkamp (EJS 2007) and of Bickel, Ritov and Tsybakov (Ann. Statist. 2009, Theorem 6.1) have this form, and the paper notes that sharpness "was not achieved in the previous work on the Lasso" (p. 24). A leading constant larger than means the bound is not informative when the true regression function is far from every sparse linear combination: the inequality then only says that the Lasso is within a constant factor of the best approximation.
Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study nuclear-norm penalized estimation of low-rank matrices in the trace regression model. Their general oracle inequality for a linear subspace of matrices (Theorem 2) has leading constant . Restricted to diagonal matrices with a fixed design, the trace regression model becomes ordinary linear regression and the estimator becomes the Lasso. Section 5.4 of the paper draws the consequence: a sharp (leading constant ) sparsity oracle inequality for the Lasso with Gaussian noise, Theorem 14. This mission formalizes that theorem. The source is the arXiv preprint arXiv:1011.6256v4.
Fix integers and and fixed vectors , the rows of the design matrix . The diagonal elements of the Gram matrix are assumed not larger than . The observations are
with independent random variables, .
For , , and . For , agrees with on and vanishes on . The support of is and the sparsity is its cardinality.
Given , a Lasso estimator is any minimizer
The restricted constant at , with and , is
equal to when the set is empty, and . It is the inverse of a restricted eigenvalue computed at the single support ; the paper obtains it from its matrix quantity for . Finally is the noise vector.
Let with , . With probability at least ,
The event is uniform over all , and the statement holds for every Lasso minimizer.
Theorem 14 gives an oracle inequality for the Lasso whose leading constant is exactly . As a consequence (Corollary 4 of the paper), under the restricted eigenvalue condition RE of Bickel, Ritov and Tsybakov the Lasso's prediction error is at most the best -sparse approximation error plus , which improves the non-sharp inequality of that paper. The bound also shows that the matrix-valued argument of the paper, written for nuclear-norm penalization, specializes cleanly to the vector case; the same argument underlies the matrix completion results of the other missions of this series.
The result is proved in the paper. As far as a search of the platform shows, no formal proof of a sharp oracle inequality for the Lasso exists; the platform has the non-sharp Bickel–Ritov–Tsybakov inequality as an open statement (LassoDantzig.Oracle.theorem_6_1). This mission produces a machine-checked version of the deterministic inequality, of the Gaussian concentration step, and of their combination, with the restricted constant defined exactly as in the paper.
The deterministic part is where the obvious argument fails. The usual Lasso analysis compares the objective at and at a candidate , controls the noise cross term, and rearranges; every version of that argument in the earlier literature loses a multiplicative factor in front of the approximation error , and the factor cannot be pushed to by tuning constants. The sharp bound has to come from a finer use of the optimality of , and the cone constant in is tied to the threshold . Formally, optimality conditions for a nonsmooth convex function on (the subdifferential of ) are infrastructure that has to be in place.
The probabilistic part needs the distribution of a linear combination of independent Gaussians, a Mills-ratio tail bound that is not in Mathlib, and a union bound over coordinates, with the exact constants of the paper.
Vectors are functions Fin p → ℝ, and the design is given by its rows x i : Fin p → ℝ. All statements are in vector form, as the paper itself writes Section 5.4; no matrix library is needed. The Lasso is an argmin predicate, and statements hold for every minimizer; in the goal, is a function of the outcome that is a minimizer at every outcome, and no measurability of is assumed (the bad event is bounded in outer measure).
The restricted constant is formalized through its witnesses: the theorems hold for every in the set whose infimum is . This is equivalent to the infimum, because the bounds are continuous and increasing in . A real-valued infimum would be on an empty set and would make the oracle inequality false, so it is deliberately not used. The infimum over is stated as "for every ", inside the event.
Hypotheses added relative to the page, each disclosed in the item's Formalization Note: (for , and the printed probability divides by zero), , , and measurability of the noise variables. is the paper's standing assumption. The condition is written coordinatewise. In the deterministic milestones the noise is a fixed vector and , which is the paper's for a fixed design and centred noise. No printed slip affects these statements. The constant is kept as printed.
A trivializing formalization would assume the event in the goal, or use a real infimum for ; both are ruled out. Contributions of reusable infrastructure are welcome: the Gaussian tail bound, the law of a weighted sum of independent Gaussians, and the subdifferential of the norm.
Mathematical programs with complementarity constraints (MPCCs, also called MPECs) model optimization problems in which some constraints say that, for every index , at least one of two nonnegative quantities , must vanish. They arise in bilevel optimization, Stackelberg games, the design of equilibria in traffic and electricity markets, and contact problems in mechanics (Luo, Pang, Ralph 1996). Standard nonlinear-programming algorithms do not apply directly: at every feasible point of an MPEC the Mangasarian–Fromovitz constraint qualification fails, so the classical convergence theory of SQP or interior-point methods gives no guarantees.
Relaxation methods replace the MPEC by a sequence of better-behaved nonlinear programs with a parameter , solve each one approximately, and study the limits of the computed points. The question every relaxation method has to answer is what kind of stationary point such limits are, and under which constraint qualification.
Timeline of the result formalized here:
The MPEC (1) on is
with continuously differentiable data. At a feasible the index sets are , , (the biactive set) and .
A feasible is weakly stationary if there are multipliers with , , , such that
with on and on . It is M-stationary if the same multipliers satisfy, for every , either and , or .
The tightened program TNLP replaces the complementarity constraints by on , on and on . CPLD (constant positive linear dependence) for a nonlinear program says: whenever a set of active-constraint gradients is positive-linearly dependent at (a nontrivial vanishing combination with nonnegative coefficients on the inequalities), the same gradients stay linearly dependent on a neighbourhood of . MPEC-CPLD is CPLD for TNLP.
The relaxation of Kadrani et al. is, for ,
A stationary point of is a feasible point with KKT multipliers.
Local minimizers of an MPEC are M-stationary under weak constraint qualifications, whereas strong stationarity needs stronger ones such as MPEC-LICQ; a C-stationary point, the kind of limit the Scholtes relaxation delivers, may still admit first-order descent directions. Theorem 3.5 shows that the Kadrani et al. relaxation reaches M-stationary limits under a constraint qualification that is implied by MPEC-LICQ and MPEC-MFCQ and that holds, for instance, whenever all constraint functions are affine. It separates this scheme from the Scholtes and Steffensen–Ulbrich relaxations in the comparison of the paper.
The theorem is proved in the paper. As far as is known, no part of MPEC theory (constraint qualifications for MPECs, the stationarity hierarchy, relaxation schemes) has a machine-checked proof in Lean or Mathlib. This mission produces a formal account of the stationarity notions of Definition 2.3, of CPLD and MPEC-CPLD, and a complete formal proof of the convergence result, including the standard constraints , that the paper's proof skips for brevity.
The obvious argument passes to the limit in the KKT conditions of . This fails because the multipliers need not be bounded: unlike under MPEC-LICQ or MPEC-MFCQ, MPEC-CPLD does not by itself bound KKT multipliers, and the KKT points of the relaxed programs need not satisfy any constraint qualification themselves (Example 3.6 of the paper). The second difficulty is the biactive set : the product constraint contributes multipliers , to both and , with signs that are not fixed a priori, so a naive limit of the multipliers only gives C-stationarity-type information, or none at all.
is EuclideanSpace ℝ (Fin n) and gradients are Mathlib's gradient; indices are 0-based (Fin m, Fin p, Fin l), and may be zero. Explicit choices fixed by the formalization:
P.IsC1 of every analytic statement.LinearIndependent ℝ of a family indexed by a disjoint union of subtypes, so repeated gradients count as dependent.∀ᶠ y in 𝓝 x*.Two trivializing readings are ruled out. M-stationarity uses one multiplier tuple for both the weak-stationarity equation and the condition on ; separate multipliers would make the sign condition vacuous. MPEC-CPLD demands linear dependence on a whole neighbourhood of , not only at ; the pointwise version is a different hypothesis.
A complete development needs the gradient calculus of products and compositions on EuclideanSpace, a Carathéodory-type lemma (a conic combination can be reduced to one over linearly independent vectors with the same signs), and compactness of bounded sequences in finite dimensions. The Carathéodory lemma and the CPLD/positive-linear-dependence layer are reusable for any constraint-qualification argument in nonlinear programming. Proofs of individual milestones, and of the lemma behind (15), are welcome independently of the goal.
Open networks of single-server queues with general (non-exponential) interarrival and service times, generalized Jackson networks (GJNs), model manufacturing lines, communication networks and service systems. Their stationary distributions are almost never available in closed form. The standard engineering approximation replaces the scaled queue-length vector by the stationary distribution of a reflected Brownian motion (RBM) in the orthant, which is the diffusion limit of the network in heavy traffic, when every station is close to full utilisation.
The diffusion limit itself (Reiman, 1984) is a statement about the process on finite time intervals. Using the RBM's stationary law as an approximation of the network's stationary law requires interchanging two limits: time to infinity (steady state) and traffic intensity to one (heavy traffic). For a long time this interchange was assumed rather than proved.
Timeline.
There are stations. Station receives external arrivals with i.i.d. interarrival times of law (rate , or no arrivals at all) and serves jobs first-in-first-out with i.i.d. service times of law (mean , rate ). A job finishing at moves to with probability or leaves. The routing matrix is substochastic with spectral radius below one. Interarrival and service times have uniformly bounded conditional exponential moments of their residual lives (conditions (1)–(2)). The traffic equation gives the effective rates and the traffic intensities .
The queue lengths are not Markov. The state , which adds the elapsed interarrival and service times, is a Markov process on . A law on is stationary if implies for all .
Heavy traffic. Fix a critically loaded network ( for all ) and a vector . The network slows the arrivals of at station by the factor , so that for an explicit (display (17)). Let be any stationary distribution of , and let be the law of under .
The RBM. For a Brownian motion with drift and covariance , the RBM with parameters solves the Skorohod problem , with nondecreasing and increasing only when is on the boundary. Here and is the explicit covariance matrix of Reiman's theorem, built from , , and the squared coefficients of variation , of .
where is the unique stationary distribution of the -RBM. The formal goal asserts three things: a stationary distribution of the RBM exists, it is the only one, and converges weakly to it, for every choice of stationary distributions .
The result. Theorem 8 justifies the use of the RBM's stationary distribution, which is computable or at least numerically tractable, as an approximation of steady-state queue lengths of a heavily loaded network. Theorem 7 also shows that each stationary queue is of order uniformly in . Together with Theorem 8 this gives convergence of all moments (Corollary 2 of the paper) and, through Theorems 9–12, steady-state approximations of sojourn times and product-form limits.
Formalizing it. No part of this argument is machine-checked. The formalization would add reusable infrastructure for queueing theory in Lean: a Markov-state model of a generalized Jackson network with residual times, Lyapunov bounds on stationary distributions of general Markov processes (Theorems 5–6), and the link between tightness and identification of limit points for stationary laws. Reiman's theorem (Theorem 4) and the Harrison–Williams theorem (Theorem 3) are cited by the paper and are themselves open formalization targets.
Tightness and Reiman's theorem do not combine on their own. Reiman's theorem describes the network on finite time intervals, started empty, while a stationary distribution describes it as time goes to infinity; nothing in the finite-horizon limit forces a limit point of to be stationary for the RBM, or forces different subsequences to have the same limit. The interchange therefore needs the process limit from an arbitrary initial law and the uniqueness of the RBM's stationary law, besides tightness.
The tightness step is the technical core. Moment bounds must be uniform in and in the initial residual times. A Lyapunov argument on the workload over a time horizon of order requires deviation bounds of order for renewal processes started at arbitrary ages. This is why the residual-life conditions (1)–(2) appear, and why the strong approximation of Lemma A.2 is used. A naive drift argument over a fixed time horizon fails: in heavy traffic the drift of per unit time is only of order .
Fin J, vectors Fin J → ℝ, is Pᵀ, and the norm is the norm, written as an explicit sum. The spectral-radius condition is .IsGJN (positive times, conditions (1)–(2), substochastic ). and count renewal epochs in . The initial times , are residual lives given the elapsed ages , . States carry their elapsed times as reals; the predicate InStateSpace cuts out , and the uniform bounds over initial states (Lemma A.1, Propositions 2–3) and the initial laws of Theorem 4 range over only.Reiman84.QueueLength.Paths (Brownian motion with drift and covariance, and the reflection pair). An RBM stationary law must be a probability measure carried by . Weak convergence of laws on uses Mathlib's topology on ProbabilityMeasure. Theorem 4's process convergence is in coupling form with the uniform topology on .Classical arbitrage pricing fixes one probabilistic model of the underlying asset and prices a contingent claim as an expectation under an equivalent martingale measure. When the volatility is not known, a seller who wants to be safe under every plausible model has to superreplicate: hold an initial capital and a trading strategy whose terminal value dominates the claim under all models at once. The uncertain volatility model (UVM) of Avellaneda, Levy and Parás (Appl. Math. Finance 1995) and Lyons (Appl. Math. Finance 1995) is the standard instance: the volatility is only known to lie in an interval .
The family of laws describing such uncertainty is not dominated by a single reference probability, so "almost surely" and the usual stochastic integral are not available. Denis and Martini (Ann. Appl. Probab. 2006) replace them by a capacity and a quasi-sure stochastic integral, and show that the superreplication price of a broad class of path-dependent European claims is a supremum of expectations over martingale laws. This framework is a precursor of quasi-sure analysis and -expectations (Denis, Hu and Peng, Potential Anal. 2011; Soner, Touzi and Zhang, Electron. J. Probab. 2011).
Fix . is the space of continuous paths with , with the uniform norm, Borel -field and canonical filtration . A martingale measure is a probability on under which is an -martingale; denotes the set of these.
A nonzero measure on with continuous distribution function bounds the bracket. Hypothesis on a set says for every ; adds a lower bound . In the UVM, and .
The capacity of a bounded continuous is , extended to all functions through lower semicontinuous majorants. A set is polar if its capacity is , and a property holds quasi-surely (q.s.) outside a polar set. is the completion of under . Elementary integrands have integrals , and is their completion for . is the space of attainable gains. The superreplication price of a claim is
Assume and that is Hölder continuous. There is a set of martingale measures satisfying such that
for every bounded continuous of the form , or , with (and the cylindrical ) bounded continuous. The goal leaves unspecified, as the paper does.
In attack order: the transfer of a.s. inequalities to q.s. ones (Lemma A.7); the pathwise moment bound q.s. (Proposition 2.9) and its price form (Proposition 2.13); a universal bracket (Lemma 2.10) approximated by realized variance (Lemma 2.14); weak duality (Lemma 2.15); the representation over probabilities on the Stone–Čech compactification (§5, p. 19) and the Cauchy–Schwarz inequality for (Lemma 4.3); the martingale property and continuity of under each (Proposition 5.2); the bracket bounds for the induced law (Lemma 5.3); membership of the three claim families in the class of with (Lemmas 5.4–5.6); and Theorem 3.1 for the literal class .
Further statements: Theorem 6.1 (all martingale measures with form a valid ), Proposition 3.2 (the case ), Proposition 2.12 (measures not charging polar sets inherit the bracket bounds), Theorem A.8 (closedness of under ).
The theorem identifies the cheapest model-free hedge of path-dependent European claims (cylindrical payoffs, Asian-type averages, lookbacks on the maximum) with a worst-case expectation over martingale laws obeying the same bracket bounds. Theorem 6.1 specializes it to the generalized UVM, where the dual set is all martingale measures with ; the paper notes this is new even for the Lebesgue case. The result supplies a rigorous non-dominated duality on which robust pricing bounds and -expectation pricing rest.
The theorem is proved in the paper; no part of it is machine-checked. A formalization would produce the first Lean development of a capacity on path space, of a quasi-sure stochastic integral, and of a continuous-time quadratic variation on the canonical space. These objects are absent from Mathlib, which has discrete- and continuous-time martingales, the Stone–Čech compactification and the Riesz–Markov–Kakutani theorem, but no stochastic integral.
The family is not dominated, so neither the Itô integral of a single model nor a common null set is available: every inequality obtained under one by the Itô formula must be lifted to a quasi-sure one, and every limit taken in the capacity. The natural dual argument (Hahn–Banach on ) produces linear forms whose representation as measures on is not available because need not be all of . The paper's route works on bounded continuous claims and compactifies; the price is that the dual measures live on , where is unbounded and must be extended by truncation, and the identity linking back to holds only for a class of claims that has to be checked family by family.
is a subtype of C(Set.Icc 0 T, ℝ) (paths with ) with the Borel -field of the sup-norm topology. Distribution functions are continuous StieltjesFunctions vanishing at and positive at . The quadratic variation is a predicate: an adapted process with -a.s. continuous nondecreasing paths from such that is a martingale. The capacity takes values in with the Appendix's Lebesgue extension; q.s. means outside a set of capacity zero. , and are membership predicates on functions. is the image of the completion . and every supremum are extended reals. is Mathlib's StoneCech, and is the set of Borel probabilities on it dominated by on .
Standing assumptions, stated as hypotheses: on for all §2 results, where the page assumes it, and Hölder continuity of for every result of §4–§5 and the goal (p. 12: "From now on, we assume that is Hölder continuous"). The goal replaces the class , which is defined only inside the proof, by the three families of Lemmas 5.4–5.6. The literal form is a milestone. Lemma 2.14 adds . Lemma 5.3 is stated for the law on .
The following trivializing formalizations are ruled out. An empty with a real-valued would make the goal ; here both sides are . Defining q.s. as "a.s. for every " would make Lemma A.7 a tautology. Replacing by the closure of elementary integrals would shrink . Dropping the martingale condition from the quadratic-variation predicate would make satisfiable by any deterministic process.
A complete development needs Itô's formula and the Burkholder–Davis–Gundy inequalities for continuous martingales, Doob–Meyer uniqueness, a Kolmogorov continuity criterion, and the theory of regular Choquet capacities. These are reusable well beyond this mission, and contributions of any of them are welcome.
Large call centers, cloud server farms and hospital wards are modeled as many-server queues: identical servers, customers arriving according to a counting process, each customer served by one server for a random time drawn from a distribution , and customers who find all servers busy waiting in a first-come first-served queue. When is large, the number of customers is of order and the natural object of study is the fluid limit, obtained by dividing all quantities by and letting . For exponential service times the fluid limit is a finite-dimensional ordinary differential equation. For a general service distribution — and call-center data show service times far from exponential (lognormal, in Brown et al., 2005) — the state must record how long each customer in service has been served, and the fluid limit is a measure-valued process.
Kaspi and Ramanan (Ann. Appl. Probab. 21 (2011) 33–114) characterize this limit by a pair of fluid equations for general with a density, prove that they have at most one solution, show that the scaled -server processes converge to it, and describe its long-time behavior. This mission is the last of these results: in the critically loaded fluid system, every solution converges to equilibrium.
Timeline. Whitt (2006) introduced a fluid model of the many-server queue with general service times and abandonment, and stated the case of property (1) of the goal theorem without proof (his Theorem 7.3). Kaspi and Ramanan (2011) gave the measure-valued formulation with the age process, uniqueness and existence of fluid solutions, and the convergence to equilibrium formalized here. Reed (2009) treated the related queue in the Halfin–Whitt regime.
The service distribution has a density , is carried by , and has mean one: . Let , and let be the hazard rate on .
The fluid state at time is a number , the scaled number of customers in system, and a measure on of total mass at most one: is the scaled number of customers in service whose age (time already spent in service) lies in . The input is a nondecreasing càdlàg arrival function with , an initial number and an initial age measure , satisfying (servers are idle only when nobody waits). The set of such triples is .
A càdlàg pair solves the fluid equations if the cumulative departures are finite, the entries into service satisfy the transport equation
for every compactly supported test function on (ages grow at unit rate, customers leave at rate , new customers enter at age ), mass is conserved, , and the system is non-idling, .
The equilibrium measure is on , a probability measure by the mean-one normalization. With (arrival rate equal to the total service capacity), and is a constant solution. Assumption 2 asks that be bounded or lower semicontinuous near . The renewal measure of is , the unit mass at included.
Under Assumption 2:
Theorem 3.9(2) is the stability statement of the fluid model in the critically loaded case: whatever the initial occupancy and the initial ages, the age distribution of customers in service converges to the stationary excess distribution of . It justifies using as the operating point around which diffusion approximations of many-server queues are built, and it is the fluid counterpart of the classical fact that the age of a stationary renewal process has density . Part (1) gives the transient behavior of an underloaded or critically loaded system started empty.
The result is proved in the paper; nothing here is open. To our knowledge none of it has been formalized. A formalization adds machine-checked statements of a measure-valued fluid model that the companion mission (uniqueness of fluid solutions, Theorem 3.5) shares, and exercises renewal theory — the renewal measure, a key renewal theorem for laws with a density, Lorden's inequality — in a form usable by other queueing developments.
The naive argument would show that is given by an explicit formula and pass to the limit. The explicit age representation of a solution involves , which is known only through a renewal equation whose forcing term depends on itself; there is no closed form unless the system never fills up. For the system can alternate between full and not full, and the convergence must be proved without knowing when. Two ingredients carry the weight: a comparison showing that the occupancy tends to one, and a key renewal theorem for the backward recurrence time of a renewal process with a density, which needs total-variation rather than vague convergence because the test functions are only bounded and continuous. The uniform-in-time control of Lemma 6.3 is where the second moment enters.
Everything lives in ManyServerFluid.Equilibrium. The service law is a structure holding the density with , on , , and mean one. Time is , read on . Age measures are Mathlib FiniteMeasure ℝ carried by , with the weak topology, so "càdlàg" is in the paper's topology. The departures are lower integrals in ; and are Lebesgue–Stieltjes measures. The convolution powers are the published QueueingFundamentals.MG1.convPow.
Explicit choices, each also stated in the item that uses it:
Weak convergence in Theorem 3.9(2) is against all bounded continuous functions, not compactly supported ones; vague convergence would let mass escape towards and is not the theorem. The monotonicity in part (1) is part of the statement. A formalization in which these were dropped, or in which omitted the unit mass at , would state a different result.
Existence. The paper's proof of Theorem 3.9(2) compares an arbitrary solution with the solution started empty, which it obtains from its Theorem 3.7 (existence via the -server limit); that theorem is not part of this series. Here every solution is a hypothesis, so nothing false is stated, but a proof of the goal must construct the empty-start solution for . It is explicit: has density on while , and from on it equals (Proposition 6.1, Remark 3.8, Lemma 3.4).
Contributions welcome: general renewal theory (local finiteness of , Lorden's inequality, the key renewal theorem for spread-out laws in total variation), and lemmas on the fluid equations shared with the uniqueness mission (the monotonicity of , the renewal equation (4.5), the age representation (3.11)).
Affine processes are Markov processes whose Laplace transform depends exponential-affinely on the initial state. On the cone of positive semidefinite matrices they model stochastic covariance matrices in multivariate stochastic volatility, interest-rate and credit models. Examples include the Wishart process of Bru (Bru 1991) and Ornstein–Uhlenbeck processes driven by matrix Lévy subordinators (Barndorff-Nielsen and Stelzer 2007, reference [3] of the paper). Cuchiero, Filipović, Mayerhofer and Teichmann (2011) characterize all affine processes on by admissible parameter sets.
On the canonical state space , Duffie, Filipović and Schachermayer (2003) showed that regular affine processes are exactly the infinitely decomposable Markov processes: the law started at is a -fold convolution of laws started at the . That property drives their existence proof. On with it fails. The Wishart marginals are not infinitely divisible, a classical result of Paul Lévy. This mission formalizes the exact characterization: Theorem 2.9 of Cuchiero et al.
is the space of real matrices and the symmetric ones. carries the pairing and the norm . is the closed convex cone of positive semidefinite matrices, and its one-point compactification. The point is the cemetery, where a killed process goes.
A transition family consists of sub-stochastic kernels on satisfying and the Chapman–Kolmogorov equations. It is stochastically continuous if weakly as . The process is affine (Definition 2.1) if there are and with
Theorem 2.4 of the paper attaches to every affine process a unique admissible parameter set . In it, is the diffusion parameter, the constant drift, and the killing rates, and and the jump measures. The exponents solve the generalized Riccati equations , , with given by (2.16)–(2.17).
The canonical space consists of paths that stay at once they reach it, with coordinate process . is the set of families of laws on under which is a stochastically continuous Markov process with . The convolution is the image of under . A family is infinitely decomposable (Definition 2.7) if for every there is with . It is infinitely divisible if every marginal is.
For and , the following are equivalent:
The theorem separates two classes that coincide on . On with , a diffusion component, which must satisfy , is incompatible with taking -th roots, because the root would need drift . So the existence proof of Duffie–Filipović–Schachermayer, which builds a process from infinitely divisible kernels, covers exactly the pure-jump affine processes on . Processes with a diffusion part need the martingale-problem approach of the paper's §5. Proposition 5.11 gives the alternative existence proof for (§5.3).
The theorem is proved in the paper. As far as is known, none of it has been machine-checked: no formal library has affine processes on matrix cones, convolution of path measures, or the Lévy–Khintchine form on . Formalization contributes a checked equivalence that rests on the paper's other main theorem (Theorem 2.4), together with reusable statements about Cauchy's equations on cones and Laplace functionals of Markov families. It is the third mission of a series. Missions I and II formalize the two halves of Theorem 2.4.
The equivalence links three layers: path-space laws, one-dimensional kernels, and Riccati exponents. (i) (ii) first needs the multiplicative structure of Laplace functionals in the initial state. That gives affinity of the process and of each -th root, with exponents . Then it needs the fact that the root's parameter set is and is again admissible, so for all . The second step relies on the full necessity theorem, in particular Proposition 4.18. The first fails without strict positivity of the Laplace functional: Cauchy's exponential equation has non-exponential solutions that vanish somewhere (Remark 6.3). (ii) (iii) requires every Riccati solution to stay in the Lévy–Khintchine cone. This is clear for finite-variation jumps via Picard iteration, but the general case needs the approximation . (iii) (i) must produce a Markov family of -th roots on path space, not merely roots of each marginal. The case shows that cannot be dropped: there the Cox–Ingersoll–Ross process has and is infinitely decomposable.
Fin d → Fin d → ℝ, with and . is the subtype of matrices with Mathlib's PosSemidef.OnePoint of the cone, with its Borel σ-algebra. Addition is extended with absorbing. is the space of all paths with the product σ-algebra; every notion in the theorem depends only on finite-dimensional distributions. Absorption at and the Markov property with transition family are imposed through finite-dimensional distributions. The path-sum map is measurable, which is checked in Lean, so the convolution is a genuine push-forward.A multistage stochastic program chooses decisions over time periods while a random input is revealed one stage at a time; the decision at stage may use what has been observed so far and nothing more. Such models are used for capacity expansion, hydro-thermal power scheduling, asset–liability management and production planning. In practice the true input process is never used directly: it is replaced by an estimate, a discretization or a scenario tree with few branches, and the program is solved for that approximation. Whether the optimal value of the approximate program is close to the true one is therefore the basic question behind every scenario-tree method.
For two-stage programs () the answer is classical: the optimal value is Lipschitz continuous with respect to suitable distances of probability distributions (Rachev and Römisch, 2002). For that methodology breaks down, because the multistage objective depends on conditional expectations given the past, and hence on the information structure of the input, not only on its distribution. Heitsch, Römisch and Strugarek (SIAM J. Optim. 2006) showed that the gap is closed by adding one more term: a distance between the filtrations generated by the true and the approximate inputs. Their estimate is the basis of later work on scenario-tree construction and on the nested distance of Pflug and Pichler.
Let be a probability space and a process with . The information available at stage is , and is the σ-field it generates; is deterministic, so . The linear multistage program (1) is
where is a polyhedron, for are polyhedral cones, and are fixed matrices, and the costs and right-hand sides are affine functions of the current input . Write for the objective and for the feasible set.
Which data are random fixes two integrability exponents: if only the costs are random, and ; if only the right-hand sides are random, ; otherwise . The input lives in and the decisions in , and is the distance of two inputs.
Three conditions are imposed: (A1) complete fixed recourse, for ; (A2) is finite and is level-bounded locally uniformly at : for some there are and a bounded set such that the level set is nonempty and contained in whenever ; (A3) .
The filtration distance at stage compares how well a near-optimal decision of one problem is predicted from the other problem's information:
Under (A1)–(A3) and boundedness of there are positive constants , , such that
for every input with and finite. The constants are existential: the theorem asserts the shape of the estimate, not its numerical values.
The theorem identifies what an approximation of a multistage input must preserve: closeness in alone is not enough, and the filtration term measures exactly the information that is lost or gained. It justifies scenario-tree construction by forward selection and reduction (Heitsch and Römisch, 2009), where both terms are controlled, and it is the precursor of the nested distance, for which analogous Lipschitz bounds are proved. Without such an estimate a scenario tree that matches the marginal distributions can still give an arbitrarily wrong optimal value.
The result is proved in the paper; it has not been formalized. A machine-checked version needs, and would produce, a formal theory of linear programs with decisions adapted to a generated filtration in spaces, Lipschitz continuity of polyhedral set-valued maps, and measurable selections of conditional-expectation projections. Each of these is reusable well beyond this paper.
The obvious argument — take a near-optimal policy for and evaluate it for — fails at once: that policy is adapted to , not to , so it is not feasible for the perturbed problem, and projecting it by conditional expectation onto destroys the equality constraints. Any repaired policy must again be -measurable at every stage, and an error made at stage propagates to all later stages through the recursion , where it must stay controlled in the right norm. The three integrability regimes need separate estimates; in the regime the error must be bounded essentially, not only on average.
The program is encoded in a single definitions file. Stages are natural numbers with dimension functions , . is given by finitely many linear inequalities and each , , by finitely many homogeneous ones, so "polyhedral" and "polyhedral cone" are built in. The matrices are linear maps between Euclidean spaces; and . A randomness pattern (costs, rhs, both) carries the exponents and its restriction on the data: for costs, for rhs, none for both.
The committed conventions are:
condExp;Trivializing formalizations are ruled out: the constants , , are quantified before ; the theorem covers all three randomness patterns; the level sets are nonempty, so the suprema are not vacuous; and a sorry-free check exhibits data satisfying (A1) with a feasible policy, so the hypotheses are satisfiable.
Contributions are welcome on Lipschitz continuity of polyhedral set-valued maps (Walkup–Wets), measurable selections, conditional expectation of set-constrained random vectors, and any of the case estimates.
A mathematical program with complementarity constraints (MPEC, also called MPCC) is a nonlinear program in which some pairs of constraint functions must be nonnegative with at least one of each pair equal to zero. Such programs model bilevel optimization, Stackelberg games, contact problems in mechanics, and traffic equilibrium design; see Luo, Pang and Ralph, Mathematical Programs with Equilibrium Constraints (Cambridge University Press, 1996). The complementarity constraints make every standard constraint qualification of nonlinear programming fail at every feasible point: neither LICQ nor MFCQ ever holds. Off-the-shelf NLP theory and solvers therefore do not apply directly.
Relaxation methods work around this by replacing the MPEC with a family of ordinary nonlinear programs indexed by a parameter and letting . The oldest of these is the global relaxation of Scholtes (SIAM J. Optim. 11, 2001). The relaxed programs are only useful if they are themselves well posed: a local minimizer of a relaxed program should carry Lagrange multipliers, so that the sequence of KKT points the method computes actually exists. Hoheisel, Kanzow and Schwartz (Preprint 299, Univ. Würzburg, 2010; published in Mathematical Programming) compare five relaxation schemes, prove convergence under weaker MPEC constraint qualifications than before, and ask which standard constraint qualification the relaxed programs satisfy. This mission formalizes their answer for Scholtes' scheme, Theorem 3.2.
A standard nonlinear program (2) on minimizes subject to and for finitely many and . At a feasible , the active set is . A family is positive-linearly dependent if some combination vanishes with and not all coefficients zero. The Mangasarian–Fromovitz constraint qualification (MFCQ) holds at if the gradients are linearly independent and some direction has for every active and for every .
The MPEC (1) minimizes subject to
with continuously differentiable data. At a feasible point the indices of the complementarity pairs split into (), () and (). The tightened program TNLP replaces each pair by equalities on the components that vanish at and a sign constraint on the other. MPEC-MFCQ holds at if standard MFCQ holds for TNLP at .
Scholtes' relaxed program , for , keeps , , , and replaces by . Its feasible set is . Lean notation: the MPEC is MPEC n m p l, TNLP is P.TNLP xs, is P.RS t, and MFCQ of an NLP Q at x is Q.IsMFCQ x.
If is feasible for the MPEC and MPEC-MFCQ holds at , there are a neighbourhood of and such that
The neighbourhood is fixed before and works for every .
Theorem 3.2 says that the relaxed programs inherit a standard constraint qualification from the MPEC. Consequently every local minimizer of near is a KKT point, which is exactly the hypothesis of the convergence theorem for Scholtes' method (Theorem 3.1 of the paper: limits of KKT points of are C-stationary under MPEC-MFCQ). Without it, the convergence theorem could be about sequences that do not exist. The result also replaces the MPEC-LICQ-based regularity results of earlier work by the weaker MPEC-MFCQ.
The theorem is proved in the paper; to our knowledge no part of this theory has been machine-checked. A formal development delivers a reusable layer for nonlinear programming in Lean: positive-linear dependence, MFCQ and its dual characterization, the tightened program of an MPEC and the MPEC constraint qualifications. Sibling missions of this series formalize Theorem 3.1 and the Kadrani–Dussault–Benchakroun relaxation (Theorem 3.5) on the same vocabulary.
The obvious argument is a continuity argument: MFCQ is an open condition, so it should persist near . This fails as stated, because MFCQ for is not a perturbation of MFCQ for TNLP: the two programs have different constraints, and the active set of at changes with and . Near a biactive index , the product constraint can be active, and its gradient tends to zero as . So it cannot be treated as a small perturbation of any gradient in the TNLP family. In addition, the neighbourhood must be uniform in , while the active product constraints depend on . The step that needs care is the regrouping of the multiplier equation of into a combination of TNLP-type gradients, with every coefficient's sign accounted for. The separate step from MPEC-MFCQ to positive-linear independence needs a theorem of the alternative (Motzkin's transposition theorem), which is not in Mathlib in this form.
EuclideanSpace ℝ (Fin n); is the inner product of gradient f x with d. Indices are Fin m (0-based), and are allowed.P.IsC1 on the goal and on milestones 3–5. Milestones 1–2 do not need it.𝓝 xs chosen before .The goal would be trivialized by a weakened MFCQ, for instance one that omits the linear independence of the equality gradients or requires the strict inequality only for some of the active constraints. Such a formalization is ruled out: IsMFCQ requires both conditions, over the full active set of . The neighbourhood must be a genuine element of 𝓝 xs, so an empty is excluded.
Welcome contributions: a proof of Remark 2.2, general lemmas on persistence of positive-linear independence under continuous perturbation, and the final assembly. These lemmas apply to nonlinear programming in general, not only to this mission.
Affine maximal graphs satisfy a nonlinear fourth-order geometric equation. The target asks whether completeness forces such a locally uniformly convex graph to be a paraboloid. The pinned manuscript supplies the research context.
The dimension is between three and nine. The domain is nonempty, open and convex, the function is smooth with positive-definite Hessian, and completeness uses intrinsic Euclidean graph length.
The selected goal is OAI.AffineBernstein.affine_bernstein. Its central assertion is
The theorem states that, for every integer dimension 3 ≤ n ≤ 9, a nonempty open convex set Ω ⊆ ℝⁿ and a function u : ℝⁿ → ℝ that is smooth on Ω satisfy the following conclusion under three hypotheses. First, the Hessian H = D²u is positive definite at every point of Ω. Second, u satisfies the affine maximal equation ∑ᵢⱼ Uᵢⱼ ∂ᵢ∂ⱼw = 0 throughout Ω, where U = (det H)H⁻¹ and w = (det H)^{−(n+1)/(n+2)}. Third, the graph is complete for its intrinsic Euclidean path distance: the distance between x and y in Ω is the infimum over C¹ paths γ in Ω joining them of ∫₀¹ √(‖γ′(t)‖² + (Du(γ(t))γ′(t))²) dt, and every Cauchy sequence for this distance has a limit in Ω for the same distance. Then Ω = ℝⁿ and there exist a symmetric positive definite real n × n matrix A, a vector b ∈ ℝⁿ, and c ∈ ℝ such that u(x) = ½xᵀAx + b·x + c for every x ∈ ℝⁿ. Moreover, an invertible affine map of ℝⁿ × ℝ carries the standard paraboloid {(x, ‖x‖²)} onto the graph {(x, u(x)) : x ∈ Ω}.
The goal also gives an invertible affine map from the standard paraboloid to the graph. The wider immersed-hypersurface formulation is not included as a separate target. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The domain is not initially assumed to be all of space. Both global domain exhaustion and the quadratic form must follow from the equation and completeness.
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.
adc7f1241b42. Selected goal source.Nodal sets are the zero loci of Laplace eigenfunctions. Their size probes how geometry constrains high-frequency oscillation. The pinned manuscript supplies the research context.
The encoded manifold is S4×S1 with one smooth Riemannian metric. The sequence consists of nonzero smooth real eigenfunctions with positive eigenvalues tending to infinity.
The selected goal is OAI.Yau.Target.yau_nodal_set_upper_bound_counterexample. Its central assertion is
The theorem states that the defined proposition MainTarget holds, i.e. that there exist a smooth Riemannian metric g on the 5-manifold S⁴ × S¹ (the unit sphere in ℝ⁵ times the circle, modelled on ℝ⁴ × ℝ¹), a sequence of positive reals λₖ, and a sequence of smooth real functions uₖ on this manifold, each not identically zero, such that the following hold. At every point x, in the extended chart at x, the coordinate Laplacian of uₖ, namely (1/√det G) Σᵢ ∂ᵢ(√det G Σⱼ Gⁱʲ ∂ⱼ(uₖ∘chart⁻¹)), where G is the matrix of g in the chart's coordinate frame and Gⁱʲ its inverse, satisfies −Δ_g uₖ(x) = λₖ uₖ(x), so each uₖ is a Laplace eigenfunction with eigenvalue λₖ. Moreover λₖ → ∞, and the 4-dimensional Hausdorff measure (taken with respect to the distance induced by g) of the nodal set {uₖ = 0}, divided by √λₖ, tends to +∞ as k → ∞. Thus the nodal-set size grows faster than the order √λₖ, which is a counterexample to a Yau-type upper bound on nodal sets in this setting. The theorem is admitted in the source and not proved there.
The selected target is divergence relative to the square-root eigenvalue scale. It does not specify the fixed additional power ε0 asserted by the manuscript title and abstract. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The same smooth metric must support the whole eigenfunction sequence, and the nodal measure uses the distance induced by that metric.
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.
adc7f1241b42. Selected goal source.A symplectic form can be positive on complex lines without being invariant under the almost complex structure. The target asks whether some compatible form nevertheless exists in four dimensions. The pinned manuscript supplies the research context.
The manifold is smooth, compact, connected, Hausdorff and second countable, modeled on real four-space. The almost complex structure squares to minus the identity.
The selected goal is OAI.TamingCompatibility.taming_implies_compatibility. Its central assertion is
The theorem states that, for a smooth manifold X modeled on four-dimensional Euclidean space ℝ⁴ (charted with smooth transition maps) that is Hausdorff, second countable, compact and connected, and for an almost complex structure J on X, if some symplectic two-form α tames J, then there exists a symplectic two-form η that is compatible with J. Here a two-form assigns to each point x a continuous alternating real bilinear form on the tangent space at x, and an almost complex structure J is a smooth field of continuous linear endomorphisms of the tangent spaces with J(Jv) = −v for every tangent vector v. A two-form is symplectic when it is smooth (its pullbacks along smooth maps from open subsets of ℝ⁴ are smooth), closed (the exterior derivative of each such pullback vanishes), and nondegenerate (a tangent vector v with α(v,w) = 0 for all w must be zero). The form α tames J when α(v, Jv) > 0 for every nonzero tangent vector v at every point. The form η is compatible with J when it tames J and is J-invariant, meaning η(Ju, Jv) = η(u, v) for all tangent vectors u and v at every point. This is a formal statement admitted without proof.
The conclusion supplies a possibly different symplectic form. It does not assert that the original taming form is compatible or prescribe its cohomology class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
A pointwise compatibility adjustment need not preserve closedness. The conclusion requires both global symplectic structure and positivity.
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.
adc7f1241b42. Selected goal source.Sharp filling inequalities compare the mass of a cycle with the least mass needed to fill it. The selected formulation extends a Euclidean coefficient to proper CAT(0) metric spaces. The pinned manuscript supplies the research context.
Integral currents are encoded metric currents with integer-multiplicity chart decompositions and integral boundary. The input is a compactly supported n-cycle for n at least two. In the displayed coefficient, σ_n=(n+1)ω_{n+1}, where ω_{n+1} is the Euclidean volume of the unit ball in dimension n+1; this is the published sphereArea convention.
The selected goal is OAI.CAT0Fillings.sharp_integral_filling. Its central assertion is
The theorem states that, for a proper metric space X with its Borel σ-algebra that is CAT(0), meaning there is a choice of geodesic parametrization segment(x,y,t) from x to y (with segment(x,y,0)=x, segment(x,y,1)=y, and dist(segment(x,y,s),segment(x,y,t))=|s−t|·dist(x,y) for s,t in [0,1]) satisfying the comparison inequality dist(segment(o,x,s),segment(o,y,t))² ≤ (s·d(o,x) − t·d(o,y))² + s·t·(d(x,y)² − (d(o,x) − d(o,y))²), the following filling property holds for every integer n ≥ 2. Let T be an integral n-current on X, that is, a metric current (a multilinear functional on a bounded Lipschitz function and n Lipschitz functions, with locality, continuity and finite mass) that is a countable sum of disjointly supported integer-multiplicity bi-Lipschitz chart pieces and whose boundary has the same properties, and suppose T is compactly supported and a cycle, meaning its boundary is zero. Then there exists a compactly supported integral (n+1)-current S on X whose boundary is T and whose mass satisfies mass(S) ≤ c_n · mass(T)^((n+1)/n), where c_n = 1/((n+1)·(σ_n)^(1/n)), σ_n = (n+1)·ω_{n+1} is the area of the unit n-sphere and ω_{n+1} is the volume of the unit ball in Euclidean (n+1)-space. This is an admitted theorem statement, not a verified proof.
The goal is the CAT(0) integral-current filling inequality. Euclidean coefficient optimality is an additional reference. The manifold perimeter comparison and equality-rigidity statements in the manuscript are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The sharp coefficient must hold without a smooth manifold model, while preserving integrality, compact support and the exact boundary.
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:
adc7f1241b42. Selected goal source.Uniqueness of irreducible representations is a strong condition on a C*-algebra. The target asks for a counterexample to the expected compact-operator characterization without added set-theoretic hypotheses. The pinned manuscript supplies the research context.
Representations are nonzero star homomorphisms on complete complex inner product spaces. Irreducibility is expressed by closed invariant subspaces, and equivalence by an intertwining linear isometry.
The selected goal is OAI.NaimarkZFC.main. Its central assertion is
The theorem states that, for every universe level choice, there exists a type A carrying a C*-algebra structure (over ℂ) with the following five properties. First, A is simple in the sense that it is nontrivial and its only closed two-sided ideals are {0} and A itself. Second, A is not finite-dimensional as a complex vector space. Third, there is a continuous linear functional τ : A → ℂ that is a faithful tracial state: τ has norm 1, τ(aa) is a nonnegative real number for every a, τ(ab) = τ(ba) for all a and b, and τ(aa) > 0 whenever a ≠ 0. Fourth, A has a unique irreducible representation up to unitary equivalence: whenever π and ρ are nonzero star-homomorphisms (non-unital algebra homomorphisms preserving star) from A into the bounded operators on complete complex inner product spaces H and K, taken in the stated universe levels, and each has no closed invariant subspace other than 0 and the whole space, there is a linear isometric isomorphism U : H → K with U(π(a)x) = ρ(a)(Ux) for all a and x. Fifth, for every complete complex inner product space H in the stated universe, A is not isomorphic to the algebra of compact operators on H, meaning there is no injective star-homomorphism φ : A → B(H) whose range is exactly the set of compact operators on H.
The target explicitly requires simplicity, infinite dimension, a faithful tracial state and failure of all compact-operator isomorphisms in the stated universes. No additional set-theoretic hypothesis appears in its binders. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The construction must combine infinite dimension, a faithful trace and uniqueness across the specified representation universes.
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.
adc7f1241b42. Selected goal source.Hochschild cohomology measures whether a cocycle equation admits a primitive. In an operator algebra the boundedness requirement is part of the mathematical problem. The pinned manuscript supplies the research context.
Cochains are continuous complex multilinear maps into the von Neumann algebra itself, with its natural left and right multiplication actions.
The selected goal is OAI.BoundedHochschild.KadisonRingrose.main_result. Its central assertion is
The theorem states that, for a complex von Neumann algebra M (a C*-algebra with a partial order making it star-ordered, equipped with the W*-algebra structure), and any natural number n, every bounded Hochschild cocycle of degree n+2 with values in M is a coboundary. Here a cochain of degree m is a continuous complex m-linear map from M^m to M. The Hochschild differential of a cochain f of degree m, evaluated at (v_0,...,v_m), is v_0 f(v_1,...,v_m) plus the sum over j from 0 to m-1 of (-1)^(j+1) f(v_0,...,v_j v_{j+1},...,v_m), where the j-th and (j+1)-th inputs are multiplied into one, plus (-1)^(m+1) f(v_0,...,v_{m-1}) v_m. The hypothesis is that f has degree n+2 and its differential vanishes at every (n+3)-tuple of elements of M. The conclusion is that there exists a continuous multilinear cochain g of degree n+1 whose differential equals f at every (n+2)-tuple of elements of M.
The goal covers every natural n, hence degrees at least two. It does not include a separately referenced degree-one inner-derivation theorem. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
An algebraic primitive is insufficient: the lower-degree cochain must remain continuous and bounded in the encoded operator-norm sense.
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.
adc7f1241b42. Selected goal source.Quasitraces behave linearly on commutative subalgebras but need not initially be additive on all positive elements. A uniform defect on a fixed pair would separate them from traces. The pinned manuscript supplies the research context.
The algebra is separable and carries a normalized 2-quasitrace, meaning a quasitrace with the specified extension to two by two matrices. The witnesses are positive contractions.
The selected goal is OAI.Kaplansky.kaplansky_quasitrace_counterexample. Its central assertion is
The theorem (admitted in the source, not proved there) states that there exists a separable C*-algebra A, with its complex C*-algebra structure, for which the following hold. First, A carries a normalized 2-quasitrace. Here a 1-quasitrace is a function τ : A → ℂ such that τ(xx) is a nonnegative complex number for all x; τ(xx) = τ(xx*); τ(h + i k) = τ(h) + i τ(k) for self-adjoint h and k; and the restriction of τ to every norm-closed commutative (non-unital) star-subalgebra over ℂ is ℂ-linear. It is normalized if τ(1) = 1, and it is a 2-quasitrace if it extends to a 1-quasitrace σ on the 2×2 matrices over A (as a C*-matrix algebra) satisfying σ of the matrix with a in the upper-left corner and zeros elsewhere equal to τ(a) for all a. Second, there are positive contractions a and b in A, meaning each is of the form x*x and has norm at most 1, such that every normalized 2-quasitrace τ on A satisfies Re(τ(a+b) − τ(a) − τ(b)) ≥ 1/144. So no such τ is additive on this pair.
The selected goal is the quantitative quasitrace counterexample. The stable-finiteness and tensor-product consequences are retained as a separate published bundle. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The same positive contractions must exhibit the defect for every normalized 2-quasitrace, while at least one such quasitrace exists.
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:
adc7f1241b42. Selected goal source.Norm ultrapowers permit approximations along a free ultrafilter. An explicit algebra excluded from every nuclear target ultrapower tests the limits of this embedding mechanism. The pinned manuscript supplies the research context.
The group is the stated dyadic semidirect product. Its full group C*-algebra is specified by a universal property, and the ultrapower is bounded sequences modulo norm-null sequences along the ultrafilter.
The selected goal is OAI.NuclearUltrapower.main_no_embedding. Its central assertion is
The theorem states that, working in universe level 0, there exist a nonzero unital complex C*-algebra A and a group homomorphism ι from G into the unitary group of A such that the following hold. Here G is the semidirect product of the additive group of 3-vectors over the dyadic rationals Z[1/2] by SL₃(ℤ) × ℤ, where a matrix acts linearly on the vectors and the integer n acts by multiplication by 2ⁿ. First, (A, ι) is the full group C*-algebra of G: the span of ι(G) is dense in A, and every homomorphism of G into the unitaries of a nonzero unital C*-algebra D extends uniquely to a unital -homomorphism A → D. Second, A is separable as a topological space. Third, for every nonzero unital C-algebra B that is nuclear in the tensor-norm sense (minimal and maximal C*-tensor norms agree on B ⊗ C for every C*-algebra C) and every free ultrafilter ω on ℕ (one containing no finite set), there is no injective unital -homomorphism from A into the norm ultrapower of B, namely bounded B-valued sequences modulo those tending to 0 along ω. Fourth, there exist a nonzero unital C-algebra O and two elements s₀, s₁ of O satisfying the Cuntz relations (each sᵢsᵢ = 1 and s₀s₀ + s₁s₁* = 1), with O universal for these relations, such that for every free ultrafilter ω there is likewise no injective unital *-homomorphism from A into the norm ultrapower of O. The theorem is admitted in the source, not proved.
The goal includes separability, the full group universal property, nonembedding and the Cuntz-algebra corollary in the stated base universe. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
A single source algebra must obstruct all nuclear targets and free ultrafilters. Universal full-group and Cuntz-algebra constructions are part of the target.
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.
adc7f1241b42. Selected goal source.A bounded algebra representation need not visibly preserve adjoints. The similarity problem asks whether one bounded change of Hilbert-space coordinates restores that structure. The pinned manuscript supplies the research context.
Representations are continuous unital complex algebra homomorphisms into bounded operators on a complete complex inner product space. The conjugating operator must have a bounded inverse.
The selected goal is OAI.KadisonSimilarity.similarityTheorem. Its central assertion is
The theorem states that, for every C*-algebra A in universe u and every complex inner product space K in universe v that is complete (a Hilbert space), every bounded unital representation of A on K is similar to a star representation. Here a bounded unital representation is a continuous ℂ-algebra homomorphism π from A into the algebra of bounded linear operators on K; being an algebra homomorphism of unital algebras, it preserves the identity. Similarity to a star representation means that there is an invertible bounded operator S on K, with bounded inverse, such that for every a in A, S π(a*) S⁻¹ equals the adjoint of S π(a) S⁻¹. Equivalently, the conjugated map a ↦ S π(a) S⁻¹ commutes with the involution. This is the Kadison similarity statement as a defined proposition SimilarityTheorem, and the source declares it as a theorem whose proof is admitted rather than supplied.
Similarity is the selected goal. The two commutator formulations and explicit hyperreflexivity estimate remain distinct references with their own constants and universes. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
One operator S must work simultaneously for every algebra element. Uniform matrix-amplification estimates cannot acquire a dimension-dependent constant.
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.KadisonSimilarity.universalCommutatorTheorem (Open).OAI.KadisonSimilarity.universalHyperreflexivity (Open).OAI.Kadison.uniform_commutator (Open).adc7f1241b42. Selected goal source.Group von Neumann algebras encode a free group's regular representation as an operator algebra. Whether the rank remains visible in that algebra is the motivating isomorphism problem. The pinned manuscript supplies the research context.
The parameter runs over extended nonnegative reals greater than one. Integer ranks use group factors, infinity uses countably many generators, and other parameters use the encoded stabilized corner model.
The selected goal is OAI.FreeGroupFactorMain.Interpolation.allInterpolatedIsomorphic. Its central assertion is
The theorem states that for any two extended nonnegative real parameters r and s, both strictly greater than 1 (so either may be infinite), the interpolated factors attached to r and s are isomorphic as C*-algebras with trace and topology, meaning the type of normal tracial equivalences between them is nonempty. The interpolated factor at a parameter is chosen by cases: for r = ∞ it is the group von Neumann algebra of the free group on countably many generators; for r equal to a natural number n it is the group von Neumann algebra of the free group on n generators; otherwise it is the corner pAp of the stabilization of the rank-two free group algebra, cut down by a selected star projection p whose stabilized projection trace is the real number 1/√(r−1), with the trace being the stabilized trace rescaled by the inverse of that value. Each carries its canonical trace or this rescaled trace and an ultraweak-type topology. A NormalTracialEquiv between two such models consists of a ℂ-linear star-algebra isomorphism that preserves the traces and is continuous in both directions for the given topologies.
The goal is a nonempty type of normal tracial equivalences between the precise interpolated models. Statements about fundamental groups are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The required equivalence must preserve the algebra, involution and trace, and be continuous in both directions for the specified topologies.
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.
adc7f1241b42. Selected goal source.Vertex operator algebras describe conformal theories algebraically, while conformal nets describe local operator algebras. Passing between them requires analytic control of fields. The pinned manuscript supplies the research context.
The selected algebra is simple, unitary, CFT-type and strongly rational. Its modes act on an inner product space, and smeared fields act on the Hilbert completion.
The selected goal is OAI.MinimalVertex.main. Its central assertion is
The theorem states that, for a CFT-type vertex operator algebra A on a complex inner product space V (a vertex algebra with vacuum, state-field map and Jacobi identity, together with a conformal vector, central charge, finite-dimensional graded pieces with degree-zero part spanned by the vacuum, conformal vector in degree 2 acting as the grading operator, and the Virasoro relations), equipped with a unitary structure U (an antilinear involution fixing the vacuum and conformal vector, compatible with all modes, together with a unit-norm vacuum and an invariance relation between a mode and the corresponding mode of the transformed adjoint-side vector), if A is simple (nonzero vacuum and no ideals other than 0 and the whole space) and strongly rational (self-contragredient, rational in the sense that every admissible weak module is completely reducible, and C2-cofinite), then three things hold. First, A has polynomial energy bounds: for every a in V there are C>0 and natural numbers p,k with ||a_(n) b|| ≤ C(1+|n|)^p ||(1+L_0)^k b|| for all integers n and all b in V. Second, the CKLW strong locality property holds: all vectors satisfy these bounds, and for every proper circle arc I the von Neumann algebra generated by closed smeared fields supported in I, built on the completion of V, lies in the commutant of the algebra attached to the complementary arc. Third, the assignment of these interval algebras to proper arcs admits the structure of an irreducible conformal net, meaning a separable Hilbert space with isotony, locality, a continuous Mobius representation extended to a continuous projective representation of smooth circle diffeomorphisms with covariance and locality of the action, a unit invariant vacuum that is unique up to scalar and cyclic, a positive self-adjoint Hamiltonian generating the rotation flow, and trivial commutant of all interval algebras apart from scalars.
The target proves polynomial energy bounds, the specified CKLW strong locality property, and existence of an irreducible conformal-net structure. Complete rationality, category equivalences and extension classification are not conclusions of this 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.
Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.
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.
adc7f1241b42. Selected goal source.A known zero-energy vector does not by itself give a uniform positive gap above it. The Laughlin problem asks for a lower bound controlling every competing antisymmetric state. The pinned manuscript supplies the research context.
At N particles set Q=3(N−1). States are complex functions on finite configurations, with antisymmetry under exchanging particles. The energy is a sum of squared pair-annihilation amplitudes.
The selected goal is OAI.LaughlinGap.thm_main. Its central assertion is
The theorem states that there is a threshold N₀ ≥ 2 such that for every N ≥ N₀ and every antisymmetric complex-valued state ψ on N particles, each with local levels 0,…,Q where Q = 3(N−1), one has (1/25)·d(ψ)² ≤ E(ψ). Here a state assigns a complex number to each configuration a : Fin N → {0,…,Q}, and antisymmetric means that swapping the values at two distinct positions i and j negates ψ. The energy E(ψ) sums, over pairs i<j, over p = 0,…,2Q−2, and over configurations a with a_i = a_j = 0, the squared modulus of the pair amplitude, which is the sum over x,y of pairCoefficient(Q,p,x,y)·ψ(a with a_i replaced by x and a_j by y). The pair coefficient vanishes unless x+y = p+1, in which case it equals (x−y)/√2 times the square root of Q^{(x)}·Q^{(y)}·p! divided by Q·(2Q−2)^{(p)}·x!·y!, where m^{(k)} is the descending factorial. The Laughlin vector is built from the polynomial ∏{i<j}(x{i,0}x_{j,1} − x_{j,0}x_{i,1})³ in variables indexed by particle and a Boolean: its coefficient at the monomial with exponent a_i on x_{i,1} and Q−a_i on x_{i,0} is divided by ∏_i √C(Q,a_i). The quantity d(ψ)² is the infimum over complex c of the sum over configurations of |ψ(a) − c·Laughlin(a)|², the squared distance from ψ to the line spanned by the Laughlin vector, with no normalization of ψ assumed.
The selected goal has constant 1/25 and no normalization requirement on the state. The Fock-space inequality, the earlier 1/100 formulation and the planar endpoint are separate references; they retain their own representations and constants. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The bound must be uniform for all sufficiently large particle numbers and for every state, rather than a variational estimate on a selected excitation.
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.Laughlin.mainTarget_proved (Open).OAI.LaughlinFock.thm_fock (Open).OAI.Laughlin.planar_gap (Open).adc7f1241b42. Selected goal source.An exterior electron count defines a radius of a neutral atom without selecting individual electrons. Its scaling tests how well Thomas–Fermi theory describes the outer region of the full interacting atom. The pinned manuscript supplies the research context.
Choose any normalized ground state for each neutral atom with N+1 electrons. The radius is the infimum of radii outside which the expected electron mass is at most m.
The selected goal is OAI.NeutralAtom.generalized_outer_radii. Its central assertion is
The theorem states that, for every choice of wavefunctions Ψ_N for neutral atoms with N+1 electrons and nuclear charge Z=N+1 (each a spin-dependent complex function of N+1 positions in three-dimensional space, with spins taking two values), such that each Ψ_N is a normalized ground state, the outer radii of the atoms obey a Thomas–Fermi-type scaling law. A normalized ground state is an antisymmetric wavefunction with a weak gradient, square-integrable in each spin component together with its gradient, with finite Coulomb integrals against |Ψ|², total squared norm 1 summed over spins, and minimal energy among all such normalized functions. The energy is half the squared L² norm of the gradient plus the expectation of the Coulomb potential, which is −Z times the sum of inverse distances of electrons to the nucleus plus the sum of inverse inter-electron distances over pairs. The electron density is N+1 times the spin-summed integral of |Ψ|² over the other N positions, and the radius for m is the infimum of r≥0 such that the density mass outside the ball of radius r is at most m. For each m, upperRadius and lowerRadius are the limsup and liminf, in the extended reals, of these radii as N→∞ with N+1>m. With bTF=(81π²/2)^(1/3), the theorem states that both m^(1/3)·upperRadius(m) and m^(1/3)·lowerRadius(m) converge to bTF as m→∞ through the natural numbers.
The target uses extended-real upper and lower radii, followed by a natural-number limit in m. No spherical symmetry is assumed, and the atom remains neutral. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The assertion must hold for every choice of ground states. The inner large-charge limsup and liminf cannot be silently replaced with an assumed pointwise limit.
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.
adc7f1241b42. Selected goal source.Removing outer electrons changes an atom's energy on a smaller scale than its total binding energy. A total-energy asymptotic alone does not determine the difference. The pinned manuscript supplies the research context.
The quantum model uses antisymmetric spin-dependent wavefunctions, two spin states, weak gradients and the full nuclear and electron-electron Coulomb interactions. The comparison is with the Thomas–Fermi density functional.
The selected goal is OAI.CoulombAtom.generalized_ionization. Its central assertion is
The theorem states that the proposition MainStatement holds: there is a real constant a>0 such that three asymptotic statements about atomic ionization energies all hold with this same a. Here the quantum energy of N electrons around a nucleus of charge Z is the infimum, taken over admissible spin-dependent wavefunctions on (ℝ³)^N, of the energy (1/2) times the total squared L² norm of all gradient components, minus Z times the expectation of Σᵢ 1/|xᵢ|, plus the expectation of Σ_{i<j} 1/|xᵢ−xⱼ|, with energy defined as 0 when N=0. Admissibility means that each spin component and each prescribed gradient component is square integrable, the gradient components are the weak partial derivatives of the values, the values are antisymmetric under simultaneous permutation of spins and positions (by the sign of the permutation, almost everywhere), the total squared norm summed over spins is 1, and the nuclear and electron-electron Coulomb densities are integrable. The ionization energy of removing m electrons from a neutral atom of charge Z is ionization(m,Z)=E(Z, Z−m)−E(Z, Z), with natural-number subtraction. The Thomas-Fermi energy tfEnergy(Z,M) is the infimum over nonnegative integrable densities ρ on ℝ³ of total mass M, with ρ^{5/3}, ρ/|x| and ρ(x)ρ(y)/|x−y| integrable, of (3/10)(3π²)^{2/3}∫ρ^{5/3} − Z∫ρ/|x| + (1/2)∬ρ(x)ρ(y)/|x−y|, and tfIonization(m,Z)=tfEnergy(Z,Z−m)−tfEnergy(Z,Z) for real m and Z. The three conclusions are: for every real m>0, tfIonization(m,Z) tends to a·m^{7/3} as the real number Z tends to infinity; for all natural-number sequences m_j, Z_j with 1≤m_j<Z_j, m_j→∞ and Z_j/m_j→∞, the ratio ionization(m_j,Z_j)/m_j^{7/3} tends to a; and as m→∞ through the naturals, both limsup and liminf over Z of ionization(m,Z), each divided by m^{7/3}, tend to a.
The main proposition includes a positive common constant, the fixed-m Thomas–Fermi limit, the joint quantum limit, and normalized limsup and liminf limits. It concerns energies rather than outer-electron radii. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Errors negligible relative to the total atomic energy can still dominate ionization energies. The common leading constant must work in the joint regime and both iterated limits.
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.
adc7f1241b42. Selected goal source.Replacing a hyperboloidal end by an asymptotically flat end can connect Bondi mass with ADM mass. The source seeks a replacement that preserves interior geometry, the energy condition, and almost all enclosing area. The source is OpenAI's September 2026 manuscript.
A CKS exterior datum describes a three-dimensional hyperboloidal end and its mass aspect. Its Bondi charge is energy-momentum , assumed strictly future timelike. An enclosing cut is a surface in the supplied geometric class; its area is computed from the metric.
For a connected, Hausdorff, second countable smooth 3-manifold N with boundary and a smooth Riemannian metric g with a smooth symmetric tensor field K, such that N is orientable, the boundary is compact and nonempty, g is complete, and (g,K) satisfies the pointwise local-chart physical dominant energy condition PhysicalDEC, the following holds. Suppose d is a CKS exterior-end datum for (g,K): a coordinate end outside radius d.chart.radius in which g and K are represented by smooth perturbations, together with a smooth mass aspect function on the sphere and the tensor patches realizing it. If the Bondi charge (energy, momentum) of d's mass aspect, (E,P), is timelike, meaning |P|<E, then there exist another such datum d', a radius R₀ with d'.chart.radius<R₀ and 12≤R₀, and a function ε with ε(R)→0 as R→∞, such that d' has Bondi charge (√(E²−|P|²),0), and the minimal enclosing area of g is finite. Moreover, for every R≥R₀ one has 0≤ε(R)<1 and there are a complete smooth metric gR, a smooth symmetric tensor field kR, spatial tensor fields G and k on Euclidean 3-space, and a number η with these properties. The pair (gR,kR) agrees with (g,K) at every point outside the chart domain or with chart coordinate norm at most R, and satisfies PhysicalDEC and integrable constraints. Also gR≥(1−ε(R))g as quadratic forms. On the end, gR and kR equal the end metrics built from G and k in d'.chart. Each Cartesian component of G minus the identity satisfies the order-1 Symbol condition from CKSADM, and k vanishes where ‖x‖>2R². As r→∞ the spatial ADM energy of G tends to √(E²−|P|²)+η and the ADM momentum of (G,k) tends to 0, with 0≤η≤2R^(−1/2). Finally, gR has finite minimal enclosing area, (1−ε(R)) times the minimum enclosing area of g is at most that of gR, and for every outer domain D the cut areas of g and gR are finite and satisfy (1−ε(R))·cutArea(g,D)≤cutArea(gR,D).
The goal is OAI.CKSSourceExterior.area_controlled_end_replacement. Supporting targets are listed below; they retain their individual hypotheses and are separate statements.
The selected goal constructs end replacements with zero limiting ADM momentum and quantitative area comparison, including minimum enclosing area. The Schwarzschild equality examples are attached as a separate target. 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.
Changing the end can create a cheaper enclosing surface or violate the dominant energy condition. Agreement on each retained interior region does not alone prevent either problem.
The manifold is a connected Hausdorff second-countable smooth three-manifold with compact nonempty boundary, and the original complete data satisfy the physical dominant energy condition. The main target is end replacement; it does not itself state the final Bondi–Penrose inequality. The equality-example target keeps its stronger boundary and no-additional-horizon hypotheses.
The shared definitions are supplied by CKSBondiPenrose, CKSBondiPenrose_002. 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.