All missions

Motivation: ordinary multiplication over a fixed field

Polynomial multiplication is a basic operation in computer algebra: two coefficient lists must be converted into the coefficient list of their product. Its bit complexity depends on the coefficient field and the permitted machine operations. For a field fixed before the input length varies, Harvey and van der Hoeven established the unconditional benchmark $O_q(n\log n\,4^{\log^*n})$ using cyclotomic coefficient rings. Their later $O(n\log n)$ finite-field theorem has an explicit Linnik hypothesis; the conditional and unconditional results must be distinguished. 2019 paper, 2022 paper

The research preprint Ordinary Binary Polynomial Multiplication below $n\log n$ claims a strict saving in the logarithmic exponent for ordinary multiplication over $\mathbb F_2$. It builds on those arithmetic foundations and on recent finite-network and transform constructions. The present target is the preprint's precise main theorem, not a new claim of priority or an endorsement of its written proof. Preprint, Theorem 9

Setting: literal input, output and machine steps

The binary field $\mathbb F_2=\{0,1\}$ has addition modulo two. For $n\ge1$, inputs $a,b:\operatorname{Fin}(n)\to\{0,1\}$ represent

$$A(X)=\sum_{i=0}^{n-1}a_iX^i,\qquad B(X)=\sum_{i=0}^{n-1}b_iX^i.$$

The ordinary product has the exact output length $2n-1$, in ascending degree order. Its coefficient $c_j$ is $\sum_{i+k=j}a_i b_k$ in $\mathbb F_2$. Zero inputs and zero coefficients at the high-degree end remain literal input and output bits. This is neither an integer product with carries nor multiplication modulo $X^n-1$. Preprint, scope and main theorem

A deterministic multitape Turing machine has a fixed finite alphabet, fixed finite control and a fixed finite number of tapes. One transition reads only scanned cells, writes only scanned cells and moves each head by at most one cell. The shared formal machine model has a read-only input tape, a separate output tape and one-way tapes with preserved origin markers. The input is the two coefficient words separated by $\#$; all work tapes start blank after their markers. Shared machine definition

Formalization targets: the selected binary bound

Put $L(n)=\max\{1,\lceil\log_2n\rceil\}$ and $\kappa_*=2^{-38}=1/274877906944$. The goal is the following existence statement from Theorem 9:

$$\exists M\;\exists C>0\;\exists n_0\;\forall n\ge1\;\forall a,b:\operatorname{Fin}(n)\to\{0,1\}\;\exists t\in\mathbb N,$$ $$M(a\#b)\text{ halts with all coefficients of }A B\text{ after }t\text{ transitions},$$ $$n\ge n_0\quad\Longrightarrow\quad t\le CnL(n)^{1-\kappa_*}.$$

The machine, alphabet, tape count, control, constant and threshold are chosen before $n,a,b$. Halting and correctness include lengths below the eventual time threshold. The output tape contains its origin marker, exactly $2n-1$ coefficient symbols and then only blanks. Theorem 9, shared output convention

The initial supporting milestone is Corollary 10. In the notation above, its target is

$$\forall F\text{ a finite field of characteristic }2,\qquad \exists M_F\;\exists C_F>0\;\exists n_{0,F}:\quad T_F(n)\le C_F nL(n)^{1-\kappa_*}\quad(n\ge\max\{1,n_{0,F}\}).$$

Here $T_F(n)$ bounds the actual transition count for every pair of length-$n$ coefficient lists over $F$. A positive bit width and an injective encoding of $F$ are chosen before the inputs; the complete output has $2n-1$ coefficients in that encoding. Correct halting is required for every positive length. Each field is fixed individually; neither the machine nor its constants must be uniform as the field grows. Corollary 10

The paper's Proposition 1 and Lemmas 2–8 and 11–15 provide internal interchange, routing, host-initialization, arithmetic and execution results. A separate source map records them for possible later decomposition. They are not additional formal milestones in this initial draft. Main text and appendices

Significance: a complete bit-complexity statement

A proof would establish an attained positive saving below logarithmic exponent one for ordinary binary coefficient input and output. It would resolve the particular transfer claimed by this preprint, including the costs of the constructions between its algebraic endpoints. It would not establish a practical speed advantage, a growing-field uniform bound, or the sharper odd-characteristic claim from the separate companion paper. Theorem 9 and Corollary 10

The formalization must connect finite algebraic identities to a complete uniform computation. The manuscript and its internal AI-assisted inspections supply written arguments; independent human proof review and complete theorem-level Lean verification remain outstanding. Substantial generative AI assisted exploration, construction, writing and review, and historical model versions were not consistently recorded. Preprint status and AI disclosure

No completed Lean proof of either target is supplied with this draft. Local type checking against the platform environment is also incomplete; the draft statements must pass the platform's compilation check before submission can proceed. The goal and milestone are requests for formal verification of the stated research claims, with their full computation and cost obligations intact.

Difficulty: movement, representation and uniformity

An efficient arithmetic circuit alone does not establish the desired time bound. Its wires must be realized as charged movements on fixed tapes, including arbitrary payload, dirty workspace, address metadata, padding, scalar preparation and cleanup. A finite successful test cannot establish that one fixed program works at every input length. Proposition 1 and the machine ledger

Likewise, a fast transform on a convenient address grid does not automatically compute an ordinary polynomial product. The correspondence between original coefficient positions, residue indices, transform frequencies and the complete output must be exact. Roundtrip and product checks alone can miss a consistent permutation of Fourier frequencies. Separate coefficient components and temporarily extended coefficient lanes must retain their specified meanings and lifetimes. Lemma 8

The cited OpenAI integer-interchange and exact-complex-DFT manuscripts provide antecedents in their stated models. Neither global result is a substitute for the finite-field bit-complexity theorem requested here. Interchange source, local transform source

Formalization scope: shared foundations and explicit bridges

Binary coefficients are Booleans interpreted in Mathlib's ZMod 2; full-product equality uses Mathlib's Polynomial. The extension-field milestone quantifies over Mathlib fields with finite carriers and characteristic two, using a fixed injective coefficient encoding. The machine foundation is the existing IntMul.MultitapeTM definition. Its integer-value and integer-product predicates are not the polynomial task. The task-specific definitions specify coefficient lists, exact polynomial output and eventual transition bounds, with rational saving $\kappa_*$ interpreted in a real-valued envelope. Shared definition, Theorem 9, Corollary 10

The paper permits a fixed finite alphabet and sequential tapes; the existing local foundation uses two-way integer-indexed tapes with four symbols and output on tape zero. The shared platform convention instead has one-way tapes, a read-only input and separate output. A charged constant-overhead simulation and layout adapter is an explicit bridge obligation before the local development can be reused as a proof in that model. The goal uses the paper's ceiling-log envelope directly.

Supplying an assumed fast multiplier or declaring the desired time contract as an axiom does not meet the target. Reusable contributions include faithful coefficient and encoding lemmas, tape-model adapters, exact component theorems and composition with explicit costs. Every contribution must preserve its actual hypotheses; fixed finite checks and conditional implications retain their narrower scope.

Selected references

• Árpád Csizmadia, Ordinary Binary Polynomial Multiplication below $n\log n$: Controlled tensor routing on fixed tapes, research preprint, version 0.1.0, 2026, Theorem 9 and appendices. Pinned source, status.
• David Harvey and Joris van der Hoeven, Faster polynomial multiplication over finite fields using cyclotomic coefficient rings, Journal of Complexity 54, 101404, 2019. DOI.
• David Harvey and Joris van der Hoeven, Polynomial multiplication over finite fields in time $O(n\log n)$, Journal of the ACM 69(2), Article 12, 2022. DOI.
• Arnold Schönhage and Volker Strassen, Schnelle Multiplikation großer Zahlen, Computing 7, 281–292, 1971. DOI.
• OpenAI, Integer multiplication below $n\log n$, research preprint, 23 September 2026, Sections 3–4. Pinned interchange source.
• OpenAI, An explicit power saving for the exact discrete Fourier transform, research preprint, 25 September 2026, local compiler section. Pinned source.
• avi, Multitape Turing machines and exact integer multiplication in time $O(g(n))$, Prove2Me definition IntMul_MultitapeModel, 2026. Definition.

Motivation

The completely bounded trace and spectral norms in finite dimensions are shown to be expressible by semidefinite programs. This provides an efficient method by which these norms may be both calculated and verified, and gives alternate proofs of some known facts about them.

This mission is the statement-level formalization of Semidefinite programs for completely bounded norms (arXiv:0901.4709v2). 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 Explicit SDPs for completely bounded norms (Abstract and §3: explicit SDPs for completely bounded trace and spectral norms, 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

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

• Theorem 1 (Weak duality): General Hermiticity-preserving operator-inequality SDP weak duality, including extended-real empty feasible-set values (hard)
• Theorem 2 (Slater-type condition for strong duality): Both full Slater implications for the general operator-inequality SDP, with opposite-side attainment and the correct finite-value premise (hard)
• Theorem 4 (well-bounded SDP approximation): Rationally encoded well-bounded SDP approximation with deterministic Turing bit runtime (hard)
• Theorem 6 (Uhlmann’s Theorem): Arbitrary-PSD fixed-purification Uhlmann theorem, with both rank bounds and an attained overlap maximum (hard)
• Theorem 9 (Alberti’s Theorem): Alberti product infimum for arbitrary PSD P,Q over all positive definite Z (hard)
• Section 3, Computational efficiency; pp.10–11: One uniform finite deterministic bit-machine with a self-delimiting binary codec for n,m,r,A,B and unary precision k, rational output decoding, and actual step-count bounds tied to encoded length (hard)

Selected references

• Semidefinite programs for completely bounded norms, arXiv:0901.4709v2, https://arxiv.org/abs/0901.4709v2

Motivation

We extend the concept of the relative error to mixed-state cloning and related physical operations, in which the ancilla contains some a priori information about the input state. The lower bound on the relative error is obtained. It is shown that this result contributes to the stronger no-cloning theorem.

This mission is the statement-level formalization of Lower bound on the relative error of mixed-state cloning and related operations (arXiv:quant-ph/0208159v2). 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 Relative-error lower bound for two mixed-state clones (§IV, Theorem (i)–(ii), Eq. (15), 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

• Lower bound on the relative error of mixed-state cloning and related operations, arXiv:quant-ph/0208159v2, https://arxiv.org/abs/quant-ph/0208159v2

Motivation

The use of entangled light to illuminate objects is shown to provide significant enhancements over unentangled light for detecting and imaging those objects in the presence of high levels of noise and loss. Each signal sent out is entangled with an ancilla, which is retained. Detection takes place via an entangling measurement on the returning signal together with the ancilla. Quantum illumination with e bits of entanglement increases the effective signal-to-noise ratio of detection and imaging by a factor of 2^e, an exponential improvement over unentangled illumination.

This mission is the statement-level formalization of Quantum Illumination (arXiv:0803.2022v2). 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 Detection: a factor of d = 2^e in effective SNR (Unnumbered main detection result; abstract and (9),(14), 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

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

• Thermal truncation and thermalization error estimates, before (1.1): An unambiguous full-Fock thermal parameter and exact thermalization channel, specified norm, and a valid leading-coefficient expansion for both displayed errors. This requires an authorial correction; a generic O((db)^2) bound is not the printed result. (source-ambiguity)
• Operational trial requirements in good/bad unentangled regimes: A specified sequential/fixed-sample decision rule, target error probabilities, averaging convention, and joint limiting hierarchy that yields the claimed numerical coefficient 8 for trials. A Chernoff-rate identity alone cannot select these. (source-ambiguity)
• Low-order unentangled Chernoff expansion (5): A precise joint filter for (b,eta) and constants uniform over the stated s domain that bound the difference between the exact minimized overlap and (5) by C(b^2+eta*b), or an independently moderated correction to the remainder. (source-ambiguity)
• Good-regime displayed remainder (6): A valid specified hierarchy under which the optimized exact Chernoff factor differs from 1-eta by O((db)^2), or a corrected error scale with independent moderation. The b/eta -> 0 condition by itself is insufficient. (source-ambiguity)
• Bad-regime displayed Chernoff expansion (7): A joint asymptotic hierarchy controlling eta/b, the cubic Taylor remainder eta^3/b^2, and all discarded thermal terms at the printed O(b^2+eta*b) scale. The inequality eta<b alone is insufficient. (source-ambiguity)
• Low-order entangled Chernoff expansion, second line of (11) on p.7: For each fixed d, a specified joint small-parameter filter and a valid uniform remainder in s/minimization proving the second line of (11), or a corrected remainder independently moderated. Its exact first line is already stated. (source-ambiguity)
• Entangled bad-regime expansion (13) and trial reduction: A joint small-ratio hierarchy for eta*d/b and a valid printed remainder, together with a defined testing-error/stopping criterion for the claimed factor-d reduction in trials. (source-ambiguity)
• Imaging: potential exponential SNR enhancement and practical caveat: A specified spatial propagation/noise model, detector-efficiency model, imaging task and loss/accuracy criterion, and an advantage theorem in those terms. The source explicitly leaves practical spatial-mode analysis open. (source-ambiguity)

Selected references

• Quantum Illumination, arXiv:0803.2022v2, https://arxiv.org/abs/0803.2022v2

Motivation

We propose a family of exactly solvable toy models for the AdS/CFT correspondence based on a novel construction of quantum error-correcting codes with a tensor network structure. Our building block is a special type of tensor with maximal entanglement along any bipartition, which gives rise to an isometry from the bulk Hilbert space to the boundary Hilbert space. The entire tensor network is an encoder for a quantum error-correcting code, where the bulk and boundary degrees of freedom may be identified as logical and physical degrees of freedom respectively. These models capture key features of entanglement in the AdS/CFT correspondence; in particular, the Ryu-Takayanagi formula and the negativity of tripartite information are obeyed exactly in many cases. That bulk logical operators can be represented on multiple boundary regions mimics the Rindler-wedge reconstruction of boundary operators from bulk operators, realizing explicitly the quantum error-correcting features of AdS/CFT recently proposed by Almheiri et. al in arXiv:1411.7041.

This mission is the statement-level formalization of Holographic quantum error-correcting codes: Toy models for the bulk/boundary correspondence (arXiv:1503.06237v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Operator pushing preserves the operator norm (§2, operator pushing (2.3), 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

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

• Theorem 1: the holographic pentagon encoder (seed paper result): RegularTilingPatch and normalized NetworkContraction (hard)
• Theorem 2: exact connected-region lattice RT formula: PlanarDiscNetwork, its dual-distance condition, and cut contraction (hard)
• §4.2: greedy closure is well defined and defines an isometry: GreedyWedge with actual half-edge eligibility and contracted map (hard)
• Theorem 3: entropy lower bound from common greedy-cut links: Complementary greedy cuts and common-link residual factorization (hard)
• §4.2: no bipartite residual region implies exact RT: Residual-region emptiness modulo balanced unitary cut moves (hard)
• §4.3: local-unitary entanglement distillation and multipartite map: Greedy-induced local unitaries and register decompositions (hard)
• §4.3: O(1) residual-region claim (heuristic): A precise discrete residual-size theorem (source-ambiguity)
• §4.4: tripartite information from isolated residual tensors: Four-party greedy residual components and their tensor factors (hard)
• Theorem 5: connected causal-wedge reconstruction: CausalWedge, actual code encoder, and supported matrix reconstruction (hard)
• §5.5: disconnected causal and greedy entanglement wedge reconstruction: Componentwise causal wedge and simultaneous greedy entanglement wedge (hard)
• §5.5: explicit reconstruction beyond the causal wedge (Figure 13): The finite Figure-13 patch, two explicit intervals, and central algebra maps (hard)
• §5.6: weight-two logical obstruction in the triangle code: Recursive triangle-tree contraction and the X/X-inverse path representative (hard)
• §5.6: weight-four logical obstruction and absence of erasure threshold: Figure-16b leaf family and signed five-qubit cancellation (hard)
• §5.6 / Appendix D.2: positive threshold for the pentagon/hexagon code: Alternating pentagon/hexagon patches and actual iid recovery events (hard)
• Theorem 6: perfect stabilizer tensor networks give stabilizer codes: Perfect stabilizer local-state network and its Clifford composition (hard)
• §5.7: composition of stabilizer encoding isometries: Partial-wire Clifford encoder composition and generated output stabilizer (hard)
• §5.7: efficient computation of stabilizer and encoder: Finite network-to-tableau/Clifford program and uniform operation bound (hard)
• §5.8: disconnected reconstruction obstructs local stabilizer generators: Explicit Figure-13 encoder and derived complement representations of the full central logical algebra, including spectator logical factors (hard)
• §6: puncturing the central tensor and black-hole microstate count: Central deletion operation, horizon encoder and old-range inclusion (hard)
• Appendix B: unitary circuit interpretation criterion: Tensor network sequential evaluation under a topological wire schedule (hard)
• Appendix C.1: exact tensor counts and asymptotic pentagon-code rate: Graph-derived layer counts of actual {5,4} truncations (hard)
• Appendix C.2: best/worst connected central reconstruction in the pentagon code: Figure-21/22 connected regions and endpoint-pruned patch counts (hard)
• Appendix C.2: parity-dependent pentagon/hexagon code rate (C.11): Free logical/physical leg counts of alternating mixed patches (hard)
• Appendix C.2: pentagon/hexagon connected reconstruction fractions (C.12): Actual mixed-patch favorable/worst connected greedy reconstruction regions (hard)
• Theorem 7: analytic single-qubit hexagon erasure bound: Single-qubit hexagon patches and hierarchical recovery events (hard)
• Appendix E.1: local Fourier symmetries induce global code duality: Bipartite network Fourier action and supported logical duality (hard)
• Appendix E.1: recovery on either side for one self-dual CSS logical qudit: Prime-dimensional CSS logical-support algebra and full either-side reconstruction (hard)
• Appendix E.1, footnote 12: stronger 2k−2 claim: Scope and restricted support-rank calculation for footnote 12 (source-ambiguity)
• Appendix E.2: typical residual tensors and approximate reconstruction (conjecture): Distribution on perfect tensors and a quantitative approximate recovery statement (source-ambiguity)

Selected references

• Holographic quantum error-correcting codes: Toy models for the bulk/boundary correspondence, arXiv:1503.06237v2, https://arxiv.org/abs/1503.06237v2

Motivation

Previous work on symmetric group equivariant neural networks generally only considered the case where the group acts by permuting the elements of a single vector. In this paper we derive formulae for general permutation equivariant layers, including the case where the layer acts on matrices by permuting their rows and columns simultaneously. This case arises naturally in graph learning and relation learning applications. As a specific case of higher order permutation equivariant networks, we present a second order graph variational encoder, and show that the latent distribution of equivariant generative models must be exchangeable. We demonstrate the efficacy of this architecture on the tasks of link prediction in citation graphs and molecular graph generation.

This mission is the statement-level formalization of The general theory of permutation equivarant neural networks and higher order graph variational encoders (arXiv:2004.03990v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Fourier blocks classify equivariant linear layers and their dimension (Theorem 3 (§4): Fourier block classification and exact parameter count; headline selected from the paper-level seed, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• §4, unnumbered: ambiguous symmetric second order type: Unspecified symmetric activation subspace (source-ambiguity)
• Abstract and §6.1: necessity claim for exchangeable latent distributions: Meaning of equivariance for a random generative model (source-ambiguity)
• §7: necessity of k-th order architecture (unnumbered conclusion claim): Correct learning, relation class and permitted lower-order architectures (source-ambiguity)

Selected references

• The general theory of permutation equivarant neural networks and higher order graph variational encoders, arXiv:2004.03990v1, https://arxiv.org/abs/2004.03990v1

Motivation

The Peres-Horodecki criterion of positivity under partial transpose is studied in the context of separability of bipartite continuous variable states. The partial transpose operation admits, in the continuous case, a geometric interpretation as mirror reflection in phase space. This recognition leads to uncertainty principles, stronger than the traditional ones, to be obeyed by all separable states. For all bipartite Gaussian states, the Peres-Horodecki criterion turns out to be necessary and sufficient condition for separability.

This mission is the statement-level formalization of Peres-Horodecki separability criterion for continuous variable systems (arXiv:quant-ph/9909044v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-mode Gaussian Peres–Horodecki separability criterion (Theorem, PDF p.4 (announced p.1): two-mode Gaussian Peres–Horodecki criterion, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Equations (1), (4), (5): Canonical all-Hilbert–Schmidt one- and two-mode Wigner transforms on the real Hermite/Fock realization, with source normalization and reflection pullbacks on L2. (hard)
• Equations (13)–(14): All-input Wigner covariance law (13) bundled in the plan with active covariance law (14), and the full Fock/Hermite adapter for its actual conjugated density. (hard)
• Equation (17): Source-supplied nonvacuous matrix domain or extra physicality guard for the claimed equivalence (17). (source-ambiguity)
• Closing paragraph before Note Added: Named family, quantifier domain, kernel normalization and distributional regularity for “other quasi-probability distributions”. (source-ambiguity)

Selected references

• Peres-Horodecki separability criterion for continuous variable systems, arXiv:quant-ph/9909044v1, https://arxiv.org/abs/quant-ph/9909044v1

Motivation

A striking feature of quantum error correcting codes is that they can sometimes be used to correct more errors than they can uniquely identify. Such degenerate codes have long been known, but have remained poorly understood. We provide a heuristic for designing degenerate quantum codes for high noise rates, which is applied to generate codes that can be used to communicate over almost any Pauli channel at rates that are impossible for a nondegenerate code. The gap between nondegenerate and degenerate code performance is quite large, in contrast to the tiny magnitude of the only previous demonstration of this effect. We also identify a channel for which none of our codes outperform the best nondegenerate code and show that it is nevertheless quite unlike any channel for which nondegenerate codes are known to be optimal.

This mission is the statement-level formalization of Degenerate Quantum Codes for Pauli Channels (arXiv:quant-ph/0604107v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-Pauli Channels are Special: nondegradability on the whole open noise interval (Two-Pauli Channels are Special: nondegradability on the whole open noise interval, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Main coding claim: nonzero cat rate at the hashing point for almost all Pauli channels: Measure/quantifier domain for almost all, precise exceptional set and hashing-point family (source-ambiguity)
• Almost-bitflip heuristic: optimal repetition length and claimed hashing-point asymptotic rate: Precise limiting regime, repetition optimizer and asymptotic approximation relation (source-ambiguity)
• Figure 1: asymmetric independent-noise cat-code advantage and threshold: Consistent printed bias/basis and certified threshold interval (source-ambiguity)
• Concatenated Repetition Codes: numerical 3-in-19 depolarizing threshold: Certified threshold tolerance and specified optimization domain for the 3-in-19 observation (source-ambiguity)
• Concatenated Repetition Codes: numerical 5-in-16 depolarizing threshold: Certified tolerance for the 5-in-16 observation without claiming global optimality (source-ambiguity)
• Two-Pauli Channels are Special: no gain in the examined repetition-code searches: Enumerated tested codes and parameter sweep for the empirical no-gain report (source-ambiguity)

Selected references

• Degenerate Quantum Codes for Pauli Channels, arXiv:quant-ph/0604107v2, https://arxiv.org/abs/quant-ph/0604107v2

Motivation

Variational quantum circuits are used in quantum machine learning and variational quantum simulation tasks. Designing good variational circuits or predicting how well they perform for given learning or optimization tasks is still unclear. Here we discuss these problems, analyzing variational quantum circuits using the theory of neural tangent kernels. We define quantum neural tangent kernels, and derive dynamical equations for their associated loss function in optimization and learning tasks. We analytically solve the dynamics in the frozen limit, or lazy training regime, where variational angles change slowly and a linear perturbation is good enough. We extend the analysis to a dynamical setting, including quadratic corrections in the variational angles. We then consider hybrid quantum-classical architecture and define a large-width limit for hybrid kernels, showing that a hybrid quantum-classical neural network can be approximately Gaussian. The results presented here show limits for which analytical understandings of the training dynamics for variational quantum circuits, used for quantum machine learning and optimization problems, are possible. These analytical results are supported by numerical simulations of quantum machine learning experiments.

This mission is the statement-level formalization of Representation Learning via Quantum Neural Tangent Kernels (arXiv:2111.04225v3). 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 Non-Gaussianity from large quantum width (Main Theorem 5; SM Eqs.(202)-(203), PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Main Theorem 1; Eqs.(10)-(12), SM Eq.(70): A consistent rate sign/norm convention and a nondegenerate, stable scalar optimization regime (source-ambiguity)
• Main Theorem 2; Eqs.(18)-(22): Nondegeneracy/stability and a consistent model for the asserted infinite-time limit (source-ambiguity)
• Main Eqs.(41)-(44); SM Eqs.(119),(122)-(125): Consistently normalized algorithm-projector tensor and retained second-order increment (source-ambiguity)
• SM Eqs.(155)-(158): A nonvacuous output-space restriction or independently derived generalized-inverse prediction theorem (source-ambiguity)
• SM Eqs.(178)-(181): A nonvacuous amplitude inverse and a consistently normalized doubled algorithm-projector tensor (source-ambiguity)
• SM Eqs.(143)-(150),(159)-(169),(182)-(184): Consistent ordered first and equal-index second circuit coefficients (source-ambiguity)
• SM paragraph following Eq.(204): Uniform derivative/activation/depth/evolution hypotheses implying a quantitative meta-kernel bound (source-ambiguity)
• Abstract/Fig.2; main IV; SM V: A specified Gaussian-process convergence conclusion and sufficient higher-order or conditional-covariance hypotheses (source-ambiguity)

Selected references

• Representation Learning via Quantum Neural Tangent Kernels, arXiv:2111.04225v3, https://arxiv.org/abs/2111.04225v3

Motivation

We present a resource-performance tradeoff of an all-optical quantum repeater that uses photon sources, linear optics, photon detectors and classical feedforward at each repeater node, but no quantum memories. We show that the quantum-secure key rate has the form $R(η) = Dη^s$ bits per mode, where $η$ is the end-to-end channel's transmissivity, and the constants $D$ and $s$ are functions of various device inefficiencies and the resource constraint, such as the number of available photon sources at each repeater node. Even with lossy devices, we show that it is possible to attain $s < 1$, and in turn outperform the maximum key rate attainable without quantum repeaters, $R_{\rm direct}(η) = -\log_2(1-η) \approx (1/\ln 2)η$ bits per mode for $η\ll 1$, beyond a certain total range $L$, where $η\sim e^{-αL}$ in optical fiber. We also propose a suite of modifications to a recently-proposed all-optical repeater protocol that ours builds upon, which lower the number of photon sources required to create photonic clusters at the repeaters so as to outperform $R_{\rm direct}(η)$, from $\sim 10^{11}$ to $\sim 10^{6}$ photon sources per repeater node. We show that the optimum separation between repeater nodes is independent of the total range $L$, and is around $1.5$ km for assumptions we make on various device losses.

This mission is the statement-level formalization of Rate-distance tradeoff and resource costs for all-optical quantum repeaters (arXiv:1603.01353v4). 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 Balanced binary fusion: photon count and inverse size budget (III.A: size and fusion-depth relation for the balanced construction, 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

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

• Abstract; I.B; IV; VI: claimed power-law rate-distance envelope with repeater advantage: Abstract; I.B; IV; VI: claimed power-law rate-distance envelope with repeater advantage (source-ambiguity)
• III.A.2, Fig.5: resource savings and percolation-like transition: III.A.2, Fig.5: resource savings and percolation-like transition (source-ambiguity)
• III.B–IV, Eqs.(1),(7)–(9): exact finite-chain success and rate: Complete cluster-preparation/conditional-loss/pruning/endpoint experiment for the prescribed graph states (hard)
• IV, Eqs.(10)–(17): exact power-law identity at the sampled distances: Actual finite-chain rate experiment and its n-dependent preparation probability at integer sampled distances (hard)
• IV, Eq.(18): asserted range-independent optimal spacing: IV, Eq.(18): asserted range-independent optimal spacing (source-ambiguity)
• IV, Fig.6: numerical envelope, s<1, and crossover: IV, Fig.6: numerical envelope, s<1, and crossover (source-ambiguity)
• V: resource and parallel-channel advantage of the improved design: V: resource and parallel-channel advantage of the improved design (source-ambiguity)
• V, Table II and Fig.7: resource-constrained design optima: V, Table II and Fig.7: resource-constrained design optima (source-ambiguity)
• V: two numerical operating points at 5000 km: V: two numerical operating points at 5000 km (source-ambiguity)
• V: qualitative implication for scalable tree-protected LOQC: V: qualitative implication for scalable tree-protected LOQC (source-ambiguity)
• Appendix A, Fig.8(d): moving final X/Y measurements before fusion: Concrete Fig.8(d) GHZ/fusion-port quantum instrument with every feedforward correction (hard)

Selected references

• Rate-distance tradeoff and resource costs for all-optical quantum repeaters, arXiv:1603.01353v4, https://arxiv.org/abs/1603.01353v4

Motivation

Quantum key distribution is widely thought to offer unconditional security in communication between two users. Unfortunately, a widely accepted proof of its security in the presence of source, device and channel noises has been missing. This long-standing problem is solved here by showing that, given fault-tolerant quantum computers, quantum key distribution over an arbitrarily long distance of a realistic noisy channel can be made unconditionally secure. The proof is reduced from a noisy quantum scheme to a noiseless quantum scheme and then from a noiseless quantum scheme to a noiseless classical scheme, which can then be tackled by classical probability theory.

This mission is the statement-level formalization of Unconditional Security Of Quantum Key Distribution Over Arbitrarily Long Distances (arXiv:quant-ph/9803006v5). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is General common-basis quantum-to-classical reduction (General common-basis quantum-to-classical reduction, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract: unconditional long-distance noisy QKD: Abstract: unconditional long-distance noisy QKD (source-ambiguity)
• First reduction: noisy distributed protocol to noiseless logical protocol: First reduction: noisy distributed protocol to noiseless logical protocol (source-ambiguity)
• Passing-string count in announced parity constraints: Passing-string count in announced parity constraints (source-ambiguity)
• Main claim: Bell premeasurement leaves cheating probability unchanged: BDSW LOCC instrument with shrinking registers and transported virtual Bell tests (hard)
• Random-hashing verification bounds, equations (5)–(8): Execution-derived acceptance probability and virtual posterior for BDSW random hashing (hard)
• Proposition 1 in note [21]: quantum Trojan-horse defense: Trusted-origin quantum boundary semantics with malicious outside instrument (hard)
• Supplementary Note 4: explicit deterministic-key attack if masks are known: Phase- and pair-order-validated execution of Figure 1 and Note 4 (source-ambiguity)
• Supplementary Note 5 and [36]: full public outcomes preserve secrecy: Accepted full-transcript CQ instrument and retained transformed Bell target (hard)
• Discussion: Alice’s premeasurement gives an equally secure qubit-transmission version: Complete Alice-premeasured and EPR QKD executions with secret mask timing (hard)
• Supplementary Note 6: probabilistic information bound from sample errors: Supplementary Note 6: probabilistic information bound from sample errors (source-ambiguity)
• Note [40]: security of Wiesner money against double spending: Note [40]: security of Wiesner money against double spending (source-ambiguity)
• Background: no cloning: Background: no cloning (hard)
• Background: bit commitment and oblivious transfer impossibility: Background: bit commitment and oblivious transfer impossibility (hard)
• Background: Mayers’s distinct BB84 result: Background: Mayers’s distinct BB84 result (hard)
• Background: independent-noise FT threshold: Background: independent-noise FT threshold (hard)
• Background: purification and repeater distribution: Background: purification and repeater distribution (hard)
• Background: depolarizing-pair purification threshold 1/2: Background: depolarizing-pair purification threshold 1/2 (hard)
• Background: correctable syndrome reveals no logical information: Background: correctable syndrome reveals no logical information (hard)
• Background: BDSW local subset-parity realization: Background: BDSW local subset-parity realization (hard)
• Background: purification of mixed states: Background: purification of mixed states (hard)
• Background: quantum teleportation: Background: quantum teleportation (hard)
• Background: Holevo theorem used by Lemma 2: Background: Holevo theorem used by Lemma 2 (hard)
• Supplementary Note 3: cited concatenated-error suppression: Supplementary Note 3: cited concatenated-error suppression (source-ambiguity)
• Background: fidelity monotonicity under discard: Background: fidelity monotonicity under discard (hard)
• Background: finite-population CLT/confidence methods: Background: finite-population CLT/confidence methods (source-ambiguity)

Selected references

• Unconditional Security Of Quantum Key Distribution Over Arbitrarily Long Distances, arXiv:quant-ph/9803006v5, https://arxiv.org/abs/quant-ph/9803006v5

Motivation

An optical transmitter irradiates a target region containing a bright thermal-noise bath in which a low-reflectivity object might be embedded. The light received from this region is used to decide whether the object is present or absent. The performance achieved using a coherent-state transmitter is compared with that of a quantum illumination transmitter, i.e., one that employs the signal beam obtained from spontaneous parametric downconversion (SPDC). By making the optimum joint measurement on the light received from the target region together with the retained SPDC idler beam, the quantum illumination system realizes a 6 dB advantage in error probability exponent over the optimum reception coherent-state system. This advantage accrues despite there being no entanglement between the light collected from the target region and the retained idler beam.

This mission is the statement-level formalization of Quantum Illumination with Gaussian States (arXiv:0810.0534v1). 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 Eqs.(1)–(2): SPDC number state and Wigner covariance (Eqs.(1)–(2): SPDC number state and Wigner covariance, 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

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

• Abstract and p.4: 6 dB illumination advantage despite absent return–idler entanglement: Specify a limiting filter/order and error control for the QI overlap, and justify equality of the corresponding optimal-error exponent before comparing it to the coherent optimum. (source-ambiguity)
• Eq.(14): doubly approximated coherent lower bound: Specify relative-error, logarithmic, or iterated-limit meaning for (14), with growth control on M times the omitted high-NB exponent correction. (source-ambiguity)
• Eq.(18): low-brightness QI Bhattacharyya approximation: Specify a joint or iterated limit in k→0+, NS→0+, NB→infinity and a remainder/tolerance for -log Tr(sqrt(rho0)sqrt(rho1)); distinguish this overlap exponent from optimal-error exponent. (source-ambiguity)
• p.4: at least 3 dB QI advantage over all classical transmitters: Specify the asymptotic convention and remainders supporting the comparison of (14) and (18), keeping the exact finite-M classical lower bound distinct from an optimum-classical exponent characterization. (source-ambiguity)
• p.4: no close classical-input approximation to the QI returned state: Specify a state metric, approximation tolerance and quantifiers, and whether the energy budget constrains signal alone or signal plus idler. (source-ambiguity)

Selected references

• Quantum Illumination with Gaussian States, arXiv:0810.0534v1, https://arxiv.org/abs/0810.0534v1

Motivation

The quantum internet holds promise for performing quantum communication, such as quantum teleportation and quantum key distribution, freely between any parties all over the globe. For such a quantum internet protocol, a general fundamental upper bound on the performance has been derived [K. Azuma, A. Mizutani, and H.-K. Lo, arXiv:1601.02933]. Here we consider its converse problem. In particular, we present a protocol constructible from any given quantum network, which is based on running quantum repeater schemes in parallel over the network. The performance of this protocol and the upper bound restrict the quantum capacity and the private capacity over the network from both sides. The optimality of the protocol is related to fundamental problems such as additivity questions for quantum channels and questions on the existence of a gap between quantum and private capacities.

This mission is the statement-level formalization of Aggregating quantum repeaters for the quantum internet (arXiv:1606.00135v1). 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 Independent edge Bell products have additive trace-norm error (Eq.(4), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Eqs.(8)-(9): Unrestricted adaptive network protocols, two-way edge capacities, channel squashed entanglement, and iterated operational limits. (hard)
• Eq.(3): Actual adaptive history law and arbitrary-system channel squashed-entanglement optimization. (hard)
• Eqs.(5)-(6): Multipartite local-instrument semantics with register ownership and an explicitly computed path-swapping protocol. (hard)
• Eq.(7): Operational ENNReal supremum over all eps-close budget-feasible protocols, and legal aggregated construction. (hard)
• Eq.(12): Unconstrained bosonic pure-loss channel network operational capacity and ordered limits. (hard)
• Eq.(14): Actual optical network optimum in the Eq.(12) sandwich. (hard)
• Eq.(15): Two-superparty bidirectional crossing-bundle capacity under normalized relative-use budgets. (hard)
• Eq.(16): Operational private crossing-bundle capacity retaining arbitrary shield systems. (hard)
• Eq.(17) and following sentence: Operational crossing-bundle and network quantum rates related to the constructed repeater yield. (hard)
• Eqs.(18)-(19) and following sentence: Operational private bundle and network rates plus actual assisted entanglement edge rates. (hard)

Selected references

• Aggregating quantum repeaters for the quantum internet, arXiv:1606.00135v1, https://arxiv.org/abs/1606.00135v1

Motivation

Given an arbitrary single-qubit operation, an important task is to efficiently decompose this operation into an (exact or approximate) sequence of fault-tolerant quantum operations. We derive a depth-optimal canonical form for single-qubit quantum circuits, and the corresponding rules for exactly reducing an arbitrary single-qubit circuit to this canonical form. We focus on the single-qubit universal H,T basis due to its role in fault-tolerant quantum computing, and show how our formalism might be extended to other universal bases. We then extend our canonical representation to the family of Solovay-Kitaev decomposition algorithms, in order to find an ε-approximation to the single-qubit circuit in polylogarithmic time. For a given single-qubit operation, we find significantly lower-depth ε-approximation circuits than previous state-of-the-art implementations. In addition, the implementation of our algorithm requires significantly fewer resources, in terms of computation memory, than previous approaches.

This mission is the statement-level formalization of A Depth-Optimal Canonical Form for Single-qubit Quantum Circuits (arXiv:1206.3223v1). 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 1: uniqueness of the canonical core under two-sided Clifford equivalence (seed result) (Theorem 1: uniqueness of the canonical core under two-sided Clifford equivalence (seed result), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered §III: advertised canonical-circuit cardinality: Unnumbered §III: advertised canonical-circuit cardinality (source-ambiguity)
• Unnumbered §§II/V: relation of Clifford depth and HSH count to T-count: Unnumbered §§II/V: relation of Clifford depth and HSH count to T-count (source-ambiguity)
• Unnumbered introduction: claimed improved exact-search complexity: Unnumbered introduction: claimed improved exact-search complexity (source-ambiguity)
• Unnumbered §IV: equivalence of constrained minimum-cost Queries 1–4: Unnumbered §IV: equivalence of constrained minimum-cost Queries 1–4 (source-ambiguity)
• §IV empirical observations 1–3: trace counts and search costs: §IV empirical observations 1–3: trace counts and search costs (source-ambiguity)
• Abstract/§V: claimed polylogarithmic approximation with canonical reductions: Abstract/§V: claimed polylogarithmic approximation with canonical reductions (source-ambiguity)
• §VI and Figure 3: reported resource and approximation improvements: §VI and Figure 3: reported resource and approximation improvements (source-ambiguity)
• Conjecture 1: differing canonical T-counts have differing absolute traces: Conjecture 1: differing canonical T-counts have differing absolute traces (source-ambiguity)

Selected references

• A Depth-Optimal Canonical Form for Single-qubit Quantum Circuits, arXiv:1206.3223v1, https://arxiv.org/abs/1206.3223v1

Motivation

We prove the security of quantum key distribution against the most general attacks which can be performed on the channel, by an eavesdropper who has unlimited computation abilities, and the full power allowed by the rules of classical and quantum physics. A key created that way can then be used to transmit secure messages in a way that their security is also unaffected in the future.

This mission is the statement-level formalization of A Proof of the Security of Quantum Key Distribution (arXiv:quant-ph/9912053v1). 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 Symmetry after measuring the test (Appendix C: symmetry survives test measurement, 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

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

• Main result: security of used-bits BB84 against general attacks; Eq.(11): Complete execution-derived used-bits BB84 experiment with the Eq.(11) information event (hard)
• Section 2 / Appendix C: optimality of 0/1 symmetrization: Public-transcript/key simulation by measuring the retained coherent mask (hard)
• Lemma 4.1: fixed-basis weighted information bound (corrected tail): Execution-derived test-weighted information and conjugate-information joint law at fixed basis and partition (hard)
• Lemma 4.2: average over bases: One physical preannouncement unitary represented consistently in all x/z basis strings (hard)
• Lemma 4.3: average over balanced partitions: Full transcript law for independent uniform balanced partition after the fixed attack (hard)
• Section 4.1 unnumbered corollary: exponentially small weighted information: Unconditional protocol-weighted information as an actual function of the attack and public choices (hard)
• Section 4.1: reliability of fixed-code protocol: Executed syndrome decoder and both actual final key variables on the same sampled run (hard)
• Appendix B: ordinary BB84 reduces to used-bits BB84: Original BB84 sifting execution, first-2n selection and unused-register attack reduction (hard)
• Appendix B: claimed extension to high losses: An erasure/detection and loss-filtering experiment for the claimed high-loss extension (source-ambiguity)
• Appendix O: finite random-code reliability bound, Eqs.(47)–(49): Pinned finite random-code ensemble and a consistent Eq.(48) exponent (source-ambiguity)
• Appendix O: finite random-code security bound, Eqs.(50)–(51): Actual random ECC/PA parity-span law and its advertised g2 failure probability (source-ambiguity)
• Appendix O: asymptotic secret-key rate and 7.56 percent threshold: Random ECC/PA selection and probabilistic decoder families tied to the actual abort-inclusive protocol (hard)
• Abstract: future security of messages sent with the key: Encryption/disclosure experiment and future message-security notion (source-ambiguity)
• Section 1.3: swap attack defeats secrecy conditioned only on passing: Concrete swap/substitution attack evaluated in the full disclosed-code and passing-test experiment (hard)

Selected references

• A Proof of the Security of Quantum Key Distribution, arXiv:quant-ph/9912053v1, https://arxiv.org/abs/quant-ph/9912053v1

Motivation

In this paper we use the AdS/CFT correspondence to refine and then establish a set of old conjectures about symmetries in quantum gravity. We first show that any global symmetry, discrete or continuous, in a bulk quantum gravity theory with a CFT dual would lead to an inconsistency in that CFT, and thus that there are no bulk global symmetries in AdS/CFT. We then argue that any "long-range" bulk gauge symmetry leads to a global symmetry in the boundary CFT, whose consistency requires the existence of bulk dynamical objects which transform in all finite-dimensional irreducible representations of the bulk gauge group. We mostly assume that all internal symmetry groups are compact, but we also give a general condition on CFTs, which we expect to be true quite broadly, which implies this. We extend all of these results to the case of higher-form symmetries. Finally we extend a recently proposed new motivation for the weak gravity conjecture to more general gauge groups, reproducing the "convex hull condition" of Cheung and Remmen. An essential point, which we dwell on at length, is precisely defining what we mean by gauge and global symmetries in the bulk and boundary. Quantum field theory results we meet while assembling the necessary tools include continuous global symmetries without Noether currents, new perspectives on spontaneous symmetry-breaking and 't Hooft anomalies, a new order parameter for confinement which works in the presence of fundamental quarks, a Hamiltonian lattice formulation of gauge theories with arbitrary discrete gauge groups, an extension of the Coleman-Mandula theorem to discrete symmetries, and an improved explanation of the decay $π^0\toγγ$ in the standard model of particle physics. We also describe new black hole solutions of the Einstein equation in $d+1$ dimensions with horizon topology $\mathbb{T}^p\times \mathbb{S}^{d-p-1}$.

This mission is the statement-level formalization of Symmetries in quantum field theory and quantum gravity (arXiv:1810.05338v2). 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 Local conjugation forces a tensor product of unitaries (Theorem 2.1: local unitary factorization, PDF p. 23). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• §2.1: conformal transport of splittability: Flat/sphere conformal net and bounded collar-localized implementer transport (hard)
• §2.2: continuous symmetry without a Noether current: Noncompact Maxwell observable net, bounded electric-flux spectral functions, and all candidate local currents (hard)
• §2.2: compact-gauge discrete unsplittable symmetries: Compact Maxwell Wilson/flux algebra for both discrete examples (hard)
• §2.4: CFT symmetries preserved on the cylinder: Weyl transport and Lorentzian reconstruction of the full local-operator symmetry (hard)
• §2.5: residual chiral symmetry and interacting unsplittability: Nonperturbative chiral QED algebra and nontrivial flavor range (source-ambiguity)
• §2.5: interacting noncompact-gauge Noether counterexample: Interacting noncompact QED and compact/noncompact local-sector equivalence (source-ambiguity)
• §2.5: neutral-pion Goldstone interpretation: Massless QCD vacuum and controlled low-energy effective-theory regime (source-ambiguity)
• §2.6: anomalous transformations need not be scalar rescalings: Regulated background partition function and counterterm class (source-ambiguity)
• §3.2 / Appendix F: finite-gauge Wilson Hamiltonian: Oriented finite-gauge lattice, Gauss projection, and normalized Wilson transfer generator (hard)
• §3.3: charge criterion distinguishes two gauge-matter phases: Exact thermodynamic phases and parameter neighborhoods (source-ambiguity)
• §3.5: gauge/global mixing: Long-range charged-sector realization of the gauged scalar model (source-ambiguity)
• Theorem 4.1: bulk global symmetry induces the same boundary global symmetry: Quantified quasilocal bulk-operator and boundary-limit class (source-ambiguity)
• Theorem 4.2 / abstract headline: no bulk global symmetry in AdS/CFT: Exact holographic operator/code interfaces for both no-go proofs (source-ambiguity)
• §4.4: boundary global / bulk gauge duality: Exact bulk-gauge/boundary-global reconstruction interface (source-ambiguity)
• §5: completeness of compact gauge representations: Wilson operator extension from dressing/code domains to the full CFT tensor product (source-ambiguity)
• Theorem 6.1: compact completion of finitely generated CFT symmetry: Full finitely generated CFT operator algebra and compact-closure symmetry extension (hard)
• §6: continuous-spectrum finite-generator extension: Continuous-spectrum CFT finite-OPE generation with finite-dimensional generator orbits (hard)
• Theorem 7.1: discrete Coleman–Mandula theorem: Precise Coleman-Mandula applicability and dimension range (source-ambiguity)
• §7: no ungauged spacetime reflections: Antiunitary localized splitting and disconnected-region reconstruction (source-ambiguity)
• §7: states of all allowed spin: Rotation representation branching class and gravitational Wilson domains (source-ambiguity)
• §8.3: no higher-form bulk global symmetries: Quantified filling, torus-size regime and higher-form reconstruction (source-ambiguity)
• §8.3: higher-form gauge-charge completeness: Exact surface-state correspondence and r-to-zero operator domains (source-ambiguity)
• §8.3: finite surface generation and compact completion: Surface OPE, grading and surface-state domain (source-ambiguity)
• Appendix C: unbounded-operator extension: Common conjugation-invariant domain and separating vacuum seminorm (source-ambiguity)
• Appendix D: closed-hypersurface symmetry insertions: Defect path-integral gluing and deformation axioms (source-ambiguity)
• Appendix G (G.5): closed-lattice degeneracy: Actual finite cellular chain incidence, Pauli Hamiltonian, and mod-two homology (hard)
• Appendix G (G.11): boundary-lattice degeneracy: Relative cellular gauge register and boundary inclusion homology map (hard)
• Appendix G: unique ball ground state: Cellular pair homeomorphism to a ball and relative gauge ground space (hard)
• §8.3 / Appendix I: sphere-contracting vacuum: Global Einstein vacuum family with exact parameter range and boundary conditions (source-ambiguity)
• §8.3 / Appendix I: torus-sphere wormhole family: Global Einstein wormhole family including p=1 (source-ambiguity)

Selected references

• Symmetries in quantum field theory and quantum gravity, arXiv:1810.05338v2, https://arxiv.org/abs/1810.05338v2

Motivation

Shor and Preskill have provided a simple proof of security of the standard quantum key distribution scheme by Bennett and Brassard (BB84) by demonstrating a connection between key distribution and entanglement purification protocols with one-way communications. Here we provide proofs of security of standard quantum key distribution schemes, BB84 and the six-state scheme, against the most general attack, by using the techniques of two-way entanglement purification. We demonstrate clearly the advantage of classical post-processing with two-way classical communications over classical post-processing with only one-way classical communications in QKD. This is done by the explicit construction of a new protocol for (the error correction/detection and privacy amplification of) BB84 that can tolerate a bit error rate of up to 18.9%, which is higher than what any BB84 scheme with only one-way classical communications can possibly tolerate. Moreover, we demonstrate the advantage of the six-state scheme over BB84 by showing that the six-state scheme can strictly tolerate a higher bit error rate than BB84. In particular, our six-state protocol can tolerate a bit error rate of 26.4%, which is higher than the upper bound of 25% bit error rate for any secure BB84 protocol. Consequently, our protocols may allow higher key generation rate and remain secure over longer distances than previous protocols. Our investigation suggests that two-way entanglement purification is a useful tool in the study of advantage distillation, error correction, and privacy amplification protocols.

This mission is the statement-level formalization of Proof of security of quantum key distribution with two-way classical communications (arXiv:quant-ph/0105121v2). 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 B and P steps: conditional Pauli error transformations (Appendix C, equations (15)–(22), PDF p. 22). 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

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

• Theorem 6 (Main Theorem): two-way CSS-like EPP conversion: Evaluated symmetric CSS-like EPP tree, phase-independent tree transformation, and Definition 8/9 protocol security (hard)
• Lemma 1: EPR fidelity gives agreement, randomness and small Eve information: Full joint-key agreement/randomness and n-dependent mutual-information asymptotic family (source-ambiguity)
• Lemma 2 [23]: joint-to-Pauli attack reduction: Same-protocol joint-to-Pauli attack construction preserving abort probability and EPR overlap (hard)
• Lemma 3: robust IID correction controls symmetric correlated Pauli attacks: Sampling-conditioned robust purification family for permutation-symmetric correlated Pauli noise (hard)
• Theorem 4: EPP QKD protocols are secure and correct: Definition 8 security/correctness of the robust §2.3 EPP protocol family (hard)
• Theorem 5 [33]: CSS-like one-way EPP conversion: Constructed one-way CSS EPP conversion and per-attack Definition 9 security relation (hard)
• Claim 7: high fidelity implies low entropy: Corrected dimension symbol and precise small-delta domain for the entropy bound (source-ambiguity)
• Claim 8: entropy bounds information of local measurements: Joint classical distribution of arbitrary local generalized measurements on a computed pure bipartite state (hard)
• Theorem 9: a=0 is the worst BB84 channel: Operational high-fidelity asymmetric CSS completion of the same finite B/P schedule (hard)
• §7: explicit EPP 2 / classical Protocol 2 construction: Explicit EPP 2 tree and seven-step Protocol 2 with computed key coset and transcript (hard)
• §7: five B then six P steps secure BB84 at 18.9%: Five-B/six-P BB84 protocol with robust CSS completion and general-attack security (hard)
• §7: five B steps secure six-state at 26.4%: Five-B six-state protocol with actual CSS completion and general-attack security at QBER 33/125 (hard)
• §7: alternating B/P BB84 security at 17.9%: Uniform finite alternating-round BB84 schedule with operational security at QBER 179/1000 (hard)
• §7: alternating B/P six-state security at 23.6%: Uniform finite alternating-round six-state protocol at measured QBER 59/250 (hard)
• §2.2: two-way intercept-resend upper bounds: Arbitrary public-discussion key extraction and no-positive-fresh-key theorem for the explicit intercept-resend source (hard)
• §2.2: cited cloning upper bounds for one-way processing: Explicit symmetric approximate cloners and one-way public-discussion key impossibility (hard)
• §2.2: cited one-way BB84 rate 1-2h(p): Operational one-way BB84 security and rate 1-2h(p) per sifted bit (hard)
• §2.2: cited one-way six-state tolerance around 12.7%: Operational degenerate-code correlated-syndrome six-state security theorem (hard)
• §3: cited correspondence of one-way EPPs and QECCs: Encoding/decoding execution correspondence between 1-EPP and QECC (hard)
• §7: background asymmetric CSS coding assertion: Asymptotic stochastic asymmetric CSS code and decoder family with fidelity/resources (hard)
• §2.1 footnote 4: cited efficient biased-basis QKD: Biased-basis QKD execution with refined per-basis tests and adequate sample parameters (hard)
• §2.1 footnote 3: two-way discussion can raise secrecy capacity: Classical one-/two-way secrecy-capacity source model and a witnessing strict-advantage channel (hard)
• Appendix D.1: Inamori BB84 net-rate derivation: Stored original-data postselection, encrypted-syndrome seed accounting and asymptotic rate (source-ambiguity)
• Appendix D.2: Inamori six-state rate and roughly 12.6% tolerance: Three-basis original-agreement postselection and net fresh-key rate with the factor two (source-ambiguity)

Selected references

• Proof of security of quantum key distribution with two-way classical communications, arXiv:quant-ph/0105121v2, https://arxiv.org/abs/quant-ph/0105121v2

Motivation

The quantum Fourier transform (QFT) is the principal algorithmic tool underlying most efficient quantum algorithms. We present a generic framework for the construction of efficient quantum circuits for the QFT by ``quantizing'' the separation of variables technique that has been so successful in the study of classical Fourier transform computations. Specifically, this framework applies the existence of computable Bratteli diagrams, adapted factorizations, and Gel'fand-Tsetlin bases to offer efficient quantum circuits for the QFT over a wide variety a finite Abelian and non-Abelian groups, including all group families for which efficient QFTs are currently known and many new group families. Moreover, the method gives rise to the first subexponential-size quantum circuits for the QFT over the linear groups GL_k(q), SL_k(q), and the finite groups of Lie type, for any fixed prime power q.

This mission is the statement-level formalization of Generic Quantum Fourier Transforms (arXiv:quant-ph/0304064v1). 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 Symmetric groups: a polynomial-size ideal QFT in Young orthogonal coordinates (Unnumbered application: symmetric groups, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1: generic QFT complexity (original seed): Controlled generator-block coefficients, centralizer choices, and coherent synthesis/selection beyond the three routines of Definition 2. (source-ambiguity)
• Lemma 2: one subgroup-extension stage: Controlled generator-block coefficients, centralizer choices, and coherent synthesis/selection beyond the three routines of Definition 2. (source-ambiguity)
• Unnumbered corollary: polynomially bounded tower parameters: Controlled generator-block coefficients, centralizer choices, and coherent synthesis/selection beyond the three routines of Definition 2. (source-ambiguity)
• Unnumbered application: permutation wreath products: The permutation-action wreath product H^n semidirect S_n, its complete based induced dual, alternating-tower path coordinates, and fixed product-coset encodings. (hard)
• Unnumbered application: GL, SL, PGL and PSL at fixed q: Concrete parabolic-tower Fourier coordinates and product-coset encodings for GL_n, SL_n and their actual center quotients PGL_n, PSL_n. (hard)
• Unnumbered application: other Lie-type, finite unitary, Chevalley and Weyl families: An enumerated Lie-type/unitary/Chevalley/Weyl family domain and its matching parameter/tower bounds. (source-ambiguity)
• Theorem 2: homothetic Abelian extension stage: Definition-3 homothetic extension with literal same-row conjugate representatives, cost-bearing classical orbit/path programs, and its constructed induced G Fourier coordinates. (hard)
• Unnumbered corollary: closure under homothetic Abelian extensions: The constructed homothetic-stage interface composed with a supplied family of base H QFT circuits, with common quantitative bounds. (hard)
• Unnumbered application: split metacyclic, dihedral and affine groups: Efficient classical orbit-length and row/path relabeling for arbitrary encoded cyclic semidirect actions. (source-ambiguity)
• Unnumbered introductory claim: bounded extensions of Abelian groups: Uniform action, subgroup and based-representation encodings for all bounded-index Abelian extensions. (source-ambiguity)
• Unnumbered conditional extension claim: efficient powers of C(gamma): A fixed extension model and costed coherent interface for powers of the actual intertwiner C(gamma), including base-QFT assumptions. (source-ambiguity)
• Unnumbered application: the source's split Abelian-by-Abelian class: The exact split Abelian-by-Abelian class, based-dual construction, and action/orbit/intertwiner algorithms. (source-ambiguity)

Selected references

• Generic Quantum Fourier Transforms, arXiv:quant-ph/0304064v1, https://arxiv.org/abs/quant-ph/0304064v1

Motivation

A pure-loss bosonic channel is a simple model for communication over free-space or fiber-optic links. More generally, phase-insensitive bosonic channels model other kinds of noise, such as thermalizing or amplifying processes. Recent work has established the classical capacity of all of these channels, and furthermore, it is now known that a strong converse theorem holds for the classical capacity of these channels under a particular photon number constraint. The goal of the present paper is to initiate the study of second-order coding rates for these channels, by beginning with the simplest one, the pure-loss bosonic channel. In a second-order analysis of communication, one fixes the tolerable error probability and seeks to understand the back-off from capacity for a sufficiently large yet finite number of channel uses. We find a lower bound on the maximum achievable code size for the pure-loss bosonic channel, in terms of the known expression for its capacity and a quantity called channel dispersion. We accomplish this by proving a general "one-shot" coding theorem for channels with classical inputs and pure-state quantum outputs which reside in a separable Hilbert space. The theorem leads to an optimal second-order characterization when the channel output is finite-dimensional, and it remains an open question to determine whether the characterization is optimal for the pure-loss bosonic channel.

This mission is the statement-level formalization of Second-order coding rates for pure-loss bosonic channels (arXiv:1408.5328v3). 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 One-shot achievability for separable-output pure-state cq channels (Theorem 3, (4.1)–(4.2), 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

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

• (2.2), (6.9), §6.1: Operational mean photon-number constraint and unchanged-parameter code selection (source-ambiguity)
• §5 last paragraph and Remark 4: Capacity-achieving ensemble and error-dependent dispersion selection in the claimed converse (source-ambiguity)
• §6.2, Figure 3 discussion: Finite-block converse certifying the at-least-200-symbol necessity claim (source-ambiguity)

Selected references

• Second-order coding rates for pure-loss bosonic channels, arXiv:1408.5328v3, https://arxiv.org/abs/1408.5328v3

Motivation

Fawzi and Renner [Commun. Math. Phys. 340(2):575, 2015] recently established a lower bound on the conditional quantum mutual information (CQMI) of tripartite quantum states $ABC$ in terms of the fidelity of recovery (FoR), i.e. the maximal fidelity of the state $ABC$ with a state reconstructed from its marginal $BC$ by acting only on the $C$ system. The FoR measures quantum correlations by the local recoverability of global states and has many properties similar to the CQMI. Here we generalize the FoR and show that the resulting measure is multiplicative by utilizing semi-definite programming duality. This allows us to simplify an operational proof by Brandao et al. [Phys. Rev. Lett. 115(5):050501, 2015] of the above-mentioned lower bound that is based on quantum state redistribution. In particular, in contrast to the previous approaches, our proof does not rely on de Finetti reductions.

This mission is the statement-level formalization of The Fidelity of Recovery is Multiplicative (arXiv:1502.07973v2). 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 Generalized fidelity of recovery is multiplicative (Proposition 2, (26), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Selected references

• The Fidelity of Recovery is Multiplicative, arXiv:1502.07973v2, https://arxiv.org/abs/1502.07973v2

Motivation

Transmitting data reliably over noisy communication channels is one of the most important applications of information theory, and well understood when the channel is accurately modelled by classical physics. However, when quantum effects are involved, we do not know how to compute channel capacities. The capacity to transmit quantum information is essential to quantum cryptography and computing, but the formula involves maximising the coherent information over arbitrarily many channel uses. This is because entanglement across channel uses can increase the coherent information, even from zero to non-zero! However, in all known examples, at least to detect whether the capacity is non-zero, two channel uses already suffice. Maybe a finite number of channel uses is always sufficient? Here, we show this is emphatically not the case: for any n, there are channels for which the coherent information is zero for n uses, but which nonetheless have capacity. This may be a first indication that the quantum capacity is uncomputable.

This mission is the statement-level formalization of Unbounded number of channel uses are required to see quantum capacity (arXiv:1408.5115v1). 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 Arbitrarily many uses can fail to detect positive quantum capacity (Abstract/introduction; proved by Supplementary Theorem, p.11, 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.

Selected references

• Unbounded number of channel uses are required to see quantum capacity, arXiv:1408.5115v1, https://arxiv.org/abs/1408.5115v1

Motivation

We show how adaptive protocols of quantum and private communication through bosonic Gaussian channels can be simplified into much easier block versions that involve resource states with finite energy. This is achieved by combining the adaptive-to-block reduction technique devised earlier [S. Pirandola et al., Nat. Commun. 8, 15043 (2017)], based on teleportation stretching and relative entropy of entanglement, with an alternative simulation of Gaussian channels recently introduced by Liuzzo-Scorpo et al. [Phys. Rev. Lett. 119, 120503 (2017)]. In this way, we derive weak converse upper bounds for the secret-key capacity of phase-insensitive Gaussian channels, which approximate the optimal limit for infinite energy. Our results apply to both point-to-point and repeater-assisted private communications.

This mission is the statement-level formalization of Finite-resource teleportation stretching for continuous-variable systems (arXiv:1706.06065v3). 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 Constructed separable Gaussian comparison for finite-resource REE (IV, Eqs. (28)–(29); resource Eqs. (8)–(11), p.2, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 2, Eq. (23): finite-resource secret-key weak converse: Extended nonnegative secret-key capacity as a supremum of achievable asymptotic bit rates of these physical protocols, with actual private-state targets, vanishing FULL trace-norm error and division only by positive transmission counts. Also requires Genuine normal instruments on arbitrary separable local Hilbert spaces, including continuous homodyne outcomes and measurable history-dependent local operations; their trace-preserving averaged LOCC maps, referenced tensor extensions, and recursive outputs from product local initialization with public two-way communication, no initial secret/entangled resource, no input-energy constraint and counted channel calls. (hard)
• III C, Eqs. (20)-(21): exact adaptive-to-block output and REE reduction: Genuine normal instruments on arbitrary separable local Hilbert spaces, including continuous homodyne outcomes and measurable history-dependent local operations; their trace-preserving averaged LOCC maps, referenced tensor extensions, and recursive outputs from product local initialization with public two-way communication, no initial secret/entangled resource, no input-energy constraint and counted channel calls. (hard)
• III C, Eq. (22): regularized finite-resource bound: Extended nonnegative secret-key capacity as a supremum of achievable asymptotic bit rates of these physical protocols, with actual private-state targets, vanishing FULL trace-norm error and division only by positive transmission counts. Positive-copy tensor powers and regularized REE connected to the actual assisted task. (hard)
• III C, Eq. (25): every finite Choi approximant is an LOCC image of the resource: Full trace-preserving bosonic LOCC with untouched references, local TMSV preparation and exact ideal Bell instrument. (hard)
• III C, Eqs. (24)-(25): claimed no-improvement over the asymptotic bound: Admissible converging separable sequences and the asymptotic relative-entropy functional in Eq. (24). (source-ambiguity)
• IV A, Eqs. (30)-(32): thermal-loss finite-resource bound: Extended nonnegative secret-key capacity as a supremum of achievable asymptotic bit rates of these physical protocols, with actual private-state targets, vanishing FULL trace-norm error and division only by positive transmission counts. A referenced thermal-loss channel attached to that same task. (hard)
• IV B: noisy-amplifier finite-resource bound and Eq. (33) comparison: Extended nonnegative secret-key capacity as a supremum of achievable asymptotic bit rates of these physical protocols, with actual private-state targets, vanishing FULL trace-norm error and division only by positive transmission counts. A referenced physical noisy-amplifier channel with T=sqrt(eta)I, N=(eta-1)(nbar+1/2)I. (hard)
• IV C: additive-noise finite-resource bound and Eq. (34) comparison: Extended nonnegative secret-key capacity as a supremum of achievable asymptotic bit rates of these physical protocols, with actual private-state targets, vanishing FULL trace-norm error and division only by positive transmission counts. Referenced physical additive-noise map with eta=1 and N=xi I. (hard)
• IV D, Eq. (36): replacement finite-resource simulation and bound: Actual referenced ideal-Bell LOCC simulation with a constructed finite-energy TMSV resource (36), and Extended nonnegative secret-key capacity as a supremum of achievable asymptotic bit rates of these physical protocols, with actual private-state targets, vanishing FULL trace-norm error and division only by positive transmission counts. (hard)
• V, Eq. (38): exact finite-resource chain cut stretching: Dimension-general network LOCC histories, recursive counted chain outputs, and grouped-cut resource-consuming simulation on genuine normal states. (hard)
• V, Eq. (39): finite-resource repeater-assisted key-capacity bound: Operational end-to-end two-way secret-key capacity per full chain use, based on the same unrestricted physical network protocol and cut semantics. (hard)
• V: unqualified optimality of equidistant additive-noise repeaters: Precisely specified optimization objective and admissible repeater placement/noise-allocation model. (source-ambiguity)
• VI: unrestricted all-phase-insensitive-channel finite-resource claim: Complete noncircular finite-resource assignment for the unqualified all-channels statement. (source-ambiguity)

Selected references

• Finite-resource teleportation stretching for continuous-variable systems, arXiv:1706.06065v3, https://arxiv.org/abs/1706.06065v3