All missions

Motivation

By combining the Minkowski inequality and the quantum Chernoff bound, we derive easy-to-compute upper bounds for the error probability affecting the optimal discrimination of Gaussian states. In particular, these bounds are useful when the Gaussian states are unitarily inequivalent, i.e., they differ in their symplectic invariants.

This mission is the statement-level formalization of Computable bounds for the discrimination of Gaussian states (arXiv:0806.1625v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Minkowski spectral bound for Gaussian-state discrimination (Theorem 4, Eqs. (60)–(62), PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Computable bounds for the discrimination of Gaussian states, arXiv:0806.1625v2, https://arxiv.org/abs/0806.1625v2

Motivation

After proving a general no-cloning theorem for black boxes, we derive the optimal universal cloning of unitary transformations, from one to two copies. The optimal cloner is realized by quantum channels with memory, and greately outperforms the optimal measure-and-reprepare cloning strategy. Applications are outlined, including two-way quantum cryptographic protocols.

This mission is the statement-level formalization of Optimal cloning of unitary transformations (arXiv:0804.0129v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal universal one-to-two unitary cloning, with attaining channels (Theorem 1; Eqs. (8)–(10), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Paragraph following Theorem 1, controlled-swap realization: Consistent controlled-swap Stinespring realization of Eq. (8) in the stated +/- memory basis (source-ambiguity)

Selected references

• Optimal cloning of unitary transformations, arXiv:0804.0129v2, https://arxiv.org/abs/0804.0129v2

Motivation

In this paper we develop two types of tools to deal with differentiability properties of vectors in continuous representations $\pi \: G \to \GL(V)$ of an infinite dimensional Lie group $G$ on a locally convex space $V$. The first class of results concerns the space $V^\infty$ of smooth vectors. If $G$ is a Banach--Lie group, we define a topology on the space $V^\infty$ of smooth vectors for which the action of $G$ on this space is smooth. If $V$ is a Banach space, then $V^\infty$ is a Fr'echet space. This applies in particular to $C^*$-dynamical systems $(\cA,G, \alpha)$, where $G$ is a Banach--Lie group. For unitary representations we show that a vector $v$ is smooth if the corresponding positive definite function $\la \pi(g)v,v\ra$ is smooth. The second class of results concerns criteria for $C^k$-vectors in terms of operators of the derived representation for a Banach--Lie group $G$ acting on a Banach space $V$. In particular, we provide for each $k \in \N$ examples of continuous unitary representations for which the space of $C^{k+1}$-vectors is trivial and the space of $C^k$-vectors is dense.

This mission is the statement-level formalization of On Differentiable Vectors for Representations of Infinite Dimensional Lie Groups (arXiv:1002.1602v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Hilbert-valued smoothness and the inner-product kernel (Theorem 7.1, PDF p. 21). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

42 results of the paper are not stated yet, because the library lacks an interface they need:

• Lemma 3.3: Finite-order directional manifold calculus, tangent vectors, smooth exponential, and generator domains (hard)
• Lemma 3.4: Finite-order Ck orbit vectors and iterated partial-generator domains (hard)
• Lemma 4.2: The Definition 4.1 smooth-vector space, topology and derived action (hard)
• Lemma 4.3: Smooth-vector seminorms and the actual differential of conjugation (hard)
• Theorem 4.4: The smooth-vector topology and Bastiani-smooth action into it (hard)
• Corollary 4.5: The induced smooth-vector space and its Definition 4.1 topology (hard)
• Proposition 4.6: Smooth compact-open topology and the orbit-map embedding (hard)
• Lemma 4.10: Distribution-vector dual and smooth-function intertwiner spaces (hard)
• Proposition 5.4: Canonical smooth-vector locally convex uniform structure (hard)
• Theorem 6.2: Smooth C-star subalgebra with its derivative topology and unit group (hard)
• Theorem 7.2: Locally convex Lie-group smooth maps and local smooth matrix coefficients (hard)
• Corollary 7.3: Smooth orbit vectors and their density for a cyclic unitary representation (hard)
• Corollary 7.4: Locally convex Lie groups and local scalar smoothness for semidefinite functions (hard)
• Theorem 8.2: Smooth exponential and generator-domain derivative map (hard)
• Lemma 8.4: Frechet-Lie exponential curves and a derivative-defined common domain (hard)
• Theorem 8.5: C1 orbit vectors in Bastiani calculus and the common generator domain (hard)
• Lemma 9.2: The canonical first graph norm on the generator domain (hard)
• Lemma 9.3: Iterated generator domains and ordered derived multilinear maps (hard)
• Theorem 9.4: The exact higher graph norms and successive derived-action spaces (hard)
• Proposition 9.7: Graph-norm representations, operator-norm derivative maps and Frechet-Ck orbit vectors (hard)
• Lemma 10.2: The a.e. phase-multiplication representation on L2 (hard)
• Lemma 10.3: A.e. Lp phase generators and canonical inclusions in L2 (hard)
• Proposition 10.4: Iterated phase-generator domains and common Lp embeddings (hard)
• Theorem 11.3: The prescribed countable finite-dimensional direct-limit Lie structure (hard)
• Theorem 12.4: A pro-Lie realization with compatible smooth projection quotients (hard)
• Remark 3.2: Generator domains and the fundamental-theorem integral in an incomplete locally convex space (hard)
• Remark 4.7a: Smooth compact-open Frechet structure and smooth-vector topology (hard)
• Example 4.8: Product-sequence phase representation and universal locally convex topology quantification (hard)
• Example 4.9: Affine-function representation and compact/bounded convergence dual topologies (hard)
• Application 4.10-homogeneous: Smooth homogeneous quotient and distribution-vector parametrization (hard)
• Footnote 7.1-finite: An unambiguous finite-order regularity hypothesis near the diagonal (source-ambiguity)
• Remark 8.3: One-parameter generator domains for an isometric Banach representation (hard)
• Remark 9.5: Higher graph domains, derivatives and the sum norm on the product (hard)
• Remark 9.6: The projective derivative topology on the infinite common domain (hard)
• Remark 9.8: Finite-dimensional graph-domain action and the concrete p=2 counterexample (hard)
• Example 9.9: The Lp phase action on its first graph-norm domain (hard)
• Example 9.10: Periodic sup-norm representation and its generator domains (hard)
• Remark 10.5: The concrete p=2n phase representation and its Cn domains (hard)
• Remark 10.6: Exact phase graph norms and natural Lq norm comparison (hard)
• Remark 10.7: Frechet-C1 orbit regularity and continuity in the p=2 graph norm (hard)
• Remark 12.5: The smooth projective-limit realization of R^N and its phase action (hard)
• Remark 12.6: Seminorm-kernel quotients with their induced norms and factored representations (hard)

Selected references

• On Differentiable Vectors for Representations of Infinite Dimensional Lie Groups, arXiv:1002.1602v3, https://arxiv.org/abs/1002.1602v3

Motivation

We address the problem of the information-disturbance trade-off associated to the estimation of a quantum transformation, and show how the extraction of information about the a black box causes a perturbation of the corresponding input-output evolution. In the case of a black box performing a unitary transformation, randomly distributed according to the invariant measure, we give a complete solution of the problem, deriving the optimal trade-off curve and presenting an explicit construction of the optimal quantum network.

This mission is the statement-level formalization of Information - Disturbance Tradeoff in the Estimation of a Unitary Transformation (arXiv:1006.5665v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Attained optimal information–disturbance frontier (§IV C, Eqs.(30)–(34); abstract on PDF p.1, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Information - Disturbance Tradeoff in the Estimation of a Unitary Transformation, arXiv:1006.5665v2, https://arxiv.org/abs/1006.5665v2

Motivation

We analyze quantum algorithms for cloning of a quantum measurement. Our aim is to mimic two uses of a device performing an unknown von Neumann measurement with a single use of the device. When the unknown device has to be used before the bipartite state to be measured is available we talk about 1 -> 2 learning of the measurement, otherwise the task is called 1 -> 2 cloning of a measurement. We perform the optimization for both learning and cloning for arbitrary dimension of the Hilbert space. For 1 -> 2 cloning we also propose a simple quantum network that realizes the optimal strategy.

This mission is the statement-level formalization of Cloning of a quantum measurement (arXiv:1103.5709v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal one-to-two measurement cloning fidelity (§V, Eq.(61): optimal one-to-two cloning fidelity (seed announced in abstract), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

3 results of the paper are not stated yet, because the library lacks an interface they need:

• §IV, Eq.(48): explicit numerical block score coefficients: Numerical Schur score coefficients in Eq.(48) (source-ambiguity)
• §V, Eqs.(62),(63), p.8 replica formula: printed optimal cloners: Operational optimality of the two printed Eq.(62) block arrays (source-ambiguity)
• §VI final paragraph and author note [17]: estimate-and-prepare comparison: An operationally specified optimal-estimation-and-prepare strategy (source-ambiguity)

Selected references

• Cloning of a quantum measurement, arXiv:1103.5709v2, https://arxiv.org/abs/1103.5709v2

Motivation

A definition of the Schmidt number of a state of an infinite dimensional bipartite quantum system is given and properties of the corresponding family of Schmidt classes are considered. The existence of states with a given Schmidt number such that any their countable convex decomposition does not contain pure states with finite Schmidt rank is established. Partially entanglement breaking channels in infinite dimensions are studied. Several properties of these channels well known in finite dimensions are generalized to the infinite dimensional case. At the same time, the existence of partially entanglement breaking channels (in particular, entanglement breaking channels) such that all operators in any their Kraus representations have infinite rank is proved.

This mission is the statement-level formalization of The Schmidt number and partially entanglement breaking channels in infinite dimensions (arXiv:1110.4363v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 9B: exact k-PEB channels with only infinite-rank nonzero Kraus operators (Proposition 9B: exact k-PEB channels with only infinite-rank nonzero Kraus operators, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Proposition 2: Source-pinned infinite-dimensional LOCC class, specifying deterministic versus selected outputs, measurable outcome instruments, round limits and topology. (source-ambiguity)

Selected references

• The Schmidt number and partially entanglement breaking channels in infinite dimensions, arXiv:1110.4363v3, https://arxiv.org/abs/1110.4363v3

Motivation

We study quantum learning algorithms for quantum measurements. The optimal learning algorithm is derived for arbitrary von Neumann measurements in the case of training with one or two examples. The analysis of the case of three examples reveals that, differently from the learning of unitary gates, the optimal algorithm for learning of quantum measurements cannot be parallelized, and requires quantum memories for the storage of information.

This mission is the statement-level formalization of Quantum learning algorithms for quantum measurements (arXiv:1103.0480v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Three-example qubit learning requires adaptation (Abstract; §V.C and Remark 1: optimal three-example qubit learning requires adaptation, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

7 results of the paper are not stated yet, because the library lacks an interface they need:

• Lemma 5 / Eq.(48), printed unrestricted random-mixture range: Lemma 5 / Eq.(48), printed unrestricted random-mixture range (source-ambiguity)
• §V.A: strict inferiority of estimating then preparing the estimated measurement: An unrestricted one-use estimate-and-replay-projective-measurement domain with its measurable joint outcome law and actual replica contraction. (hard)
• Eqs.(82),(A14): printed final two-use scalar formula: Eqs.(82),(A14): printed final two-use scalar formula (source-ambiguity)
• §V.C: approximate optimal three-use qubit score: §V.C: approximate optimal three-use qubit score (source-ambiguity)
• §VI: general statement that examples after the second must be sequential: §VI: general statement that examples after the second must be sequential (source-ambiguity)
• Abstract / §I: requirement of coherent quantum memory: Abstract / §I: requirement of coherent quantum memory (source-ambiguity)
• §VI: optimal learners for different N do not share initial steps: §VI: optimal learners for different N do not share initial steps (source-ambiguity)

Selected references

• Quantum learning algorithms for quantum measurements, arXiv:1103.0480v2, https://arxiv.org/abs/1103.0480v2

Motivation

A consistent functional calculus approach to the spectral theorem for strongly commuting normal operators on Hilbert spaces is presented. In contrast to the common approaches using projection-valued measures or multiplication operators, here the functional calculus is not treated as a subordinate but as the central concept. Based on five simple axioms for a "measurable functional calculus", the theory of such calculi is developed in detail, including spectral theory, uniqueness results and construction principles. Finally, the functional calculus form of the spectral theorem is stated and proved, with some proof variants being discussed.

This mission is the statement-level formalization of The Functional Calculus Approach to the Spectral Theorem (arXiv:2003.06130v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

49 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 7.6 (Spectral Theorem: General Case) (Theorem 7.6 (Spectral Theorem: General Case), PDF p. 35). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

• Example 6.2: Concrete subsequence-tail characters on l-infinity, their bounded diagonal representation on l2 of all increasing subsequences, and the common-kernel anchor-set predicate. (hard)
• Remark 6.8: arbitrary Borel product analogue: Exact hypotheses and regularity predicate for an arbitrary product of Borel calculi. (source-ambiguity)

Selected references

• The Functional Calculus Approach to the Spectral Theorem, arXiv:2003.06130v2, https://arxiv.org/abs/2003.06130v2

Motivation

We consider three different communication tasks for quantum broadcast channels, and we determine the capacity region of a Hadamard broadcast channel for these various tasks. We define a Hadamard broadcast channel to be such that the channel from the sender to one of the receivers is entanglement-breaking and the channel from the sender to the other receiver is complementary to this one. As such, this channel is a quantum generalization of a degraded broadcast channel, which is well known in classical information theory. The first communication task we consider is classical communication to both receivers, the second is quantum communication to the stronger receiver and classical communication to other, and the third is entanglement-assisted classical communication to the stronger receiver and unassisted classical communication to the other. The structure of a Hadamard broadcast channel plays a critical role in our analysis: the channel to the weaker receiver can be simulated by performing a measurement channel on the stronger receiver's system, followed by a preparation channel. As such, we can incorporate the classical output of the measurement channel as an auxiliary variable and solve all three of the above capacities for Hadamard broadcast channels, in this way avoiding known difficulties associated with quantum auxiliary variables.

This mission is the statement-level formalization of Hadamard quantum broadcast channels (arXiv:1611.07651v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2: exact classical capacity of a Hadamard broadcast channel (Theorem 2, §3.3: classical capacity of a Hadamard broadcast channel (seed paper result), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• Hadamard quantum broadcast channels, arXiv:1611.07651v3, https://arxiv.org/abs/1611.07651v3

Motivation

We prove the existence of a universal recovery channel that approximately recovers states on a v. Neumann subalgebra when the change in relative entropy, with respect to a fixed reference state, is small. Our result is a generalization of previous results that applied to type-I v. Neumann algebras by Junge at al. [arXiv:1509.07127]. We broadly follow their proof strategy but consider here arbitrary v. Neumann algebras, where qualitatively new issues arise. Our results hinge on the construction of certain analytic vectors and computations/estimations of their Araki-Masuda $L_p$ norms. We comment on applications to the quantum null energy condition.

This mission is the statement-level formalization of Approximate recovery and relative entropy I. general von Neumann subalgebras (arXiv:2006.08002v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A support-dominating state in a closed convex family (Lemma 2: support-dominating state in a closed convex set, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

31 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 1 (Faithful case): strengthened monotonicity: Supported relative modular operators, faithful rotated Petz map and Araki entropy (hard)
• Lemma 1: reduction to support corners, parts (i)–(iv): Projected inclusion (29) outside the domain of Phi_A inverse (source-ambiguity)
• Corollary 1: nonfaithful reference version of Theorem 1: Nonfaithful map (37) depending on projected inclusion (29) (source-ambiguity)
• Theorem 2: universal approximate recovery (original paper seed): Full Theorem 2 explicit nonfaithful map (37),(41) (source-ambiguity)
• Lemma 3: fidelity, Araki–Masuda L1, and Fuchs–van de Graaf bounds: Araki–Masuda p=1 variational quantity from Eq.(53) (hard)
• Theorem 3: first law for Renyi relative entropy: Supported modular expectations and Araki–Masuda quantities for varying parameters (hard)
• Lemma 4: uniform modular estimate and norm comparison: Unbounded modular expectation and AM norm comparison (hard)
• Theorem 4: interpolating vector holomorphy and boundary domination: Canonical general-vector embedding and interpolating vector Gamma (hard)
• Remark 4: arbitrary-vector variant and cyclic equality: Polar representative partial isometry and arbitrary-vector Gamma (hard)
• Lemma 5: properties of smoothly filtered vectors: Filtered vector from the spectral multiplier of log Delta (hard)
• Theorem 5: filtered entropy, including printed Gaussian iff: Printed Gaussian necessity in the iff of part (3) (source-ambiguity)
• Theorem 5(1)–(2): finite entropy and two limiting bounds: Homogeneous Araki entropy of unnormalized filtered vectors (hard)
• Theorem 5(3), valid Gaussian sufficient direction: Homogeneous filtered entropy and centered Gaussian spectral multiplier (hard)
• Lemma 6: extended analyticity, norm bound and entropy derivative: Regulated Gamma and logarithmic spectral cutoff Pi_Lambda (hard)
• Lemma 7: top-edge L1 and regulator removal: Regulated top-edge AM quantity and recovered states (hard)
• Lemma 8: joint p→2, z→0 derivative: Joint endpoint norm and entropy derivative of regulated Gamma (hard)
• Lemma 9: Hirschman interpolation for Araki–Masuda norms: Araki–Masuda interpolation on a nonfaithful reference (hard)
• Theorem 2 faithful case / Eq.(149): explicit averaged channel: Weak predual average of the actual rotated Petz maps (hard)
• Section 4.1: finite type-I density identifications and Gamma formula: Identification of the actual Gamma and AM norm with matrix expressions (hard)
• Section 4.2, Eq.(167): recovery channel for half-sided inclusions: Half-sided modular data and normalized translation group (hard)
• Corollary 2: strengthened monotonicity for a half-sided inclusion: Half-sided entropy drop and translated-state fidelity integral (hard)
• Conjecture 1: infinitesimal saturation and prospective QNEC: Unproved infinitesimal limit identity (170) (source-ambiguity)
• Lemma 12: cited Hirschman improvement: Exact cited Hirschman growth and boundary hypotheses (source-ambiguity)
• Lemma 13: continuity of norms under faithful mixing: AM norm with the natural-cone representative of a faithful mixture (hard)
• Lemma 14: cited analytic-product criterion: Exact cited analytic-product domains and boundary regularity (source-ambiguity)
• Lemma 15: alternative interpolating vector analyticity: Alternative vector Xi from actual supported modular products (hard)
• Lemma 16: alternative-vector top-boundary identity: Self-adjoint implementer for an arbitrary majorizing vector (source-ambiguity)
• Appendix E Eq.(247): proposed averaged-recovery endpoint bound: Source-backed implementer and existence of the endpoint limit (source-ambiguity)
• Appendix E Eq.(248): expressly unproved entropy-derivative identity: Unproved infimum/endpoint derivative identity (source-ambiguity)
• Appendix E footnote 7 Eq.(249): proposed sufficient derivative formula: Unproved derivative and spectral-log domains (source-ambiguity)
• Section 2.3 Eq.(42): closed convex sets admitting universal recovery: Nonfaithful universal recovery construction for the selected support-dominating state (source-ambiguity)

Selected references

• Approximate recovery and relative entropy I. general von Neumann subalgebras, arXiv:2006.08002v1, https://arxiv.org/abs/2006.08002v1

Motivation

We present an efficient machine learning (ML) algorithm for predicting any unknown quantum process $\mathcal{E}$ over $n$ qubits. For a wide range of distributions $\mathcal{D}$ on arbitrary $n$-qubit states, we show that this ML algorithm can learn to predict any local property of the output from the unknown process~$\mathcal{E}$, with a small average error over input states drawn from $\mathcal{D}$. The ML algorithm is computationally efficient even when the unknown process is a quantum circuit with exponentially many gates. Our algorithm combines efficient procedures for learning properties of an unknown state and for learning a low-degree approximation to an unknown observable. The analysis hinges on proving new norm inequalities, including a quantum analogue of the classical Bohnenblust-Hille inequality, which we derive by giving an improved algorithm for optimizing local Hamiltonians. Numerical experiments on predicting quantum dynamics with evolution time up to $10^6$ and system size up to $50$ qubits corroborate our proof. Overall, our results highlight the potential for ML models to predict the output of complex quantum dynamics much faster than the time needed to run the process itself.

This mission is the statement-level formalization of Learning to predict arbitrary quantum processes (arXiv:2210.14894v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

37 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Corollary 3 (Norm inequality for general 𝑘-local Hamiltonian) (Corollary 3 (Norm inequality for general 𝑘-local Hamiltonian), PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

17 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 1 (Learning an unknown quantum process): The advertised sample bound for the actual first-regime learner, uniformly under the pinned quantifiers (source-ambiguity)
• Corollary 1 (Optimizing general 𝑘-local Hamiltonian): A fixed randomized output law with the claimed mean-energy and cost guarantee (source-ambiguity)
• Corollary ∑︀ 2 (Optimizing bounded-degree 𝑘-local Hamiltonian): A fixed randomized output law with the claimed mean-energy and cost guarantee (source-ambiguity)
• Theorem 4 (Learning an unknown observable): The advertised sample bound for the actual first-regime learner, uniformly under the pinned quantifiers (source-ambiguity)
• Fact 3: A specified uniform geometric Hamiltonian class (source-ambiguity)
• Theorem 5 ∑︀ (Random product states for optimizing 𝑘-local Hamiltonian): A fixed randomized output law with the claimed mean-energy and cost guarantee (source-ambiguity)
• Theorem 6 (Random product states for optimizing 𝑘-local Hamiltonian; alternative): A fixed randomized output law with the claimed mean-energy and cost guarantee (source-ambiguity)
• Theorem 7 (Approximation ∑︀ guarantee from [43] for optimizing 𝑘-local Hamiltonian): A specified randomized output law with the printed absolute-of-mean guarantee (source-ambiguity)
• Corollary 5 (Optimizing arbitrary 𝑘-local Hamiltonian): A fixed randomized output law with the claimed mean-energy and cost guarantee (source-ambiguity)
• Corollary 6 (Optimizing bounded-degree 𝑘-local Hamiltonian): A fixed randomized output law with the claimed mean-energy and cost guarantee (source-ambiguity)
• Theorem 8 (Approximation guarantee from [44]): A source-pinned graph/term degree model and scalar-case convention for the A17-A18 coefficient restatement (source-ambiguity)
• Lemma 4 (Khintchine inequality for polarized observables): Correct cross-dimension Frobenius normalization in the literal lemma (source-ambiguity)
• Lemma 12: Consistent scaling and positivity hypotheses for the hard-state ensemble (source-ambiguity)
• Theorem 13 (Learning to ∑︀ predict an unknown observable): The advertised sample bound for the actual first-regime learner, uniformly under the pinned quantifiers (source-ambiguity)
• Theorem 14 (Learning to predict a quantum evolution): The advertised sample bound for the actual first-regime learner, uniformly under the pinned quantifiers (source-ambiguity)
• Section II.B–C / Appendix E.2: product training transfers to every locally flat input law: The advertised sample bound for the actual first-regime learner, uniformly under the pinned quantifiers (source-ambiguity)
• Appendix A.4, Eq.(A34): polarization Frobenius normalization: A valid ordinary-trace polarization identity (source-ambiguity)

Selected references

• Learning to predict arbitrary quantum processes, arXiv:2210.14894v3, https://arxiv.org/abs/2210.14894v3

Motivation

Let $\mathfrak{g}$ be a real finite-dimensional Lie algebra containing pointed generating invariant closed convex cones. We determine those derivations $D$ of $\mathfrak{g}$ which induce a 3-grading of the form $\mathfrak{g} = \mathfrak{g}_{-1} \oplus \mathfrak{g}_0 \oplus \mathfrak{g}_1$ on $\mathfrak{g}$ such that the $(\pm 1)$-eigenspaces $\mathfrak{g}_{\pm 1}$ of $D$ are generated by the intersections with generating cones of the form $W = \mathcal{O}_f^*$, where $\mathcal{O}_f$ is the coadjoint orbit of a linear functional $f \in \mathfrak{z}(\mathfrak{g})^*$ and $\mathcal{O}_f^*$ is the dual cone of $\mathcal{O}_f$. In particular, we show that, if $\mathfrak{g}$ is solvable, no such derivation except the trivial one exists. This continues our classification of Lie algebras generated by Lie wedges of endomorphism semigroups of standard subspaces. The classification is motivated by the relation of nets of standard subspaces to Haag-Kastler nets of von Neumann algebras in Algebraic Quantum Field Theory.

This mission is the statement-level formalization of Lie wedges of endomorphism semigroups of standard subspaces in admissible Lie algebras (arXiv:2007.13445v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

25 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 3.17 (Non-degeneration Theorem); precise result selected for the seed (Theorem 3.17 (Non-degeneration Theorem); precise result selected for the seed, PDF p. 23). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

23 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 2.8 (Spindler’s Construction), complete printed statement: A uniquely specified valid full source statement on its printed domain. (source-ambiguity)
• Theorem 2.11: admissibility criterion: Complexified ordinary roots, adapted positive systems, and the real central minimal root cone with its dual interior. (hard)
• Theorem 2.14: convex symplectic module structure: Symplectic isotypic decomposition with actual multiplicities, form-level equivalences, and compact/hermitian ideal actions. (hard)
• Theorem 2.22, complete printed statement: A uniquely specified valid full source statement on its printed domain. (source-ambiguity)
• Theorem 2.22(a),(c): generalized Jacobi admissibility: Generalized sp as an actual Lie subalgebra and its generalized Jacobi Lie algebra for all dimensions. (hard)
• Lemma 3.4: A uniquely specified valid full source statement on its printed domain. (source-ambiguity)
• Proposition 3.10: Actual Jacobi and conformal Jacobi Lie algebras with inner-derivation restriction. (hard)
• Corollary 3.11: Concrete Jacobi grading derivations, antisymplectic involutions, and their exact bidirectional coordinate classification. (hard)
• Theorem 3.14 (Classification Theorem): Transported derivations in structural coordinates, real spectral isotypic data, and all continuation clauses (a)–(c). (hard)
• Corollary 3.15: A uniquely specified valid full source statement on its printed domain. (source-ambiguity)
• Lemma A.2: Algebraic subgroups of GL(V), tangent Lie algebras over arbitrary characteristic-zero fields, and their algebraic hull. (hard)
• Lemma A.3: Algebraic hull of ad(g), actual derivation-subalgebra embedding, and algebraicity of the hull plus RD. (hard)
• Example 2.4: symplectic grading elements: Concrete sp(2n,R) matrix action with its standard Cartan involution, diagonal maximal abelian space, and antisymplectic grading operators. (hard)
• Example 2.17: sl(2,R) convex modules: Standard sl2 module copies with a common global symplectic sign and compatible H/U block representation. (hard)
• Example 2.20: normalized Jacobi/Poisson model and cone: Concrete all-dimension Jacobi Lie algebra and its normalized degree-at-most-two polynomial Poisson isomorphism. (hard)
• Remark 3.2: transport under a change of complement: Inner conjugation and canonical quotient-defined transport between two prescribed complements, intertwining Phi and transporting cones. (hard)
• Remark 3.12: Jacobi eigenspace cones generate: Jacobi positive cone and the exact eigenspaces of its Levi-preserving nonzero derivation. (hard)
• Example 3.19: two-copy grading with mixed central signs: A uniquely specified valid full source statement on its printed domain. (source-ambiguity)
• Example 3.20: canonical exterior-square central extension: Actual exterior-square Lie module, fixed/effective splitting, canonical projection, and invariant central extension. (hard)
• Example 3.20(a): claimed universal grading construction: A uniquely specified valid full source statement on its printed domain. (source-ambiguity)
• Example 3.20(b): centralizer description: Canonical exterior-square beta and the symmetric-module-automorphism centralizer. (hard)
• Example 3.20(b): intermediate convexity assertion: A uniquely specified valid full source statement on its printed domain. (source-ambiguity)
• Remark 2.10, continued on PDF p.8: A valid source-scoped fixed/effective symplectic splitting from weak convex type. (source-ambiguity)

Selected references

• Lie wedges of endomorphism semigroups of standard subspaces in admissible Lie algebras, arXiv:2007.13445v1, https://arxiv.org/abs/2007.13445v1

Motivation

The quantum Schur transform maps the computational basis of a system of $n$ qudits onto a \textit{Schur basis}, which spans the minimal invariant subspaces of the representations of the unitary and the symmetric groups acting on the state space of $n$ $d$-level systems. We introduce a new algorithm for the task of weak Schur sampling. Our algorithm efficiently determines both the Young label which indexes the irreducible representations and the multiplicity label of the symmetric group. There are two major advantages of our algorithm for weak Schur sampling when compared to existing approaches which proceed via quantum Schur transform algorithm or Generalized Phase Estimation algorithm. First, our algorihtm is suitable for streaming applications and second it is exponentially more efficient in its memory usage. We show that an instance of our weak Schur sampling algorithm on $n$ qubits to accuracy $\epsilon$ requires only $O(\log_2n)$ qubits of memory and $O(n^3\log_2(\frac{n}{\epsilon}))$ gates from the Clifford+T set. Further, we show that our weak Schur sampling algorithm on $n$ qudits decomposes into $O\big(dn^{2d}\log_2^p\big(\frac{n^{2d}}{\epsilon}\big)\big)$ gates from an arbitrary fault-tolerant qudit universal set, for $p\approx 4$, and requires a memory of $O(\log_dn)$ qudits to implement.

This mission is the statement-level formalization of Weak Schur sampling with logarithmic quantum memory (arXiv:2309.11947v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Streaming weak Schur sampling with logarithmic quantum memory at fixed local dimension (Abstract; III and III.A, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

3 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 2; Algorithm 2; Eqs.(46)-(47): An explicit history-dependent padded Algorithm-2 unitary compiler, with fixed spin/GT coordinate encodings, rearranging permutations, Clifford+T list semantics, and accumulated nuclear-trace-norm local error. (hard)
• III.B, Eqs.(48)-(51): A corrected quantitative general-d irrep-dimension and qudit gate/memory analysis replacing III.B Eqs.(48)-(51). (source-ambiguity)
• IV, claimed classical simulation corollary: A specified classical input-access, output, accuracy and bit-cost model for simulating arbitrary correlated quantum streams. (source-ambiguity)

Selected references

• Weak Schur sampling with logarithmic quantum memory, arXiv:2309.11947v1, https://arxiv.org/abs/2309.11947v1

Motivation

Banks and other financial institutions are notoriously hard to see into: their loan books are complex and their public reports are coarse. A long-standing policy question is whether competition among financial institutions makes them more or less transparent. One view holds that competition for funding disciplines institutions into disclosing more; another that competitive pressure rewards opacity. G. Zhang, Competition and Opacity in the Financial System (SSRN 3428683; Management Science 2020, doi:10.1287/mnsc.2019.3512), gives an answer inside a coordination model in the tradition of Morris and Shin (2002) and Angeletos and Pavan (2004): competition lowers disclosure precision exactly when investors' own private information is precise.

The model belongs to the literature on public information in beauty-contest economies, where public reports serve both as information about fundamentals and as a focal point for coordination. The paper adds a second force, competition between two institutions for the same investors, and asks how the institutions' chosen precision of public disclosure responds.

Setting

Two financial institutions (FIs) $i \in \{1, 2\}$ raise funds from a continuum of risk-neutral investors $j \in [0,1]$. FI $i$'s project has fundamentals $\theta_i \sim N(\bar\theta, 1/q)$, independent across $i$, with prior mean $\bar\theta > 0$ and prior precision $q > 0$. Its return is

$$R_i = 2(\theta_i + aK_i),$$

where $K_i$ is the aggregate investment in FI $i$ and $a \in [0, \tfrac12]$ is the FI's rollover-risk exposure: the more others invest, the higher the return.

Before learning $\theta_i$, FI $i$ commits to a disclosure precision $m_i \ge 0$ and pays $\tfrac{c_m}{2}m_i^2$. It then publishes $z_i = \theta_i + \varepsilon_i$ with $\varepsilon_i \sim N(0, 1/m_i)$. Each investor $j$ also observes private signals $x_{ij} = \theta_i + \eta_{ij}$ of precision $n > 0$, and invests

$$k_{ij} = E_j[R_i/2] - b\,E_j[R_{-i}/2]$$

in FI $i$, where $b \in [0, 1]$ is the intensity of competition ($b = 0$: none; $b = 1$: the intense case analysed in the paper's main result). Here $E_j$ is investor $j$'s posterior expectation; for Gaussian signals $E_j[\theta_i] = (m_i z_i + n x_{ij} + q\bar\theta)/(m_i + n + q)$. A linear equilibrium of the investors' game is a strategy $k_{ij} = \beta_i x_{ij} + \gamma_i z_i - b(\lambda_i x_{-ij} + \omega_i z_{-i}) + h_i$ that satisfies this rule when every investor uses it.

FI $i$'s payoff is $\Pi_i = E[\tfrac{R_i}{2}K_i - \tfrac12 K_i^2] - \tfrac{c_m}{2}m_i^2$. A disclosure equilibrium is a pair $(m_1, m_2)$ of precisions, each a best response to the other given the investors' linear equilibrium. Write $m^{NC}$ for the equilibrium precision without competition ($b = 0$) and $m^*$ for the one with competition.

Formalization targets

Goal: Proposition 4

For $c_m$ sufficiently large:

1. if $a = 0$, then for every $b \in (0,1]$ the disclosure equilibrium is unique and $m^* = m^{NC}$;
2. if $a \in (0, \tfrac12)$, then at $b = 1$ there is a unique threshold $\hat n > 0$ with

$$m^* \le m^{NC}\ (\text{strictly if } m^{NC} > 0) \iff n > \hat n.$$

The goal fixes no constants: $\hat n$ is only asserted to exist.

Milestones

• Investor equilibrium. Lemma 1 (the unique linear equilibrium at $b = 0$, in closed form) and Proposition 3 (the unique linear equilibrium at $b > 0$, whose responses to every signal exceed the no-competition ones by multipliers greater than $1$).
• Marginal payoffs. (33) and (44): the derivative of FI $i$'s payoff in $m_i$ at $b = 0$ and at $b = 1$, in closed form.
• Disclosure without and with competition. Proposition 2 ($m^{NC} > 0$ iff $a > \tfrac58 - \tfrac18\sqrt{16q/n + 9}$), the monotonicity of $m^{NC}$ in $n$, and (46)–(47) ($m^* > 0$ iff $n < q/(1-2a)$).
• The comparison. (50)–(53): the difference of the two marginal payoffs is a positive multiple of a quartic $L(n/(q+m))$; and $L$ has a unique positive root $\Delta$, with $L(x) < 0$ iff $x > \Delta$.

Significance

Proposition 4 is the paper's main result. It separates two channels through which competition acts on disclosure: competition amplifies investors' reaction to every signal, which both reduces the coordination problem that disclosure is meant to solve and raises the value of a precise report for allocating funds between the institutions. Which effect dominates depends on the precision of private information, and the result pins this down to a single threshold. Without rollover risk the two channels vanish and competition is neutral. The paper's policy discussion of opacity in the financial sector (§3.3–§4) and its welfare analysis rest on this comparison.

The result is proved in the paper by hand computation; it has no machine-checked proof. Formalizing it requires the Gaussian payoff computation, a linear fixed-point argument for the investors' game, an optimization argument for the institutions' disclosure choice under a large-cost assumption, and a sign analysis of an explicit quartic.

Difficulty

The payoff $\Pi_i$ is an expectation of a quadratic in four independent Gaussians whose coefficients are themselves the solution of the investors' fixed point. Differentiating it in $m_i$ means differentiating through the equilibrium coefficients, and at $b = 1$ the coefficients of FI $i$ depend on both precisions; the closed form (44) holds only after cross terms cancel.

The comparison is global in $n$. Reading off the sign of the marginal payoff at $m^{NC}$ gives a condition on $n/(q + m^{NC})$, not on $n$, and $m^{NC}$ itself moves with $n$. A threshold on $n$ exists only because $n/(q + m^{NC}(n))$ is monotone and the quartic changes sign once. The "sufficiently large $c_m$" must be uniform in $n$: a bound that depends on $n$ does not give a single threshold.

Formalization scope

• Representation. FIs are Fin 2 (FI 1 of the paper is 0), the other FI is i.rev. The law of $(\theta_1, \theta_2, \varepsilon_1, \varepsilon_2)$ is a product of Mathlib gaussianReal measures; precision $q$ is variance $q^{-1}$. At $m_i = 0$ the noise is a point mass, and the equilibrium puts no weight on $z_i$.
• Expectations. Investor $j$'s expectation is the posterior-mean formula (27)–(28). The paper prints $x_{ij}$ where $x_{-ij}$ is meant in the terms about FI $-i$ of (25), (27), (28); the formalization uses $x_{-ij}$.
• Equilibria. Investors' equilibria are linear (uniqueness among all strategies, the paper's footnote 10, is not formalized). The payoff is evaluated at a linear equilibrium chosen by Classical.epsilon; Lemma 1 and Proposition 3 show it is determined in every coefficient the payoff uses. A disclosure equilibrium is a Nash equilibrium in $m_i \ge 0$.
• Added hypotheses. $a < \tfrac12$ wherever $b = 1$ (at $a = \tfrac12$, $b = 1$ positive disclosure precisions have no linear investor equilibrium); in Proposition 3 also $a > 0$, $m_1, m_2 > 0$ and $b \le 1$. "$c_m$ sufficiently large" is $\exists c_0\ \forall c_m \ge c_0$; in Proposition 4 part 1 the bound is chosen for each $b,n$, while in part 2 it is chosen before $n$.
• Ruled out. The equilibrium coefficients, $m^{NC}$ and $m^*$ are never defined by their closed forms; the payoff is the expectation (9) under the model's law, not a function whose derivative is (44); and in Proposition 4 part 2 (and in the milestones Proposition 2, (46)–(47) and the monotonicity of $m^{NC}$) $c_0$ is chosen before $n$ and before $\hat n$.
• Infrastructure. Second moments of Gaussian products, differentiation of parametric expectations, Descartes' rule of signs (in Mathlib) and the intermediate value theorem. A reusable lemma computing $E[(\alpha^\top \xi + c)^2]$ for independent Gaussians $\xi$ would serve other information-design missions. Contributions of any milestone are welcome; the polynomial milestones (50)–(53) and the root of $L$ are self-contained.

Selected references

• G. Zhang, Competition and Opacity in the Financial System, Management Science 66 (2020); SSRN 3428683, 2019. https://ssrn.com/abstract=3428683, https://doi.org/10.1287/mnsc.2019.3512
• S. Morris and H. S. Shin, Social Value of Public Information, American Economic Review 92(5), 2002, 1521–1534. https://doi.org/10.1257/000282802762024610
• G.-M. Angeletos and A. Pavan, Transparency of Information and Coordination in Economies with Investment Complementarities, American Economic Review 94(2), 2004, 91–98. https://doi.org/10.1257/0002828041301641
• I. Goldstein, E. Ozdenoren and K. Yuan, Trading Frenzies and Their Impact on Real Investment, Journal of Financial Economics 109(2), 2013, 566–582. https://doi.org/10.1016/j.jfineco.2013.03.011

Why continuous time matters

Intertemporal choice compares outcomes received at different times. A familiar model assigns each instantaneous outcome a utility and aggregates those utilities with a time weight. That model is useful in economics and operations research, but its meaning depends on what choices are feasible and how a preference over one stretch of time relates to a preference over another. When outcomes must vary continuously, an agent cannot freely paste two trajectories together at a chosen instant. Pivato's 2018 preprint asks which observable properties of preferences still force an integral representation under that constraint. The resulting theorem concerns a finite horizon; the paper also develops distinct infinite-horizon representations, which are outside this mission.

Earlier discounted-utility models often begin with an integral or a discounted sum and then study its implications. Here the integral is the conclusion. This changes the formalization problem: the preference structure, the permitted trajectories, and the relation between preferences on overlapping time regions must be defined independently of any utility or discount function. Theorem 1 on p. 13 is the paper's finite-horizon characterization. The Appendix A and B results selected as milestones connect its structural axioms to a content-based representation and then to an integral.

Trajectories, spans, and preferences

Time is the compact interval $\mathcal T=[0,T]$, with $T>0$. The outcome space $\mathcal X$ is connected, and a trajectory $\alpha$ is a continuous map from $\mathcal T$ to $\mathcal X$. A set $\mathcal A$ of feasible trajectories includes every constant trajectory $\kappa^x$, which gives outcome $x$ at every time. Feasibility is substantive: a trajectory obtained by pasting arbitrary continuous pieces may fail to be continuous at the join.

A time interval $\lfloor r,s\rceil$ is relatively open in $\mathcal T$. It includes $0$ when $r=0$ and $T$ when $s=T$, but excludes any interior endpoints. A time span $\mathcal S$ is a finite union of disjoint such intervals with distinct endpoints. The empty span is allowed. Relative interior and closure give the Boolean operations $\neg\mathcal S=\operatorname{int}(\mathcal S^{\mathrm c})$ and $\mathcal Q\vee\mathcal R=\operatorname{int}\operatorname{cl}(\mathcal Q\cup\mathcal R)$. These operations can bridge omitted boundary instants.

For every time interval $\mathcal I$, a primitive preference order $\succeq_{\mathcal I}$ compares restrictions of members of $\mathcal A$ to $\mathcal I$. Each such order is complete, transitive and nontrivial. The order $\succeq$ on the whole horizon is $\succeq_{\mathcal T}$; its comparison of constant trajectories induces the synchronic preference $\succeq_{\mathrm{sy}}$ on outcomes. Preferences $\succeq_{\mathcal S}$ on general spans are induced through the paper's limited-separability construction: representatives agree with the compared trajectories on $\mathcal S$, are indifferent on each component of $\neg\mathcal S$, and are then compared on the full horizon. The representatives must belong to $\mathcal A$.

The axioms constrain this primitive structure. Richness (R) permits preference-preserving insertion of a middle trajectory between fixed outer restrictions. Minimal equicontinuity (MinEqn) requires interiors of synchronic contour preimages to be time spans. The eight characterization axioms are interval separability (ISep), limited separability (LSep), static equivalence (StEq), continuity of synchronic preferences (C), dominance (Dom), continuity of intertemporal preferences (CIP), tradeoff consistency (TC), and ephemerality (Eph). Their definitions refer only to preferences and feasible trajectories.

Formalization target

A discounted utility integral representation consists of a continuous utility $u:\mathcal X\to\mathbb R$ and a continuous, strictly increasing map $\rho:[0,T]\to[0,1]$ with $\rho(0)=0$ and $\rho(T)=1$. For every time span $\mathcal S$ and feasible restricted trajectories $\alpha,\beta$, it satisfies

$$\alpha\succeq_{\mathcal S}\beta \quad\Longleftrightarrow\quad \int_{\mathcal S}u(\alpha(t))\,d\rho(t) \geq \int_{\mathcal S}u(\beta(t))\,d\rho(t).$$

The goal is Theorem 1 of the preprint: under the standing preference assumptions, (R), and (MinEqn), the eight axioms hold if and only if such a representation exists. The theorem also says that the normalized $\rho$ is unique and that any two representing utility functions differ by $u'=a u+b$ for some $a>0$ and $b\in\mathbb R$. The milestone list includes the structural equivalences of Lemmas A1, A3 and A4; the compatibility and separability results of Lemma A5 and Proposition A6; the richness result of Lemma A9; the comeasurability claim of Lemma B1; and the content-utility characterization in Theorem B2(b).

What the result supplies

The characterization identifies when local comparisons, continuity, and consistency of tradeoffs across regions of time determine one common utility scale and one normalized time weight. The uniqueness clauses prevent two different discount profiles from representing the same structure, while allowing the expected positive affine freedom in utility. Without the characterization, an integral can be used as an example of a preference rule, but the stated axioms would not certify that every admissible rule has that form.

The paper gives a mathematical proof, but this mission records open Lean statements rather than verified proofs. A completed development would make the time-span algebra, the induced intermittent order, and the content integrator reusable for related representation results. It would also expose precisely where the finite-horizon assumption is used before adapting the framework to the paper's later infinite-horizon theorems. The cited preprint relies in part on companion results about contents and their measure representations; formal proofs of those results are welcome groundwork.

Main obstacle

Continuous trajectories cannot generally be pasted at a time boundary while remaining feasible. This blocks the immediate finite-product argument often used for separable preferences. The paper's richness conditions replace that maneuver with preference-equivalent trajectories whose restrictions can be coordinated across component intervals. A second difficulty is that a finitely additive content on regular-open spans is not automatically a Borel measure: the representation needs a way to account for boundary behavior before the integral formula follows. The source treats this in its appendices and invokes companion work.

Formalization scope

Lean uses the subtype $[0,T]$ with its relative topology, continuous maps for feasible trajectories, and sets of subtype times for spans. A member of $\mathcal A(\mathcal S)$ is represented by a full member of $\mathcal A$, so comparisons never range over arbitrary functions on $\mathcal S$. The intermittent order is existentially induced from whole-horizon comparisons; a universally quantified extension rule could be vacuous when no extension exists. The axioms are stated directly on preferences, without mentioning $u$ or $\rho$.

The integral is represented by integration against the Lebesgue–Stieltjes measure of a continuous StieltjesFunction. This is the paper's Riemann–Stieltjes expression on bounded continuous integrands, using its equation (B12). Integrals are restricted to the image of the span in $\mathbb R$. The representing function is normalized at both horizon endpoints; uniqueness compares its values on $[0,T]$. Both the final integral representation and the intermediate content representation require agreement with primitive interval orders, in accordance with their identification with induced orders in Lemma A5. The intermediate utility also represents synchronic preference.

The strict clauses of (Dom), (TC), and (CIP) range over nonempty spans; at the empty span their literal unqualified forms become contradictory. Condition (R) is stated for a nonempty middle interval, $q\le r<s\le t$: with $r=s$ as printed, continuity would force the two outer trajectories to agree at $r$, which no set containing two distinct constant trajectories in a Hausdorff outcome space can satisfy. These domain choices and the specialization of Appendix B's Theorem B2 to $[0,T]$ are recorded in the moderation notes. Definitions of time spans, preference orders, contents, simple-function integration, and the measure connection are reusable contributions. Machine-checked proofs of the listed milestones and of the final equivalence are the intended contributions.

Selected references

• Marcus Pivato, Intertemporal Choice with Continuity Constraints, SSRN preprint 3232014, August 10, 2018. Preprint. The later journal version appeared in Mathematics of Operations Research (2021), DOI; the mission's page and theorem citations use the 2018 preprint.
• Alfred Horn and Alfred Tarski, Measures in Boolean Algebras, Transactions of the American Mathematical Society 64 (1948). DOI. The paper cites its extension theorem at Lemma B4.

Motivation

Large bonuses in some industries are paid within a few weeks of each other across firms: banks in a given region announce bonuses in the same months, and top-tier US law firms announce theirs almost simultaneously. Van Wesep and Waters (SSRN 3124536, published in Management Science, 2022, doi:10.1287/mnsc.2021.4076) explain this coordination with a search model of the labor market. If many workers leave their employers at the same time of year, the labor market is deeper at that time, which makes it a better time to replace a worker who has become a poor match. Firms then have reason to make dissatisfied workers stay until that time, which a bonus at the end of the cycle achieves, and the bonuses in turn concentrate quits at that time. The question is when this self-reinforcing seasonality is an equilibrium.

The model builds on the search-theoretic labor market with an aggregate matching function (surveys: Petrongolo and Pissarides, 2001; Rogerson, Shimer and Wright, 2005) and on wage bargaining with transferable utility.

Setting

Time is discrete; periods alternate between odd (index 1) and even (index 2). A continuum of firms of mass $M>0$ and of workers of mass $N>0$, $N\neq M$, are either matched in pairs or searching. A match produces revenue $1$ per period. A new worker is satisfied, with per-period disutility $x^L$; at the end of each period a satisfied worker becomes dissatisfied, with disutility $x^H$, with probability $p$, and stays so; matches separate exogenously with probability $\delta$; workers may quit at the end of any period. Here $0<x^L<x^H<1$ and $\beta,\delta,p\in(0,1)$, $\beta$ the discount factor. The importance of match quality is

$$\alpha=\frac{x^H-x^L}{1-x^L}.$$

If $M^0$ firms and $N^0$ workers search, $m(M^0,N^0)$ matches form, where $m$ is homogeneous of degree one, increasing in each argument, differentiable, and $m\le\min\{M^0,N^0\}$ (Assumption A1). A vacant firm matches with probability $f=m(M^0,N^0)/M^0$ and an unemployed worker with probability $g=m(M^0,N^0)/N^0$; these depend only on the labor market depth $n^0=N^0/M^0$.

In the periodic turnover plan, a dissatisfied worker quits at the end of even periods and stays at the end of odd periods. Under it the masses searching at the start of each period solve a fixed system of flow equations, which yield matching likelihoods $f_1,f_2,g_1,g_2$. A newly matched pair bargains over pay with worker weight $\theta\in(0,1)$ (generalized Nash bargaining); the resulting values $J_s$ (firm with a new hire), $V_s$ (vacant firm), $W_s$ (new hire, gross of pay), $U_s$ (unemployed worker) and the bargained present value of pay $P_s$ solve a linear system together with the Nash conditions. With $h_s=\theta g_s+(1-\theta)f_s$ and $\hat\beta=\beta(1-\delta)$ the paper defines two thresholds

$$\underline\alpha=\frac{(1-h_1)(1-\hat\beta(1-p))(1+\hat\beta(1-h_2))}{1+\hat\beta(1-h_1)\big(p-\hat\beta(1-p)(1-h_2)\big)},\qquad \overline\alpha=\frac{1-h_2-\hat\beta(1-p)(1-h_1)\big(h_2+\hat\beta(1-p)(1-h_2)\big)}{1-\hat\beta^2(1-p)^2(1-h_1)(1-h_2)}.$$

A periodic equilibrium consists of a labor-market state solving the flow equations, with depth differing between odd and even periods; Nash-bargained values; Pareto optimality of the periodic plan for every newly matched pair (no other turnover plan yields a larger joint value); and a periodic contract $\{b^s_1,b^s_2,w_1,w_2\}$ (a signing bonus depending on the hiring period, a wage $w_1$ in odd and $w_2$ in even periods) that makes the periodic plan incentive compatible and delivers the bargained present values $P_1$, $P_2$.

Formalization targets

Goal: Proposition 2

With $\underline\alpha,\overline\alpha$ computed from the solution of the flow equations,

$$\underline\alpha<\alpha<\overline\alpha\ \Longrightarrow\ \text{a periodic equilibrium exists},\qquad \alpha\notin[\underline\alpha,\overline\alpha]\ \Longrightarrow\ \text{no periodic equilibrium exists}.$$

Milestones

1. Lemma 1: $f$ increases and $g$ decreases in labor market depth.
2. Lemma 2: the flow equations have a unique solution; $f_2<f_1<g_1<g_2$ if $N<M$ and $g_2<g_1<f_1<f_2$ if $M<N$.
3. Equations (24)–(25): the Nash transfer is $P_1=\beta U_2-W_1+\theta S_1$, $P_2=\beta U_1-W_2+\theta S_2$, with $S_s$ the match surplus.
4. Lemma 3: closed forms for $S_1,S_2,P_1,P_2$.
5. Equations (78)–(79), (84)–(85): $U_s$ and $U_s+V_s$ in terms of the surpluses.
6. Lemma 4: incentive compatibility of a periodic contract reduces to three linear inequalities in $w_1,w_2$; the bonuses are determined by $P_1,P_2$.
7. Lemma 5: an incentive-compatible periodic contract with present values $P_1,P_2$ exists.
8. Conditions (i) and (ii) of the proof of Proposition 1: retaining a dissatisfied worker after an odd period is optimal iff $\alpha\le\overline\alpha$; releasing her after an even period is optimal iff $\alpha\ge\underline\alpha$.
9. Proposition 1: for $\alpha\in(\underline\alpha,\overline\alpha)$ the periodic plan strictly beats every other plan; for $\alpha\notin[\underline\alpha,\overline\alpha]$ it is not Pareto optimal.

Significance

Proposition 2 is the existence result on which the paper's account of coordinated bonuses rests: the subsequent results on equilibrium contracts (that rising wage profiles, i.e. end-of-cycle bonuses, always implement the equilibrium and are sometimes necessary) and on the stylized facts of compensation in finance and law presuppose a periodic equilibrium. It shows that seasonality of labor markets can be self-sustaining, with no exogenous seasonal shock, exactly when match quality matters neither too little (then dissatisfied workers are never released) nor too much (then they are released at once).

The result is proved in the paper by hand algebra over a dozen coupled equations. No part of it is machine-checked, and the platform has no search-and-matching labor market, no aggregate matching function and no turnover contract. The mission produces a checked version of the existence characterization, of the closed forms behind it, and a reusable formal model of a two-period search market with Nash-bargained, incentive-compatible contracts.

Difficulty

Lemma 2's existence and ordering do not follow from monotonicity of $m$ alone: the flow equations couple both periods, and the natural scalar reduction evaluates $m$ outside its domain when $N>M$, so the interval on which an intermediate-value argument runs must be chosen with care. The closed forms of Lemma 3 come from eliminating ten unknowns from a linear system whose coefficients are themselves the matching likelihoods; the paper's own equation (21) contains a typo that makes (29) false if taken literally. The thresholds of Proposition 1 require turning two inequalities on joint values into inequalities in $\alpha$, where the sign of each denominator has to be controlled. Finally, the equilibrium compares the periodic plan with every alternative plan through their joint-value recursions, not through the closed forms.

Formalization scope

All quantities are real. Periods are indexed 1 (odd) and 2 (even); firm masses are derived, $M^0_s=N^0_s+M-N$. Assumption A1 is stated on the closed quadrant, with "increasing" read strictly, which Lemma 2's strict inequalities require. Equation (21) is used with $\delta$ restored, $W_2=-x^L+\beta((1-\delta)(1-p)W_1+[1-(1-\delta)(1-p)]U_1)$. Nash transfers are defined as maximizers of the Nash product, not by (24)–(25). Definition D3 is imposed as $N^0_1\neq N^0_2$. Pareto optimality compares the four turnover plans that are stationary across periods of the same parity, with satisfied workers never quitting, through their joint-value recursions. Present values of contracts are infinite sums. The goal leaves the endpoints $\alpha=\underline\alpha,\overline\alpha$ open: the paper's statement excludes them while its proof includes them. Proposition 1's printed interval $[\overline\alpha,\underline\alpha]$ is read as $[\underline\alpha,\overline\alpha]$, as in its proof.

The periodic equilibrium is not defined through $\underline\alpha$, $\overline\alpha$, conditions (i)–(ii) or the closed forms, which would make the goal a tautology; it is built from the market equations, the bargaining problem, the plan comparison and the contract.

Corollary 1, Proposition 3, Lemmas 6–7 and §5–6 are not part of this mission. Contributions to the infrastructure (Nash split, geometric tsum evaluation of periodic present values, contraction arguments for the value recursions) are welcome and reusable for other search and bargaining models.

Selected references

• E. D. Van Wesep and B. Waters, Bonus season: A theory of periodic labor markets and coordinated bonuses, SSRN 3124536 (version of January 13, 2021); Management Science, 2022. https://ssrn.com/abstract=3124536, https://doi.org/10.1287/mnsc.2021.4076
• B. Petrongolo and C. A. Pissarides, Looking into the black box: A survey of the matching function, Journal of Economic Literature 39, 390–431, 2001. https://doi.org/10.1257/jel.39.2.390
• R. Rogerson, R. Shimer and R. Wright, Search-theoretic models of the labor market: A survey, Journal of Economic Literature 43, 959–988, 2005. https://doi.org/10.1257/002205105775362014

Motivation

Asset-pricing models relate an asset's expected return to the risks it shares with the market. A familiar covariance term measures exposure to the market return, while a coskewness term measures exposure to the square of that return. Shi, Cui and Zhou ask how these two coefficients change when investors weight probabilities as well as valuing outcomes. Their 2020 working paper derives a market pricing kernel and a three-moment capital asset pricing relation from a representative investor's rank-dependent utility. The paper subsequently studies the signs of the coefficients and tests the resulting relationships with financial data; this mission concerns its theoretical pricing result, Theorem 2.

Setting

At date 0, investors choose positions in finitely many assets. At date 1, asset $i$ pays a random total return $R_i$ per unit invested. One asset is risk-free, so its total return is the constant $1+r_f$. A pricing kernel $\tilde m$ is a strictly positive random variable that prices every total return by $\mathbb E[\tilde mR_i]=1$. The market return is $\tilde R_M=\sum_i x_i^M R_i$, where the market-capitalization weights sum to one. A return rate subtracts the invested unit: $\tilde r_i=R_i-1$ and $\tilde r_M=\tilde R_M-1$. These are the conventions of §§2–3 of the source.

The representative investor has rank-dependent utility. For a nonnegative payoff $X$ with cumulative distribution function $F_X$, an outcome-utility function $u$, and a probability-weighting function $w$, its value is the distributional integral

$$U(X)=\int_{\mathbb R}u(x)w'(1-F_X(x))\,dF_X(x).$$

The model assumes an atomless probability space; $u$ is strictly increasing and strictly concave on positive wealth, continuously differentiable there, and satisfies the Inada and asymptotic-elasticity conditions of Assumption 1; $w$ is strictly increasing and continuously differentiable on $[0,1]$, with $w(0)=0$ and $w(1)=1$. Problem (P′) asks for the largest $U(X)$ among measurable nonnegative payoffs with $\mathbb E[\tilde mX]=1$. Equilibrium means that $\tilde R_M$ attains this value. The working paper states these assumptions and this optimization problem on pp. 8–9 and identifies equilibrium with the optimal market return in Appendix A, p. 33 (source).

Write $F_M$ for the CDF of $\tilde R_M$ and set $K=\mathbb E[w'(1-F_M(\tilde R_M))u'(\tilde R_M)]$. The paper defines the pricing function

$$m(x)=\frac{w'(1-F_M(x))u'(x)}{(1+r_f)K},\qquad x>0.$$

The probability weight depends on the market distribution, while marginal utility depends on the realized total return. Their joint variation determines the pricing coefficients in Theorem 2 (source, pp. 10–11).

Formalization targets

Equilibrium kernel

For an equilibrium whose market return has a continuous CDF, the goal begins with the almost-sure identity

$$\tilde m=m(\tilde R_M).$$

Appendix A states an intermediate first-order form with a positive multiplier $\lambda^*$, then equation (12) determines $\lambda^*=(1+r_f)K$ from the risk-free asset. Both are milestones (source, pp. 33–34).

Three-moment pricing relation

When $F_M$ has a continuously differentiable density $f$, Theorem 2 gives a beta premium $A$ and a coskewness premium $B$ by the closed forms in its equations (6)–(7), with $A=-(1+r_f)m'(1)$ and $B=-(1+r_f)m''(1)$. It states

$$\mathbb E[\tilde r_i] =r_f+A\operatorname{Cov}(\tilde r_i,\tilde r_M) +\tfrac12B\operatorname{Cov}(\tilde r_i,\tilde r_M^2)+o(\tilde r_M^2).$$

The formal target makes the last term exact. Define $\rho(x)=m(1+x)-m(1)-m'(1)x-\tfrac12m''(1)x^2$, with $\rho(x)=o(x^2)$ as $x\to0$. The pricing identity then has remainder $-(1+r_f)\operatorname{Cov}(\rho(\tilde r_M),\tilde r_i)$. The source's quadratic expansion (13), its premium identities (6)–(7), and its covariance pricing identity are the remaining milestones (source, pp. 11 and 34–35).

Significance

The kernel identity connects the market's state prices to both marginal utility and probability weighting. The three-moment relation then specifies how an asset's covariance and coskewness with the market enter its expected return. Without the kernel identity the coefficients would be free parameters; without the density and derivatives their explicit forms would be unavailable. The paper uses these coefficients to analyze beta and coskewness pricing under particular weighting functions and later compares the relationships with data (source, §§3–5).

The paper result is published in Operations Research; this mission follows the held SSRN version of June 2, 2020, whose theorem numbering and pages are pinned below. The Lean theorem statements in this proposal compile as open targets; they do not yet have machine-checked proofs. A completed development would add a reusable RDU model, a pricing-kernel characterization under equilibrium, and a precise covariance relation with a controlled remainder. The later parameter-specific propositions and empirical sections are outside this mission.

Difficulty

The central difficulty is the first part of the theorem. The optimality condition concerns an objective that depends on the entire payoff distribution through $F_X$, so ordinary pointwise differentiation of $u(X)$ does not identify the kernel. The paper obtains this step from an earlier result of Xia and Zhou, then uses the risk-free asset to fix the multiplier (source, Appendix A). The second part needs third derivatives of $u$ and $w$ although Assumption 1 only says they are continuously differentiable. It also uses a random-variable little-o without specifying how that term enters an expected return. These are mathematical conditions the formal statement must make explicit.

Formalization scope

Lean represents the probability space by a probability measure and atomless by the event-splitting property: every positive-measure event has a measurable subset of strictly intermediate measure. Assets are indexed by Fin n; the risk-free asset is specified by its constant total return, and $\tilde R_M$ is computed from the weights and asset returns. The RDU objective is the paper's integral against the payoff law, including the CDF factor, and equilibrium is optimality for problem (P′). It is not defined through the desired kernel equation.

The Bochner RDU integral is required to be integrable for the market payoff and for compared competitors. Those competitors also have continuous CDFs and positive payoffs almost surely, so endpoint values of the two-sided derivatives and the utility at zero do not affect the comparison. This is a disclosed strengthening of the conclusion's scope: the equilibrium requirement compares fewer payoffs than the paper writes. The CAPM clause assumes local $C^3$ regularity of $u$ at $1$ and $w$ at $1-F_M(1)$, $0<F_M(1)<1$, a nonnegative $C^1$ density represented as the law of $\tilde R_M$, and finite second and fourth moments needed for genuine covariances. Its premiums are the closed forms of (6)–(7), and its remainder is computed from $m$, once for every asset. The kernel identity is a conclusion; an assumed kernel or an independently chosen remainder would erase the target.

The development uses Mathlib's CDF, pushforward and density measures, Bochner integrals, covariance, MemLp, derivatives, and little-o. The event-splitting predicate, priced-market interface, RDU functional, feasibility and equilibrium notions, closed-form premiums, and Taylor remainder are local definitions. Contributions to the first-order characterization, the derivative identities, the precise expansion, and the covariance step all advance the goal.

Selected references

• Yun Shi, Xiangyu Cui and Xun Yu Zhou, Beta and coskewness pricing: perspective from probability weighting, SSRN 3579960, version of June 2, 2020; published in Operations Research 71(2), 2023. Working paper; journal DOI.

Motivation

A trade moves the price at which subsequent trades are executed. Price impact models describe this shift as a function of the signed order flow and are the basic input of optimal execution and statistical-arbitrage problems. Empirically, the immediate impact of a trade is a concave function of its size, close to a square root for large orders (Bouchaud et al. 2009; Bucci et al. 2019), while most tractable models for optimal trading assume linear impact, as in the model of Obizhaeva and Wang (2013). Muhle-Karbe, Wang and Webster (SSRN 4286108; Operations Research, 2022) connect the two: when trades are small, frequent and diffusive, a nonlinear propagator model with concave impact converges to a linear impact model whose illiquidity parameter is stochastic and moves with the volatility of order flow. This mission formalizes that scaling limit, Theorem 3.3 of the paper, together with the steps of its proof in Appendix A.1.

Setting

Fix a horizon $T>0$ and a filtered probability space $(\Omega,\mathcal F,(\mathcal F_t),P)$ carrying two independent $(\mathcal F_t)$-Brownian motions $W$ and $W^\perp$. The signed order flow is an Itô process with stochastic volatility,

$$dF_t=\mu_t\,dt+v_t\,dW_t,\qquad dv_t=a_t\,dt+\eta_t\,dW_t+b_t\,dW^\perp_t,$$

where $\mu,a,\eta,b$ are locally bounded càdlàg processes, $v_t>0$, and $E\big[\int_0^T F_t^2\,dt\big]<\infty$.

Divide $[0,T]$ into $N$ steps of width $\Delta t^N=T/N$, with grid points $t^N_n=n\Delta t^N$ and increments $\Delta F^N_n=F_{t^N_n}-F_{t^N_{n-1}}$. An impact function $g:\mathbb R\to\mathbb R$ is odd, continuously differentiable and concave on $[0,\infty)$. The nonlinear propagator model (Definition 2.1) with the diffusive scaling (3.1) is the recursion

$$I^N_0=0,\qquad \Delta I^N_n=-\beta I^N_{n-1}\Delta t^N+\sqrt{\Delta t^N}\,g\Big(\tfrac{1}{\sqrt{\Delta t^N}}\Delta F^N_n\Big),$$

for a decay rate $\beta>0$: each trade shifts the price by a concave function of its size, and the shift decays exponentially.

The limit involves Gaussian averages of $g$. With $\phi_v$ the density of the centred normal law with standard deviation $v$,

$$\lambda_t=\int g'\phi_{v_t},\quad \chi_t=\tfrac12\int(v_t^{-2}x^2-1)g'(x)\phi_{v_t}(x)\,dx,\quad \zeta_t=\Big(\int g^2\phi_{v_t}\Big)^{1/2},\quad h_t=\int xg(x)\phi_{v_t}(x)\,dx,$$

and $\theta_t=\sqrt{\lambda_t^2v_t^2+\zeta_t^2-2\lambda_th_t}$.

A limit of this kind lives on an extension of the probability space, a larger filtered space $(\Omega',(\mathcal G_t),P')$ with a projection $\pi:\Omega'\to\Omega$ preserving the law; it is very good if every $(\mathcal F_t)$-martingale remains a $(\mathcal G_t)$-martingale. Stable convergence in law of processes $X^N$ on $\Omega$ to $X$ on such an extension means $E[Y f(X^N)]\to E'[(Y\circ\pi)f(X)]$ for every bounded measurable $Y$ on $\Omega$ and every bounded path functional $f$ that is Lipschitz for the uniform distance on $[0,T]$.

Formalization targets

Goal: Theorem 3.3 (p. 7)

As $N\to\infty$, the step paths $t\mapsto I^N_{\lceil t/\Delta t^N\rceil}$ converge stably in law to a solution of the linear impact model

$$dI_t=-\beta I_t\,dt+\lambda_t\,dF_t+\eta_t\chi_t\,dt+\theta_t\,dW'_t,\qquad I_0=0,$$

where $W'$ is a Brownian motion on a very good extension with

$$d[W,W']_t=\frac{1}{\theta_t}\Big(\frac{h_t}{v_t}-\lambda_tv_t\Big)dt .$$

Milestones (Appendix A.1, in attack order)

1. Explicit solution (p. 27): $I^N_n=\sum_{m=1}^n(1-\beta\Delta t^N)^{n-m}\sqrt{\Delta t^N}g(\Delta F^N_m/\sqrt{\Delta t^N})=(1-\beta\Delta t^N)^n\sqrt{\Delta t^N}\sum_{m=1}^n(1-\beta\Delta t^N)^{-m}g(\Delta F^N_m/\sqrt{\Delta t^N})$.
2. Theorem A.3 (p. 25): for an Itô process $dX_t=b_t\,dt+\sigma_t\,dW_t$ with Itô volatility (Assumption A.1) and $F(t,x)$ odd, $C^1$ in $x$, of linear growth and Hölder in time (Assumption A.2),

$$\sqrt{\Delta t^N}\sum_{n=1}^{\lceil t/\Delta t^N\rceil}F\Big(t^N_{n-1},\tfrac{\Delta X^N_n}{\sqrt{\Delta t^N}}\Big)\to\int_0^t\Big(b_s\tilde E[\partial_xF(s,\sigma_sZ)]+\tfrac{\tilde\sigma_s}{2}\tilde E[(Z^2-1)\partial_xF(s,\sigma_sZ)]\Big)ds+\int_0^t\sqrt{\tilde E[F^2(s,\sigma_sZ)]}\,dW'_s$$

stably in law, with $Z$ standard normal and $[W,W']_t=\int_0^t\tilde E[ZF(s,\sigma_sZ)]/\sqrt{\tilde E[F^2(s,\sigma_sZ)]}\,ds$. 3. Rescaled convergence (p. 28): $\sqrt{\Delta t^N}\sum_{m=1}^{n}e^{\beta t^N_m}g(\Delta F^N_m/\sqrt{\Delta t^N})\to e^{\beta t}I_t$ stably in law.

Significance

The theorem shows that the nonlinearity of microstructure impact does not disappear in the continuous-time limit; it is absorbed into a stochastic illiquidity $\lambda_t$ that is an explicit Gaussian average of $g'$ at the current order-flow volatility, plus an additional noise term $\theta_t\,dW'_t$ and a drift correction $\eta_t\chi_t$. Section 4 of the paper uses the limit to solve optimal trading problems explicitly for nonparametric signals and to derive conditions that rule out price manipulation, and Section 5 fits the resulting model to public trading data. Without the limit theorem, those linear-model results would have no stated connection to the concave impact observed in the data.

The paper proves Theorem 3.3 by reduction to a functional central limit theorem of Jacod and Protter (2012, Theorem 10.3.2(a)), outlined in Appendix A.1 rather than written out. To our knowledge none of these results has a machine-checked proof. The mission produces a precise statement of the scaling limit, including the mode of convergence and the space on which the limit lives, and a formal statement of the stable functional CLT (Theorem A.3), which is a standard tool in high-frequency statistics and reusable well beyond this paper.

Difficulty

The impact process is not a functional of increments of a fixed process: $I^N$ solves a difference equation whose coefficients depend on the grid, so a central limit theorem for sums $\sum F(\Delta X^N_n)$ does not apply to it directly. Even for such sums the stable CLT is needed in full: the rescaled increments $\Delta F^N_n/\sqrt{\Delta t^N}$ are of order one, so $g$ cannot be linearized pointwise, and the limit carries both a Gaussian average of $g'$ and an independent noise term. The CLT itself is the hard part. Its limit lives on an extension of the original space, the drift term arises from the correlation between the volatility increments and the increments of $X$, and stability (joint convergence with every bounded $\mathcal F$-measurable variable) is what allows the limit to be combined with the stochastic factor $e^{-\beta t}$ and with $\lambda_t\,dF_t$. A naive Taylor expansion of $g$ around zero gives the wrong limit for every nonlinear $g$.

Formalization scope

Time is $\mathbb R_{\ge0}$ and statements read $[0,T]$. Brownian motions are IsBrownianReal with continuous paths for every $\omega$, adapted, with increments independent of the past; Itô integrals use the published relation EthierKurtz_HasBrownianItoIntegral with continuous versions, and quadratic covariation the published EthierKurtz_HasCrossVariation. Itô coefficients are progressively measurable with locally integrable drift paths. $\phi_v$ is Mathlib's gaussianPDFReal 0 (v^2), whose parameter is the variance. Stable convergence is encoded with bounded measurable $Y$ times bounded functionals Lipschitz for the $[0,\infty]$-valued uniform distance on $[0,T]$; since the limits have continuous paths this matches Skorohod-topology stable convergence, and no Skorohod space is built. The goal is existential in the extension, in $W'$ and in the solution $I$; a universal reading would be false.

Added and disclosed conventions: the growth bound $|g(x)|+|g'(x)|\le C(1+|x|)$ (Assumption A.2(c), p. 25, required by the paper's proof); $I^N_0=0$ and $I_0=0$; $\lceil t/\Delta t^N\rceil$ capped at $N$ for the paper's $\lceil Nt\rceil$; $\beta\Delta t^N\ne1$ for the negative powers on p. 27. The printed formulas for $\theta_t$ and $d[W,W']_t$ are kept.

The statements cannot be satisfied trivially: $I$ is a solution of the integral equation (3.2), not a definition as the limit of $I^N$; the coefficients are the Gaussian integrals themselves; and the test class of stable convergence contains non-constant functionals, so convergence of the zero process to a non-zero limit fails (checked in a sorry-free sanity file).

A complete development needs a stable functional CLT for triangular arrays, Gaussian integration by parts, existence of very good extensions carrying independent Brownian motions, and pathwise stochastic calculus for Itô processes with stochastic volatility. The extension and stable-convergence definitions and Theorem A.3 are reusable for realized-variance and high-frequency estimators. Contributions on any milestone, and on the general infrastructure, are welcome.

Selected references

• J. Muhle-Karbe, Z. Wang, K. Webster, Stochastic liquidity as a proxy for nonlinear price impact, Operations Research, 2022; cited from SSRN 4286108, version of November 2, 2023. https://ssrn.com/abstract=4286108 (DOI 10.1287/opre.2022.0627)
• J. Jacod, P. Protter, Discretization of Processes, Springer, 2012. https://doi.org/10.1007/978-3-642-24127-7
• A. A. Obizhaeva, J. Wang, Optimal trading strategy and supply/demand dynamics, Journal of Financial Markets 16, 2013. https://doi.org/10.1016/j.finmar.2012.09.001
• J.-P. Bouchaud, J. D. Farmer, F. Lillo, How markets slowly digest changes in supply and demand, Handbook of Financial Markets, 2009. https://arxiv.org/abs/0809.0822
• F. Bucci, M. Benzaquen, F. Lillo, J.-P. Bouchaud, Crossover from linear to square-root market impact, Physical Review Letters 122(10):108302, 2019. https://doi.org/10.1103/PhysRevLett.122.108302

Why bilevel optimality needs a second-order condition

In a bilevel program, the decision maker chooses an upper-level variable while a second decision must solve a lower-level optimization problem. This structure occurs when a leader anticipates the response of a follower, or when an outer design problem contains an optimization problem as a constraint. A feasible upper-level decision can therefore change the lower-level solution set as its parameters move. Ordinary smooth constrained optimization tests do not directly describe that dependence. Mehlitz and Zemkoho study sufficient optimality conditions for this setting; their Theorem 5.3 gives a second-order condition ensuring a strict local minimum with quantitative growth. Mehlitz and Zemkoho, 2019

The bilevel model and the value function

Write $x\in\mathbb R^n$ for the upper-level decision and $y\in\mathbb R^m$ for the lower-level decision. The upper-level objective is $F(x,y)$, with componentwise constraints $G_i(x,y)\leq0$. At each fixed $x$, the lower-level feasible set is $K(x)=\{y:g_j(x,y)\leq0\text{ for every }j\}$, and its solution set is $S(x)=\operatorname*{argmin}_{y\in K(x)}f(x,y)$. The bilevel feasible set is $M=\{(x,y):G_i(x,y)\leq0\text{ for all }i,\ y\in S(x)\}$. The program minimizes $F$ over $M$. All components of $F,f,G,g$ are twice continuously differentiable, as assumed on page 2 of the source. Mehlitz and Zemkoho, pp. 1–2

The lower-level value function is $\varphi(x)=\inf_{y\in K(x)}f(x,y)$. It may be nonsmooth even though the data are smooth. The condition $y\in S(x)$ can be expressed using $g(x,y)\leq0$ and $f(x,y)\leq\varphi(x)$, giving the value-function reformulation. For the main theorem, $\varphi$ is locally Lipschitz near the reference point and has a second-order directional derivative $\varphi''(\bar x;d,w)$. This derivative measures the second-order change along the curved path $\bar x+td+\tfrac12t^2w$, after subtracting the first-order directional term. Mehlitz and Zemkoho, pp. 5, 8–9

At a feasible point $(\bar x,\bar y)$, the paper defines a linearization cone $L_M^\varphi$ by the active $G$ and $g$ inequalities and the linearized value-function inequality. Its critical cone $C_M^\varphi$ adds the directions in which the first-order change of $F$ is nonpositive. The Abadie constraint qualification, abbreviated ACQ, equates the tangent cone of $\{(x,y):g(x,y)\leq0\}$ with its linearization cone at $(\bar x,\bar y)$. It is imposed on this lower-level constraint set in the joint $(x,y)$ space. Mehlitz and Zemkoho, pp. 18–19

Formalization targets

Second-order growth for the bilevel program

The goal is Theorem 5.3. At a feasible $(\bar x,\bar y)$, assume ACQ for the lower-level constraint set, local Lipschitz continuity and second-order directional differentiability of $\varphi$, and second-order epi-regularity of $-\varphi$. The first-order test requires $\nabla F(\bar x,\bar y)^\top d\geq0$ on $L_M^\varphi$. For each nonzero $d\in C_M^\varphi$, the minimax program (5.5), formed from the second-order expansions of $F$, active $G_i$, $f-\varphi$, and active $g_j$, must have positive optimal value. The conclusion is

$$\exists C>0,\ \exists U\ni(\bar x,\bar y),\ \forall(x,y)\in M\cap U:\quad F(x,y)\geq F(\bar x,\bar y)+C\bigl(\|x-\bar x\|_2^2+\|y-\bar y\|_2^2\bigr),$$

and $(\bar x,\bar y)$ is a strict local minimizer of the bilevel program. The milestones capture the paper's supporting results: the $C^2$ derivative formula, rules for a finite maximum, the Hadamard derivative and tangent-cone necessary condition, Remark 5.1 under ACQ, and Proposition 2.10 on second-order growth. Mehlitz and Zemkoho, Theorem 5.3, pp. 19–20

What the result provides

The theorem turns tests on first- and second-order directional behavior into a guarantee about actual feasible bilevel decisions near the reference point. The growth estimate is stronger than strict local minimality: it quantifies how the upper-level objective rises with displacement along the feasible set. It applies when the lower-level value function is nonsmooth, provided its directional derivatives and epi-regularity are available. The paper gives special cases in which these hypotheses can be checked more concretely. Mehlitz and Zemkoho, §5, pp. 18–28

The result is proved in the source paper. The open work here is a machine-checked development of its variational definitions, finite-maximum rules, and sufficient-condition argument. The mission includes open Lean statements, not completed proofs. The reusable part is the generic theory of directional derivatives, epi-regularity, and growth on finite-dimensional normed spaces; the bilevel model and cones specialize it to this paper.

Where the formal proof is difficult

Smooth Taylor expansion alone does not handle $\varphi$: an infimum over a parameter-dependent feasible set can be nonsmooth. First-order stationarity on the paper's linearization cone also gives no quadratic increase in directions where the first-order change vanishes. The second-order test must retain the active indices of each constraint and the dependence of $\varphi''$ on both the first- and second-order directions. ACQ matters because the tangent-cone necessary condition for $f-\varphi$ does not automatically apply to every linearized lower-level direction; Example 5.2 of the paper demonstrates the failure without a constraint qualification. Mehlitz and Zemkoho, pp. 19–20

Formalization scope

Lean uses EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), with zero-based Fin indices and uncurried maps on their product. Fréchet derivatives express the paper's gradient and Hessian terms. Generic preliminary results are stated on finite-dimensional real normed spaces, a generalization of the Euclidean statements. The tangent cone uses positive sequences converging to zero. Directional derivatives are named finite limits; epi-regularity uses the eventual inequality for every admissible curved path and every positive error coefficient. The value function takes values in EReal, so an empty feasible set and an unbounded-below lower-level problem are represented by $+\infty$ and $-\infty$. A real representative agrees with it on a neighbourhood of $\bar x$, where the local Lipschitz and derivative hypotheses apply. This agreement rules out an unrelated or default-valued value function.

The theorem's growth estimate uses the sum of squared Euclidean norms printed in (5.6), not the product space's sup norm. The positive value of (5.5) is expressed by a uniform positive lower bound over every $w$ on its maximum of constraint expressions. The generic maximum rules use a nonempty finite index type. The preliminary formulation of Proposition 2.10 includes local Lipschitz continuity, used in this mission's application and disclosed as an added hypothesis relative to its printed statement. Real-valued functions and finite second-order limits are also explicit scope conventions.

Selected references

• Patrick Mehlitz and Alain B. Zemkoho, Sufficient Optimality Conditions in Bilevel Programming, arXiv:1911.01647v1, 2019; published in Mathematics of Operations Research, 2021. Preprint.

Motivation

Dividing indivisible goods fairly among agents with different preferences is a central problem of fair division, with uses ranging from inheritance and divorce settlements to course allocation and fair-division services such as Spliddit (Goldman–Procaccia 2014). Envy-freeness cannot always be achieved with indivisible goods (one good, two agents), so relaxations are studied. Envy-freeness up to any good (EFX), introduced by Caragiannis et al. (2019), is widely regarded as the strongest relaxation of this kind whose existence is still unsettled: whether every instance admits a complete EFX allocation is open in general, even for additive valuations.

Timeline.

• Plaut and Roughgarden (2020): complete EFX allocations exist when all agents share one identical general valuation, and for two agents with general valuations.
• Chaudhury, Garg and Mehlhorn (2020): existence for three agents with additive valuations.
• Mahara (2020): existence when every agent has one of two additive valuations.
• Berger, Cohen, Feldman and Fiat (2022): extension to two nice cancelable valuations; Pareto improvable cycles in the champion graph.
• Mahara (2021/2024): existence when every agent has one of two general valuations, the result of this mission.

Setting

There are $n \ge 1$ agents $0,\dots,n-1$ and a set $M$ of $m$ indivisible items. Each agent $i$ has a valuation $v_i$ assigning a real number to every bundle $S \subseteq M$. It is normalized, $v_i(\emptyset)=0$, and monotone, $S\subseteq T \Rightarrow v_i(S)\le v_i(T)$. Nothing else is assumed (general valuations: no additivity, submodularity or cancelability). Write $S <_i T$ for $v_i(S)<v_i(T)$.

An allocation $X=(X_0,\dots,X_{n-1})$ is a family of pairwise disjoint bundles. It is complete if every item is allocated, and partial otherwise. Agent $i$ envies $j$ if $X_i <_i X_j$. Agent $i$ EFX envies $j$ if $X_i <_i X_j\setminus\{h\}$ for some $h\in X_j$. The allocation is EFX if no agent EFX envies another, i.e.

$$v_i(X_j\setminus\{g\})\le v_i(X_i)\quad\text{for all agents } i,j \text{ and all } g\in X_j .$$

The two-valuation setting: there are set functions $v_a, v_b$ such that every $v_i$ equals one of them. $N_a$ and $N_b$ denote the agents with valuation $v_a$ and $v_b$.

The proof works with a vocabulary that the definition file formalizes. The terms are non-degeneracy (distinct bundles have distinct values), minimum preferred sets and $\kappa_X(i,S)$, most envious agents, $g$-champions, the champion graph $M_X$ and its Pareto improvable (PI) cycles, semi-EFX allocations, and the partition leximin potential $\psi(X)$. The potential lists $v_a(X_a)$ over $a\in N_a$ in increasing order, followed by $v_b(X_b)$ over $b\in N_b$ in increasing order. $Y\succ_{\mathrm{p.lexmin}}X$ means that $\psi(Y)$ is lexicographically larger than $\psi(X)$.

Formalization targets

Goal: Theorem 1 (p. 3)

$$\forall\, n\ge 1,\ \forall\, v \text{ normalized, monotone with } v_i\in\{v_a,v_b\}:\quad \exists\, X \text{ complete allocation that is EFX}.$$

Milestones, in the order the proof uses them

1. Lemma 18 (p. 25): for $\varepsilon>0$ small, $v'_i(S)=v_i(S)+\varepsilon\sum_{g_j\in S}2^j$ preserves strict preferences, is non-degenerate, and every EFX allocation for $v'$ is EFX for $v$.
2. Lemma 5 (p. 8): a $g$-champion of $j$ that does not envy $j$, with neither agent a self $g$-champion, $g$-decomposes $j$.
3. Lemma 8 (p. 9, Berger et al.): a PI cycle in $M_X$ yields a Pareto-dominating allocation that preserves the absence of EFX envy.
4. Lemma 15 (p. 12): a semi-EFX allocation can be turned into an EFX allocation without changing the bundles of $N_a$ or of the $v_b$-poorest agent $b_0$.
5. Theorem 14 (p. 12): for every partial EFX allocation $X$ there is an EFX allocation $Y$ with $Y\succ_{\mathrm{p.lexmin}}X$.
6. Termination (p. 12): Theorem 14 implies the existence of a complete EFX allocation.

Milestones 2–6 are stated for non-degenerate instances, as in the paper. The goal is not.

Significance

The result. Theorem 1 is the most general multi-agent EFX existence theorem in which the number of agents is unbounded and the valuations carry no structure beyond monotonicity. It contains the identical-valuation theorem of Plaut and Roughgarden and the two-additive-valuation theorem as special cases. The potential $\psi$ is the paper's tool for making progress when no Pareto-dominating EFX allocation exists. Pareto domination is the progress measure used for additive and cancelable valuations, and it fails for general ones.

Formalization. The theorem is proved on paper and, to our knowledge, has no machine-checked proof. The remaining work is to formalize the known proof: the perturbation reduction, the champion-graph machinery (minimum preferred sets, most envious agents, PI cycles), the semi-EFX repair, and the case analysis of Theorem 14. The champion-graph layer is shared with the proofs of EFX with charity and of EFX for four agents.

Difficulty

The obvious argument is Pareto improvement: from a partial EFX allocation, hand out an unallocated item and keep everyone at least as well off. For general valuations no Pareto-dominating EFX allocation need exist. The progress step must therefore sometimes make an agent strictly worse off, and that agent may then come to EFX envy others. Theorem 14 allows an agent of $N_b$ to lose value while improving the $v_a$-block of $\psi$. The paper repairs the resulting EFX envy, which is confined to $N_b$ (semi-EFX), by trimming bundles. Keeping track of which agents may envy which bundles through several reallocations is the central difficulty. The champion-graph statements are also delicate: minimum preferred sets are not unique, and the cardinality parameter $\kappa_X$ takes the value $+\infty$.

Formalization scope

Agents are Fin n and items Fin m, both 0-indexed. Valuations are maps Fin n → Finset (Fin m) → ℝ, assumed normalized and monotone (IsNormalized, IsMonotoneVal). Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values (IsPartialAllocation). Completeness is pool X = ∅. EFX is IsEFX, from the published definition file LittleCharity.EFX.Setting. The two valuation classes are a finset A of agents with v i = va on A and v i = vb off A; in the goal they are ∀ i, v i = va ∨ v i = vb. $\kappa$ takes values in ℕ∞. PI cycles are indexed by Fin k: distinct vertices, edge labels Option (Fin m), unallocated champion labels, labels pairwise disjoint. $\psi$ is a pair of sorted lists, and $\succ_{\mathrm{p.lexmin}}$ is the strict List.Lex (· < ·).

Disclosed readings:

• Decomposition quantifies over every minimum preferred set.
• The PI-cycle label condition is read for distinct edges.
• Lemma 15 keeps only the part of the chain $X_{b_0}<_b\cdots$ that names $b_0$.
• Theorem 14 assumes both classes nonempty, as its proof does.
• Lemma 8's printed clause "for any $i,j$, if $i$ does not EFX envy $j$ in $X$, then neither in $Y$" is false for non-EFX $X$. It is formalized along the cycle: the bundle of $a_t$ in $Y$ is judged against $a_{t+1}$'s bundle in $X$. This is the form the proof of Theorem 14 uses.

The goal assumes neither additivity nor non-degeneracy. Its only added hypothesis is $0<n$, which is necessary. Every item must be allocated: the empty allocation is always EFX, so a goal without completeness would be trivial. Contributions are welcome at every level: proofs of the milestones, the champion-graph library, and the termination argument for strict lexicographic orders on finite sets.

Selected references

• R. Mahara, Extension of Additive Valuations to General Valuations on the Existence of EFX, arXiv:2107.09901v2, 2021; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2107.09901
• B. Berger, A. Cohen, M. Feldman, A. Fiat, (Almost Full) EFX Exists for Four Agents (and Beyond), AAAI 2022. https://arxiv.org/abs/2102.10654
• B. Plaut, T. Roughgarden, Almost Envy-Freeness with General Valuations, SIAM Journal on Discrete Mathematics 34(2), 2020. https://doi.org/10.1137/19M124397X
• B. R. Chaudhury, J. Garg, K. Mehlhorn, EFX Exists for Three Agents, EC 2020. https://arxiv.org/abs/2002.05119
• R. Mahara, Existence of EFX for Two Additive Valuations, arXiv:2008.08798, 2020. https://arxiv.org/abs/2008.08798
• I. Caragiannis, D. Kurokawa, H. Moulin, A. D. Procaccia, N. Shah, J. Wang, The Unreasonable Fairness of Maximum Nash Welfare, ACM Transactions on Economics and Computation 7(3), 2019. https://doi.org/10.1145/3355902