All missions

Motivation

In this paper all of the classical constructions of A. Young are generalized to affine Hecke algebras of type A. It is proved that the calibrated irreducible representations of the affine Hecke algebra are indexed by placed skew shapes and that these representations can be constructed explicitly with a generalization of Young's seminormal construction of the irreducible representations of the symmetric group. The seminormal construction of an irreducible calibrated module does not produce a basis on which the affine Hecke algebra acts integrally but using it one is able to pick out a different basis, an analogue of Young's natural basis, which does generate an integral lattice in the module. Analogues of the "Garnir relations" play an important role in the proof. The Littlewood-Richardson coefficients arise naturally as the decomposition multiplicities for the restriction of an irreducible representation of the affine Hecke algebra to the Iwahori-Hecke algebra.

This mission is the statement-level formalization of Skew shape representations are irreducible (arXiv:math/0401326v2). 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 Local intertwiners on generalized weight spaces (Proposition 3.2, 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

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

• Lemma 2.2: Multiplicative placed-skew geometry and its content-preserving isomorphism quotient (hard)
• Intertwiners 3.3 3.5: Rational Bernstein localization, PBW coefficients, and evaluation on generalized weight spaces (hard)
• Theorem 4.1 (a)–(c); Introduction main results (1),(4); original title seed: Explicit placed-shape seminormal modules and their isomorphism classes (hard)
• Proposition 5.3: The actual column-reading tableau and unnormalized vectors n_L=T_w v_C (hard)
• Nonstandard 5.4: An extension of the local tau_w to singular nonstandard fillings (source-ambiguity)
• Theorem 5.5: Geometric snakes, actual parabolic shuffles and both Garnir zero relations on the computed natural basis (hard)
• Proposition 5.6: Coordinates of the actual natural basis and its evaluated Z[q,q^-1] lattice (hard)
• Theorem 6.1: Restriction of the actual q-Hecke module and the actual straight-shape modules in an LR direct sum (hard)
• Theorem 6.2: Source-specified compatibility of placed factors under vertical/horizontal gluing (source-ambiguity)
• Corollary 6.3: Actual principal-series induction, finite composition-factor classes and normalized connected ribbon modules (hard)

Selected references

• Skew shape representations are irreducible, arXiv:math/0401326v2, https://arxiv.org/abs/math/0401326v2

Motivation

A representation of the exceptional Lie algebras is presented. It reflects a simple unifying view and it is realized in terms of Zorn-type matrices. The role of the underlying Jordan pair and Jordan algebra content is crucial in the development of the structure. Each algebra contains three Jordan pairs sharing the same Lie algebra of automorphisms and the same external su(3) symmetry. Applications in physics are outlined.

This mission is the statement-level formalization of Exceptional Lie Algebras, SU(3) and Jordan Pairs Part 2: Zorn-type Representations (arXiv:1403.5120v2). 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 G2 realized by the closed special Zorn commutator (§4, (4.4)–(4.7): G2 Lie realization, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Abstract and §1: unified exceptional Zorn realizations: Joint exceptional/Jordan-pair compatibility; compatible normalized G2 generator and Tits-to-Zorn comparison maps (hard)
• §5.1: normalization equivalence with Tits: Two fully specified normalized Tits tensor constructions (hard)
• (5.15): F4 branching: The labelled equivariant (3,bar6)+(bar3,6) module interface (hard)
• §6 Table 2: root and weight correspondence: A pinned E6 Cartan/root-coordinate dictionary and all nine Table-2 weight vectors (hard)
• (6.9): E6 branching: Root-aligned three-factor module restriction with the exact Table-2 dictionary (hard)
• (7.2): specified E6 inside E7: The specified quaternion-unit embedding of the E6 coordinate bracket inside E7 (hard)
• (7.3)–(7.5): E6 action on the two 27 spaces: The two nilpotent 27 coordinate modules and the four block extraction maps (hard)
• (7.6): E7 branching: A standard central sl6 identification and labelled exterior-square/dual module equivalences (hard)
• §9: closure of the new operator Zorn bracket: Concrete complex Albert algebra, reduced structure operators, and their intrinsic trace adjoint (hard)
• §9: E8 operator-valued realization: The concrete Albert operator Zorn space and its comparison with independent complex E8 (hard)
• (9.5): E8 branching: External sl3 plus operator-E6 restriction with the Albert 27 and its true contragredient (hard)
• §10: Jacobi for E8 raw operator bracket: The raw nonassociative Albert operator bracket of (9.2)-(9.4) (hard)

Selected references

• Exceptional Lie Algebras, SU(3) and Jordan Pairs Part 2: Zorn-type Representations, arXiv:1403.5120v2, https://arxiv.org/abs/1403.5120v2

Motivation

We derive the class of covariant measurements which are optimal according to the maximum likelihood criterion. The optimization problem is fully resolved in the case of pure input states, under the physically meaningful hypotheses of unimodularity of the covariance group and measurability of the stability subgroup. The general result is applied to the case of covariant state estimation for finite dimension, and to the Weyl-Heisenberg displacement estimation in infinite dimension. We also consider estimation with multiple copies, and compare collective measurements on identical copies with the scheme of independent measurements on each copy. A "continuous-variables" analogue of the measurement of direction of the angular momentum with two anti-parallel spins by Gisin and Popescu is given.

This mission is the statement-level formalization of Covariant quantum measurements which maximize the likelihood (arXiv:quant-ph/0403083v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §III, Eq.(12): finite-component weak twirling formula (§III, Eq.(12): finite-component weak twirling formula, 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

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

• Abstract / §§IV,VII: unrestricted pure-state canonical maximum-likelihood measurement: Source-selected domain and pointwise density convention for unrestricted generalized pure-state canonical seeds, including infinite attained likelihood (source-ambiguity)
• §III, Eqs.(3),(12): unrestricted operator class and infinite sums: Unrestricted operator/form class, well-defined component traces, and convergence topology for the weak Haar twirl and infinite double sum (source-ambiguity)
• §V, Eq.(19): asserted independent-average likelihood bound: Outcome coordinate space, real scaling dimension, reference measure, and valid dimension-dependent arithmetic-mean bound (source-ambiguity)
• §V.A.2: asserted universal breach for N>2: Correct admissible dimension/copy range for the printed universal strict inequality dim(Sym^N C^d)>Nd (source-ambiguity)
• §V.B.3: continuous Wedderburn identity: Domain and diagonal pairing with generalized continuous-spectral projectors, and weak/direct-integral convergence (source-ambiguity)
• §V.B.3: canonical optimum for arbitrary two-mode input: Invariant generalized-seed domain and selected pointwise likelihood for arbitrary L2 spectral inputs, including divergent likelihood (source-ambiguity)

Selected references

• Covariant quantum measurements which maximize the likelihood, arXiv:quant-ph/0403083v1, https://arxiv.org/abs/quant-ph/0403083v1

Motivation

We start with Fannes' type and Winter's type tight continuity bounds for the quantum conditional mutual information and their specifications for states of special types. Then we analyse continuity of the Holevo quantity with respect to nonequivalent metrics on the set of discrete ensembles of quantum states. We show that the Holevo quantity is continuous on the set of all ensembles of m states with respect to all the metrics if either m or the dimension of underlying Hilbert space is finite and obtain Fannes' type tight continuity bounds for the Holevo quantity in this case. In general case conditions for local continuity of the Holevo quantity for discrete and continuous ensembles are found. Winter's type tight continuity bound for the Holevo quantity under constraint on the average energy of ensembles is obtained and applied to the system of quantum oscillators. The above results are used to obtain tight and close-to-tight continuity bounds for basic capacities of finite-dimensional channels (refining the Leung-Smith continuity bounds).

This mission is the statement-level formalization of Tight continuity bounds for the quantum conditional mutual information, for the Holevo quantity and for capacities of quantum channels (arXiv:1512.09047v7). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

28 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2, (35): optimized energy-constrained QCMI continuity; original seed (Proposition 2, (35): optimized energy-constrained QCMI continuity; original seed, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Proposition 1, (20)–(21): Jordan-part QCMI comparison: Normalized Jordan parts on arbitrary nuclear coefficient operators, plus their actual finite-dimensional marginal support predicates. (hard)
• Corollary 1, (25): finite-minimum-dimension QCMI bound and tightness: Compatibility of the accepted exact isotropicDensity witness with normalized nuclear states and the extended QMI model, including the large-d tightness comparison. (hard)
• Corollary 2, (28): qqc continuity and Shannon refinement: Complete countable qqc continuity theorem: computed gamma laws, dimension/Shannon alternatives, finite-difference domains, and both equal-marginal refinements. (hard)
• Remark 3: claimed attainment of optimal t: Attained minimum for all admissible entropy majorants (source-ambiguity)
• Corollary 3, (44): tight oscillator QCMI bound: Actual oscillator Gibbs purification/mixed-product witness and its energy/information evaluations. (hard)
• Proposition 3, (45)–(47): n-copy output QCMI continuity: Local-marginal stabilized channel divergence for arbitrary entangled blocks, plus actual finite and oscillator sharpness witnesses. (hard)
• Remark 6, second clause: claimed standard linear programming: Standard linear-program encoding of general noncommuting EHS distance (source-ambiguity)
• Proposition 5, (60)–(61): tight global Holevo bounds: All four global Holevo tightness witnesses and normalized gamma-law Shannon refinement in the same ensemble model. (hard)
• Proposition 7, (68)–(70): tight energy-bounded discrete Holevo continuity: Actual Gibbs pure-state ensemble sharpness construction (70) and its coefficient-state entropy/energy bridge. (hard)
• Proposition 10, (80)–(81): tight Holevo/assisted capacity bounds: CPTP adapters and actual depolarizing channel capacity evaluations in nats, with the unstabilized induced trace norm on all operators. (hard)
• Proposition 11, (86)–(87): classical/quantum capacity bounds: Signed extended coherent information, operational/regularized capacity identification and actual erasure/depolarizing sharpness. (hard)

Selected references

• Tight continuity bounds for the quantum conditional mutual information, for the Holevo quantity and for capacities of quantum channels, arXiv:1512.09047v7, https://arxiv.org/abs/1512.09047v7

Motivation

In order to study multipartite quantum cryptography, we introduce quantities which vanish on product probability distributions, and which can only decrease if the parties carry out local operations or carry out public classical communication. These ``secrecy monotones'' therefore measure how much secret correlations are shared by the parties. In the bipartite case we show that the mutual information is a secrecy monotone. In the multipartite case we describe two different generalisations of the mutual information, both of which are secrecy monotones. The existence of two distinct secrecy monotones allows us to show that in multipartite quantum cryptography the parties must make irreversible choices about which multipartite correlations they want to obtain. Secrecy monotones can be extended to the quantum domain and are then defined on density matrices. We illustrate this generalisation by considering tri-partite quantum cryptography based on the Greenberger-Horne-Zeilinger (GHZ) state. We show that before carrying out measurements on the state, the parties must make an irreversible decision about what probability distribution they want to obtain.

This mission is the statement-level formalization of Multipartite Classical and Quantum Secrecy Monotones (arXiv:quant-ph/0202103v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The two classical multipartite secrecy monotones (Abstract; §III, (12)–(17),(24),(28),(30),(35), 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

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

• §II.B.1, exact case of (8)–(11): A general exact finite-block LOPC conversion relation retaining arbitrary initial Eve side information, full public-copy transitions, and independent Eve output registers. (hard)
• §II.B.1, (8)–(11): An approximation metric, growth-controlled continuity modulus, and operational asymptotic rate for general M. (source-ambiguity)
• §III.B: The admissible classical local erasure operations, environment initialization/return constraints, entropy cost, and exact/asymptotic precision convention. (source-ambiguity)
• §V.B: The admissible quantum local erasure operations, environment initialization/return constraints, entropy cost, and exact/asymptotic precision convention. (source-ambiguity)
• §V.E, after (70): A correct equality characterization or a source-specified nondegenerate measurement class. (source-ambiguity)

Selected references

• Multipartite Classical and Quantum Secrecy Monotones, arXiv:quant-ph/0202103v1, https://arxiv.org/abs/quant-ph/0202103v1

Motivation

The purpose of this work is to extend the result of previous papers quant-ph/9611023, quant-ph/9703013 to quantum channels with additive constraints onto the input signal, by showing that the capacity of such channel is equal to the supremum of the entropy bound with respect to all apriori distributions satisfying the constraint. We also make an extension to channels with continuous alphabet. As an application we prove the formula for the capacity of the quantum Gaussian channel with constrained energy of the signal, establishing the asymptotic equivalence of this channel to the semiclassical photon channel. We also study the lower bounds for the reliability function of the pure-state Gaussian channel.

This mission is the statement-level formalization of On Quantum Communication Channels with Constrained Inputs (arXiv:quant-ph/9705054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2: constrained discrete classical–quantum capacity, (10) (Proposition 2: constrained discrete classical–quantum capacity, (10), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Section IV, sentence after (34): A valid shell-probability asymptotic on the source domain of all admissible priors. (source-ambiguity)
• Section IV, (40)-(41) and reliability lower bound: A finite valid optimized reliability lower bound over all pi in P1 and all p>=0 after removal of the shell factor. (source-ambiguity)

Selected references

• On Quantum Communication Channels with Constrained Inputs, arXiv:quant-ph/9705054v1, https://arxiv.org/abs/quant-ph/9705054v1

Motivation

We consider quantum devices for turning a finite number N of d-level quantum systems in the same unknown pure state \sigma into M>N systems of the same kind, in an approximation of the M-fold tensor product of the state \sigma. In a previous paper it was shown that this problem has a unique optimal solution, when the quality of the output is judged by arbitrary measurements, involving also the correlations between the clones. We show in this paper, that if the quality judgement is based solely on measurements of single output clones, there is again a unique optimal cloning device, which coincides with the one found previously.

This mission is the statement-level formalization of Optimal Cloning of Pure States, Judging Single Clones (arXiv:quant-ph/9807010v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Sharp single-clone error bound and explicit attainment (Theorem 1, inequality and Eq.(3), 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

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

• Theorem 1, unrestricted equality iff: Validity of the printed equality-if-and-only-if characterization over every CP unital cloning map. (source-ambiguity)
• Proposition 7: Validity of the printed assertion that the normalized U(d) Haar-average fiber of the canonical cloner is a singleton. (source-ambiguity)

Selected references

• Optimal Cloning of Pure States, Judging Single Clones, arXiv:quant-ph/9807010v1, https://arxiv.org/abs/quant-ph/9807010v1

Motivation

The more than thirty years old issue of the (classical) information capacity of quantum communication channels was dramatically clarified during the last years, when a number of direct quantum coding theorems was discovered. The present paper gives a self contained treatment of the subject, following as much in parallel as possible with classical information theory and, on the other side, stressing profound differences of the quantum case. An emphasis is made on recent results, such as general quantum coding theorems including cases of infinite (possibly continuous) alphabets and constrained inputs, reliability function for pure state channels and quantum Gaussian channel. Several still unsolved problems are briefly outlined.

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

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: general quantum-channel coding theorem (seed) (Theorem 1: general quantum-channel coding theorem (seed), 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

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

• §IV.3, (80)–(81): claimed general constrained reliability exponents: A corrected admissible-prior class and proved subexponential positive shell probabilities, with finite tilted moments, or a different construction proving the unrestricted exponents in (80)-(81). (source-ambiguity)
• §V.2, (100) and piecewise Gaussian reliability comparison: A theorem optimizing both exponent functionals over all admissible priors, or a source-pinned reformulation explicitly limited to the fixed Gaussian prior, with the stationary-s direction corrected. (source-ambiguity)
• §V.4, (148)–(150): formal continuum-noise commutator and covariance: A test-function space, a growth condition on N, a specified finite-part kernel and a smeared CCR/quasifree-state construction on which (149)-(150) are well-defined identities. (source-ambiguity)

Selected references

• Coding Theorems for Quantum Channels, arXiv:quant-ph/9809023v1, https://arxiv.org/abs/quant-ph/9809023v1

Motivation

We show that no distillation protocol for Gaussian quantum states exists that relies on (i) arbitrary local unitary operations that preserve the Gaussian character of the state and (ii) homodyne detection together with classical communication and postprocessing by means of local Gaussian unitary operations on two symmetric identically prepared copies. This is in contrast to the finite-dimensional case, where entanglement can be distilled in an iterative protocol using two copies at a time. The ramifications for the distribution of Gaussian states over large distances will be outlined. We also comment on the generality of the approach and sketch the most general form of a Gaussian local operation with classical communication in a bipartite setting.

This mission is the statement-level formalization of On the impossibility of distilling Gaussian states with Gaussian operations (arXiv:quant-ph/0204052v4). 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 Two-copy Gaussian no-distillation under the restricted Fig.1 protocol (Theorem (p.2); restricted two-copy Gaussian no-distillation result announced p.1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Unnumbered closing sketch: general Gaussian LOCC decomposition: An exact operational Gaussian-LOCC class, including adaptive composition, ideal-limit closure and selective failure branches, and an equivalence theorem for the five-step sketch. (source-ambiguity)

Selected references

• On the impossibility of distilling Gaussian states with Gaussian operations, arXiv:quant-ph/0204052v4, https://arxiv.org/abs/quant-ph/0204052v4

Motivation

We introduce two dual, purely quantum protocols: for entanglement distillation assisted by quantum communication (mother'' protocol) and for entanglement assisted quantum communication (father'' protocol). We show how a large class of children'' protocols (including many previously known ones) can be derived from the two by direct application of teleportation or super-dense coding. Furthermore, the parent may be recovered from most of the children protocols by making them coherent''. We also summarize the various resource trade-offs these protocols give rise to.

This mission is the statement-level formalization of A family of quantum protocols (arXiv:quant-ph/0308044v2). 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 Mother: qubit-assisted entanglement distillation (Mother resource inequality (♀); seed pinned to the first new parent result, 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:

• (7): asymptotic coherent-bit equivalence: Sequential resource protocols with resource-generated startup entanglement and vanishing-rate catalytic recycling (hard)
• Rule I: coherify input classical communication: Retained-environment measured protocol family and constructive input-message coherification (hard)
• Rule O: coherify output classical communication: Retained-environment unitary protocol family and constructive output-message coherification (hard)
• Unnumbered proposed relaxation of Rule I uniformity: Quantified real log-probability equiprobability condition and its entanglement yield (source-ambiguity)
• Constructive hashing-to-mother Rule I adapter: Actual admissible hashing implementation and resource-counted Rule I witness (hard)
• Constructive noisy-super-dense-coding-to-mother Rule O adapter: Specified noisy-super-dense family with full residual decoupling and Rule O transformation (hard)
• Constructive entanglement-assisted-classical-to-father Rule O adapter: Specified retained-environment EAC family, corrected vectorization cleanup and catalytic father adapter (hard)
• Coherifying the new noisy-teleportation child regenerates mother: The constructed noisy-teleportation child family and its coherent regeneration map (hard)

Selected references

• A family of quantum protocols, arXiv:quant-ph/0308044v2, https://arxiv.org/abs/quant-ph/0308044v2

Motivation

The new approach to the theory of complex representrations of the finite symmetric groups which based on the notions of Coxeter generators., Gelfand-Zetlin algebras, Hecke algebra, Young-Jucys-Murphi generators and which hardly used inductive structure - is systematically developed. The appearence of Young diagrams, tables is naturally explained - the set of content vectors of all Young tables is the spectra of Gel'fand-Zetlin algebra. The first steps of the theory (the list of the irrediucible representatinos, branching rule, Young orthopgonal form, Murnagan-Nakayama rule etc.)are established.This appraoch canbe used for other classical series, wreath products with symmetric groups. This paper is the revcised version of the paper of the same authors which was published in Selecta MAth. (New Series) V.2(1996).

This mission is the statement-level formalization of A New Approach to the Representation Thoery of the Symmetric Groups. 2 (arXiv:math/0503040v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5.8: Young branching, content spectrum, and equivalence relations (Theorem 5.8, 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

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

• Proposition 1.1: The full general finite-group tower, its canonical class projectors/path lines, and the global diagonal subalgebra across all irreducibles. (hard)
• Remark 1.2: Canonical lines and all GZ joint characters for an arbitrary simple-branching finite-group chain. (hard)
• Remark 1.3: An arbitrary split finite-dimensional semisimple complex algebra tower with independent GZ and actual branching graph. (hard)
• Theorem 2.4: A corrected general real-star-algebra criterion with explicitly stated representation hypotheses and the missing coefficient-invariance premise. (source-ambiguity)
• Unnumbered classification of finite-dimensional irreducible H(2)-modules: An independently moderated corrected classification specifying both irreducible 1D/2D modules and, at b=a+/-1, the correctly labelled invariant submodule and quotient. Equal a=b must remain allowed in the generic 2D family. (source-ambiguity)
• Remark 5.7: A precise infinite Young-path successor/predecessor map, its domain and exceptional-path convention, and the meaning of finite tableau orbit intervals. (source-ambiguity)
• Unnumbered canonical seminormal construction (6.1), (6.2): The row-reading starting vector, character-product projectors, and the vectors constructed by (6.1), with length filtration. (hard)
• Proposition 6.1: The constructed seminormal basis indexed by ordinary tableaux in each actual shape-labelled irreducible, together with rational descent. (hard)
• Proposition 6.2: A normalized Young basis in an explicitly invariant positive definite Hermitian structure, coherently indexed by tableaux. (hard)
• Remark 6.3: The actual shape-labelled row-reading starting tableau/vector and its lexicographic spectral weight. (hard)
• Corollary 7.1: Shape-labelled actual restriction multiplicities, finite skew-path counts, and an explicit globally sharp factorial family. (hard)
• Unnumbered two-step branching cases: The full two-level interval/multiplicity classification and scalar action on every extended canonical path. (hard)
• Unnumbered uniqueness and normalization claims for deletion: A corrected and distinguished group-valued versus linear projection uniqueness statement, with an accurate threshold; the valid constructed-map identities are already stated separately. (source-ambiguity)
• Proposition 7.2: A source-authorized correction distinguishing the group-valued preimage of the identity from the inverse image of all scalars under the linear extension; do not replace cycle deletion by coefficient truncation. (source-ambiguity)
• Remark 7.4: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
• Theorem 8.1: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
• Murnaghan–Nakayama rule (unnumbered): The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
• Proposition 8.2: An actual ordinary shape-labelled irreducible trace character and the full-hook predicate/height, with the source shape association. (hard)
• Proposition 8.3: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
• Proposition 8.4: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
• Proposition 8.5: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
• Unnumbered strengthening after Proposition 8.5: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)
• Proposition 8.6: The actual skew Hom multiplicity module, centralizer/tail action, coherent skew Young basis, and its ordinary trace character. (hard)

Selected references

• A New Approach to the Representation Thoery of the Symmetric Groups. 2, arXiv:math/0503040v3, https://arxiv.org/abs/math/0503040v3

Motivation

Before the thermodynamic limit, macroscopic averages need not commute for a quantum system. As a consequence, aspects of macroscopic fluctuations or of constrained equilibrium require a careful analysis, when dealing with several observables. We propose an implementation of ideas that go back to John von Neumann's writing about the macroscopic measurement. We apply our scheme to the relation between macroscopic autonomy and an H-theorem, and to the problem of equivalence of ensembles. In particular, we show how the latter is related to the asymptotic equipartition theorem. The main point of departure is an expression of a law of large numbers for a sequence of states that start to concentrate, as the size of the system gets larger, on the macroscopic values for the different macroscopic observables. Deviations from that law are governed by the entropy.

This mission is the statement-level formalization of Quantum Macrostates, Equivalence of Ensembles and an H-Theorem (arXiv:math-ph/0601027v2). 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 Theorem 3.1: equivalence of the three quantum ensembles (Theorem 3.1: equivalence of the three quantum ensembles, 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

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

• §2.1.4: printed spin microcanonical projection construction: A source-corrected directional spin shell and its physical domain. (source-ambiguity)
• §3 opening: equality iff a concentrating canonical maximizer exists: An admissibility/attainment domain for equality of canonical entropy suprema. (source-ambiguity)
• §4.3: printed product-shell Kac microcanonical macrostate: A source-corrected spin factor and domain for the Kac product-shell macrostate. (source-ambiguity)

Selected references

• Quantum Macrostates, Equivalence of Ensembles and an H-Theorem, arXiv:math-ph/0601027v2, https://arxiv.org/abs/math-ph/0601027v2

Motivation

A connected algebraic group in characteristic 0 is uniquely determined by its Lie algebra. In this paper an algorithm is given for constructing an algebraic group in characteristic 0, given its Lie algebra. Using this an algorithm is presented for finding a maximal reductive subgroup and the unipotent radical of an algebraic group.

This mission is the statement-level formalization of Constructing algebraic groups from their Lie algebras (arXiv:math/0612557v1). 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 Chevalley: connected algebraic subgroups generate by uniformly bounded products (Theorem 1 (Chevalley), 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

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

• Unnumbered main result: reconstruct the connected group from its algebraic Lie algebra: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations (source-ambiguity)
• Algorithm 3: terminating closed-product construction of the generated algebraic group: Executable base-field polynomial product-closure, geometric equality testing, and terminating Algorithm 3 loop (hard)
• Algorithm 7: semisimple hull defining polynomials: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations (source-ambiguity)
• Unnumbered main application: compute maximal reductive subgroup and unipotent radical: Effective presentation of arbitrary characteristic-zero F, splitting extension access and complete rational eigenvalue relations; transport/recompute a Levi factor compatible with the newly computed toral complement (source-ambiguity)
• Unnumbered algorithmic consequence of Lemma 11: compute bases of d′ and n: Executable Jordan decomposition, finite Fitting bracket iteration, and finite basis extraction relative to the cited Cartan primitive (hard)

Selected references

• Constructing algebraic groups from their Lie algebras, arXiv:math/0612557v1, https://arxiv.org/abs/math/0612557v1

Motivation

We present an algorithm for the explicit numerical calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients, based on the Gelfand-Tsetlin pattern calculus. Our algorithm is well-suited for numerical implementation; we include a computer code in an appendix. Our exposition presumes only familiarity with the representation theory of SU(2).

This mission is the statement-level formalization of A numerical algorithm for the explicit calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients (arXiv:1009.0437v2). 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 GT Littlewood–Richardson acceptance and multiplicities (§VIII, Eq.(31), Appendix B, PDF p. 9). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• §XII steps 1–3, §I p.1 announcement: Operational exact real-algebraic three-stage GT CG table-construction program, with deterministic rank-ordered product columns and RREF/Gram–Schmidt highest rows, returning all labels, multiplicities and coefficients. (hard)
• §XII polynomial running-time assertion: Specified operation-cost and precision model, uniformity in N and allowed polynomial-constant dependencies. (source-ambiguity)

Selected references

• A numerical algorithm for the explicit calculation of SU(N) and SL(N,C) Clebsch-Gordan coefficients, arXiv:1009.0437v2, https://arxiv.org/abs/1009.0437v2

Motivation

We describe a new method for approximating an arbitrary $n$ qubit unitary with precision $\varepsilon$ using a Clifford and T circuit with $O(4^{n}n(\log(1/\varepsilon)+n))$ gates. The method is based on rounding off a unitary to a unitary over the ring $\mathbb{Z}[i,1/\sqrt{2}]$ and employing exact synthesis. We also show that any $n$ qubit unitary over the ring $\mathbb{Z}[i,1/\sqrt{2}]$ with entries of the form $(a+b\sqrt{2}+ic+id\sqrt{2})/2^{k}$ can be exactly synthesized using $O(4^{n}nk)$ Clifford and T gates using two ancillary qubits. This new exact synthesis algorithm is an improvement over the best known exact synthesis method by B. Giles and P. Selinger requiring $O(3^{2^{n}}nk)$ elementary gates.

This mission is the statement-level formalization of Synthesis of unitaries with Clifford+T circuits (arXiv:1306.3200v1). 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 Approximate Clifford+T synthesis with two ancillas (Theorem 1, 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

• Synthesis of unitaries with Clifford+T circuits, arXiv:1306.3200v1, https://arxiv.org/abs/1306.3200v1

Motivation

In this note we collect several characterizations of unitary representations $(\pi, \mathcal{H})$ of a finite dimensional Lie group $G$ which are trace class, i.e., for each compactly supported smooth function $f$ on $G$, the operator $\pi(f)$ is trace class. In particular we derive the new result that, for some $m \in \mathbb{N}$, all operators $\pi(f)$, $f \in C^m_c(G)$, are trace class. As a consequence the corresponding distribution character $\theta_\pi$ is of finite order. We further show $\pi$ is trace class if and only if every operator $A$, which is smoothing in the sense that $A\mathcal{H}\subseteq \mathcal{H}^\infty$, is trace class and that this in turn is equivalent to the Fr'echet space $\mathcal{H}^\infty$ being nuclear, which in turn is equivalent to the realizability of the Gaussian measure of $\mathcal{H}$ on the space $\mathcal{H}^{-\infty}$ of distribution vectors. Finally we show that, even for infinite dimensional Fr'echet-Lie groups, $A$ and $A^*$ are smoothing if and only if $A$ is a Schwartz operator, i.e., all products of $A$ with operators from the derived representation are bounded.

This mission is the statement-level formalization of On the characterization of trace class representations and Schwartz operators (arXiv:1512.02451v1). 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 Lemma 1.1: integrated operators preserve smooth vectors (Lemma 1.1, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 1.3: Finite-order test topology and canonical Nelson resolvent (hard)
• Unnumbered main consequence: Distribution character on the finite-order test-function topology (hard)
• Theorem 1.4 (Nelson–Stinespring): L1 integrated action and canonical compact Nelson resolvent (hard)
• Unnumbered smoothing factorization, equation (5): Bounded integrated action and the smoothing complex submodule (hard)
• Proposition 1.6: Trace-class representation predicate tied to the actual bounded integrated action (hard)
• Proposition 1.7: Hilbert-Schmidt topology and restricted left action (hard)
• Corollary 1.8: Hilbert-Schmidt joint orbits and the arbitrary-representation Schwartz form (hard)
• Lemma 1.9: Actual derived action, derivative topology and continuous anti-dual (hard)
• Proposition 1.10: Complex trace sandwich pairing on the HS smooth-vector Frechet space (hard)
• Proposition 1.11: Locally convex nuclearity and real distribution dual Gaussian realization (hard)
• Proposition 2.2: Nonnormable locally convex Lie representation and derived sandwich (hard)
• Unnumbered quantitative estimate (7) for derivative sandwiches: Maximal generator weights, unbounded square roots and canonical bounded extensions (hard)
• Remark 2.3(a,b): Locally convex joint C1 calculus and operator-norm orbit derivatives (hard)
• Theorem 2.4: Nonnormable Frechet-Lie smoothness and bounded-form Schwartzness (hard)
• Remark 2.5: Form-defined bounded sandwich and squared maximal-generator domain (hard)
• Theorem 2.6: Merely metrizable locally convex Lie algebra and operator-norm joint smoothness (hard)
• Proposition 2.7: Arbitrary Frechet-Lie Schwartz predicate with actual positive square root (hard)
• Proposition 3.1: Constructed polarized Heisenberg Schrodinger representation and derivative algebra (hard)
• Unnumbered comparison: Coordinate transport and equality of the HS and KKW Schwartz topologies (hard)
• Unnumbered general consequence: General trace-class representation and arbitrary derived Schwartz sandwiches (hard)

Selected references

• On the characterization of trace class representations and Schwartz operators, arXiv:1512.02451v1, https://arxiv.org/abs/1512.02451v1

Motivation

In this paper we consider the $\chi$-function (the Holevo capacity of constrained channel) and the convex closure of the output entropy for arbitrary infinite dimensional channel. It is shown that the $\chi$-function of an arbitrary channel is a concave lower semicontinuous function on the whole state space, having continuous restriction to any set of continuity of the output entropy. The explicit representation for the convex closure of the output entropy is obtained and its properties are explored. It is shown that the convex closure of the output entropy coincides with the convex hull of the output entropy on the convex set of states with finite output entropy. Similarly to the case of the $\chi$-function, it is proved that the convex closure of the output entropy has continuous restriction to any set of continuity of output entropy. Some applications of these results to the theory of entanglement are discussed. The obtained properties of the convex closure of the output entropy make it possible to generalize to the infinite dimensional case the convex duality approach to the additivity problem.

This mission is the statement-level formalization of On entropic quantities related to the classical capacity of infinite dimensional quantum channels (arXiv:quant-ph/0411091v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §6, unnumbered Theorem: convex-duality additivity equivalence and consequences (§6, unnumbered Theorem: convex-duality additivity equivalence and consequences, PDF p. 19). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Section 7, unnumbered energy-continuity assertion: The Hamiltonian domain intended by the unqualified Section 7 mean-energy-continuity sentence. (source-ambiguity)

Selected references

• On entropic quantities related to the classical capacity of infinite dimensional quantum channels, arXiv:quant-ph/0411091v1, https://arxiv.org/abs/quant-ph/0411091v1

Motivation

We show that for a fixed amount of entanglement, two-mode squeezed states are those that maximize Einstein-Podolsky-Rosen-like correlations. We use this fact to determine the entanglement of formation for all symmetric Gaussian states corresponding to two modes. This is the first instance in which this measure has been determined for genuine continuous variable systems.

This mission is the statement-level formalization of Entanglement of formation for symmetric Gaussian states (arXiv:quant-ph/0304042v1). 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 Symmetric Gaussian entanglement of formation (Proposition 2: entanglement of formation of symmetric two-mode Gaussian states, 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

• Entanglement of formation for symmetric Gaussian states, arXiv:quant-ph/0304042v1, https://arxiv.org/abs/quant-ph/0304042v1

Motivation

Previous work on the classical information capacities of bosonic channels has established the capacity of the single-user pure-loss channel, bounded the capacity of the single-user thermal-noise channel, and bounded the capacity region of the multiple-access channel. The latter is a multi-user scenario in which several transmitters seek to simultaneously and independently communicate to a single receiver. We study the capacity region of the bosonic broadcast channel, in which a single transmitter seeks to simultaneously and independently communicate to two different receivers. It is known that the tightest available lower bound on the capacity of the single-user thermal-noise channel is that channel's capacity if, as conjectured, the minimum von Neumann entropy at the output of a bosonic channel with additive thermal noise occurs for coherent-state inputs. Evidence in support of this minimum output entropy conjecture has been accumulated, but a rigorous proof has not been obtained. In this paper, we propose a new minimum output entropy conjecture that, if proved to be correct, will establish that the capacity region of the bosonic broadcast channel equals the inner bound achieved using a coherent-state encoding and optimum detection. We provide some evidence that supports this new conjecture, but again a full proof is not available.

This mission is the statement-level formalization of Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture (arXiv:0706.3416v1). 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 Conditional coherent-state capacity region (Section IV, Eqs. (1), (16)-(17); PDF pp.1,3-5, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Section V / Figure 4, PDF pp.6-7: The exact MAC photon-budget/power-allocation constraint defining the envelope compared with the coherent bosonic broadcast region. (source-ambiguity)

Selected references

• Classical capacity of bosonic broadcast communication and a new minimum output entropy conjecture, arXiv:0706.3416v1, https://arxiv.org/abs/0706.3416v1

Motivation

We introduce a new form for the bosonic channel minimal output entropy conjecture, namely that among states with equal input entropy, the thermal states are the ones that have slightest increase in entropy when sent through a infinitesimal thermalizing channel. We then detail a strategy to prove the conjecture through variational techniques. This would lead to the calculation of the classical capacity of a communication channel subject to thermal noise. Our strategy detects input thermal ensembles as possible solutions for the optimal encoding of the channel, lending support to the conjecture. However, it does not seem to be able to exclude the possibility that other input ensembles can attain the channel capacity.

This mission is the statement-level formalization of The bosonic minimum output entropy conjecture and Lagrangian minimization (arXiv:0906.2758v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal and displaced thermal stationary witnesses and local output-entropy minima (Unnumbered main result: thermal stationarity and local output-entropy minima, 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

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

• Section I: finite conjecture: A proved unrestricted global vacuum-output entropy bound, rather than its conjecture. (hard)
• Section I: infinitesimal fixed-entropy conjecture: A proved global fixed-entropy instantaneous-rate inequality. (hard)
• Section VIII: claimed equivalence: A reverse implication from the finite pure-input minimum to the positive-entropy rate conjecture. (source-ambiguity)
• Section II, Eq.(5): entropy trace expansion: A source-specified trace differentiability domain and controlled second-order entropy remainder. (source-ambiguity)
• Section IV, Eqs.(6)–(8): all-cutoff stationarity: An exact N-to-N+1 cutoff dynamics, its rectangular dual, and order-of-time convention. (source-ambiguity)
• Section IV: energy-minimum attainment in a connected minimum manifold: A source-supported attainment condition on every connected minimum component. (source-ambiguity)
• Section V, Eqs.(9)–(13): double-stationary classification: Consistent complete primal/dual stationarity equations and common unbounded domains for all candidate solutions. (source-ambiguity)
• Section VI, Eq.(14): full thermal perturbation expansion: Norm/domain and remainder bound for the complete infinite-dimensional Eq.(14). (source-ambiguity)
• Section VII: attributed stationarity sufficiency: A valid second-order or convexity sufficiency hypothesis for Eq.(16). (source-ambiguity)
• Appendix 1: cutoff-independent stationary solutions and their limit: Consistent cutoff CCR, truncated Gibbs normalization, and a stationary-limit theorem. (source-ambiguity)
• Appendix 2: unqualified boundary asymptotic coefficient: A pinned, correct general boundary leakage coefficient and its trace domain. (source-ambiguity)

Selected references

• The bosonic minimum output entropy conjecture and Lagrangian minimization, arXiv:0906.2758v3, https://arxiv.org/abs/0906.2758v3

Why loan trading can change bank capital

Banks that can sell loans after origination may face different incentives to screen them before lending. A buyer that has invested in screening can inspect a seller's loan and buy it when its quality is high. That opportunity can make screening more valuable and reduce the equity a buyer needs to commit. At the same time, a seller may prefer to avoid the screening cost and rely on a later sale. Song and Thakor study when these two choices coexist in an interbank market, even though banks begin with the same opportunities and information (Song and Thakor, SSRN 3667175). The resulting question concerns the capital structure of banks and whether a trading market opens a region of heterogeneous behavior between two homogeneous regimes.

The paper's Proposition 2 is a result about this transition as the chance of a boom changes. It also compares the width of the heterogeneous region across market efficiencies. The mission formalizes that result from the authors' specified model and their preprint's assumptions. The preprint describes the paper as forthcoming in Management Science; the DOI record identifies the associated journal work.

The model and its quantities

A good loan pays $X>I$ at its final date. A medium loan pays $X$ in a boom and zero in a recession. Both require an initial investment $I$. The probability of a boom is $\theta\in[0,\bar\theta]$, with $\bar\theta<I/X$, so a medium loan is not creditworthy on its own. Before a bank screens, each type has probability one half. Screening costs $c$ and reveals the type. A bank can finance the loan with deposits and equity; supplying one unit of equity costs insiders $\psi$ per unit. Default also loses the bank its charter value $Y(\theta)$. The paper restricts $X,I,c,\delta,\psi,\bar\theta$, and $Y$ by Assumptions 1–4 and fixes the matching technology by Assumption 5 (preprint, pp. 7–12); $Y$ is increasing and concave.

Without loan trading, the minimum screening equity is $E^{\mathrm{hom}}(\theta)$, the profit from screening is $\pi_s^{\mathrm{hom}}(\theta)$, and the profit without screening is $\pi_{ns}^{\mathrm{hom}}(\theta)$. Their difference, $\Delta\pi^{\mathrm{hom}}(\theta)$, is the screening advantage. The paper writes each quantity as an explicit real-valued function of $\theta$ in equations (8)–(11). A cutoff $\theta^*$ separates the choices when the loan market is closed (Proposition 1, p. 15).

With trading, some banks can be buyers that screen, while others are sellers that do not. If buyers have mass $N_b$ and sellers mass $N_s$, market tightness is $n=N_b/N_s$. A seller meets a buyer with probability $\alpha(n)=\lambda n/(1+n)$; a buyer meets a seller with probability $\lambda/(1+n)$. Here $\lambda\in[0,1]$ measures matching efficiency. The buyer's bargaining weight is $1/(1+n)$, and the price for a verified good loan is $p(n)=X-(X-I)/(1+n)$. Trading reduces the buyer's required equity to $E^{\mathrm{het}}(\theta,n)=E^{\mathrm{hom}}(\theta)-\lambda(X-p(n))/(1+n)$ (Assumption 5, equation (13), and Lemma 1; the matching function follows Kiyotaki and Wright (1993)).

Formalization targets

The main target is Proposition 2, p. 21. Under the paper's assumptions and its endpoint conditions, there are cutoffs $0<\theta_L<\theta_H<\bar\theta$. Every bank screens below $\theta_L$; none screens above $\theta_H$; between them, buyers and sellers coexist. In the interior the buyer/seller ratio is determined by

$$\lambda(X-I)\left[\frac{1-\theta}{2}\frac{n-1}{n+1}-\frac{\psi}{(n+1)^2}\right] =\Delta\pi^{\mathrm{hom}}(\theta).$$

The two cutoffs solve the paper's equations (A4) and (A7). The mission also targets uniqueness of the equilibrium in every regime, expansion of the heterogeneous region when a larger feasible $\lambda$ is used, and falling $n$ and $p(n)$ as $\theta$ rises within that region. The milestone list covers the matching identities of Assumption 5, the Nash price (13), Lemma 1's equity threshold, the monotonicity of $E^{\mathrm{hom}}$ (footnote 19), the sign form of the cost condition (A1), the strict concavity of $\Delta\pi^{\mathrm{hom}}$, the closed-market cutoff of Proposition 1, the two trading cutoffs (A4) and (A7), the interior indifference equation (A9)/(15), and the monotonicity in $n$ of the left side of (15) (Appendix A, pp. 34–37).

What the result establishes

The result identifies a region in which banks that started alike choose different capital structures and screening decisions. A loan-trading market changes the relative payoffs of screening and not screening, and the boom probability determines which choice can survive a unilateral switch. The cutoffs show precisely where the market moves from all-screening to mixed behavior and then to no-screening. The market-efficiency comparison says when the mixed region widens. These distinctions matter for the paper's subsequent welfare comparison and its discussion of capital requirements (Song and Thakor, §§3–4).

The result is proved in the source paper. The remaining work is a machine-checked proof of the model-specific statements and their consequences, including the bargaining maximum, incentive threshold, cutoff existence and uniqueness, and comparative statics. The definitions are reusable for further formal work on the paper's welfare and capital-requirement results; this mission does not assert that those extensions have been formalized.

Main mathematical difficulty

The equilibrium claim joins several regimes in one statement. The homogeneous corners are governed by whether a single bank would gain by changing its behavior, whereas the interior is governed by equality of buyer and seller profits. A root of the displayed equation alone does not establish an equilibrium: the cutoff and no-switch conditions must also hold, and the root must be unique. Moreover, the source's claimed global negative derivative for $\Delta\pi^{\mathrm{hom}}$ is not implied by its assumptions. The cutoff argument must therefore use a valid shape condition without importing that false assertion. The charter-value function $Y$ is concave but otherwise general, so reasoning cannot rely on a particular polynomial example.

Formalization scope

Lean represents all expectations by the closed-form real expressions in equations (7)–(15); there is no probability space. The parameter structure fixes $X,I,c,\delta,\psi,\lambda,\bar\theta$, and $Y$. All five numbered assumptions remain explicit, including Assumption 4. The formalization reads screening cost and equity cost as positive, reads the paper's smooth $Y$ as differentiable on $[0,\bar\theta]$, and requires $\lambda>0$ for an open market. The bargaining price is optimized over $[I,X]$. The buyer meeting probability uses its continuous value $\lambda$ at $n=0$. Proposition 1 uses a reduced closed-market outcome that records screening and equity; at its profit tie, footnote 21 selects no screening. The open-market equilibrium variable is the buyer share $s\in[0,1]$, with $n=s/(1-s)$ only in the interior; the all-buyer corner uses the sole-seller limit instead. Price and buyer equity are constructed from the paper's equations, and are never arbitrary choices. The cutoffs are required to satisfy $0<\theta_L<\theta_H<\bar\theta$, so all three regimes are nonempty; a version in which the equilibrium is any root of (15), or in which price or buyer equity are free variables, would be a different and weaker statement and is excluded. The hypotheses are jointly satisfiable, but only for small market efficiency (numerical searches find $\lambda\lesssim0.015$); an explicit rational instance is checked in Lean.

The preprint prints a plus sign in (A6) where its preceding deviation inequality requires a minus sign; the Lean condition uses the latter. The paper also claims that the absolute sensitivity of $n$ to $\theta$ falls with $\lambda$, but that claim is false under its hypotheses, so the mission does not include either sensitivity clause of Proposition 2. The paper's unsupported global first-derivative bound for $\Delta\pi^{\mathrm{hom}}$ is excluded. The milestone from the proof of Proposition 5 states its displayed second-derivative identity wherever $Y''$ exists, and states strict concavity throughout the interval. Any further result should keep these corrections explicit. Contributions to the bargaining, real-analysis, and equilibrium lemmas are welcome; proofs of the milestone statements can then support the capstone theorem.

Selected references

• N. Kiyotaki and R. Wright, A search-theoretic approach to monetary economics, American Economic Review 83(1), 63–77, 1993. JSTOR
• F. Song and A. V. Thakor, Market Freeze and Bank Capital Structure Heterogeneity, SSRN preprint 3667175, version dated 2022-02-21; forthcoming in Management Science in the source artifact. SSRN; DOI.

Motivation

Rooftop solar changes both a household's electricity bill and the utility's cost of serving its customers. A tariff that encourages an aggregate amount of solar generation can still leave one customer tier paying more than before. Regulators therefore face a joint design question: can they induce a chosen adoption pattern while meeting the solar supplier's and utility's profit requirements and protecting every customer tier? Singh and Scheller-Wolf formulate this question for a solar company that sells generation through a power purchase agreement, a regulated utility, and households grouped into tiers. Their SSRN paper studies several tariff families; Proposition 5 identifies a tiered tariff that can implement the selected outcome and, when the customers' aggregate financial gain is nonnegative, avoid cross-subsidization.

The selected outcome is assumed to have been chosen for social welfare reasons. The result concerns the next task: implementing it through the tariff while customers decide whether to adopt and the solar company chooses its price. That distinction matters because a tariff that appears to allocate enough money to all parties may change the solar company's preferred price, and therefore change which households adopt.

Setting

There are finitely many customer tiers $i$. Tier $i$ contains $h_i$ households. Each household has annual electricity demand $d_i$, potential solar generation $g_i$, and excess generation $e_i$. If it adopts solar, it draws $d'_i=d_i-(g_i-e_i)$ from the grid and sells $e_i$ back. The target adopting set $A$ identifies the tiers whose households install solar. Let $E^0=\sum_i h_i d_i$ be baseline utility demand, $\Delta_E^A=\sum_{i\in A}h_i g_i$ the target rooftop generation, and $E^A=E^0-\Delta_E^A$ net utility demand. The paper restricts attention to outcomes with at least one adopting tier and $\Delta_E^A\le E^0$ (§3, pp. 10–11).

The regulator sets a tariff $T(d',e,s)$, a customer's utility bill based on grid draw $d'$, electricity sold to the grid $e$, and adoption indicator $s$. For tier $i$, the two relevant bills are $T(d_i,0,0)$ and $T(d'_i,e_i,1)$. A solar company chooses a single price $p_s$ per unit generated by adopting households and pays unit cost $c_s(y)$ when its sales volume is $y$. Each customer adopts when its adopter bill plus $p_sg_i$ is no larger than its nonadopter bill. With ties favoring adoption, this is $p_s\le t(i)$, where $t(i)=[T(d_i,0,0)-T(d'_i,e_i,1)]/g_i$. Thus the solar company's price determines both its sales volume and its unit cost (§§3–4, pp. 10–13).

The regulator's P2 objective is the largest increase in a tier household's cash outflow relative to the baseline rate $p_{r0}$. A nonpositive objective means no tier is financially worse off, which the paper calls cross-subsidization free. P2 also requires a specified solar-company profit $\Delta_S$ and utility profit change $\Delta_U$. Write $\Delta_{WF}$ for the financial welfare improvement of the whole system and $\Delta_C=\Delta_{WF}-\Delta_S-\Delta_U$ for customers' aggregate financial gain (§4, pp. 12–15).

Formalization targets

Proposition 5(a): inducing the target outcome

Tariffs of type $T_3$ charge nonadopters $p_rd_i$ and adopters $p_rd'_i-p_re_i+f_i$, where $p_r$ is a common rate and $f_i$ a tier-specific adopter charge. The paper constructs one such tariff, $T^*$, from the target outcome. At its prescribed price $t(m)$, the target tiers adopt, the solar company earns $\Delta_S$ and earns strictly less at every other price, and the utility receives its specified profit change $\Delta_U$:

$$A(t(m))=A,\qquad \Pi_S(t(m))=\Delta_S>\Pi_S(p)\quad(p\ne t(m)),\qquad \Delta\Pi_U=\Delta_U.$$

This is the feasibility claim of Proposition 5(a), p. 18.

Proposition 5(b): equity and optimality

When the aggregate customer gain is nonnegative, $T^*$ has a nonpositive P2 objective:

$$\Delta_C\ge0\quad\Longrightarrow\quad\max_i\Delta\mathrm{outflow}_i(T^*,t(m))\le0.$$

If a tier with the smallest demand does not adopt, Proposition 5(b) further says $T^*$ minimizes this objective among feasible $T_3$ tariffs. Both clauses belong to the combined goal theorem. The milestone list also includes the customer threshold, the welfare identity, the $T_3$ threshold formula, Proposition 5(a), Lemma 1, the retail-rate identity for $T^*$, and the cross-subsidization clause (p. 18 and proof on p. S.3).

Significance

Proposition 5 gives a tariff implementation for any admissible target adoption set without relying on control of the solar company's price. Its equity guarantee has a clear limit: it requires nonnegative aggregate customer gain. Within the paper's $T_3$ family, the additional lowest-demand condition gives an exact minimax result for customers' bill changes (Proposition 5, p. 18). This distinguishes the existence of an implementing tariff from its distributional performance.

The mathematical result is already proved in the paper; this mission asks for a machine-checked development of its model, construction, and claims. The reusable pieces include finite-tier induced-adoption sets, price-dependent sales volume, and the accounting identities between company profits and customer outflows. The statements in this proposal are proof targets and do not claim an existing Lean proof.

Difficulty

Setting each customer's adoption threshold to produce $A$ is insufficient by itself. The solar company chooses $p_s$ to maximize profit, and a change in price can change both the adopting set and the unit cost $c_s(y)$. The prescribed price must beat every alternative real price strictly. The utility's required profit change constrains the same tier fees used to set thresholds. Finally, a nonnegative total customer gain does not by itself imply that every tier benefits; P2 asks about the largest individual tier increase. These coupled requirements are visible in the paper's P2 formulation and in the proof of Proposition 5 (pp. 13–14, 18, S.3).

Formalization scope

Lean represents tiers by a finite type and outcomes by finite sets of tiers. All demands, prices, bills, costs, volumes, and profit changes are real. The tier type is unordered: the paper relabels tiers during $T^*$'s construction. A tariff is represented by its two bills per tier, the evaluations P2 uses. For $T_3$, fees are indexed by tier, consistent with the paper's statement that the utility can infer a solar customer's tier from grid draw (p. 17). Adoption ties go to adoption, and the solar company's price ranges over all real numbers. P2 feasibility includes the induced adopter set, the firm's unique best response, and the utility constraint.

The standing assumptions state $h_i,d_i,g_i>0$, $0\le e_i\le g_i$, nonincreasing $c_s$, and $\Delta_S>0$. Positivity of $h_i,d_i,g_i$ is implicit in the paper and makes the displayed volume and price divisions valid. The target set is nonempty and satisfies $\Delta_E^A\le E^0$. The utility's total generation cost is outside the household sum in its accounting constraint; this is the reading consistent with the paper's welfare identity. The printed indexing slips in (17) and (19) are avoided by expressing the induced equilibrium directly. Customer aggregate gain is computed from $\Delta_{WF}-\Delta_S-\Delta_U$, rather than defined from the desired conclusion. The optimality quantifier covers feasible $T_3$ tariffs, the family studied in §4.3. Contributions may develop the equilibrium argument, the accounting lemmas, the $T^*$ rate identity, or the complete optimality proof.

Selected references

• Singh, S. P., and A. Scheller-Wolf, That’s Not Fair: Tariff Structures for Electric Utilities with Rooftop Solar, SSRN version, 2022. SSRN 2926676. Source for all statement and appendix page references in this mission.
• Singh, S. P., and A. Scheller-Wolf, That’s Not Fair: Tariff Structures for Electric Utilities with Rooftop Solar, Manufacturing & Service Operations Management 24(3), 2022. DOI:10.1287/msom.2020.0930. Published bibliographic record; the mission cites the SSRN version's numbering and pages.

Motivation

A standard-essential patent is a patent that an implementer must use to make a product compliant with a technical standard. Its owner may demand a royalty from firms using the standard. Whether a patent is truly essential can be disputed, yet licensing offers and investment decisions are made before a court resolves that dispute. Standard-setting organizations can commission essentiality checks that certify patents before licensing. Better checks identify more patents that are not essential, but they also change what an implementer believes about a patent that passes the check. Schuett and Wipusanawan study how those two effects interact with litigation and research investment in their TILEC discussion paper, §§2–5.

A common policy intuition is that a more accurate check should save litigation costs by excluding weak patent claims. The paper identifies a countervailing effect in a model where an innovator chooses research effort before it knows whether its patent will be essential. The question here is local: when a small increase in check accuracy leaves each state's licensing regime unchanged, how does equilibrium welfare change if the patent owner faces no effective cap on royalties? The paper's Proposition 1 answers this question, building on its licensing, investment, and welfare formulas Schuett and Wipusanawan, pp. 16–25.

Setting

An upstream firm chooses research effort $x\in[0,1]$ at cost $c(x)$. Research succeeds with probability $x$. Following success, the standard uses the firm's technology, its patent is essential, and the commercial value is one of finitely many values $v_i$ with probabilities $p_i^H$. Following failure, the standard uses a status-quo technology, the patent is not essential, and value $v_i$ occurs with probability $p_i^0$. The separate distribution $p^L$ for the unsuccessful upstream technology enters the paper's assumption that the status quo has higher expected value than that technology. The model requires $\sum_i p_i^H v_i>\sum_i p_i^0 v_i>\sum_i p_i^L v_i$ Assumption 1, p. 10.

An essentiality check certifies an essential patent correctly. It also certifies a non-essential patent in error with probability $1-\beta$, where $\beta\in[0,1]$ is accuracy. After observing certification and value, the upstream firm offers a royalty fraction $\alpha_i$ bounded by $\bar\alpha\in(0,1]$. The downstream firm can accept or litigate. Litigation costs each firm $l_i$; the court determines essentiality correctly. A non-certified patent earns the upstream firm no licensing revenue in this model. The paper assumes $l_i<\bar\alpha v_i$ Assumption 2, p. 12.

A certified patent can produce a hybrid licensing outcome, in which the unsuccessful firm sometimes offers a low royalty and the downstream firm sometimes litigates a high offer, or a pooling outcome, in which both types offer the maximum royalty. Write $H$ and $P$ for the sets of states with those outcomes. The implementer's belief that a certified patent is essential, $\lambda_i^c$, depends on expected effort $\hat x$, accuracy $\beta$, and the value distributions. In equilibrium, $\hat x=x^*$. The paper derives a private investment wedge from the difference between expected licensing revenues after success and failure, and a social wedge from expected value less both parties' litigation costs equations (1)–(7), pp. 16–22.

Formalization targets

The main target is Proposition 1. With an ineffective royalty cap, $\bar\alpha=1$, fix $\beta_0<1$ where no positive-probability state lies exactly at the hybrid–pooling boundary. Along a continuous path of nearby equilibrium efforts $x^*(\beta)$, the right derivative of welfare $w$ satisfies

$$\frac{d}{d\beta}w\bigl(\beta,x^*(\beta)\bigr)\bigg|_{\beta_0+}\le 0.$$

The inequality is weak because the paper concludes $\partial w^*/\partial\beta\le0$ Proposition 1 and its proof, pp. 24–25. The target concerns a marginal increase that preserves the licensing regimes; it makes no claim about a large change that moves states between $H$ and $P$.

The milestone statements cover the regime condition (4), the private revenue wedge (5), the welfare identity (6), Lemma 2's positive response of research effort to accuracy, and Lemma 3's comparison of private and social investment incentives. Their order exposes the quantities the goal uses without replacing Proposition 1 with a narrower fixed-regime statement.

Significance

Within this model, the result says that improved screening can lower welfare when unconstrained licensing already induces too much research investment. It identifies a limit on an intervention aimed at reducing disputes over essentiality: even a check that detects more non-essential patents may change the incentives of firms whose patents pass. This is a statement about the model's local equilibrium, not a claim that every real-world checking program lowers welfare. The paper separately examines changes large enough to alter licensing regimes and the case of an effective royalty cap Schuett and Wipusanawan, §§5–6.

The economic theorem is proved in the cited paper. This mission asks for a machine-checked account of its finite-state model and the local welfare claim; the displayed Lean statements are open proof targets. The shared definitions of certification beliefs, licensing outcomes, revenue, and welfare are useful for checking later variants of the model, including alternative certification errors or royalty caps. No machine-checked proof of this paper's proposition is claimed here.

Difficulty

The local comparison crosses three choices. Accuracy changes the chance that a failed innovator is certified. Certification changes the downstream firm's belief when it sees a high royalty. The resulting licensing outcome affects the innovator's incentive to invest, and effort feeds back into the belief. Simply holding effort fixed misses the welfare effect in Proposition 1. Treating the hybrid and pooling sets as fixed for all accuracy levels is also too broad: the paper restricts the result to a neighborhood where the regime condition does not meet equality. At a boundary, the relevant formulas can switch and the local derivative need not have the same form pp. 20, 24–25.

Formalization scope

The Lean model uses real values and probabilities on a finite state type Fin n. Each of $p^H$, $p^L$, and $p^0$ is a nonnegative probability vector. Assumptions 1 and 2, $0<\bar\alpha\le1$, and the paper's increasing convex research cost with $c'(0)=0$ and $c'(x)\to\infty$ as $x\uparrow1$ are explicit standing conditions. The cost is represented by a real function twice continuously differentiable on $(-\infty,1)$, which covers the effort domain below one. Equilibrium effort is interior and satisfies the private first-order condition with the implementer's belief equal to effort.

Three premises used in the paper's argument are made explicit. Litigation costs satisfy $l_i>0$. The second derivative at the equilibrium effort satisfies $c''(x^*)>0$, as required by the displayed denominator in Lemma 2; convexity alone gives only nonnegativity. A right-continuous equilibrium-effort path supplies nearby equilibria for the local comparison. The derivative is one-sided because the target concerns an increase from $\beta_0$, including $\beta_0=0$. Strictness of the regime condition is demanded only for states with positive probability under $p^H$ or $p^0$; an absent state cannot affect welfare or investment.

The belief formula is the paper's ratio when its denominator is positive. Its value at a zero-probability state is immaterial to the weighted outcome; the regime milestone also gives a cross-multiplied condition there. Uncertified patents give the upstream firm zero revenue, and the downstream firm retains value without litigation. Welfare is assembled from the two firms' payoffs in every certification and licensing outcome, then related to equation (6). Defining welfare directly by (6), fixing $H$ in the goal, or assuming the derivative of $x^*$ would remove the main work of the proposition. Contributions to the finite-state payoff model, the regime and welfare identities, and the local derivative and wedge comparison are all within scope.

Selected references

• F. Schuett and C. Wipusanawan, Essentiality Checks for Standard Essential Patents, TILEC Discussion Paper DP 2023-21, December 2023, SSRN 4688864. The pinned discussion-paper version is the citation basis for every page and equation in this mission.
• F. Schuett and C. Wipusanawan, Essentiality Checks for Standard Essential Patents, Management Science, 2024, DOI 10.1287/mnsc.2023.04292. The mission does not use the journal pagination.

Motivation

Bundle methods minimize a convex objective while using local supporting affine functions to represent a component that may be nonsmooth. Their iterations can spend time improving the model without moving the current proximal center, so a bound on useful center changes alone does not bound the total work. Liang and Monteiro study a common generic proximal bundle (GPB) framework for several model update rules and give one explicit iteration bound that covers every rule admitted by its bundle update blackbox. The result is a proved theorem in their paper, rather than an open complexity conjecture.

The framework matters when a convex objective combines a component supplied through subgradients with another component whose proximal subproblems can be handled directly. One-cut, two-cut, and multiple-cut bundle updates fit the same abstract requirements in the paper. A common statement makes their guarantees comparable without identifying a specific update formula as canonical.

Setting

The problem is to minimize hybrid convex composite objective $\phi=f+h$ over $\mathbb R^n$. The effective domain $D=\operatorname{dom}h$ is nonempty and contained in the domain of $f$. The function $h$ is lower semicontinuous and $\mu$-convex, for $\mu\ge0$: its convexity inequality gains the quadratic term $\mu\alpha(1-\alpha)\|x-y\|^2/2$. For each $x\in D$, a chosen subgradient $f'(x)$ defines a supporting affine cut

$$\ell_f(u;x)=f(x)+\langle f'(x),u-x\rangle.$$

The hybrid oracle condition allows both a constant and a distance-dependent part:

$$\|f'(x)-f'(y)\|\le 2M_f+L_f\|x-y\|\qquad(x,y\in D),$$

where $M_f,L_f\ge0$. For tolerance $\bar\varepsilon>0$, the pair $(\bar M_f,\bar L_f)$ minimizes $M^2+\bar\varepsilon L$ among all nonnegative pairs satisfying the same condition. An optimal point $x_0^*$ nearest the initial point $x_0\in D$ exists under the paper's assumptions, and $d_0=\|x_0-x_0^*\|$.

A GPB run is an infinite sequence of points $x_j$, best-so-far points $y_j$, centers $x_j^c$, and convex bundle models $\Gamma_j$. At a serious update, the next center is the current point and the next model lies between $\ell_f(\cdot;x_j)+h$ and $\phi$. At a null update, the center stays fixed and a bundle update blackbox selects the next model. Its output must dominate a mixture of a fresh cut and an auxiliary model $\bar\Gamma_j$ that agrees with the previous model at $x_j$ and has $x_j$ as its proximal minimizer. Every new $x_j$ minimizes its model plus the squared distance to its center divided by $2\lambda$. The best-so-far point $y_j$ minimizes the observed objective values. The gap $t_j$ compares $\phi(y_j)$ with the proximal model value; a step is serious when $t_j\le\bar\varepsilon/2$.

Formalization targets

The goal is Proposition 4.9, an explicit total iteration bound for every run admitted by GPB when $\tau$ is set by equation (38). Put $\lambda_\mu=\lambda/(1+\lambda\mu)$ and

$$\bar t=\bar M_f^2+4(\bar L_f+2) \bigl(\max\{1,2\lambda\bar L_f\}d_0+\lambda\bar M_f\bigr)^2.$$

There is an index $j$ with $\phi(y_j)-\phi^*\le\bar\varepsilon$ and

$$j\le\left( \left\lceil\left(1+\frac{8\lambda_\mu(M_f^2+\bar\varepsilon L_f)}{\bar\varepsilon}\right) \max\left\{\log\frac{4\bar t}{\bar\varepsilon},0\right\}\right\rceil+1\right) \left(\operatorname{serBound}(\mu,\lambda,\bar\varepsilon,d_0^2)+1\right).$$

Here $\operatorname{serBound}$ is the minimum of the two serious-iteration expressions in (61), with the paper's limiting convention at $\mu=0$. The milestones follow the two quantities in this product: Corollary B.2 and Lemma 4.2 yield the serious-iteration estimate; Proposition 4.3 packages it. Equation (7), Lemmas 4.6, A.3, and 4.7 bound the behavior within each cycle; Proposition 4.8 bounds the cycle length. The goal combines the two bounds without selecting one concrete bundle update.

Significance

The theorem gives a finite tolerance certificate with a numerical bound on all iterations, including those that only improve the bundle model. The bound depends on the oracle parameters, curvature, initial distance to the solution set, tolerance, and proximal stepsize. It therefore states what an implementation gains by satisfying the BU conditions even when its internal model construction differs from another implementation. The broader paper also analyzes particular update schemes and an adaptive method, but the target here is the common GPB result Liang and Monteiro, §3–4.

The mathematical result is already proved in the source. This mission asks for machine-checked definitions and proofs of its explicit bound and the selected supporting statements. No machine-checked proof is supplied by these open theorem items. The definitions of the hybrid oracle, proximal model, and abstract GPB run can be reused to formalize the paper's concrete update schemes later.

Difficulty

Counting serious steps does not count intervening null steps. A null step can leave the center fixed while the model changes, and the BU condition permits many such models. The main obstacle is to obtain a uniform bound for a complete cycle from conditions that are local to one model update. The separate analytic obstacle is the hybrid descent estimate (7): the oracle bound contains both a constant term and a term proportional to distance, and the needed quadratic coefficient is $L_f/2$, not the easier $L_f$. The source's auxiliary proximal displacement estimate also depends on lower semicontinuity so that its minimizers exist.

Formalization scope

The Lean space is EuclideanSpace ℝ (Fin n), with its usual norm and real inner product. The function domain $D$ stands for $\operatorname{dom}h$; $f$, $h$, and each bundle model are real-valued on $D$, with an extended value $+\infty$ off $D$ when lower semicontinuity is stated. All model inequalities and proximal minimizations are over $D$. This represents the paper's extended-valued functions without ambiguous arithmetic at $+\infty$. The selected subgradient inequality is also required only on $D$. The source's lower semicontinuity of $f$ and of the BU auxiliary model is omitted, which strengthens the resulting claims; lower semicontinuity of $h$ and of each generated model remains. The abstract serious-iterate sequences explicitly keep their auxiliary points in $D$.

Index zero is initialization and counts as serious because $t_0=0$; subsequent indices are natural numbers. The GPB run predicate retains the existential auxiliary model in every null update, so it covers every admissible variant. The goal concludes existence of a successful bounded index. It assumes $M_f^2+\bar\varepsilon L_f>0$ so equation (38) defines $\tau\in(0,1)$. For $\mu=0$, the serious-step formula uses the limiting value rather than real division by zero. The printed cycle and total bounds omit an integer rounding and can be too small; the formal targets use a ceiling and a nonnegative logarithm. Lemma 4.2(c), Lemma A.3, and Lemma 4.7 carry the additional qualifications needed by their printed proofs, disclosed beside their statements.

The development needs Mathlib's finite-dimensional Euclidean spaces, convexity, lower semicontinuity, and real logarithm, plus real-sequence and finite-index estimates. Contributions proving the milestones, the goal, or reusable facts about the GPB model are within scope. A proof for one fixed update formula alone does not establish the goal over the BU blackbox.

Selected references

• J. Liang and R. D. C. Monteiro, A Unified Analysis of a Class of Proximal Bundle Methods for Solving Hybrid Convex Composite Optimization Problems, Mathematics of Operations Research, 2024; source used here: arXiv:2110.01084v3, 2023, §§2–4 and Appendices A–B.

Motivation

Large language models answer reasoning questions better when they are allowed to write out a chain of thought (CoT) before the final answer, but every generated token costs time and money. A large body of recent work therefore asks models to "think less": prompts such as "be concise" or "use at most 10 words", and training methods that shorten the reasoning trace. These methods trade accuracy for length, and the natural question is how good such a trade can possibly be.

Lee, Che and Peng (2025) study this question empirically on MATH-500, GSM8K and MMLU-Pro Math with 31 prompts and several frontier models. Their key observation is that, question by question, correctness is almost a threshold function of the response length: a model solves a question if and only if its chain of thought is at least as long as a question-specific token complexity. Under this hypothesis they derive the best possible accuracy–length tradeoff over all prompts, and show that existing prompting strategies are far from it (Table 4 of the paper). This mission formalizes that derivation: Theorem 1 of the paper and the steps of its proof in Appendix D.

Setting

Fix one language model and a dataset of $n \ge 1$ questions $i = 1, \dots, n$. A prompt $P$ determines, for each question $i$, a chain of thought of token length $t_i(P) \in \mathbb N$ and a correctness indicator $a_i(P) \in \{0, 1\}$. The accuracy and the average token length of a prompt are

$$\mathrm{Acc}(P) = \frac1n \sum_{i=1}^n a_i(P), \qquad \bar t(P) = \frac1n \sum_{i=1}^n t_i(P).$$

The two optimal tradeoff curves are the optimal accuracy at average budget $T$ and the minimal average length for accuracy $\alpha$:

$$\alpha^*(T) = \max_P \{\mathrm{Acc}(P) : \bar t(P) \le T\}, \qquad T^*(\alpha) = \min_P \{\bar t(P) : \mathrm{Acc}(P) \ge \alpha\}.$$

Assumption 1 (token complexity hypothesis). There are numbers $\tau_i \in \mathbb N \cup \{\infty\}$, the token complexities, such that for every prompt $P$ and question $i$,

$$a_i(P) = \mathbf 1\{t_i(P) \ge \tau_i\}.$$

The value $\tau_i = \infty$ marks a question the model never solves. The paper also assumes the prompts are rich: every vector of token counts $(t_i) \in \mathbb N^n$ is produced by some prompt. The answer is expressed through the empirical quantities

$$F_n(t) = \frac1n \sum_{i} \mathbf 1\{\tau_i \le t\}, \qquad E_n(t) = \frac1n \sum_{i} \tau_i \mathbf 1\{\tau_i \le t\}, \qquad A^* = \frac1n \sum_i \mathbf 1\{\tau_i < \infty\},$$

where $A^*$ is the largest accuracy any prompt can reach.

Formalization targets

Goal: Theorem 1 (corrected), p. 7

Assume Assumption 1, rich prompts, and pairwise distinct finite token complexities. Let $t_T$ be the largest finite $\tau_j$ with $E_n(\tau_j) \le T$ and $q_\alpha$ the smallest finite $\tau_j$ with $F_n(\tau_j) \ge \alpha$. Then for every $T \ge 0$ and every $0 < \alpha \le A^*$,

$$\alpha^*(T) = \frac1n \sum_{i=1}^n \mathbf 1\{\tau_i \le t_T\}, \qquad T^*(\alpha) = \frac1n \sum_{i=1}^n \tau_i\, \mathbf 1\{\tau_i \le q_\alpha\},$$

with both optima attained. As printed, the theorem defines $t_T \equiv \inf\{t \in \mathbb R : E_n(t) = t\}$, which does not depend on $T$, and $q_\alpha = \sup\{t : F_n(t) \le \alpha\}$, which overshoots the quantile; both readings give wrong values on one- and two-question examples. The goal uses the thresholds that the proof and the text describe ("the highest value of τ that the LLM puts into the knapsack", "the α-quantile of the empirical distribution").

Milestones (Appendix D, p. 14)

1. Eq. (8): under Assumption 1, $\mathrm{Acc}(P) = \frac1n\sum_i \mathbf 1\{\tau_i \le t_i(P)\}$ (the page prints the inequality reversed).
2. Eqs. (9)–(10): with rich prompts, $\alpha^*(T)$ and $T^*(\alpha)$ are the optima of the same problems over token-count vectors $t \in \mathbb N^n$.
3. Eqs. (11)–(12): these equal the optima of a 0-1 knapsack with unit rewards and costs $\tau_i$,

$$\max_{x \in \{0,1\}^n} \frac1n \sum_i x_i \quad \text{s.t.} \quad \frac1n \sum_i \tau_i x_i \le T.$$

4. The greedy claim: for $T \ge 0$ the knapsack optimum is $m/n$, where $m$ is the largest number with $\tau_{(1)} + \dots + \tau_{(m)} \le nT$ for the sorted finite token complexities $\tau_{(1)} \le \tau_{(2)} \le \cdots$.
5. The $T^*$ analogue: for $0 \le \alpha \le A^*$ the minimal cost is $\frac1n(\tau_{(1)} + \dots + \tau_{(\lceil n\alpha\rceil)})$.

Milestones 4 and 5 allow ties among the token complexities; the goal's closed form does not.

Significance

Theorem 1 turns an optimization over all conceivable prompting strategies, an infinite and unstructured set, into a formula in the empirical distribution of $n$ numbers. Its consequence, Corollary 1, is that $T^*(A^*)$, the average token complexity of the solvable questions, is a lower bound on the average length of any lossless compression of the chain of thought; the paper's Table 4 uses it to show that current concise prompts leave a 3–11× reduction unrealized. The same characterization explains why adaptive strategies, which spend more tokens on harder questions, are necessary to approach the frontier.

The result has a pen-and-paper proof of a few lines in Appendix D; the prior-art search found no machine-checked version. Formalizing it adds a correct statement: the printed definitions of $t_T$ and $q_\alpha$ are wrong, eq. (8) has a reversed inequality, and the closed form silently needs distinct token complexities. The mission records the correct versions with the counterexamples to the printed ones, and separates the tie-robust greedy form (milestones 4–5) from the CDF form (the goal).

Difficulty

The individual steps are elementary, but the obvious argument skips three points. First, passing from prompts to token vectors uses richness in both directions: an optimal prompt must be matched by a token vector and conversely, and the optima must be shown attained, not merely bounded. Second, the reduction to $t_i \in \{0, \tau_i\}$ must handle questions with $\tau_i = \infty$, which can never be selected. Third, the greedy claim is a statement about every feasible selection, not only the sorted ones, and translating the greedy count into the threshold forms $\mathbf 1\{\tau_i \le t_T\}$ and $\mathbf 1\{\tau_i \le q_\alpha\}$ is exactly where ties break the formula, so distinctness must be used at that step and nowhere else.

Formalization scope

• Model. One LLM, superscript $\pi$ dropped. Questions are Fin n; prompts are an arbitrary type; a Benchmark gives token lengths len : Prompt → Fin n → ℕ and correctness correct : Prompt → Fin n → Bool. Each (prompt, question) pair yields one deterministic chain of thought.
• Token complexities are ℕ∞-valued; $\tau_i = \infty$ is ⊤. Assumption 1 is correct P i = true ↔ τ i ≤ len P i ("above" read as $\ge$, as the displayed formula on p. 5 shows). Every count or sum over $\tau$ filters on $\tau_i \ne \infty$ before converting to a natural number.
• Averages are real numbers with division by $n$; the goal assumes $n \ge 1$.
• Optima are IsGreatest/IsLeast predicates over the set of values achieved by prompts, never sSup/sInf, so empty or unbounded feasible sets cannot produce a junk value.
• Added hypotheses, all disclosed: $n \ge 1$; $T \ge 0$; $0 < \alpha \le A^*$ for the $T^*$ part ($\alpha \ge 0$ in milestone 5); pairwise distinct finite token complexities in the goal only.
• Trivializing formalizations ruled out. The goal quantifies over prompts and links them to $\tau$ only through Assumption 1 and richness; neither $\alpha^*$ nor $T^*$ is defined as its closed form, and the goal is not stated over token vectors or knapsack variables. Richness is satisfiable: the canonical benchmark with prompts $\mathbb N^n$ satisfies both hypotheses for every $\tau$.
• Not formalized: Corollary 1 (a consequence the proof of Theorem 1 does not use), the threshold-classifier estimators of §3, and the empirical results.

The definitions (benchmark, empirical CDF over an ℕ∞-valued family, sorted prefix sums) are self-contained. A proof of the greedy milestones gives a reusable fact about unit-reward knapsacks. Proofs of any milestone and of the goal are welcome, as is a formalization of Corollary 1 on top of the goal.

Selected references

• A. Lee, E. Che, T. Peng, How Well do LLMs Compress Their Own Chain-of-Thought? A Token Complexity Approach, arXiv preprint, 2025. https://arxiv.org/abs/2503.01141 (version v2 is the one formalized).
• J. Wei et al., Chain-of-Thought Prompting Elicits Reasoning in Large Language Models, NeurIPS, 2022. https://arxiv.org/abs/2201.11903