All missions

Motivation

We show that, in any open set of distillable states, all asymptotic entanglement measures $E(ρ)$ are continuous as a function of (a single copy of) $ρ$, even though they quantify the entanglement properties of $ρ^{\otimes N}$ is the large $N$ limit.

This mission is the statement-level formalization of On the continuity of asymptotic measures of entanglement (arXiv:quant-ph/0203107v1). 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 Proposition 6 (abstract and main result): continuity inside the distillable region (Proposition 6 (abstract and main result): continuity inside the distillable region, PDF p. 2). 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:

• Eqs.(26)–(31): catalytic conversion inequality: Operational asymptotic catalytic mixed-state LOCC rate with pinned catalyst-size and return-error conventions (source-ambiguity)
• Unnumbered main result: catalytic distillation boundary continuity: Operational asymptotic catalytic mixed-state LOCC rate with pinned catalyst-size and return-error conventions; boundary topology in the convention of note [10] (source-ambiguity)

Selected references

• On the continuity of asymptotic measures of entanglement, arXiv:quant-ph/0203107v1, https://arxiv.org/abs/quant-ph/0203107v1

Motivation

In this paper, we introduce the concept of dual universality of hash functions and present its applications to quantum cryptography. We begin by establishing the one-to-one correspondence between a linear function family {\cal F} and a code family {\cal C}, and thereby defining \varepsilon-almost dual universal_2 hash functions, as a generalization of the conventional universal_2 hash functions. Then we show that this generalized (and thus broader) class of hash functions is in fact sufficient for the security of quantum cryptography. This result can be explained in two different formalisms. First, by noting its relation to the δ-biased family introduced by Dodis and Smith, we demonstrate that Renner's two-universal hashing lemma is generalized to our class of hash functions. Next, we prove that the proof technique by Shor and Preskill can be applied to quantum key distribution (QKD) systems that use our generalized class of hash functions for privacy amplification. While Shor-Preskill formalism requires an implementer of a QKD system to explicitly construct a linear code of the Calderbank-Shor-Steane type, this result removes the existing difficulty of the construction a linear code of CSS code by replacing it by the combination of an ordinary classical error correcting code and our proposed hash function. We also show that a similar result applies to the quantum wire-tap channel. Finally we compare our results in the two formalisms and show that, in typical QKD scenarios, the Shor-Preskill--type argument gives better security bounds in terms of the trace distance and Holevo information, than the method based on the δ-biased family.

This mission is the statement-level formalization of Dual universality of hash functions and its applications to quantum cryptography (arXiv:1101.0064v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

29 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §VII.A, equations (59)–(61): dual-universal privacy amplification on an iid Pauli wire-tap channel (§VII.A, equations (59)–(61): dual-universal privacy amplification on an iid Pauli wire-tap channel, PDF p. 14). 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

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

• Theorem 2: claimed sharpness of (8): A faithful valid statement of the printed parameter/domain claim. (source-ambiguity)
• Theorem 3, moreover: claimed sharpness of (18): A faithful valid statement of the printed parameter/domain claim. (source-ambiguity)
• Theorem 4, furthermore: claimed sharpness of (19): A faithful valid statement of the printed parameter/domain claim. (source-ambiguity)
• Lemma 1: printed dual-universality to delta-bias conversion: A faithful valid statement of the printed parameter/domain claim. (source-ambiguity)
• Lemma 2 ([10, Theorem 3.2]): cited quantum delta-biased masking bound: Verified full-scope quantum masking theorem with its support convention; this is cited background, not a new paper result. (hard)
• Lemma 3: printed collision bound for variable-dimension dual-universal families: A faithful valid statement of the printed parameter/domain claim. (source-ambiguity)
• §III, equation (28): corrected full-trace leftover bound: Full Hilbert-space cq leftover-hashing interface with trace-class blocks and possibly unbounded singular-reference inverse powers. (hard)
• §VI, equations (56)–(58): arbitrary Pauli-law phase and security bounds: Actual arbitrary-channel BB84 transcript instrument and its twirling-to-virtual-phase reduction. (hard)
• §VI: asymptotic sacrifice rate: A faithful valid statement of the printed parameter/domain claim. (source-ambiguity)
• §VII.A: complementary outputs of uniform coset and coherent CSS encoders: A faithful valid statement of the printed parameter/domain claim. (source-ambiguity)
• §VI / §VIII.C: security for full code-pair ensembles: Arbitrary-channel BB84 security transport for complete jointly seeded nested-code pairs. (hard)

Selected references

• Dual universality of hash functions and its applications to quantum cryptography, arXiv:1101.0064v4, https://arxiv.org/abs/1101.0064v4

Motivation

We provide a unified graphical calculus for all Gaussian pure states, including graph transformation rules for all local and semi-local Gaussian unitary operations, as well as local quadrature measurements. We then use this graphical calculus to analyze continuous-variable (CV) cluster states, the essential resource for one-way quantum computing with CV systems. Current graphical approaches to CV cluster states are only valid in the unphysical limit of infinite squeezing, and the associated graph transformation rules only apply when the initial and final states are of this form. Our formalism applies to all Gaussian pure states and subsumes these rules in a natural way. In addition, the term "CV graph state" currently has several inequivalent definitions in use. Using this formalism we provide a single unifying definition that encompasses all of them. We provide many examples of how the formalism may be used in the context of CV cluster states: defining the "closest" CV cluster state to a given Gaussian pure state and quantifying the error in the approximation due to finite squeezing; analyzing the optimality of certain methods of generating CV cluster states; drawing connections between this new graphical formalism and bosonic Hamiltonians with Gaussian ground states, including those useful for CV one-way quantum computing; and deriving a graphical measure of bipartite entanglement for certain classes of CV cluster states. We mention other possible applications of this formalism and conclude with a brief note on fault tolerance in CV one-way quantum computing.

This mission is the statement-level formalization of Graphical calculus for Gaussian pure states (arXiv:1007.0725v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

33 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is II.E: graph from measured second moments, Eq. (2.27) (II.E: graph from measured second moments, Eq. (2.27), 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

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

• Main result: Gaussian graphical calculus, abstract and Sections II–III: Operational Gaussian homodyne disintegration and state-output graph identification (hard)
• II.G: H-graph Hamiltonian generates Z=i exp(-2alpha G): Self-adjoint multimode squeezing generator and its unitary evolution on oscillator L2 (hard)
• II.H: complex nullifiers and canonical annihilators: Closed nullifier/annihilator operators, common CCR domain, and full Hilbert-space kernel uniqueness (hard)
• III.D–E: local quadrature measurements as phase shift and deletion: Quadrature probability-density instrument/disintegration with normalized conditional Gaussian states (hard)
• IV.D: claimed list and minimization of quarter-turn error values: A valid scope restriction and definition of n in Eq. (4.18) (source-ambiguity)
• IV.F: two quadratic parent Hamiltonians: Two closed nonnegative quadratic parent Hamiltonians on the full oscillator space (hard)
• IV.F: H-graph as a coupled-oscillator potential ground state: Self-adjoint coupled-oscillator Hamiltonian and ground-state energy shift (hard)
• Appendix D: extension of the graph calculus to identical thermal symplectic eigenvalues: Operational ideal quadrature measurement on equal-temperature mixed oscillator Gaussian densities, with a normalized outcome law and conditional outputs (hard)

Selected references

• Graphical calculus for Gaussian pure states, arXiv:1007.0725v3, https://arxiv.org/abs/1007.0725v3

Motivation

We revisit and prove some convexity inequalities for trace functions conjectured in the earlier part I. The main functional considered is Φ_{p,q}(A_1,A_2,...,A_m) = (trace((\sum_{j=1}^m A_j^p)^{q/p}))^{1/q} for m positive definite operators A_j. In part I we only considered the case q=1 and proved the concavity of Φ_{p,1} for 0 < p \leq 1 and the convexity for p=2. We conjectured the convexity of Φ_{p,1} for 1< p < 2. Here we not only settle the unresolved case of joint convexity for 1 \leq p \leq 2, we are also able to include the parameter q\geq 1 and still retain the convexity. Among other things this leads to a definition of an L^q(L^p) norm for operators when 1 \leq p \leq 2 and a Minkowski inequality for operators on a tensor product of three Hilbert spaces -- which leads to another proof of strong subadditivity of entropy. We also prove convexity/concavity properties of some other, related functionals.

This mission is the statement-level formalization of A Minkowski Type Trace Inequality and Strong Subadditivity of Quantum Entropy II: Convexity and Concavity (arXiv:0710.4167v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1.1: convexity, concavity, and failure beyond p=2 (Theorem 1.1, PDF p. 2). 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

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

• Undefined p=0 endpoints in Theorem 1.1 and its repeated lemmas: A specified p=0 (and any q=0) extension of the rooted trace functionals. (source-ambiguity)
• Unnumbered extension of the matrix inequalities to separable Hilbert spaces: An audited extended-positive-form domain, spectral calculus and partial traces for separable tensor factors. (source-ambiguity)
• Theorem 1.3: Minkowski inequality on three separable factors, full scope: A common extended domain on which every nested partial trace and power in (1.7) is defined. (source-ambiguity)
• Unnumbered Lq(Lp) constructions: unrestricted infinite-dimensional domains: A specified operator ideal/vector space on which the decomposition and dilation expressions are finite norms. (source-ambiguity)
• Lemma 2.4: cited Ando convexity and Lieb concavity, literal singular domain: Singular negative-power operator perspectives with support conditions or extended-positive values. (source-ambiguity)
• Lemma 2.6: joint trace map, full printed domain: A singular inverse-factor trace functional with a specified support/extended-value convention. (source-ambiguity)
• Lemma 5.1: singular inverse-factor boundary: The singular boundary of the corrected trace perspective Tr A^p B^(1-p). (source-ambiguity)
• Lemma 5.2: claimed equivalence of trace and tensor convexity: A corrected scope for the claimed arbitrary-real equivalence of unweighted trace and operator tensor convexity. (source-ambiguity)

Selected references

• A Minkowski Type Trace Inequality and Strong Subadditivity of Quantum Entropy II: Convexity and Concavity, arXiv:0710.4167v3, https://arxiv.org/abs/0710.4167v3

Motivation

Macroscopic fields like electromagnetic, MHD, acoustic or gravitational waves are usually described by classical wave equations with possible additional damping terms and coherent sources. The aim of this paper is to develop a complete macroscopic formalism including random/thermal sources, dissipation and random scattering of waves by environment. The proposed reduced state of field (RSF) combines averaged field with the two-point correlation function called single-particle density matrix. The evolution equations for RSF is obtained by reduction of the generalized quasi-free dynamical semigroups describing irreversible evolution of bosonic quantum field and the definition of RSF's entropy follows from the von Neumann entropy of quantum field states. The presented formalism can be applied, for example, to superradiance phenomena and allows to unify the Mueller and Jones calculi in polarization optics.

This mission is the statement-level formalization of Quantum features of macroscopic fields. Entropy and dynamics (arXiv:1904.06170v1). 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 Positivity bounds the Stokes vector (§II, (2)–(3): Stokes positivity bound, PDF p. 2). 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

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

• §IV, after (31): maximum-entropy RSF representative: Normal full-Fock states with finite unbounded moments and extended entropy at fixed RSF (hard)
• §III, (19)–(22): additive expectations, covariance, and number normalization: Full-Fock unbounded additive expectation, SPDM reduction, and vacuum-fixing second quantization (hard)
• §III, (24): positivity of centered correlation: Actual full-density first and second moment reduction (hard)
• §III, following (24): pure RSF iff coherent field: Normal full-Fock density equality to the coherent rank-one projector (hard)
• §IV, (27)–(29): quasi-free realization and entropy: Countable-mode occupation density construction, zero modes, finite two-point forms, and entropy (hard)
• §IV, (30)–(31): Weyl displacement and entropy invariance: Concrete Weyl displacement of normal full-Fock densities with moment and entropy transport (hard)
• §IV, after (32): nonnegative entropy and pure-RSF zero set: Extended spectral entropy of the actual countable RSF correlation operator (hard)
• §V, after (33): claimed general CPTP semigroup: Conservative normal semigroup for the unbounded generator (33) (source-ambiguity)
• §V, (36)–(37): claimed exact reduction of (33): Consistent Hamiltonian, damping normalization and complex loss-matrix indices (source-ambiguity)
• §V, (38): preservation of coherent RSFs: Differentiable finite-mean RSF trajectories on invariant unbounded-operator domains (hard)
• §VI.A, (39)–(42): independent modes: Mode-diagonal scattering rather than commutation with a degenerate Hamiltonian (source-ambiguity)
• §VI.A, after (44): rotating-bath amplification: Strict pumping and nonzero initial amplitude with valid scalar mode equations (source-ambiguity)
• §VI.B, (45),(47): full-field Stokes–Jones reduction: Compatible reduction of multiple unresolved q modes (source-ambiguity)
• §VI.B, (46),(48): joint dynamics with the same rates: Common compatible absorption normalization in (46),(48) (source-ambiguity)

Selected references

• Quantum features of macroscopic fields. Entropy and dynamics, arXiv:1904.06170v1, https://arxiv.org/abs/1904.06170v1

Motivation

Lecture notes of a minicourse given at the Summer School on Large Coulomb Systems - QED in Nordfjordeid, 2003, devoted to representations of the CCR and CAR. Quasifree states, the Araki-Woods and Araki-Wyss representations, and the lattice of von Neumenn algebras in a bosonic/fermionic Fock space are discussed in detail.

This mission is the statement-level formalization of Introduction to representations of the canonical commutation and anticommutation relations (arXiv:math-ph/0511030v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Uniqueness of the irreducible one-degree Weyl representation (Introduction, unnumbered: uniqueness of the irreducible one-degree-of-freedom Weyl pair, 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

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

• unnumbered intro-CAR-UHF: Universal CAR C*-completion and the UHF(2^infinity) inductive limit (hard)
• unnumbered intro-infinite-inequivalence: Source scope/correction requiring independent review (source-ambiguity)
• unnumbered tensor-closure: Algebraic tensor of partial operators on completed Hilbert tensors (hard)
• Theorem 1: Real/complex trace-class affine space, trace-norm topology, finite-rank determinant normalization (hard)
• Theorem 3: Schrodinger Weyl operators on L2 of an arbitrary finite real vector space (hard)
• Theorem 4: Schrodinger Weyl operators on L2 of an arbitrary finite real vector space (hard)
• Theorem 5: Stone field generator with actual derivative domain and graph topology (hard)
• Theorem 7: Finite-dimensional metaplectic sign quotient and lift of the Weyl implementation (hard)
• Theorem 8: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 8: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 9: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 12: Source scope/correction requiring independent review (source-ambiguity)
• unnumbered full-tensor-algebra-claim: Source scope/correction requiring independent review (source-ambiguity)
• unnumbered gamma-closed-domains: Unbounded full-Fock sector tensor powers and graph-domain direct sums (hard)
• Theorem 13: Unbounded full-Fock sector tensor powers and graph-domain direct sums (hard)
• Theorem 14: Completed arbitrary-H symmetric tensor sector and the pure-power embedding (hard)
• Theorem 15: Finite-particle symmetric/antisymmetric tensor multiplication and sectorwise second quantizations (hard)
• Theorem 16: Canonical arbitrary-H Fock exponential unitary with closed-domain Gamma intertwiners (hard)
• Theorem 17: Actual homogeneous creation/annihilation operators and dGamma on the common finite-particle core (hard)
• Theorem 18: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 18: Actual homogeneous creation/annihilation operators and dGamma on the common finite-particle core (hard)
• Theorem 18: Actual homogeneous creation/annihilation operators and dGamma on the common finite-particle core (hard)
• Theorem 18: Actual homogeneous creation/annihilation operators and dGamma on the common finite-particle core (hard)
• Theorem 19: Canonical Fock tensor unitary, parity and quadratic-degree twist acting on actual creators (hard)
• Theorem 20: Canonical Fock tensor unitary, parity and quadratic-degree twist acting on actual creators (hard)
• unnumbered multiple-creation: Actual homogeneous creation/annihilation operators and dGamma on the common finite-particle core (hard)
• unnumbered bosonic-field-core: Bosonic field closure and Weyl exponential for arbitrary one-particle Hilbert space (hard)
• Theorem 21: Bosonic field closure and Weyl exponential for arbitrary one-particle Hilbert space (hard)
• Theorem 22: Two-particle Gaussian creation exponential and Fredholm normalization (hard)
• Theorem 23: Infinite-dimensional real/complex Bogolubov block operators and operator ideals (hard)
• Theorem 24: Actual infinite-dimensional Bogolubov implementers and projective/sign quotient maps (hard)
• Theorem 25: Infinite-dimensional real/complex Bogolubov block operators and operator ideals (hard)
• Theorem 25: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 26: Actual infinite-dimensional Bogolubov implementers and projective/sign quotient maps (hard)
• unnumbered positive-symplectic-form: Positive restricted symplectic map, inverse square roots and bosonic normal-ordered implementer (hard)
• Theorem 27: Positive restricted symplectic map, inverse square roots and bosonic normal-ordered implementer (hard)
• unnumbered fermionic-volume-parity: Arbitrary-H fermionic Fock fields and parity (hard)
• Theorem 28: Arbitrary-H fermionic Fock fields and parity (hard)
• Theorem 29: Two-particle Gaussian creation exponential and Fredholm normalization (hard)
• Theorem 30: Infinite-dimensional real/complex Bogolubov block operators and operator ideals (hard)
• unnumbered orthogonal-nondegenerate-hs: Infinite-dimensional real/complex Bogolubov block operators and operator ideals (hard)
• Proposition 1: restricted orthogonal group criteria: Infinite-dimensional real/complex Bogolubov block operators and operator ideals (hard)
• Theorem 31: Actual infinite-dimensional Bogolubov implementers and projective/sign quotient maps (hard)
• Theorem 32: Infinite-dimensional real/complex Bogolubov block operators and operator ideals (hard)
• Theorem 32: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 33: Actual infinite-dimensional Bogolubov implementers and projective/sign quotient maps (hard)
• Theorem 34: Actual infinite-dimensional Bogolubov implementers and projective/sign quotient maps (hard)
• Theorem 35: Source scope/correction requiring independent review (source-ambiguity)
• unnumbered wstar-predual: Sigma-weak topology, normal maps, genuine standard forms and modular operators (hard)
• unnumbered standard-form-properties: Sigma-weak topology, normal maps, genuine standard forms and modular operators (hard)
• unnumbered tomita-standard-form: Sigma-weak topology, normal maps, genuine standard forms and modular operators (hard)
• unnumbered kms-invariance-uniqueness: Normal states with sigma-weak continuity, unbounded Gibbs spectral trace and strip-analytic KMS (hard)
• unnumbered type-I-normal-and-inner: Normal states with sigma-weak continuity, unbounded Gibbs spectral trace and strip-analytic KMS (hard)
• unnumbered type-I-HS-standard: Sigma-weak topology, normal maps, genuine standard forms and modular operators (hard)
• unnumbered type-I-tensor-standard: Sigma-weak topology, normal maps, genuine standard forms and modular operators (hard)
• Theorem 36: Sigma-weak topology, normal maps, genuine standard forms and modular operators (hard)
• Theorem 38: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 39: Source scope/correction requiring independent review (source-ambiguity)
• unnumbered classical-quasifree: Arbitrary-dimensional isonormal Gaussian realization and L2 multiplication fields (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 40: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 40: Constructed Araki-Woods fields/algebras and modular interfaces (hard)
• Theorem 41: Covariance completion and constructed Araki-Woods target for quasi-free CCR realization (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 43: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 43: Constructed endpoint-safe Araki-Wyss fields/algebras and modular interfaces (hard)
• Theorem 44: Polar covariance complexification and actual doubled/mixed Araki-Wyss target (hard)
• Theorem 45: Constructed tracial and mixed full fermionic representations with modular data (hard)
• unnumbered general-quasifree-CAR: Polar covariance complexification and actual doubled/mixed Araki-Wyss target (hard)
• Theorem 46: Constructed tracial and mixed full fermionic representations with modular data (hard)
• unnumbered confined-trace-determinants: Confined full-Fock densities, trace determinants and Hilbert-Schmidt standard identification (hard)
• unnumbered confined-KMS: Source scope/correction requiring independent review (source-ambiguity)
• unnumbered confined-stationarity: Confined full-Fock densities, trace determinants and Hilbert-Schmidt standard identification (hard)
• Theorem 47: Confined full-Fock densities, trace determinants and Hilbert-Schmidt standard identification (hard)
• Theorem 48: Confined full-Fock densities, trace determinants and Hilbert-Schmidt standard identification (hard)
• unnumbered confined-intertwining: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 49: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 50: Source scope/correction requiring independent review (source-ambiguity)
• Theorem 53: Spectral/polar calculus for the generic closed real subspace graph parameters (hard)
• unnumbered closed-subspace-and-algebra-lattices: General topological closed-subspace lattice and concrete von Neumann bicommutant lattice package (hard)
• unnumbered field-algebra-closure: Actual Fock real-subspace von Neumann algebras and canonical graded tensor identification (hard)
• Theorem 54: Actual Fock real-subspace von Neumann algebras and canonical graded tensor identification (hard)
• Theorem 55: Actual Fock real-subspace von Neumann algebras and canonical graded tensor identification (hard)
• Theorem 56: Actual Fock real-subspace von Neumann algebras and canonical graded tensor identification (hard)
• unnumbered pauli-fierz-selfadjoint: Coupled full-Fock Pauli-Fierz operators, conjugate coupling transpose and standard dynamics (hard)
• Proposition 2: positive-density Pauli-Fierz interaction: Coupled full-Fock Pauli-Fierz operators, conjugate coupling transpose and standard dynamics (hard)
• Theorem 57: Coupled full-Fock Pauli-Fierz operators, conjugate coupling transpose and standard dynamics (hard)
• Theorem 58: Coupled full-Fock Pauli-Fierz operators, conjugate coupling transpose and standard dynamics (hard)
• Proposition 3: proposed Pauli-Fierz standard cone: Source scope/correction requiring independent review (source-ambiguity)
• Proposition 4: standard interaction and its modular conjugate: Coupled full-Fock Pauli-Fierz operators, conjugate coupling transpose and standard dynamics (hard)
• Theorem 59: Coupled full-Fock Pauli-Fierz operators, conjugate coupling transpose and standard dynamics (hard)
• Theorem 60: Coupled full-Fock Pauli-Fierz operators, conjugate coupling transpose and standard dynamics (hard)

Selected references

• Introduction to representations of the canonical commutation and anticommutation relations, arXiv:math-ph/0511030v2, https://arxiv.org/abs/math-ph/0511030v2

Motivation

Notions of a Gaussian state and a Gaussian linear map are generalized to the case of anticommuting (Grassmann) variables. Conditions under which a Gaussian map is trace preserving and (or) completely positive are formulated. For any Gaussian map an explicit formula relating correlation matrices of input and output states is presented. This formalism allows to develop the Lagrangian representation for fermionic linear optics (FLO). It covers both unitary operations and the single-mode projectors associated with FLO measurements. Using the Lagrangian representation we reduce a classical simulation of FLO to a computation of Gaussian integrals over Grassmann variables. Explicit formulas describing evolution of a quantum state under FLO operations are put forward.

This mission is the statement-level formalization of Lagrangian representation for fermionic linear optics (arXiv:quant-ph/0404180v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Occupation projectors have the FLO Gaussian integral representation (§VIII, Eq.(51): Lagrangian FLO measurement representation (seed paper result), PDF p. 11). 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

• Lagrangian representation for fermionic linear optics, arXiv:quant-ph/0404180v2, https://arxiv.org/abs/quant-ph/0404180v2

Motivation

The concept of reflection positivity has its origins in the work of Osterwalder--Schrader on constructive quantum field theory and duality between unitary representations of the euclidean motion group and the Poincare group. On the mathematical side this duality can be made precise as follows. If $\g$ is a Lie algebra with an involutive automorphism $τ$. Decompose $\g = \fh \oplus \fq = \ker(τ- \1) \oplus \ker(τ+ \1)$ into $τ$-eigenspaces and let $\g^c := \fh \oplus i \fq$. At the core of the notion of reflection positivity is the idea that this duality can sometimes be implemented on the level of unitary representations. The idea is simple on the Lie algebra level: Let $(π,\cH^0)$ be a representation of $\g$ where $π$ acts by skew-symmetric operators. Assume that there exists a unitary operator $J$ of order two such that $J πJ = π\circ τ$ and a $\g$-invariant subspace $\cK^0$ which is {\it $J$-positive}. Then complex linear extension leads to a representation of $\g^c$ on $\cK^0$ by operators which are skew-symmetric with respect to $h_J$, so that we obtain a "unitary" representation of $\g^c$ on the pre-Hilbert space $\cK_J^0 := \cK_J/{v \: \cK^0 \: h_J(v,v)=0}$. The aim of this article is twofold. First we discuss reflection positivity in an abstract setting using {\it reflection positive distributions} on the Lie group $G_τ=G\rtimes {1,τ}$ and {\it reflection positive distribution vectors} of a unitary representation of $G_τ$. Then we apply these ideas to the conformal group $\OO_{1,n+1}^+(\R)$ of the sphere $\bS^n$ as well as the the half-space picture mostly used in physics.

This mission is the statement-level formalization of Reflection Positivity and Conformal Symmetry (arXiv:1206.2039v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is OS quotient: induced star-semigroup contractions (Lemma 1.4, 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

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

• Example 1.6 (vector-valued GNS): operator-valued GNS construction with densely defined star action (hard)
• Proposition 1.11: canonical operator-valued GNS space and restriction unitary from its OS completion (hard)
• Corollary 1.12: scalar GNS reflection action with the unnormalized cyclic vector (hard)
• Remark 2.2: continuous functions and distributions: Lie-group LF test functions, modular convolution and continuous antidual distributions (hard)
• Remark 2.4 and (12)–(13): smoothing distribution vectors: Frechet smooth vectors, strong antidual and integrated smoothing action (hard)
• Theorem 2.6: distribution-vector equivariant embedding correspondence (hard)
• Proposition 2.8: completed covariance Hilbert space embedded in the strong distribution antidual (hard)
• Example 2.9: abelian spectral realization: tempered spectral covariance realization with compatible Fourier normalization (hard)
• Proposition 2.12: reflection-positive distributions and their canonical cyclic GNS vectors (hard)
• Lemma 2.13: regular radial-power distribution and positive-definite LF functional (hard)
• Example 2.14: homogeneous reflection-positive covariance: homogeneous covariance completion, distribution-vector injection and time reflection (hard)
• Proposition 3.1: finite positive operator-valued Borel measures and weak operator integration (hard)
• Remark 3.2(b): even extension and dilation: canonical strong endpoint extension and minimal unitary RKHS dilation (hard)
• Example 3.5: exponential covariance and rank-one OS space: Cauchy spectral GNS realization and rank-one OS identification (hard)
• Example 3.6(a): additive power covariance: additive radial-power covariance Hilbert completion and reflection-positive distribution (hard)
• Example 3.6(b): multiplicative reflection and character decomposition: multiplicative covariance action, cyclic distribution vector and character direct sum (hard)
• §3.3: reflection-positive finite-part extensions: finite-part regularization with real-power/log asymptotics and delta corrections (hard)
• Proposition 4.1: LF test convolution algebra on an open subsemigroup extended by zero (hard)
• Lemma 4.2: smooth semigroup distribution convolution on a neighborhood of closure(S) (hard)
• Lemma 4.3: antilinear distribution characters and smooth multiplicative representatives (hard)
• Lemma 4.4: L1 norm and modular sharp on the zero-extended LF test algebra (hard)
• Remark 4.6: bounded distribution representation: bounded nondegenerate distribution GNS representation and its kernel criterion (hard)
• Proposition 4.10: enveloping C-star algebra and topological Fourier-Laplace character spectrum (hard)
• Theorem 4.11: cone distribution spectral measure and surjective Plancherel intertwiner (hard)
• Example 4.12: three spectral specializations: three distributional Fourier-Laplace specializations with correct spectral domains (hard)
• Theorem 4.13: analytic representatives of one-bounded cone distributions and unique Laplace measure (hard)
• Remark 5.2: conformal kernel identities: Lorentz conformal action, stereographic surface measure and differential cocycle (hard)
• Remark 5.3: conformal Cayley transform: global conformal sphere Cayley involution and finite chart domain (hard)
• Lemma 5.5: normalized sphere surface measure and singular positive covariance measure (hard)
• Lemma 5.6: integrable singular spherical covariance operator on continuous functions (hard)
• Lemma 5.8: complementary-series Hilbert subspace of Radon measures and weighted push-forward action (hard)
• Remark 5.9: equivariant covariance map: computed spherical covariance map and its two weighted intertwining actions (hard)
• Remark 5.10: circle projective-invariance obstruction: smooth circle projective maps, kernel cocycles and fractional linear action (hard)
• Lemma 5.12: smooth complementary-series vectors, density inverse and strong-antidual transpose (hard)
• Proposition 6.5: conformal compression Olshanski cone, subgroup and Lie algebra decomposition (hard)
• Lemma 6.6: closed supported covariance-image subspace of the canonical complementary series (hard)
• Theorem 6.7: computed point-mass distribution vector and cyclic reflection-positive complementary series (hard)
• Remark 6.9: positive equator distributions: finite positive equator measure as a nonzero cyclic distribution vector (hard)
• §6.3: c-dual highest-weight representation: specific simply connected c-dual group and integrated highest-weight OS representation (hard)
• Theorem A.1: holomorphic kernels on complex Frechet manifolds and full real-form submanifolds (hard)

Selected references

• Reflection Positivity and Conformal Symmetry, arXiv:1206.2039v2, https://arxiv.org/abs/1206.2039v2

Motivation

We prove the security of the Bennett-Brassard (BB84) quantum key distribution protocol in the case where the source and detector are under the limited control of an adversary. Our proof applies when both the source and the detector have small basis-dependent flaws, as is typical in practical implementations of the protocol. We derive a general lower bound on the asymptotic key generation rate for weakly basis-dependent eavesdropping attacks, and also estimate the rate in some special cases: sources that emit weak coherent states with random phases, detectors with basis-dependent efficiency, and misaligned sources and detectors.

This mission is the statement-level formalization of Security of quantum key distribution with imperfect devices (arXiv:quant-ph/0212066v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Complementary measurement concentration for quantum coins (Lemma 1: complementary measurement concentration for quantum coins, PDF p. 11). 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 2 (seed headline): security of BB84 against weakly basis-dependent attacks: Operational BB84 security and achievable extraction for balanced, correlated device attacks (hard)
• Theorem 1: security against basis-independent attacks (reviewed Shor–Preskill result): Operational basis-independent BB84 extraction (hard)
• Theorem 3: individual source flaws with basis-independent detector: Product source preparation from root fidelity plus operational extraction (hard)
• Lemma 3: weak individual oblivious Fred maps are balanced: Completed Hilbert tensor product of individual controlled local isometric dilations (hard)
• Theorem 4: entanglement-based security for individual oblivious flaws: Individual oblivious entanglement-based protocol and extraction (hard)
• Theorem 5: individually misaligned source and detector: Phase-fixed individual axis rotations and operational BB84 extraction (hard)
• Unnumbered worst-case misalignment estimate, eqs.(40)–(43): Allowed SU(2) axis rotations with worst-case attainment and their coin experiment (hard)
• Lemma 5: simultaneous individual generic source and detector flaws: Sequential general source-purification/Eve/product-squash coin construction (hard)
• Unnumbered generic-device security consequence of Lemma 5: Generic simultaneous imperfect-device operational extraction (hard)
• Unnumbered simple tagged-signal security rate, eq.(45): Classical-subset restricted coin attack and CSS extraction (hard)
• Theorem 6: operational extraction against tagging: Operational all-compatible-attack extraction from constructed classical-subset tagged states (hard)
• Unnumbered application: phase-randomized weak coherent sources and quadratic loss scaling: Phase-randomized photon source linked to detection, tagging and operational extraction (hard)
• Unnumbered coherent-superposition tagging extension via Theorem 2: Coherent physical tagging isometry with retained qutrit labels and security (hard)
• Unnumbered counterexample: small mean phase/bit gap does not imply security: Concrete global revelation source, attack, and key-information law (hard)
• Unnumbered adversarial detector erasure rate, eqs.(54)–(57): Basis-dependent erasure mask experiment and operational CSS rate (hard)
• Theorem 7: random losses followed by adversarial basis-dependent detector losses: Random thinning followed by adversarial thinning and detected-key extraction (hard)
• Unnumbered refined phase-error inference for random basis-dependent losses: Separate-basis verification and complementary phase-error inference after random thinning (hard)

Selected references

• Security of quantum key distribution with imperfect devices, arXiv:quant-ph/0212066v3, https://arxiv.org/abs/quant-ph/0212066v3

Motivation

We present a polynomiality property of the Littlewood-Richardson coefficients c_{λμ}^ν. The coefficients are shown to be given by polynomials in λ, μand νon the cones of the chamber complex of a vector partition function. We give bounds on the degree of the polynomials depending on the maximum allowed number of parts of the partitions λ, μand ν. We first express the Littlewood-Richardson coefficients as a vector partition function. We then define a hyperplane arrangement from Steinberg's formula, over whose regions the Littlewood-Richardson coefficients are given by polynomials, and relate this arrangement to the chamber complex of the partition function. As an easy consequence, we get a new proof of the fact that c_{NλNμ}^{Nν} is given by a polynomial in N, which partially establishes the conjecture of King, Tollu and Toumazet that c_{NλNμ}^{Nν} is a polynomial in N with nonnegative rational coefficients.

This mission is the statement-level formalization of A polynomiality property for Littlewood-Richardson coefficients (arXiv:math/0308101v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 4.1: polynomiality on the Littlewood–Richardson complex (seed headline) (Theorem 4.1: polynomiality on the Littlewood–Richardson complex (seed headline), PDF p. 10). 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:

• Section 5 complete 18-row table: A certified corrected complete 18-row maximal-cone polynomial table for the actual LR_3 complex. (source-ambiguity)

Selected references

• A polynomiality property for Littlewood-Richardson coefficients, arXiv:math/0308101v2, https://arxiv.org/abs/math/0308101v2

Motivation

We study non-equilibrium statistical mechanics of a Gaussian dynamical system and compute in closed form the large deviation functionals describing the fluctuations of the entropy production observable with respect to the reference state and the non-equilibrium steady state. The entropy production observable of this model is an unbounded function on the phase space, and its large deviation functionals have a surprisingly rich structure. We explore this structure in some detail.

This mission is the statement-level formalization of Entropic fluctuations in Gaussian dynamical systems (arXiv:1509.03244v1). 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 Theorem 2.4 (1)–(3),(5): reference-state fluctuations and strong law (Theorem 2.4 (1)–(3),(5): reference-state fluctuations and strong law, 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

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

• Theorem 2.4 (4): printed reference-state CLT: Printed all-Borel-set CLT with permitted zero asymptotic variance (source-ambiguity)
• Theorem 2.5 (all three clauses): Holomorphic bounded-operator functional calculus and extended endpoint subsequence domains (hard)
• Theorem 2.6 (5): printed NESS CLT: Printed NESS all-Borel-set CLT at zero variance (source-ambiguity)
• Theorem 2.7 (both clauses): Convergent extended endpoints of nonsymmetric NESS domains and the concrete operator E (hard)
• §2.6 Case 1: dissipating trace-class perturbations: Dissipating precision perturbation domains and the concrete E invariance (hard)
• §2.6 Case 2: printed δ^(λP)→∞ subclaim: False numerical delta-from-(10) divergence for general conserved coercive P (source-ambiguity)
• §3.1: rank-one toy model, explicit cumulants and rate functions: Purely AC spectral measure of the complexified skew-adjoint generator and complete toy-model domain branches (hard)
• §3.2 equation (32): homogeneous-crystal entropy production and analytic germ: Concrete harmonic-crystal operator and three-temperature Dirichlet Gaussian reference (hard)
• §3.2 Remark 1: temperature dependence of minimal domains: Temperature-dependent concrete crystal families and actual endpoint collapse/exhaustion (hard)
• §3.2 Remark 3: constructed perturbed reference attains J_o: Concrete Neumann half-crystal reference and inconsistent printed perturbation block (source-ambiguity)
• §3.2 Remark 5: equilibrium can retain nontrivial fluctuations: Equilibrium crystal families and subsequential piecewise-linear rate endpoints (hard)
• §3.2 Remark 6: inhomogeneous-crystal hypotheses: Bounded variable-coefficient Jacobi model, complex spectral AC and source reference construction (hard)
• §3.2 Remark 6: unspecified scattering-data formulas: Unspecified quantitative scattering-data formula of Remark 6 (source-ambiguity)

Selected references

• Entropic fluctuations in Gaussian dynamical systems, arXiv:1509.03244v1, https://arxiv.org/abs/1509.03244v1

Motivation

Diminishing stepsizes, $\gamma^\nu\to 0$ with $\sum_\nu\gamma^\nu=\infty$, are the standard device of stochastic and distributed optimization: they need no line search, no function evaluations and no global information. For unconstrained or convex problems their convergence theory is classical. For nonconvex problems with nonconvex constraints it was missing: SQP and penalty methods rely on line searches on a merit function or on updates of a penalty parameter, and neither fits a method that only takes prescribed steps.

Facchinei, Kungurtsev, Lampariello and Scutari (arXiv:1709.03384, Mathematics of Operations Research 2021) give the first general convergence analysis of such a method. The algorithm is penalty-free; the classical exact penalty function enters only the proof, hence the name ghost penalty. The same device yields iteration-complexity bounds for SQP-type methods in later sections of the paper. This mission formalizes the convergence theorem (Theorem 1) and the chain of lemmas the paper proves it with.

Setting

The problem is

$$\text{(P)}\qquad \min_x\ f(x)\quad\text{s.t.}\quad g(x)\le 0,\ \ x\in K,$$

where $K\subseteq\mathbb R^n$ is nonempty, closed and convex and $f:\mathbb R^n\to\mathbb R$, $g:\mathbb R^n\to\mathbb R^m$ are $C^{1,1}$ (continuously differentiable with locally Lipschitz gradients) on an open set containing $K$. Nothing else is assumed: (P) may be infeasible, and no constraint qualification is imposed.

Write $\max_i\{g_i(x)_+\}$ for the largest constraint violation, $e$ for the vector of ones, and $N_C(y)$ for the normal cone of a convex set $C$ at $y$. The multiplier sets

$$M_1(x)=\{\xi\in N_{\mathbb R^m_-}(g(x)):\ 0\in\nabla f(x)+\nabla g(x)\xi+N_K(x)\},$$ $$M_0(x)=\{\xi\in N_{\mathbb R^m_-}(g(x)-\max_i\{g_i(x)_+\}e):\ 0\in\nabla g(x)\xi+N_K(x)\}$$

define three kinds of points $\hat x\in K$ (Definition 1): KKT ($g(\hat x)\le0$, $M_1(\hat x)\ne\emptyset$), Fritz-John ($g(\hat x)\le 0$, $M_0(\hat x)\ne\{0\}$) and External Stationary (some $g_i(\hat x)>0$, $M_0(\hat x)\ne\{0\}$). Any of the three is a generalized stationary point. The eMFCQ at $\hat x$ is $M_0(\hat x)=\{0\}$ (Definition 2).

At $x\in K$ the method solves the strongly convex subproblem

$$(\mathrm P_x)\qquad \min_d\ \tilde f(d;x)\quad\text{s.t.}\quad \tilde g(d;x)\le\kappa(x)e,\ \ \|d\|_\infty\le\beta,\ \ d\in K-x,$$

with a strongly convex surrogate $\tilde f$ of $f$ and convex surrogates $\tilde g_i$ of $g_i$ that agree with $f$, $g$ to first order at $d=0$ (Assumption A), and the enlargement

$$\kappa(x)=(1-\lambda)\max_i\{g_i(x)_+\}+\lambda\min_d\Big\{\max_i\{\tilde g_i(d;x)_+\}:\ \|d\|_\infty\le\rho,\ d\in K-x\Big\},\qquad \lambda\in(0,1),\ \rho\in(0,\beta),$$

which keeps $(\mathrm P_x)$ feasible. Its unique solution is $d(x)$. Algorithm 1 starts at $x^0\in K$, stops if $x^\nu$ is generalized stationary, and otherwise sets $x^{\nu+1}=x^\nu+\gamma^\nu d(x^\nu)$ with $\gamma^\nu\in(0,1]$, $\gamma^\nu\to0$, $\sum\gamma^\nu=\infty$. The quantity $\theta(x)=\max_i\{g_i(x)_+\}-\kappa(x)$ measures stationarity for the violation problem $\min_{x\in K}\max_i\{g_i(x)_+\}$. Assumption B asks that $d(\cdot)$ be Hölder continuous on compact subsets of $K$.

Formalization targets

Goal: Theorem 1

For every non-terminating run of Algorithm 1 under Assumption A, every iterate lies in $K$, and either $\{x^\nu\}$ is unbounded, or

$$\exists\,\hat x\in\operatorname{Lim}\{x^\nu\}:\ \hat x\ \text{generalized stationary, and KKT if the eMFCQ holds at }\hat x,$$

and, if moreover Assumption B holds and the eMFCQ holds at every limit point, every limit point is a KKT point of (P).

Milestones

In proof order: well-posedness of $(\mathrm P_x)$; Lemma 1 (i)–(iii) on the set $\beta\mathbb B^n_\infty\cap(K-x)$ and its normal cone; Proposition 2 (continuity of $\kappa$); Lemma 2 (the three cases at a point of $K$); Proposition 3 ($\theta$ as a stationarity measure, and $\theta(x)\le\|\nabla g(x)\|_\infty\|d(x)\|$); Proposition 4 (continuity of $d$ under the eMFCQ); Proposition 6 (locally bounded multipliers of $(\mathrm P_x)$ under Slater's condition); the KKT property of $d(x)$ at non-stationary points; inequality (22); the ghost-penalty estimate (25)

$$W(x+\gamma d;\varepsilon)-W(x;\varepsilon)\le\gamma\nabla f(x)^Td-\tfrac{\gamma}{\varepsilon}\theta(x)+\tfrac{\gamma^2}{2}\big(L_{\nabla f}+\tfrac{\max_iL_{\nabla g_i}}{\varepsilon}\big)\|d\|^2,\qquad W(x;\varepsilon)=f(x)+\tfrac1\varepsilon\max_i\{g_i(x)_+\};$$

and (35), $\|d(x^\nu)\|\to0$ under Assumption B.

Significance

Theorem 1 shows that a penalty-free, line-search-free SQP-type method converges in the weakest sense available without assumptions (to generalized stationary points), and to KKT points under the standard constraint qualification. It is the base case for the paper's complexity results (Theorems 2–4, which reuse inequality (25)) and covers the classical SQP subproblem as well as convex models that keep part of the problem's structure.

The result is proved in the paper; nothing here is open mathematics. No part of it has a machine-checked proof. Formalizing it requires a library of finite-dimensional variational analysis that Mathlib lacks: set-valued continuity, normal-cone calculus for intersections, parametric stability of convex programs, and Lagrange multipliers for convex problems with an abstract set constraint.

Difficulty

The first idea is to use the penalty function $W(\cdot;\varepsilon)=f+\tfrac1\varepsilon\max_i\{g_i(\cdot)_+\}$ as a Lyapunov function for one fixed $\varepsilon$. This fails: whether $d(x^\nu)$ decreases $W(\cdot;\varepsilon)$ depends on the size of the multipliers of the subproblem $(\mathrm P_{x^\nu})$, which may be unbounded along the run, so no single $\varepsilon$ need work for every iterate, and the algorithm never computes one. The analysis must therefore control the multipliers of a family of parametric convex programs, which brings in the stability of their feasible sets, solutions and multipliers as the base point moves. A second difficulty is part (ii): diminishing stepsizes alone only yield $\liminf_\nu\|d(x^\nu)\|=0$, not a limit, which is why Assumption B is needed. Each parametric statement (Lemma 1, Propositions 2, 4, 6) needs variational-analysis infrastructure that Mathlib does not have.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n) (Euclidean norm), constraints are indexed by Fin m, multipliers are functions Fin m → ℝ. The box $\|d\|_\infty\le\beta$ is coordinatewise, $\max_i\{g_i(x)_+\}$ is a real supremum over Fin m (zero when $m=0$), and $K-x$ is $\{d: x+d\in K\}$. Normal cones of $K$ and of $\beta\mathbb B^n_\infty\cap(K-x)$ are the published normalCone, used only at points of the set; $N_{\mathbb R^m_-}$ includes the feasibility condition. The solution map $d$ is a hypothesis characterised by minimality over $\widetilde X(x)$ for $x\in K$; a milestone proves that such a map exists and is unique on $K$. Strong convexity follows Mathlib's StrongConvexOn convention $(c/2)t(1-t)\|d-d'\|^2$. Assumption A's convexity requirements A1 and A5 are imposed on the box $\beta\mathbb B^n_\infty$ instead of the open set $O_d$, a weaker hypothesis. The run is infinite: no iterate is generalized stationary, which is the case Theorem 1 addresses. Limit points are MapClusterPt.

The goal cannot be satisfied vacuously: the blanket assumptions, Assumption A and the solution-map hypothesis hold together in concrete instances (for example the classical surrogates (10)), stepsizes $1/(\nu+1)$ satisfy (3), and $0\in M_0(x)$ for all $x\in K$, so FJ and ES require a nonzero multiplier.

Reusable infrastructure includes sequential outer and inner semicontinuity of set-valued maps, normal-cone sum rules under a constraint qualification, Slater-based KKT existence and multiplier bounds for convex programs with a set constraint, and the descent lemma along a segment. Contributions that prove any milestone, or that add these general tools as separate lemmas, are welcome.

Selected references

• F. Facchinei, V. Kungurtsev, L. Lampariello, G. Scutari, Ghost Penalties in Nonconvex Constrained Optimization: Diminishing Stepsizes and Iteration Complexity, arXiv:1709.03384v3, 2020; Mathematics of Operations Research, 2021. https://arxiv.org/abs/1709.03384v3
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309

Motivation

Matrix scaling asks for positive diagonal matrices that turn a nonnegative matrix into one with prescribed row and column sums. The Sinkhorn algorithm, which alternately normalizes rows and columns, is the standard method; it appears in statistics (iterative proportional fitting), entropic optimal transport, and combinatorial optimization. For the doubly stochastic target, a classical fact connects scaling to matching theory: an $n\times n$ nonnegative matrix can be scaled arbitrarily close to doubly stochastic if and only if its support graph has a perfect matching.

Linial, Samorodnitsky and Wigderson (Combinatorica, 2000) showed that $O(n^2\log n)$ Sinkhorn iterations decide whether a bipartite graph has a perfect matching. A decision is not a certificate: when the answer is "no", the algorithm does not exhibit a reason. Hayashi, Hirai and Sakabe (arXiv:2204.07425v2, 2023; Mathematics of Operations Research, 2024) show that the scaling vectors themselves contain the certificate: sorting them yields a Hall blocker, a set of rows with fewer neighbours than elements. The rounding from sorted scaling vectors to a blocker is essentially that of Franks, Soma and Goemans (arXiv:2207.08311, Lemma 3.3); the new contribution is the iteration bound.

Setting

Let $A=(A_{ij})$ be a nonnegative real $n\times n$ matrix with no zero row and no zero column. Its support graph $G=G(A)$ is the bipartite graph with rows $U$ and columns $V$, $|U|=|V|=n$, in which row $i$ and column $j$ are adjacent iff $A_{ij}>0$. For a set $X$ of rows, $\Gamma(X)$ is the set of columns adjacent to some row of $X$. A Hall blocker is a set $X$ of rows with $|\Gamma(X)|<|X|$. Let $m$ be the number of positive entries of $A$, $A_{\max}$ its largest entry and $A_{\min}$ its least positive entry.

With marginals $(r,c)=(\mathbf 1,\mathbf 1)$ the normalization vectors are

$$R(y)_i=\frac{1}{\sum_j A_{ij}y_j},\qquad C(x)_j=\frac{1}{\sum_i A_{ij}x_i}.$$

The algorithm Sinkhorn & Sorting Scaling Vectors (§4.1 of the paper) is:

• Step 0. $x=y:=\mathbf 1$, then $y\leftarrow C(x)$.
• Step 1. Repeat $\ell$ times: $x\leftarrow R(y)$, $y\leftarrow C(x)$.
• Step 2. Sort $x_{i_1}\ge\dots\ge x_{i_n}$ and $y_{j_1}\le\dots\le y_{j_n}$, choose $k^*$ with $(x_{i_{k^*}}y_{j_{k^*}})^n\ge x_1\cdots x_ny_1\cdots y_n$, and output $\{i_1,\dots,i_{k^*}\}$.

The analysis uses the capacity $\kappa(x,y)=\sum_{i,j}A_{ij}x_iy_j\big/\big(\prod_ix_i^{r_i/R}\prod_jy_j^{c_j/C}\big)$ for general positive marginals $r,c$ with $R=\sum r_i$, $C=\sum c_j$, and the KL divergence $D(p\|q)=\sum_ip_i\log(p_i/q_i)$ of nonnegative vectors, with $0\log\frac0x=0$ and $x\log\frac x0=\infty$.

Formalization targets

Goal: Theorem 4.1

If $G$ has no perfect matching and

$$\ell\ \ge\ \frac14\,n^2\log\frac{mA_{\max}}{A_{\min}},$$

then step 2 has an output, and every output of step 2 (every tie-break in the two sorts, every admissible $k^*$) is a Hall blocker. The threshold is the paper's exact constant; $\log$ is natural.

Milestones

1. Lemma 1.1, Pinsker's inequality for nonnegative vectors with equal sums: $D(p\|q)\ge\|p-q\|_1^2/(2p([n]))$.
2. Lemma 2.2: for every scaling $\tilde A$, $\|\tilde A\mathbf 1-r\|_1+\|\tilde A^\top\mathbf 1-c\|_1\ge2r(X)+2c(Y)-R-C$ for every stable set $X\sqcup Y$.
3. Hall's theorem (already proved on the platform, referenced).
4. Lemma 2.4: $\log\kappa(x',y')-\log\kappa(x,y)=-D(r\|p)/R-D(c\|q)/C$ for one row-and-column normalization.
5. §2.1: $R(y)$ and $C(x)$ minimize $\kappa$ in their block.
6. The decrement $\log\kappa(x',y')-\log\kappa(x,y)\le-4/n^2$ when $G$ has no perfect matching.
7. The iteration bound $\log\kappa\le\log(mA_{\max})-4\ell/n^2$, hence $\kappa\le A_{\min}$ at the threshold.
8. Lemma 2.5: unboundedness criterion for an unconstrained geometric program.
9. Theorem 2.3 (2): approximate scalability iff $\inf\kappa>0$.
10. Corollary 2.6, both sentences: non-scalability iff some $\kappa(x,y)\le A_{\min}$, and then $x_ky_\ell<\prod_ix_i^{r_i/R}\prod_jy_j^{c_j/C}$ on every edge.
11. Step 2 is well posed: an admissible $k^*$ exists.
12. Rounding: under the strict edge inequality, every step-2 output $X$ satisfies $\Gamma(X)\subseteq\{j_1,\dots,j_{k^*-1}\}$.

Significance

A Hall blocker is a short, independently checkable proof that no perfect matching exists. Theorem 4.1 shows that a first-order scaling method, run for $O(n^2\log(mA_{\max}/A_{\min}))$ iterations, produces one by a sort, matching (up to constants) the known iteration bound for the scalable case. It turns Sinkhorn into a certifying algorithm for bipartite matching and illustrates a general principle: iterates of a geometric program that drift to $-\infty$ can be rounded to a combinatorial separating certificate.

The result is proved in the paper; none of it is formalized. The platform has Hall's theorem (from Mathlib) but no matrix scaling, no Sinkhorn iteration in this orientation, no capacity, and no vector form of Pinsker's inequality. This mission formalizes the complete proof chain of Theorem 4.1, including the cited results it relies on (Pinsker's inequality, Theorem 2.3 (2) of Rothblum and Schneider).

Difficulty

The natural first attempt, proving that the scaled matrix approaches a block structure and reading the blocker off the limit, does not give an iteration count: the Sinkhorn limit for non-scalable matrices is reached only asymptotically. The proof instead needs a quantitative potential argument. The central step is the per-iteration decrement $4/n^2$: it requires the exact KL identity of Lemma 2.4, Pinsker's inequality in its unnormalized form, and the observation (Lemma 2.2) that a Hall blocker keeps the $\ell_1$ marginal error at least $2$ at every iterate. The second difficulty is the rounding: the analytic condition $\kappa\le A_{\min}$ must be turned into a strict inequality on every edge (Lemma 2.5 / Corollary 2.6), and then into a set inclusion by a sorting argument that has to work for every tie-break.

Formalization scope

Matrices are Matrix ι κ ℝ over finite index types; in the square setting of §4 rows and columns are Fin n (0-based), so $k^*$ is encoded as k = k* − 1 and the output as σ '' {0, …, k}. A perfect matching is a permutation $\sigma$ with $A_{i\sigma(i)}>0$. The standing assumptions are hypotheses: no zero row or column, positive marginals, $R=C$ in §2.1, $(r,c)=(\mathbf 1,\mathbf 1)$ and $n=|U|=|V|$ in §4. The $m$ of the threshold is numEdges A, the number of positive entries, distinct from §2's column count. $\log$ is Real.log. Step 2 is nondeterministic in the paper; it is formalized as a relation IsStep2Output, and the goal asserts both that an output exists and that every output is a Hall blocker. The existence clause rules out a vacuous goal. The KL divergence is EReal-valued, with $\top$ exactly when some $q_i=0<p_i$, and has no mass-correction term. Approximate scalability is stated with the $\ell_1$ norm. Corollary 2.6 is stated for matrices with at least two positive entries; for a $1\times1$ matrix the printed statement fails, and Lemma 2.5, from which it is derived, assumes at least two terms.

Needed infrastructure: weighted AM–GM and log-sum-exp estimates, Pinsker's inequality for finite vectors, and a sorting lemma for products. The definitions of $\kappa$, $D$, $R(y)$, $C(x)$ and the Sinkhorn iteration are reusable for other matrix-scaling results (for instance Theorem 4.3 of the same paper). Contributions are welcome on any milestone, and on a direct proof of Theorem 2.3 (2).

Selected references

• K. Hayashi, H. Hirai, K. Sakabe, Finding Hall blockers by matrix scaling, arXiv:2204.07425v2, 2023; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2204.07425
• N. Linial, A. Samorodnitsky, A. Wigderson, A deterministic strongly polynomial algorithm for matrix scaling and approximate permanents, Combinatorica 20, 2000. https://doi.org/10.1007/s004930070007
• U. G. Rothblum, H. Schneider, Scalings of matrices which have prespecified row sums and column sums via optimization, Linear Algebra and its Applications 114/115 (1989), 737–764 (reference [27] of the paper; Theorems 2.1 and 2.3 there). https://arxiv.org/abs/2204.07425
• C. Franks, T. Soma, M. X. Goemans, Shrunk subspaces via operator Sinkhorn iteration, SODA 2023. https://arxiv.org/abs/2207.08311
• T. M. Cover, J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006 (Lemma 11.6.1). https://doi.org/10.1002/047174882X
• P. Hall, On representatives of subsets, J. London Math. Soc. 10, 1935. https://doi.org/10.1112/jlms/s1-10.37.26

Investment under the prospect of a breakthrough

Real-options theory, as in Dixit and Pindyck (1994), asks when a firm should sink a cost into a project whose value follows a diffusion. The standard answer invests the first time the state exceeds a threshold, so investment is procyclical. Décamps, Gensbittel and Mariotti (2021) add a feature of research-intensive industries: a better technology arrives when market conditions first exceed an unknown level. Waiting then carries an option on the breakthrough, and the firm's stopping rule changes qualitatively. The firm invests in the available technology after conditions have fallen enough from a maximum, that is, in busts.

The problem also sits in the line of optimal stopping problems for the running maximum of a diffusion, from Shepp and Shiryaev (1993) and Peskir (1998). There a free boundary is selected by a growth condition or by the maximality principle. Here neither applies, and a limit condition selects it.

Setting

Let $X$ be a one-dimensional diffusion on the interval $\mathcal I=(\alpha,\beta)$, $-\infty\le\alpha<\beta\le\infty$, solving

$$dX_t=\mu(X_t)\,dt+\sigma(X_t)\,dW_t,$$

with $\mu,\sigma$ continuous, $\sigma>0$ on $\mathcal I$, and natural endpoints. Fix a discount rate $r>0$. A threshold $Y$ with density $f>0$ on $\mathcal I$ is independent of $X$. The decision maker observes $X$ only and picks a stopping time $\tau$ of the right-continuous filtration of $X$. If $\tau$ comes before $\tau_{X\ge Y}=\inf\{t:X_t\ge Y\}$, the reward is $e^{-r\tau}R(X_\tau)$. Otherwise it is $e^{-r\tau_{X\ge Y}}G(X_{\tau_{X\ge Y}})$. The value $\bar V(x)$ is the supremum over $\tau$ of the expected reward, and rewards at $\tau=\infty$ are $0$.

Assumptions A1–A8 bound the growth of $R,G$, give $\mathcal LR-rR$ a single sign change, make $G$ dominate the stand-alone value $V_R$, and make $\mathcal LG-rG\le0$, where $\mathcal L$ is the generator of $X$. The threshold $x_R$ is the point with $\{V_R=R\}=[x_R,\beta)$.

With the running maximum $M_t=m\vee\sup_{s\le t}X_s$, Proposition 1 gives $\bar V(x)=V(x,x)+F(x)G(x)$, where

$$V(x,m)=\sup_{\tau}\mathbf E_{x,m}\Big[[1-F(M_\tau)]e^{-r\tau}R(X_\tau)+\int_0^\tau e^{-rt}G(M_t)f(M_t)\,dM_t\Big]$$

on $J=\{(x,m)\in\mathcal I^2:m\ge x\}$ and $F$ is the distribution function of $Y$. The variational system (VS) seeks a level $\underline m$, a boundary $b$ and a function $W$ with $b(\underline m)=x_R$, $x_R\le b(m)<m$, $b(m)\to\beta$; $\mathcal LW-rW=0$ off the stopping region $S=\{\underline m\le m,\ x_R\le x\le b(m)\}$; value matching and smooth fit along $b$; the Neumann condition $\partial_mW(m,m)=-f(m)G(m)$ at the diagonal; and $W\to0$ at $\alpha$.

Formalization targets

Goal: Theorem 1

For every model satisfying A1–A8 and every threshold $x_R$, (VS) has a unique solution $(\underline m,b,W)$ in the class $(x_R,\beta)\times C^1([\underline m,\beta))\times\mathcal V$. Moreover $b$ is strictly increasing, $W=V$, and

$$\tau_b=\inf\{t\ge0:M_t\ge\underline m,\ x_R\le X_t\le b(M_t)\}$$

is optimal. The goal keeps $\mu,\sigma,R,G,f$ general: no geometric Brownian motion, no Lipschitz coefficients, no finite endpoints.

Milestones

In proof order: the classical facts (12)–(18); the stand-alone problem and Lemma 1; the change of variables, Lemma 2; Proposition 1; the ODE analysis, Lemmas 3–6; the explicit $W_b$, Lemma 7 and Proposition 2; the verification bounds, Lemmas 8–9 and Corollaries 1–2; superharmonicity, Lemma 10; Lemma 11; and Proposition 3.

Significance

The result gives a complete description of investment under the threat of obsolescence, including the countercyclical form of the optimal rule. It yields comparative statics that the paper develops in §9, such as the behaviour of the value in $m$.

The theorem is proved on paper and, as of this mission, has no machine-checked proof. The mission also adds general assets to the platform: a diffusion on an interval with natural endpoints, and a stopping problem with an integral against the running maximum. Its $x_R$ needs a correction. The paper says that A3 alone gives a threshold, which fails for $R<0$ (geometric Brownian motion with $r=2$ and $R(x)=-x^2/(1+x^6)$ has $V_R\equiv0$). A threshold exists exactly when $R>0$ somewhere, so the goal assumes one, and the milestone on the stand-alone problem proves the equivalence.

Difficulty

The obvious route is to guess the boundary, solve its ODE from a starting point, and verify. It fails at the first step, because the ODE $b'=E(b,m)$ has a vector field that explodes at the diagonal and has no continuous extension there, so Cauchy–Lipschitz gives no global solution. The endpoint $\underline m$ is not given either: the maximality principle does not apply, and the set of admissible endpoints is first obtained only as a nonempty compact interval, by a retraction argument of Ważewski type. Uniqueness of the solution of (VS) then comes only from the verification. Verification needs Itô's formula across a kink along a curve, since $W$ is not $C^1$ on the segment $J_{\underline m}$.

Formalization scope

The canonical space is $C([0,\infty),\mathcal I)$ with endpoints in EReal, and $X$ is the coordinate process. Stopping times are those of the right-continuous natural filtration, not augmented, valued in WithTop ℝ≥0. The laws $(P_x)$ are weak solutions of the SDE on the canonical space, with the Itô integral given by the published EthierKurtz.HasBrownianItoIntegral. Natural endpoints are the published Feller tests EthierKurtz.diffusionBoundaryTests, both infinite. Rewards at $\tau=\infty$ follow Footnote 2 of the paper. The measure $dM$ is the Stieltjes measure of the continuous nondecreasing path.

$C^1$ and $C^{2,1}$ on non-open sets are read as slice derivatives with continuous extensions. "Piecewise $C^2$" is read as $C^2$ off a set with no accumulation point in $\mathcal I$. Uniqueness in the goal is on $[\underline m,\beta)$ for $b$ and on $J$ for $W$, and the solution predicate does not include strict monotonicity. Real suprema and Bochner integrals have junk values, so $V$ is pinned by IsLUB in the goal and by the integrability clause of Proposition 1. A solution that omits uniqueness, or that adds monotonicity to the class, would be a weaker theorem.

A complete development needs the Feller classification, the strong Markov property, the hitting-time transform, Itô's formula for $C^{2,1}$ functions with a kink along a monotone curve, and a retraction argument for ODEs with a singular boundary. The first four are reusable. Contributions on any of them, or on the purely analytical Lemmas 3–9, are welcome. Appendix C's verification of the example is not part of this mission.

Selected references

• J.-P. Décamps, F. Gensbittel, T. Mariotti, Investment Timing and Technological Breakthroughs, arXiv:2106.05112v1, 2021. https://arxiv.org/abs/2106.05112
• A. Dixit, R. Pindyck, Investment under Uncertainty, Princeton University Press, 1994. https://doi.org/10.1515/9781400830176
• G. Peskir, Optimal stopping of the maximum process: the maximality principle, Annals of Probability 26, 1998. https://doi.org/10.1214/aop/1022855875
• L. Shepp, A. Shiryaev, The Russian option: reduced regret, Annals of Applied Probability 3, 1993. https://doi.org/10.1214/aoap/1177005355
• S. Dayanik, I. Karatzas, On the optimal stopping problem for one-dimensional diffusions, Stochastic Processes and their Applications 107, 2003. https://doi.org/10.1016/S0304-4149(03)00076-0
• G. Peskir, A change-of-variable formula with local time on curves, Journal of Theoretical Probability 18, 2005. https://doi.org/10.1007/s10959-005-3517-6

Motivation

The feedback arc set (FAS) problem asks, for a digraph $G=(V,A)$ with nonnegative integral arc weights $w$, for a set of arcs of minimum total weight whose deletion destroys every directed cycle. It is $NP$-hard, and it remains $NP$-hard on tournaments (Alon 2006; Charbit, Thomassé and Yeo 2007), where it models ranking from pairwise comparisons. A standard way to understand such a problem is through the integrality properties of its linear programming relaxation, which, by the theory of Grötschel, Lovász and Schrijver, also yields polynomial-time algorithms on the classes where those properties hold.

Two dual minimax relations come with the problem. Packing directed cycles against covering them by an FAS gives the notions cycle ideal and cycle Mengerian; packing FASs against the minimum weight of a cycle gives their blocker versions, FAS ideal and FAS Mengerian. The paper of Chen, Ding, Zang and Zhao (MOR 2024) characterizes the blocker versions for tournaments.

Timeline.

• 1976–1978: Lucchesi and Younger prove their minimax theorem for packing dicuts (J. London Math. Soc., 1978). Edmonds and Giles (1977) conjecture the dual statement for dijoins, which on planar digraphs says every planar digraph is FAS Mengerian.
• 1980: Schrijver refutes the Edmonds–Giles conjecture (Discrete Math., 1980); further counterexamples follow (Cornuéjols–Guenin 2002, Williams–Guenin).
• 1991: Applegate, Cook and McCormick, and independently Barahona, Fonlupt and Mahjoub, prove that every tournament on five vertices is cycle Mengerian.
• 2020: Chen, Ding, Zang and Zhao characterize cycle ideal and cycle Mengerian tournaments: both are equivalent to being Möbius-free (Theorem 1.1, refs. [11, 12] of the paper, J. Combin. Theory Ser. B 141 and 142, 2020).
• 2024: the same authors prove the blocker version, Theorem 1.2, formalized here.

Setting

A digraph $G=(V,A)$ has a finite vertex set $V$ and an arc set $A$ of ordered pairs; a tournament has precisely one arc between any two distinct vertices and no loops. A directed cycle is the arc set of a closed walk through $k\ge2$ distinct vertices. A set $F\subseteq A$ is a feedback arc set (FAS) if $G\setminus F$ has no directed cycle.

Let $N$ be the FAS-arc incidence matrix (one row per FAS) and $M$ the cycle-arc incidence matrix (one row per directed cycle). A polyhedron is integral if it is the convex hull of the integral vectors it contains. A system $Ax\ge b,\ x\ge0$ is totally dual integral (TDI) if for every integral $w$ for which $\min\{w^Tx: Ax\ge b,\ x\ge0\}$ is finite, the dual $\max\{y^Tb : y^TA\le w^T,\ y\ge0\}$ has an integral optimal solution. Then $G$ is

• FAS ideal if $\{x\ge0 : Nx\ge\mathbf 1\}$ is integral, and FAS Mengerian if $Nx\ge\mathbf1,\ x\ge0$ is TDI;
• cycle ideal and cycle Mengerian likewise with $M$ in place of $N$.

An FAS packing is a collection of FASs, repetition allowed, using each arc $e$ at most $w(e)$ times. Write $\lambda_w(G)$ for its maximum size and $\mu_w(G)$ for the minimum weight of a directed cycle. By the Edmonds–Giles theorem, $G$ is FAS Mengerian iff $\lambda_w(G)=\mu_w(G)$ for every $w\in\mathbb Z_+^A$.

A tournament is Möbius-free if it contains none of the four Möbius ladders $K_{3,3}$, $K'_{3,3}$, $M_5$, $M_5^*$ (Figure 1 of the paper, on 6, 7, 6 and 6 vertices) as a subgraph, not necessarily induced.

Formalization targets

Goal: Theorem 1.2

For every finite tournament $T$,

$$T \text{ is Möbius-free} \iff T \text{ is FAS ideal} \iff T \text{ is FAS Mengerian}.$$

Milestones

The milestones follow the proof (pp.23–27):

• (iii) ⇒ (ii): total dual integrality implies integrality (Edmonds–Giles).
• (ii) ⇒ (i): Lehman's theorem makes FAS ideal the same as cycle ideal for tournaments, and Theorem 1.1 makes cycle ideal the same as Möbius-free.
• (i) ⇒ (iii), through five steps:
  1. the reduction to strong tournaments;
  2. the two exceptional tournaments $G_1$ (Lemma 4.1, via Lemmas 4.2, 4.3 and Claim 1) and $F_1=G_1-v_6$;
  3. the structure theorem (Theorem 2.7, built on Lemmas 2.2 and 2.11): every other Möbius-free strong tournament on at least three vertices lies in the class $\mathcal P$ of Figure 7;
  4. the base case: every tournament in the class $\mathcal Q$ is FAS Mengerian (Lemma 3.2);
  5. the induction on the number of vertical blocks of $\mathcal P$ (Theorem 3.1).

Significance

Theorem 1.2 is a complete description of the tournaments on which the FAS-packing minimax $\lambda_w=\mu_w$ holds for all weights. On these tournaments, the LP relaxation of the FAS problem has integral optimal solutions on both sides. Combined with Theorem 1.1 it gives Corollary 1.3: for tournaments, cycle Mengerian, FAS Mengerian and Möbius-free coincide, so the same four ladders obstruct both minimax relations. This is notable because, on general digraphs, the FAS-packing relation is much less understood: it contains the Edmonds–Giles and Woodall questions on planar digraphs.

The result is proved in the literature but has no machine-checked proof. Formalizing it requires a library for feedback arc sets, Möbius ladders and tournament structure. It also requires two classical polyhedral facts that are absent from Mathlib: Edmonds–Giles (total dual integrality implies integrality, and its minimax form) and Lehman's theorem on ideal clutters and their blockers. Finally, the computer-assisted part (Lemma 4.1: 41022 integer programs certified through Lemma 4.3) is a natural candidate for a certificate-checking proof in Lean.

Difficulty

Two of the three implications rest on deep external theorems. Lehman's theorem is a substantial result about ideal clutters, and Theorem 1.1 is the main result of two earlier papers. The direct implication (i) ⇒ (iii) cannot be argued locally: FASs are global objects, and an FAS packing of a tournament does not split along a 1-sum the way a cycle packing does. That is why the paper needs the global chain structure $\mathcal P$ rather than the local 1-sum decomposition used for Theorem 1.1. The induction step (Theorem 3.3, about ten pages) glues FAS packings of the two sides of a vertical block by a breadth-first-search construction. The tournament $G_1$ resists this structural argument and is handled by exhaustive computation over the odd stable sets of an auxiliary 41-vertex graph.

Formalization scope

Digraphs are Mathlib's Digraph V on a finite type $V$; IsTournament excludes loops and requires exactly one arc between distinct vertices. Arcs are the subtype Arc G of adjacent pairs. A directed cycle is an arc set (IsDirCycle), and FASs are finite arc sets. $\lambda_w$ and $\mu_w$ take values in $\mathbb N\cup\{\infty\}$; both are $\infty$ exactly when $G$ is acyclic. IsTDI is defined once, for an integral matrix with finite row and column types and a rational right-hand side, quantifying over all integral costs. FAS Mengerian is IsTDI of the FAS-arc incidence matrix with rows indexed by all FASs, and FAS ideal uses the published IsIntegralPolyhedron ($P=\operatorname{conv}(P\cap\mathbb Z^A)$). The ladders, $G_1$ and $F_1$ are explicit digraphs on Fin n, with vertex $u_i$ at index $i-1$. Containment is a not-necessarily-induced embedding; with induced containment every tournament would be Möbius-free, since the ladders are not tournaments, and the goal would collapse. "Other than $F_1$ and $G_1$" means not isomorphic to them.

Theorem 2.7 carries one correction: $|V|\ge3$, since the one-vertex tournament is strong and Möbius-free but not in $\mathcal P$. The goal itself has no restriction: empty and acyclic tournaments are included.

The development needs LP duality for finite systems, the Edmonds–Giles and Lehman theorems (reusable well beyond this mission), the tournament structure theory of Section 2, and certificate checking for Lemma 4.1. Contributions to any of these layers are welcome, as are proofs of Theorem 1.1, which is cited here and not proved in the paper.

Selected references

• X. Chen, G. Ding, W. Zang, Q. Zhao, Packing Feedback Arc Sets in Tournaments Exactly, Mathematics of Operations Research, 2024. https://doi.org/10.1287/moor.2023.1352
• X. Chen, G. Ding, W. Zang, Q. Zhao, Ranking tournaments with no errors I: Structural description, J. Combin. Theory Ser. B 141 (2020), 264–294.
• X. Chen, G. Ding, W. Zang, Q. Zhao, Ranking tournaments with no errors II: Minimax relation, J. Combin. Theory Ser. B 142 (2020), 244–275.
• J. Edmonds, R. Giles, A min-max relation for submodular functions on graphs, Annals of Discrete Mathematics 1 (1977), 185–204.
• A. Lehman, On the length-width inequality, Mathematical Programming 17 (1979), 403–417.
• A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986 (Corollary 22.13d).
• A. Schrijver, A counterexample to a conjecture of Edmonds and Giles, Discrete Mathematics 32 (1980), 213–214.
• N. Alon, Ranking tournaments, SIAM J. Discrete Math. 20 (2006), 137–142.

Motivation

Linear stochastic approximation (LSA) solves a linear system $\bar{\mathbf A}\theta=\bar{\mathbf b}$ when only noisy observations of the matrix and of the right-hand side are available. It is the linear core of temporal-difference learning with linear function approximation, of stochastic gradient descent on least squares, and of many online estimation schemes in statistics and reinforcement learning. Its practical form uses a fixed step size together with Polyak–Ruppert averaging, introduced by Ruppert (1988) and Polyak and Juditsky (doi:10.1137/0330046), whose asymptotic theory gives the central limit theorem with optimal covariance.

Asymptotic statements say little at a finite sample size, so the question is how fast the averaged iterate reaches the Gaussian regime, with explicit dependence on the moment order $p$, the dimension $d$ and the noise. Mou et al. (arXiv:2004.04719) gave a $p$-th moment bound with a remainder of order $n^{-2/3}$. Durmus, Moulines, Naumov and Samsonov (arXiv:2207.04475v2) obtain a remainder of order $n^{-3/4}$ with a leading term that matches the central limit theorem, and a step size that depends on the dimension only through $1/\log d$.

Setting

Let $(\mathsf Z,\mathcal Z)$ be a measurable space with a probability measure $\pi$, and let $\mathbf A:\mathsf Z\to\mathbb R^{d\times d}$ and $\mathbf b:\mathsf Z\to\mathbb R^d$ be measurable, $d\ge1$. Write $\bar{\mathbf A}=\int\mathbf A\,d\pi$, $\bar{\mathbf b}=\int\mathbf b\,d\pi$, $\tilde{\mathbf A}=\mathbf A-\bar{\mathbf A}$ and $\tilde{\mathbf b}=\mathbf b-\bar{\mathbf b}$. Let $\theta^\star$ be the solution of $\bar{\mathbf A}\theta=\bar{\mathbf b}$, and let the noise be

$$\varepsilon(z)=\tilde{\mathbf A}(z)\theta^\star-\tilde{\mathbf b}(z),\qquad\Sigma_\varepsilon=\int\varepsilon(z)\varepsilon(z)^\top d\pi(z).$$

Three assumptions are in force. A 1: $\mathrm C_{\mathbf A}=\sup_z\|\mathbf A(z)\|\vee\sup_z\|\tilde{\mathbf A}(z)\|<\infty$ in the spectral norm, and every eigenvalue of $\bar{\mathbf A}$ has positive real part. A 2: $\|\varepsilon\|_\infty=\sup_z\|\varepsilon(z)\|<\infty$. IND 1: $(Z_k)_{k\in\mathbb N}$ is i.i.d. with law $\pi$.

For a step size $\alpha>0$ and a starting point $\theta_0$, the LSA iterates and, for even $n$, the Polyak–Ruppert average with burn-in $n/2$ are

$$\theta_k=\theta_{k-1}-\alpha\{\mathbf A(Z_k)\theta_{k-1}-\mathbf b(Z_k)\},\qquad\bar\theta_n=\frac2n\sum_{k=n/2}^{n-1}\theta_k.$$

The Lyapunov matrix $Q$ is the unique symmetric positive definite solution of $\bar{\mathbf A}^\top Q+Q\bar{\mathbf A}=\mathrm I$. With $\|x\|_Q=(x^\top Qx)^{1/2}$ and the induced operator norm,

$$a=\|Q\|^{-1}/2,\quad\alpha_\infty=\tfrac12\|\bar{\mathbf A}\|_Q^{-2}\|Q\|^{-1}\wedge\|Q\|,\quad\kappa_Q=\frac{\lambda_{\max}(Q)}{\lambda_{\min}(Q)},\quad b_Q=2\sqrt{\kappa_Q}\mathrm C_{\mathbf A},\quad\mathrm c_{\mathbf A}=\frac a{2b_Q^2}.$$

Formalization targets

Goal: Theorem 1

There are a function $C$ and an exponent $k$ such that, for every $d\ge1$, every instance as above, every real $p\ge2$, every even $n\ge2$ and every $\theta_0$, with the step size $\alpha(n,d,p)=(\alpha_\infty\wedge\mathrm c_{\mathbf A}/\{1+\log d\})(pn^{1/2})^{-1}$,

$$\mathbb E^{1/p}\big[\|\bar{\mathbf A}(\bar\theta_n-\theta^\star)\|^p\big]\le C(\kappa_Q,a,\mathrm C_{\mathbf A})(1+\log d)^k\Big(\frac{\{\mathrm{Tr}\,\Sigma_\varepsilon\}^{1/2}p^{1/2}}{n^{1/2}}+\|\varepsilon\|_\infty\Big(\frac p{n^{3/4}}+\frac{p^2}n\Big)+p\|\theta_0-\theta^\star\|\exp\Big\{-\frac{a(\alpha_\infty\wedge\mathrm c_{\mathbf A})\sqrt n}{8p(1+\log d)}\Big\}\Big).$$

The factor $a$ in the exponent is absent from the printed statement (p.7), which is false without it: for $d=1$, $\mathbf A\equiv1/8$, $\mathbf b$ constant, the left side decays like $\mathrm e^{-\sqrt n/(16p)}$ and the printed right side like $\mathrm e^{-\sqrt n/(8p)}$. The paper's proof yields the form above.

Exact-constant milestone: Theorem 2

For every $\alpha\in(0,\alpha_{p(1+\log d),\infty})$,

$$(n/2)^{1/2}\,\mathbb E^{1/p}\big[\|\bar{\mathbf A}(\bar\theta_n-\theta^\star)\|^p\big]\le\mathrm C_{\mathrm{Rm},1}\{\mathrm{Tr}\,\Sigma_\varepsilon\}^{1/2}p^{1/2}+\Delta^{(\mathrm{fl})}_{n,p,\alpha}\|\varepsilon\|_\infty+\mathrm e^{-\alpha an/8}\Delta^{(\mathrm{tr})}_{n,p,\alpha}\|\theta_0-\theta^\star\|,$$

with the constants (53) of the paper.

Supporting milestones

• Proposition 1 (Lyapunov contraction) and Proposition 2 (exponential stability of random matrix products).
• Lemma 8 (vector Hoeffding, Pinelis), Lemma 7 (moments from sub-Gaussian tails), the Burkholder–Minkowski bound with constant $p$, and Rosenthal's inequality with $\mathrm C_{\mathrm{Rm},1}=60\mathrm e$, $\mathrm C_{\mathrm{Rm},2}=60$.
• The pathwise identities (8), (11), (13) and (14).
• Propositions 3, 4 and 6, the moment bounds on the expansion terms and on the last iterate.

Significance

The bound says that the averaged iterate attains the Gaussian rate in every moment up to a remainder of order $n^{-3/4}$, with exponential forgetting of the starting point. It separates the variance-driven term from higher-order effects at a fixed sample size, and the step size condition scales with $1/\log d$ rather than with a power of $d$. The exact-constant form, Theorem 2, is what a practitioner or a downstream analysis would instantiate.

The paper's results are proved, not open. What this mission adds is a machine-checked version of a finite-time theory that, on this platform, has so far been asymptotic (Polyak–Juditsky) or restricted to projected temporal-difference learning. No proof of Theorem 1 or Theorem 2 is known to be formalized. The cited inequalities with explicit constants, Hoeffding, Burkholder and Rosenthal in Euclidean space, are not in Mathlib and are reusable well beyond this mission.

Difficulty

The noise in $\mathbf A(Z_k)$ multiplies the iterate, so $\theta_n-\theta^\star$ is not a sum of independent terms. Bounding $\Gamma^{(\alpha)}_{1:n}$ by the product of the norms of its factors fails: individual factors need not be contractions, and the resulting bound grows with $n$. One needs contraction in expectation of a random matrix product, with a dimension factor no larger than $d^{1/q}$. A second obstacle is the order of the remainder. The first-order expansion only gives $\mathbb E^{1/p}[\|H^{(0)}_n\|^p]=O(\sqrt\alpha)$, which cannot reach $n^{-3/4}$, so the second-order expansion is needed. Finally, the leading constant requires Rosenthal's inequality with a dimension-free Gaussian term, not a coordinatewise argument, which would cost a factor of $d$.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin d), $d\ge1$. Matrices are Matrix (Fin d) (Fin d) ℝ, with the spectral norm matNorm and the action matApply, reused from PolyakJuditsky_Averaging_Model together with the Hurwitz condition EigenRePos. $\mathbb E^{1/p}[\|X\|^p]$ is eLpNorm X (ENNReal.ofReal p) P in $[0,\infty]$. $p$ and $q$ are real. $\mathrm C_{\mathbf A}$ and $\|\varepsilon\|_\infty$ are upper bounds of the suprema, $Q$ is a hypothesis, and $\bar{\mathbf A}$ and $\bar{\mathbf b}$ are the integrals, so they cannot be chosen independently of $\pi$.

The symbol $\lesssim_d$ is the outer quantifier $\exists C\,\exists k$, chosen before the dimension and the instance, and $C$ receives only $\kappa_Q,a,\mathrm C_{\mathbf A}$; a constant allowed to see $n$, $p$ or $\theta_0$ would make the goal trivial.

A complete development needs Burkholder's inequality with an explicit constant for Hilbert-space-valued martingales, Pinelis's Hoeffding and Rosenthal inequalities, and the Schatten-norm argument behind Proposition 2. These are the reusable parts. Contributions to any milestone are welcome, including alternative proofs of the cited inequalities.

Selected references

• A. Durmus, E. Moulines, A. Naumov, S. Samsonov, Finite-time High-probability Bounds for Polyak-Ruppert Averaged Iterates of Linear Stochastic Approximation, arXiv:2207.04475v2, 2023. https://arxiv.org/abs/2207.04475v2
• A. Durmus, E. Moulines, A. Naumov, S. Samsonov, K. Scaman, H.-T. Wai, Tight High Probability Bounds for Linear Stochastic Approximation with Fixed Stepsize, NeurIPS 2021. https://arxiv.org/abs/2106.01257
• W. Mou, C. J. Li, M. J. Wainwright, P. L. Bartlett, M. I. Jordan, On Linear Stochastic Approximation: Fine-grained Polyak-Ruppert and Non-Asymptotic Concentration, COLT 2020. https://arxiv.org/abs/2004.04719
• I. Pinelis, Optimum Bounds for the Distributions of Martingales in Banach Spaces, Annals of Probability 22(4), 1994. https://doi.org/10.1214/aop/1176988477
• A. Osękowski, Sharp Martingale and Semimartingale Inequalities, Birkhäuser, 2012. https://doi.org/10.1007/978-3-0348-0370-0
• B. T. Polyak, A. B. Juditsky, Acceleration of Stochastic Approximation by Averaging, SIAM Journal on Control and Optimization 30(4), 1992. https://doi.org/10.1137/0330046

Motivation

A seller with one item faces buyers whose values are drawn i.i.d. from a distribution $F$. The welfare-optimal mechanism is an auction: it allocates to the highest bidder and achieves $M_n(F)$, the expected maximum of $n$ values. Dynamic pricing, which offers the item to the buyers one at a time at prices that may depend on the remaining number of buyers, is simpler and widely used, but with the same $n$ buyers it only guarantees a constant fraction of $M_n(F)$ (about $0.745$, the i.i.d. prophet constant, which the paper re-derives as $1/(1+\phi^{-1}(1))$). The competition complexity question, in the spirit of Bulow and Klemperer's "auctions versus negotiations", asks how many additional buyers dynamic pricing needs to match or approximately match the auction.

Brustle, Correa, Dütting and Verdugo (MOR 2024) answer this question. With exact matching ($\varepsilon=0$) no number of extra buyers suffices (their Theorem 1). With a factor $1+\varepsilon$ of slack, a linear number $\phi(\varepsilon)n$ of buyers is necessary and sufficient, where $\phi(\varepsilon)$ grows only like $\log\log(1/\varepsilon)$. Through standard reductions the same bounds hold for revenue in the regular i.i.d. case.

The analysis builds on the i.i.d. prophet-inequality line of work, in particular Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (MOR 2021), whose differential equation and recursion for optimal thresholds are the continuous and discrete objects compared here, and on Kertz (J. Multivariate Anal. 1986).

Setting

A distribution $F$ is a probability law on $[0,\infty)$ with finite mean; nothing else is assumed. Write $F(y)$ for its distribution function and $\omega_0(F)=\inf\{y:F(y)>0\}$, $\omega_1(F)=\sup\{y:F(y)<1\}$ for the endpoints of its support. With $X_1,X_2,\dots$ i.i.d. with law $F$:

• $M_0(F)=0$ and $M_n(F)=\mathbb E\max\{X_1,\dots,X_n\}$ for $n\ge1$;
• $A_0(F)=0$ and $A_{n+1}(F)=\mathbb E\max\{X,A_n(F)\}$, the value of the optimal stopping rule (optimal dynamic pricing) with $n+1$ buyers.

For a sequence $(S_n)_{n\ge0}$, $\partial S_n=S_{n+1}-S_n$. The paper's central object is the program

$$\min\ (1+\varepsilon)\sum_{i=0}^{m-1}\delta_i-\sum_{i=0}^{\infty}\Bigl(1-\Bigl(\frac{\delta_{i+1}}{\delta_i}\Bigr)^n\Bigr)\delta_i$$

over sequences with $\delta_0=1$, $\delta_j>0$, $\delta_{j+1}\le\delta_j$ and $\delta_j^2\le\delta_{j-1}\delta_{j+1}$, together with the recursion $\rho_{\varepsilon,1}=1$, $(n-1)\rho_{\varepsilon,j-1}^n-\varepsilon=n\rho_{\varepsilon,j}^{n-1}$, and the function

$$\phi(\varepsilon)=\int_0^1\frac{dy}{y(1-\log y)+\varepsilon}.$$

Formalization targets

Goal: Theorem 2

For every $\varepsilon>0$, every $n\ge1$ and every integer $m\ge\phi(\varepsilon)n$,

$$(1+\varepsilon)A_m(F)\ge M_n(F)\quad\text{for every distribution }F;$$

$\phi(\varepsilon)=\Theta(\log\log 1/\varepsilon)$ as $\varepsilon\to0^+$; and for every $\delta>0$ there is $n_0$ such that for each $n\ge n_0$ some distribution $G$ has

$$(1+\varepsilon)A_m(G)<M_n(G)\quad\text{for all } 1\le m<(\phi(\varepsilon)-\delta)n .$$

Milestones, in proof order

1. Proposition 1 and Lemma 1: increment formulas for $A_n(F)$; $(A_n(F))$ is strictly increasing with non-increasing increments and non-decreasing increment ratios.
2. Lemmas 2–3 and Claim 1: $M_n(F)\le\sum_j(1-(\partial A_{j+1}/\partial A_j)^n)\partial A_j$, and every such sequence with $\partial A_j\to0$ is realized by a distribution with equality (the printed Lemma 3 omits this condition, without which it is false: $B_n=n$).
3. Theorem 3: the competition-complexity inequality for all $F$ is equivalent to the program having non-negative value.
4. Claim 2, Propositions 2–4 and Lemma 4: the program's value is $\varepsilon-(n-1)\rho_{\varepsilon,m}^n$.
5. Propositions 5–6, Lemma 5 and Claim 4: the recursion is compared with the ODE $y'=y(\log y-1)-\varepsilon$, $y(0)=1$, whose solution hits $0$ at time $\phi(\varepsilon)$.

Significance

Theorem 2 gives an exact linear rate for the approximate competition complexity: dynamic pricing needs $\phi(\varepsilon)n$ buyers, no fewer, to be within a factor $1+\varepsilon$ of the optimal auction. For moderate $\varepsilon$ the constant is small (for instance $\phi(\varepsilon)\le1$ once $1/(1+\varepsilon)$ is at most the i.i.d. prophet constant), and it grows doubly logarithmically as $\varepsilon\to0$, in contrast with the unbounded exact competition complexity.

The formalization adds two things. First, a machine-checked reduction (Theorem 3) of a statement quantified over all distributions to an optimization over log-convex sequences, which is reusable for other i.i.d. stopping problems. Second, a checked comparison of the discrete recursion (9) with its ODE. The paper's proof of Lemma 5(b) contains a gap: the third-order Taylor remainder is written as $y'''(\xi)/(6n^6)$ where it is $y'''(\xi)/(6n^3)$, and with the correct remainder the paper's Proposition 7 does not carry the argument. Lemma 5(b) itself checks numerically. Lemma 5(c) is not proved in the paper (it is described as an extension of Kertz's Corollary 6.9). A formal proof of Lemma 5 therefore needs new work. As of 2026, none of these results is formalized.

Difficulty

The sufficiency direction cannot be obtained by bounding $A_m(F)$ and $M_n(F)$ separately for each $F$: the worst distribution depends on $n$, $m$ and $\varepsilon$, and must be found among all distributions. The paper does this by an exact characterization of the reachable sequences $(A_j(F))$ and an exact solution of the resulting infinite-dimensional, non-convex program. The second obstacle is quantitative: the last index at which the recursion (9) stays positive has to be located to within $o(n)$, which requires a two-sided comparison with an ODE whose solution has an infinite second derivative of $\log$ type at its endpoint, and a third-derivative analysis (Proposition 6) with explicit numerical constants.

A tempting shortcut for tightness is to fix one distribution $G$ that works for all large $n$. That fails for every $G$ with bounded support, since $A_m(G)\to\omega_1(G)\ge M_n(G)$, and the paper's witness depends on $n$. The goal states tightness in that form.

Formalization scope

Distributions are Lean measures on $\mathbb R$ that are probability measures with $\mu((-\infty,0))=0$ and an integrable identity. $A_n$ is the published recursion CorreaThreshold.Adaptive.dpW. $M_n$ is the published SamuelCahnProphet.IID.Emax (a lower integral in $[0,\infty]$), with $M_0=0$; comparisons map $(1+\varepsilon)A_m$ into $[0,\infty]$. Indices are 0-based as in the paper, except $\rho_{\varepsilon,j}$ and $\Gamma^\varepsilon_{n,m}$, which use the paper's 1-based indices. $\omega_1$ is extended-real valued. Series over feasible sequences are real tsums whose summability is proved in the verification file, or are summed in $[0,\infty]$. The value of the program is expressed through "non-negative at every feasible point" and IsGLB, never sInf, because it is not attained. A solution of the ODE is continuous on $[0,\phi(\varepsilon)]$, positive with the prescribed derivative on $(0,\phi(\varepsilon))$, and the third derivative is taken within $[0,\phi(\varepsilon)]$; statements about it stop before $\phi(\varepsilon)$, where it is undefined. Theorem 2's converse is stated with the witness $G$ chosen after $n$ and uniform in $m$.

Infrastructure needed: tail-integral formulas for expectations of non-negative variables, $\mathbb E\max=\int_0^\infty(1-F^n)$, construction of a distribution from a prescribed distribution function, Picard–Lindelöf on an open interval with a continuous extension, and asymptotics of $\phi$. The reduction (Theorem 3 and Lemmas 1–3) and the ODE analysis are each reusable. Contributions welcome on any milestone, in particular a repaired proof of Lemma 5(b). A related open platform statement is CorreaThreshold.Adaptive.lemma_7, the analogous comparison for a different recursion.

Selected references

• J. Brustle, J. Correa, P. Dütting, V. Verdugo, The Competition Complexity of Dynamic Pricing, Mathematics of Operations Research 49(3):1986–2008, 2024. https://doi.org/10.1287/moor.2022.0230 (accepted manuscript: LSE Research Online eprint 124364)
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted Price Mechanisms and Optimal Threshold Strategies for Random Arrivals, Mathematics of Operations Research 46(4):1452–1478, 2021. https://doi.org/10.1287/moor.2020.1105
• R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19(1):88–112, 1986. https://doi.org/10.1016/0047-259X(86)90095-3
• J. Bulow, P. Klemperer, Auctions versus Negotiations, American Economic Review 86(1):180–194, 1996. https://www.jstor.org/stable/2118262