All missions

Motivation

Two new classes of quantum channels, which we call more capable and less noisy, are introduced. The more capable class consists of channels such that the quantum capacities of the complementary channels to the environments are zero. The less noisy class consists of channels such that the private capacities of the complementary channels to the environment are zero. For the more capable class, it is clarified that the private capacity and quantum capacity coincide. For the less noisy class, it is clarified that the private capacity and quantum capacity can be single letter characterized.

This mission is the statement-level formalization of Private and Quantum Capacities of More Capable and Less Noisy Quantum Channels (arXiv:1110.5746v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: more capable channels have equal private and quantum capacities (Theorem 1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• Private and Quantum Capacities of More Capable and Less Noisy Quantum Channels, arXiv:1110.5746v3, https://arxiv.org/abs/1110.5746v3

Motivation

We show that the conditional min-entropy Hmin(A|B) of a bipartite state rho_AB is directly related to the maximum achievable overlap with a maximally entangled state if only local actions on the B-part of rho_AB are allowed. In the special case where A is classical, this overlap corresponds to the probability of guessing A given B. In a similar vein, we connect the conditional max-entropy Hmax(A|B) to the maximum fidelity of rho_AB with a product state that is completely mixed on A. In the case where A is classical, this corresponds to the security of A when used as a secret key in the presence of an adversary holding B. Because min- and max-entropies are known to characterize information-processing tasks such as randomness extraction and state merging, our results establish a direct connection between these tasks and basic operational problems. For example, they imply that the (logarithm of the) probability of guessing A given B is a lower bound on the number of uniform secret bits that can be extracted from A relative to an adversary holding B.

This mission is the statement-level formalization of The operational meaning of min-and max-entropy (arXiv:0807.1338v2). 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 / abstract: min-entropy is maximum achievable singlet fraction (Theorem 2 / (32), PDF p. 9). 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 I C, implications; (14) on p.4: A fixed numerical secrecy metric, public-seed/reference convention, and finite-error extraction length. (source-ambiguity)

Selected references

• The operational meaning of min-and max-entropy, arXiv:0807.1338v2, https://arxiv.org/abs/0807.1338v2

Motivation

We exhibit a possible road towards a strong converse for the quantum capacity of degradable channels. In particular, we show that all degradable channels obey what we call a "pretty strong" converse: When the code rate increases above the quantum capacity, the fidelity makes a discontinuous jump from 1 to at most 0.707, asymptotically. A similar result can be shown for the private (classical) capacity. Furthermore, we can show that if the strong converse holds for symmetric channels (which have quantum capacity zero), then degradable channels obey the strong converse: The above-mentioned asymptotic jump of the fidelity at the quantum capacity is then from 1 down to 0.

This mission is the statement-level formalization of "Pretty strong" converse for the quantum capacity of degradable channels (arXiv:1301.4927v3). 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: pretty strong quantum converse (Theorem 2: pretty strong quantum converse, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 20; proof p.16: A positive finite code-dimension rounding and smoothing-endpoint convention for the printed one-shot formula. (source-ambiguity)
• Section IX nonstationary-memoryless claim: Precise error/privacy thresholds and sequence-uniform quantifiers for the two-sided nonstationary o(n) expansion. (source-ambiguity)

Selected references

• "Pretty strong" converse for the quantum capacity of degradable channels, arXiv:1301.4927v3, https://arxiv.org/abs/1301.4927v3

Motivation

Quantum Stein's Lemma is a cornerstone of quantum statistics and concerns the problem of correctly identifying a quantum state, given the knowledge that it is one of two specific states ($ρ$ or $σ$). It was originally derived in the asymptotic i.i.d. setting, in which arbitrarily many (say, $n$) identical copies of the state ($ρ^{\otimes n}$ or $σ^{\otimes n}$) are considered to be available. In this setting, the lemma states that, for any given upper bound on the probability $α_n$ of erroneously inferring the state to be $σ$, the probability $β_n$ of erroneously inferring the state to be $ρ$ decays exponentially in $n$, with the rate of decay converging to the relative entropy of the two states. The second order asymptotics for quantum hypothesis testing, which establishes the speed of convergence of this rate of decay to its limiting value, was derived in the i.i.d. setting independently by Tomamichel and Hayashi, and Li. We extend this result to settings beyond i.i.d.. Examples of these include Gibbs states of quantum spin systems (with finite-range, translation-invariant interactions) at high temperatures.

This mission is the statement-level formalization of Second-order asymptotics for quantum hypothesis testing in settings beyond i.i.d. - quantum lattice systems and more (arXiv:1510.04682v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: second-order testing bounds beyond IID (seed result) (Theorem 1, PDF p. 9). 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

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

• Proposition 4 (4.22)–(4.23): claimed boundary correction: Proposition 4 (4.22)–(4.23): claimed boundary correction (source-ambiguity)
• Remark 2: claimed Gaussian tradeoff identity: Remark 2: claimed Gaussian tradeoff identity (source-ambiguity)
• Remark 5: claimed one-dimensional application of Corollary 1: Remark 5: claimed one-dimensional application of Corollary 1 (source-ambiguity)
• Remark 5: higher-dimensional second-order discussion: Remark 5: higher-dimensional second-order discussion (source-ambiguity)
• Remark 6: claimed different-temperature Gibbs application: Remark 6: claimed different-temperature Gibbs application (source-ambiguity)

Selected references

• Second-order asymptotics for quantum hypothesis testing in settings beyond i.i.d. - quantum lattice systems and more, arXiv:1510.04682v4, https://arxiv.org/abs/1510.04682v4

Motivation

We present a framework for studying bosonic non-Gaussian channels of continuous-variable systems. Our emphasis is on a class of channels that we call photon-added Gaussian channels, which are experimentally viable with current quantum-optical technologies. A strong motivation for considering these channels is the fact that it is compulsory to go beyond the Gaussian domain for numerous tasks in continuous-variable quantum information processing such as entanglement distillation from Gaussian states and universal quantum computation. The single-mode photon-added channels we consider are obtained by using two-mode beam splitters and squeezing operators with photon addition applied to the ancilla ports giving rise to families of non-Gaussian channels. For each such channel, we derive its operator-sum representation, indispensable in the present context. We observe that these channels are Fock preserving (coherence nongenerating). We then report two examples of activation using our scheme of photon addition, that of quantum-optical nonclassicality at outputs of channels that would otherwise output only classical states and of both the quantum and private communication capacities, hinting at far-reaching applications for quantum-optical communication. Further, we see that noisy Gaussian channels can be expressed as a convex mixture of these non-Gaussian channels. We also present other physical and information-theoretic properties of these channels.

This mission is the statement-level formalization of Non-Gaussian operations on bosonic modes of light: Photon-added Gaussian channels (arXiv:1604.07859v4). 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 The explicit photon-added Kraus families represent the canonical channels (Theorem 3, 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:

• Conjecture 2: A proved exact converse to Gaussian-dilatable implies linear Bosonic (source-ambiguity)
• Proposition 4: A consistent universal mixed-input Fock-support equality with endpoint domains (source-ambiguity)
• Corollary 5: Valid restrictions for the no-finite-support-fixed-point claim (source-ambiguity)
• Theorem 7: A valid all-classical-input strong-activation theorem (source-ambiguity)
• Conjecture 10: A proof of positive operational Q and P for every kappa>0,n>0 (hard)
• Conjecture 17: Within-branch independence and a justified infinite-dimensional extremality criterion (hard)
• Remark 18: A substantive new photon-added-channel theorem in the extremality remark (source-ambiguity)
• §IV E, unnumbered: Gaussian inputs become non-Gaussian: Source-supported photon-addition and coupling restrictions for Gaussian-input non-Gaussian output (source-ambiguity)

Selected references

• Non-Gaussian operations on bosonic modes of light: Photon-added Gaussian channels, arXiv:1604.07859v4, https://arxiv.org/abs/1604.07859v4

Motivation

We show that a recent definition of relative Rényi entropy is monotone under completely positive, trace preserving maps. This proves a recent conjecture of Müller-Lennert et al.

This mission is the statement-level formalization of Monotonicity of a relative Rényi entropy (arXiv:1306.5358v3). 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 Monotonicity of the sandwiched relative Rényi entropy (Theorem 1 (Monotonicity), 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

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

• Lemma 4: Extended negative-order spectral penalty on all bounded positive H and nonnegative sigma (hard)
• Lemma 5: Extended trace of (B* A^p B)^(1/p) for negative p and arbitrary singular B (hard)
• Remark 6: Two-parameter extended spectral/form trace for singular nonnegative A and negative p (hard)

Selected references

• Monotonicity of a relative Rényi entropy, arXiv:1306.5358v3, https://arxiv.org/abs/1306.5358v3

Motivation

In this short note, I show how a recent result of Alhejji and Smith [arXiv:1909.00787] regarding an optimal uniform continuity bound for classical conditional entropy leads to an optimal uniform continuity bound for quantum conditional entropy of classical--quantum states. The bound is optimal in the sense that there always exists a pair of classical--quantum states saturating the bound, and so no further improvements are possible. An immediate application is a uniform continuity bound for entanglement of formation that improves upon the one previously given by Winter in [arXiv:1507.07775]. Two intriguing open questions are raised regarding other possible uniform continuity bounds for conditional entropy, one about quantum--classical states and another about fully quantum bipartite states.

This mission is the statement-level formalization of Optimal uniform continuity bound for conditional entropy of classical--quantum states (arXiv:1909.01755v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Sharp continuity of finite classical–quantum conditional entropy (Proposition 1, Eqs. (4)–(6), 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.

Selected references

• Optimal uniform continuity bound for conditional entropy of classical--quantum states, arXiv:1909.01755v2, https://arxiv.org/abs/1909.01755v2

Motivation

A central goal in information theory and cryptography is finding simple characterizations of optimal communication rates subject to various restrictions and security requirements. Ideally, the optimal key rate for a quantum key distribution (QKD) protocol would be given by {\em single-letter formula} involving a simple optimization over a single use of an effective channel. We explore the possibility of such a formula for one of the simplest and most widely used QKD protocols--Bennett-Brassard-84 (BB84) with one way classical post-processing. We show that a conjectured single-letter key-rate formula is false, uncovering a deep ignorance about asymptotically good private codes and pointing towards unfortunate complications in the theory of QKD. These complications are not without benefit--with added complexity comes better key rates than previously thought possible. We improve the threshold for secure key generation from a bit error rate of 0.124 to 0.129.

This mission is the statement-level formalization of Structured Codes Improve the Bennett-Brassard-84 Quantum Key Rate (arXiv:quant-ph/0607018v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Repetition-code logical Pauli error and exact syndrome probability (Lemma 2 / Eq. (3), 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:

• Abstract/introduction; qualification in footnote [21], PDF p.4: An operational BB84 one-way distillable-key rate and the complete BB84 single-letter stochastic-preprocessing objective on the same source family. (hard)
• Theorem 1, Eq. (1)–(2); proof on PDF p.3: Computed processed ccq objective for Eq.(1), together with a genuine source-uniform operational BB84 achievability predicate. (hard)

Selected references

• Structured Codes Improve the Bennett-Brassard-84 Quantum Key Rate, arXiv:quant-ph/0607018v2, https://arxiv.org/abs/quant-ph/0607018v2

Motivation

We consider the manipulation of multipartite entangled states in the limit of many copies under quantum operations that asymptotically cannot generate entanglement. As announced in [Brandao and Plenio, Nature Physics 4, 8 (2008)], and in stark contrast to the manipulation of entanglement under local operations and classical communication, the entanglement shared by two or more parties can be reversibly interconverted in this setting. The unique entanglement measure is identified as the regularized relative entropy of entanglement, which is shown to be equal to a regularized and smoothed version of the logarithmic robustness of entanglement. Here we give a rigorous proof of this result, which is fundamentally based on a certain recent extension of quantum Stein's Lemma proved in [Brandao and Plenio, Commun. Math. 295, 791 (2010)], giving the best measurement strategy for discriminating several copies of an entangled state from an arbitrary sequence of non-entangled states, with an optimal distinguishability rate equal to the regularized relative entropy of entanglement. We moreover analyse the connection of our approach to axiomatic formulations of the second law of thermodynamics.

This mission is the statement-level formalization of A reversible theory of entanglement and its relation to the second law (arXiv:0710.5827v3). 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 I, equation (2): reversible multipartite entanglement (Theorem I, equation (2): reversible multipartite entanglement, PDF p. 6). 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

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

• Section III unnumbered: unique entanglement measure: An admissible normalized class of entanglement functionals with the axioms needed for a literal uniqueness assertion. (source-ambiguity)
• Section IV closing Remark: other free families and PPT: A cross-system free-family convention for the generalized operational extension, and the multipartite PPT cuts; the Bell currency itself and five fixed-H testing axioms are specified. (source-ambiguity)
• Section V unnumbered: asymptotically continuous leakage: A consistent continuity modulus and a quantified growing-dimension leakage convention for arbitrary measures. (source-ambiguity)
• Section V unnumbered: scaled norm leakage and bounded yield: The system H in dimension-scaled trace/operator-norm leakage and the resulting dual coefficient. (source-ambiguity)

Selected references

• A reversible theory of entanglement and its relation to the second law, arXiv:0710.5827v3, https://arxiv.org/abs/0710.5827v3

Motivation

We present a continuous-variable quantum key distribution protocol combining a continuous but slightly non-Gaussian modulation together with a efficient reverse reconciliation scheme. We establish the security of this protocol against collective attacks which correspond to a linear quantum channel. In particular, all Gaussian attacks are considered in our framework. We show that this protocol outperforms all known practical protocols, even taking into account finite size effects.

This mission is the statement-level formalization of Long distance quantum key distribution with continuous variables (arXiv:1005.0328v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Uniform spherical modulation by Gaussian normalization (Section 2, Eq. (2) and footnote 4: normalized Gaussian sampling of the uniform sphere modulation, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract, pp.1,3,9: asymptotic security of the spherical-modulation protocol against linear collective attacks: sphere-modulated four-coherent-state ensemble; heterodyne instrument; linear collective attack and Eve purification; octonion-dependent public rotation and norm transcript; binary reconciliation code and its syndrome; privacy amplification; asymptotic secret-key rate, beta, mutual information and conditional Holevo information (source-ambiguity)
• Section 2: reduction to binary reconciliation with the four-state protocol efficiency: eight-dimensional octonion rotations; random bits; hypercube encoding; public norm and rotation; syndrome of C; reconciliation success probability and efficiency (source-ambiguity)
• Section 3 opening: binary-input AWGN capacity interpretation: raw sphere-modulated variables x,y; transformed binary variables; conditioning on the public norm and rotation; binary-input AWGN law; SNR and mutual information in bits (source-ambiguity)
• Section 3: actual covariance matrices before and after a symmetric linear channel: An actual general Heisenberg linear-channel/noise form-domain model, together with the computed resource cross moment and its convergence. (hard)
• Section 3, Eq. (4): correlation series and its strict comparison with Z_TMS: actual correlation Z of Eq. (3); infinite factorial series in Eq. (4); V_A and Z_TMS (source-ambiguity)
• Section 3: Gaussian upper bound via effective transmission and excess noise: Continuous heterodyne conditioning of actual infinite-dimensional Eve densities and its finite raw Holevo functional, linked to the resource and channel. (hard)
• Section 3, Fig. 1: small equivalent noise and larger useful modulation variance: physical Z and Z_TMS; four-state correlation comparator; equivalent excess noise as a function of V_A; range of reasonable modulation variances (source-ambiguity)
• Section 3, Fig. 2: nearly order-of-magnitude key-rate advantage at 50 km: distance-to-transmission law; detector trust/noise model; two asymptotic rate functions; optimization over modulation variance; meaning of nearly an order of magnitude (source-ambiguity)
• Section 3, Fig. 3 and p.9: secret keys over distances of order 50 km with finite-size effects: finite-key formula; confidence region for transmission and excess noise; security-error allocation; signal and retained-block counting conventions; finite code failure probability; range and key positivity (source-ambiguity)
• Abstract and conclusions: superiority over all known practical CVQKD protocols: class of known practical comparison protocols; common physical and security parameters; rate and range ordering (source-ambiguity)
• Fig. 1 caption: one shot-noise unit of excess noise implies entanglement breaking: input-referred versus output-referred excess noise; shot-noise normalization; actual phase-insensitive channel; entanglement-breaking and secret-key impossibility (source-ambiguity)
• Appendix, Eq. (5): modulation-independent gains and added-noise variances: Fixed-channel quantum first/second moments for arbitrary input-uncorrelated noise under replacement of the probe modulation. (hard)
• Section 1: previously established Gaussian-modulation collective-attack security: Gaussian-modulation CVQKD protocol; collective-attack security criterion; measurement and reconciliation conventions (source-ambiguity)
• Section 1: previously established discrete-modulation security for linear channels: two-state/four-state protocol; reverse reconciliation; linear-channel attack model; security and key-rate criterion (source-ambiguity)
• Section 1: infinite-dimensional de Finetti reduction: infinite-dimensional de Finetti theorem; energy test or constraint; permutation symmetry; collective versus coherent attacks; security-parameter loss (source-ambiguity)
• Section 1, Eq. (1): asymptotic reverse-reconciliation key-yield expression: signed asymptotic yield K=beta I(x;y)-chi(y;E); mutual information and continuous Eve ensemble; privacy-amplification leakage; key-length normalization (source-ambiguity)
• Sections 1 and 3, Appendix: Gaussian extremality/optimality used to bound Eve: actual Gaussian and non-Gaussian oscillator densities; fixed complete moments; conditional quantum entropy/Holevo functional; Gaussian optimality hypotheses (source-ambiguity)
• Sections 1–3: cited low-SNR reconciliation efficiency: code and decoder family; SNR; block length; probability of decoding failure; efficiency beta (source-ambiguity)
• Sections 1 and 3: finite-size parameter-estimation corrections from earlier work: parameter confidence region; maximal compatible Holevo information; finite-key length formula; privacy-amplification and parameter-estimation errors (source-ambiguity)
• Section 4: cited decoy-state removal of the linear-channel restriction: decoy-state ensemble and mixing probabilities; overall Gaussian mixture; Gaussian parameter estimation; security without the linear-channel hypothesis (source-ambiguity)

Selected references

• Long distance quantum key distribution with continuous variables, arXiv:1005.0328v3, https://arxiv.org/abs/1005.0328v3

Motivation

Universality of local unitary transformations is one of the cornerstones of quantum computing with many applications and implications that go beyond this field. However, it has been recently shown that this universality does not hold in the presence of continuous symmetries: generic symmetric unitaries on a composite system cannot be implemented, even approximately, using local symmetric unitaries on the subsystems [I. Marvian, Nature Physics (2022)]. In this work, we study qubit circuits formed from k-local rotationally-invariant unitaries and fully characterize the constraints imposed by locality on the realizable unitaries. We also present an interpretation of these constraints in terms of the average energy of states with a fixed angular momentum. Interestingly, despite these constraints, we show that, using a pair of ancilla qubits, any rotationally-invariant unitary can be realized with the Heisenberg exchange interaction, which is 2-local and rotationally-invariant. We also show that a single ancilla is not enough to achieve universality. Finally, we discuss applications of these results for quantum computing with semiconductor quantum dots, quantum reference frames, and resource theories.

This mission is the statement-level formalization of Rotationally-Invariant Circuits: Universality with the exchange interaction and two ancilla qubits (arXiv:2202.01963v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main result: exchange universality with two ancillary qubits (Main result: exchange universality with two ancillary qubits, 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

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

• Unnumbered proposed extension beyond SU(2): A quantified beyond-SU(2) theorem specifying on-site and ancillary representations and the exact irrep-block phase-only reachability condition. (source-ambiguity)

Selected references

• Rotationally-Invariant Circuits: Universality with the exchange interaction and two ancilla qubits, arXiv:2202.01963v1, https://arxiv.org/abs/2202.01963v1

Motivation

We show that the positivity of the Wigner function of Gaussian states and measurements provides an elegant way to bound the discriminating power of "linear optics", which we formalise as Gaussian measurement operations augmented by classical (feed-forward) communication (GOCC). This allows us to reproduce and generalise the result of Takeoka and Sasaki [PRA 78:022320, 2008], which tightly characterises the GOCC norm distance of coherent states, separating it from the optimal distinguishability according to Helstrom's theorem. Furthermore, invoking ideas from classical and quantum Shannon theory we show that there are states, each a probabilistic mixture of multi-mode coherent states, which are exponentially reliably discriminated in principle, but appear exponentially close judging from the output of GOCC measurements. In analogy to LOCC data hiding, which shows an irreversibility in the preparation and discrimination of states by the restricted class of local operations and classical communication (LOCC), we call the present effect GOCC data hiding. We also present general bounds in the opposite direction, guaranteeing a minimum of distinguishability under measurements with positive Wigner function, for any bounded-energy states that are Helstrom distinguishable. We conjecture that a similar bound holds for GOCC measurements.

This mission is the statement-level formalization of Bosonic data hiding: power of linear vs non-linear optics (arXiv:2102.01622v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Bounded Wigner negativity bounds a binary measurement bias (Remark 4, (23), PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 8, (32)–(34): Full completed-oscillator adaptive GOCC instrument semantics, including partial homodyne spectral measures, variable vacuum ancillas, arbitrary Gaussian unitaries, measurable history-dependent controls, discrete coarse-graining, and strong-operator closure (hard)
• Section III, Definition 1 and (19)–(21): Full completed-oscillator adaptive GOCC instrument semantics, including partial homodyne spectral measures, variable vacuum ancillas, arbitrary Gaussian unitaries, measurable history-dependent controls, discrete coarse-graining, and strong-operator closure (hard)
• Lemma 3: Full completed-oscillator adaptive GOCC instrument semantics, including partial homodyne spectral measures, variable vacuum ancillas, arbitrary Gaussian unitaries, measurable history-dependent controls, discrete coarse-graining, and strong-operator closure (hard)
• Corollary 5, (24)–(26): Full completed-oscillator adaptive GOCC instrument semantics, including partial homodyne spectral measures, variable vacuum ancillas, arbitrary Gaussian unitaries, measurable history-dependent controls, discrete coarse-graining, and strong-operator closure (hard)
• Example 6, (27)–(30): Full completed-oscillator adaptive GOCC instrument semantics, including partial homodyne spectral measures, variable vacuum ancillas, arbitrary Gaussian unitaries, measurable history-dependent controls, discrete coarse-graining, and strong-operator closure (hard)
• Example 7, (31): Full completed-oscillator adaptive GOCC instrument semantics, including partial homodyne spectral measures, variable vacuum ancillas, arbitrary Gaussian unitaries, measurable history-dependent controls, discrete coarse-graining, and strong-operator closure (hard)
• Corollary 10, (45)–(48): Full completed-oscillator adaptive GOCC instrument semantics, including partial homodyne spectral measures, variable vacuum ancillas, arbitrary Gaussian unitaries, measurable history-dependent controls, discrete coarse-graining, and strong-operator closure (hard)
• Corollary 12, (51)–(55): A source-supported valid numerical energy/cutoff rank bound for the printed Corollary 12 constant (source-ambiguity)

Selected references

• Bosonic data hiding: power of linear vs non-linear optics, arXiv:2102.01622v1, https://arxiv.org/abs/2102.01622v1

Motivation

We prove a version of the data-processing inequality for the relative entropy for general von Neumann algebras with an explicit lower bound involving the measured relative entropy. The inequality, which generalizes previous work by Sutter et al. on finite dimensional density matrices, yields a bound how well a quantum state can be recovered after it has been passed through a channel. The natural applications of our results are in quantum field theory where the von Neumann algebras are known to be of type III. Along the way we generalize various multi-trace inequalities to general von Neumann algebras.

This mission is the statement-level formalization of Trace-and improved data processing inequalities for von Neumann algebras (arXiv:2102.07479v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Measured relative entropy bounds the unsquared fidelity penalty (Proposition 1, PDF p. 17). 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

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

• Theorem 1, (105)–(106): General Araki entropy and the support-corner averaged rotated Petz map (hard)
• Lemma 1, (16)–(18): Domain-aware extended Araki-Masuda norms for both exponent regimes (hard)
• Lemma 2, (28): A missing interior growth hypothesis in scalar Hirschman interpolation (source-ambiguity)
• Lemma 3: Incompatible nonfaithful support-zero norm continuity (source-ambiguity)
• Lemma 4, (37): Nonfaithful reference changes invalidate modular-power convergence on the full domain (source-ambiguity)
• Corollary 1, (50): General weighted norms and support-zero complex products with the r=1 endpoint measure (hard)
• Corollary 2, (53): General modular-power extended norm on arbitrary zeta (hard)
• Corollary 3, (59)–(60): Extended upper-semibounded affiliated perturbations, their sum and perturbed vectors (hard)
• Equation (81): Actual general Araki relative entropy and bounded perturbation partition value (hard)
• Equation (85): Actual spectral probability laws and entropy of all commutative restrictions (hard)
• Lemma 5, (115): Constructed Gamma, analytic Connes cocycle and script-Lp product identity (hard)
• Lemma 6; (109), (115), (126): Corrected cocycle derivative and domain-aware Araki-Trotter perturbed-vector limit (hard)

Selected references

• Trace-and improved data processing inequalities for von Neumann algebras, arXiv:2102.07479v2, https://arxiv.org/abs/2102.07479v2

Motivation

We experimentally demonstrate a controlled-phase gate for continuous variables in a fully measurement-based fashion. In our scheme, the two independent input states of the gate, encoded in two optical modes, are teleported into a four-mode Gaussian cluster state. As a result, one of the entanglement links present in the initial cluster state appears in the two unmeasured output modes as the corresponding entangling gate acting on the input states. The genuine quantum character of this gate becomes manifest and is verified through the presence of entanglement at the output for a product two-mode coherent input state. By combining our controlled-phase gate with the recently reported module for universal single-mode Gaussian operations [R. Ukai et al., Phys. Rev. Lett. 106, 240504 (2011)], it is possible to implement universal Gaussian operations on arbitrary multi-mode quantum optical states in form of a fully measurement-based one-way quantum computation.

This mission is the statement-level formalization of Demonstration of a Controlled-Phase Gate for Continuous-Variable One-Way Quantum Computation (arXiv:1107.0514v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Controlled-phase feedforward propagation preserves the output channel (Fig.1(b) and authors’ note [18], PDF p.4, 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:

• Abstract and Eq.(2): experimentally demonstrated cluster-based entangling gate: Exact experimental output state and statistical/calibration meaning of the witness uncertainty. (source-ambiguity)
• Eq.(1): Bell injection and feedforward implement the finite-squeezing noisy C_Z relation: Operational all-input four-outcome bosonic Bell/feedforward instrument with the actual finite-squeezed cluster resource. (hard)
• After Eq.(1): infinite-squeezing noise limit gives the ideal gate: All-state characteristic function of the same actual finite-r operational output channel. (hard)
• Unnumbered: optimal witness gain and finite resource threshold: Actual vacuum-output density and finite form-domain witness moments, linked to physical nonseparability. (hard)
• Fig.2(a): theoretical output variances for vacuum inputs: Observable finite second moments of the actual vacuum-output protocol density. (hard)
• Fig.2(b-e): theoretical coherent amplitudes are transmitted with unity gain: Actual coherent input/output densities and their finite first quadrature moments for the specified protocol. (hard)
• Abstract and conclusion: ideal C_Z plus universal one-mode Gaussian gates generate multimode Gaussian operations: Input-independent finite composition of ideal measurement-based Gaussian modules on arbitrary normal states. (hard)
• Figs.2-3: measured coherent transfer, quadrature noises, and witness gains: Raw measured traces and an explicit calibration/statistical model for the reported rounded data. (source-ambiguity)

Selected references

• Demonstration of a Controlled-Phase Gate for Continuous-Variable One-Way Quantum Computation, arXiv:1107.0514v1, https://arxiv.org/abs/1107.0514v1

Motivation

We construct a model for the string group as an infinite-dimensional Lie group. In a second step we extend this model by a contractible Lie group to a Lie 2-group model. To this end we need to establish some facts on the homotopy theory of Lie 2-groups. Moreover, we provide an explicit comparison of string structures for the two models and a uniqueness result for Lie 2-group models.

This mission is the statement-level formalization of A Smooth Model for the String Group (arXiv:1104.4288v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fibers of locally convex submersions are submanifolds (Corollary A.4, PDF p. 26). 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

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

• Introduction, unnumbered: no finite CW or finite-dimensional model: Three-connected-cover homotopy type and integral cohomology obstruction (hard)
• Theorem 3.7: Actual String_G bundle-automorphism group and compatible Frechet structures (hard)
• Lemma 2.3: Smooth gauge group with compact-open iterated-tangent topology (hard)
• Proposition 2.5: Canonical smooth-to-continuous gauge inclusion as a continuous map (hard)
• Proposition 2.7: Source hypotheses insufficient for the full printed result (source-ambiguity)
• Remark 2.8: Source hypotheses insufficient for the full printed result (source-ambiguity)
• Corollary 3.3: Smooth string-model kernel topology and homotopy groups (hard)
• Remark 3.4.1: Serre lifting property and actual local trivializations of q (hard)
• Remark 3.4.2: Nonfibrational three-connected-cover data and manifold finiteness (hard)
• Remark 3.8: Source hypotheses insufficient for the full printed result (source-ambiguity)
• Remark 3.9: Standard loop-group central extensions and norm-smooth unitary representations (hard)
• Lemma 4.4: Smooth strict Lie 2-group nerve and CGWH fat/ordinary realizations (hard)
• Proposition 4.5: Realization of a given smooth functor with object and arrow weak equivalences (hard)
• Proposition 4.7: Smooth weak equivalence and induced map on CGWH realizations (hard)
• Proposition 4.9: Smooth categorical pi groups, realization fiber sequence and actual kernel bundle (hard)
• Lemma 4.11: Source hypotheses insufficient for the full printed result (source-ambiguity)
• Remark 4.12: Identity-only 2-group of the actual constructed String_G and its realization (hard)
• Lemma 5.1: Frechet smooth circle mapping group and descended normalized Haar integral (hard)
• Proposition 5.3: Actual Haar-pushout gauge extension with quotient smooth structure (hard)
• Proposition 5.4: Descended precomposition action on the concrete gauge pushout (hard)
• Theorem 5.6: Concrete smooth STRING_G crossed-module groupoid and realization inclusion (hard)
• Remark 5.7: Path-bundle equivariant lifted gauge group and Haar pushout crossed modules (hard)
• Proposition 6.1: Principal 2-bundle bicategory and actual change-of-structure functor (hard)
• Proposition 6.3: Model morphisms preserving both identifications and bundle bicategories (hard)
• Lemma 6.4: Good-cover twisted groupoid, presented stacks and central stack extension (hard)
• Theorem 6.5: Source hypotheses insufficient for the full printed result (source-ambiguity)
• Lemma A.1: Supplied quotient Lie structure, non-split Lie subgroup and smooth principal trivializations (hard)
• Proposition A.3: Actual locally convex smooth pullback atlas and smooth universal property (hard)
• Remark A.5: Two smooth sites, groupoid-presented stacks and Hom-category restriction (hard)
• Lemma B.1: Smooth categorical component quotient and endpoint map to its actual fiber product (hard)
• Proposition B.2: Source hypotheses insufficient for the full printed result (source-ambiguity)
• Proposition B.3: Smooth essential-surjectivity domain and induced Lie pi_0 isomorphism (hard)
• Corollary B.4: Smooth weak equivalence of smoothly separable internal Lie categories (hard)
• Proposition B.5: Induced categorical Lie pi maps and smooth inverses (hard)

Selected references

• A Smooth Model for the String Group, arXiv:1104.4288v4, https://arxiv.org/abs/1104.4288v4

Motivation

Randomized load balancing assigns arriving jobs to servers without inspecting every server. Uniformly choosing one destination is inexpensive, but a small number of servers can accumulate substantially more work than the average. Sampling a fixed number of destinations and choosing a least-loaded one provides an alternative with little additional information cost. The same mathematical model describes bucket occupancy in multiple-choice hashing.

This mission concerns the classical finite equal-load theorem, not a new conjecture. Its source is Azar, Broder, Karlin and Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 180–200 (1999), DOI. The original conference version appeared at STOC 1994. The present mission is a Textbook/known-result exercise scoped to the finite n-balls/n-bins theorem, rather than a ResearchPaper mission claiming to cover the entire article.

Setting

Let B be a positive number of bins and let D ≥ 2 be a fixed number of choices. Start with B empty bins and allocate exactly B balls, one at a time. For each ball sample an ordered list of D bins independently and uniformly, with replacement. Choose a bin having minimum current load among these choices and add the ball there. Ties are broken by the earliest sampled position. Let M(B,D) denote the maximum final bin load.

The underlying finite sample space consists of all B-by-D arrays of bin labels. All arrays have equal probability, so repeated samples are permitted and both within-ball and between-ball choices are independent. The allocation procedure is deterministic once the array is fixed. The loads depend on the earlier choices through this procedure; they are not independent random variables.

Formalization targets

For every fixed integer D ≥ 2, the goal is the existence of a nonnegative constant C, depending on D but not on B or on the tolerated failure probability, such that

$$\Pr\left(\left|M(B,D)-\frac{\log\log B}{\log D}\right|\le C\right)\longrightarrow1\quad(B\to\infty).$$

The two milestones are the paper's Theorem 3.2, p. 184, the corresponding additive-constant upper bound, and Theorem 3.3, p. 186, the corresponding additive-constant lower bound. Their conjunction gives the displayed two-sided statement by a union bound. An unspecified additive constant absorbs the difference between strict and non-strict inequalities in the upper bound.

Significance

The case D = 2 is the power-of-two-choices phenomenon: the largest bucket is controlled at the doubly logarithmic scale. The goal retains the coefficient 1/log D and an additive constant, rather than weakening the result to an unspecified multiple of log log B. It also keeps D fixed before taking the limit in B; it does not assert uniformity when D grows with B.

The mathematical result is established in the cited paper. The work requested here is a machine-checked proof of this particular finite theorem. The proposed development supplies an operational model and precise probability predicates rather than assuming the maximum-load estimate as a hypothesis. The reusable objects are the allocation trace, greedy state transition, final load vector, maximum, and uniform finite-event probability.

The Prove2Me API queried on 2026-10-28 reports a related theorem, PowerTwoChoices.Asymptotics.theorem_4, as Proved. That theorem concerns an expected-time series in the limiting supermarket model as arrival intensity tends to one. It is not this finite maximum-load theorem. Its companion PowerTwoChoices.Limit.corollary_2 is Open. These platform statuses have not been independently rebuilt in this project.

Difficulty

Allocations are sequential and the state used by the next allocation depends on the previous choices. Treating bin loads or successive high-load events as independent would change the model. A correct proof must justify the probabilistic comparison used in the paper's layered argument and the asymptotic estimates that turn layer thresholds into a fixed additive constant. The lower bound also needs a high-probability statement, not merely an expectation estimate or a collection of successful simulations.

Formalization scope

Lean parameters are shifted: n : Nat represents B = n+1 bins and balls, while d : Nat represents D = d+2 choices. Thus all positive bin counts and all choice counts at least two are represented, with no empty sampling type. The first occurrence convention makes tie-breaking explicit. The probability of an event is its subtype cardinality divided by the cardinality of the complete trace type, interpreted in the real numbers. Its denominator is positive.

The functions Upper, Lower and TwoSided expand high probability as: there exists C ≥ 0 such that, for every ε > 0, there exists N such that the event has probability at least 1−ε for every n ≥ N. The order of these quantifiers is essential: C cannot depend on ε. Natural logarithms and real absolute values are used. The total definition of log at zero affects only the one-bin boundary and does not alter the limit; no finite small-size bound is claimed.

This exercise covers neither the paper's unequal number of balls and bins, stochastic optimality among online policies, deletion process, nor its offline assignment and hashing-cost results. Those are not silently inferred from this goal. All three theorem declarations currently contain explicit sorry placeholders because they are open targets. Compiling the statements checks syntax and types, not their truth. There are no completed theorem proofs or platform proof-graph edges in this project yet.

Selected references

• Y. Azar, A. Z. Broder, A. R. Karlin and E. Upfal. Balanced Allocations. SIAM J. Comput. 29(1), 180–200, 1999. Author-hosted full text. Model: §2, p. 183; upper bound: Theorem 3.2, p. 184; lower bound: Theorem 3.3, p. 186.
• M. Mitzenmacher. The Power of Two Choices in Randomized Load Balancing. IEEE TPDS 12(10), 1094–1104, 2001. DOI. Related queueing-model work, not the source of this finite theorem.

Motivation

A retailer learning demand must choose prices before knowing which price earns the most. Each sale provides information only at the price actually posted. A demand curve can have several locally attractive regions, so a method that searches near one apparent optimum can overlook a better region. Wang, Chen and Simchi-Levi study pricing under smoothness assumptions that allow such multimodal behavior in Multi-Modal Dynamic Pricing, supplied artifact, §§2–3. The mathematical question is how the smoothness order changes the cost of learning over a finite selling season.

Setting

A price interval is a nonempty compact real interval $P=[p_{\min},p_{\max}]$ with $0\le p_{\min}\le p_{\max}$. At each of $T$ rounds, a decision maker posts $p_t\in P$, observes demand $d_t\in[0,1]$, and receives revenue $p_td_t$. Decisions use previously observed prices and demands and may be randomized. There is no inventory constraint. The mean demand $f:P\to[0,1]$ is unknown. Its sequential interpretation requires the conditional demand law, given the history and current price, to have mean $f(p_t)$. Dependence on earlier observations is permitted; independent or Bernoulli demands are not required.

For an integer $k\ge1$ and $C>0$, the smoothness class $\Sigma^k(P;C)$ contains functions with $k-1$ successive derivatives on the interval, each bounded in absolute value by $C$, whose last derivative is $C$-Lipschitz. Order zero means the function itself. Thus $k=1$ requires bounded Lipschitz demand, without differentiability. The expected revenue is $r(p)=pf(p)$.

The two-level pricing algorithm partitions $P$ into $N$ equal closed bins. Each bin retains its cumulative revenue and its ordered observations. An upper confidence index chooses a bin. Within that bin, a ridge estimate based on the centered monomials $(1,p-a,\ldots,(p-a)^{k-1})$ determines an optimistic revenue function, maximized over the entire interval. The demand estimate is clipped above at one. These are the transitions in Algorithms 1–2, supplied artifact, p. 11; neither action space is replaced by a finite price grid.

The realized fixed-price benchmark follows the literal display on p. 9. A common response field $D_t(p,\omega)$ specifies counterfactual demands, and actual demand is its value at the posted price. Regret is

$$R_T(\omega)=\sup_{p\in P}\sum_{t=1}^T pD_t(p,\omega)-\sum_{t=1}^T p_t(\omega)d_t(\omega).$$

This fixes a stronger reading than expected regret or pseudo-regret. All bounded couplings with the prescribed fixed-price means and actual sequential observation law are included.

Formalization targets

The milestones are exactly Lemmas 1, 10, 2 and 3, in dependency order, from the supplied artifact, pp. 12, 33, 14 and 14. Lemma 1 asserts local polynomial approximation with both error $C(b-a)^k$ and factorial coefficient bounds. Lemma 10 asserts simultaneous concentration over every positive-definite matrix, with radius $\sqrt{2k\log(4kt/\delta)}+2$. Lemma 2 bounds a single local call's revenue gap by

$$2p_{\max}\min\{1,\gamma\sqrt{\phi(\widehat p)^\top\Lambda^{-1}\phi(\widehat p)}+\Delta\},$$

where $\gamma=C\sqrt k+\Delta\sqrt t+\sqrt{2k\log(4kt/\delta)}+2$. Lemma 3 asserts the average local pseudo-regret bound $(\Delta+\max\{1,C\}/\sqrt t)3k\log(2kT)$ with failure probability $O(T^{-1})$.

The goal is Theorem 1, equation (3), p. 11. Write $L=p_{\max}-p_{\min}$ and use $N=\lceil T^{1/(2k+1)}\rceil$, $\Delta=C(L/N)^k$. For fixed $k,C,p_{\min},p_{\max}$, there exist $A,B>0$ and an integer $m\ge0$ such that every positive integer $T\ge L^{2k+1}$ satisfies

$$\mathbb P^*\left(R_T>A\sqrt T\log(2T)^m+3k\log(2kT)[4\max\{1,C\}+CL^k]T^{(k+1)/(2k+1)}\right)\le B/T.$$

The constants are chosen before demand functions, horizons, noise laws and tie choices. The displayed explicit coefficient is unchanged. The resulting $\widetilde O(T^{(k+1)/(2k+1)})$ upper rate follows from this bound for fixed parameters, since its exponent is at least $1/2$.

Significance

The paper's claim relates smoother demand to a smaller horizon exponent without imposing unimodality. Formalizing its precise content distinguishes this claim from stronger assumptions that could simplify the pricing problem. The deliverable contains concrete stochastic and algorithmic definitions and five unproved statements. Compilation verifies that these are well-typed declarations; it does not establish their truth. The already proved elliptical-potential lemma is included as background infrastructure, with its existing platform identifier, rather than posed again.

The source also contains defects relevant to these claims. Recording them makes the distinction between a printed statement and a valid theorem explicit. A proof or disproof must address the stated target; a corrected result would be a separate contribution.

Difficulty

The source's concentration statement quantifies over all positive-definite matrices. Its proof instead uses additional bounds appropriate to a regularized design matrix. The printed lemma is false: with $k=t=1$, fair centered Bernoulli noise $\pm1/2$, feature $1$ and $\Lambda=1/400$, the ellipsoid supremum is $10$, above $\sqrt{2\log8}+2$ at $\delta=1/2$. This is finding I1.

The initialized empty histories also make Algorithm 2's printed radius contain $\log0$. Every feasible first price is therefore covered, followed by its exact defined transitions, rather than supplying a favorable initialization. Finding I2 records the omission. Findings I3 and I5 identify a coefficient derivation gap and inconsistent uncentered explanatory features. Finding I4 shows that smooth mean demand alone does not control the realized supremum: independent Bernoulli responses at countably many rational prices can give a linear hindsight advantage. These observations concern the source statements and proofs, pp. 9–15 and 32–33, and remain attached to the unchanged targets.

Formalization scope

Real functions are restricted to closed intervals through within-set derivatives. Ordered lists retain repeated data, matrices and coefficient vectors use finite coordinate types, and time starts at zero. Markov kernels and filtrations represent sequential probability laws on arbitrary probability spaces. Bad events use outer probability. The finite real supremum agrees with the relevant benchmark on a full-measure set because demands are bounded. No successful confidence event is built into an algorithm definition.

The smoothness helpers and deterministic approximation lemma allow arbitrary real endpoints. The pricing performance statements retain nonnegative prices, including singleton intervals; negative prices would invalidate the signed revenue comparison in Lemma 2. A predecision filtration may contain additional information only when the same history-and-price kernel remains the conditional demand law. All maximizing ties are covered. The undefined first call is quantified universally; $T=1$ is retained. The exact derivative, probability, indexing and asymptotic conventions are listed with every theorem's differences metadata.

The limited-inventory extension, lower bound and improved special-case rates are outside this mission. The citation basis remains the supplied metadata's “published,” although the artifact has an SSRN footer and manuscript pagination. All page citations refer to that exact 37-page artifact, with printed and PDF pages equal.

Selected references

• Wang, Chen and Simchi-Levi, Multi-Modal Dynamic Pricing, Management Science, DOI 10.1287/mnsc.2020.3819. Catalog year 2019; supplied artifact with SSRN 3489355 footer. The journal issue year and pagination are not independently asserted here.
• Lattimore and Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Lemma 19.4, p. 243: the elliptical-potential lemma used as proved background.

Motivation

A seller learning demand from sales data also changes the conditions under which that data is generated. Customers may compare today's price with a reference formed from earlier prices. A price experiment can therefore affect both current sales and future demand. The seller observes prices and sales, while the reference price remains hidden. This mission concerns the slow-moving pricing policy in den Boer and Keskin, Dynamic Pricing with Demand Learning and Reference Effects, using the supplied April 19, 2021 artifact.

The relevant question is quantitative: how much cumulative revenue does this policy lose against a seller who knows the demand parameters and the reference mechanism? A guarantee must account for the cost of learning and the consequences of changing customers' reference prices. The target includes mechanisms whose smoothing coefficient changes over time and whose reference price can reset.

Setting

A price interval is the entire real interval $I=[\ell,u]$, with $0\le\ell<u$. The seller has a demand parameter $\theta=(\alpha,\beta,\eta^+,\eta^-)$ in a known bounded rectangle intersected with $\eta^+\le\eta^-$. Here $\alpha\ge0$, $\beta>0$ and the reference sensitivities are nonnegative. The expected demand and revenue are

$$d(p,r,\theta)=\alpha-\beta p+\eta^+(r-p)^+-\eta^-(p-r)^+, \qquad R(p,r,\theta)=p\,d(p,r,\theta).$$

For every allowed parameter vector, demand is nonnegative on $I^2$ and $\alpha/(2\beta)$ lies strictly inside $I$. Equality of the sensitivities and zero sensitivities are allowed. Observed demand adds an independent shock. The shocks are identically distributed, have mean zero and finite variance, and possess a finite moment generating function in some neighborhood of zero. Their law need not be Gaussian or bounded, and zero variance is allowed.

A reference mechanism is a continuous map from each finite price history to a reference in $I$. In the class $\mathcal R_{ES}$, one coefficient $\zeta\in[0,1)$ gives $r_{t+1}=\zeta r_t+(1-\zeta)p_t$. The larger class $\mathcal R_G$ has change times $\tau_1=1$ and coefficients $\zeta_k\in[0,1)$. Smoothing applies between changes; at a change the reference may reset continuously as a function of the full preceding price history. For some fixed finite $c>0$, every interval $(s,t]$ with positive integers $s<t$ contains at most $c\sqrt{t-s}$ changes. Infinitely many changes are permitted, as are coefficients tending to one. These are the mechanisms of Section 3.3, without an additional uniform contraction condition.

The slow-moving policy divides time into episodes $i\ge1$, each comprising two blocks of $2^i$ periods. With $\delta_i=c_0 2^{-i/4}$, it charges the previous price estimate minus or plus $\delta_i$, clipped at the appropriate price endpoint. At each completed episode it fits a linear demand model to that episode alone, projects the intercept and slope separately onto their known intervals, and updates its price estimate. The policy uses observed price-demand pairs, never the reference, unknown demand parameters or change schedule.

Formalization targets

The goal is Theorem 3 of the supplied source, printed and PDF page 17. Fix the model, an admissible noise process, a mechanism in $\mathcal R_G$, $\theta\in\Theta$, tuning $0<c_0<2^{-3/4}(u-\ell)$ and allowed initial estimates. The claim is

$$\exists c_6>0\quad\forall T\ge1:\quad \Delta_S(T,\rho,\theta)\le c_6\sqrt T.$$

The constant is finite and chosen before the horizon. Here regret compares the policy with the full dynamic clairvoyant benchmark

$$\Pi^*(T,\rho,\theta)=\sup_{(p_1,\ldots,p_T)\in I^T} \sum_{t=1}^{T}R(p_t,\rho_t(p_1,\ldots,p_{t-1}),\theta).$$

The three milestones retain their source numbering and dependency order. Proposition 2, page 17, asserts the same regret rate under two uniform sufficient conditions: the fixed price $\alpha/(2\beta)$ loses at most $c_4\sqrt T$, uniformly also over $\Theta$, and holding any price after any history incurs total reference deviation at most $c_5\sqrt{t-s}$. Theorem 1, page 10, gives a horizon-independent fixed-price loss bound for $\mathcal R_{ES}$. Proposition 1, page 13, bounds the sum of absolute reference deviations by one constant under the same exponential-smoothing class. Neither sufficient condition from Proposition 2 is a premise of the goal.

Significance

The printed result provides a square-root upper bound for a concrete learning rule when reference prices are hidden and can change their updating behavior. It compares that rule with all dynamic feasible price vectors, rather than with a fixed-price substitute. The claim applies to each finite prefix, including horizons that end before an episode or a block is complete.

Formalizing these statements makes the causal algorithm, the benchmark and the quantifier order explicit. The resulting definitions separate continuous reference mechanisms and iid noise from the specific demand model. All four theorem items are open statement targets in this mission; no machine-checked proofs of them are claimed. The source's description as asymptotic optimality is retained, but an independent minimax lower bound is outside the mission.

Difficulty

Holding a price fixed need not make its reference track it at a rate that is uniform across infinitely many regimes. Each coefficient being strictly below one does not place the entire sequence below a common number less than one. The source proof of Theorem 3 uses maxima over the regimes encountered before the horizon as though they yielded horizon-independent constants. The recorded finding supplies an allowed mechanism for which its intermediate tracking bound fails. This identifies a proof gap, not a disproof of the policy's regret conclusion.

The theorem remains the full printed target. Adding uniform contraction, limiting the number of changes or assuming the desired tracking bound would change the result. The nondifferentiable demand function, adaptive estimates and latent reference dynamics also have to be handled under the actual observation model.

Formalization scope

Prices remain real interval elements. Continuous maps describe references, extended naturals describe change times, and finite products describe histories. Internally, period zero represents source period one; positive horizons and source interval endpoints retain explicit guards. The algorithm is a causal recursion with compatible finite prefixes. Its least-squares update uses the explicit unique two-block solution, followed by the original coordinate projections. Prices are interval-valued; full clipping equals the printed one-sided clipping because the allowed projected center is interior. Real negative quarter powers determine perturbations.

The history domain is extended to real observations, agreeing with the printed nonnegative-history convention wherever it applies and accommodating the additive-noise model. Expected demand remains nonnegative; realized demand is not truncated. The benchmark is a real supremum of a continuous function on a nonempty compact box. Expected policy revenue is a Bochner integral of a bounded measurable finite-horizon random variable. Default values for unbounded suprema or nonintegrable functions therefore cannot trivialize the statements.

Definitions contain no regret or estimator-accuracy assumptions. The scope consists of the goal and its three specified milestones, with their shared foundations. Other results on incumbent pricing, gain-seeking behavior and statistical tests are intentionally excluded. Contributions establishing the full claims or resolving the recorded source findings must preserve these domains and quantifiers.

Selected references

• Arnoud V. den Boer and N. Bora Keskin, Dynamic Pricing with Demand Learning and Reference Effects, Management Science, supplied April 19, 2021 artifact marked “Forthcoming in Management Science,” first version December 23, 2017. DOI: 10.1287/mnsc.2021.4234. This mission preserves the repository's published citation basis and the supplied artifact's numbering: main pages 7–17 and electronic companion pages 1–17, PDF pages 33–49.