Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A non-interactive zero-knowledge (NIZK) proof lets a prover convince a verifier that a statement is true by sending a single message, computed from a common reference string that both parties share, without revealing why the statement is true. NIZK proofs were introduced by Blum, Feldman and Micali (STOC 1988). They are a basic component of chosen-ciphertext secure encryption, signature schemes and secure multi-party computation.
Groth, Ostrovsky and Sahai (J. ACM 59(3), 2012; conference versions at EUROCRYPT 2006 and CRYPTO 2006) built NIZK proofs for all of NP from bilinear groups. The construction rests on one abstraction, the homomorphic proof commitment, and one protocol, the NIZK proof for Circuit SAT of their Figure 3. Theorem 6 says that the Figure 3 protocol works for every homomorphic proof commitment. This mission formalizes the part of Theorem 6 that holds exactly, with no computational assumption.
A homomorphic proof commitment scheme (Section 3) has a message space , a finite cyclic group with generator . It also has a randomizer space and a commitment space , both finite abelian groups. It comes with algorithms :
The exact properties used here are the following. The homomorphic property is on keys of either mode. Perfect binding says that on binding keys no commitment has openings to two different messages. Perfect completeness of the 0/1 proof says that honest proofs for are always accepted, on keys of either mode. Perfect soundness of the 0/1 proof says that on binding keys an accepted proof implies for some . Perfect extractability says that on binding keys for .
A NAND circuit on wires is a list of gates , with inputs and output , and an output wire . An assignment satisfies it, , when for every gate and .
The protocol of Figure 3 takes with . The prover commits to every wire, , with . It proves with that each contains or . For each gate it proves that contains or , using message and randomizer . The verifier checks and every 0/1 proof.
If and the scheme has the homomorphic property, perfect binding, and perfectly complete and perfectly sound 0/1 proofs, then
The theorem holds for every scheme with these properties, with no assumption on how the scheme is built.
Theorem 6 is the step from a commitment primitive to NIZK proofs for an NP-complete language. With the subgroup-decision commitment of Section 4 or the decisional-linear commitment of Section 5 it gives Corollaries 9 and 10: perfectly sound NIZK proofs for Circuit SAT with proofs of size . When the common reference string is instead a hiding key, the same protocol becomes the perfect NIZK argument of Theorem 11. Its completeness clause is the hiding-key half of the completeness formalized here.
The result is proved in the paper. Lemma 5 and the soundness of the circuit protocol are left to the reader there or proved in three sentences. No machine-checked proof of this theorem, or of any commitment-based NIZK, was found in Mathlib or in the public Lean libraries searched. This mission states its exact content against an abstract scheme interface. The same interface can then be instantiated by machine-checked versions of the concrete commitments, which are the third and fourth missions of this series.
The argument is short, so the difficulty lies in the bookkeeping. On a binding key the verifier only learns that each commitment opens to some bit. Perfect binding is what identifies the message a gate proof certifies with , which in turn identifies it with the wire bits. Lemma 5 must then be checked in rather than in the integers, where , and must be shown to differ from and . This is exactly where enters: for the all-zero assignment passes every gate check, since . The output wire is handled by the literal check together with binding. Completeness needs the prover's convention to be used consistently in the gate proofs.
ZMod N. A finite cyclic group with a chosen generator is this group, and every theorem that needs it assumes 4 ≤ N, the paper's restriction on p. 14.AddCommGroup and a finite CommGroup. Key generators are PMFs. takes its randomness as an argument.Prop, quantified over the support of the relevant generator. The paper's "for all adversaries, " (or ) is equivalent for unbounded adversaries.Fin n with an output wire. No acyclicity is required, so the statements cover every system of NAND constraints.Dropped, because they are computational:
Perfect zero-knowledge on hiding keys (Lemma 8) is the second mission of this series. The definitions of this mission (the scheme interface, NAND circuits, the protocol) are reusable by any formalization of commitment-based proof systems. Proofs of the milestones are welcome in any order.
Augmented Lagrangian methods (the method of multipliers of Hestenes, Powell and Rockafellar) solve a constrained nonlinear program by a sequence of easier subproblems in which some constraints are moved into the objective through a penalty term plus a multiplier estimate. Andreani, Birgin, Martínez and Schuverdt (SIAM J. Optim. 18 (2007); preprint HAL hal-01295437) split the constraints into upper-level constraints, which are penalized, and lower-level constraints, which are kept in every subproblem and may be arbitrary (not only bounds). This is the design of the solver ALGENCAN and of its successors.
A practical method usually cannot guarantee that its iterates approach a feasible point: the problem may be infeasible, and even when it is not, a local method may stall. The question this mission formalizes is what a limit point of the method is when the penalty parameter is or is not driven to infinity. The answer, Theorem 4.1 of the paper, states that infeasible limit points are not arbitrary: they are stationary for the problem of minimizing the upper-level infeasibility over the lower-level set, unless a weak constraint qualification fails there.
The problem is (2.1):
with , , , , , all continuously differentiable. Write and .
The PHR augmented Lagrangian (2.2) with respect to is, for , , ,
Algorithm 3.1 has parameters , , , boxes and , and tolerances with . At outer iteration it finds and lower-level multipliers , satisfying the approximate KKT conditions (3.1)–(3.4) of minimizing over to tolerance ; it chooses new safeguarded multipliers , in the boxes; and it keeps when
and sets otherwise. A run is a sequence produced this way in which the subproblem of Step 2 is always solvable.
A point is a KKT point of a problem with objective , equalities and inequalities if it is feasible and for some and some vanishing on inactive inequalities. The constant positive linear dependence condition (CPLD, Qi and Wei) holds at if every nontrivial null combination of gradients of equalities and active inequalities, with nonnegative coefficients on the inequalities, has gradients that remain linearly dependent at every point near . CPLD is weaker than both LICQ and the Mangasarian–Fromovitz condition.
Let be a run and a limit point of it. If is bounded, then . Otherwise at least one of the following holds:
Theorem 4.1 is the feasibility half of the global convergence theory of the method; Theorem 4.2 of the same paper (a companion mission) shows that feasible limit points satisfying CPLD are KKT points of (2.1). Together they say that the method either finds a stationary point of the original problem or a stationary point of the infeasibility, under a constraint qualification weaker than MFCQ and only at the limit point. Because the lower-level set is arbitrary, the theorem covers the many variants in which bounds, linear constraints or structured sets are kept out of the penalty.
The result is proved in the paper; no machine-checked proof of it is known. Formalizing it requires the gradient of the PHR function, a conic Carathéodory theorem with linear independence (Mathlib contains only the convex-hull version), and the subsequence and normalization arguments of the proof. Each is reusable: milestone 5 is used again, unchanged, in the proof of Theorem 4.2.
The bounded case is elementary. The unbounded case is where the work lies. Dividing the approximate stationarity condition by removes the objective and the multiplier estimates, but the lower-level multipliers divided by need not stay bounded, so no limit can be taken directly. The supports of the lower-level combinations must first be reduced to linearly independent ones, uniformly along a subsequence, before the bounded/unbounded dichotomy on the reduced multipliers yields either a KKT point of (4.1) or a nontrivial null combination at whose gradients are independent at points arbitrarily close to . Taking limits of the original multipliers without this reduction does not work.
is EuclideanSpace ℝ (Fin n); constraint maps are families of real functions indexed by Fin m. Continuous differentiability "on a sufficiently large and open domain" is read as on all of . The norm in (3.1) is the Euclidean one; (3.4), Step 4 and the vectors , use the sup norm. The paper's norm is arbitrary and the results do not depend on the choice. A run is a predicate on sequences indexed by : x 0 is the initial point , the outer iterations are , the three subproblem tolerances are kept separate, and is the true gradient of the defined function (2.2). "Limit point" is a cluster point of the sequence; "bounded" is boundedness above of . KKT and CPLD are defined once for arbitrary finite index types; CPLD carries no feasibility clause, and linear independence is that of a family indexed by a disjoint union, so a repeated gradient counts as dependent.
No hypothesis is added to Theorem 4.1 beyond the reading. Junk values cannot trivialize the statement: the run evaluates (2.2) and only at ; the gradients are taken of functions; the run is satisfiable; and both alternatives (i) and (ii) can fail at the same point, so the second half of the theorem has content.
Contributions are welcome on every milestone. The gradient computation (4.2) and the conic Carathéodory theorem are self-contained and useful beyond this paper.
The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.
Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to dimensions, and the projected vectors are obtained from calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.
Let be a connected, simple, weighted undirected graph with vertices, edge set and edge weights . Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix has if is the head of , if is its tail, and otherwise. With the diagonal matrix of weights, the Laplacian is , a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when is connected. Its Moore–Penrose pseudoinverse is , where are orthonormal eigenvectors of with nonzero eigenvalues .
For a vertex let be its indicator vector. The effective resistance between and is
and for an edge with endpoints . The -norm of is . Let and be the smallest and largest edge weights.
A resistance sketch is a matrix (columns indexed by ) with
where is the Euclidean norm. In the paper, for a random matrix with , and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write and for the -th rows of and of an approximation , as vectors in .
Let . If is a resistance sketch, if every row satisfies
and if
then for every pair
The lemma is stated for arbitrary , and : nothing about the random projection or the solver enters beyond (4) and the sketch property.
Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in time, that returns any effective resistance to within a factor in time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.
The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative -norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.
The hypothesis (4) controls the error row by row, in the -norm on , while the conclusion concerns the columns of applied to , in the Euclidean norm on , and it is a relative bound for every pair at once. A relative bound cannot hold unless is bounded below uniformly over all pairs of distinct vertices, which is where the factors , and of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make arbitrarily small, and the relation between the -norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between and .
Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from ; no theorem relating the two is available.
The graph is a structure WGraph V E over finite types (vertices, Fintype.card V) and (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes ); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by and . is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of on the Euclidean space , converted back to a matrix; for symmetric this is the spectral pseudoinverse of §2.2. is the sum of squares of the coordinates, not Lean's sup norm. is the real number .
Choices committed to, relative to the page:
A trivializing formalization is ruled out: the goal does not assume the intermediate inequality of the proof, nor a stronger condition on than (5); its hypotheses are satisfiable (for example with and ), and its conclusion is not vacuous for .
Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity and as the projection onto for a connected Laplacian; the trace identity; Loewner-order monotonicity of in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.
Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. 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. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.
Timeline:
A discounted ambiguous Markov decision process has a countable state set , for each state a nonempty set of admissible actions, for each admissible pair a nonempty set of probability measures on (the ambiguity set), a bounded reward and a discount factor . Decisions are made at epochs .
A policy maps each history to a probability measure on . is the set of all such policies. A deterministic Markov policy plays for maps with . A stationary policy uses one such rule at every epoch.
Under Rectangularity, the adversary picks a law separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is . In the static model the adversary fixes one per pair. The robust value of a policy and the robust value function are
Let be the bounded functions on with . For a set of deterministic Markov rules, the robust Bellman operator is
is the only bounded solution of this equation, and for every some stationary deterministic policy has .
Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.
The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.
The contraction property is a state-by-state -argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.
States and actions are countable Lean types; and are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and as a tsum. The rewards satisfy on admissible actions. This is the reading of the page's "", which its bounds require. The discount factor satisfies . Epochs start at , so the first reward is undiscounted.
A policy maps to a PMF supported on . The dynamic adversary maps to a law in . The path law is built by PMF.bind, and the discounted reward is , which converges absolutely. Values are real infima and suprema over nonempty families bounded by , so no junk value arises. is the predicate "bounded", and is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.
is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in is the dynamic one; the static adversary appears only in Lemma 3.
The mission deviates from the page in three places:
Only the first claim of Lemma 1 is posed. Its second claim, that an -greedy rule is -optimal, is false as printed.
A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform -optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.
Risk-averse stochastic optimization replaces the expected cost of an uncertain outcome by a risk function : conditional value-at-risk, mean–semideviation and mean–upper-semideviation models, and the coherent and convex risk measures of Artzner, Delbaen, Eber and Heath and of Föllmer and Schied. Ruszczyński and Shapiro, Optimization of convex risk functions (Math. Oper. Res. 31, 2006), develop the convex analysis of such functions on general spaces of random variables, so that they can be used inside optimization problems .
Optimality conditions, duality and sensitivity analysis for such problems need two regularity properties of : continuity, and the existence of subgradients that are continuous linear functionals. For extended-valued convex functions on infinite-dimensional spaces neither comes for free. The standard sufficient condition, boundedness from above on a neighbourhood of a point (Ioffe and Tikhomirov), often cannot be used: the paper notes (p. 436) that the cone of nonnegative functions in , , a continuous probability measure, has empty interior. Section 3.1 shows instead that for monotone convex risk functions on a Banach lattice both properties follow from convexity and monotonicity alone. This mission formalizes that result, Proposition 3.1, and its instance, Corollary 3.1.
Let be a real vector space with a partial order , and . Outcomes are costs: smaller is better. A function has domain and is proper if for all and . The paper's axioms used here are
A linear functional , not necessarily continuous, is an algebraic subgradient of at if
When is a Banach space it carries its norm topology and is paired with its dual . The subdifferential is the set of continuous satisfying (3.1), and is subdifferentiable at if .
A Banach lattice is a real Banach space whose order makes it a lattice, compatible with addition, such that implies . Every , , with the almost-everywhere order, is one.
In Lean everything lives in the namespace ConvexRiskFn.Cont: dom, IsProper, A1, A2, IsAlgSubgradient and subdiff are defined in the setting file.
Let be a Banach lattice and proper, satisfying (A1) and (A2). Then
Proposition 3.1 removes lower semicontinuity from the list of assumptions a modeller has to check. In the paper's framework, the dual representation (Theorem 2.2) requires lower semicontinuity. The subdifferential formulas, the Hadamard directional differentiability of composite functions and the optimality conditions of §§3.2 and 6 require continuity or subdifferentiability at the point of interest. On spaces, Corollary 3.1 gives all of these on the interior of the domain from (A1) and (A2) alone, for example for real-valued convex monotone risk functions such as the mean–upper-semideviation and conditional value-at-risk models of §4.
The result is proved in the paper, so the formalization adds no new mathematics. It does add two classical functional-analytic facts that the paper cites without proof: automatic continuity of positive functionals on Banach lattices, and continuity of lower semicontinuous convex functions on open subsets of Banach spaces, here for extended-real-valued functions. As far as a search of Mathlib and of the platform shows, neither is formalized in this generality. Mathlib's continuity result for convex functions is finite-dimensional. Mathlib has the Hahn–Banach extension theorem but no theory of positive functionals on Banach lattices.
An algebraic subgradient exists at an interior point by Hahn–Banach applied to the directional derivative, and in a general Banach space it may be discontinuous. Continuity cannot come from local boundedness either: the usual criterion (bounded above near a point) is exactly what fails for natural examples, since positive cones in , , have empty interior. The order structure has to do the work. Monotonicity forces the subgradient to be positive, and positivity forces continuity on a Banach lattice. That last step needs completeness and solidity of the norm. Without them, positive linear functionals need not be continuous, for example on the space of finitely supported sequences.
The second difficulty is passing from lower semicontinuity at each interior point to continuity on the interior. For a convex function this needs a Baire category argument on the Banach space, and completeness cannot be dropped.
E with NormedAddCommGroup, NormedSpace ℝ, CompleteSpace, Lattice, HasSolidNorm (the solidity condition) and IsOrderedAddMonoid. This is the paper's definition, and it contains the paper's function spaces, so the formal goal is a generalization. Compatibility of the order with multiplication by nonnegative scalars is not assumed; it follows from these axioms.EReal. Convexity (A1) is written with EReal arithmetic, which agrees with the paper's for proper functions. Continuity on the interior is continuity of an EReal-valued function in the order topology. On the interior the function is finite, so this is ordinary continuity.E →L[ℝ] ℝ, i.e. . A version stating only an algebraic (possibly discontinuous) subgradient would be the easy half of the result and is not the goal; it is milestone 2.Lp ℝ p μbar (a.e. classes) with a finite measure (the paper's measures are finite, p. 434) and . Its subgradient is a function with MemLp g q μbar for the Hölder conjugate , paired by the integral.exists_extension_of_le_sublinear in Mathlib), positive functionals on Banach lattices, and the Baire-category continuity theorem for convex lower semicontinuous functions. The last two are reusable well beyond risk functions. Contributions proving any milestone, or proving the Phelps or Levin step in greater generality, are welcome.A risk function assigns to an uncertain cost (a function of the random state ) a single number that a decision maker can minimize. Artzner, Delbaen, Eber and Heath (Math. Finance 9, 1999) singled out four axioms, convexity, monotonicity, translation equivariance and positive homogeneity, and called real-valued functions satisfying all four coherent. Föllmer and Schied (Finance Stoch. 6, 2002) and Frittelli and Rosazza Gianin dropped homogeneity to obtain convex risk measures. In each of these works, a central result is a dual representation: the risk function is a supremum of expectations under a family of probability measures, possibly with a penalty.
Ruszczyński and Shapiro (Math. Oper. Res. 31, 2006) place these representations inside general conjugate duality. Their Theorem 2.2 shows that, for any proper, lower semicontinuous, convex risk function on a locally convex space of measurable functions paired with a space of signed measures, the representation holds over the domain of the conjugate, and each remaining axiom corresponds exactly to a property of the measures in that domain. The paper then builds its optimization theory (subdifferentials of composite risk functions, optimality conditions, duality for nonanticipativity constraints) on this representation.
Timeline. Artzner et al. (1999): the coherent axioms, with a representation for finite . Delbaen (2002): coherent measures on under the Fatou property. Föllmer–Schied (2002): convex risk measures on bounded functions. Cheridito, Delbaen and Kupper (2004): spaces of processes. Rockafellar, Uryasev and Zabarankin (2002–2006): the risk envelope in . Ruszczyński–Shapiro (2006): the general paired-space statement formalized here.
Outcomes are costs: smaller values of are better. Let be a measurable space and the space of finite signed measures on it. The mission fixes
Write for the nonnegative functions, for for all , for the nonnegative measures in , and for the probability measures in . Condition (C) requires that every have for some .
A risk function is proper if it never equals and is finite somewhere. The axioms are
The conjugate is , the biconjugate , the dual domain , and the lower semicontinuous hull. In Lean these are pair, PairedSpaces, CondC, IsProper, A1–A4, conj, biconj, dualDom and lscHull in ConvexRiskFn.Dual.
Under condition (C), for proper, lower semicontinuous and convex,
and (i) (A2) holds iff every is nonnegative; (ii) when contains the constant function , (A3) holds iff for all ; (iii) (A4) holds iff for all (2.7).
Under (A1)–(A3), (2.6) holds with ; adding (A4), is the indicator of .
Theorem 2.2 is the unifying statement behind the dual representations of coherent and convex risk measures: one theorem covers bounded measurable functions paired with all finite signed measures, paired with , and weak topologies. Downstream, the paper uses it to describe subdifferentials of risk functions as subsets of , to derive optimality conditions for , and to obtain the risk envelope (2.8) used in distributionally robust optimization.
The result is proved in the paper, assuming Fenchel–Moreau in locally convex spaces as a cited theorem. As far as is known, neither Theorem 2.2 nor Fenchel–Moreau for extended-real functions on a general locally convex space has a machine-checked proof. At the pinned revision Mathlib has geometric Hahn–Banach separation in locally convex spaces but no Fenchel conjugate at all. A formal proof of the goal would yield, in particular, a reusable Fenchel–Moreau theorem for extended-real convex functions under a measure pairing.
The characterizations (i)–(iii) are short once (2.6) is available; the weight sits in (2.6), that is, in Fenchel–Moreau. Its proof separates a point below the epigraph from the closed convex epigraph in , which needs Hahn–Banach in a locally convex space, the identification of the separating functional with a measure in through the compatibility assumption, and a careful case analysis when the separating hyperplane is vertical, a case that occurs because may take the value . The extended-real arithmetic (, ) has to be tracked through every supremum. A finite-dimensional argument does not transfer: is an arbitrary locally convex space, and lower semicontinuity is with respect to its own topology.
is an abstract real vector space with a topology and the instances IsTopologicalAddGroup, ContinuousSMul ℝ, LocallyConvexSpace ℝ (no Hausdorff assumption), mapped injectively and linearly into . is a Submodule ℝ (SignedMeasure Ω). The pairing is the difference of the Bochner integrals against the Jordan parts; integrability against is a field of the structure, so the pairing is never the junk value of a non-integrable integral. The topology of is not modelled, since no statement uses it. Risk functions take values in EReal, and every supremum is an iSup in EReal. The order is pointwise, not almost everywhere. The constant in (A3) is for an element equal to the constant function . Condition (C) is a separate hypothesis, assumed where it is used.
Two statements depart from the page, and both departures are disclosed in their items. Theorem 2.1 carries the extra hypothesis , without which the printed statement is false in infinite dimension; Theorem 2.1 is a cited result, and the goal does not depend on this choice. The indicator-function milestone names the set explicitly instead of "a closed convex subset of ".
The goal mentions neither nor : it is stated about , and alone, and a proof must establish (2.6) from the hypotheses, not assume it. The hypotheses are satisfiable: a one-point with , and meets all of them, including (C) and (A1)–(A4).
Contributions are welcome at every level: Fenchel–Moreau for EReal-valued convex functions on locally convex spaces (reusable well beyond this mission), lemmas about the pairing (linearity, , positivity), and the milestones in the order listed.
The dial-a-ride problem (DARP) asks for minimum-cost vehicle routes that carry users from individual pick-up points to individual drop-off points, subject to vehicle capacities, time windows, route durations and a bound on each user's ride time. It models door-to-door transport for elderly and disabled people, shared taxis and on-demand microtransit. Cordeau (Oper. Res. 54(3), 2006) gave a mixed-integer formulation of the DARP and the first branch-and-cut algorithm for it, and reported that instances with up to 30 users can be solved to optimality in reasonable time. The algorithm's strength comes from families of valid inequalities: linear constraints satisfied by every feasible route plan that cut off fractional points of the linear relaxation. Several of these families were adapted from the precedence-constrained asymmetric TSP (Balas, Fischetti and Pulleyblank 1995; Grötschel and Padberg 1985) and from the pick-up and delivery problem (Ruland and Rodin 1997); others, notably the generalized order-matching inequalities, were new in this paper.
Let be the number of users. Nodes are with pick-up nodes , drop-off nodes , origin depot and destination depot ; user travels from node to node . An instance fixes, for each node , a load , a service duration and a time window ; for each pair of nodes a travel time ; for each vehicle in a finite set a capacity and a maximal route duration ; and a maximal ride time . The standing conditions are , for , and .
A feasible solution gives each vehicle a route through distinct nodes of , start-of-service times and loads such that every node of is visited by exactly one vehicle, and are on the same route with first, and along each travelled arc, the ride time lies in , the route lasts at most , and the time windows and capacity bounds hold at every visited node. These are the constraints (2)–(14) of the paper's model.
The arc variables are when vehicle travels from to , and . For a node set write , , , , and . An inequality in is valid for the DARP when the aggregated arc variables of every feasible solution satisfy it.
Let be distinct users and let satisfy and . Then every feasible solution satisfies
The handle and the teeth are not required to be disjoint from one another beyond , and is arbitrary.
The mission also states the other propositions of §4: the lifted subtour elimination inequalities (33) and (34) (Propositions 1 and 2), the predecessor inequality (30), the two liftings (36) and (37) of the generalized order constraint (Propositions 3 and 4), the redundancy of the strengthening (40) of (39) under (30) for fractional points (Proposition 6), and the infeasible path inequality (41) under the triangle inequality for travel times (Proposition 7).
Valid inequalities are what make branch-and-cut work: each family is added to the linear relaxation by a separation heuristic, and the paper's computational section reports how the bound improves as families are added. Validity is the one property the algorithm cannot check at run time, since a cut that removes a feasible route plan silently returns a suboptimal answer. Remark 2 of the paper observes that (39) is stronger than the TSP comb inequality on the same sets, and Proposition 6 shows that its natural strengthening adds nothing once the predecessor inequalities (30) are present, which tells an implementer which families to separate.
All propositions are proved in the paper, partly in an appendix; none is formalized. A machine-checked development would give a precise route-based model of the DARP that later DARP and pick-up and delivery papers can reuse, and certified validity of the cut families that branch-and-cut codes for these problems separate.
The proofs are short on paper but argue about the shape of routes: "there exists a path connecting all nodes in ", "this path cannot finish at node because of the precedence constraint". Turning a tight subtour count into a single covering path requires knowing that the arcs of a feasible solution inside a subset of form vertex-disjoint paths, which in turn rests on each node of having exactly one predecessor and one successor and on routes containing no cycles. The arithmetic step from tight teeth to the bound on the handle needs the degree identities for every subset of , and counting the arcs leaving needs the distinctness of the users . Reasoning directly with the linear constraints (2)–(14) does not suffice: those constraints alone do not exclude cycles of zero duration.
Nodes are natural numbers, so and appear literally; , , and are Finset.range (2n+2), Icc 1 n, Icc (n+1) (2n) and Icc 1 (2n). All data and arc variables are real-valued, and every right-hand side is computed in . Feasible solutions are route-based: each vehicle has a duplicate-free list of nodes of , and the constraints of the model are imposed along that list. Read literally, the program (1)–(14) admits closed cycles when around a cycle, on which every proposition fails, and imposes (11)–(13) also at nodes a vehicle does not visit; the route encoding follows the paper's verbal definition of the DARP and its proofs, which reason about routes. Precedence ( before ) is a field of the solution, since with zero travel and service times the nonnegativity of ride times does not order the visits. The routing cost plays no role and is omitted. No positivity is assumed for travel or service times.
Added hypotheses, each necessary: sets in the subtour bound and in (30) are nonempty ( gives ); the users of Proposition 5 are distinct; the generalized order constraint (Propositions 3 and 4) has (for it is false); the ordered sets of Propositions 1 and 2 have nodes, the standing assumption of the paragraph that introduces them; Proposition 7 has and a path through distinct nodes. Proposition 6 is the only statement about fractional points: it assumes nonnegativity, no loops, (2), (3) and (30), and drops the remaining constraints of the relaxation, which makes it stronger.
The inequalities are stated for the arc variables of every feasible solution, not for an arbitrary – vector satisfying a few degree constraints; a statement of the latter kind is a different and false theorem. Useful contributions include the path structure of the arcs of a feasible solution inside a subset of , the degree identities, and the milestone proofs, which are reusable for the other propositions.
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 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.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.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.The separable quotient problem asks whether every infinite-dimensional Banach space admits a separable infinite-dimensional quotient. The selected statement isolates a negative result under the continuum hypothesis. The pinned manuscript supplies the research context.
A quotient is encoded as a surjective bounded linear map between Banach spaces over the same scalar field. The target considers both real and complex scalars.
The selected goal is OAI.SeparableQuotient.negative_main. Its central assertion is
The theorem states that, under the continuum hypothesis CH (the defined proposition that the cardinality of ℝ equals ℵ₁), the separable quotient assertion fails over both the real and the complex numbers, at any universe level u. Here SQ over a scalar field 𝕜 (ℝ or ℂ) asserts that every complete normed space X over 𝕜 in Type u that is not finite-dimensional has a separable quotient in the following sense: there exist a complete, separable, infinite-dimensional normed space Y over 𝕜, also in Type u, and a bounded 𝕜-linear map T from X to Y that is surjective. The conclusion is the conjunction of ¬SQ(ℝ) and ¬SQ(ℂ), so for each field there is an infinite-dimensional Banach space with no such bounded surjection onto an infinite-dimensional separable Banach space. The statement is admitted without proof in the source.
CH is an explicit assumption. The published goal does not state relative consistency, a positive model, or the complete independence assertion in the manuscript title. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The obstruction must rule out every bounded surjection onto every separable infinite-dimensional target space, rather than one proposed quotient.
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.The homotopy hypothesis relates algebraic higher groupoids to spaces. Elementary expansions provide a concrete test of whether adjoining a higher cell preserves homotopy information. The pinned manuscript supplies the research context.
C is a globular coherator in the encoded convention, X is a cellular model, and Y is a pushout that attaches an (n+1)-disk along the source-face inclusion of an n-disk.
The selected goal is OAI.Grothendieck.elementary_expansion. Its central assertion is
The theorem states that, for a coherator C (a globular theory, meaning a category of shapes built from globes by iterated gluing, with morphisms preserving the globular pushouts, which has a cellular presentation as a countable-stage colimit of free extensions along admissible pairs of parallel cells and in which every admissible pair is filled by some morphism), the following holds for models of C, i.e. presheaves on C sending globular pushouts to pullbacks. Let X be a cellular model, meaning that it is built from an initial model by a well-ordered transfinite composition in which each successor step attaches cells freely along boundaries of cells of the previous stage. Let n be a natural number, let a be a map from the free model disk(n) on the n-globe to X, and let J_n : disk(n) → disk(n+1) be the map induced by the source-face inclusion of the n-globe into the (n+1)-globe. If Y, together with i : X → Y and b : disk(n+1) → Y, forms a pushout square of a and J_n, then i is a weak equivalence. Here weak equivalence means that i induces a bijection on sets of components (0-cells modulo being joined by a 1-cell) and, for every 0-cell x of X and every n, a bijection on homotopy groups, which are classes of n-loops based at the degenerate cells above x, identified when joined by an (n+1)-cell.
The selected goal is the elementary-expansion theorem. It does not itself assert the complete equivalence between the homotopy theory of spaces and all coherator models. 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 conclusion requires preservation of components and every based homotopy group, for cellular models built through transfinite attachments.
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.Tensorial absorption is a structural regularity property of a C*-algebra. A criterion in the central-sequence algebra would detect it through asymptotically commuting elements. The pinned manuscript supplies the research context.
For a nontrivial separable unital C*-algebra A and a free ultrafilter, the central algebra is the commutant of A's diagonal copy inside its norm ultrapower.
The selected goal is OAI.KirchbergRordam.character_criterion. Its central assertion is
The theorem states that, for a nontrivial separable C*-algebra A (in the base universe Type) and a free ultrafilter ω on the natural numbers, meaning an ultrafilter that refines the cofinite filter, the norm central-sequence algebra of A has no characters if and only if A is isomorphic to its minimal (spatial) C*-tensor product with the Jiang–Su algebra. The norm ultrapower of A is the quotient of the C*-algebra of bounded sequences in A by the ideal of sequences whose norms tend to zero along ω; the central algebra is the closed star-subalgebra of this ultrapower consisting of elements commuting with the diagonal copy of A, the images of constant sequences. The central algebra has no characters means that every star-homomorphism from it to ℂ (a linear, multiplicative, star-preserving map, not required to preserve the unit) is the zero map. The Jiang–Su algebra is the inductive limit C*-algebra of the standard prime-dimension-drop model system. The right-hand side asserts the existence of a star-algebra isomorphism over ℂ from A onto this tensor product. The proof is admitted in the source.
The target is the character criterion for one algebra and one free ultrafilter. The manuscript's infinite tensor-power consequence is not separately attached. 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 two directions relate a scalar-valued representation obstruction to an isomorphism with a tensor product, using the precise inductive-limit Jiang–Su model.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.Quasitraces behave linearly on commutative subalgebras but need not initially be additive on all positive elements. A uniform defect on a fixed pair would separate them from traces. The pinned manuscript supplies the research context.
The algebra is separable and carries a normalized 2-quasitrace, meaning a quasitrace with the specified extension to two by two matrices. The witnesses are positive contractions.
The selected goal is OAI.Kaplansky.kaplansky_quasitrace_counterexample. Its central assertion is
The theorem (admitted in the source, not proved there) states that there exists a separable C*-algebra A, with its complex C*-algebra structure, for which the following hold. First, A carries a normalized 2-quasitrace. Here a 1-quasitrace is a function τ : A → ℂ such that τ(xx) is a nonnegative complex number for all x; τ(xx) = τ(xx*); τ(h + i k) = τ(h) + i τ(k) for self-adjoint h and k; and the restriction of τ to every norm-closed commutative (non-unital) star-subalgebra over ℂ is ℂ-linear. It is normalized if τ(1) = 1, and it is a 2-quasitrace if it extends to a 1-quasitrace σ on the 2×2 matrices over A (as a C*-matrix algebra) satisfying σ of the matrix with a in the upper-left corner and zeros elsewhere equal to τ(a) for all a. Second, there are positive contractions a and b in A, meaning each is of the form x*x and has norm at most 1, such that every normalized 2-quasitrace τ on A satisfies Re(τ(a+b) − τ(a) − τ(b)) ≥ 1/144. So no such τ is additive on this pair.
The selected goal is the quantitative quasitrace counterexample. The stable-finiteness and tensor-product consequences are retained as a separate published bundle. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The same positive contractions must exhibit the defect for every normalized 2-quasitrace, while at least one such quasitrace exists.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
Additional published targets are included as separate references:
adc7f1241b42. Selected goal source.Hilbert-space spectral localization does not automatically produce bounded elements of the underlying operator algebra. Bounded recovery asks when positive averaged detection survives that passage. The pinned manuscript supplies the research context.
A standard modular datum has a cyclic separating vector, spectral calculus and scalar centralizer. Unit vectors lie in shrinking bands around a fixed real spectral parameter.
The selected goal is OAI.BoundedRecovery.bounded_recovery. Its central assertion is
The theorem states that, for a standard modular datum S on a complex Hilbert space H (a von Neumann algebra M with a unit cyclic and separating vector ξ, a nondegenerate real spectral calculus D with unitary group D.unitary t, an antilinear isometric involution J, and a closed Tomita graph of a ↦ (aξ, a*ξ) over a ∈ M equal to the pairs (p, Jq) where p is mapped to q by the half-exponential graph of D) satisfying ScalarCentralizer (every a in M fixed by conjugation with D.unitary t for all real t is a complex multiple of the identity), the following holds. Let ω be an ultrafilter on ℕ that refines the at-infinity filter (ω ≤ atTop), let T be a bounded complex-linear operator on H, let s be real, and let δₙ > 0 tend to 0. Suppose hₙ are unit vectors, each with spectral support in the interval [s − δₙ, s + δₙ] (every bounded continuous function vanishing on that interval annihilates hₙ under the calculus), and suppose the limsup over n of the ω-limit of the symmetric time averages (1/2k)∫{−k}^{k} ‖T(D.unitary t hₙ)‖² dt is strictly positive. Then the recovery conclusion holds: there are a strictly increasing sequence nⱼ, operators vⱼ in M, and constants C and η > 0 such that for every j, ‖vⱼ‖ ≤ C, ‖T(vⱼ ξ)‖ ≥ η, and vⱼξ has spectral support in [s − 4δ{nⱼ}, s + 4δ_{nⱼ}]. The proof is admitted, not supplied.
The hypothesis is positivity of the specified ultrafilter time average and outer limsup. Bicentralizer triviality and further rigidity applications are not separate conclusions 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.
The recovered vectors must come from uniformly bounded algebra elements while retaining detection and shrinking spectral support along a subsequence.
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 hierarchy of infinitely many overlap scales need not fill an interval. Full support asks whether an admissible zero-temperature SK minimizer leaves any gap below overlap one. The pinned manuscript supplies the research context.
An order parameter is a nonnegative, monotone, right-continuous integrable function on [0,1). The Parisi value is defined by a Brownian stochastic-control supremum. The Stieltjes measure μ lives on the subtype Time=[0,1); its support below is taken in that relative topology.
The selected goal is OAI.ZeroTemperatureSK.full_support. Its central assertion is
The theorem states that, for any probability space carrying a real Brownian motion B (a BrownianSystem W) and any order parameter γ on [0,1), if γ minimizes the Parisi functional over all order parameters, then a five-part full-support conclusion holds. An order parameter γ:[0,1)→ℝ is nonnegative, monotone, right-continuous and integrable (extended by zero outside [0,1)). For a time t and position x, the value is the supremum, over controls α progressive for the filtration generated by the Brownian increments after t and bounded by 1 in absolute value, of the expected payoff |x + B₁ − B_t + ∫_t^1 γ(s)α(s−t)ds| − ½∫_t^1 γ(s)α(s−t)²ds. The gradient and curvature are its first and second derivatives in x, and the Parisi functional is value at (0,0) minus ½∫_0^1 tγ(t)dt. Being a minimizer means the functional at γ is at most its value at every order parameter η. The conclusion says: (1) there is a measure μ on [0,1) with μ((−∞,t]) = γ(t) for every t in [0,1); (2) there is a diffusion X, a process progressive for the Brownian filtration that almost surely is continuous on [0,1], starts at 0, and satisfies X_t = B_t + ∫_0^t γ(s)·gradient(s,X_s)ds; (3) every such measure μ has full support, equal to all of [0,1); (4) γ is strictly increasing, γ(a)<γ(b) whenever a<b; and (5) for every such diffusion X and every t in [0,1), the expected square of the gradient at X_t equals t, and the expected square of the curvature at X_t equals 1.
The main target is the five-part full-support conclusion for every encoded minimizer and Brownian system. The separate value-consequences bundle is retained as an additional formal 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 conclusion couples support, strict increase, diffusion existence and derivative identities. Minimization alone is not an assumption of those conclusions.
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.SKValue.value_consequences (Open).adc7f1241b42. Selected goal source.Vertex operator algebras describe conformal theories algebraically, while conformal nets describe local operator algebras. Passing between them requires analytic control of fields. The pinned manuscript supplies the research context.
The selected algebra is simple, unitary, CFT-type and strongly rational. Its modes act on an inner product space, and smeared fields act on the Hilbert completion.
The selected goal is OAI.MinimalVertex.main. Its central assertion is
The theorem states that, for a CFT-type vertex operator algebra A on a complex inner product space V (a vertex algebra with vacuum, state-field map and Jacobi identity, together with a conformal vector, central charge, finite-dimensional graded pieces with degree-zero part spanned by the vacuum, conformal vector in degree 2 acting as the grading operator, and the Virasoro relations), equipped with a unitary structure U (an antilinear involution fixing the vacuum and conformal vector, compatible with all modes, together with a unit-norm vacuum and an invariance relation between a mode and the corresponding mode of the transformed adjoint-side vector), if A is simple (nonzero vacuum and no ideals other than 0 and the whole space) and strongly rational (self-contragredient, rational in the sense that every admissible weak module is completely reducible, and C2-cofinite), then three things hold. First, A has polynomial energy bounds: for every a in V there are C>0 and natural numbers p,k with ||a_(n) b|| ≤ C(1+|n|)^p ||(1+L_0)^k b|| for all integers n and all b in V. Second, the CKLW strong locality property holds: all vectors satisfy these bounds, and for every proper circle arc I the von Neumann algebra generated by closed smeared fields supported in I, built on the completion of V, lies in the commutant of the algebra attached to the complementary arc. Third, the assignment of these interval algebras to proper arcs admits the structure of an irreducible conformal net, meaning a separable Hilbert space with isotony, locality, a continuous Mobius representation extended to a continuous projective representation of smooth circle diffeomorphisms with covariance and locality of the action, a unit invariant vacuum that is unique up to scalar and cyclic, a positive self-adjoint Hamiltonian generating the rotation flow, and trivial commutant of all interval algebras apart from scalars.
The target proves polynomial energy bounds, the specified CKLW strong locality property, and existence of an irreducible conformal-net structure. Complete rationality, category equivalences and extension classification are not conclusions of this reference. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
Formal algebraic identities must yield polynomial operator bounds and locality for closed smeared fields on the completion.
The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.
The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.
adc7f1241b42. Selected goal source.The parity function tests whether a shallow quantum circuit can combine information from all input bits. Polynomially many ancillary qubits make the measured-output formulation substantially stronger than a restriction to clean final registers. The pinned manuscript supplies the research context.
Allowed gates are arbitrary one-qubit unitaries and Toffoli gates with finitely many controls. Gates within a layer have disjoint supports. Inputs occupy the first n qubits, with zero ancillas.
The selected goal is OAI.QAC.parity_lower_bound_polynomial_size. Its central assertion is
The theorem states that, for any positive integers d, k and C, there is a threshold n₀ such that for every n ≥ n₀ and every total qubit count N with n ≤ N ≤ C(n+1)^k, the following holds. Take any circuit given as a list of at most d physical layers on N qubits, where a layer is a list of gates with pairwise disjoint supports and each gate is either a one-qubit unitary on a single qubit or a Toffoli gate with an arbitrary finite set of control qubits and a target outside that set (flipping the target exactly when all controls are 1). The circuit's matrix is the product of the layer matrices, with the first layer acting first. For every choice of output qubit out among the N qubits, there exists an n-bit input x such that successProbability, the total Born probability over all final computational-basis strings y whose out-th bit equals the parity (sum mod 2) of x, is strictly less than 2/3. Here the input state is x placed on the first n qubits with all remaining qubits set to 0, and the remaining qubits are summed over with no requirement that they be clean. So fixed-depth circuits with polynomially many qubits cannot compute parity with worst-case success probability at least 2/3. The theorem is admitted in the source (proof is sorry).
The published goal fixes success threshold 2/3 and positive integer depth, polynomial exponent and coefficient. It does not state the manuscript's full range of positive advantages. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.
The bound covers arbitrary gates, all choices of output qubit and polynomially many total qubits. Discarded registers can retain unrestricted garbage.
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.