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.
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?
In an online decision problem a decision maker chooses actions one period at a time, and only after each choice learns what that choice cost. The classical instance is prediction with expert advice: each day one of experts is followed, and afterwards every expert's loss is revealed. The goal is a strategy whose total cost is close to that of the best single fixed action in hindsight, whatever the sequence of costs.
Many structured problems have exponentially many actions, such as paths in a graph whose edge delays change daily. Weighted-majority methods keep one weight per action and are then inefficient. A. Kalai and S. Vempala (J. Comput. System Sci. 71 (2005) 291–307) showed that it suffices to be able to solve the offline problem: given total costs, find the best single action. Their algorithm, Follow the Perturbed Leader (FPL), adds a random perturbation to the accumulated costs and calls the offline solver once per period. The idea goes back to J. Hannan (1957); the paper's analysis made it short and broadly applicable, and FPL has since become a standard tool in online learning and online combinatorial optimization.
Timeline.
Decisions and states are vectors in . The decision set is a possibly infinite set and the state set is . In period the decision maker picks , then the state is revealed, and the cost is the dot product . The state sequence is fixed in advance (an oblivious adversary).
Write , with . The offline oracle is a map with
Because costs are linear, the best fixed decision after periods has cost
Three parameters measure an instance, with :
FPL(), for a parameter : in each period , draw uniformly at random from the cube and play . Its expected cost is .
Hannan(): the same rule with uniform on .
For every state sequence and every ,
The constants are the paper's. With the expected regret is at most .
For any state sequence in , any and any ,
This bound needs no knowledge of . It is included as a separate theorem, not a milestone of the goal.
The result. Theorem 1.1(a) reduces online linear optimization over any decision set to its offline counterpart, at the price of one oracle call per period and regret . Applied to online shortest paths, spanning trees and other combinatorial problems it gives efficient algorithms where weighted majority would maintain exponentially many weights. Later uses of FPL (approximate oracles, robust optimization via online learning) start from this bound.
Formalizing it. The theorem has been proved in print for twenty years; it has no machine-checked proof that we know of. The platform already holds a formalization of Ben-Tal, Hazan, Koren and Mannor's approximate-oracle variant (OracleRO.ApproxFPL), which takes a maximising oracle and an oscillation bound and therefore yields a weaker constant () in this setting. This mission states the exact-oracle bound with the paper's constant , where bounds itself. A correct proof must handle that constant carefully; see the next section.
Display (4), Lemma 3.1 and display (5) are finite-sum arguments from the defining property of . Lemma 3.2 is a statement about Lebesgue measure of a cube and its translate.
The central difficulty is the stability step: bounding, period by period, how much worse it is to play than . The obvious argument says that the two perturbed points have laws that agree on a fraction, and on the rest "one can only be larger". Under the printed definition of the difference of two costs can be as large as , so this per-period bound fails for costs of mixed sign: with , and suitable , the per-period difference is , while . The theorem itself, with , remains true, but a proof cannot proceed by the per-period comparison as written. Proving the goal with the stated constant, rather than , is the substantive part of the mission.
Fin n → ℝ; is dotProduct (⬝ᵥ); is written out as ; is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The sets are Dset and S; the diameter is Ddiam.s : ℕ → Fin n → ℝ indexed from (s 0 is unused); the hypothesis is imposed for .IsArgminOracle Dset M: and for all . Every theorem quantifies over all such ; the oracle is never a chosen Classical.epsilon minimiser.OracleRO.ApproxFPL.FPL: prefixSum s t ; perturbLaw n ε, the uniform law on ; and fplExpectedReward M s ε T , which with an argmin oracle is the expected cost of FPL() (its name reflects a maximisation source). Using one integral per period is the paper's own observation that fresh and shared perturbations give the same expectation.Contributions welcome: proofs of the milestones, the goal and Theorem 3.3, and reusable lemmas on uniform laws over translated cubes.
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)).
Principal component analysis estimates the eigenvalues of a population covariance matrix by those of the sample covariance matrix . Before random matrix theory turned to the regime where the dimension grows with the sample size, the classical question was the opposite one: the number of variables is fixed and the number of samples tends to infinity. In that regime almost surely, and the next question is the size and shape of the fluctuations of the sample eigenvalues. When has a repeated eigenvalue, the sample eigenvalues near it do not fluctuate independently: they repel each other, and their joint limit law is that of the eigenvalues of a random Hermitian (or symmetric) matrix. Anderson (1963) derived these limits for real Gaussian samples.
Baik, Ben Arous and Péché (2005) study complex Gaussian samples whose covariance matrix is the identity apart from finitely many "spiked" eigenvalues, and find a phase transition for the largest sample eigenvalue as together. Their Proposition 1.1 is the fixed-dimension counterpart: with fixed and all population eigenvalues equal, fluctuates on the scale with the law of the largest eigenvalue of a Gaussian unitary ensemble (GUE). The paper places it beside its Theorem 1.1(b), where a -fold spike above the critical value gives the same GUE limit when . This mission formalizes Proposition 1.1.
Fix and . A standard complex Gaussian is with independent centred real Gaussians of variance , so . For each , let , , , have independent standard complex Gaussian entries (sampleLaw M k), and let the samples be : mean zero, covariance . The sample covariance matrix is
a Hermitian matrix (sampleCov), and is its largest eigenvalue (largestEig). The general model sampleVec U ℓ G m is specialized to and , because a Hermitian matrix with all eigenvalues equal to is .
Write (vandSq). The finite-GUE distribution (Definition 1.2) is
the distribution function of the largest eigenvalue of a GUE matrix. In Lean these are G k x and Z k.
For every real and every ,
The second statement is in probability.
With , , and :
The proposition identifies the fixed-dimension limit of the top sample eigenvalue under a degenerate population spectrum: the sample eigenvalues near , rescaled by , behave like a GUE spectrum, and like its maximum. For it reduces to the central limit theorem for the sample variance of one complex Gaussian variable, with limit by (29). For general it shows that the GUE limit of the supercritical regime in Theorem 1.1(b) is already present when the dimension does not grow.
The result is proved in the paper (§5, p. 1691) by an exact computation. No machine-checked proof of it, of the complex Wishart eigenvalue density, or of the Gaussian and Laguerre cases of Selberg's integral is known to exist in Mathlib or on the platform. The formalization requires the joint eigenvalue density of a complex Wishart matrix (a Weyl-type integration formula over the unitary group), two Selberg-type integral evaluations, a Stirling asymptotic for products of factorials, and a dominated-convergence argument on . The first three are reusable well beyond this mission.
The limit itself follows from (304) and the constant asymptotics. The hard part is (302): passing from the law of the matrix to the joint law of its eigenvalues. This requires the change of variables with unitary, the Jacobian , and the integration over the unitary group. A direct central limit argument for the entries of gives the Gaussian limit of as a GUE matrix. To get from there to one needs the continuity of the largest eigenvalue in the matrix entries and a matching normalisation, so it is a different route from the paper's. Either route requires spectral facts about Hermitian matrices that Mathlib does not yet package. The Selberg evaluations (27) and (303) are classical but have no short proof: the standard arguments use orthogonal polynomials or an induction with a Dixon–Anderson type integral.
(sampleLaw M k).real of explicit sets.Contributions are welcome on each milestone. Particularly reusable are the complex Wishart eigenvalue density, the Gaussian and Laguerre Selberg integrals, and the measurability and continuity of eigenvalues of Hermitian matrix families.
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.In the local model of differential privacy, no trusted curator ever sees the raw data: each individual randomizes their own record before handing it to the analyst. This is how private telemetry is collected in practice (randomized response and its descendants), and it raises a basic question: which learning tasks remain possible when the learner only sees locally randomized records?
Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith answered it in What Can We Learn Privately? (arXiv:0803.0924v3, the accepted version of SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are the arXiv v3's). They showed that local private learning is equivalent, up to polynomial factors, to learning in Kearns' statistical query (SQ) model (Kearns 1998), where an algorithm sees a distribution only through approximate expectations. This mission formalizes one direction of that equivalence: every SQ algorithm can be run by a local algorithm (§5.1.1, Theorem 5.7). The other direction (Lemma 5.8) is a separate mission of this series.
Timeline. Blum, Dwork, McSherry and Nissim (PODS 2005) observed that SQ algorithms can be simulated by a trusted curator adding noise to sums. Dwork, McSherry, Nissim and Smith (TCC 2006) introduced the Laplace mechanism. Kasiviswanathan et al. (FOCS 2008; journal version 2011) showed the simulation works even in the local model, with each record entering a single randomizer.
A database is a vector ; two databases are neighbors if they differ in exactly one entry. A randomized algorithm is -differentially private if for all neighbors and all measurable sets of outputs. An -local randomizer is an -differentially private map applied to a single record: for all .
The Laplace distribution has density .
An SQ oracle for a distribution on receives a query and a tolerance , and may return any with . An SQ algorithm with queries asks , where may depend on the earlier answers (adaptive), and outputs a function of all answers. A vector is a valid transcript against if every is within of the true mean of the query asked at that point.
For one query , the randomizer with is applied to each record, and the local algorithm outputs the average . The simulation of an SQ algorithm answers its -th query by running on the -th block of fresh entries and finally outputs what the SQ algorithm outputs on these answers.
There is an absolute constant such that, for every SQ algorithm with queries into , and every ; the accuracy claim further takes every tolerance at least , , and :
On that event the simulation outputs exactly what the SQ algorithm outputs against a valid oracle. The constant is left unspecified, as in the paper.
Theorem 5.7 is the inclusion "SQ ⊆ local" in the paper's characterization of local private learning: every concept class learnable with statistical queries is learnable by an -local algorithm, with sample size growing like . Combined with the converse simulation (Lemma 5.8), it identifies local private learnability with SQ learnability (Theorem 5.14). It thereby transfers the known SQ lower bounds, such as the one for parity, to the local model. It also shows that nonadaptive SQ algorithms become noninteractive local protocols.
The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization fixes what "the simulation gives the same output" means against an adversarial oracle and an adaptive algorithm. It also supplies reusable Lean objects for local differential privacy, Laplace noise and SQ algorithms.
The privacy half is the easy-looking part, but it is adaptive: the query asked in block depends on the noisy answers from blocks . A database change in block therefore changes the law of all later answers, not only . The argument must use that every entry enters exactly one randomizer and compose along the adaptive transcript.
The accuracy half has the same adaptivity issue: the union bound over queries needs, for each , the failure probability of block conditioned on everything before it. That is where the fresh blocks and measurability are used. The concentration step for Laplace averages is sub-exponential, not sub-Gaussian. The naive use of the paper's appendix lemma (A.3) fails: it is stated as an equality for every deviation , but its proof only covers deviations of order the Laplace scale.
Databases are Fin n → D (0-based). Randomized algorithms are identified with the laws of their outputs (Measure); differential privacy is required on all measurable sets. An SQ algorithm is a deterministic adaptive strategy (SQAlg): a randomized one is a mixture over its coins, to which the result transfers. "At most queries" is "exactly " after padding with dummy queries. Queries are real valued with , as the paper allows after Definition 5.4. Block consists of the database indices , so the blocks are disjoint by construction, and the simulated answers are a deterministic function of the database and the noise array. The natural logarithm replaces the paper's base 2, which only changes . Constants are existential and quantified before everything else.
Explicit choices, each recorded in the item that makes it:
A trivializing formalization is ruled out: the oracle is not replaced by the exact expectation, accuracy is required for every query actually asked (not only the first), privacy holds for every database (not only i.i.d. samples), and the constant cannot depend on , , , , or the algorithm.
Needed infrastructure: the Laplace distribution as a probability measure and its moment generating function, a Hoeffding bound for bounded i.i.d. variables, the Laplace mechanism, and adaptive composition along a transcript. All of these are reusable beyond this mission. Proofs of the milestones, of standalone Laplace and composition lemmas, and of the goal are welcome.
Markov decision processes assume that the transition law is known exactly. In practice it is estimated from data, and the optimal policy computed for the point estimate can perform badly when the true law differs. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. The worst case is taken against an adversary (nature) who may choose a law from the set at every step.
For this worst case to be computable by backward induction, the set of path measures of a policy has to decompose epoch by epoch. Garud Iyengar named this property Rectangularity and proved that under it the classical finite horizon theory carries over: a robust Bellman equation holds, and deterministic Markov policies are optimal among all history dependent randomized policies, with state and action sets that may be countably infinite and ambiguity sets that need not be convex (Iyengar, CORC Tech Report TR-2002-07, rev. 2004; published in Math. Oper. Res. 30(2), 2005).
Timeline:
A finite horizon ambiguous Markov decision process (AMDP) has decision epochs , , and a terminal epoch . States lie in a countable set and actions in a countable set . In state at epoch the admissible actions form a nonempty set . For each admissible action , the next state is drawn from some probability measure , where is a nonempty set of probability measures on , the ambiguity set. The decision maker receives when is taken in and the next state is , and at the terminal epoch.
A history at epoch is . A policy assigns to each history a probability measure on . It is deterministic () if every is a point mass, and deterministic Markov () if moreover the chosen action depends on the current state alone. denotes all history dependent randomized policies.
Under Rectangularity (Assumption 1), the set of path measures consistent with is a product of one-epoch sets: nature chooses, for every epoch , every history and every admissible action , a measure , and the path measure is . The robust value of from and the robust value function are
The optimistic values , replace the infimum over by a supremum.
For , depends on only through ; for , ; and
The mission also contains, as a draft theorem that is not a milestone, the per-policy identity of the proof of Theorem 1, eq. (12): for each policy, .
Theorem 2 is the basis of robust dynamic programming in finite horizon: computing an optimal robust policy reduces to backward passes, each a family of one-stage problems . It also justifies restricting attention to deterministic Markov policies, which is what every algorithm in the robust MDP literature computes. Theorem 1 isolates the role of Rectangularity: without it the worst case over path measures does not decompose and the recursion characterizes nothing.
The results are proved on paper; no machine-checked proof is known. The platform holds the finite-state, Markov-controller special case (the Nilim–El Ghaoui RobustMDP series, posed, not proved), whose comparison class is too small to express the claim suffices against . A formal proof here supplies the history dependent policy and adversary machinery on countable spaces that the discounted robust theory and the robust MDP literature reuse.
The obvious argument writes the robust value as an inf–sup over path measures and pushes the infimum inside the expectation epoch by epoch. That step is the content of (12): the infimum of an expectation equals the expectation of an infimum only because nature's continuation choice may depend on the realized action and next state, so near-worst continuations for different branches can be glued into one admissible adversary. Infima need not be attained (the ambiguity sets are arbitrary, the state set countable), so the gluing is an -argument over countably many branches. The supremum over policies needs a matching splicing of -optimal continuation policies (13)–(14). Finally, randomized decision rules must be eliminated (15), which uses Rectangularity again, now per action. Restricting either the policies or the adversary to Markov ones from the start is not allowed: it changes the comparison class and makes the goal circular.
S and one countable action type A serve all epochs; the page's epoch-dependent sets embed into their disjoint union. Epochs are 0-based natural numbers, with terminal epoch M.N and 1 ≤ N.(Fin n → S × A) × S. Probability measures are PMF; as a tsum. The expected reward under a policy and an adversary is computed by backward iterated sums, which is the expectation under the product path measure (3).t < N; the supremum over equals that over the page's because uses only . An adversary chooses for every epoch, history and admissible action.Definitions: AMDP, History, History.extend, IsPolicy, Policy, IsDeterministic, IsDetMarkov, Adversary, Selection, expect, expTail, expectedReward, V, Vstar, Vbar, VbarStar, all in RobustDP.FiniteHorizon. Lemmas about gluing adversaries along history prefixes and about suprema of bounded families indexed by subtypes are reusable. Contributions to any milestone are welcome, in any order; (15) is a one-epoch statement independent of the rest.
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.
Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.
A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.
The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is
The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.
The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison 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.
Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.
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.A force whose derivatives decay rapidly can still encode a computation in a particle trajectory. The selected construction makes the observer condition and effectiveness requirements precise. The pinned manuscript supplies the research context.
For each finite deterministic machine and valid input, compilers produce smooth force and velocity fields on nonnegative time and real three-space, with common compact spatial support.
The selected goal is OAI.AlternatingNS.alternating. Its central assertion is
The theorem states that for every positive real viscosity ν computable by rational approximations with error at most 2⁻ⁿ, there exist computable compilers for a force f and velocity U, and one compact set K⊂ℝ³, with the following property for every well-formed finite deterministic Turing machine M and valid finite input w. The compiled programs describe smooth fields f,U on [0,∞)×ℝ³, both spatially supported in K for all nonnegative times, such that every mixed space-time derivative D satisfies sup_{t≥0,x}(1+t+‖x‖)ᴶ‖Df(t,x)‖<∞ and the analogous bound for U, for every nonnegative integer J. Each program supplies rational approximations to all mixed derivatives at rational space-time points with requested error 2⁻ᵏ, effective moduli of continuity on bounded regions, and integer bounds for all these weighted derivative norms. The velocity starts from zero, is divergence-free, and solves the classical forced Navier–Stokes equation ∂ₜU+(U·∇)U=νΔU+f with identically zero pressure; specifically f=∂ₜU+(U·∇)U−νΔU. On every interval [0,T], U is continuous in H² and continuously differentiable in L², and U and its spatial derivative are uniformly bounded in space and time. Moreover, any classical solution (v,p) with the same force and zero initial velocity equals (U,0) pointwise for all nonnegative times, provided on every [0,T] it has v continuous in H², continuously differentiable in L², and uniformly bounded, and p continuous in H¹. Here these Sobolev continuity conditions mean continuous L² representatives of every spatial derivative through the indicated order; time derivatives at zero are taken within [0,∞). Every initial point a has a unique trajectory X(a,t) for t≥0 satisfying X(a,0)=a and ∂ₜX(a,t)=U(t,X(a,t)). Finally, the trajectory starting at (−1,0,0) has strictly positive first coordinate at some nonnegative time if and only if M halts on w, where encountering a missing instruction also counts as halting.
The goal is the alternating-coordinate construction at every positive computable viscosity. It includes Sobolev time regularity, effective bounds, zero initial velocity and the exact observer condition, rather than all three manuscript constructions. 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 encoding must preserve all weighted derivative bounds and uniqueness in the stated comparison class while recording arbitrarily long computations.
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.Incompressible transport can implement prescribed geometric operations on coding sheets. The selected statement concerns one such finite transport construction with effective smooth forcing. The pinned manuscript supplies the research context.
Source and target rectangles have rational data and specified positive diagonal ratios. In the formula, D_i(y)=q_i+diag(r_i)(y−p_i), with source and target centers p_i and q_i. Space is represented periodically with period ten, and the viscosity is a positive computable real.
The selected goal is OAI.Solenoidal.sheet_theorem. Its central assertion is
The theorem states that, for any natural number N, any sheet datum D of size N, and any computable real viscosity ν>0, there exist a forcing field f and a velocity field u (each a time-dependent vector field on ℝ³) and a flow map X such that the following hold. Here D consists of N source rectangles and N target rectangles with rational corners, all inside the square [2,3]², with the sources pairwise separated by a positive distance and likewise the targets, together with positive rational ratios in each of two coordinates such that the diagonal affine map from source i to target i, which sends the source center to the target center and scales offsets by the ratios, maps the source rectangle exactly onto the target rectangle. Both f and u are periodic in space with period 10 in every coordinate and are C^∞ in space and time jointly. The forcing f is effective, meaning that all its mixed space-time partial derivatives can be approximated to any rational accuracy by a single fixed partial recursive procedure from computable names of the evaluation point. Moreover f has zero mean over the fundamental cell [0,10)³ at every time, is divergence free, and is 1-periodic in time. The field u is a classical solution on t≥0 of the forced Navier–Stokes equations ∂ₜu + (u·∇)u = −∇p + ν Δu + f with zero pressure, zero initial data, incompressibility and spatial periodicity, so u is a solution driven by f without pressure. Any classical solution v with pressure p for the same f and ν and with zero initial velocity coincides with u, and has p identically zero, for all t≥0. The flow map X satisfies X(0,a)=a and solves the particle-path equation dX/dt=u(t,X) for t≥0, and for each i and each point y of the i-th source rectangle, the time-1 flow image of the sheet point (y₀,y₁,2) agrees modulo the torus ℝ³/(10ℤ)³ with the sheet point at the diagonal-map image of y. Further, u vanishes in a neighborhood of every integer time, the advection term (u·∇)u vanishes everywhere, and both f and u have all their mixed space-time derivatives uniformly bounded by rational bounds computable from the derivative multi-index by a fixed partial recursive procedure. Finally, if N=0 then f and u are identically zero.
The target is the sheet theorem, including its encoded uniqueness statement and zero-advection conditions. Machine-halting detection is not a conclusion of this published goal. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The construction must simultaneously enforce smoothness, incompressibility, temporal periodicity, effective bounds and exact transport on every point of each sheet rectangle.
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.An optimal coupling can exist even when no deterministic transport maps attain its cost. The target separates attainment from equality of infima for a three-marginal repulsive cost. The pinned manuscript supplies the research context.
All three marginals are the same smooth compactly supported probability density in real three-space, with smooth compactly supported square root. Coincident points have infinite Coulomb cost.
The selected goal is OAI.Problem356.coulomb_counterexample_and_equal_infima. Its central assertion is
The theorem states, without a proof being verified here, that there exists a function ρ on three-dimensional Euclidean space ℝ³ satisfying a full Coulomb conclusion. This means ρ is a nonnegative C^∞ function with compact support, whose square root is also C^∞ with compact support, and with integral 1 over ℝ³; its density measure μ (Lebesgue measure weighted by ρ) is a probability measure. Consider three-marginal couplings of μ, namely probability measures on triples (x,y,z) of points of ℝ³ all of whose three coordinate marginals equal μ, with cost 1/|x−y| + 1/|x−z| + 1/|y−z| valued in [0,∞] (the inverse of distance zero is ∞). The Kantorovich value of μ is the infimum of the expected cost over all such couplings, and the theorem asserts it is finite and attained by some coupling. Further, no pair of measurable maps T₂,T₃ each preserving μ (pushing μ forward to itself) is a Monge optimizer: for every such pair, the expected cost of the triple (x,T₂x,T₃x) under μ is strictly larger than the Kantorovich value. Nevertheless, the Monge value, the infimum of this graph cost over all such pairs of μ-preserving maps, equals the Kantorovich value, and for every ε>0 there are μ-preserving maps T₂,T₃ with finite graph cost at most the Kantorovich value plus ε.
The goal includes a finite attained Kantorovich value, no Monge minimizer, equal infima and arbitrarily accurate finite-cost maps. Other dimensions and Riesz exponents are not part of this selected 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.
Every measure-preserving pair of maps must be strictly suboptimal, while a sequence of such pairs still approaches the coupling minimum.
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.Homogeneous minimizers model possible free-boundary singularities. A nonflat example in seven dimensions supplies one side of the claimed critical-dimension threshold. The pinned manuscript supplies the research context.
The one-phase Bernoulli energy on a ball is the integral of squared weak gradient plus the indicator of positivity. Competitors are nonnegative Sobolev functions with the prescribed H1-zero-boundary difference.
The selected goal is OAI.Bernoulli.nonflat_in_seven. Its central assertion is
The theorem states that there exists a function u: ℝ⁷ → ℝ that is nonnegative almost everywhere, belongs locally to H¹, and is a global minimizer of the one-phase Bernoulli energy E_B(u) = ∫B (|∇u|² + 1{u>0}) dx. Here ∇u is a distributional gradient, and global minimality means that, for every open ball B of positive radius and every nonnegative almost-everywhere Sobolev competitor v ∈ H¹(B) with v − u ∈ H¹₀(B), one has E_B(u) ≤ E_B(v). Membership in H¹₀(B) requires approximation by smooth functions compactly supported in B, with both the functions and their gradients converging in L². The function is nonzero in the sense that it is not equal to zero almost everywhere, and it is homogeneous of degree one: for each real r > 0, u(rx) = r u(x) for almost every x. Nevertheless, it is not flat: there is no unit vector e ∈ ℝ⁷ for which u(x) = max(⟨x,e⟩, 0) almost everywhere. All almost-everywhere statements and integrals use Lebesgue measure.
The selected goal is existence of a nonzero nonflat one-homogeneous global minimizer in dimension seven. Flatness in dimensions at most six and singular-set dimension bounds are not attached conclusions. 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 stationary cone is insufficient: the example must minimize against all admissible ball competitors and fail every half-space profile.
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.Negative curvature suggests strong analytic control, but bounded holomorphic coordinates impose a different global condition. The target constructs a complex threefold separating them. The pinned manuscript supplies the research context.
The construction uses the encoded Hartogs domain and a complete Kähler metric with sectional curvature between two negative constants. Holomorphic coordinate obstructions are stated in the published main proposition.
The selected goal is OAI.PinchedHartogs.main_theorem. Its central assertion is
The theorem states that there exist a subset M of ℂ³ (realized as ℂ² × ℂ) and a matrix-valued function g assigning a 3×3 complex matrix to each point, together with real numbers A and B, such that M is open, nonempty and contractible, and g is a Kähler metric on M, meaning g is C^∞ on M, Hermitian at each point (g_ij = conj(g_ji)), positive definite (the Hermitian form of g at u has positive real part for every nonzero u), and satisfies the closedness condition ∂g_kj/∂z_i = ∂g_ij/∂z_k, with ∂ the Wirtinger derivative (1/2)(∂_x − i∂_y). Moreover the metric is geodesically complete on M: for every point p in M and every vector v there is a C^∞ curve γ: ℝ → M with γ(0)=p, γ'(0)=v that satisfies the geodesic equation γ''k + Σ Γ^k{ac} γ'_a γ'_c = 0 for all t, where the Christoffel symbols are built from the inverse of g and the ∂ derivatives of g. The metric is also negatively pinched: 0 < A ≤ B and, for every point of M and every real-linearly independent pair u, v, the sectional curvature, computed from the explicit curvature tensor formula in the source, lies between −B and −A. In addition, M has no bounded coordinates: there is no map F from ℂ³ to ℂ³, holomorphic on a neighbourhood of every point of M and bounded in every component on M, whose complex Jacobian determinant is nonzero at every point of M. Finally, M is not biholomorphic to a bounded domain, that is, there is no bounded open set N with holomorphic maps F on M and G on N, each analytic near the respective set, mapping M into N and N into M, which are mutually inverse.
The selected main theorem requires a nonempty open contractible domain, a geodesically complete Kähler metric with two-sided negative real-sectional pinching, no bounded holomorphic map to complex three-space with everywhere-nonsingular differential, and no biholomorphism to a bounded domain. The controlled potential and metric-transfer statements are attached as supporting milestones. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Metric completeness and two-sided negative curvature must coexist with a global obstruction to bounded holomorphic coordinates.
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.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.Fixed-point bounds compare Hamiltonian dynamics with critical points of smooth functions. Degenerate fixed points are central to the unrestricted formulation tested here. The pinned manuscript supplies the research context.
The space is the complex projective quadric threefold, represented through its unit quadric and quotient tangent directions. Hamiltonian maps are endpoints of the specified smooth isotopies.
The selected goal is OAI.ArnoldCounterexample.main. Its central assertion is
The theorem states that the complex projective quadric Q = {[z] ∈ ℂP⁴ : ∑ⱼ₌₀⁴ zⱼ² = 0} admits a Hamiltonian bijection φ with exactly three fixed points, whereas every smooth real-valued function on Q has at least four critical points, including functions with degenerate critical points; equivalently, 3 < 4 ≤ the infimum of their critical-set cardinalities, with infinite cardinalities recorded as ∞. Here Hamiltonian means that φ is the endpoint of an isotopy starting at the identity whose forward maps, inverse maps, and Hamiltonian have globally smooth extensions on ℝ × ℂ⁵. For times in [0,1], the maps preserve the unit quadric, are inverse there, and commute with multiplication by unit complex scalars; the Hamiltonian is invariant under these scalars. They satisfy ω(∂ₜFₜ(z),v) = dHₜ(Fₜ(z))[v] for every horizontal v at Fₜ(z), where ω(u,v) = 2 Im ∑ⱼ conjugate(uⱼ)vⱼ and horizontality at z means both ∑ⱼ conjugate(zⱼ)vⱼ = 0 and ∑ⱼ zⱼvⱼ = 0. Smooth functions on Q are those with smooth local extensions after pullback to the unit quadric, and criticality means that every such extension has zero derivative in all horizontal directions. Moreover, φ has a degenerate fixed point: some unit representative z and nonzero horizontal vector v admit a smooth local lift G of φ with G(z) = z and DG(z)v − v = a iz for some real a. Thus the induced derivative on the quotient tangent has a genuine nonzero eigenvector with eigenvalue 1.
The goal includes the lower bound on all smooth critical sets and at least one degenerate fixed point. A rational cup-length computation is not a separate conclusion of this 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.
Counting fixed points is insufficient: the construction must satisfy the Hamiltonian lift conditions and give a genuine nonzero quotient-tangent eigenvector at a degenerate point.
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.Recursive potentials can define tree norms with controlled midpoint behavior. The central question is whether that control forces an asymptotically uniformly convex renorming. The pinned manuscript supplies the research context.
The encoded constructions include root-sum and zero-root completions, finite tree heads, aggregation spaces and variable-exponent coordinate models. Two least nonnegative potential fields determine the norms.
The selected goal is OAI.ComparatorModel.RecursivePotentials.main. Its central assertion is
The theorem states (its proof is admitted with sorry) that the defined proposition MainClaim holds. MainClaim asserts that there exist constructions, over index types in universe 0, of the finite rooted tree head structure, the tree-vector spaces, the zero-root tree-vector spaces, the aggregation-vector spaces, and their l^p-coordinate models, such that eleven statements about completions of finite-support vectors on rooted trees hold simultaneously. These comprise: (1) completion statements saying that the root-sum tree space for the sequence tree and for the joined tree, and the zero-root space for the joined tree, are complete, infinite-dimensional, with continuous coordinates extending the vector coordinates, continuous potential fields P and Q extending the finite-tree ones, norm equal to P+Q at the root (or both P and Q at the root in the zero-root case, where the root coordinate vanishes), and with norm-nonincreasing idempotent coordinate projections onto initial subtrees having finite-dimensional range, closed finite-codimensional tails and approximation of tail elements by vectors vanishing on the head, and that XZero and XJoined are reflexive; (2) a main statement giving the lower bound t^3/128 on the averaged modulus of XSigma and XJoined for 0<t<1, a cubic-type uniform convexity inequality (‖x+z‖+‖x-z‖)/2 ≥ ‖x‖+‖z‖^3/(8(2‖x‖+‖z‖)^2) for x supported on a head and z vanishing there, and that no equivalent norm on XSigma, XZero or XJoined has the AUC property (positive modulus at every positive t); (3) positivity of the averaged modulus of XSigma at every positive radius t; (4) a separation statement for XJoined: for each ε>0 there is η in (0,1), equal to min(1/2, logarithmicGamma(2, ε/16)) when ε≤2, such that if ‖x±z_n‖≤1 for all n and the z_n are pairwise at distance at least ε, then ‖x‖≤1-η; (5) properties of the variable-exponent l^2-sum of height-h tree spaces with exponents 1+1/h, namely completeness, reflexivity, separable dual, a root-sum functional ν (nonnegative, definite, subadditive, absolutely homogeneous) bounded above and below by explicit multiples of the l^p norm, dense finitely supported vectors, and finite-rank projections; (6) a recursive characterization of the l^p-model potentials by least pairs, with ν equal to the root P plus Q; (7) for every equivalent norm A on the variable space, the modulus at lower/upper vanishes; (8) the absence of any equivalent AUC norm there; (9) a sixth-power stability inequality and (10) a cubic stability inequality for admissible heads, with explicit constants; and (11) a weak-tail estimate: if x and a weakly null sequence y_j with ‖y_j‖≥ε, 0<ε≤1, satisfy ‖x±y_j‖≤1, then ‖x‖≤θ(ε)<1.
The published MainClaim is an eleven-part package, not only the displayed midpoint inequality. Its additional completion, separation, stability, weak-tail and no-AUC assertions remain part of the goal. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The bundled target must coordinate completion, continuous coordinate maps, finite-head approximations, reflexivity and uniform estimates across several related spaces.
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.Independent positive multipliers on a branching tree generate concrete subspaces of real L1. Their asymptotic geometry can distinguish midpoint estimates from AUC renormability. The pinned manuscript supplies the research context.
A nonconstant positive multiplier has probability law μ, mean one and finite second moment. Path products are multiplied along nonempty prefixes, and their L1 classes generate a closed real span.
The selected goal is OAI.IndependentProducts.main_general. Its central assertion is
The theorem states that, for any Borel measure μ on ℝ satisfying the multiplier hypotheses, the closed real L¹ span of the path products is infinite-dimensional, and no equivalent norm on it is AUC. The hypotheses say that μ is a probability measure, almost every value is positive, μ is not almost surely equal to any constant, its mean is 1, and the identity function has a finite second moment (is in L²). Vertices are finite lists of positive integers, a sample assigns a real number to each nonroot vertex, and the product measure is the infinite product of independent copies of μ, one per nonroot vertex. The path product of a vertex v multiplies the sample values at the nonempty prefixes of v, and is 1 for the root. productSpan(μ) is the topological closure, in L¹ of the product measure, of the real linear span of the classes equal almost everywhere to some path product. The theorem concludes first that productSpan(μ) is not finite-dimensional over ℝ. Second, for every seminorm N on productSpan(μ) that is an equivalent norm, meaning there are constants 0<a≤b with a‖x‖≤N(x)≤b‖x‖ for all x, N fails the AUC property, which requires that, for every t>0, the one-sided asymptotic modulus of N at t is strictly positive. That modulus is the infimum over N-unit vectors x of the supremum over closed finite-codimension subspaces F of the infimum of N(x+ty)−1 over y in F with N(y)=1. The statement is given as an admitted theorem without proof.
The selected general target asserts infinite dimension and absence of AUC renormings. Specific exponential and Gaussian-square midpoint estimates are separate published targets, retained as additional references. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The obstruction must work for every admissible multiplier distribution and every equivalent norm, rather than only a particular exponential example.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
OAI.IndependentProducts.main_exponential (Open).OAI.IndependentProducts.main_gaussian_12 (Open).OAI.IndependentProducts.main_gaussian_24 (Open).adc7f1241b42. Selected goal source.A positive averaged midpoint modulus need not supply a positive one-sided asymptotic modulus. Tree-potential norms give explicit spaces in which to separate those notions. The pinned manuscript supplies the research context.
Coordinates are finite lists of natural numbers. Tests have bounded prefix potentials, one of the specified quadratic budgets and a budget-dependent support condition; the normed space is completed.
The selected goal is OAI.BoundedTreePotentials.TreeCalculus.main_counterexample. Its central assertion is
The theorem states that, for every choice of a Boolean flag r (whether the root node, the empty list, is included as a coordinate) and every quadratic kind k among sibling, antichain and global, the following hold for the Banach space X = TestCompletion(treeTestFamily r k). Here nodes are finite lists of natural numbers, the potential of a coefficient function f at a node s is the sum of f over all prefixes of s, and a coefficient function f is a tree test if f vanishes at the root when r is false, every potential satisfies |potential f s| ≤ 1, a quadratic budget holds, and a support condition holds. The budget says that the sum of f(s)² over every admissible finite set B of nodes is at most 1, where admissible means: all of B are children of one common parent (sibling), pairwise prefix-incomparable (antichain), or any finite set (global). The support condition is vacuous for sibling, finite support for antichain, and square-summability for global. The tree test family is the set of such functions on the coordinates, and each finitely supported vector x is given the norm sup over tests f of |Σ x_i f_i|; X is the completion of this normed space. First, X is complete, separable, and not finite-dimensional over ℝ. Second, for every 0 < t < 1, the averaged modulus of X, defined as the infimum over unit vectors x of the supremum over closed finite-codimension subspaces F of the infimum over y in F with ‖y‖ ≥ 1 of (‖x+ty‖+‖x−ty‖)/2 − 1, is at least √(1+t²/4) − 1. Third, for every real normed space Y that is linearly homeomorphic to X, Y does not satisfy IsAUCReal, meaning it is false that the one-sided modulus (defined like the averaged one but with ‖y‖ = 1 and the quantity ‖x+ty‖ − 1) is positive for every t > 0.
The formal statement quantifies over both root flags and all three encoded quadratic kinds. Its claims are completeness, separability, infinite dimension, the stated modulus bound and no linearly equivalent AUC space. 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 lower estimate must coexist with an obstruction to every equivalent AUC norm, not just failure for the original tree norm.
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.Uniform discreteness places a lower bound on distances between points. The target tests whether that metric simplicity forces uniformly bounded finite-rank approximation in the associated Lipschitz-free space. The pinned manuscript supplies the research context.
The free space is the closed real span of point evaluations in the dual of Lipschitz functions vanishing at a base point. Approximation and bounded approximation retain their distinct operator-norm quantifiers.
The selected goal is OAI.DiscreteFree.source_endpoints. Its central assertion is
The theorem states that two propositions hold together, both about the Lipschitz-free space FreeSpace(o) of a pointed metric space (M,o), which is the closed linear span, inside the dual of the Banach space Lip0(o) of real Lipschitz functions vanishing at o (normed by the supremum of the slopes |f(x)-f(y)|/d(x,y)), of the point evaluations; delta(o,a) denotes the evaluation at a. The first, BlockStatement, says that for every natural number p ≥ 1 there exist a countable metric space M and a base point o with all distinct points at distance at least 1 and all distances at most 300p²+150p+5, together with a finite set A of M containing o, such that every bounded linear operator T on FreeSpace(o) of finite rank and norm at most p moves some delta(o,a) with a in A by at least 1/2, that is ‖T(delta(o,a))-delta(o,a)‖ ≥ 1/2. The second, MainStatement, says there exist a countable metric space M and a point o such that distinct points are at distance at least 1, M is unbounded, M is not a proper space, FreeSpace(o) has the approximation property (finite-rank bounded operators approximate the identity uniformly on every compact set to within any ε>0), and yet for every Λ ≥ 1 FreeSpace(o) fails the bounded approximation property with constant Λ, meaning the approximating finite-rank operators cannot all be chosen with norm at most Λ. The theorem is stated with sorry, so no proof is asserted here.
The selected conjunction includes quantitative block obstructions and an unbounded, nonproper, uniformly discrete example. The quantitative real-ℓ1 renorming target is retained as an additional reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Compact-set approximation must remain possible while every candidate uniform norm bound fails. The finite block obstruction must survive in one countable space.
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.Markov type is a metric inequality for the displacement of reversible chains. The target connects this probabilistic control to the possibility of uniformly convex renorming. The pinned manuscript supplies the research context.
Chains are finite, stationary and reversible. A map sends their states into a complete real normed space, and the inequality compares n-step and one-step pth displacement moments.
The selected goal is OAI.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm. Its central assertion is
The theorem states that for a real normed space X that is complete (a Banach space), X has nontrivial Markov type if and only if X admits an equivalent uniformly convex norm. Nontrivial Markov type means there exist p>1 and K>0 such that for every finite reversible Markov chain on m states {0,…,m−1}, with stationary probability vector π, nonnegative row-stochastic transition matrix P, and detailed balance π(s)P(s,t)=π(t)P(t,s), every map f from the states to X, and every n≥1, the expected value of ‖f(Z_n)−f(Z_0)‖^p along n-step paths, started from π, is at most K^p·n times the corresponding one-step expectation of ‖f(Z_1)−f(Z_0)‖^p. Having an equivalent uniformly convex norm means there is a seminorm q on X and constants a,b>0 with a‖x‖≤q(x)≤b‖x‖ for all x, such that for every ε in (0,2] there is δ>0 with q((x+y)/2)≤1−δ whenever q(x)≤1, q(y)≤1 and q(x−y)≥ε.
The exact target uses uniformly convex norms with two-sided equivalence constants. It is not phrased as a direct uniformly smooth norm construction. 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 inequality is uniform over all finite chains and state maps, while the conclusion is one norm controlling all vectors of the Banach space.
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.