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?
An action of an affine algebraic group on an affine variety is observable when invariant regular functions see every nonzero -stable ideal of the coordinate ring: if is a nonzero -stable ideal, then . The notion goes back to Grosshans' theory of observable subgroups (F. D. Grosshans, Observable groups and Hilbert's fourteenth problem, Amer. J. Math. 95, 1973): a closed subgroup is observable exactly when the action of on by left translations is observable (p. 2 of the paper), and observable subgroups are the ones for which is quasi-affine.
L. Renner and A. Rittatore (arXiv:0902.0137) characterise observability geometrically. Their Theorem 3.10 states that an action on an irreducible affine variety is observable if and only if (1) every invariant rational function is a quotient of invariant regular functions, and (2) the set of closed orbits of maximal dimension contains a nonempty open set. Section 4 of the paper specialises this to reductive groups, where the answer becomes a single condition on closed orbits, and identifies a canonical closed subvariety, the socle, on which the action is observable. This mission formalizes that section.
Timeline:
Let be an algebraically closed field. An affine algebraic group is given by its coordinate ring , a reduced, finitely generated, smooth -algebra whose -points form a group with regular multiplication and inversion. An affine variety is given by its coordinate ring , a reduced finitely generated -algebra; its points are the -algebra maps . A regular action is a group homomorphism whose evaluation is a regular function of ; points move by .
For reductive acting on an irreducible affine variety :
and is the maximum -stable closed subset such that the restricted action is observable.
The result. For reductive groups observability is decided by one closed orbit of maximal dimension, with no condition on invariant rational functions. This simplification fails for general groups: a Borel subgroup acting on a semisimple group by left translation has every orbit closed of maximal dimension, yet the action is not observable (Example 3.11 of the paper). The second sentence gives every reductive action a canonical observable piece, the socle, computed from the closed orbits alone, and Proposition 4.8 of the paper then identifies its ideal as the largest -stable ideal without nonzero invariants.
Formalizing it. The results are proved in the paper (Proposition 4.4 is Popov's theorem, cited there). None of them is machine-checked. Theorem 3.10 and Lemma 3.1 are open goals of an existing public mission on the same paper, which covers §§2–3 and defers §4; this mission states §4 on the same definitions, so a proof of either referenced statement serves both. A complete development needs the basic geometric invariant theory of reductive groups: finite generation of invariants, separation of closed -stable sets by invariants, the existence of a unique closed orbit in each orbit closure, and semicontinuity of orbit dimension. None of this is in Mathlib.
The direction "observable " follows from Theorem 3.10. The converse is where reductivity enters: given a nonzero -stable ideal, one must produce a nonzero invariant in it, and the natural route is to separate the closed orbits in from the zero set of the ideal by invariant functions. That separation is a theorem about reductive groups (closed disjoint -stable sets are separated by invariants), not available for arbitrary groups, and it must be combined with the openness of . For the maximality of the socle, the paper reduces to irreducible components through Lemma 3.1, which assumes connected; Theorem 4.7 makes no such assumption, so a disconnected needs a reduction to the stabiliser of a component.
All statements are built on the public definitions module QAlgorithms_Papers_Independent_Support21_P10 for this paper: points are -algebra maps, is a coordinate ring H with a group structure on its points (IsAffineAlgebraicGroup), is a coordinate ring A (IsAffineVariety, finite type and reduced), the action is rho : Point k H →* (A ≃ₐ[k] A) with IsRegularAction. Closure is the Zariski closure on -points (classicalClosure), and is the set of -points of with the restriction map (quotientPoint). No finite generation of is assumed.
Conventions committed to:
IsDomain A) in Theorems 4.6 and 4.7, the paper's standing assumption for §4 (p. 2). Without it the first sentence of 4.7 is false. Lemmas 4.3, 4.5 and Proposition 4.4 are stated for arbitrary affine , as printed.IsReductiveGroup k H: every Zariski-closed normal subgroup of with prime vanishing ideal and consisting of unipotent points is trivial. Unipotence is local unipotence of right translation on .classicalClosure {x | IsClosedOrbit rho x}.rhoZ on A ⧸ coordinateVanishingIdeal Z compatible with the quotient map (IsRestrictionOf). For the socle its existence is part of the conclusion; for a competitor , compatibility is a hypothesis. No statement quantifies over an uncoupled action.(omegaLocus rho).Nonempty. This is strictly weaker than Theorem 3.10's condition that contain a nonempty open set.A trivializing reading is excluded: the socle is computed from the closed orbits and is never defined as "the largest closed set with observable restricted action", which would make the maximality claim a tautology.
Welcome contributions: proofs of the milestones, and reusable infrastructure for reductive group actions (finite generation of invariants, separation of closed invariant sets, orbit-closure structure).
Quantum Max Cut asks for the highest energy of a two-qubit interaction Hamiltonian placed on the edges of a weighted graph. It is a quantum analogue of Max Cut: a classical cut assigns one of two labels to each vertex, while a quantum state can use correlations and entanglement across the qubits. Lee studies an approximation algorithm that first solves a semidefinite program and then uses its vectors to choose both a bit string and the angles of a quantum circuit. The result applies to arbitrary nonnegatively weighted simple graphs, without a degree or regularity restriction. The guarantee is an approximation ratio of for the energy of the algorithm's random output in expectation Lee, 2022, pp. 9–13.
The paper places this algorithm alongside earlier approaches that round a level-one or level-two quantum Lasserre program. Its distinguishing object is a circuit with one parameter per graph edge, computed from the SDP vectors rather than optimized over circuit angles after rounding. The parameter rule makes a global approximation guarantee possible even when neighboring edge gates interfere Lee, 2022, pp. 3–5, 9.
Let be a finite simple graph with nonnegative weights . Associate one qubit with each vertex. On qubit , let be the standard Pauli operators, and let be the identity. Each edge contributes
For a unit state , its energy is . The Quantum Max Cut optimum is the largest eigenvalue of , equivalently the largest energy over all unit states Lee, 2022, Definition 2, p. 2.
The paper's canonical Lasserre program at level uses a real positive semidefinite matrix indexed by Pauli strings of weight at most . Its constraints make matrix entries consistent with products of Pauli strings. At level two, its objective has one term for each of , , and on every edge. Lemma 1 places all quantum-state energies below feasible Lasserre objectives. The paper then introduces a vector semidefinite program (S). It uses a unit vector , vectors for vertices and , and vectors for pairs of distinct vertices. Relations (1)–(8) fix their norms and inner products. Writing , its objective is
Lemma 2 shows that (S) relaxes the level-two Lasserre program Lee, 2022, Definitions 3–5 and Lemmas 1–2, pp. 3–6.
Algorithm 1 takes an optimal feasible solution of (S). It picks uniformly, chooses a random direction , and sets bit by the sign of . For each edge it computes the normalized correlation
It starts in the computational basis state and applies the commuting edge gates , with when and when . The result is a random state Lee, 2022, Algorithm 1, p. 9.
The goal is the expectation form of Theorem 1. For every nonnegatively weighted graph, every globally optimal feasible SDP solution , and every unit quantum state ,
The goal also states that the random energy is integrable. Because the inequality holds for every unit , it is exactly the comparison with times the maximum eigenvalue. The printed theorem omits the expectation sign, while its proof explicitly averages the rounded output Lee, 2022, Theorem 1 and proof, pp. 10–11.
The milestones are the source's relaxation lemmas, the feasible-vector identities, the star monogamy bound, the hyperplane cut-probability bound, the circuit's edge-energy bound, equations (19) and (21)–(24), the final scalar minimum, and the per-solution expected-energy bound. Their order moves from the Hamiltonian and SDP model to the output of Algorithm 1. The coefficient and the parameter are the paper's values, not tunable placeholders.
Together, the two relaxation lemmas connect the quantum optimum to the objective optimized by (S). The rounding results then connect a feasible SDP value to a physically represented output state. The theorem certifies a constant approximation ratio for arbitrary weighted graphs in the model of the paper. The star monogamy inequality and edge-energy lemma also isolate claims useful for analyzing related rounding circuits Lee, 2022, Lemmas 1–6, pp. 4–10.
This result is proved in the cited paper. The mission asks for machine-checked proofs of its statements and for the model that makes those statements precise. Its definitions of Pauli strings, the quantum Hamiltonian, canonical Lasserre feasibility, the vector SDP, and the rounded circuit can support later comparisons of SDP-based quantum approximation algorithms. The draft statements compile, but a compiling sorry is not a proof; the theorem and milestones remain open formalization targets.
Bounding the probability that a rounded bit string cuts an edge is only one part of the argument. Its circuit gate acts on the same qubits as gates at neighboring edges. Consequently, a good cut probability alone does not determine the energy on that edge. The monogamy bound limits how much SDP value can be concentrated around a vertex, while the edge-energy statement accounts for the neighboring gate parameters. A formal proof must also connect matrix feasibility, vector feasibility, Gaussian rounding, and complex matrix expectations without losing the edge weights or the factor Lee, 2022, pp. 7–13.
Vertices are Fin n, computational basis labels are bit strings Fin n → Fin 2, and Pauli strings are maps Fin n → Fin 4. The graph is simple; each edge occurs once, with its smaller endpoint first. Only that orientation's weight is read. The vector SDP uses Fin N → ℝ, and its feasibility predicate states relations (1)–(8) with distinct-index conditions. The ordered-pair implementation of includes symmetry, making the paper's undirected edge indexing explicit. Optimality in the goal compares feasible solutions across every finite dimension, so a solution optimal only in a small dimension cannot satisfy the intended premise.
The random direction is a standard Gaussian vector. Its signs have the same distribution as the signs from a direction uniform on the sphere; a zero projection gives bit zero. The circuit uses the cosine-sine form of each Pauli-product exponential and a lexicographic edge order. Its gates commute, so the chosen order represents the paper's product. The expectation averages the three choices of and integrates over the Gaussian vector. The goal includes integrability, and its universal unit-state comparison avoids a supremum with a default value on a bad domain.
Three source boundaries are stated explicitly. The Lasserre objective requires because it indexes two-qubit Pauli strings. Lemma 6 requires on edges; the printed nonnegative-angle condition is too broad, while Algorithm 1 always gives angles in that interval. Definition 4's repeated objective term is read as , as required by the Hamiltonian and its appendix calculation. The Goemans–Williamson quotient uses since the printed closed endpoint gives . A single arbitrary feasible SDP solution cannot replace the globally optimal one in the final comparison with the quantum optimum, and a deterministic bound for every random outcome is not asserted.
Contributions that establish the two relaxation maps, the vector identities, the Gaussian cut bound, the circuit's local energy bound, and the final expected-energy comparison all belong to this mission. Proofs of the paper's polynomial running-time claim and cited hardness results are outside the formal statements here.
Many manufacturing processes deliver only a random fraction of what they start: semiconductor wafers, biologics, agricultural produce and recycled materials all suffer random yield. A firm facing yield risk has two classical levers. It can inflate production to hedge against low yield, and it can postpone pricing until the yield is observed, so that the price clears whatever was actually produced. The operations literature has long studied both levers for a risk-neutral firm, starting from the price-setting newsvendor (Petruzzi and Dada, 1999).
Real firms, and especially small producers exposed to a single bad harvest or batch, care about low-profit outcomes more than about the mean. Kouvelis, Xiao and Yang (Management Science, 2021) model this with the conditional value-at-risk (CVaR) of profit, the criterion introduced by Rockafellar and Uryasev (2000) and used for newsvendor problems by Chen, Xu and Zhang (2009). Their first finding is that a sufficiently risk-averse firm does not produce at all, and that the risk level at which production stops is the same whether or not the firm can postpone its price. This mission formalizes that finding.
A monopoly firm sells one product to a market with deterministic demand , continuous and strictly decreasing in the price , where is the maximal allowable price, . The inverse demand satisfies and for . Assumption 2 of the paper requires the revenue to be concave on .
Producing units of input costs and yields sellable units. The yield factor is a continuous random variable with law , support with , c.d.f. and mean . The cost satisfies , so that production is not hopeless. Write for the lower quantile and
for the mean of the lowest -fraction of yields.
For a random profit and a risk level ,
the average profit over the worst -fraction of outcomes; is risk neutrality and smaller means more risk aversion.
Under ex ante pricing the firm picks and before the yield realizes and maximizes . Under responsive pricing it picks , observes , then picks the revenue-maximizing price, and maximizes
Since gives CVaR , the firm produces under a scheme when some decision has strictly positive CVaR, and otherwise not producing is optimal.
There is a single , either or a solution of , such that for every
This is the paper's , with the boundary case stated correctly (there the optimal CVaR is , so the firm is indifferent and "produces" in the strict sense fails).
The result says that price postponement, although it raises the profit of a firm that does produce, does not enlarge the set of risk-averse firms willing to produce. The threshold is explicit: when , and otherwise solves . Because depends only on the yield law, the threshold separates cost and price power () from yield risk (), which is what the paper's comparative statics in , and the yield distribution (Proposition 4(ii)–(iv)) build on.
The mission states the paper's threshold results and its two CVaR properties in Lean. None of them is machine-checked anywhere. Proofs of the milestones would also provide a reusable CVaR toolkit on a general probability space: the identification of the maximization formula with the lower-tail mean, and concavity of CVaR in a decision parameter.
The paper's argument uses densities and derivatives throughout: , a first-order condition at , L'Hospital's rule for . The model here assumes only an atomless law with full support, so every such step has to be replaced by a measure-theoretic one. CVaR is a supremum of integrals over an unbounded index, so comparisons between the two schemes cannot be read off a closed form. The responsive profit is itself a maximum over prices inside an expectation inside a supremum. Finally, the two schemes have different optimal decisions everywhere except in the limit of vanishing production, so an argument that compares optimal values fails: the content is in comparing whether positive CVaR is attainable at all.
ν : Measure ℝ: a probability measure without atoms (NullSingletonClass), with ν [l,u]ᶜ = 0 and positive mass on every open subinterval of [l,u]. The paper's density is not assumed. Expectations are Bochner integrals against ν.d and inverse demand P are two functions with both inverse identities on their intervals.RiskPostpone.Threshold.cvar) is the real supremum over of the bracket. The model's profits are bounded on the support, so the supremum is genuine there; the general CVaR properties assume integrability. VaR and the yield quantile use the published MultistageStochastic.valueAtRisk.sSup of the image of , which is nonempty and bounded.Contributions welcome: proofs of the milestones, especially the general CVaR facts (Properties 1 and 2) and the measure-theoretic properties of , which are reusable beyond this model.
The generalized Stieltjes transform of order of a non-negative measure on is the function . For this is the classical Stieltjes transform, whose functions (Stieltjes functions) appear in moment problems, in the theory of completely monotone and Bernstein functions, in the spectral theory of positive operators, and in the functional calculus of sectorial operators. The classes of order were studied by Widder, Hirschman and Widder, Sokal, and Schwarz, among others, and appear in work on functional calculi of sectorial operators (Batty, Gomilko and Tomilov, arXiv:1309.0318).
D. Karp and E. Prilepkina, Generalized Stieltjes transforms: basic aspects (arXiv:1111.4271), collect and prove the basic real- and complex-variable properties of these classes. One elementary but structural fact is that the classes are nested: a function of order is also of every larger order . This raises a natural question that the paper answers: given in the class of order , is the smallest order available, or can it be lowered? The paper introduces the exact Stieltjes order and gives a criterion of exactness phrased purely in terms of the representing measure of . This mission formalizes that criterion (Theorem 16) together with the results its proof relies on.
For , write for the set of non-negative Borel measures on with
The generalized Stieltjes class consists of the functions of the form
with a constant and . The paper writes the atom of at separately as a term (its formula (1)); here it is part of . The pair is a representation of in , and is its representing measure. Write .
For a measure on , its left-continuous distribution function is , so . For , the left-sided Riemann–Liouville fractional integral (Definition A1) is the measure on with Lebesgue density
The exact Stieltjes order of is
Finally, for with representing measure and a parameter , set
For and with representing measure ,
The order is exact precisely when no admissible makes monotone.
The result. Theorem 16 reduces the question "is the order of optimal?" to a monotonicity test on a single function built from the representing measure. The paper derives two practical corollaries from it: if has a limit below , then is exact (Corollary 1), and if has compact support, then is exact (Corollary 2). Both are immediate once Theorem 16 is available and are natural follow-up targets. The milestones are of independent use: Theorem 3 is the nesting of the classes with an explicit formula for the new representing measure, and Theorem A1 is the integrability and inversion theory of fractional integrals of measures, which the paper's appendix develops because the authors found no reference treating measures rather than functions.
Formalizing it. The results are proved in the paper; none is formalized. The platform has the generalized Stieltjes class itself (a published definition from the Batty–Gomilko–Tomilov formalization) and the half-line Beta integral, but no fractional integrals of measures, no inversion formula, and nothing on the exact order. A complete development provides a reusable Riemann–Liouville calculus for measures on the half-line and the uniqueness of the representing measure in , which milestone 5 contains.
The forward direction of Theorem 16 looks like a computation: pass from to a smaller order and read off the measure. The obstacle is that one must know that the representing measure in is unique, since is built from the representing measure and the inversion formula (11) must apply to it; milestone 5 states the inversion for an arbitrary representing measure for this reason. The converse direction must produce a measure from a function: a non-decreasing is a distribution function, and one must show the resulting measure satisfies (2) at the lower order, which is claim (26) and needs a careful tail estimate rather than a direct comparison. Throughout, interchanges of integration are carried out for measures with atoms (including an atom at ), where the naive differentiation formula of (11) and (29) for higher breaks down at jumps.
Functions are real-valued on (PositiveReal), and the classes and representations are the published StieltjesClass and StieltjesRepresentation (QAlgorithms_Papers_Independent_Renew46_P11), reused unchanged. Representing measures are measures on ℝ≥0; the paper's atom at is the constant . All orders are positive. All kernel integrals and the functions and take values in (lower Lebesgue integrals), so a divergent integral is , not ; "non-decreasing" is monotonicity in . The exact order is the real infimum of , which is nonempty and bounded below whenever . Densities are with respect to Lebesgue measure on pushed to ℝ≥0.
Corrected readings, each disclosed in the item: (25) is taken over , while the paper prints ; with the theorem fails for , whose representing measure is the unit mass at . Formulas (11) and (29) are stated only for , the case Theorem 16 uses; as printed for they differentiate a function at its jumps. Claim (26) is stated for the distribution function of an arbitrary measure, the generality its proof gives.
A trivializing formalization is ruled out: must be built from the representing measure of the given (not from an arbitrary measure), over (over an atom at makes identically ), and in (a real-valued Bochner would be wherever the integral diverges).
Contributions welcome: proofs of any milestone, a reusable Riemann–Liouville integral of measures on ℝ≥0 with its Tonelli computations, uniqueness of generalized Stieltjes representations, and the corollaries of Theorem 16.
In quantum field theory the vacuum is entangled between any two regions of space, and the amount of entanglement between nearby regions is infinite: the algebras of observables of regions that touch admit no normal separable state at all. For regions at a positive distance the question becomes quantitative. How much entanglement does the vacuum carry between a region and a second region at distance , and how does it depend on and on the field content of the theory? Questions of this type underlie area laws for entanglement entropy, the thermodynamics of black holes, and the information-theoretic approach to quantum field theory.
S. Hollands and K. Sanders, Entanglement measures and their properties in quantum field theory (arXiv:1702.04924, SpringerBriefs in Mathematical Physics, 2018), define entanglement measures directly on the von Neumann algebras of local observables, without assuming a tensor product structure, and prove upper and lower bounds for them in several classes of theories. For conformal field theories in dimensions, , they bound the relative entanglement entropy of the vacuum between a ball of radius and the outside of a concentric ball of radius by the partition function of the conformal Hamiltonian (Theorem 13, p. 79).
Let be a Hilbert space and commuting von Neumann algebras, with join . A normal state on the join is separable if for , , with positive normal functionals and . Araki's relative entropy of two positive normal functionals generalizes . The relative entanglement entropy of a normal state is
equal to when there is no separable state. Two auxiliary measures enter: the logarithmic dominance , and the modular entanglement measure , where , is the modular operator of at the vector of , and is the 1-nuclear norm.
A conformal field theory in dimensions is given, in its vacuum representation, by a net of von Neumann algebras on a Hilbert space indexed by causal diamonds of Minkowski space , a unitary representation of a covering group of the conformal group that acts covariantly on the net, and an invariant vacuum vector with vacuum state . The conformal Hamiltonian is the generator of the rotation of , the sum of the energy and the generator of special conformal transformations in the time direction; generates dilations. For , is the algebra of the double cone over the ball of radius about the origin, and that of the domain of dependence of the complement of the ball of radius .
for every conformal field theory satisfying the axioms, every and every . The right side is when the trace diverges.
Theorem 13 bounds the vacuum entanglement of two regions by a quantity of the theory's spectrum alone. Combined with the paper's identification of with over the spectrum of operator dimensions (Theorem 14, p. 83), it shows that for the entanglement decays like with the smallest non-zero dimension, and for it diverges at most like . The general results on the way, and the nuclearity estimates, apply to any pair of commuting von Neumann algebras and underlie all upper bounds of the paper, including those for free and integrable models.
The results are proved in the paper, at the level of rigour of mathematical physics, with some steps cited (the Hislop–Longo theorem, the Heinz–Löwner inequality for unbounded operators, the edge-of-the-wedge theorem, the Reeh–Schlieder theorem). None of them is machine-checked. A formal proof would also make precise which axioms each step uses, for instance where statistical independence of and , which is not an axiom here, enters.
The obvious route, comparing the vacuum with product states through a tensor product decomposition , is not available: the local algebras are type III factors and there is no such decomposition. Every step must work with modular operators of the local algebras and normal functionals on their join. The analytic core is the operator identity (212): and are unbounded, Lemma 13 holds for real only, and reaching requires analytic continuation in a strip, domain control through the Heinz–Löwner inequality, and the edge-of-the-wedge theorem. Separately, needs that products of normal functionals on and are normal on the join, which in the conformal setting follows from modular nuclearity rather than from an axiom.
The general layer (Definitions 5, 7, 10–13) is stated for von Neumann algebras in Mathlib's VonNeumannAlgebra, with functionals as maps of which only the values on the relevant algebra matter. Normal functionals are given by vector sums . The relative entropy is Araki's, in Kosaki's variational form, which is defined for all pairs of positive normal functionals. , , , take values in EReal and norms in ℝ≥0∞, so empty infima are , as Definitions 5, 12 and 13 require. Separability is defined on the join, as in Theorem 2 c); no split property is assumed in the goal. Lemma 4 and Theorem 4 carry the §3 standing assumption of statistical independence, in the form that products of positive normal functionals are normal on the join. Modular operators are the published StandardModularData of BoundedRecovery; is the limit of spectral cut-offs.
The conformal layer is a structure CFTVacuum d H₀: the net with isotony and locality (the algebra of a region such as contains those of the double cones inside it and commutes with those spacelike to it, without an additivity assumption the paper does not make) and weak additivity; a covering group of presented by a covering homomorphism with discrete kernel and an exponential map; a strongly continuous unitary representation with local covariance a3′); a unique invariant vacuum vector, cyclic for the quasi-local algebra (the GNS representation of a4′)); the generators , and as spectral calculi; and the Hislop–Longo theorem for the unit double cone as a disclosed field. The projective representation of the paper is taken as a true representation of the cover (Bargmann). Generator signs are fixed so that generates forward time translations and shrinks regions, consistent with (217), (219) and p. 84. is the bounded function of the conformal Hamiltonian, whose spectrum is non-negative (footnote 42), and the trace is taken in . The goal assumes (§4.4, p. 78).
No conclusion of the paper is a field of the structure: not modular nuclearity a5′), not the split property, not (212) or (219), so the goal is not a restatement of its hypotheses. Theorem 14 (the field-content form ) is not stated: a faithful encoding of the operator-valued fields, their conformal transformation law (224) and descendants is left for a later mission.
Reusable beyond this mission: the entanglement measures on general von Neumann algebras, the 1-nuclear norm, , and the conformal structure. Contributions are welcome on the Kosaki formula (scaling, monotonicity, ), on Heinz–Löwner for unbounded operators, and on the analytic continuation of modular groups.
A Hilbert space has an orthonormal basis, so every Hilbert space is isometric to some . Hilbert C-modules, the analogue of Hilbert spaces in which the inner product takes values in an operator algebra, have no such basis in general. Over a von Neumann algebra , Paschke showed that the self-dual Hilbert C-modules are exactly the "ultraweak direct sums" of corners cut by projections (Paschke, Trans. AMS 182, 1973).
Junge and Sherman (arXiv:math/0301044v2, 2003, revised 2004) carried this picture to the noncommutative spaces , . They introduced modules, whose inner product takes values in , and proved that every module is a column sum of corners . The result organizes the study of module maps between noncommutative spaces (the paper's §5–§6 on commutants and bimodules build on it), and it is the form of the orthonormal-basis theorem. Earlier, Junge had proved a version for a special class of modules ([J1, Prop. 2.8]).
Let and let be a unital -subalgebra of the matrix algebra ; these are exactly the finite-dimensional von Neumann algebras. For real , is with the tracial (quasi)norm
In the Lean files this is lpNorm p a, the published Schatten norm schattenNorm.
Let be a complex vector space with a right action of (act). An -valued inner product (Definition 2.1) is a map (ip). It is conjugate linear in the first variable and linear in the second, and satisfies
It induces
(gauge p ip ξ). By Proposition 2.2 this is a norm for and a -norm for . A right -module (Definition 2.3) is such an that is complete in .
Given projections of , the column sum (2.4) is
In Lean this is columnSumSet M q with colIp. The paper calls these modules principal.
For every right -module there are an index set , projections of and a map with the following properties: is bijective, complex linear and a module map, and
This is the paper's statement as printed: "isometrically isomorphic, as a module". The index set and the projections are not fixed; they are part of the conclusion.
Theorem 2.5 reduces questions about arbitrary modules to columns of corners of . Two consequences follow. Module maps between modules become matrices of maps between corners, and the paper identifies the commutant of the right action and describes bimodules in this way. For the theorem is the orthonormal-basis theorem with -valued inner products; for it is Paschke's theorem. In between, there is no Hilbert-space structure to fall back on.
The result is proved in the paper for every von Neumann algebra and every . No part of it has been formalized. Mathlib has Hilbert C-modules with the C-norm and the Hermitian functional calculus for matrices, but no noncommutative spaces, no modules and no column sums. This mission produces the finite-dimensional theory: the definitions, the Cauchy–Schwarz inequality (2.1)–(2.2) for -valued inner products, the column-sum construction and the structure theorem.
Even when is finite-dimensional, need not be. An module may be an infinite column of corners, and the theorem must produce the decomposition without any basis to start from. The obvious idea is to copy Gram–Schmidt and Zorn: take a maximal orthogonal family and show that its closed span is everything. For this step fails as stated. Without an inner product on there is no orthogonal projection onto . A best approximation from exists only for (where is a Banach space and is reflexive), and turning " is a best approximant of " into the algebraic identity needs smoothness of the norm together with the factorization (2.1). The case is reached by a different route through tensor products with . A second difficulty is that is the trace norm of : it depends on and is not the C-module norm, so Mathlib's C-module results do not apply.
StarSubalgebra ℂ (Matrix (Fin n) (Fin n) ℂ). is with the Schatten (quasi)norm of the trace, which is isometric to Haagerup's . This restriction is forced: Haagerup spaces of a general von Neumann algebra exist neither in Mathlib nor on the platform. Because as a set, the inner-product axioms do not depend on ; the norm does.act with the right-module axioms for elements of , and the inner product is the structure LpInnerProduct. Completeness is sequential completeness for (GaugeComplete), since is only a quasi-norm for .The Brauer algebra packages pairings of points into an algebra whose multiplication records how pairings join when diagrams are stacked. It was introduced by Brauer as the centralizer algebra of orthogonal and symplectic groups acting on tensor powers of their natural representation (Brauer 1937), and is semisimple for generic (Wenzl 1988). It provides an example where diagram combinatorics and the choice of coefficient ring affect the same algebraic question. King, Martin, and Parker study central idempotents that separate the diagrams with few propagating lines from the remaining part of the algebra. Their construction works over a ring designed to retain useful specializations of the parameter ; a solution obtained only in the field would lose that arithmetic information. King–Martin–Parker, §1–§2
The mission concerns their main result, Theorem 14. It asks for the precise bridge between a diagram equation, coefficients constrained to , and an idempotent that splits an ideal quotient. The source is the 2016 arXiv version; all page and result numbers here refer to that version. King–Martin–Parker, Theorem 14
A Brauer diagram on strands is a perfect matching of two rows of nodes. A strand joining the rows is a propagating line; a strand within one row is a horizontal arc. The set of all such diagrams is a basis for , here over , where is an indeterminate. To multiply diagrams and , place over and identify the adjacent rows. The resulting outer pairing is another diagram . If connected components close entirely in the middle row, then
This loop factor is part of the algebra, even when no loop is visible in a particular example. The span of diagrams with at most propagating lines is a two-sided ideal. Simultaneous relabelling of the upper and lower rows by partitions diagrams into orbits . The orbit sum uses each original, unnormalised diagram once. King–Martin–Parker, §2.2–§2.3
The source works with a coefficient ring inside :
For and even , let be the diagram with cups at in each row and vertical lines elsewhere. The paper uses the normalized element . Its required equation has the same solutions as over . King–Martin–Parker, §2.2, equation (4), and §3, equation (5)
The goal is Theorem 14. For orbit coefficients and , it asserts a unique solution with to
It further asserts that satisfies and , and is central and idempotent. By Lemma 10, these properties identify the splitting of . King–Martin–Parker, Lemma 10 and Theorem 14
The milestones follow the paper's proof, in attack order: the general bimodule splitting criterion (Lemma 10); the basis of the -centralizer given by the orbit sums (Lemma 11); the paper's assertion that for the splitting idempotent exists with coefficients in (p. 8); the fact that fixes every diagram carrying its cups and maps no other diagram onto without a negative power of (Proposition 12); the independence of the linear equations in the , i.e. injectivity of on orbit-sum combinations (equation (6)); and membership of every solution coefficient in (Proposition 13). Lemma 10 is reusable beyond diagram algebras. King–Martin–Parker, §3
The idempotent separates the ideal of diagrams with few propagating lines from the quotient as bimodules. Its centrality means this separation is compatible with multiplication on either side. Specifying the coefficients in also preserves information about specializations of that a field-only existence statement would omit. The paper uses the resulting splitting idempotents in its discussion of primitive central idempotents and Brauer algebra representations. King–Martin–Parker, §4
The theorem is proved in the cited paper. This mission supplies a machine-checkable interface for its definitions and statements; the theorem proofs remain open. A completed development would verify the diagram multiplication, the ideal and orbit descriptions, the ring-theoretic splitting criterion, and the coefficient claim in one Lean environment. These components can support later formalizations involving diagram algebras or central idempotents.
An equation over alone does not give a splitting idempotent with coefficients in . The coefficient restriction is sensitive to the exact loop factor in multiplication and to whether orbit sums use normalized or original diagrams. The equations indexed by diagrams also need to determine the orbit coefficients uniquely, while the two-sided annihilation requirement concerns every element of the ideal, not just the displayed cup diagram. These are distinct claims in the source; checking one of them does not silently establish the others. King–Martin–Parker, §3
Lean represents a diagram as a fixed-point-free involution on Fin n ⊕ Fin n; the left summand is the upper row. A three-row graph defines its composite and loop count. The Brauer space is the finite-dimensional function space Diagram n → RatFunc ℚ, with an explicit bilinear multiplication bmul; the statements do not assume a ring instance whose associativity has not yet been proved. The parameter is RatFunc.X, representing the indeterminate . The ideal is the -span of exactly the basis diagrams with propagating count at most .
The goal fixes and additionally assumes even (the existence milestone, stated on the page for every , does not). That parity condition makes the paper's displayed product well defined. Lean uses zero-based indices, so the paper's cup is represented by . The equation uses unnormalised but has the same solutions as the paper's normalized equation because is nonzero in . Orbit sums are unnormalised, as in the printed Theorem 14. The centralizer is the set of elements commuting with every diagram having propagating lines. The index set of the goal consists only of orbits of diagrams with at most propagating lines; it is equivalent to the paper's Spore-tableau index set, without introducing that classification into this mission.
The statement constructs as from coefficients , rather than postulating an arbitrary splitting idempotent. Neither the ideal nor the equation is replaced with a degenerate special case: with condition (ii) would force , and with it would be vacuous, so the ideal is exactly the span of the diagrams with at most propagating lines, and the loop factor is kept in the product. The main reusable infrastructure comprises finite diagrams, the loop-weighted product, orbit sums, and the generic bimodule splitting lemma. Contributions may establish these structural facts, the milestone statements, and the final theorem.
The Temperley–Lieb algebra is a family of algebras built from generators that satisfy local relations. It appears in diagrammatic representation theory and provides a tractable setting in which to study cellular bases and Gram determinants. A Gram determinant tests whether the bilinear form on a module is degenerate after specializing its parameter. Thus an explicit determinant formula records information about when a cell module may cease to be simple. Enyang's 2007 paper develops a Murphy-style basis, a commuting family of operators and an orthogonal basis, then gives a closed product for these determinants. The mission targets that final product, with the preceding statements retained as milestones. Enyang, 2007
The generic cellular-algebra definitions and spectral-projector construction have already been formalized in the published package associated with Mathas's work. This mission specializes those objects to the actual Temperley–Lieb presentation and computes its explicit polynomial factors. Mathas, 2006
Let , with an indeterminate. For , the algebra has generators and relations
A shape at level is a pair with . A standard up–down tableau of shape is a path of shapes from to : at each level its cup count stays fixed or increases by one. Write for the set of these paths and . The paper orders paths by comparing their cup counts at every level; means strict pointwise dominance. Enyang, §§1–2
For each shape, is the product . Ordered generator products and their tableau products give the Murphy elements . Lemma 2.3 asserts that they form a cellular basis. The cellular multiplication law computes a Gram form on each cell module . The determinant is the determinant of this computed form in the Murphy basis; it is not assigned the desired closed product by definition. Enyang, Lemma 2.3 and §5
The Jucys–Murphy elements form a commuting family in . Their triangular action on a tableau has content . Over the fraction field , the spectral product produces a vector . These vectors form an orthogonal basis, with squared norms whose product equals . The auxiliary polynomials are fixed by , and . Enyang, §§3–5
The milestones follow the paper's own sequence: the Murphy cellular basis (Lemma 2.3) and the neighbour criterion for the elements (Corollary 2.2); the basic properties of and (Lemma 3.1), the sum identities for (Lemma 3.4), the action of on the generator of a cell module (Lemma 3.5), the triangular action of and with diagonals and (Corollaries 3.6, 3.7) and the alternative recursion for (Corollary 4.2); the seminormal basis (Lemma 4.4), the diagonal coefficients of on it (Corollary 4.6) and the norm ratio of neighbouring seminormal vectors (Lemma 4.7); the identification of with (§5) and the branching law (Lemma 5.1). The goal is Lemma 5.2, the closed product. When ,
When , the predecessor shape lies at level , and the target is
The quotient in the first formula is evaluated in ; the second equality is in . Both clauses occur in the printed Lemma 5.2. Enyang, Lemma 5.2, p. 20
The result turns a determinant of a matrix indexed by all tableaux of a shape into a finite product of explicit recursive polynomials. It makes the factors that can vanish under specialization visible and lets later representation-theoretic questions be asked in terms of those factors. The branching law supplies a compatible description across levels of the algebra tower. Enyang, §5
The paper proves the formulas mathematically. The statements in this mission are compiled Lean targets with proof holes; they do not yet constitute machine-checked proofs of Enyang's results. A complete development would supply the cellular-basis theorem, establish the paper's explicit content action, connect the integral and field Gram forms, and prove the norm and determinant formulas. The quotient presentation, tableau encoding and cellular package can be reused for related specializations and diagram-algebra calculations.
The generator relations make local products manageable, but a determinant does not expose its factors directly. The cell module is indexed by whole paths, and the operators act triangularly rather than diagonally in the Murphy basis. Passing to seminormal vectors changes the basis while keeping track of the bilinear form; this requires the local coefficient and norm statements, not just the commutation of the operators. At the boundary , one of the two possible predecessor shapes disappears, so a uniform two-factor branching formula would introduce a nonexistent module. Enyang, §§3–5
The Lean algebra is a quotient of a free algebra by all three defining relation families. It uses one-based generators; an out-of-range generator is set to zero, and every stated result guards its meaningful indices. Shapes are finite cup-count indices and tableaux are finite paths with a pointwise order. The unrolled products defining and follow the page's multiplication order. The integral statements use ; seminormal vectors use and the published cellular-algebra package's coordinate-space cell module and Gram form. Existence of the required Murphy and JM data is asserted, preventing a theorem about an empty class of such data from passing vacuously.
Several printed details need explicit treatment. The page-2 endpoint in is replaced by , giving exactly factors and . The missing is zero by the paper's sum formula. The denominator in the definition of means . Lemma 4.4(3) says “orthonormal,” but later nonunit norms show that the valid conclusion is pairwise orthogonality. The direction of in the printed definition of and Lemma 5.2 is reversed relative to the formula's denominator and the proof; the target product runs over shapes with fewer cups. Identity (3.3) of Lemma 3.4 is false as printed (at , it reads ); the target is the form its proof derives, with last factor . The goal and the cellular milestones take , since the paper's tower starts at ; for the even case of Lemma 5.2 would refer to the non-existent shape . Enyang, pp. 2, 10, 17, 19–20
Useful contributions include proofs of the algebraic Murphy-basis statement, the content formulas, the seminormal basis properties, the integral-to-field determinant identification and the branching law. Each has a separate mission item and source index.
A quantum dynamical semigroup describes the irreversible evolution of an open quantum system: a family , , of normal completely positive maps on the algebra of bounded operators, with and weakly continuous. When the generator is bounded its structure is given by the Lindblad–Gorini–Kossakowski–Sudarshan form (Lindblad 1976). For unbounded generators, the bounded-generator formula alone does not settle trace preservation or describe the generator's domain.
W. Arveson (The domain algebra of a CP-semigroup, 2002) attached to every such semigroup its domain algebra, the set of observables for which , and all lie in the domain of the generator. This is the largest set on which the generator can be handled algebraically, through derivations and the "dissipation function". Arveson computed it for one explicit example built from the shift on with a rank-one rebound to a pure state , found that its strong closure consists of the operators commuting with , and asked whether there exist dynamical semigroups whose domain algebra is as small as .
A. S. Holevo (arXiv:1706.04866v5, §2) generalizes Arveson's example to a rebound into an arbitrary density operator and answers the question positively: when is nondegenerate, the domain algebra is .
Let and let be the semigroup of left shifts. On trace-class operators put , with dual semigroup on bounded operators, and let be the generator of . The shift moves probability out of through the endpoint , so is not trace preserving.
Fix an arbitrary density operator (positive, trace class, ). The rank-one reset
re-injects the lost probability in the state . For with absolutely continuous with square-integrable derivative (), . Let be the minimal perturbed semigroup generated by (constructed by a resolvent series), its dual, and the ultraweak generator of : means as for every trace-class . The generator of is defined in the same way. Arveson's domain algebra is
For every ,
and if is nondegenerate, . The goal is the existing Open platform theorem QAlgorithms.Papers.Independent.Renew46.P06.shiftReset_domainAlgebra, which this mission references rather than restates.
The milestones follow the paper's proof, in order:
shiftDual_nonunitalStarDomain).shiftReset_centeredGenerator).The goal and Lemmas 3 and 4 are Open platform theorems posed from this paper without a mission; this mission supplies the remaining milestones of the paper's proof and the attack path connecting them.
Theorem 2 answers Arveson's question: there are quantum dynamical semigroups on whose domain algebra contains only the scalars. For such a semigroup, no non-scalar lies in the generator domain together with both and , so algebraic tools built on the domain algebra (derivations, the dissipation function) see only scalars. For degenerate the theorem still forces every element of to act as a scalar on the range of , extending Arveson's computation for a pure to every density operator.
The result is proved in the paper; nothing here is open mathematically. None of it has a machine-checked proof. The mission produces, on top of Mathlib, a formal account of weak generators of semigroups on (the Favard-class criterion (11)), a Duhamel formula for a minimal perturbation, and the equality case of the Cauchy–Schwarz inequality for density operators, each of which is reusable outside this paper.
The algebra of the proof of Theorem 2 is short once its inputs are available; the inputs are the work. Criterion (11) is a statement about the ultraweak generator: with the operator-norm derivative in its place it is false, since the bounded difference quotients describe the Favard class, which is in general larger than the norm domain. Its reverse direction must connect uniform operator-norm bounds with a limit against every trace-class operator. Unitality of depends on the minimal resolvent series of the perturbation actually conserving trace, which can fail for general unbounded perturbations (explosion). The integral equation (12) requires knowing that the minimal semigroup satisfies the Dyson-type equation on rank-one operators built from functions, together with the evaluation , which uses boundary values of functions that only continuous representatives possess.
All statements use the published definitions module QAlgorithms_Papers_Independent_Renew46_P06 and its imports: is HalfLine as an Lp space; semigroups are Evolution (normal, CP, subunital, weakly continuous) with times in NNReal, real times entering through t.toNNReal only for ; trace-class operators and density operators are TraceClass and State b, with the trace operatorTrace b taken in a fixed Hilbert basis ; and the graph of are the ultraweak dualGeneratorDomain and InDualGeneratorGraph; the shift, the pair and the reset construction are IsLeftShift, IsShiftPair and IsResetConstruction; is domainAlgebra; is identityObservable. Every semigroup milestone uses exactly the goal's binders, so the milestones compose with the goal. In (12), are encoded by classes with named locally absolutely continuous representatives, and only those representatives are evaluated at a point; is Mathlib's inner product, conjugate-linear in the first slot. The Cauchy–Schwarz milestone is stated on an arbitrary complex Hilbert space.
A formalization that takes a local semigroup in place of the published construction, an operator-norm generator in place of the ultraweak one, or that turns (12) into a definition of , would not state the paper's results and is ruled out.
The setting of the semigroup milestones is satisfiable exactly when a reset construction exists, which is part of the separate Open platform theorem shiftReset_standard_nonclosable; contributions proving that existence are welcome alongside the milestones. Also welcome: general Favard-class results for weak-continuous semigroups, Duhamel formulas for minimal perturbations in the sense of the published IsMinimalPerturbation, and trace inequalities for State.
A strongly continuous unitary representation turns each group element into a unitary operator on a Hilbert space. Averaging those operators against a smooth, compactly supported function gives a bounded operator. When every such average is trace class, its trace defines a distribution character. The trace condition is therefore a bridge from an operator representation to a scalar distribution that can be studied by harmonic analysis. Van Dijk, Neeb, Salmasian and Zellner collect and extend characterizations of this condition for finite-dimensional Lie groups in their 2015 preprint. Their Theorem 1.3 is the target here.
The authors identify one of the equivalences, between the trace class property and a trace class negative power of the Nelson Laplacian, with an earlier statement of Cartier that had appeared without a proof or reference. Their further conclusion that one finite degree of differentiability suffices is presented as a new result; it gives finite order for the distribution character. These are claims about the cited preprint, not claims of prior machine verification. Source: introduction and Theorem 1.3, pp. 2–5.
Let be a finite-dimensional real Lie group, let be a complex Hilbert space, and let be a strongly continuous unitary representation. Fix a left Haar measure . For a compactly supported continuous function , the integrated operator is for each . Write for compactly supported functions with continuous derivatives and for smooth compactly supported functions. Write and for the trace class and Hilbert–Schmidt ideals of bounded operators on .
Choose a basis of the Lie algebra . The Nelson Laplacian is in the enveloping algebra. The derived representation applies on smooth vectors. Its closure is a non-positive self-adjoint operator, and is bounded. The choice of basis determines , while the theorem holds for an arbitrary fixed basis. Source: §1 and proof of Theorem 1.3, pp. 3–4.
The mission goal is the complete five-way equivalence in Theorem 1.3:
The continuity clauses are part of the target; they cannot be inferred merely from the displayed inclusions. The milestone list includes the four nontrivial implications named in the paper's proof, its finite-order claim and the two displayed identities needed to connect the function and operator Laplacians. Source: Theorem 1.3 and proof, pp. 3–5.
Condition (iii) is formulated using every smooth compactly supported function. Condition (i) replaces smoothness by one finite differentiability order that works uniformly for the representation, while retaining continuity into the trace class ideal. This is the form needed to conclude that the distribution character has finite order. Condition (v) tests the same property with one operator associated with the Lie algebra basis. These consequences are stated by the authors in the introduction and derived in §1. Source: pp. 2–5.
A formal proof would connect Lie-group differentiation, Bochner integration, Schatten ideals and the topology of compactly supported function spaces in one reusable development. The target and milestones here are open Lean statements: compilation checks their types, not their proofs. The previously posed Lemmas 1.1 and 1.2 of the same paper remain separate open platform items, and can be used by solvers without being re-posed here.
Showing that each is trace class does not immediately give continuity of in trace norm: operator-norm convergence alone does not control trace norm. The paper also needs to pass from trace class images of smooth functions to an operator statement about , and then back to functions with only finitely many derivatives. The obvious shortcut of treating as a bounded operator fails because its natural domain is the smooth-vector space and its closure is generally unbounded. The proof therefore has substantial analytic content beyond elementary ideal inclusions. Source: proof of Theorem 1.3, pp. 4–5.
Lean represents as a Hausdorff finite-dimensional Lie group modelled on a finite-dimensional real normed space , equipped with a regular left Haar measure. It represents as a complete complex inner-product space, without a separability assumption, and the representation by a strongly continuous monoid homomorphism into unitary continuous linear equivalences. The Lie algebra is the tangent space at the identity, and the basis is an arbitrary finite basis of . The quantifiers for and include explicit lower bounds and , matching the paper's convention .
Smooth vectors are exactly those whose orbit maps are smooth. The derived action is the manifold derivative of that orbit map at the identity, used only on smooth vectors. The function-side Laplacian uses right-invariant directional derivatives; its second-order sign agrees with the paper's action. A bounded operator is characterized by on every smooth vector. The paper's essential self-adjointness and density statement identifies this uniquely with ; the theorem carries that characterization as a hypothesis. The hypothesis must be satisfiable, and the interpretation must remain the paper's resolvent.
Continuity on is encoded by a bound on the Schatten -norm for every compact support set, with one constant for all functions supported there. For , the derivative order may depend on the compact set. The Schatten norms and classes are reused published definitions, with norm values in ; no alternate trace norm is introduced. Equation (1) is an identity of distributions tested against smooth compactly supported functions. A complete proof needs the smooth-vector integration lemma, Lie-group test-function approximation, the function-side parametrix and operator ideal estimates. These components are useful beyond this mission.
Classical information can be sent by choosing a quantum state, transmitting it, and asking a receiver to measure it. An ideal noiseless channel seems to have no finite information limit if its carrier can occupy arbitrarily many quantum states. A physical carrier, however, has a limited average energy, and a channel carrying massive particles also has a limited average particle number. Sen(De), Sen, Gromek, Bruß, and Lewenstein ask for the greatest information transfer compatible with both constraints. Their answer connects the channel's information capacity to the entropy of the grand-canonical ensemble familiar from statistical mechanics. Sen(De) et al., pp. 1–2.
The paper also studies how capacities of Bose and Fermi systems respond to condensation and pairing. This mission concerns the result that supports those comparisons: the capacity formula for an ideal, noiseless channel under fixed average energy and particle number. Its finite-dimensional form gives a precise setting in which the optimization and its attaining ensemble can both be stated. Sen(De) et al., pp. 2–4.
The carrier has a finite-dimensional complex state space. Its Hamiltonian assigns energy, and its number operator counts particles. The two Hermitian operators commute, so the system has an orthonormal basis of states with definite energy and particle number. These are the Fock states used as signals. For inverse temperature and chemical potential , the grand-canonical state is
A sender chooses one state from a finite ensemble with probability . Each state may be mixed. The mean state is . A receiver chooses a finite quantum measurement and observes its outcome. The accessible information is the largest mutual information between the sender's label and the receiver's outcome among these measurements. The Holevo quantity is , where is von Neumann entropy. All information and entropy values use base-two logarithms, so their units are bits. Sen(De) et al., p. 1.
Fix and . An ensemble is admissible when its mean state obeys the two exact constraints and . The paper defines as the maximum accessible information among admissible ensembles. For the theorem here, and are the expectations of and in ; no claim of a global inverse from to is needed. Sen(De) et al., p. 2.
The first targets are the paper's entropy bounds: the Holevo bound and . The grand-canonical variational principle says that, under the two fixed expectations, no state has greater entropy than . The first and third targets correspond to existing Open platform statements; the second is drafted here. Sen(De) et al., pp. 1–2.
The goal combines the value of the capacity with its attainment:
where consists of joint energy and number eigenstates with probabilities supplied by . Two further milestones record that this ensemble has mean and that orthogonal pure signals make their classical label information accessible to a measurement. The goal includes an actual maximizing ensemble; an equality involving a supremum alone would leave the paper's attainment claim unstated. Sen(De) et al., p. 2 and abstract.
The result turns a channel optimization over encodings and measurements into a thermodynamic quantity, while specifying signals that reach the bound. The second constraint matters: energy by itself selects a canonical ensemble, whereas fixed average energy together with fixed average particle number selects a grand-canonical ensemble in the paper's setting. This is the connection the authors use when comparing massive Bose and Fermi carriers. Sen(De) et al., pp. 1–2.
A formalization would add a reusable statement linking three kinds of objects: operational accessible information, entropy maximization with conserved quantities, and a concrete optimal ensemble. The shared quantum definitions already exist on the platform; the Holevo and grand-canonical variational statements are Open goals, rather than machine-checked results claimed by this mission. The present draft has compile-checked statements, not proofs of the capacity theorem or those Open goals.
The accessible information is itself an optimization over measurements, while capacity optimizes it again over every admissible ensemble. Merely diagonalizing the grand-canonical state does not establish that no other ensemble, including an ensemble of mixed or noncommuting states, carries more accessible information. The matching attainment assertion also needs an ensemble of the paper's Fock states that obeys both average constraints. The comparison must use the same bit-valued entropy convention throughout, even though one existing grand-canonical platform theorem states its variational principle using natural logarithms.
Lean represents states and observables by complex matrices indexed by a finite nonempty type, with and Hermitian and commuting. The grand-canonical state uses the published Gibbs-state definition. Expected values are real parts of traces, and both constraints are equalities. The finite-dimensional model is exact for finitely many fermionic levels; it is a truncation of the unbounded bosonic Fock space, so this mission does not claim the paper's infinite-dimensional bosonic formula. The theorem permits every real and , with and defined from the resulting state.
The capacity domain includes all finite ensemble sizes and arbitrary mixed density matrices, and accessible information optimizes over all finite POVMs. Restricting the ensemble to Fock-diagonal or pure states, fixing its label type to the Fock basis, or fixing the measurement would turn the capacity claim into a different problem. The maximum is expressed as a greatest element of the value set, which records membership and hence attainment. The reusable work includes the ensemble entropy bound, the joint-eigenbasis interface, and the link between orthogonal signals and accessible information. Contributions that establish these links for the stated definitions or connect the existing Open reference theorems to this interface fit the mission. The paper's separately labelled comparison theorem for bosons and fermions, its asymptotic expansions, and its numerical figures are outside this mission.
Many spaces used in differential geometry are described by the maps permitted into them from simple domains. For a diffeological space, the domains are open subsets of Euclidean space; for a Chen space, they are convex subsets. A map between spaces is smooth when it sends permitted plots to permitted plots. Baez and Hoffnung use the language of concrete sheaves to put these examples in one setting and to explain why their categories share certain categorical properties (Baez–Hoffnung, §§1 and 4). A common theorem matters because it identifies which properties follow from the site of domains and its covers, without relying on a coordinate presentation of either kind of smooth space.
The paper first defines a quasitopos in Definition 8 and states the smooth-space application as Theorem 9, both on page 17. It then builds the general theory of concrete sites and spaces in §§4–5. Theorem 52 on page 40 is the general result from which the smooth-space application follows, using the paper's identifications of Chen and diffeological spaces with suitable categories of spaces (Baez–Hoffnung, Theorems 9 and 52). This mission targets that general theorem.
A site consists of a category of domains and a coverage . A covering family of a domain is a family of arrows into . The coverage requires that a cover can be refined after pulling it back along any arrow. A presheaf assigns a set of plots to each domain and restricts plots along arrows. It is a sheaf when every compatible family of plots over a cover has exactly one amalgamating plot. Compatibility tests equality after further restriction along arrows into two members of the cover (Baez–Hoffnung, Definitions 10–15).
A concrete site has a terminal domain . Maps are the points of , and maps between domains are determined by their action on points. Every point of a covered domain must lift through some covering arrow. The site is also subcanonical: each representable presheaf is a sheaf. These are exactly the conditions of Definition 18, including the subcanonicity of Definition 17 (Baez–Hoffnung, p. 19).
A plot has an underlying function , defined by . The presheaf is concrete if no two distinct plots have the same underlying function. A space is a concrete sheaf, and a map of spaces is a natural transformation of presheaves. Their category is written (Baez–Hoffnung, Definitions 19–20). Its underlying-set functor evaluates a space at .
The goal is the full assertion of Theorem 52:
A quasitopos is locally cartesian closed, has finite colimits, and has a weak subobject classifier. A weak classifier consists of an object and a truth arrow ; each strong monomorphism is the pullback of along a unique characteristic arrow . Local cartesian closure means that for every space , the slice is cartesian closed: it has finite products, and product with any object over has a right adjoint. The paper gives these notions in Definitions 8, 38, 42, and 43 (Baez–Hoffnung, pp. 17, 30, 32–33).
The milestones follow the paper's proof, in order. Four of them are the results cited in the proof of Theorem 52: Proposition 39 (all small limits, computed pointwise), Proposition 40 (the weak subobject classifier), Proposition 45 (local cartesian closure), and Proposition 50 (all small colimits). Together they cover every clause of the target. The others are the results these four rest on:
The classifier in Proposition 40 is the paper's of Proposition 30; the milestone states the existence property (Baez–Hoffnung, pp. 24–40).
The theorem provides a single categorical setting for several plot-based smooth-space constructions. All small limits and colimits allow diagrams of spaces to be assembled within the same category. Local cartesian closure gives parametrized mapping spaces over an arbitrary base, while the weak classifier describes strong subspaces through characteristic maps. These are the specific convenient properties singled out by the paper, and Theorem 9 transfers them to the paper's smooth-space examples (Baez–Hoffnung, §§3 and 5).
The mathematical theorem is already proved in the cited preprint. This mission supplies Lean statements for its general hypotheses, categorical notions, the thirteen results of §5 its proof uses, and its final conclusion. The drafted theorem bodies contain sorry; the work remaining is to prove them and build reusable support for concrete sheaves, pointwise limits, parametrized mapping spaces, and concrete sheafification. A machine-checked development would permit later applications to particular sites without restating the same categorical infrastructure. The present draft does not claim a machine-checked proof.
Presheaf categories already have pointwise limits and colimits, but a pointwise construction need not visibly retain both the sheaf and concreteness conditions. In particular, pointwise colimits of concrete sheaves do not by themselves establish Proposition 50; the result must return to the category of concrete sheaves. For local cartesian closure, constructing a mapping object in the unsliced category handles only the case of a terminal base. Proposition 45 requires the corresponding statement in each slice and for each object over that base. A classifier for every monomorphism would ask for a different property: the paper classifies strong monomorphisms, while it gives examples showing that arbitrary monomorphisms need not be subspaces (Baez–Hoffnung, pp. 10 and 26–37).
The Lean development fixes a universe , a small category with SmallCategory D, a coverage , and a chosen terminal domain with proof that it is terminal. Presheaves are . A covering family is represented by a Mathlib presieve; repeated arrows have no effect on the sheaf or point-covering conditions. The sheaf predicate uses Presieve.IsSheafFor for each member of the coverage. Subcanonicity, faithfulness of , and pointwise surjectivity of covers are all clauses of the concrete-site predicate. The smallness restriction and choice of are explicit scope decisions: the preprint states its theorem for any concrete site, while this development works in Mathlib's small-site setting.
DSpace is the full subcategory of presheaves satisfying the sheaf and concreteness predicates. Its morphisms are natural transformations. The truth-value object uses Bool; the paper's set has the same two elements. Concretization is represented by the image of the map sending a plot to its underlying function, which is canonically the quotient described in Definition 46. The weak-classifier predicate carries a terminal object as existence data; the quasitopos predicate takes finite limits as an instance, reflecting the ambient assumption in Definition 38. The goal's limits clause supplies this instance. In the slice predicate, is used; symmetry identifies it with the paper's .
The classifier must classify strong monomorphisms, and local cartesian closure must range over every slice. Mathlib's Classifier, which classifies all monomorphisms, would make the goal false: the paper's example of the reals with the discrete structure mapping to the standard reals (p. 10) is a monomorphism that is not a subspace. Ordinary cartesian closure is only the case of a terminal base. A model with functions between underlying sets as morphisms would not be Definition 20 and would make Proposition 28 trivial. The complete proof will need Mathlib's coverage and sheaf APIs, strong monomorphisms, pullbacks, slice categories, adjunctions, and limit and colimit interfaces. The concrete-site and -space definitions can be reused for further results of this paper. Lemma 44 takes the existence of the pullback and product as instance arguments, which Proposition 39 supplies; Lemma 47 states the adjunction as the universal property of the quotient map ; Lemma 49 uses Mathlib's plus construction for the Grothendieck topology generated by , as the paper's proof does. Contributions toward the milestone proofs are in scope; the site-specific equivalences used for Theorem 9 are outside this mission.
Classical Max Cut asks for a partition of the vertices of a weighted graph that maximises the total weight of edges crossing it. Its best-known approximation algorithm, due to Goemans and Williamson, rounds a semidefinite relaxation and guarantees ratio . Quantum Max Cut is the analogous problem for a family of local Hamiltonians: each edge contributes a two-qubit term that rewards the two qubits for being antisymmetric, and one asks for the maximum energy of the sum. Estimating it precisely is QMA-complete (Piddock and Montanaro), so attention has turned to efficient approximation algorithms, and to the question of which classes of quantum states can certify a good fraction of the optimum.
A short history of the approximation ratio on weighted graphs:
Let be a simple graph on with nonnegative edge weights (the paper's standing assumption). Each vertex carries a qubit; a state is a vector , and it is a unit state if . With the Pauli matrices acting on qubit written , the quantum Max Cut Hamiltonian is
each edge counted once. The term equals twice the projector onto the singlet , so is positive semidefinite, and
Two weight statistics appear throughout: the total weight and, for a vertex , , the largest weight of an edge incident to (zero for an isolated vertex).
A tensor product of 1- and 2-qubit states is obtained by partitioning the qubits into blocks of size one or two (a pair need not be an edge of ), choosing a unit vector of or for each block, and multiplying the block amplitudes. Product states (all blocks of size one) and singlets placed on a matching are examples; a generic entangled state of three qubits is not.
For every graph with nonnegative weights there is a tensor product of 1- and 2-qubit states such that
The constant is the exact minimum of the optimisation problem (28) of the paper.
The proof combines an upper bound on with three candidate states:
The result shows that the limitation of product states for quantum Max Cut is not a limitation of efficiently describable states: allowing entanglement only within disjoint pairs of qubits already guarantees a fraction strictly above on every weighted graph, including those (a single heavy edge) where product states are stuck at exactly . The accompanying algorithmic statement (an efficient randomized algorithm with ratio ) improved the best known efficient approximation ratio at the time. The upper bound of Lemma 1 is a quantitative form of monogamy of entanglement on a star: the centre qubit cannot be maximally entangled with all of its neighbours.
The theorem is proved in the paper; none of it is formalized. A complete development gives a machine-checked model of a frustrated quantum spin Hamiltonian on arbitrary weighted graphs, a formal upper bound on its ground-state energy, and an explicit certified family of entangled states. The final step, (28)–(29), is evaluated in the paper "by a computer"; a formal proof replaces that evaluation.
The obvious upper bound, , is too weak: it allows every edge to be maximally entangled simultaneously, and with it no ratio above follows. The improvement needs the star bound of Lemma 1, which the paper derives from the Lieb–Mattis theorem on the spin of the ground state of bipartite antiferromagnets, restricting the problem to the Hamming-weight-one sector where the Hamiltonian becomes a weighted graph Laplacian. Neither Lieb–Mattis nor the angular-momentum decomposition of is available in Mathlib. The combinatorial side (Lemma 2) needs a careful choice of a maximal incident edge at each vertex and an argument that these edges form no cycle. Eq. (25) is an exact energy computation for a state that is entangled across a matching.
Fin n, basis configurations Fin n → Fin 2, states (Fin n → Fin 2) → ℂ, operators complex matrices indexed by configurations; onSite i σ places a matrix on qubit . The graph is a SimpleGraph (Fin n); weights are w : Sym2 (Fin n) → ℝ with ∀ e, 0 ≤ w e in every statement. sums over the ordered representatives of the edges, so each edge is counted once. The energy is the real part of .onSite, energies of computational basis states (equal to cut values), partial-trace style computations for tensor products of blocks, and a Laplacian/Gershgorin bound; the Hamiltonian layer is reusable for later quantum Max Cut missions. Contributions of any of these as separate lemmas are welcome.Permutation of tensor factors is a basic operation in quantum information and in the algebra of braids. A braid representation assigns an operator to each crossing so that different drawings of the same braid act identically. A Yang–Baxter equation adds spectral parameters to this local consistency condition; such families appear in integrable lattice models and in constructions of quantum gates. The paper by Zhang, Kauffman, and Werner asks when one operator family built from permutation and partial transpose can meet both requirements. It connects two familiar operations on bipartite matrices with algebraic relations on three tensor factors.
The article studies several related representations and two main theorems. This mission concerns Theorem 1 in §6.3 and the source equations that support it. The theorem is a classification of a specific three-term family, not a claim about arbitrary Yang–Baxter solutions. The paper's printed wording has degenerate counterexamples already present elsewhere in the same article. The target here makes their exclusions explicit, so that the formal statement records the intended classification. The source is the first arXiv version, quant-ph/0606005v1; page and equation numbers below refer to that version.
Fix an integer and let with its standard basis. The permutation operator acts on by . The partial transpose transposes the matrix index belonging to the second copy of . Write . This operator is and satisfies . In dimension two the paper also uses ; the star's position matters, since and are different matrices. These definitions and identities are in §2.1, pp. 5–6.
For fixed complex coefficients and , the family under study is
Here is the spectral parameter: it is the coefficient of . On , the subscripts and mean that an operator acts on the first two or last two factors, with the identity on the unused factor. The braid relation is . The paper considers two parameterized versions, with multiplicative law in equation (14) and additive law in equation (15):
The equations are identities for all indicated parameter pairs, with fixed. The source gives the braid relation as (54), defines the family in (69), and states the two Yang–Baxter forms in §3.1 and §5.
For and , classify this family by three equivalences. At every nonzero ,
If , the family satisfies the additive equation (15) for all exactly when and . The family satisfies the multiplicative equation (14) for all exactly under the same dimension and coefficient condition. The source's “only for” statement and the sufficiency part of its proof support equivalences; the explicit guards correct the printed exceptions. This is the mission goal.
The milestones capture the source's operator identities and ; the dimension-two braid and mixed relations (66)–(67) for and ; the second dimension-two braid branch displayed in (70); the coloured identity (74) for ; the necessary coefficient system (127) above dimension two; and Appendix B's higher-dimensional exclusions, stated with the same corrected guards. These are the source's own named or displayed claims in the order useful to a reader of the goal.
The result locates the precise dimension in which this particular linear combination supplies braid and spectral-parameter solutions simultaneously. It also distinguishes two braid branches: gives the parameterized family , while gives another fixed braid matrix. Above dimension two, with the stated nonzero conditions, neither branch survives as a solution of the three requested relations. This keeps a tempting general-dimensional extrapolation from being treated as a theorem.
The source result is a published mathematical argument, but these Lean statements are proposed open goals. A completed mission would produce machine-checked proofs for the classification and its selected intermediate identities in one reusable matrix representation. The definitions of permutation, partial transpose, and the two three-factor placements may also serve later formalizations of braid and Yang–Baxter calculations. This mission does not claim to formalize the paper's second theorem, its full virtual braid group development, or its later applications to gates and Hamiltonians.
The dimension-two formulas are finite matrix identities, but the classification asks for necessity as well as sufficiency. Verifying the displayed solution matrices alone cannot rule out other coefficients. In higher dimension the paper compares terms in an expansion on three tensor factors. Its observation that the ambient vector space has dimension does not by itself establish independence of the 15 operators being compared; a formal proof must justify every coefficient conclusion that it uses. Appendix B's sentence about a unique solution at fixed parameters also has degenerate counterexamples, so the milestone records only the necessary equations (127). These issues make the source's computational looking argument a substantive formalization task.
The Lean model takes and represents two-factor and three-factor operators by matrices indexed by Fin d × Fin d and Fin d × Fin d × Fin d. Fin d starts at zero while the paper labels basis vectors from one; this only changes names of indices. Tensor placement is defined entrywise, with the identity matrix on the unused factor. Scalars and spectral parameters are complex. The goal quantifies over every natural-number dimension , every fixed with , and every indicated spectral parameter. In (14), the paper introduces and , hence initially nonzero. The Lean predicate quantifies over all complex ; for polynomial matrix identities these formulations are equivalent.
The definition is retained explicitly. Replacing it by an unrelated matrix with a convenient identity, fixing the dimension to two in every definition, or varying the coefficient as the spectral parameter would change the problem. The guard excludes the higher-dimensional braid family from §6.1, (60), and excludes the rational additive solution in §3.2, (21). At , all three basic matrices are scalar, so the paper's implicit convention is stated. Contributions that establish the shared identities, the two-dimensional coefficient classification, or the uniform higher-dimensional exclusions all advance the target.
A quantum computer that runs long computations must protect its data with a quantum error-correcting code and must compute on the encoded data without letting errors spread. The simplest gates with that property are transversal gates: a code is laid out in several code blocks, and a transversal gate couples each physical subsystem of one block only to the corresponding subsystem of the other blocks, so a single fault never becomes several faults inside one block (Gottesman 1997; Aliferis, Gottesman, Preskill 2006). Every known code has some encoded gate that is not transversal, and fault-tolerant schemes pay for the missing gates with expensive constructions such as magic-state distillation. Whether some code has a universal transversal gate set was a long-standing question.
Timeline.
A composite quantum system consists of finitely many physical subsystems , subsystem having dimension . Operators on are complex matrices on . A product operator is with acting on subsystem , and is the group of unitary product operators ().
A quantum code is a subspace of the state space, represented by the orthogonal projector onto it; its dimension is the dimension of the encoded system, and the code is nontrivial when this dimension is at least . An error is detectable when . The code is local-error-detecting when every error on any single subsystem is detectable: for every operator acting on one subsystem.
A unitary is logical when it preserves the code space,
and denotes the logical unitary product operators. An encoded unitary is a unitary operator of the code space (, ). A set of unitaries is universal when every encoded unitary is approximated to arbitrary accuracy by the actions , , on the code space.
For a code made of blocks , each with subsystems at the same positions and a block code , the joint code is . The transversal part collects subsystem of every block, and a transversal unitary is a product of unitaries, one on each transversal part.
For block codes , each local-error-detecting, with , the set of transversal logical unitaries is not universal:
The same conclusion for product operators on the physical subsystems of a single local-error-detecting code with .
In attack order: Lemma 1 (logical unitaries form a group); Lemma 2 (logical unitaries in a closed group of unitaries form a closed subgroup); is a compact group; the derivative step ; elements of the Lie algebra of are sums of local Hermitian operators; for a logical sum of local Hermitians; the identity component of acts on the code space as a scalar; has finitely many actions on the code space up to phase; Theorem 1; and the detectability of an error on a single transversal part.
The result. The theorem rules out the simplest route to fault tolerance for every code that detects single-subsystem errors, which includes every code of distance at least . It explains why every fault-tolerant architecture needs a non-transversal ingredient (state injection and distillation, code switching, gauge fixing, measurements with feed-forward), and it is the starting point for later refinements: approximate and covariant versions for continuous symmetries (Faist et al. 2020), and restrictions on the level of the Clifford hierarchy reachable transversally (Bravyi–König 2013).
Formalizing it. The result is proved; no machine-checked proof of it is known to exist. The mission produces a checked statement of the theorem for arbitrary finite-dimensional subsystems and arbitrary (non-stabilizer) codes, together with a reusable layer: tensor-product operators on index-typed subsystems, codes as projectors, logical operators, local error detection, encoded universality and block codes. Related platform items are QAlgorithms_Defs_QECC (qubit stabilizer codes, detectability for submodule codes) and QAlgorithms.GottesmanIntro.knillLaflamme (the error-correction criterion), which use a different model of codes and are not imported here.
The paper's argument runs through Lie theory: is a closed subgroup of the compact group , so it is a compact Lie group with finitely many connected components; its identity component is generated by exponentials of its Lie algebra, and local error detection forces that Lie algebra to act on the code space by scalars. None of this is about the code alone; the difficulty is the passage from a closed matrix group to its Lie algebra and back (exponential coordinates, connectedness of the identity component, finiteness of the component group of a compact Lie group). Mathlib has the matrix exponential and compactness of the unitary group but not Cartan's closed-subgroup theorem or the Lie algebra of a closed matrix group.
A frequent first idea, that itself is a finite group, is false: every global phase is a logical product unitary, so always contains a circle. Only the action of on the code space is finite, and only up to phase; a statement that ignores the phase is false.
Subsystem is a finite index type (so ), and the system has basis ; operators are Matrix over ℂ, unitaries are Matrix.unitaryGroup. A code is its projector (Hermitian, idempotent) and its dimension is Matrix.rank; "nontrivial" is . Closure is in the standard topology on complex matrices, which is the topology of any norm. Exponentials are NormedSpace.exp with the factor of the physics convention (footnote 1).
Disclosed restatements:
Universality is defined only through approximation of encoded unitaries, local error detection quantifies over every matrix on one subsystem, and is the full intersection of with the logical unitaries, so no hypothesis trivializes the conclusion; at rank the conclusion is false, which is why the rank hypothesis is and not .
A complete development needs the Lie algebra of a closed subgroup of Matrix.unitaryGroup, connectedness of the identity component via exponentials, and finiteness of the component group of a compact matrix group. These parts are reusable far beyond this mission, and contributions of them, as well as alternative proofs of Theorem 1 that avoid Lie theory, are welcome.
Small retailers often cannot pay for their orders out of their own capital and borrow from banks to do so. Banks in turn are regulated: risk-control rules such as value-at-risk caps limit how much they may lend against an uncertain revenue, and they charge fixed fees to process a loan. Loan insurance, offered by insurers or guaranteed by governments, relaxes those caps for a premium. The common view, in practice and in policy discussions of financing for small firms, is that a higher credit limit and a cheaper loan help every firm in the supply chain.
Wang and Cai (Management Science, 2023) study a supplier selling to such a capital-constrained buyer and show that the common view fails in a precise region of parameters. They build on the capital-constrained newsvendor literature, which studies how financing frictions distort ordering and pricing (Buzacott and Zhang, 2004; Kouvelis and Zhao, 2012), and on the price-only wholesale contract of Lariviere and Porteus (2001), whose equilibrium price and quantity are the benchmark without any capital constraint.
Demand for a product with retail price has distribution function , complementary distribution , density on and failure rate , and satisfies the increasing generalized failure rate (IGFR) property: is increasing. The expected sales of an order are .
A supplier with unit cost sets a wholesale price . A buyer with initial capital then chooses an order and how to finance it:
The supplier earns . The game is a Stackelberg game solved backwards, with the paper's goodwill tie-breaking rule: a firm indifferent between choices picks the one better for the other firm. and denote the supplier's and the buyer's equilibrium profits.
The equilibrium is described through explicit thresholds. is the buyer's additional revenue from insurance at price (the paper's equation (A-7)); the buyer insures exactly when . are the two roots of . With , and defined in the paper's appendix, and . The insurance-cooperation region (Area II) is
In it, the equilibrium price is : the supplier lowers its price just enough for the buyer to be willing to insure.
Assume , and the paper's global assumptions, and Area II. Then
The monotonicity is stated along every segment of (or ) on which the hypotheses hold at each point, and for every equilibrium at the two ends.
In attack order: the buyer's best response and the threshold (Lemma A.7), its monotonicity and unimodality (Lemma A.7, "Moreover"), the shape of the supplier's profit in (Lemma A.8), the monotonicity of (Lemma A.9), the equilibrium in Area II (Proposition 1 item 1(b), including existence), the comparative statics of (Proposition A.8, "Moreover"), and the closed-form equilibrium profits in Area II (proof of Proposition 2).
The result reverses an intuition that regulators and firms rely on: a tighter or costlier bank loan, normally a loss for everyone, here benefits the supplier, because the buyer is pushed towards insurance and the supplier then needs to cut its price less to keep the buyer insuring. The buyer loses at the same time, so the two firms' interests over bank credit terms conflict in this region. The paper builds on this a parallel statement about curtailing loan insurance (Proposition 3) and a Stackelberg prisoner's dilemma (Proposition 5); both are outside this mission.
The paper's proofs are derivative computations through the implicit function theorem applied to piecewise-defined thresholds, with several details left to figures. A machine-checked proof would pin down the exact hypotheses under which the region exists and the claims hold, settle the role of the tie-breaking rule (without which no equilibrium exists in Area II), and give a reusable formal model of a capital-constrained newsvendor with several financing modes. No part of the paper has been formalized before.
The obvious argument differentiates the closed-form equilibrium profits in and . It requires first knowing that the equilibrium is the price throughout a segment of parameters, which in turn needs the full best-response analysis of the buyer (three financing modes, two binding regimes for each loan cap), the unimodality of , and the comparison of the supplier's profit at with its profit at the competing price . Each threshold is defined as a root of an equation involving and , and the region boundaries and themselves move with and . The implicit function theorem gives local derivative signs; turning them into strict monotonicity along a segment needs continuity of the thresholds across the switches between regimes.
All quantities are real numbers. Demand is a probability measure on with a density that vanishes on , is continuous and positive on the positive open support, with finite mean and the IGFR property; continuity, positivity and the finite mean are added to the paper and disclosed. Expected sales use the published SupplyChainTheory.expSales. IGFR is imposed where the failure rate is defined, on the positive support with ; this includes bounded-support demand laws such as the uniform distribution. Prices range over . The loan limits are parameters; their value-at-risk derivation is not modelled. In the supplier's threshold , an inverse of expected sales above its range is treated as inside the minimum with the finite unconstrained order. Lemma A.8's buyer profit is nonincreasing in price; strict decrease additionally requires positive initial capital, since with zero capital and a positive bank fee the buyer can earn zero throughout a high-price interval.
Every threshold is defined from the paper's own equation as an infimum or supremum of an explicitly named set, never passed as a free parameter. The goal is about the game's equilibria (IsEquilibrium) on the region AreaII; restating it about and the closed-form profits, or defining the profits or Area II through the equilibrium's expected shape, would trivialize it and is excluded. Proposition 1 item 1(b) asserts existence of an equilibrium in Area II, so the goal is not vacuous.
A complete development needs the inverse functions and and their continuity and derivatives, the newsvendor with a spending cap, and the implicit-function arguments for the roots. The capped newsvendor and the financing-mode best response are reusable for other supply-chain-finance missions. Contributions to any milestone, and to the missing lemmas about under IGFR, are welcome.
A manufacturer that sells through a retailer usually knows less about end-customer demand than the retailer does. In the classical one-shot screening model (Laffont and Martimort, 2002) the manufacturer offers a menu of quantity–payment pairs, pays the well-informed retailer an information rent to reveal high demand, and distorts the low-demand quantity downward to keep that rent small. Real vertical relationships are repeated, and after each selling season the retailer can choose whether to share its past sales data (point-of-sale data, sell-through reports) with the manufacturer. Such data says nothing about future demand when demand is i.i.d., yet it lets the manufacturer check, after the fact, whether the retailer reported truthfully.
Shamir and Yehezkel (2023) ask when the retailer, who owns the data, wants to share it. The manufacturer can never lose from more information, since it can ignore it. The retailer's side is the interesting one: sharing lets the manufacturer punish misreports and so cut the retailer's rent for a given quantity, but it also lets the manufacturer raise the low-demand quantity, which increases the rent. The paper's main result, Proposition 3, gives an explicit threshold on the discount factor that separates the two cases. The question belongs to the literature on trust and information sharing in supply chains (for example Özer, Zheng and Chen, 2011).
In every period demand is high () with probability and low () with probability , independently across periods. The inverse demand is linear, with , so the retailer's revenue from quantity in state is , and . The retailer observes the state before ordering; the manufacturer does not.
The manufacturer offers a menu : quantity for the payment . The per-period expected profits are
Both firms discount future periods by .
In the static problem the manufacturer maximizes subject to participation and incentive compatibility . Its solution has and , and the retailer's expected profit is . The paper assumes , so that .
In the repeated game, the manufacturer offers the same menu every period and reverts to the static menu forever after a deviation. The dynamic participation constraint, common to both regimes, is
Without sales information a misreport cannot be detected, so incentive compatibility stays static. With sales information a misreport is detected at the end of the period and punished:
In each regime the manufacturer chooses a menu that maximizes among all menus satisfying that regime's constraints. Write and for the retailer's expected profit at the optimal menu without and with sales information.
For , , and , and for every optimal menu of each program,
Proposition 3 answers the paper's central question: sharing past sales data can arise voluntarily, and it does so exactly when the retailer is impatient enough, . For patient retailers the repeated relationship already sustains a large low-demand quantity without verification, and the retailer loses more rent from detection than it gains from the higher quantity. Since the manufacturer always gains, is also the region where sharing is a Pareto improvement for the channel. The threshold depends on alone, not on or .
The results are proved in the paper by first-order conditions on the reduced profits and direct substitution. Nothing in this mission is machine-checked yet. The formalization would turn the paper's chain (binding constraints, slack constraints, reduced profit, maximizer, retailer profit, sign of the gap) into one verified argument, including the step the paper treats informally: that the relaxed program with two binding constraints has the same optimum as the full four-constraint program, and that the optimum is unique.
The algebra of (15), (30) and (31) is long but mechanical. The substantive step is optimality over all menus. The paper drops two of the four constraints, solves the remaining two with equality, and maximizes the resulting quadratic. A rigorous version must show that no feasible menu, at any quantities, earns more than the reduced profit, that the reduced profit has a unique maximizer, and that the two dropped constraints hold at the candidate (Appendix C). Proposition 3 itself is stated about any optimal menu, so it needs uniqueness, not only existence, before the closed forms can be substituted. The naive route of evaluating (31) at the closed-form menus proves the comparison only for those menus, not for the optimum of the program.
Everything is over with the linear demand of the paper. Parameters form a structure Params with fields p, VH, VL, δ; the predicate Params.Standing collects , , (footnote 2 of the paper) and . The bound is added to the paper's because the constraints divide by . A menu is a structure Menu with fields qH, TH, qL, TL; every program also requires , a condition that does not bind at the optima. Constraints are weak inequalities as printed. "Optimal" means feasible and maximizing over all feasible menus (IsOptimalNE, IsOptimalE). The retailer's profit is the ex-ante per-period , not the discounted sum.
The goal must not be stated at the closed-form menus menuNE, menuE: that version is the algebraic identity (31) and skips the optimization entirely. Likewise the retailer's profit is defined from the menu, never by the formulas (15) or (30).
All definitions live in one file, SalesTrust.Sharing.Model. Contributions are welcome on any milestone; the two relaxation arguments (milestones 2 and 5 with Appendix C) and the uniqueness parts of Propositions 1 and 2 are where the work is. The relaxation step is common to two-type screening models, so a general statement of it would be reusable beyond this mission.
Prox-functions determine how subgradient and mirror-type optimization methods turn a direction of improvement into the next feasible point. On a probability simplex, that step should respect the geometry of probability vectors and be computable from the current direction. The entropic prox-function gives the softmax rule, familiar from the logit model of discrete choice. Müller, Nesterov and Shikhman ask whether a wider family of random-utility choice models supplies prox-functions with the same operational link between optimization and choice probabilities. Their 2019 preprint, published in Mathematics of Operations Research in 2022, states that it does: the convex conjugate of the model's surplus is a prox-function on the simplex.
This question matters to optimization because the random-utility law specifies a geometry and a computable update together. It matters to discrete-choice modeling because the update from an optimization problem can be interpreted as a vector of probabilities of choosing each alternative. The mission covers the general result in Section 2 of the preprint, rather than its later specialized generalized-extreme-value parameters or economic application.
There are alternatives. A deterministic utility vector is perturbed by a random shock vector with law . Assumption 1 requires a finite mean, absolute continuity with respect to Lebesgue measure, and full support in . The surplus function is the expected best perturbed utility,
The convex conjugate of this function is taken over every utility vector, with extended-real values:
The candidate domain is the simplex . The model's choice probability is the chance that attains the largest perturbed utility. Absolute continuity makes ties null, so including ties in this event does not change its probability. The paper identifies with the th derivative of in equation (1).
A prox-function on is continuous and strongly convex there, and the optimization step that maximizes over has a unique, directly available answer. Here strong convexity uses . The relevant smoothness of uses the dual norm .
The goal combines the three claims that form the paper's Section 2 main result. First, Theorem 1 says that the finite domain of is exactly , and that is continuous even at the boundary of that simplex. Second, Theorem 2 supplies an explicit strong-convexity parameter. For distinct alternatives , let be a density of and let be a mode of that density. Then
for and . The double sum is over ordered pairs. Third, under the strong-convexity premise stated at the opening of §2.2.3, Theorem 4 identifies the optimizer and the attained value:
The milestones record Lemmas 1, 2, 3 and 5, equation (1), and Theorems 1, 2 and 4. They cover the paper's elementary surplus properties, the choice-probability identity, the relation between strong convexity and strong smoothness, the Hessian norm criterion, the matrix trace bound, and the three final clauses.
The result gives a family of simplex prox-functions indexed by shock laws, rather than by a single entropy formula. The optimizer in the auxiliary problem is a choice-probability vector, so a prox update has an explicit behavioral interpretation. The strong-convexity bound supplies the geometric constant used when such a function enters first-order optimization estimates. The paper's later sections derive parameters for generalized extreme-value models and apply the update to a consumption cycle; those consequences motivate the general theorem but are outside this mission's goal.
The result is proved in the cited paper; this mission asks for its Lean formalization. The current draft has compile-checked statements with proof placeholders. A complete development would add machine-checked proofs of the listed lemmas and goal, together with reusable results about conjugacy, probability laws of differences, and norms of finite matrices. No proof of this specific paper result is claimed here.
Continuity in the relative interior of a simplex does not by itself establish continuity at its boundary, which is part of Theorem 1. The choice-probability formula connects differentiation of an expected maximum with an event defined by inequalities; ties, measurability, and integrability must all be handled. The strong-convexity constant then depends on controlling the Hessian with the norm induced from to , while retaining the ordered-pair sum of density values. A direct substitution of the default norm on finite coordinate functions would change the theorem because that norm is .
Alternatives are Fin n with [NeZero n]; vectors are Fin n → ℝ. The law is a probability measure on shock vectors. Assumption 1 explicitly includes coordinate integrability, absolute continuity and full support. Its integrability clause keeps the Bochner integral defining meaningful, rather than allowing the integral's default value on a nonintegrable function. The choice event includes ties, which have zero measure under Assumption 1. The conjugate is EReal valued and takes its supremum over all utility vectors; defining it by a maximum over the simplex or by an entropy formula would change the result.
The real value of is used only alongside its finiteness on . Strong convexity uses an explicit sum, while Mathlib's norm on Fin n → ℝ represents . Coordinate derivatives and the Hessian are formed from Fréchet derivatives. The differences have fixed, nonnegative measurable density versions tied to their pushforward laws; each mode maximizes its selected version pointwise. Theorem 4 carries the positive strong-convexity premise stated in its section preamble. The paper uses twice differentiability of on page 7 without deriving it from Assumption 1. This mission explicitly adds ContDiff ℝ 2 E to the Hessian-dependent result and the goal. It is a necessary disclosed strengthening of the paper's stated assumptions.
For one alternative the simplex is a point, and the displayed denominator in is zero. Lean evaluates the reciprocal as zero. The strong-convexity inequality is then vacuous between distinct points; the draft asserts positivity of the displayed only when and separately asserts that some positive parameter exists for every , as Definition 1 requires. No empty set of alternatives is admitted. Contributions should keep the unrestricted conjugate, the law-dependent densities, the exact inequality, and the paper's constants. General finite-dimensional convex duality and induced matrix-norm lemmas would be reusable beyond this model.
"Buy , get one free" (BXGO) programs are among the most common loyalty schemes: coffee shops, car washes, golf courses and hotel chains hand out a free unit after a fixed number of paid purchases. A long empirical literature documents that such programs change behaviour, most visibly through point pressure, the acceleration of purchases as a customer approaches the redemption threshold (Kopalle et al. 2012; Lewis 2004). Whether that acceleration is worth the free units given away is a question for the firm's pricing and marketing operations.
Liu, Sun and Zhang (2021) study the question in a fully rational model. A forward-looking consumer facing a BXGO program solves a dynamic program, and her optimal decisions induce a Markov chain on her point inventory. The paper shows that discounting alone produces point pressure, and then asks whether the program raises the firm's long-run profit. Its answer without transaction utility (the consumer's extra enjoyment of a free unit) is negative under explicit conditions: Proposition 3. This mission formalizes that result together with the structural lemmas its proof rests on.
A monopolist sells a nondurable product at marginal cost , so revenue and profit coincide. A BXGO program is a pair : a fixed price and a threshold . A consumer earns one point per purchase, and holding points she may redeem them for a free unit, returning to points.
In each period the consumer is in the market with probability . In the market she values the product at and has an outside option , equal to with probability and to otherwise, where . A redemption gives her a transaction utility on top of . She discounts with factor .
Her value function on the point inventories solves the optimality equations
for , and the analogous equation at with (redemption) in place of . She buys, or redeems, when this is at least as good as the outside option. Her decisions turn the point inventory into a Markov chain on that moves from to (from to ) or stays put. The firm's profit is times the long-run purchase probability per period.
Two constants recur throughout:
So do the boundary prices and of the paper's p. 10, which separate the price ranges of the consumer's four response patterns (Proposition 2). The benchmark is the profit of the best price without a program, : selling to the consumer only when her outside option is , or always, at the price .
Assume and either (a) and , or (b) and . Then for every program and every solution of the optimality equations, the average expected revenue over the first periods, of a consumer who starts with points, satisfies
The statement covers every price, including those between the ranges of Proposition 2, where the paper asserts but does not show that the consumer drops out.
Proposition 3 separates two effects of a reward program. Point pressure raises the purchase probability above that of a consumer who never accelerates. Discounting forces the firm to lower its price to keep her in the program, and without transaction utility the second effect dominates. The paper's Proposition 4 shows that a small positive reverses the conclusion, and its §6 shows that an expiration term reverses it too. The result therefore locates exactly where the profitability of BXGO programs comes from: transaction utility or expiration, not the threshold alone.
The result is proved on paper but not machine-checked. The paper's proof of Proposition 3 works with the closed-form profits of four behavioural cases. Formalizing it requires connecting those closed forms to the consumer's dynamic program and to the long-run behaviour of the chain her decisions induce, and that connection is part of the mission. Machine-checked proofs of Propositions 1–2 also give a reusable template for monotone threshold policies in discounted point-accumulation problems.
The value function has no closed form until the consumer's behaviour is known, and her behaviour is defined by the value function. The paper breaks the circularity case by case: assume a behaviour, solve the linear equations it induces, and read off the price range in which that behaviour is consistent. A formal proof has to show that the four ranges, together with the gaps between them, account for every price. At a gap price the consumer either never buys from points or behaves as in a neighbouring case.
Reading profit as "price times stationary demand" also needs care. At high prices, at or at the induced chain is reducible, and the long-run revenue from points need not equal the revenue under an arbitrary stationary law. Lemmas 2 and 3 bound only the four closed forms; turning them into a bound on the Cesàro averages of the actual chain is the remaining step.
All quantities are real. Params bundles , and Params.Standing is the list of standing assumptions: , , , . The value function is a hypothesis, IsValueFn P p X J, meaning that J : ℕ → ℝ satisfies the optimality equations on . The equations have exactly one solution there, and its values beyond play no role. Decisions break ties in favour of buying or redeeming, as in the paper's Corollary 1 and Proposition 2. The chain lives on Fin (X+1). Profit is the Cesàro average avgRevenue of expected revenues from state , computed from the transition matrix of the consumer's own decisions. Stationary distributions use the published MarkovChain.IsStationary.
The goal cannot be made true by construction. Profit is computed from the decisions of , never from the paper's closed forms, and the goal quantifies over every price and every threshold with no assumed behaviour.
Hypotheses added to the paper's statements:
Proofs of individual milestones are welcome. So are general lemmas about Cesàro averages of finite stochastic matrices and the two-sided comparison of discounted value functions, both of which are reusable beyond this mission.
Payments for ecosystem services compensate landowners for conservation that a program values but cannot directly provide. A contract designer must decide how to pay when landowners differ in the amount of forest they would conserve without a payment. That baseline conservation type is privately known, so a contract can pay for forest that would have remained anyway. Li, Ashlagi and Lo study this problem for forest conservation and ask how much payoff a simple, uniform price can guarantee relative to an optimally tailored contract (Li, Ashlagi and Lo, 2022, §§1–2).
The paper's Theorem 1 establishes a guarantee that does not depend on the type distribution: a price equal to half the program's value per unit secures at least half of the optimal contract payoff. This matters to a designer who can estimate the conservation value but cannot reliably estimate the distribution of landowners' private baselines. The guarantee concerns the principal's payoff after payments, rather than the total area conserved or the agent's utility (Li, Ashlagi and Lo, 2022, §4, Theorem 1).
An agent owns an initial forest area . Their type is the fraction of that area they would conserve without incentives. The publicly known type distribution is supported on . The agent selects a conserved area . Conservation above the baseline has cost , where and
The principal values each conserved unit at . A direct revelation contract specifies an action and payment for each reported type. It is feasible when the action respects the forest-area bounds, payments are nonnegative, truthful participation gives nonnegative utility (individual rationality, IR), and truthfully reporting the type maximizes utility among all reports in the type interval (incentive compatibility, IC). Its payoff is . These are the model and contract constraints on pages 4–5 of the source preprint.
A linear contract pays the same price for every unit of conserved area, including area the agent would conserve without incentives. The agent's action at price is on the type interval. The principal then receives ; the best such payoff is . The price and payment apply to the whole action , as in Equation (3) of the source preprint.
For every probability law on the stated type interval, every feasible direct contract with a defined expected payoff, and every best-response action to the price , Theorem 1 gives
It follows that every feasible direct-contract payoff is at most . The universal bound expresses the comparison with an optimal contract even if a maximum over contracts is not attained. The milestone list contains the linear best response, the doubled payoff identity of Equation (7), the information-rent-free upper bound of Equations (4)–(5), and the pointwise comparison from Appendix A.4. All four come from the paper's §4 and Appendix A.4.
The guarantee makes the price a distribution-independent benchmark for this conservation model. The paper's Example 3 gives a single type at where the factor of two is attained, so a larger universal fraction cannot be claimed under the same assumptions (Li, Ashlagi and Lo, 2022, p. 9). The result also implies the best linear contract has the same worst-case guarantee, even though finding its maximizing price may depend on the distribution.
The result is proved in the paper but is not yet machine checked in this mission. Formalizing it will give a reusable definition of this conservation-contract model, with explicit IR and IC constraints, and Lean statements for the price guarantee and its central comparisons. It can also support later formalizations of the paper's conditional contracts and convex-cost extensions, which are outside this mission.
The benchmark is the payoff of an optimally designed contract with actual payments, under private information. Replacing those payments by conservation cost changes the benchmark: the agent may receive an information rent. Likewise, optimizing independently for each type describes an unconstrained surplus, not the direct contract in Theorem 1. A formal statement that uses either quantity as the goal's “optimal payoff” would miss the paper's claim. The paper compares the linear payoff with a bound on the contract payoff, and its Appendix treats type distributions that need not satisfy the monotone-hazard-rate condition used in the shorter proof sketch (Li, Ashlagi and Lo, 2022, pp. 10, 24–26).
Lean represents types, areas, prices and payoffs as real numbers. The law is any probability measure on the reals concentrated on ; atoms, including a point mass, are allowed. The standing parameter conditions are , and . Positive is made explicit because the paper uses . The theorem adds as stated in Theorem 1. Feasibility and best-response conditions range over supported types, and IC compares every pair of types in that interval. The contract's action and payment are integrable so their expected payoff is defined. The bounded best-response action needs no separate integrability assumption.
The formalization uses a supremum over nonnegative linear prices. Under the standing conditions its values are bounded above, so this is the ordinary best-payoff bound rather than a default value of a total supremum operation. The goal ranges over feasible direct contracts with IR, IC, action bounds and nonnegative payments; it retains the actual in the payoff. A goal stated only for an unconstrained surplus or with an empty feasible class would not represent Theorem 1. Useful contributions include proofs of the four milestones, measure-theoretic facts about supported type laws, and lemmas about the price-payoff supremum.
Clustering methods must infer a partition from noisy observations, while the quality of a partition is usually judged against labels that the method cannot see. Fei and Chen study a balanced sub-Gaussian mixture model in which a semidefinite program (SDP) estimates a cluster matrix from pairwise distances. Their Theorem 1 relates its error to a simpler integer program allowed to know the true cluster centers. This comparison makes the SDP's error interpretable through an explicit benchmark, even when exact recovery is unavailable. The paper also investigates semi-random perturbations, but this mission targets the Model 1 comparison on which that broader discussion builds.
The tension is that an SDP solution may be fractional. Its entries express pairwise affinities, whereas an assignment matrix places each point in exactly one cluster. The result bounds the fractional matrix's entrywise error by an integer assignment error without assuming that the SDP solution itself is integral. That is the hidden-integrality claim relevant to this mission.
There are observations in and clusters. The true label of point is , and every cluster contains exactly points. For unknown centers , the observations have the form
The noise vectors are independent, measurable, zero-mean, and sub-Gaussian. Their vector sub-Gaussian norms are at most . The minimum center separation and signal-to-noise ratio are
The SDP uses the squared-distance matrix . It minimizes over real matrices with row sums , diagonal entries one, nonnegative entries, and symmetric positive semidefiniteness. Write for any optimum. The true cluster matrix is when and otherwise. Its error is measured by the entrywise norm .
The benchmark is an Oracle Integer Program. An assignment matrix has zero-one entries and exactly one one in each row. The true assignment is . The oracle sees the centers and augmented observations with the fixed , so its noise is four times the realized noise in . It minimizes
The Oracle error is the largest among assignments satisfying . The Oracle feasible set has no balance constraint. In contrast, the SDP retains the row-sum constraint inherited from balanced clustering.
The goal is the paper's quantitative comparison. It asserts that universal constants and exist such that, when
an event of probability at least has, for every realized SDP optimum , the bound
The constants are independent of , the centers, the labels, and the noise law. The event and the SDP optimum are chosen after the random observations are realized. The theorem fixes the factor two and the failure-probability expression exactly as printed.
The eight milestones follow the statements in Section 5: the six structural properties of the SDP error matrix (Fact 2), the basic inequality (16), the signal estimate (Proposition 3), the two noise estimates (Propositions 1 and 2), the representation of the remaining term (Lemma 1), the identity between the integer program and Oracle error (Lemma 2), and the final deterministic bound. Each milestone keeps the paper's constants and its own hypotheses. Together they expose the interfaces needed to close Theorem 1.
Theorem 1 transfers a question about a real matrix optimum to a finite assignment benchmark. The Oracle benchmark can itself be bounded under additional assumptions, as Fei and Chen do in their separate Theorem 2. The present target preserves the comparison even in regimes where the benchmark does not vanish. It therefore expresses an error guarantee rather than an exact-recovery assertion.
A complete Lean proof would connect a probability model, finite-dimensional semidefinite feasibility, and the paper's integer assignment comparison. At present these mission statements are draft proof obligations: compiling a statement with sorry checks its formulation but does not prove the result. The development reuses published definitions of scalar and vector sub-Gaussian norms; proving the new lemmas and the main theorem remains open within this mission.
SDP optimality gives an inequality for the squared-distance objective, but it does not directly bound the entrywise difference from . Noise enters that objective through both a Gram matrix and mixed center-noise terms. A direct entrywise comparison also ignores the row-sum and positive-semidefinite structure that constrains the SDP error.
On the benchmark side, replacing a fractional matrix error by an arbitrary rounded assignment would not retain the stated factor. The paper identifies an intermediate linear program whose value can be controlled at integer cardinalities. Formalizing the result requires preserving that cardinality constraint, the exact coefficient , and the distinction between the observed points and the oracle's augmented points.
Points, clusters, and coordinates use finite index types; Lean indices start at zero while the paper's and start at one. All matrices are real. The trace inner product is represented by a double sum, the matrix norm is entrywise, and the spectral norm in Proposition 2 uses the operator norm. The minimum separation ranges over distinct center pairs, which is nonempty when . Oracle maxima are finite, nonempty, bounded sets; the true assignment is a feasible candidate. The normalized denominators are nonzero under and with balanced labels.
The random model uses one probability space and the same noise realization in both and . Measurability, zero mean, independence, and the extended-nonnegative vector sub-Gaussian norm bound are explicit. High-probability conclusions use measurable events and quantify over every optimum at each realized data set. Deterministic milestones take a fixed realization and do not add a probability space. The universal constants occur before all model parameters. These choices rule out a vacuous instance-dependent SNR constant, a norm that assigns zero to heavy-tailed noise, and an SDP optimum chosen before observing the noise.
The scope is Theorem 1 and its selected Section 5 statements. Theorem 2's separate Oracle-error rate, the rounding algorithm, semi-random Model 2, and the stochastic-ball special case are outside this proposal. Reusable work includes the SDP and assignment interfaces, matrix-error identities, and finite integer-program comparisons. Contributions that prove the eight source milestones or establish their supporting concentration and finite-dimensional optimization results are welcome.
Revealed-preference theory asks which observed choices can be explained by a decision procedure. The classical answer, maximization of a single preference, explains only choice functions that satisfy consistency conditions such as the weak axiom, and observed choices, including the menu effects in Luce and Raiffa's dinner example, often violate them. A large literature therefore studies richer procedures and characterizes the behaviour each one can generate.
The pro-con model of Dogan and Yildiz formalizes Benjamin Franklin's "prudential algebra": an agent lists reasons for and against each alternative and chooses the one whose reasons for outnumber its reasons against. Each reason is an ordering of the alternatives, and an ordering counts as a reason for (or against) an alternative at a menu when it ranks that alternative first among those available. The paper's main result is that this model is universal for deterministic choice: every choice function is pro-con rationalizable. The paper also proves the random-choice analogue (every random choice function is pro-con rational with signed weights in ), derives that every choice function is plurality-rationalizable, and recovers McGarvey's theorem on majority relations as a corollary.
Let be a finite set of alternatives. A choice set is a nonempty , and a choice function assigns to every choice set an element . An ordering is a strict linear order of ; is the -top-ranked alternative of .
A pro-con model consists of two sets of orderings, the pro-orderings and the con-orderings , with no ordering in both. For ,
is pro-con rational (Definition 1) if one pro-con model serves every choice set: for every and every , if and only if .
The proof works with signed weights on classes of orderings. For , a -prefix is the list of the first alternatives of an ordering, and is the family of sets with more than elements. A weight function on -prefixes represents a random choice function on if is the total weight of the prefixes along which is the first element of . The Möbius transform of is , extended by for .
The milestones follow the paper's proof, which runs the inductive construction of Section 6 and makes each step integral in Section 7:
Theorem 1 says that pro-con rationality imposes no testable restriction on deterministic choice: no data set of single-valued choices can refute it. A characterization of a choice procedure is therefore informative only once the model is restricted further (fewer orderings, structured orderings), and the representation of Theorem 1 serves as a starting point for building other universal models, such as the plurality representation of Section 2.4. The paper shows that universality is delicate: it fails for multi-valued choice rules when each ordering may be used only once (Section 2.3).
The result is proved in the paper; nothing in this mission is open mathematics. No part of it has a machine-checked proof. The formal work is to verify the proof. That covers its combinatorial core (Möbius inversion, the estimate, the generalized Ford–Fulkerson theorem), the integrality step, and the corrections the formalization needed: Lemma 4 requires an integral right-hand side; the paper's description of the con-orderings in the random case (inverses of negative-weight orderings, p. 16) is not what the deterministic assembly uses; and the induction of Section 7 uses a bound for the previous step that the paper establishes only for the real-valued construction.
The obvious approach, assigning pro- and con-orderings menu by menu, fails because every ordering affects every menu at once: changing one ordering changes the top element of all sets. The paper therefore builds a signed measure on orderings level by level, prefix length , and each level must solve a transportation problem with signed margins and box constraints . Classical Ford–Fulkerson theory covers nonnegative margins only. Moreover, a solution at one level has to leave the next level feasible, which is the role of the column bound in Theorem 3 and the source of the integrality gap noted above. The integrality itself rests on total unimodularity, which neither Mathlib nor the platform currently provides as a usable criterion (Heller–Tompkins) or vertex theorem (Hoffman–Kruskal).
The alternative set is a type X with [Fintype X] [DecidableEq X]; it may be empty, in which case every statement holds trivially. An ordering is a rank bijection X ≃ Fin (Fintype.card X), rank being the best, and means and for all . A pro-con model is a structure with two Finsets of rank bijections and a disjointness proof. A choice function is C : Finset X → X with C S ∈ S for nonempty S; its value at is irrelevant. ProConRational C includes this choice-function condition. Random choice functions are real-valued p : X → Finset X → ℝ, -prefixes are injections Fin k ↪ X, and weight functions are maps from prefixes to ℝ (to ℤ in the integral step). Representation on is stated with n < |S| + k to avoid natural-number subtraction. Matrices are Matrix (Fin m) (Fin n) ℝ or indexed by finite types; total unimodularity is Mathlib's Matrix.IsTotallyUnimodular, and vertices are Set.extremePoints ℝ.
The definition rules out each trivializing reading: orderings cannot be repeated (sets, not lists), cannot be both pro and con, are linear orders (unique top), count as cons at their top element, require a strict majority, and one model must serve all choice sets with the equivalence holding at every . A formalization that drops any of these makes Theorem 1 easier or false in a different way and is not this mission's goal.
Theorem 2 (random choice) is not a target; its proof steps appear as milestones. Reusable beyond this mission: the Möbius transform and its bound, the generalized Ford–Fulkerson theorem, Heller–Tompkins, and Hoffman–Kruskal for box-constrained systems. Proofs of any milestone, alternative proofs of Theorem 1 (for instance, a direct induction avoiding the gap in Section 7), and Lean infrastructure for total unimodularity are welcome.
Shortest remaining processing time first (SRPT) is the scheduling rule that always works on the jobs closest to completion. For a single server it minimizes the number of jobs in the system at every time, on every sample path (Schrage 1968). Service systems with many parallel servers and customers who leave when they wait too long, such as call centers, hospital wards and cloud platforms, are a different setting. There an overloaded system must turn customers away somehow, and the scheduling rule decides who. How SRPT behaves in such systems had resisted analysis: the state of the queue is a vector of remaining service and patience times of unbounded dimension, and preemptions couple all customers together.
Dong and Ibrahim (2021) analyze SRPT in the queue in the overloaded many-server regime. They show that SRPT asymptotically behaves like a two-class priority system with a sharp threshold on the service time. Short jobs are served with vanishing delay, long jobs almost all abandon, and the resulting waiting-time measures depend on the patience distribution only through its mean. Under first-come-first-served, by contrast, performance depends on the whole patience distribution (Whitt 2006).
Customers arrive according to a Poisson process of rate to identical servers. Customer brings a service time and a patience time . The are i.i.d. with a continuous law , density , cdf and mean ; the are i.i.d. with a continuous law and mean . Arrivals, services and patience times are mutually independent.
A schedule says which customers occupy the servers at each time. From it one reads off each customer's remaining processing time and cumulative time in queue . Customer abandons when reaches . Her patience clock keeps running across preemptions and is not reset. Under SRPT, at every time the servers are busy whenever customers are waiting, and every customer in service has remaining work no larger than that of any waiting customer. Customer is served () if she completes service and abandons () otherwise. Her waiting time is the total time she is present but not in service.
The traffic intensity is . The paper fixes and lets and grow together, with . The threshold is defined by equation (1),
so the work brought by jobs shorter than exactly matches capacity. Class 1 consists of the customers with and class 2 of those with .
The analysis couples the SRPT queue with a loss system . This system has the same customers and servers but no waiting room. Class 1 customers preempt class 2 customers, and a class 1 customer who finds all servers busy with class 1 work is lost. Its class 1 throughput is .
As , under SRPT and for a tagged customer in steady state:
The goal states all four parts. The constants , , and are those of the paper.
Proposition 1 (p. 8) is the coupling inequality , where is the throughput of the SRPT queue. The capacity constraint (5) (p. 16) says that work is completed at rate at most . Two steps in the proof of Lemma 4 (p. 17) concern Erlang's loss formula. The first is the identity . The second is the limit . Lemma 4 (p. 16) gives . Problem (7) (p. 18) is a linear program over service-probability profiles. Lemma 5 (p. 17) says the limiting service probability is ; the mission states the analytic step that concludes its proof (p. 18), not Lemma 5 itself. Theorem 2(a) is the goal's first part.
Theorem 2 is a state-space collapse: an infinite-dimensional preemptive system becomes, in the limit, a two-class priority rule with an explicit threshold. Several consequences follow from it. SRPT asymptotically minimizes the waiting time of served customers and maximizes that of abandoning ones (Corollary 1). It also asymptotically maximizes throughput among all disciplines (Proposition 3). Its performance measures are insensitive to the patience law beyond its mean.
The paper proves Theorem 2 on paper. To our knowledge none of it is machine-checked. The mission asks for a formal model of a multi-server preemptive queue with abandonment and a formal proof of the coupling. It also asks for the Erlang-formula asymptotics and the variational step that pins down . Two parts of the published argument need care in a formal proof. The proof of (b) switches to patience laws with , while the statement is for general patience laws. The proof of Lemma 5 presupposes that exists. A complete development must close both points or replace them with arguments that avoid them.
The SRPT queue has no finite-dimensional Markov description. Preemptions mean that the order in which customers are served is not their arrival order, and a preempted customer's patience keeps running. Standard fluid or diffusion limits for many-server queues track the number of customers, or a measure-valued state under first-come-first-served, and SRPT fits neither. The coupling with the loss system avoids this, but proving it requires a matching argument along the sample path that survives every preemption. Converting throughput bounds into statements about conditional waiting times then requires control of steady-state quantities that the model does not provide in closed form.
The model is a single definitions file in the namespace SRPTManyServer.Collapse, with these conventions.
IsLeast statement over measurable .The discipline in the goal is SRPT on the actual arrival stream. It is not the two-class priority system, the threshold does not appear in the scheduling predicate, and the throughputs and service probabilities are not free parameters: a statement in which they were would reduce the goal to Lemma 5. The non-idling clause is part of the SRPT predicate, so the empty schedule does not qualify.
A complete development needs a sample-path theory of preemptive multi-server queues with abandonment. It also needs renewal or regenerative arguments that connect time averages with customer averages, and the insensitivity of the blocking probability, which the paper cites from the literature and does not prove. These pieces are reusable beyond this mission. Contributions to any milestone are welcome. The Erlang identities, problem (7) and the final step of the proof of Lemma 5 are self-contained analysis.
Not formalized here: Corollary 1, Proposition 3 (Appendix B), inequality (4), and the numerical comparisons of §4.
Firms that advertise online choose whom to target from the customer data they hold, and the industry's working assumption is that more granular data can only help: a firm that knows more about each consumer can at worst ignore the extra information. Despotakis and Yu (SSRN 3900394; Management Science, 2022, doi:10.1287/mnsc.2022.4604) show that this fails once consumers draw inferences from being targeted. A consumer who receives an ad learns something about how well the product suits her, and she decides whether to spend effort clicking on that basis. When the firm uses more dimensions of data, the set of consumers it targets changes shape, and the signal that being targeted conveys becomes weaker. In equilibrium the firm can then earn strictly less with more data than with less.
The result belongs to a line of work on targeted advertising as a signal, and on the value of customer data to a firm whose actions consumers observe and interpret. It is a commitment problem: the firm would like to promise to use less information, but cannot.
A unit mass of consumers is interested in a product sold at an exogenous price . A consumer's utility from the product is
where are her matching values on two components of the product and is her private weight on the first. The three are independent and uniform on . The consumer does not know and until she clicks.
The firm sends ads at unit ad cost . Under single-dimensional (sd) targeting it observes and chooses a targeting set ; under multidimensional (md) targeting it observes and chooses .
A targeted consumer does not see but expects a set . Her posterior is uniform: under sd targeting is uniform on and uniform on ; under md targeting is uniform on . She clicks at click cost if and only if her posterior expected surplus is at least ; the weights that click form the click set . After clicking she learns and buys if and only if .
Against a click set , the ad value of a consumer is times the probability that she clicks and buys, minus ; under md targeting . The firm's profit from targeting is the integral of the ad value over .
A non-trivial equilibrium is a targeting set of positive measure that maximizes the firm's profit over all targeting sets, against the click set that consumers who correctly expect produce. An md equilibrium is symmetric if is symmetric about the 45-degree line. and denote equilibrium profits. Two thresholds from the paper enter the statements: the click-cost threshold of Equation (7), above which no non-trivial symmetric md equilibrium exists, and the ad-cost threshold from the proof of Proposition 1.
For every there is such that for every there is such that for every both a non-trivial sd equilibrium and a non-trivial symmetric md equilibrium exist, and
for every such pair. The goal fixes neither nor ; the right end of the click-cost interval is the explicit threshold of Equation (7).
The result is a clean counterexample to the monotonicity of the value of information for a firm whose actions are observed by strategic receivers. It isolates a mechanism, inference from being targeted, that does not need competition, price discrimination or privacy costs to make extra data harmful. The paper uses it to explain why firms might coarsen the data they act on, and §5 revisits the comparison with endogenous pricing and with consumers who do not know which dimension the firm targets on.
On the platform this mission is the first model of targeting with consumer inference. The model layer, uniform posteriors on an expected targeting set, click sets defined by posterior expected surplus, and equilibria defined as fixed points over arbitrary measurable targeting sets, is reusable for other signalling-through-targeting results. The result is proved on paper, with Lemmas 4 and 5 argued in sketch form; to our knowledge no part of it has a machine-checked proof.
Both equilibria are fixed points: the firm's best response depends on the click set, and the click set depends on the expected targeting set through a posterior average. The md firm may choose any measurable subset of the square, so the reduction to the two-line class of Equation (6) is part of the work, and Proposition 2 asks for uniqueness among all symmetric measurable equilibria, not only within .
The comparison itself is not a monotonicity argument. As approaches , the md click set shrinks to the threshold where the md equilibrium disappears, while the sd profit stays positive only because lies strictly below , where the sd profit vanishes. Making this precise requires the piecewise closed forms of the expected surplus (with logarithms) and control of both profits uniformly as , which the page leaves implicit. Comparing the closed forms at a single numerical point does not give the statement for every price.
All quantities are real numbers. Consumer populations are Lebesgue measure on and , so probabilities are lengths and areas. Targeting sets are measurable subsets of the unit interval or square, "non-trivial" means positive measure, "symmetric" means invariance under , and "unique" means unique up to a null set. The tie-breaks follow the page: buy at , click at equality, and indifference is allowed in the firm's optimization. Click thresholds are arbitrary reals, so an empty click set is expressible.
Equilibria are defined as fixed points, never by the paper's closed forms and ; otherwise Propositions 1 and 2 would be definitional and the goal a comparison of two formulas. The paper's is defined as the least click cost at which , which would make a literal statement nearly true by definition; the goal therefore asserts the existence of the region instead, and it includes existence of both equilibria so that the comparison is not vacuous.
Added or restricted hypotheses: Propositions 1 and 2 are stated only in the regimes Proposition 3 uses; Proposition 1 uses strictly (at equality the cutoff is and the targeting set is null); Lemma 4 adds ; Lemma 5 is stated in – form because its limit is not shown to exist; and the price is throughout.
A complete development needs set integrals and product measures from Mathlib, convexity of the expected surplus in , and real analysis of the piecewise closed forms. Proofs of any milestone, and alternative arguments for Lemmas 4 and 5, are welcome.
Interior-point methods solve a conic optimization problem by following the minimizers of a barrier function for the cone. Their iteration count is governed by the barrier's parameter : the best known algorithms need iterations to reach accuracy (Nesterov and Todd, 1997). A cone can be used natively by a solver only once a logarithmically homogeneous self-concordant barrier (LHSCB) with a small parameter is known for it, together with efficient oracles for its derivatives.
Coey, Kapelevich and Vielma (arXiv:2103.04104v2; Mathematics of Operations Research, 2022) study cones defined by spectral functions on Euclidean Jordan algebras. This framework covers vectors, real symmetric matrices and complex Hermitian matrices at once. The paper implements the resulting cones in the solver Hypatia. One of its two new barrier results concerns the root-determinant cone, the hypograph of the geometric mean of the eigenvalues. For symmetric matrices this is the hypograph of over the positive semidefinite cone, a standard modelling device for D-optimal experimental design and for determinant maximization. Before this paper, the usual way to represent it was an extended formulation with auxiliary variables and a semidefinite constraint.
A Jordan algebra is a real vector space with a bilinear product that is commutative and satisfies the Jordan identity , where . It has a multiplicative identity . It is Euclidean if . An idempotent is a with . It is primitive if it is non-zero and is not the sum of two orthogonal non-zero idempotents. A Jordan frame is a family of pairwise orthogonal primitive idempotents summing to . Every Jordan frame of has the same size , the rank of .
Every has a spectral decomposition over a Jordan frame, with real eigenvalues . From these, , , and a real function acts by . The inner product is the trace form . The cone of squares is ; means . The quadratic representation is , where .
The root-determinant is on . With and , the root-determinant cone and its candidate barrier are
A function is a -LHSCB for a cone if it is and convex on and tends to at the boundary. It must also satisfy and , and the parameter satisfies .
The goal holds for every finite-dimensional Euclidean Jordan algebra of rank , not for one matrix algebra.
which are (105), (107) and (108). 6. The scalar inequality (109c): for every . 7. The compatibility inequality (103) on :
The result gives the root-determinant cone a barrier whose parameter is one more than the optimal parameter of its domain , so it cannot be improved by more than one (p. 24). It also removes the extended formulation: a solver works with the cone in its natural dimension. The paper pairs the barrier with closed-form oracles for the gradient, Hessian product and inverse Hessian product (§7.4, Lemma 7.1), and reports computational gains in Hypatia. Because the statement is uniform over Euclidean Jordan algebras, it covers the vector, real symmetric and complex Hermitian cases at once.
The result is proved in the paper; this mission formalizes it. To the best of the curators' knowledge, it has no machine-checked proof, and Lean's Mathlib has no theory of Euclidean Jordan algebras, spectral decompositions in them, or barrier functions for their cones. Formalizing Proposition 7.1 therefore also yields a reusable layer: the Jordan-algebraic setting, the cone of squares, the quadratic representation, and an LHSCB predicate on arbitrary normed spaces.
The obvious route checks self-concordance of directly. That requires bounding the third derivative of by the -power of its Hessian in every direction. The two logarithmic terms interact, and no simple direct estimate is available. The paper instead uses a compatibility criterion of Nesterov and Nemirovskii, which reduces the barrier property to the single inequality (103) between derivatives of and . In Lean that criterion is not available and must be established for this cone; it is the deepest milestone.
The derivative identities (105), (107) and (108) require differential calculus of spectral functions on a Jordan algebra: derivatives of , of , and of , expressed through the eigenvalues of the scaled direction . Deriving them from the structure axioms needs, among other things, the fact that the eigenvalues of and are those of scaled and squared, uniqueness of the spectral decomposition, and positivity of the eigenvalues on . Only the final scalar inequality (109c) is elementary.
is a real finite-dimensional inner product space carrying a structure EJA V d. The structure bundles the Jordan product (bilinear, commutative, Jordan identity), the unit and the Euclidean property. It also bundles, for every , eigenvalues and a Jordan frame of primitive idempotents with , and the identity . The spectral theorem (Faraut–Korányi III.1.2) says such data exist for every Euclidean Jordan algebra of rank , so this is the paper's setting. Primitivity forces to be the rank: without it, a frame could be padded with zeros and would change.
The ambient space is . Directional derivatives are iterated Fréchet derivatives on the diagonal, and "boundary" is the topological frontier. The barrier limit is taken within the interior at every frontier point.
The following conventions are fixed:
Properness is a separate predicate from LHSCB, because is not pointed.
A trivializing formalization is ruled out by these choices. Specializing to or , dropping primitivity, allowing , dropping convexity, or imposing the barrier limit at only some boundary points would each prove a different, weaker or vacuous statement.
Proposition 6.1 (the -LHSCB for the matrix monotone derivative cones) and Lemma 7.1 (the inverse Hessian oracle) are deliberately absent. The first needs matrix monotonicity and Löwner's integral representation and is independent of Proposition 7.1. The second is an oracle formula that the goal does not use.
Contributions are welcome at every level: the scalar inequality (109c); the cone and homogeneity facts; the spectral calculus behind (105)–(108); and the compatibility reduction. The Jordan-algebraic infrastructure and the LHSCB predicate are reusable beyond this mission.