Mission: Motives — effective pure motives and the tannakian obstruction

Motivation

Grothendieck introduced the notion of a motive in a letter to Serre in 1964. Among all the objects he was privileged to discover, he wrote, this one appeared to him the most charged with mystery, and the yoga of motives perhaps the most powerful instrument of discovery he had brought to light. The source — James Milne's expository article "Motives — Grothendieck's Dream" — explains what motives are and why Grothendieck valued them so highly. The many good cohomology theories of algebraic geometry — singular, étale, de Rham, crystalline — cannot come from an algebraically defined Q-valued theory, yet they behave as though they did: traces of regular maps are rational and independent of the theory. Grothendieck's answer is a universal cohomology theory with values in a Q-linear category of motives: every good cohomology theory should factor uniquely through it. The construction passes through algebraic cycles modulo an adequate equivalence relation and correspondences; the category so obtained is additive and pseudo-abelian, carries a tensor product satisfying the Künneth formula, and its first computed decomposition is the motive of the projective line, h(P¹) = 𝟙 ⊕ 𝕃, whose endomorphism ring is as small as possible; the trace of the identity on a motive is the Euler-Poincaré characteristic, and the first zeta computations — the point and the projective line — exhibit the mechanism that the Weil conjectures later vindicated in general. The same trace calculus, however, contains the obstruction that Grothendieck's dream runs against: the trace of the identity on the motive of a curve of genus g is 2 − 2g, which is negative for g ≥ 2, so no fiber functor can exist on the category of effective motives and the category cannot be tannakian.

The mission formalizes the definitions and the proved structural theorems of Sections 4-7 of the source: the algebra of correspondences, the category of effective pure motives with its composition, addition, tensor structure, and pseudo-abelian splitting, Grothendieck's decomposition of the motive of the projective line, the trace of the identity as the Euler characteristic, the zeta functions of a point and of the projective line, and — as the goal — the tannakian obstruction: the category of effective motives admits no fiber functor in the presence of a curve of genus at least 2.

The fragment and its conventions

The source is an expository article; the mission formalizes the fragment consisting of the correspondence algebra and the category of effective pure motives (Sections 4-6), the trace calculus (Section 6, page 10), and the first two zeta computations (Section 7), under the following disclosed conventions.

Fourteen conventions deserve disclosure. First, the platform publishes definitions as modules, so the three definition bundles — the correspondence world, the effective motives, and the zeta coefficients — are published as platform definitions (Milne_world, Milne_motives, Milne_zeta) and attached to the proposal as reference items; the theorem drafts import them; and the creation script reads the definition code and the theorem statements directly from the repository modules that the CI has just compiled, so the code posted to the platform is byte-identical to the code whose compilation the CI verified. Second, algebraic geometry is abstract: no varieties, algebraic cycles, Chow groups, or cohomology theories are constructed, since Mathlib has none of this; the primitive datum is a world of correspondences (CorrWorld) — varieties with a product, a designated point, a projective line, and a curve of every genus, and for each pair of varieties a Q-vector space of correspondences carrying a degree function into the integers, composition, diagonals, transposes, exterior products, Künneth idempotents, and trace data — with the moving lemmas and the well-definedness of the products of cycle classes living in the interface fields, so that every theorem carries the world as a hypothesis. Third, correspondences are presented ungraded, with the grading recovered through the degree function: the graded pieces Corr^r(X, Y) are the degree-r elements, and morphisms of motives are the degree-zero correspondences of the source's f ∘ Corr⁰(X, Y)Q ∘ e. Fourth, rational coefficients are baked into the interface: the correspondence spaces are Q-vector spaces, the source's tensoring of cycle groups with Q is not repeated. Fifth, the mission lives in the effective category: the paper's second attempt of Section 5; the twist integer m of h(X, e, m), duals, and the full category M~(k) are out of scope. Sixth, morphisms are rendered as fixed points: the sandwiched image f ∘ Corr(X, Y)_Q ∘ e is the subtype of correspondences γ with f ∘ γ ∘ e = γ and degree zero, which coincides with the image when e and f are idempotent. Seventh, the closure of the sandwiched subspaces under the operations (composition, addition, zero, negation, scalar multiplication, exterior product) is imposed through interface axioms, since these are the stability statements that make the morphism spaces well defined. Eighth, direct sums are stated through the five biproduct identities rather than as an equality with a direct-sum object; the pseudo-abelian splitting is stated through the same identities, with the complement and image summands h(X, e − f) and h(X, f) as the explicit witnesses. Ninth, the tensor structure is defined on objects and morphisms through the exterior product, and the Künneth formula is stated at the level of motives: hX ⊗ hY = h(X × Y). Tenth, the Künneth idempotents of the projective line and of the curves of every genus, the diagonal decompositions Δ = e₀ + e₂ and Δ = π₀ + π₁ + π₂, and the trace values 1, −2g, 1 of the pieces — the signed Betti numbers, so that the trace of the identity is the Euler characteristic — are interface data: the source's computations from the intersection ring of the projective plane and of a curve are thereby carried as hypotheses. Eleventh, the trace of the identity on an idempotent motive is defined through the interface-supplied evaluation and coevaluation correspondences, its additivity over idempotent splits is an interface axiom, and the duality zigzag equations of the source are not stated. Twelfth, the fiber functor is rendered as a concrete structure FibFun — a dimension for each motive, an action on morphisms, preservation of identities and composition, multiplication of dimensions over tensor products, and the identification of the trace of the identity with the dimension of the fiber; exactness and faithfulness are deliberately not hypothesized, because the tannakian obstruction needs only the trace-dimension identity, so the goal theorem is formally stronger than the source's formulation — the strengthening is disclosed — and the fibers are Q-vector spaces, whereas the source allows any field F of characteristic zero. Thirteenth, the zeta function is rendered through its Taylor coefficients via a course-of-values prefix recursion equivalent to the source's logarithmic definition log Z(X, t) = Σ N_m t^m / m; the point counts 1 and 1 + p^m of the point and of the projective line are carried as data, and no finite fields are formalized. Fourteenth, everything is developed against the platform's Mathlib build (0df444a); the read-backs attached to the theorem drafts were authored by the same model that produced the statements (readback_model glm-5-latest-short); they are a self-check, not an independent audit, and human review of every item is required before submission.

Formalization targets

Eleven items: three published definition bundles attached as references, seven milestone theorem drafts, and the goal theorem.

• The correspondence world (reference): varieties with a product, a point, a projective line, curves of every genus, and Q-vector spaces of correspondences with composition, diagonals, transposes, exterior products, degrees, Künneth idempotents, and trace data (Sections 4-6).
• Effective pure motives (reference): objects h(X, e), morphisms as sandwich-fixed degree-zero correspondences, identity, composition, addition, zero, tensor products, the summands of the projective line, the splitting summands, and the fiber functor structure (Sections 5-6).
• Zeta functions (reference): the Taylor coefficients of the zeta function attached to a point-count sequence, through the prefix recursion (Section 7).
• Effective motives form a category: associativity of composition and the identity laws (Section 5) — milestone.
• Effective motives are pseudo-abelian: an idempotent endomorphism splits the motive into biproduct summands (Section 6) — milestone.
• The tensor product and the Künneth formula: the interchange law, the tensor identity, and hX ⊗ hY = h(X × Y) (Section 6) — milestone.
• The motive of the projective line: h(ℙ¹) = 𝟙 ⊕ 𝕃, and the endomorphism ring is the rational span of the two Künneth idempotents (Sections 5-6) — milestone.
• The trace of the identity on the motive of a curve is its Euler characteristic 2 − 2g (Section 6, p. 10) — milestone.
• The zeta function of a point: all Taylor coefficients are 1 (Section 7) — milestone.
• The zeta function of the projective line: the Taylor coefficients are the partial geometric sums (Section 7) — milestone.
• The tannakian obstruction: no fiber functor exists on the effective motives of a world containing a curve of genus at least 2 (Section 6, p. 10) — the goal.

Significance

The formalized fragment is the additive and tensor skeleton that every theory of motives shares, together with the trace calculus and the first two zeta computations, and it ends with the obstruction that gives the mission its point: as long as the trace of the identity on the motive of a curve is its Euler characteristic, no fiber functor can exist, so the category of effective motives is not tannakian and cannot be the representation category of an affine group scheme — the reason the source gives for passing to larger categories of motives. Formalizing the skeleton with every geometric input isolated as an explicit interface hypothesis produces a reusable shape: the same statements admit any future Mathlib development of algebraic cycles as an instantiation.

Difficulty

The categorical skeleton is pure algebra: associativity, units, biproduct identities, the interchange law, and the splitting of idempotents follow from the interface axioms by equational reasoning; the trace computation is additivity over the Künneth decomposition together with the supplied trace values; the zeta computations are inductions on the coefficient recurrence; the goal is the contradiction between a negative trace and the nonnegativity of a dimension. The difficulty is the discipline of the interface — no statement may silently use a geometric fact that has not been assumed — and the bookkeeping of the course-of-values recursion against the geometric expansion of the reciprocal of (1 − t)(1 − p t).

Formalization scope

Every item quantifies only over the objects it needs — worlds, motives, morphisms, idempotents, genera, point-count sequences. The goal carries a genus parameter together with the hypothesis that the genus is at least two; every world contains a curve of every genus by the interface, so the hypothesis is satisfiable, and it states the source of the obstruction — the middle Künneth summand of a curve of genus at least two has negative trace. This binder is disclosed here rather than left unstated. The negation-free statements produce witnesses: biproducts, splittings, and decompositions produce their morphisms; the zeta identities are equalities of coefficients; the goal is a negation, as is proper for an obstruction. The fragment excludes the twist m ∈ ℤ, duals, rigidity, and tannakianity as a positive property (Sections 5-6), the abelian category M_num and its semisimplicity, Conjectures C and D and the standard conjectures (Section 6), the zeta function of a motive via characteristic polynomials of Frobenius and the Hasse-Weil bound (Sections 2, 7-8), motivic L-functions, the big modularity conjecture, and the conjecture of Birch and Swinnerton-Dyer (Sections 8-9), and mixed motives (Section 10) — everything the source conjectures rather than proves, and everything requiring cohomological realization, is out of scope. The mission formalizes what the source proves.

Selected references

• J. S. Milne, Motives — Grothendieck's Dream, v2.04, April 24, 2012 — the mission's source.
• A. Grothendieck, letter to J.-P. Serre, 1964 — the introduction of the notion of motif.
• S. L. Kleiman, Motives, in Algebraic Geometry, Oslo 1970 — the first detailed exposition of the standard conjectures.
• U. Jannsen, S. L. Kleiman, J.-P. Serre (eds.), Motives, Proceedings of Symposia in Pure Mathematics 55, American Mathematical Society, 1994 — the standard reference, including Scholl's detailed construction of the category of motives.

The quantitative sensitivity question

Sensitivity and block sensitivity measure how a Boolean function responds to changes in its input. They are central examples of query complexity measures: an algorithm learns an unknown input by querying its individual coordinates, while these measures describe how many changes the function can detect at a single input. Understanding their relationship helps distinguish the complexity caused by individual coordinate changes from the complexity caused by changes to groups of coordinates.

The Block Sensitivity vs. Sensitivity campaign tracks the largest certified separation exponent. Its classical benchmark is a quadratic separation. OpenAI problem 132 supplied a superquadratic construction and a Lean formalization in 2026. Subsequent campaign entries reached 2.0391, 2.05, and 2.0635. This entry establishes the exact exponent $2.075=83/40$ using the same definitions and quantifiers.

Boolean functions and sensitive changes

A total Boolean function assigns an output bit to every input of $n$ bits:

$$f:\{0,1\}^n\longrightarrow\{0,1\}.$$

For an input $x$ and a coordinate set $D$, let $x^D$ denote the input obtained by flipping precisely the coordinates in $D$. The sensitivity at an input counts the individual coordinates whose flips change the output:

$$s(f,x)=\bigl|\{i:f(x^{\{i\}})\ne f(x)\}\bigr|.$$

The block sensitivity at an input, denoted $bs(f,x)$, is the largest number of pairwise disjoint nonempty coordinate sets $D_1,\ldots,D_k$ such that flipping any one of them changes the output at $x$. The sets are tested separately, always starting from the same input. The corresponding global measures are

$$s(f)=\max_x s(f,x),\qquad bs(f)=\max_x bs(f,x).$$

The maxima range over all inputs, including inputs on which the output is zero and inputs on which it is one. No monotonicity, symmetry, or restriction on the number of variables is imposed.

Target: exponent at least 2.075

For every real $\varepsilon>0$ and every integer $S\ge2$, establish the existence of a dimension $n$ and a total Boolean function $f$ with

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{83/40-\varepsilon}.$$

The campaign predicate SensitivityCampaign.AchievesExponent (2.075 : ℝ) states this exact proposition. The decimal is interpreted exactly, as $83/40$, rather than as an approximate floating-point value. The function and dimension may depend on both the exponent loss $\varepsilon$ and the requested threshold $S$.

The threshold quantifier is essential: the target concerns arbitrarily large sensitivity. A small isolated function, or a collection of functions whose sensitivity stays bounded, does not by itself establish the campaign statement. The use of an arbitrary positive exponent loss agrees with the campaign's other entries and allows their values to be compared directly.

What this entry establishes

This result increases the certified exponent beyond the campaign's 2.0635 entry. It provides an intermediate achieved bound toward the separate 2.10 research target. It does not assert that 2.10 has been reached or identify the optimal exponent.

The complete Lean proof has compiled successfully, passed local kernel replay, and been accepted by Prove2Me. The verified theorem and full proof establish the stated target. Its supporting development includes nine-predicate sensitivity estimates, bounds on joint changes of nested predicates, finite labeling existence, disjoint sensitive-block witnesses, and an exact integer certificate. The accompanying proof explanation describes how these ingredients establish the stated target. The finite-certificate and logarithmic-score theorems from the campaign foundation remain referenced as reusable milestones.

The difficulty in improving the bound

A construction must have many disjoint sensitive blocks at one input while keeping sensitivity small at every input. A large block family supplies only the lower-bound half of this requirement. An input that makes many individual coordinates sensitive can invalidate the global upper bound even if the intended block-witness input behaves well.

Joint boundary behavior is another constraint: analyzing several related predicates independently can lose information about which changes can occur together. The formal proof therefore needs correct sensitivity estimates for the actual input-coordinate flips throughout the construction. Numerical growth estimates must also account for every fixed overhead before they can certify a finite exponent inequality.

Formalization scope and reusable foundations

The function type is (Fin n → Bool) → Bool. Sensitivity and block sensitivity use the existing OAI.Paper320 definitions, imported through Definitions.Def_SensitivityCampaign. Both measures are natural numbers defined using maxima over finite collections. The exponent comparison casts them to real numbers and uses real exponentiation. Since every requested witness has sensitivity at least two, the base of that power is positive.

The mission retains the shared campaign definitions without modifications. The two foundation milestones are SensitivityCampaign.finite_certificate, which turns suitable finite sensitivity and block-sensitivity bounds into the asymptotic target, and SensitivityCampaign.finite_certificate_log, which expresses the same interface using a logarithmic score. Their normalization and unbounded-sensitivity conclusions are part of their proved statements.

The supplied proof targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The supporting assertions are proved in the submitted source; no conjectural lemma or numerical approximation is used as an assumption. The general transfer estimates and exact certificate provide material for subsequent improvements, while this mission's goal remains the fixed campaign value 2.075.

Selected references and credits

• OpenAI, A superquadratic separation between sensitivity and block sensitivity, problem 132, 2026. Formalization and source links.
• Prove2Me contributors, Separation exponent at least 2.0391, 2026. Accepted theorem and proof.
• Robin Kothari, Separation exponent at least 2.05, 2026. Accepted theorem and proof.
• abhishekdpseok, Separation exponent at least 2.0635, 2026. Accepted theorem and proof, submission f80a3f37-72fa-4d56-a094-3e4d351764f3. The present development reuses its foundation, including its earlier source credits.
• Robin Kothari and Codex, Seven-level nine-state sensitivity certificate: exponent 2.075, 19 October 2026. Full Lean proof and mathematical explanation supplied with this entry.

Motivation

An innovation contest gives several agents a fixed period to submit solutions and awards prizes according to their final ranks. A platform choosing that period faces two practical effects: more time lets agents improve their submissions, while it delays the value of the best solution and can make the effort needed to participate more costly overall. The question is how the chosen duration changes when the quality of submissions becomes more uncertain or when agents become more productive over time. Korpeoglu, Körpeoğlu, and Tunç study this decision in a contest model motivated by crowdsourcing platforms and distinguish organizers by how strongly they discount a late solution. Their patient organizer result is the target here. Korpeoglu, Körpeoğlu, and Tunç, 2020.

Setting

There are $N\ge2$ agents and a fixed present-value award scheme. Agent $i$ chooses a nonnegative per-time effort path $\eta_i(t)$ during a contest of duration $T>0$. The path improves deterministic output at rate $\theta(t)\eta_i(t)$, where productivity $\theta(t)$ is positive. The final output adds an independent random shock $\tilde\xi_i$ with a common mean-zero, log-concave density $h$. The organizer values the best final output. The model uses the scale transformation $\alpha\tilde\xi_i$ to vary uncertainty without choosing a special distribution; its density is $h_\alpha(s)=h(s/\alpha)/\alpha$ for $\alpha>0$. When studying changing productivity, the paper sets $\theta(t)=\exp(\rho t)$, so $\rho$ is the productivity exponent. Model, pp. 8–9.

Effort costs $c\eta_i(t)^b$ per unit time, with $c>0$ and $b>1$. Write $e_i=\int_0^T\theta(t)\eta_i(t)\,dt$ for total deterministic output improvement. The least cost of producing $e_i$ is $\psi(e_i,T)=c e_i^b\tau(T)^{1-b}$, where $\tau(T)=\int_0^T\theta(t)^{b/(b-1)}\,dt$. A participant also bears a fixed cost $F>0$. An agent with the $j$th-largest output receives a present-value award $A(j)=A\gamma(j)$, with $A>0$, nonnegative, nonincreasing shares $\gamma(j)$, and $\sum_{j=1}^N\gamma(j)=1$. The contest's symmetric equilibrium effort is represented by $e^*(T)=(Ax/(cb))^{1/(b-1)}\tau(T)$, where $x=\sum_{j=1}^N I_j^N\gamma(j)$ and $I_j^N$ measures the effect of a small effort increase on the probability of rank $j$. Lemma 1 and equations (3)–(5), pp. 10–12.

For this mission the award scheme is held fixed, as it is in the paper's duration analysis. The organizer chooses among positive durations satisfying the agents' best-response and participation conditions. At duration $T$, the organizer's profit is $\Pi(T)=e^{-\delta T}(e^*(T)+E[\tilde\xi^N_{(1)}])-A$, where $\delta\ge0$ is the organizer's discount factor and $\tilde\xi^N_{(1)}$ is the largest shock. An optimal duration maximizes this profit among feasible durations. The patient regime is $\delta<\delta_1$, with $\delta_1$ evaluated from the model at the solution $\bar T$ of the participation equation (9). The paper's footnote 11 requires the agent's best-response condition to hold at $\bar T$ for that duration to be available. Equations (6)–(9) and footnote 11, pp. 12–13; threshold, p. 27.

Formalization targets

The goal is Theorem 1's pair of comparative statics. For each parameter value satisfying the patient regime and the stated regularity assumptions, let $T^*$ be the unique optimal feasible duration. Holding the productivity function and award scheme fixed, the uncertainty-scale target is

$$0<\alpha_1<\alpha_2\quad\Longrightarrow\quad T^*(\alpha_1)<T^*(\alpha_2).$$

With uncertainty normalized to its unscaled distribution and productivity $\theta(t)=e^{\rho t}$, the productivity target is

$$\rho_1<\rho_2\quad\Longrightarrow\quad T^*(\rho_2)<T^*(\rho_1).$$

The regime is checked at both values in each comparison, since $\delta_1$ itself changes with the density or productivity. The milestone statements cover optimal effort allocation, the equilibrium effort formula, the patient case of Lemma 2, the scale identities for the expected maximum and rank incentives, and the duration expression under exponential productivity. Theorem 1, p. 14; proof, p. 27.

Significance

The result links the contest's deadline to two distinct features of the agents' work. Greater output uncertainty changes the return to effort, while a larger productivity exponent changes when effort is most effective. For a patient organizer, the paper concludes that the first change lengthens the selected contest and the second shortens it. The statements concern an actual maximizer of profit under participation, so they can inform a duration decision for a specified award scheme, rather than merely compare algebraic expressions. Discussion of Theorem 1, pp. 14–15.

The paper proves these results mathematically. This mission supplies compiled Lean declarations for the model and its main claims; their theorem proofs remain open. A completed development would give machine-checked versions of the fixed-award, patient-organizer conclusions and reusable definitions for real shock densities, scaling, order statistics, effort allocation, and constrained duration optimization. It would also make the assumptions behind the paper's comparative statics visible in one interface.

Difficulty

The organizer cannot choose duration by looking only at the direct effect of more time on output. Longer contests alter equilibrium effort and agent costs, which changes participation, while discounting changes the value of the best output. The organizer therefore maximizes profit over a feasible set whose boundary depends on the same effort response. Identifying the patient regime requires the threshold $\delta_1$ from the proof of Lemma 2. Under shock scaling, the expected maximum and the rank-incentive coefficient transform differently; both must be accounted for in the same optimization problem. For negative $\rho$, the integral $\tau(T)$ can have a finite upper bound, so the participation equation need not have a positive solution. Lemma 2, p. 13; proof of Theorem 1, p. 27.

Formalization scope

The Lean representation uses real-valued densities and integrals, natural-number ranks $1,\ldots,N$, real powers on positive bases, and a positive-duration feasible domain. The standing model has $N\ge2$, $b>1$, $c>0$, $F>0$, $0<A$, $F<A/N$, $\delta\ge0$, ordered nonnegative award shares summing to one, a continuous positive productivity function, and a mean-zero log-concave shock density. Published CrowdContest.Pooling.Density supplies the general density, CDF, and expected-maximum operations; its symmetric-shock condition is not used. Published ConvexOptimization.LogConcaveOn supplies log-concavity. The paper's stated assumptions that profit is unimodal and has a positive derivative at zero are explicit; unimodality is read as strict increase throughout or strict increase followed by strict decrease. The added condition $x>0$ excludes equal awards, for which the paper's cited auxiliary lemma supplies only $x\ge0$. A positive solution $\bar T$ to equation (9) is required; this avoids assigning meaning to a missing inverse or a nonpositive logarithm argument. The agent's best-response condition at $\bar T$ is required, matching footnote 11 on p. 13.

An optimal duration is defined by maximization of the paper's profit (6) under the best-response condition (7) and participation (8). It is not defined to equal $\bar T$ or the logarithmic expression: that characterization is theorem content. The effort inserted into profit is equation (5), as in the paper's reduction; a rank-probability integral states what it means for that effort to solve (7). The open development needs results about interval integrals, real powers, log-concave density moments, the change of variables under scaling, best responses, and maximization under the participation constraint. The impatient case of Lemma 2 and later award-design results are outside this mission.

Selected references

• C. G. Korpeoglu, E. Körpeoğlu, and S. Tunç, Optimal Duration of Innovation Contests, authors' SSRN version, forthcoming at Manufacturing & Service Operations Management, 2020. SSRN 3064763.

Motivation

People receive both informative reports and messages that are unrelated to the truth. A standard question in social learning is whether sharing beliefs helps a population identify the correct state. The question changes when everyone knows misinformation exists but does not know its ideological direction. Mostagir and Siderius study this setting and show that the ranking of two learning rules changes with the amount of misinformation: Bayesian updating can be at least as reliable at low levels, while simple averaging is more reliable at sufficiently high levels under full support. Their result is stated as Theorem 1 of the SSRN working paper, later published in Management Science.

The comparison matters for models of collective decisions because the same population, news quality, and misinformation distribution can lead to different rates of wrong terminal actions solely because the agents process others' beliefs differently. The paper's question is therefore about the behavior of learning rules, not just the accuracy of any one message. The mission covers the paper's regime comparison; its separate results on hazard rates, polarization, and targeting are outside this target.

Setting

The unknown state $\theta$ is either $L$ or $R$. An organic message matches the state with probability $p>1/2$. A fraction $q<1/2$ of all messages consists of misinformation. Its split $r\in[0,1]$ is the fraction of misinformation advocating $R$; $r$ has distribution $F$ with density $f$. Agents start with heterogeneous prior probabilities $x\in[0,1]$ of state $R$, distributed according to a continuous law $H$. The paper assumes these priors and the split are independent. All comparisons concern the limit of a large population, where the observed fraction of each message type is determined by $\theta$ and $r$ (§2, pp. 4–6).

A DeGroot agent first updates on her own message while treating it as organic, using equations (1) and (2) of the paper. Thereafter agents average one another's beliefs. In the large-population model used by the proof, every agent reaches the same consensus $\pi_\infty(\theta,r)$: the $H$-average of the two face-value posteriors, weighted by the fractions of $R$ and $L$ messages. A Bayesian agent treats misinformation as possible and infers the message shares from the population's beliefs. The same observed share can be explained by the true state and split or by the other state with a different split. The posterior $\pi_B(\theta,r,x)$ weighs these two narratives according to their densities under $F$ and the agent's prior $x$ (proofs of Lemmas 1–2, pp. 18–19).

An agent's terminal action favors whichever state has posterior belief at least one half. A society mislearns at $(\theta,r)$ when a positive $H$-mass of agents favors the wrong state; for DeGroot agents, who share a consensus, this is a single belief comparison. Write $P_B(\theta)$ and $P_D(\theta)$ for the $F$-probabilities of Bayesian and DeGroot mislearning. The paper studies both true states; the formulas for $R$ mirror those for $L$.

Formalization targets

The main target is Theorem 1, p. 10. For every $1/2<p\leq1$, set

$$q^*=\frac{2p-1}{2p}.$$

For every continuous symmetric prior law $H$ on $[0,1]$ and every split law $F$ supplied by a density, the goal compares both states separately:

$$\begin{aligned} 0<q<q^*&\quad\Longrightarrow\quad P_B(\theta)\leq P_D(\theta),\\ q^*<q<\tfrac12,\quad H,F\text{ fully supported on }[0,1] &\quad\Longrightarrow\quad P_D(\theta)<P_B(\theta), \end{aligned} \qquad\theta\in\{L,R\}.$$

The first comparison is non-strict because both mislearning probabilities can be zero, although the preprint uses the word “lower.” The value of $q^*$ comes from the paper's proof, which states the result with an existential threshold. The five milestones state the DeGroot and Bayesian mislearning cutoffs, the necessary misinformation level for Bayesian mislearning, the cutoff difference, and the resulting full-support probability formulas. Their source text and page numbers accompany the individual items.

Significance

The theorem isolates a regime in which adding misinformation changes the relative performance of the two learning rules. Under full support, the high-misinformation conclusion is strict: some split realizations cause Bayesian society to mislearn even while DeGroot society learns. The low-misinformation conclusion gives a uniform comparison over every allowed distribution of the split, without requiring its full support (Theorem 1 and proof, pp. 10, 20). These are statements about society-level mistakes, not a claim that an individual averaging rule is always more accurate.

The result has a published mathematical proof. It does not yet have a machine-checked proof in this development. Formalizing it requires a reusable interface for two-state misinformation models: a law of heterogeneous priors, a density for the split, the two narrative splits, posterior beliefs, and mislearning events. Those objects can also support the paper's later questions about the distributional shape of misinformation and the choice of targeting policy.

Difficulty

The obvious comparison of the two update rules at a fixed message fails to settle the result. DeGroot agents act on an average of face-value posteriors; Bayesian agents act on an agent-specific posterior after considering competing explanations of the same population message share. Thus the two groups can be wrong for different split realizations, and a statement about one representative belief does not give a society-level mislearning probability. The comparison must also distinguish a pointwise mistake at the edge of the split support from an event of positive probability. A second issue is that the converse direction of the printed Lemma 2 assumes agents with beliefs arbitrarily close to the extremes, which requires full prior support on $[0,1]$ (Lemma 2 and proof, p. 19).

Formalization scope

Lean uses the paper's large-population formulas directly: $\pi_\infty$ is an integral over $H$, and $\pi_B$ is a density-weighted posterior over the two narrative splits. The Bayesian terminal belief is its period-two posterior; later observations add no information in this model. $H$ is a probability measure concentrated on $[0,1]$ with no atoms. $F$ is given by a measurable nonnegative real density whose integral is one and whose support lies in $[0,1]$. Full support on an interval means that the density is bounded below there by a positive constant and is zero outside. Symmetry means invariance of $H$ under $x\mapsto1-x$.

The formalized regime has $0<q<1/2$ so the cutoffs involving division by $q$ are defined as intended; the paper's misinformation-free case $q=0$ is an example outside this theorem. A belief of exactly $1/2$ counts as wrong, matching the weak cutoff inequalities. Mislearning for Bayesian society requires a positive $H$-mass of wrong agents, and the final probabilities are extended nonnegative real measures of split events. The real posterior's zero-denominator default can arise outside the split support, which carries zero $F$-mass; pointwise Bayesian milestones restrict $r$ to the support.

The model defines mislearning from posterior beliefs and the law of $r$, so the main theorem cannot be reduced to a comparison of cutoff formulas by definition. Solver contributions may establish measurability and integrability facts for the model, the cutoff lemmas, and the final comparison. The standing interval-support assumptions in the paper are narrowed to $[0,1]$ where the theorem needs them; the main comparison does not fix arbitrary smaller support intervals.

Selected references

• Mostagir, Mohamed, and James Siderius. Learning in a Post-Truth World. SSRN working paper 3879174, version of 2 July 2021; published in Management Science 68, 2022. SSRN preprint. The mission cites the preprint's page and theorem numbering.

Motivation

An online platform can know more about a product than a customer arriving for a short sales campaign. It sees earlier customers' purchase decisions and the messages it sent them, while a new customer sees only her own message and private assessment. Choosing what to disclose can raise immediate sales, but a customer's response can also reveal information that improves later messages. Küçükgül, Özer and Wang study this tension for a fixed-price campaign and reduce the platform's dynamic information-design problem to a linear program in their submission manuscript, §§3–4, pp. 7–18.

The mission concerns that reduction, stated as Proposition 5 and equations (9)–(11) of the November 2019 submission manuscript. Its original problem permits a message distribution that depends on the full private history. Its optimization variables after reformulation instead track an integer summary and three possible recommendations. The gap between those two descriptions is the main mathematical content that a formal proof must justify.

Setting

A time-locked sales campaign has $T$ customers arriving one after another at a fixed price $p\in(0,1)$. The product value $V$ is either $0$ or $1$, with common prior $\Pr(V=1)=v_0\in[0,1]$. Customer $t$ observes a private signal $S_t\in\{1,-1\}$; conditional on $V$, signals are independent, and $\Pr(S_t=1\mid V=1)=\Pr(S_t=-1\mid V=0)=q$ for $q\in(1/2,1]$. She receives one message $m_t$ from the platform, then buys when her posterior value reaches $p$, with equality resolved in favor of buying. These are the primitives of §3 and equations (1)–(2) of the manuscript.

An information provision policy $\sigma$ selects a distribution over messages using the platform's history $H_t=((m_s,a_s):s<t)$ of earlier messages and purchase decisions. The customer does not see that history. The platform's expected revenue is $R(\sigma)=p\sum_{t=1}^T\Pr_\sigma(a_t=1)$. The target value $\pi^\star$ is the best revenue over all such policies in equation (3), not a value assigned by the reduced program.

Two belief thresholds determine how a message affects buying: $v^*=p(1-q)/(p(1-q)+(1-p)q)$ and $v^{**}=pq/(pq+(1-p)(1-q))$. A recommendation policy uses messages $1$, $0$, and $-1$ to recommend buying, following the private signal, and declining. The net purchase position $N(H_t)$ counts purchases minus non-purchases among customers given the neutral recommendation. Section 4 defines $v_n=\Pr(V=1\mid N(H_t)=n)$ and $u_n=\Pr(S_t=1\mid N(H_t)=n)$. This turns the history distribution into masses $z_t(n)$ and the message probabilities into $r_t^i(n)$, where $i\in\{1,0,-1\}$. The linear-program variables are their products $y_t^i(n)=z_t(n)r_t^i(n)$; see Propositions 1–5, pp. 11–18.

Formalization targets

Original policy value and the reduced programs

For parameters in the paper's focus region $v^*\le v_0<v^{**}$, the goal states a common value for the original policy problem, recommendation formulation (9), and LP (11):

$$\sup_\sigma R(\sigma) =\max_{(r,z)\text{ feasible for (9)}}p\sum_{t=1}^T\sum_n z_t(n)\bigl(r_t^1(n)+u_nr_t^0(n)\bigr) =\max_{y\text{ feasible for (11)}}p\sum_{t=1}^T\sum_n\bigl(y_t^1(n)+u_ny_t^0(n)\bigr).$$

The goal also says that every LP optimum recovers an optimum of (9) through equation (10), taking any probability vector of recommendations where $z_t(n)=0$. The first two maxima include attainment. The original-policy value is expressed as a supremum because the manuscript's weak incentive inequalities permit endpoint ties that may change the customer's actual response under (2); this reading is disclosed in the paper's Proposition 5 and proof, pp. 18, 42–43.

The milestones trace the source's claims: Proposition 1 classifies buying behavior; Proposition 2 restricts attention to recommendations; Proposition 3 identifies the net purchase position as a sufficient statistic; equation (9) states the original-to-reduced value identity; and equations (B.17)–(B.18) express the two directions between (9) and (11). Proposition 4's random-walk identity remains in the definition of feasibility for (9) and (11), though it is not a separate milestone in this proposal.

Significance

Proposition 5 replaces a search over history-dependent information policies with a finite linear program whose variables have the interpretation of joint state-and-recommendation probabilities. For a fixed campaign length, the LP has $3T(2T-1)$ variables before redundant positions are removed. This gives the computational representation used in the paper's later numerical comparison and recommendation-policy examples; see §4.3, pp. 18–20.

The result is proved in the authors' manuscript. The local Lean files for this mission compile as statements with proof placeholders; they do not yet contain machine-checked proofs. Completing the mission would provide a checked bridge from a sequential Bayesian policy model to its reduced finite-state program and LP, with reusable definitions for the joint law, Bayesian response, and state evolution.

Difficulty

The change of variables $y_t^i(n)=z_t(n)r_t^i(n)$ is only the final step. The difficult claim is that optimizing over full proprietary histories and arbitrary messages gives the value of a program whose policy uses only three recommendations and the integer $N(H_t)$. A receiver's choice is endogenous: the message affects what she believes, her private signal affects whether she buys, and the platform observes the resulting decision. Defining customer behavior as automatic obedience would erase that difficulty. The paper's endpoint inequalities add another issue: at equality a nominal recommendation can differ from the purchase rule, so value comparison must keep the tie convention visible. These are the distinctions between equations (2), (3), (9), and (11) of the manuscript.

Formalization scope

The Lean model uses real probabilities, a Boolean product value, Boolean signals and purchase decisions, and SignType for the three recommendations. It builds the joint distribution of $V$ and the proprietary history one customer at a time. Every customer buys by the joint-probability form of rule (2), including a tie; obedience is a property checked on realized signal–message pairs. Histories of length $t$ precede paper customer $t+1$, while (9) and (11) keep the source's one-based time index. The state range is $n=-(T-1),\ldots,T-1$, with zero mass outside and zero boundary terms in the recursions.

The policy class has an arbitrary finite message type. This matches the sums over histories in Appendix B and includes the three-message policies. The assumptions retain $q=1$, $v_0=0$, and $T=0$ when allowed by the stated region; the definition of $v_n$ uses a two-sided product expression so a negative exponent never acts on zero. The reduced programs use exactly the four printed weak incentive inequalities. State masses are nonnegative, as required by their meaning as probabilities. Real-number maxima are stated with IsGreatest, and the original-policy supremum with IsLUB; no default value of a real sSup is used.

The original-policy value is taken over all information policies with Bayesian response, rather than being defined by (9). The source's correction at $v^*$, the interpretation of recommendation obedience, the finite-message restriction, and the supremum reading are explicit audit points. A full development needs finite probability calculations, conditional belief identities, and equivalence between histories and net positions. The model and these supporting lemmas can be reused for later formal work on sequential persuasion in the same paper.

Selected references

• C. Küçükgül, Ö. Özer, and S. Wang, Engineering Social Learning: Information Design of Time-Locked Sales Campaigns for Online Platforms, submission manuscript, November 2019; published in Management Science, 2022. DOI: 10.1287/mnsc.2021.4151.

Motivation

An online retailer may buy products from suppliers and resell them, or let suppliers sell directly while collecting a commission. The choice changes who sets retail prices and how a wholesale price change for one product affects the prices of competing products. In the first arrangement, the retailer sets all retail prices; in the second, suppliers set their own prices after the retailer chooses a commission. Hu, Zheng, and Pan study how this cross-brand retail pass-through changes the comparison between those arrangements. Their Proposition 2 identifies a sharp split: nonnegative cross-brand pass-through favors agency selling for the retailer, while negative pass-through can reverse the retail-price ordering. The question matters when a retailer must choose a contract for several competing products rather than evaluate a single supplier in isolation. Hu, Zheng, and Pan, SSRN preprint, §§3–5.

Setting

There are $n\geq2$ symmetric suppliers, each with marginal cost $c_s\geq0$. At a common retail price $p$ in an open positive interval $D$, the demand for one product is $q(p)>0$ and falls with price. Its demand sensitivity is

$$\lambda(p)=-\frac{q(p)}{q'(p)}.$$

The paper assumes that $\lambda'(p)<1$, that $\lambda(p)[2-\lambda'(p)]$ has slope less than one, and that $p\lambda'(p)\leq\lambda(p)$. These are the symmetric-price forms of its demand conditions A1, A3, and A4. The model also uses an aggregate diversion ratio $\epsilon$: the fraction of the own-product demand response diverted to other suppliers. Under A1, $0\leq\epsilon<1$. Hu, Zheng, and Pan, §§3.1–3.2, pp. 7–9.

Let $a=\partial p_i/\partial w_i$ be own-brand pass-through and $b=\partial p_j/\partial w_i$ for $j\ne i$ be cross-brand pass-through. The total response is $a+(n-1)b=1/[1-\lambda'(p^W)]$. The suppliers' conduct parameters under wholesale and agency selling are respectively

$$\theta^W=\frac{(1-\epsilon)[a+(n-1)b]}{a-\epsilon b},\qquad \theta^B=1-\epsilon.$$

The wholesale retail price $p^W$ and agency retail price $p^B$ are any solutions, in $D$, of the two equations of Lemma 1 after the retailer's marginal cost $c_r$ is normalized to zero. The corresponding wholesale price is $w^W=p^W-\lambda(p^W)$, and the agency commission rate is $\alpha^B=c_s/[p^B-\theta^B\lambda(p^B)]$. The profits $\pi_r^W,\pi_i^W,\pi_r^B,\pi_i^B$ come from the respective wholesale and agency contract objectives. Finally, §5 defines

$$K^B=\frac{\alpha^B}{1-\lambda'(p^B)}\left[1+\frac{\lambda(p^B)-p^B\lambda'(p^B)}{p^B-\theta^B\lambda(p^B)}\right].$$

These are the quantities in Proposition 2. Hu, Zheng, and Pan, Lemma 1, p. 11; §5, p. 13.

Formalization targets

Nonnegative cross-brand pass-through

For every pair of equilibrium prices $p^W,p^B$ satisfying Lemma 1's equations, Proposition 2(i) asserts that $b\geq0$ implies

$$p^B\leq p^W,\qquad \pi_r^B\geq\pi_r^W,\qquad \pi_i^B\leq\pi_i^W.$$

The milestone list includes Proposition 1's comparison of $\theta^W$ and $\theta^B$, the price ordering, and the auxiliary profit comparisons in the authors' proof. Hu, Zheng, and Pan, Propositions 1–2, pp. 12–13; Appendix B, pp. 26–27.

Negative cross-brand pass-through

When $b<0$, the price part of Proposition 2(ii) gives the exact criterion

$$p^W<p^B\quad\Longleftrightarrow\quad\theta^W<\theta^B\min\{K^B,1\}.$$

The milestone for this case is the authors' rewrite of condition (8) in terms of $K^B$. The paper also says that wholesale selling can be more profitable for the retailer and agency selling may benefit suppliers; those are existence observations illustrated by its examples and are outside this mission's goal. Hu, Zheng, and Pan, Proposition 2(ii), p. 13; Appendix B, p. 27.

Significance

Proposition 2 separates two forces in the contract choice. Agency selling avoids the retailer's wholesale markup, while the sign of cross-brand pass-through changes the relative intensity of supplier competition. Under nonnegative pass-through, the paper obtains simultaneous comparisons of prices and both parties' profits. Under negative pass-through, the threshold $K^B$ gives a precise condition for a reversal in retail prices. These conclusions let the two contracts be compared using measurable pass-through responses and the demand curve, instead of treating the number of competing suppliers alone as decisive. Hu, Zheng, and Pan, §§4–5, pp. 12–13.

The result is proved in the source paper. This mission supplies compiled Lean statements and a common definition layer, but no machine-checked proofs of the theorem or its milestones yet. Completing it would verify the equilibrium comparisons under explicit demand and denominator conditions. The auxiliary monotonicity and profit identities can also be reused when studying the paper's later results on supplier preferences and welfare.

Difficulty

The immediate comparison of the two equilibrium price equations does not determine which price is larger: the conduct parameter differs between contracts, and the agency equation contains a cost term with a squared denominator. The paper's assumptions control the slopes of two demand-sensitivity expressions, while the profit comparisons require different auxiliary curves for suppliers and the retailer. In the negative pass-through case, the condition involving $K^B$ must still be combined with the conduct-parameter ordering. These are substantive inequalities; simply unfolding the profit definitions does not give Proposition 2. Hu, Zheng, and Pan, Appendix B, pp. 26–27.

Formalization scope

Lean uses real-valued demand on an open, order-connected interval $D\subset(0,\infty)$ and a natural-number supplier count $n\geq2$, cast to the reals in formulas. Derivatives are ordinary derivatives on $D$. The smoothness assumption is $C^3$ there because A3 differentiates an expression containing $\lambda'$. Positive demand is explicit; A1 requires $q'<0$. The strict bound $\epsilon<1$ follows from the strict total-demand decrease in A1, although the paper prints the weaker interval $[0,1]$. The expressions divide only where their denominators are positive: $a-\epsilon b>0$, $p^B-\theta^B\lambda(p^B)>0$, and $1-\lambda'(p^B)>0$ by A3. The paper uses $\theta^W\in[0,1]$ in its proof, so that bound is also explicit. The retailer's marginal cost is fixed to $c_r=0$ as on p. 12. Hu, Zheng, and Pan, A1–A4, pp. 7–8; Lemma 1, p. 11; Proposition 2 proof, p. 26.

The n-product demand system and Stackelberg games are represented by their conduct-parameter symmetric equilibrium equations from Lemma 1. Every theorem concerns every pair of prices satisfying those equations in $D$; no existence or uniqueness of such a pair is presumed. The original game and A5's invariant-conduct assumption are not reconstructed. Profits remain the original contract objectives at symmetric prices, rather than being defined by the reduced forms that the proof seeks to establish. The definition layer, demand calculus, and milestone inequalities are all open to proof contributions; the contract-profit identities must be derived from their objective definitions.

Selected references

• Hu, H., Zheng, Q., and Pan, X. A., Agency or Wholesale? The Role of Retail Pass-Through, SSRN preprint 3724934, 2021 revision; published in Management Science, 2022. SSRN; DOI.

Motivation

Quantum error correction (QEC) is an essential element of physical quantum information processing systems. Most QEC efforts focus on extending classical error correction schemes to the quantum regime. The input to a noisy system is embedded in a coded subspace, and error recovery is performed via an operation designed to perfectly correct for a set of errors, presumably a large subset of the physical noise process. In this paper, we examine the choice of recovery operation. Rather than seeking perfect correction on a subset of errors, we seek a recovery operation to maximize the entanglement fidelity for a given input state and noise model. In this way, the recovery operation is optimum for the given encoding and noise process. This optimization is shown to be calculable via a semidefinite program (SDP), a well-established form of convex optimization with efficient algorithms for its solution. The error recovery operation may also be interpreted as a combining operation following a quantum spreading channel, thus providing a quantum analogy to the classical diversity combining operation.

This mission is the statement-level formalization of Optimum Quantum Error Recovery using Semidefinite Programming (arXiv:quant-ph/0606035v1). 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 Optimum recovery is an attained semidefinite program (Abstract; IV, Eq. (22): optimum entanglement-fidelity recovery is an attained SDP, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• VI A and Fig. 2: numerical five-qubit amplitude-damping recovery comparison: Certified semantics for the approximate small-damping numerical fit and recovery comparison (source-ambiguity)
• VI B and Fig. 3: numerical four-qubit amplitude-damping recovery comparison: Certified semantics for the approximate small-damping numerical fit and recovery comparison (source-ambiguity)

Selected references

• Optimum Quantum Error Recovery using Semidefinite Programming, arXiv:quant-ph/0606035v1, https://arxiv.org/abs/quant-ph/0606035v1

Motivation

Many quantum information tasks use inputs of the form $\rho^{\otimes m}$, which naturally induce permutation and unitary symmetries. We classify all quantum channels that respect both symmetries - i.e. unitary-equivariant and permutation-invariant quantum channels from $(\mathbb{C}^{d})^{\otimes m}$ to $(\mathbb{C}^{d})^{\otimes n}$ - via their extremal points. Operationally, each extremal quantum channel factors as unitary Schur sampling $\rightarrow$ an irrep-level unitary-equivariant quantum channel $\rightarrow$ the adjoint unitary Schur sampling. We give a streaming implementation ansatz that uses an efficient streaming implementation of unitary Schur sampling together with a resource-state primitive, and we apply it to state symmetrization, symmetric cloning, and purity amplification. In these applications we obtain polynomial-time algorithms with exponential memory improvements in $m,n$. Further, for symmetric cloning we present, to our knowledge, the first efficient (polynomial-time) algorithm with explicit memory and gate bounds.

This mission is the statement-level formalization of Classification and implementation of unitary-equivariant and permutation-invariant quantum channels (arXiv:2510.08154v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Choi commutants characterize both channel symmetries (Proposition 4, PDF p. 16). 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 / Contribution I: extremal classification and operational factorization: Concrete signed-staircase SU(d) irreps with fixed orthonormal CG multiplicity coordinates, conjugate input factors, and the actual isometry I of Eq.(45). (hard)
• Theorem 2 / Contribution II: resource-assisted streaming ansatz: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. Resource-path embeddings and their supplied access model. (hard)
• Theorem 3 / Contribution III: three streaming applications: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. (hard)
• Theorem 5: all channels via positive multiplicity blocks: Concrete signed-staircase SU(d) irreps with fixed orthonormal CG multiplicity coordinates, conjugate input factors, and the actual isometry I of Eq.(45). (hard)
• Corollary 6: exact extreme-point parametrization: Concrete signed-staircase SU(d) irreps with fixed orthonormal CG multiplicity coordinates, conjugate input factors, and the actual isometry I of Eq.(45). (hard)
• Proposition 7: claimed trace adjoint and normalized reconstruction: Ordinary trace adjoint versus normalized reconstruction Eq.(58). (source-ambiguity)
• Theorem 8: operational factorization: Actual USS, normalized R, and CG-defined conditional irrep channel. (hard)
• Proposition 9: path resources realize an irrep embedding: Iterated simple/dual CG path transform I_mu, mixed Schur transform, and derived multiplicity comparison J. (hard)
• Proposition 10: length-restricted simple and dual CG costs: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. Length-restricted simple and dual CG transforms. (hard)
• Proposition 11: streaming path embedding with explicit access costs: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. Supplied coherent path resource storage and retrieval. (hard)
• Proposition 12 (Theorem 1 of [17]): streaming USS: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. The actual unitary Schur sampling channel. (hard)
• Proposition 13: streaming normalized Schur reconstruction: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. Corrected uniform GT sampler and normalized Schur reconstruction. (hard)
• Theorem 14: streaming composition with irrep-stage costs: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. Fixed implementations of the CG embedding branches. (hard)
• Corollary 15: streaming state symmetrization: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. (hard)
• Corollary 16: streaming optimal symmetric cloning: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. A circuit on the symmetric input operator algebra. (hard)
• Corollary 17: streaming one-output purity amplification: Executable adaptive streaming qubit circuits in the CNOT/H/Z^(1/4) gate set, with GT encodings, live-wire memory, gates, emitted-output semantics, and restricted diamond error. Normalized one-box Pieri embedding on concrete Schur images. (hard)
• Proposition 18: LR symmetries and compatible vectorized CG choices: Globally coherent multiplicity/basis transport under flips and dualization. (source-ambiguity)
• Theorem 19: all extremal irrep channels and three equivalent formulas: Signed SU(d) irrep channels and locally compatible vectorized CG intertwiners. (hard)
• Theorem 20 (Section 2 of [29]): uniform GT path sampling: Executable corrected GNW hook-walk sampler and its GT-path labeling. (hard)
• Proposition 21: weighted hook-walk equivalence and arithmetic costs: Corrected contracted weighted hook walk with an actual random arithmetic program and its costs. (hard)

Selected references

• Classification and implementation of unitary-equivariant and permutation-invariant quantum channels, arXiv:2510.08154v1, https://arxiv.org/abs/2510.08154v1

How often should a robo-advisor talk to its client?

A robo-advisor is an automated portfolio manager. It invests a client's wealth according to a model of the client's risk preferences, and it learns those preferences by interacting with the client: questionnaires, check-ins, requests to confirm or revise a risk profile. The design question of how often such a system should query its client is practical: each interaction updates the advisor's view of a preference that drifts over time, but each interaction is also exposed to the client's momentary reaction to recent market moves.

Capponi, Ólafsson and Zariphopoulou (Management Science 68(4), 2022; read here as arXiv:1911.01391v2) model this trade-off. Their Proposition 5.1 gives a closed-form approximation of how well the portfolio tracks the client's true risk aversion as a function of the time between interactions, and shows that this approximation has a unique optimal interaction time whose position responds monotonically to the model's parameters. This mission formalizes part (ii) of that proposition and the comparative statics (5.6).

Setting

Time is discrete. The client's true risk aversion $\gamma^C_n$ evolves over the investment horizon; in each period it receives, with probability $p_\epsilon \in [0,1]$, an idiosyncratic shock $\sigma_\epsilon W_n - \sigma_\epsilon^2/2$ with $W_n$ standard Gaussian and $\sigma_\epsilon > 0$, and no shock otherwise (p. 17). The robo-advisor and client interact every $\phi \ge 1$ periods. At an interaction the client communicates a risk-aversion parameter that is distorted by a behavioral bias: it is the true value multiplied by $e^{-\beta \cdot(\text{average excess market return since the last interaction})}$, where the coefficient $\beta \ge 0$ measures the strength of the bias (eq. (5.2), pp. 17–18). Between interactions the advisor keeps using the last communicated value. Market returns have volatility $\sigma(y) > 0$ in economic state $y$, and $\sigma_0 := \sigma(Y_0)$ is the volatility in the initial state.

The personalization measure (5.4) is the expected time-average relative error between the advisor's risk tolerance $1/\gamma_n$ and the client's $1/\gamma^C_n$,

$$\mathcal R(\phi,\beta) = \mathbb E\Big[\frac1T\sum_{n=0}^{T-1}\Big|\frac{1/\gamma_n - 1/\gamma^C_n}{1/\gamma^C_n}\Big|\Big].$$

Lower is better. Proposition 5.1(i) shows that $\mathcal R$ is, up to error terms, a multiple of the approximate personalization measure

$$\widetilde{\mathcal R}(\phi,\beta) = \sqrt{\frac{2}{\pi}}\left(\frac{\beta\sigma_0}{\sqrt{\phi}}\Big(1-\frac{\phi-1}{2}p_\epsilon\Big) + \sqrt{\frac{\beta^2\sigma_0^2}{\phi}+\sigma_\epsilon^2}\;\frac{\phi-1}{2}p_\epsilon\right).$$

The first term is the bias cost, which shrinks as interactions become rarer (the bias averages returns over a longer window); the second is the staleness cost, which grows with the number of shocks missed between interactions. The mission is about $\widetilde{\mathcal R}$, as Proposition 5.1(ii) is. In Lean the parameters are a structure Params with fields sig0 ($\sigma_0$), pe ($p_\epsilon$), se ($\sigma_\epsilon$), β, and $\widetilde{\mathcal R}$ is Rtilde P φ.

Formalization targets

Goal: Proposition 5.1(ii) and (5.6)

Assume $\sigma_0 > 0$, $\sigma_\epsilon > 0$, $p_\epsilon \in [0,1]$, $\beta \ge 0$ and $\beta + p_\epsilon > 0$. Then

$$\arg\min_{\phi\ge1}\widetilde{\mathcal R}(\phi,\beta) = \begin{cases} 1, & \beta = 0,\\ \phi_0\in[1,\infty), & \beta>0,\ p_\epsilon>0,\\ \infty, & p_\epsilon = 0,\end{cases}$$

and $\phi_0$ is increasing in $\beta$ and $\sigma_0$ and decreasing in $p_\epsilon$ and $\sigma_\epsilon$ (5.6). "$\arg\min = \infty$" means that no $\phi \ge 1$ is a minimizer, $\widetilde{\mathcal R}$ decreases strictly on $[1,\infty)$ and tends to its infimum $0$.

Milestones

The proof (Appendix C, p. 46) works with the bracket $f = \sqrt{\pi/2}\,\widetilde{\mathcal R}$ and an auxiliary function $g$ with $f'(\phi) = \tfrac12\beta\sigma_0p_\epsilon\phi^{-2}g(\phi)$. The milestones are its displayed claims, in order: $f \ge 0$; the two degenerate cases $p_\epsilon = 0$ and $\beta = 0$; the factorization of $f'$; the value of $f'(1)$ and the criterion $f'(1) \ge 0 \iff p_\epsilon\sigma_\epsilon^2/(\beta^2\sigma_0^2) \ge 2 + 1/p_\epsilon$; the sufficient condition $p_\epsilon\sigma_\epsilon/(\beta\sigma_0) < 1 \Rightarrow \partial_\phi\widetilde{\mathcal R}|_{\phi=1} < 0$ of p. 22; the lower bound $g'(\phi) \ge \tfrac12\phi^{-1/2}g(1)$, which settles the corner case $g(1)\ge 0$; and the interior case $g(1) < 0$, where $g$ is strictly convex, tends to $\infty$, and has a unique zero at which $f$ is minimized.

Significance

The result gives the model's two qualitative predictions in exact form. Without behavioral bias the advisor should interact at every period; without idiosyncratic shocks it should never interact; when both are present there is a single best interaction frequency, and it moves in the economically expected direction: more bias or more volatile markets call for rarer interaction, more frequent or larger preference shocks call for more frequent interaction. The p. 22 criterion gives a checkable condition, in terms of $p_\epsilon\sigma_\epsilon$ against $\beta\sigma_0$, under which interacting at every period is not optimal.

The proof in the paper is a sketch. The convexity of $g$ in the interior case is asserted ("it can be shown"), and the comparative statics (5.6) are stated as following from "the form of the function $f$". As printed, (5.6) asserts strict signs of partial derivatives of $\phi_0$, which fail on the open parameter region where the minimizer sits at the corner $\phi_0 = 1$ (there $\phi_0$ is locally constant). A machine-checked proof therefore supplies the missing convexity argument and the corrected comparative statics. No part of the proposition is known to be formalized.

Difficulty

The function $\widetilde{\mathcal R}$ mixes $\phi^{-1/2}$, $\phi^{1/2}$ and a square root of $\beta^2\sigma_0^2/\phi + \sigma_\epsilon^2$. The sign of its derivative is not visible from the formula, and the paper's sign analysis passes through $g$; the paper's claim that $g$ is strictly convex has no written proof. The comparative statics are not a differentiable implicit-function computation either: the minimizer switches between the corner $\phi = 1$ and an interior root of $g$, and the monotonicity must hold across that switch. The obvious move of differentiating the first-order condition $g(\phi_0) = 0$ in the parameters covers only the interior region and says nothing at the corner.

Formalization scope

All quantities are real. The time between interactions $\phi$ is a real variable on $[1,\infty)$: the model uses integer $\phi$, but Proposition 5.1 differentiates in $\phi$ and places $\phi_0$ in $[1,\infty)$. The standing ranges $\sigma_0 > 0$, $\sigma_\epsilon > 0$, $p_\epsilon \in [0,1]$, $\beta \ge 0$ are bundled in Params.Standing. "$\phi$ minimizes $\widetilde{\mathcal R}$" is the predicate IsOptInteraction P φ: $\phi \ge 1$ and $\widetilde{\mathcal R}(\phi) \le \widetilde{\mathcal R}(\psi)$ for all $\psi \ge 1$; there is no argmin function, so no junk value can satisfy the goal. Square roots are Real.sqrt, $\phi^{3/2}$ is $\phi\sqrt\phi$, and every statement restricts $\phi$ so that no radicand is negative and no denominator vanishes. Derivatives are stated with HasDerivAt and an explicit value. Rtilde P φ takes $\phi$ last, while the page writes both $\widetilde{\mathcal R}(\phi,\beta)$ and $\widetilde{\mathcal R}(\beta,\phi)$.

Two readings are fixed. The case "$\arg\min = \infty$" is: no minimizer exists, $\widetilde{\mathcal R}$ is strictly decreasing on $[1,\infty)$, and $\widetilde{\mathcal R}(\phi) \to 0$. The comparative statics (5.6) are stated as monotone comparative statics: if a parameter increases (keeping $p_\epsilon \le 1$), the minimizer moves weakly in the stated direction, and strictly whenever the original minimizer exceeds $1$. The monotonicity clauses quantify over minimizers for both parameter sets, and the existence clause of the goal ensures both exist, so they are not vacuous. Stating the goal about $f$ alone, or defining $\phi_0$ by sInf or by a formula, would trivialize the claim; the goal is about $\widetilde{\mathcal R}$ and its minimizers.

Part (i) of Proposition 5.1, which relates $\mathcal R$ to $\widetilde{\mathcal R}$ with unquantified $O(\cdot)$ error terms, is not formalized; neither is the optimal investment strategy of Proposition 4.1. The development needs one-variable real calculus from Mathlib, including square-root and quotient derivatives, monotonicity and convexity on intervals, and limits at infinity. Proofs of the milestones, of the convexity of $g$ on all of $[1,\infty)$ (which appears to hold without the hypothesis $g(1) < 0$), and of the derivative form of (5.6) on the interior region are all welcome.

Selected references

• A. Capponi, S. Ólafsson, T. Zariphopoulou, Personalized Robo-Advising: Enhancing Investment through Client Interaction, Management Science 68(4), 2022; preprint arXiv:1911.01391v2 (the version cited for all page and equation numbers). https://arxiv.org/abs/1911.01391

Motivation

Quantum communications promises reliable transmission of quantum information, efficient distribution of entanglement and generation of completely secure keys. For all these tasks, we need to determine the optimal point-to-point rates that are achievable by two remote parties at the ends of a quantum channel, without restrictions on their local operations and classical communication, which can be unlimited and two-way. These two-way assisted capacities represent the ultimate rates that are reachable without quantum repeaters. By constructing an upperbound based on the relative entropy of entanglement and devising a dimension-independent technique dubbed "teleportation stretching", we establish these capacities for many fundamental channels, namely bosonic lossy channels, quantum-limited amplifiers, dephasing and erasure channels in arbitrary dimension. In particular, we determine the fundamental rate-loss trade-off affecting any protocol of quantum key distribution. Our findings set the ultimate limits of point-to-point quantum communications and provide the most precise and general benchmarks for quantum repeaters.

This mission is the statement-level formalization of Fundamental Limits of Repeaterless Quantum Communications (arXiv:1510.08863v8). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-dimensional teleportation covariance and the Choi commutator (Eqs.(79)–(80), 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

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

• Main result: repeaterless pure-loss capacities, Eq.(19): Bosonic Hilbert space; Bosonic density operator; Bosonic CPTP channel; Pure-loss channel; LOCC protocol; Adaptive protocol; Protocol output; Private state; Achievable rate; Two-way capacity; Bipartite partial trace; Bosonic trace distance (hard)
• Theorem 1 (general weak converse), Eq.(7): Quantum relative entropy; Relative entropy of entanglement; Regularized adaptive REE bound; Adaptive protocol; Protocol output; Two-way capacity; Private state; LOCC protocol; Bosonic density operator; Bipartite partial trace; Bosonic trace distance (hard)
• Proposition 2 (tele-covariance): Teleportation covariance; Teleportation LOCC; Teleportation unitaries; Choi state; TMSV family; Asymptotic channel simulation; Exact channel simulation; Bipartite partial trace; Bosonic trace distance (hard)
• Lemma 3 (Stretching), Eqs.(11)–(12): Adaptive protocol; Protocol output; LOCC protocol; Exact channel simulation; Asymptotic channel simulation; Tensor-power state; Choi state; Bipartite partial trace; Bosonic trace distance (hard)
• Theorem 5 (one-shot REE bound), Eqs.(15)–(16): Asymptotic-resource REE comparator convergence class in Eq.(4) (source-ambiguity)
• Finite-resource REE converse, Eqs.(13)–(15): Exact channel simulation; LOCC protocol; Protocol output; Relative entropy of entanglement; Regularized REE; Tensor-power state; Two-way capacity; Bipartite partial trace; Bosonic trace distance (hard)
• Proposition 6, Eq.(31): Choi state; Exact channel simulation; Two-way capacity; Distillable key; Relative entropy of entanglement; Regularized REE; Channel REE; Private state; Bipartite partial trace; Bosonic trace distance (hard)
• Theorem 7: Gaussian cross entropy and relative entropy, Eqs.(58)–(61): Gaussian state; Symplectic form; Covariance matrix; Gibbs matrix; Gaussian cross entropy; Quantum relative entropy; Bosonic von Neumann entropy; Bipartite partial trace; Bosonic trace distance (hard)
• Lemma 8: energy truncation projector: Bosonic Hilbert space; Bosonic density operator; Total photon number; Energy-constrained state; Photon truncation projector; Postselected truncated state; Bosonic trace distance; Bipartite partial trace (hard)
• Lemma 9: CPTP energy truncation: Energy-constrained state; Photon truncation projector; Truncation channel; Bosonic trace distance; Bosonic CPTP channel; Bipartite partial trace (hard)
• Lemma 10: local CV–DV truncation and two classical bits: Mode-dependent local bosonic truncation error for arbitrary m_a,m_b (source-ambiguity)
• Lemma 11 (Shield size; adapted from S14): Private state; Shield dimension; Adaptive protocol; Protocol output; Distillable key; One-way key-distillation protocol; LOCC protocol; Achievable rate; Bipartite partial trace; Bosonic trace distance (hard)
• Operational task equivalences, p.2: Two-way capacity; Achievable rate; Private state; LOCC protocol; Adaptive protocol; Bipartite partial trace; Bosonic trace distance (hard)
• Teleportation-covariant Gaussian, Pauli and erasure families: Teleportation covariance; Teleportation unitaries; Gaussian channel; Pauli channel; Erasure channel; Asymptotic channel simulation; Choi state; Bipartite partial trace; Bosonic trace distance (hard)
• Every channel has an LOCC resource simulation: Exact channel simulation; Asymptotic channel simulation; Teleportation LOCC; Choi state; TMSV family; Bosonic CPTP channel; Bipartite partial trace; Bosonic trace distance (hard)
• Capacities of distillable channels and one-way achievability: Asymptotic Choi REE and distillable-channel convention (source-ambiguity)
• Fading-channel resource REE bound, Eq.(17): Asymptotic-resource REE in the fading expectation (source-ambiguity)
• Two-way quantum communication, Eqs.(114)–(120): Asymptotic-resource entanglement flux for the two directional channels (source-ambiguity)
• Multiband capacity bounds and additivity, Eqs.(121)–(128): Asymptotic-resource entanglement flux defining distillable bands (source-ambiguity)
• High-loss rate-loss law, Eq.(20): Pure-loss channel; Two-way capacity (hard)
• Strict two-way advantage of a lossy channel: Pure-loss channel; Two-way capacity; Unassisted quantum capacity (hard)
• Lossy capacity equals distributed discord, Eq.(S128): Pure-loss channel; TMSV family; Choi state; Quantum discord; Gaussian discord; Two-way capacity; Bipartite partial trace; Bosonic trace distance (hard)
• Pure-loss feedback and multiband operational specializations: Bidirectional protocol; Multiband channel; Pure-loss channel; Two-way capacity (hard)
• Multimode fibre bandwidth formula, Eq.(21): Temporal-mode count relating physical bandwidth W to independent multiband channel uses (source-ambiguity)
• Fading lossy-channel operational bound, Eq.(22): Fading channel; Publicly flagged mixture; Pure-loss channel; Two-way capacity (hard)
• Lossy-component bound for composite channels: Composite channel; Pure-loss channel; Bosonic CPTP channel; Two-way capacity (hard)
• Thermal-loss capacity sandwich, Eqs.(25),(S126): Thermal-loss channel; Thermal entropy; Two-way capacity; Coherent information (hard)
• Thermal amplifier capacity sandwich, Eqs.(27),(S142): Thermal amplifier channel; Thermal entropy; Two-way capacity; Coherent information (hard)
• Quantum-limited amplifier capacities, Eqs.(28),(S143): Thermal amplifier channel; Two-way capacity; Unassisted quantum capacity (hard)
• Additive Gaussian noise capacity sandwich, Eqs.(30),(S147): Additive-noise channel; Two-way capacity; Coherent information (hard)
• Gaussian entanglement-flux formulas, Eqs.(23),(26),(29), S124,S141,S146: Eq.(4) asymptotic-resource REE applied to the nonconvergent S119 comparator family (source-ambiguity)
• Explicit Gaussian comparator relative-entropy limits, S123,S134,S140,S145: Gaussian separable comparator; TMSV family; Choi state; Gaussian cross entropy; Quantum relative entropy; Thermal-loss channel; Thermal amplifier channel; Additive-noise channel; Thermal entropy; Bipartite partial trace; Bosonic trace distance (hard)
• Secondary canonical Gaussian forms: Eq.(4) entanglement flux of secondary bosonic canonical forms (source-ambiguity)
• Finite input/output dimensionality bound: Two-way capacity; Exact channel simulation; Teleportation LOCC (hard)
• Qubit Pauli flux and capacity bounds, Eqs.(33)–(34), S173–S176: Pauli channel; Choi state; Shannon entropy; Relative entropy of entanglement; Two-way capacity; Coherent information; Bipartite partial trace; Bosonic trace distance (hard)
• Qudit Pauli bounds, Eqs.(S190)–(S191): Pauli channel; Teleportation unitaries; Choi state; Shannon entropy; Relative entropy of entanglement; Two-way capacity; Gaussian-free separable comparator; Bipartite partial trace; Bosonic trace distance (hard)
• Depolarizing channels in arbitrary dimension, Eqs.(36)–(37), S196–S198: Depolarizing channel; Choi state; Relative entropy of entanglement; Shannon entropy; Two-way capacity; Bipartite partial trace; Bosonic trace distance (hard)
• Dephasing capacities in arbitrary dimension, Eqs.(39),(41), S182,S204: Dephasing channel; Teleportation unitaries; Choi state; Shannon entropy; Relative entropy of entanglement; Two-way capacity; Unassisted quantum capacity; Bipartite partial trace; Bosonic trace distance (hard)
• Secret-key capacity of a qudit erasure channel, Eqs.(43)–(44), S166–S167: Erasure channel; Choi state; Two-way capacity; Relative entropy of entanglement; One-way entanglement-distillation protocol; Bipartite partial trace; Bosonic trace distance (hard)
• Amplitude damping simulation through a bosonic loss channel, Eqs.(46), S208–S209: Amplitude damping channel; Single-rail encoding; Pure-loss channel; Asymptotic channel simulation; Protocol output; Teleportation covariance; Bipartite partial trace; Bosonic trace distance (hard)
• Amplitude damping capacity sandwich from loss, Eqs.(47)–(48), S214: Amplitude damping channel; Two-way capacity; Coherent information (hard)
• Amplitude damping strict advantage over unassisted capacity: Amplitude damping channel; Coherent information; Unassisted quantum capacity; Two-way capacity (hard)
• Amplitude damping variational squashing bounds, S231,S233–S234: Amplitude damping channel; Squashed entanglement; Squashing dilation; Entanglement-assisted classical capacity; Two-way capacity (hard)
• Claimed closed amplitude damping bound, Eq.(49), S232,S235: A valid optimizer or repaired proof for the closed S232/S235 squashing bound (source-ambiguity)
• Hashing inequality for energy-bounded bosonic states: Energy-constrained state; Bosonic von Neumann entropy; Coherent information; Distillable entanglement; One-way entanglement-distillation protocol; Photon truncation projector; Bipartite partial trace; Bosonic trace distance (hard)
• Claimed monotonic and finite Gaussian information limits, S108–S112: Valid parameter domain and direction/finite-limit assertion for Gaussian coherent information (source-ambiguity)
• Finite-error key bound, Eqs.(S82)–(S83): Private state; Untwisting map; Relative entropy distance to untwisted separable states; Relative entropy of entanglement; Protocol output; Bosonic trace distance; Bipartite partial trace (hard)
• Energy-constrained loss lower and upper bounds, S247: Pure-loss channel; TMSV family; Thermal entropy; Energy-constrained capacity; Coherent information; Two-way capacity (hard)
• Claimed optimal loss protocol CC cost, S250–S251: Quantized source coding convention turning continuous heterodyne entropy into a bit cost (source-ambiguity)
• Claimed finite-energy CV Bell POVM, Eq.(70): Normalized finite-energy joint Bell POVM under the stated displacement measure (source-ambiguity)
• Claimed optimal fixed-marginal separable Gaussian comparator: Exact optimization domain of the asserted fixed-marginal Gaussian comparator optimality (source-ambiguity)
• Finite-energy adaptive simulation error, Eqs.(98)–(106): Energy-constrained diamond norm; Energy-constrained state; Adaptive protocol; Protocol output; Asymptotic channel simulation; Bosonic trace distance (hard)

Selected references

• Fundamental Limits of Repeaterless Quantum Communications, arXiv:1510.08863v8, https://arxiv.org/abs/1510.08863v8

Motivation

We ask when qubit controls can produce an effective generator that drives every initial state to the same pure state. Lie-algebra closure alone cannot answer this question because it loses the distinction between reversible control and irreversible dissipation. Lie wedges retain this distinction by enforcing nonnegative strengths for dissipative generators. For drift-free qubits with Hamiltonian controls available with either sign and at most one independently actuated dissipator generated by a traceless jump operator, we classify all nontrivial systems into thirteen structural types, or strata. Explicit tests assign each system to a stratum, and necessary and sufficient conditions determine whether its Lie wedge contains a stabilizing generator. These criteria distinguish stabilizable and non-stabilizable systems even when they share the same generated Lie algebra and stratum. In one exceptional stratum, a single dissipative orientation cannot stabilize a pure state even with the available Hamiltonian controls. Averaging two orientations of the same dissipative channel, related by those controls, produces a stabilizing generator. △ Less

This mission is the statement-level formalization of Lie-Wedge Stratification and Pure-State Stabilizability in Single-Channel Qubit Control (arXiv:2610.00046v1). 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 Lemma 2.7: Dissipation functional with basis normalization (Lemma 2.7, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 2.3: Affine structure of the Lindblad–Kossakowski algebra: cited background result outside the original-result drafting scope (hard)
• Theorem 2.4: GKLS characterization in Kossakowski form: cited background result outside the original-result drafting scope (hard)
• Lemma 2.5: Hamiltonian edge of the GKLS wedge: cited background result outside the original-result drafting scope (hard)
• Theorem 2.6: The GKLS cone is a Lie wedge: cited background result outside the original-result drafting scope (hard)
• Corollary 2.8: Hamiltonian rigidity of the commutator ideal: computed derived ideal, solvable radical, and Levi projection inside the real GKLS algebra (hard)
• Proposition 2.15: Finite iterative construction of the minimal closed Lie wedge: minimal closed Lie wedge, edge-generated exponential subgroup, and tangent semigroup (hard)
• Lemma 2.17: Radical slice is a Lie wedge: cited background result outside the original-result drafting scope (hard)
• Lemma 2.18: Quotient cone and projected-edge invariance: cited background result outside the original-result drafting scope (hard)
• Lemma 2.19: Fiber-map properties: cited background result outside the original-result drafting scope (hard)
• Proposition 2.20: Necessity of fiber compatibility: cited background result outside the original-result drafting scope (hard)
• Proposition 2.22: Unique reconstruction from admissible fiber data: cited background result outside the original-result drafting scope (hard)
• Theorem 2.23: Levi decomposition–reconstruction correspondence: cited background result outside the original-result drafting scope (hard)
• Lemma 3.4: Invariance under the allowed equivalences: computed Levi-data tuple and transported minimal wedge under specification equivalences (hard)
• Lemma 3.9: Edge rigidity including several channels and one-sided drift: minimal Lie wedge for general finite multi-channel specifications with one-sided Hamiltonian drifts (hard)
• Proposition 3.10: Four possible semisimple Levi factors: solvable radical quotient and real Lie isomorphism classes of Levi complements (hard)
• Lemma 3.11: Orbit-average representation of the wedge: compact control group, finite Borel orbit measures, and minimal/radical Lie wedges (hard)
• Corollary 3.12: Full-control quadrupole-free radical cone: quadrupole-free SO(3) orbit-average cone and its radical span (hard)
• Corollary 3.13: Sharp axial circular radical cone: axial orbit Fourier moments and exact circular radical cone (hard)
• Lemma 3.14: Magic locus for a nonzero radical wedge: uniform axial channel average and actual radical-wedge intersection (hard)
• Corollary 3.16: Axial Lie-closure dichotomy: a source-pinned choice between traceless input and full symmetric input (source-ambiguity)
• Lemma 3.18: Parametric matrix projections and translation kernels: independent Table 1 row predicates plus computed matrix projections and translation kernels (hard)
• Corollary 3.19: Radicals across the nontrivial channel strata: Table 1 row predicates, computed solvable radicals, and the affine weight-zero average (hard)
• Corollary 3.20: Radical cones across the nontrivial channel strata: Table 1 row predicates and computed radical cones from orbit averages (hard)
• Theorem 3.21: Exhaustive thirteen-value classification and residual moduli: full thirteen-row discriminant assignment, computed Levi tuple, and residual orbit-moduli quotient (hard)
• Corollary 3.23: Globality and the exact semialgebra boundary: closed switched semigroup tangent wedge and local BCH-closed Lie semialgebra predicate (hard)
• Lemma 3.25: Pure candidates and uniform dissipative contraction: normalized pure stationary states of finite orbit-average generators and almost-everywhere jump eigenstate compatibility (hard)
• Theorem 3.26: Axial stabilization iff the scalar criterion, with minimum support: trace-norm pure-state global asymptotic stability in the computed axial wedge and minimum distinct orbit-ray support (hard)
• Corollary 3.27: Thirteen-stratum pure-state stabilization atlas: all Table 2 capability predicates and minimum support over independently defined thirteen strata (hard)
• Remark 2.12 and the strict-inclusion example: minimal local wedge, closed autonomous semigroup, and quasi-periodic Hamiltonian witness (hard)
• Unnumbered endpoint stabilization result: pure-state GAS for the actual wedge at q=0 and bare damping at q=1 (hard)
• Remark 3.29: full-control pure targets: orbit-ray pure-target GAS and laboratory-fixed-dissipator comparison (hard)
• §3.8: all four Levi types are realized: actual Levi-type predicates and realized row assignment (hard)
• §4: the mixed reductive Q4 wedge does not split: computed Q4 minimal wedge and dimensions of its span versus edge/average span (hard)

Selected references

• Lie-Wedge Stratification and Pure-State Stabilizability in Single-Channel Qubit Control, arXiv:2610.00046v1, https://arxiv.org/abs/2610.00046v1

Motivation

The use of quantum resources in the work extraction from a quantum system is an emerging research topic. Recently, [arXiv:2602.22893] established the necessity of measurement coherence for obtaining advantage in work extraction from an unknown isolated quantum system. However, a quantitative relation between the magnitude of this advantage and established measures of measurement coherence is missing. Here, we establish such a connection by introducing a faithful operational quantifier of the work advantage provided by a measurement. We show that measurement coherence is necessary and sufficient for a positive advantage, and derive upper and lower bounds in terms of the robustness of measurement coherence and an $l_{\infty}$ norm based coherence measure respectively. Finally, we examine this quantifier of advantage from the resource theoretic perspective. Our results provide an operational characterisation of measurement coherence as a resource for work extraction and reveal a nontrivial relation between its resource content and thermodynamic value. △ Less

This mission is the statement-level formalization of All coherent measurements provide observational ergotropic advantage (arXiv:2609.18735v1). 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 1 (Theorem 1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Appendix A closing sentence: A quantified meaning of optimality for the final Theorem 3 coefficient: optimal for each fixed dimension, or a weaker assertion that the displayed dimension-dependent bound cannot be improved uniformly. (source-ambiguity)

Selected references

• All coherent measurements provide observational ergotropic advantage, arXiv:2609.18735v1, https://arxiv.org/abs/2609.18735v1

Motivation

We investigate the relaxation dynamics and steady state of a qubit interacting with a coherent environment through an energy-conserving flip-flop interaction within the Markovian repeated-interaction framework. We derive an exact analytical solution for the evolving and stationary state, nonperturbative in the environmental coherence. We show that environmental coherence provides a resource for dissipative state preparation by expanding the set of accessible steady states. In particular, coherent ancillas can increase the system ground- state population beyond that of the bath, corresponding to an effective temperature below the bath temperature, and enhance its steady-state purity, with these effects controlled by the interplay between the system energy scale and the system-ancilla coupling. Nevertheless, we prove that the purity of the system can never exceed the purity of the ancilla. We further analyze the thermodynamics of the protocol and show that environmental coherence can modify and even reverse the natural direction of heat transfer, giving rise to anomalous heat flow. Remarkably, for fixed interaction parameters, the direction of the coherence-induced heat transfer is governed by the relative phase between the system and ancilla coherence, whereas their magnitudes determine the amount of heat exchanged. Our results establish environmental coherence as a resource for controlling steady-state preparation and energy transfer in repeated-interaction dynamics. △ Less

This mission is the statement-level formalization of Coherence-assisted quantum state preparation and thermal control through repeated interactions (arXiv:2610.10794v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Stationary purity is capped by ancilla purity (Abstract; §III B Eq.(26); Appendix D: ancilla purity cap, 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

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

• §II B: K>0 claimed to suffice for relaxation: A correct complete relaxation domain replacing K>0 alone (source-ambiguity)
• §III A: alleged cooling-only behavior at odd pi collisions: An attracting state at odd-pi collisions (source-ambiguity)
• §III A: maximum percentage and doubled-polarization claims: Consistent optimization claim and physically admissible nonzero polarization doubling (source-ambiguity)
• Appendix A.2: claimed equivalence of unitary and Hamiltonian symmetry: A valid converse from fixed-duration unitary symmetry to Hamiltonian symmetry (source-ambiguity)
• Appendix B Eqs.(B4)–(B7): claimed continuous-time master equation: A consistent collision-limit scaling, coherence scaling and rotating frame (source-ambiguity)
• Appendix E: literal unrounded real upper bound: An integer upper bound for a strict trace-distance tolerance (source-ambiguity)
• Appendix E Fig.9: observed coherence-induced relaxation slowdown: Quantified parameter domain and comparison for actual collision counts (source-ambiguity)

Selected references

• Coherence-assisted quantum state preparation and thermal control through repeated interactions, arXiv:2610.10794v1, https://arxiv.org/abs/2610.10794v1

Motivation

Randomized measurement protocols give experimental access to low-degree polynomial invariants of a quantum state rather than to the state itself, which raises the question of what the best entanglement criterion is that can be built from finitely many such invariants. In this work we answer this question through convex duality. For each degree we introduce the cone of local unitary trace inequalities that are valid for separable bipartite states in all local dimensions, together with its one-matrix counterparts for Hermitian and positive semidefinite matrices. Each cone is the polar dual of a moment cone; we also determine the minimal combinatorial parametrization of the separable cone. The framework organizes the known moment criteria: the PPT criterion using the first three moments of the partial transposition is the image under an embedding of a Hankel determinant from the positive semidefinite cone to the bipartite cone, which we show to be an extremal ray, and we determine the first nontrivial separable cone completely, finding exactly four extremal rays. The framework allows us to analyze the realignment criterion and its centered (or enhanced) variant. We prove that the even singular value moments of the (centered) realignment matrix are trace invariants, associated with explicit fixed-point-free involutions. Extracting the optimal trace-norm bound from $m$ such moments thus becomes a dimension-free truncated moment problem, which we solve in closed form for $m = 2$ and relax to a semidefinite program of size $O(m)$ for arbitrary $m$. The dual solutions are polynomial minorants of $\sqrt{x}$ on $[0,1]$, and two explicit families, binomial and $L^1$-weighted, yield hierarchies of separability inequalities. Finally, we compare the criteria against one another and on PPT entangled states. △ Less

This mission is the statement-level formalization of Optimal entanglement criteria from trace invariants (arXiv:2609.29471v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

43 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Abstract / §4.1: separable trace inequalities and their moment polar (Abstract / §4.1: separable trace inequalities and their moment polar, 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

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

• Abstract / Introduction unnumbered: claimed pointwise convergence of weighted minorants: Abstract / Introduction unnumbered: claimed pointwise convergence of weighted minorants (source-ambiguity)
• §6.4 / Table 1: noisy Tiles numerical detection benchmark: §6.4 / Table 1: noisy Tiles numerical detection benchmark (source-ambiguity)
• Table 2: rounded noisy binomial thresholds: Table 2: rounded noisy binomial thresholds (source-ambiguity)
• Appendix A Eq.(48): approximate degree-five optimizer: Appendix A Eq.(48): approximate degree-five optimizer (source-ambiguity)

Selected references

• Optimal entanglement criteria from trace invariants, arXiv:2609.29471v1, https://arxiv.org/abs/2609.29471v1

Motivation

Quantum entanglement is a fundamental resource in quantum information theory, yet its general characterization and quantification remain challenging, especially in multipartite systems. In this work we investigate entanglement from a geometric perspective, focusing on the Riemannian structure induced by the Fubini--Study metric on the projective Hilbert space of multi-qubit quantum states. By exploiting the local-unitary invariance of this metric, we derive the entanglement distance (ED), a geometric measure that quantifies entanglement as an obstruction to locally minimizing the sum of squared Fubini--Study distances generated by local operations. We analyze the properties of ED for pure multi-qubit states and discuss its behavior under local operations and classical communication. In particular, we show that ED reproduces established entanglement measures in well-defined and restricted settings. For pure states of two qubits, ED reduces to an exact monotone function of the concurrence and, independently, to an explicit monotone function of the entropy of entanglement. These results provide a clear geometric interpretation of standard bipartite entanglement measures within the present framework, while highlighting the limitations of such correspondences beyond the two-qubit case. △ Less

This mission is the statement-level formalization of Geometric Aspects of Entanglement (arXiv:2610.03446v1). 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 Unnumbered main result: geometric minimum principle and closed ED formula, Eqs.(18)–(24) (Unnumbered main result: geometric minimum principle and closed ED formula, Eqs.(18)–(24), 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:

• Property iii; Eqs.(25)-(32): A clarified average-over-outcomes pure-state LOCC assertion replacing the printed conditional claim. (source-ambiguity)

Selected references

• Geometric Aspects of Entanglement, arXiv:2610.03446v1, https://arxiv.org/abs/2610.03446v1

Motivation

This is a continuation of the expository article \cite{krp} with some new remarks. Let $S_n$ denote the set of all Gaussian states in the complex Hilbert space $L^2 (\mathbb{R}^n),$ $K_n$ the convex set of all momentum and position covariance matrices of order $2n$ in Gaussian states and let $\mathcal{G}_n$ be the group of all unitary operators in $L^2 (\mathbb{R}^n)$ conjugations by which leave $S_n$ invariant. Here we prove the following results. $K_n$ is a closed convex set for which a matrix $S$ is an extreme point if and only if $S=\frac{1}{2} L^{T} L$ for some $L$ in the symplectic group $Sp (2n, \mathbb{R}).$ Every element in $K_n$ is of the form $\frac{1}{2} (L^{T} L + M^{T} M)$ for some $L,M$ in $Sp (2n, \mathbb{R}).$ Every Gaussian state in $L^2 (\mathbb{R}^n)$ can be purified to a Gaussian state in $L^2 (\mathbb{R}^{2n}).$ Any element $U$ in the group $\mathcal{G}_n$ is of the form $U = \lambda W ({\bm {\alpha}}) \Gamma (L)$ where $\lambda$ is a complex scalar of modulus unity, ${\bm {\alpha}} \in \mathbb{C}^n,$ $L \in Sp (2n, \mathbb{R}),$ $W({\bm {\alpha}})$ is the Weyl operator corresponding to ${\bm {\alpha}}$ and $\Gamma (L)$ is a unitary operator which implements the Bogolioubov automorphism of the Lie algebra generated by the canonical momentum and position observables induced by the symplectic linear transformation $L.$

This mission is the statement-level formalization of The Symmetry Group of Gaussian States in L²(ℝⁿ) (arXiv:1101.5041v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The Gaussian covariance set is closed and convex (§1, following (1.3), PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Theorem 7: Normalized Gaussian density operators on L²(R^n), the actual Weyl operators of (2.4), and symplectic implementers defined by (2.9). (hard)
• §2, (2.12)–(2.17): The Hilbert–Schmidt ideal as a Hilbert space, its kernel isometry I, full L² dilations and second quantization, linked to the trace-class characteristic transform. (hard)
• Theorem 4, (3.11): Constructed normalized multimode Gaussian density and full number-basis thermal spectral operator, together with Weyl and metaplectic actions on L²(R^n). (hard)
• Corollary 2, pp.14–15: Normalized squeezed Gaussian L² wavefunctions, their finite tensor product and actual passive second-quantization unitary. (hard)
• Theorem 5, pp.15–16: The completed n+n mode Hilbert tensor identification, normalized pure Gaussian joint densities and actual relative trace over the second n modes. (hard)
• Theorem 6, pp.16–18: Full multimode number-basis thermal density, Gaussian state predicate and spectral unitary beta on every occupation vector in N^n. (hard)
• §2, paragraph after (2.17): A corrected source statement for the printed 12th-root and 12th-power claim. (source-ambiguity)

Selected references

• The Symmetry Group of Gaussian States in L²(ℝⁿ), arXiv:1101.5041v1, https://arxiv.org/abs/1101.5041v1

Motivation

Simple optical instruments are linear optical networks where the incident light modes are turned into equal numbers of outgoing modes by linear transformations. For example, such instruments are beam splitters, multiports, interferometers, fibre couplers, polarizers, gravitational lenses, parametric amplifiers, phase-conjugating mirrors and also black holes. The article develops the quantum theory of simple optical instruments and applies the theory to a few characteristic situations, to the splitting and interference of photons and to the manifestation of Einstein-Podolsky-Rosen correlations in parametric downconversion. How to model irreversible devices such as absorbers and amplifiers is also shown. Finally, the article develops the theory of Hawking radiation for a simple optical black hole. The paper is intended as a primer, as a nearly self-consistent tutorial. The reader should be familiar with basic quantum mechanics and statistics, and perhaps with optics and some elementary field theory. The quantum theory of light in dielectrics serves as the starting point and, in the concluding section, as a guide to understand quantum black holes.

This mission is the statement-level formalization of Quantum Physics of Simple Optical Instruments (arXiv:quant-ph/0305007v2). 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 Canonical constraints and passive photon-number conservation (§3.1: canonical matrix constraints and photon-number conservation, 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

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

• §2.1: wave equation and conserved scalar product: Classical wave-action variation and full-line indefinite mode product (hard)
• §2.2: canonical quantization and oscillator energy: Complete generalized-mode quantization and electromagnetic energy quadratic form (hard)
• §2.3: transfer equation, structure, determinant, inverse: Forward transfer fundamental solution for the impedance ODE (hard)
• §2.4: unitary scattering from dielectric transfer data: Normalized asymptotic dielectric modes and their mode-operator basis change (hard)
• §3.2: Heisenberg–Schrodinger state correspondence: Bounded observable pairing and conjugation on arbitrary trace-class Fock states (hard)
• §3.2: unrestricted single-logarithm implementation recipe: A valid domain for a symmetry-compatible single Hamiltonian logarithm (source-ambiguity)
• §3.3: real beam-splitter Hamiltonian: Self-adjoint closure and full-Fock unitary exponential of the beam generator (hard)
• §3.3: two-mode amplifier Hamiltonian: Self-adjoint two-mode squeezing generator and its full unitary group (hard)
• §3.4, Eq.(3.30): Wigner covariance of simple optical instruments: General finite-mode trace-class Wigner transform and active metaplectic covariance (hard)
• §4.2: rotations and general beam-splitter evolution: Closed Jordan–Schwinger exponentials with simultaneous mode and Stokes actions (hard)
• §5.1: Lindblad absorption/emission becomes Fokker–Planck drift and diffusion: Weak Wigner generator identity for the unbounded absorption/emission Lindbladian (hard)
• §5.2: thermal stationary state: Thermal density, Wigner correspondence and stationary generator domain (hard)
• §5.2: exact thermal-loss beam-splitter model and long-time limit: Thermal attenuator semigroup and full-state trace-norm limit (hard)
• §5.3: exact thermal-amplifier model: Thermal amplifier channel and unbounded-generator equivalence (hard)
• §5.3: balanced gain/loss strictly reduces purity: Quantum heat semigroup purity derivative for every physical input (hard)
• §5.3: phase-sensitive Gaussian reservoir model: Squeezed Gaussian reservoir conjugation of the Lindblad semigroup (hard)
• §6.2: Lorentz action, unitary amplifier, and number-difference conservation: Full squeezing exponentials and Lorentz conjugation on closed unbounded operators (hard)
• §6.3: squeezed-vacuum Wigner density and EPR quadrature widths: Identification of the squeezed state Wigner transform and EPR variances (hard)
• §6.3: either reduced squeezed-vacuum state is thermal: Squeezed-vacuum partial trace, Gibbs state and temperature correspondence (hard)
• §6.3: maximal entanglement at fixed oscillator energy: Extended oscillator von Neumann entropy under a finite energy constraint (hard)
• §6.3: normalized Fock expansion of the two-mode squeezed vacuum: Squeezed-vacuum geometric series linked to its unitary preparation (hard)
• §6.3: weak downconversion and the effect of photon-pair postselection: Weak-squeezing asymptotics, nonzero pair conditioning and exact product output (hard)
• §6.3: polarization-invariant downconversion produces singlet pairs: Four-mode unitary downconversion and corrected tensor-product squeezed output (hard)
• §7.1: moving-medium effective wave equation: Variational Euler–Lagrange interface for the effective moving dielectric (hard)
• §7.2: moving light is a massless field in the effective metric: Effective Lorentz metric and scalar d’Alembert operator identification (hard)
• §7.3: general null-coordinate wave solution: Both directions of null-coordinate solution classification on horizon-free patches (hard)
• §7.3: logarithmic horizon coordinate and wavelength scaling: One-sided horizon coordinate asymptotics with signed branch control (hard)
• §7.4: conserved moving-medium mode product: Moving-medium conserved indefinite current with full-line integral domain (hard)
• §7.4: local analytic horizon connection and Bogoliubov ratio: Branch-fixed local horizon modes and their normalized Bogoliubov connection (hard)
• §7.4: global identification of the pre-collapse vacuum: Quantified horizon-formation history preserving the required analyticity (source-ambiguity)
• §7.4: Hawking thermal spectrum in the stated analytic-vacuum model: Stationary analytic-vacuum thermal density with spectral normalization (hard)
• §7.5: grey-body scattering of the generated radiation: Exterior variable-epsilon wave scattering and normalized radiation channel (hard)

Selected references

• Quantum Physics of Simple Optical Instruments, arXiv:quant-ph/0305007v2, https://arxiv.org/abs/quant-ph/0305007v2

Motivation

We give a mathematical formulation for the Choi-Jamiolkowski (CJ) correspondence in the infinite-dimensional case in the form close to one used in quantum information theory. We show that there is no need to use a limiting procedure to define "unnormalized maximally entangled state" and the corresponding analog of the Choi matrix since they can be defined rigorously as, in general, nonclosable forms on an appropriate dense subspace. The properties of these forms are discussed in Sec. 2. An important question is: when the CJ form is given by a bounded operator. This is the case for entanglement-breaking channels: we prove this in Sec. 3 along with a version of a result of Wolf et al. characterizing CJ operators which correspond to such channels by giving precise definitions of a separable operator and a relevant integral. In Sec. 4 we obtain explicit expressions for CJ forms and operators defining a general Bosonic Gaussian channel. In Sec. 5 we give a decomposition of the Gaussian CJ form into product of the four principal types and a necessary and sufficient condition for existence of the bounded CJ operator.

This mission is the statement-level formalization of On the Choi-Jamiolkowski Correspondence in Infinite Dimensions (arXiv:1004.0196v3). 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 2: separable normalized CJ operators are contractions (Lemma 2: separable CJ operators are contractions, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

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

Deferred results

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

• Lemma 1: existence and uniqueness of the CJ form: Trace-class channel, basis conjugation, algebraic-domain sesquilinear form, and bounded-operator trace duality for both equalities in (2). (hard)
• Equations (3)–(4) and converse correspondence: Reconstruction of a complex-linear trace-class channel from a normalized positive algebraic-domain form. (hard)
• Countable Kraus representation: Countable bounded Kraus operators, strong normalization, and trace-norm-convergent action on every trace-class operator. (hard)
• Identity-channel form and weak maximally entangled prescription: Unbounded diagonal tensor functional, closability of its positive form, and weak Phi tensor identity on that form. (hard)
• Basis covariance and basis-independent bounded norm: Basis-dependent channel/CJ correspondence and conjugate transpose, including unbounded form pullback. (hard)
• Faithful-reference normalized CJ state and recovery: Faithful density spectral purification, tensor channel on full trace class, partial traces and dense-range square-root recovery. (hard)
• Proposition 1: entanglement breaking iff separable bounded CJ operator: Trace-class tensor channels, entanglement breaking, operator-valued measures and their weak integral against conjugated input effects. (hard)
• General Weyl integral for the CJ form (13): Strongly continuous irreducible finite-mode Weyl systems, channel adjoint, and scalar integrability for matrix elements of (13). (hard)
• Gaussian integrals (16)–(18) and sufficient boundedness: Operational Gaussian channel/Weyl model and weak versus norm-convergent Gaussian operator integrals. (hard)
• Case 4: noiseless delta form and nonclosability: Distributional Weyl inversion and nonclosability for actual noiseless multi-mode CJ forms. (hard)
• Case 3: commuting-noise Gaussian operator: Joint spectral calculus for the strongly commuting unbounded quadratures R_BA. (hard)
• Proposition 2: exact norm for nondegenerate commutator defect: Operational Gaussian CJ operator and spectral absolute value of the generally nonnormal matrix Delta_K^(-1) mu. (hard)
• Case 1: strictly mixed Gaussian CJ operator (22): Williamson-defined Gibbs quadratic form and spectral exponential of unbounded quadratures. (hard)
• Case 2: printed pure-noise kernel formula (source discrepancy): Source discrepancy: the printed quadratic kernel has a missing factor 1/2. (source-ambiguity)
• Normal modes and thermal spectral formula (23)–(28): Fock number operators, tensor decomposition of a reducible CCR representation, and unbounded Gibbs functional calculus. (hard)
• One-mode norm and non-EB contraction example: Actual one-mode Gaussian channel/CJ operator and EB predicate, including the commuting k=1,m>0 regime. (hard)
• One-mode mixed operator (29) and pure boundary: Canonical/Fock transposition, unbounded one-mode quadratic Hamiltonian and its spectral projections. (hard)
• Four principal factors, rank counts, and tensor realization: Symplectic extension and unitary tensor realization of the four weak Gaussian form integrals, including singular classical blocks. (hard)
• Proposition 3: exact boundedness criterion: Operational Gaussian CJ form across all singular/noise/commutator regimes and its bounded-representability predicate. (hard)
• Open-system interpretation and four noise types: Given operational Gaussian reversible dilation, its noise observables, their covariance, commutators and quantum/classical interpretation. (hard)

Selected references

• On the Choi-Jamiolkowski Correspondence in Infinite Dimensions, arXiv:1004.0196v3, https://arxiv.org/abs/1004.0196v3

Motivation

Shareholder engagement with corporate management is a public good: when a change of policy raises firm value, every shareholder gains, but only the shareholders who engage pay the cost. Since Grossman and Hart (1980) this free-rider problem has been the standard explanation for why dispersed owners under-monitor management. In practice, however, engagement campaigns are increasingly run by wolf packs: several activist funds, each holding a small block, who engage together even though none could change policy alone.

Brav, Dasgupta and Mathews ask why such packs form when each member's stake is small and most of the capital they invest belongs to outside investors. Their answer is competition for flow. Fund investors observe who engaged and move their capital toward funds that revealed skill by engaging; the fees on that capital are a private, excludable reward for engagement. The paper shows that this flow motive can sustain collective engagement over parameter ranges where it fails both for funds that manage delegated money without flows and for funds that invest only their own money.

Setting

A firm has a unit continuum of shares. There are $N$ skilled and $M$ unskilled activist funds; each holds one block of size $b \in (0,1)$ and cash $c > 0$, and $(M+N)b \le 1$. A block consists of a fraction $\phi \in (0,1)$ of the fund's own capital and $1-\phi$ of delegated capital, on which the fund earns a fee $w \in (0,1)$. The difficulty $\eta$ of changing policy lies in $(b, U]$ with $U > 1$ and is public. Only skilled funds can engage, each at cost $c$. If $k$ funds engage, engagement succeeds iff $kb \ge \eta$; the firm is then worth $P_2 = P_h > 0$, otherwise $P_2 = 0$. Write $\alpha = Nb$ and let $K_\eta$ be the least natural number $x$ with $xb \ge \eta$.

A skilled fund's payoff is $(s\,bP_2 + w f_2 + c\,\mathbf 1_{NE})R_S$, where $R_S > 1$ is its reinvestment return, $s$ its proprietary fraction and $f_2$ the value of the delegated capital it holds at the end. Three games differ only in $s$ and $f_2$:

1. delegated game with competition for flow: $s = \phi$; if $k \ge 1$ funds engage, the delegated capital of the $M+N-k$ non-engagers moves evenly to the $k$ engagers;
2. delegated game without competition for flow: $s = \phi$; every fund keeps its own delegated capital $(1-\phi)bP_2$;
3. proprietary blocks game: $s = 1$ and there is no delegated capital.

The fee value of an engager's capital when exactly $x$ funds engage and succeed is (Definition 5)

$$\hat c(x) = w\Big((1-\phi)bP_h + \tfrac1x (M+N-x)\,b(1-\phi)P_h\Big).$$

For each $\eta$ the skilled funds play a finite simultaneous game, the $\eta$-subgame. A maximal success equilibrium (Definition 1) picks, for every $\eta$, a Nash equilibrium of the $\eta$-subgame whose probability of successful engagement is maximal among all its Nash equilibria, mixed ones included.

Formalization targets

Goal: Proposition 7

With $\bar c(\eta) = \phi bP_h + \hat c(K_\eta)$, for every $\eta \in (b, \alpha]$:

$$c \in \big(\phi bP_h + w(1-\phi)bP_h,\ \bar c(\eta)\big] \ \Longrightarrow\ \text{flow game succeeds, no-flow game cannot},$$ $$c \in \big(bP_h,\ \bar c(\eta)\big] \ \Longrightarrow\ \text{flow game succeeds, proprietary game cannot};$$

the first range is always non-empty, and the second is non-empty for some $\eta$ when $M+N > 2/w$. "Succeeds" means that every maximal success equilibrium of the flow game succeeds with probability one at $\eta$ (and one exists); "cannot" means every Nash equilibrium of the comparison game's $\eta$-subgame has success probability zero.

Milestones

• Lemma 2: on each interval $(\hat c(L+1), \hat c(L)]$ (and $(\hat c(K_\eta+1), \phi bP_h + \hat c(K_\eta)]$) a pure equilibrium of the flow game with exactly $L$ (resp. $K_\eta$) engagers exists; all $N$ engage for $c \le \hat c(N)$, or for $c \le \phi bP_h + \hat c(N)$ when $K_\eta = N$.
• Proposition 4: in the flow game success occurs iff $\eta \le \alpha$ and $c \le \bar c(\eta)$; otherwise no equilibrium involves engagement.
• Proposition 3: in the no-flow game the same holds with the threshold $\phi bP_h + w(1-\phi)bP_h$, by exactly $K_\eta$ funds.
• Proposition 2: in the proprietary game the same holds with the threshold $bP_h$.

Significance

Propositions 2 and 3 formalize the classical underprovision result and its aggravation by delegation: since $w < 1$, a fund that manages other people's money has weaker incentives to bear private engagement costs. Proposition 7 shows that flows reverse this ranking, and that the reversal against the proprietary benchmark is driven by the number of funds: the larger $M+N$, the more capital an engager can attract. This is the paper's explanation of why wolf packs of small funds can be more effective than a single large owner, and it underlies the paper's comparative statics in activist capital.

The results are proved in the paper (Management Science, 2022); none of them has been formalized. The mission produces a machine-checked model of threshold engagement games with three payoff regimes on top of a published finite-game vocabulary, and machine-checked proofs that also cover mixed equilibria, which the paper treats in a short argument. Two hypotheses missing from the printed Proposition 7 ($M \ge 1$, $N \ge 2$) and one endpoint in Lemma 2 are made explicit.

Difficulty

Each pure-profile check is a comparison of two numbers, but three steps need care. First, the cost intervals of Lemma 2 must cover the whole half-line $c \le \bar c(\eta)$; this uses that $\hat c$ is strictly decreasing and the endpoint $c = \hat c(N)$, which the printed lemma excludes. Second, "no engagement" above the thresholds must hold for every mixed equilibrium, so the argument has to work with expected payoffs over all $2^N$ pure profiles rather than with one pivotal fund. Third, a maximal success equilibrium is a family indexed by $\eta$, and maximality compares it against every mixed equilibrium of each subgame. The naive reading of Proposition 7 as three interval inequalities misses all of the game theory and is not the target.

Formalization scope

The model is one definitions file, WolfPack.FlowEngage.Model, built on the published agt_games vocabulary (AGT.IsPureNash, AGT.IsMixedNash, AGT.profileProb). Players are Fin N (the skilled funds; unskilled funds never act and enter only through $M$ in the reallocation). Actions are Bool, with true = engage. Mixed profiles are weight functions; the success probability sums over the $2^N$ pure profiles. $K_\eta$ is sInf over $\mathbb N$; $\hat c$ casts to $\mathbb R$ before subtracting. The proprietary game is the model with the proprietary fraction set to $1$, all else unchanged (p. 15, footnote 14).

Conventions and additions, all disclosed in the items:

• standing assumptions $0<b<1$, $c>0$, $U>1$, $R_S>1$, $\phi, w \in (0,1)$ from §2, plus $P_h > 0$, $M \ge 1$ and $(M+N)b \le 1$, which the model implies but does not display;
• $N \ge 2$ in the goal: with $N = 1$ there is no $\eta \in (b,\alpha]$ and the "for some $\eta$" clause fails;
• the reallocation of delegated capital is the off-equilibrium belief fixed in the proof of Lemma 2 (engagers posterior 1, non-engagers below 1), built into the payoff rather than left as a parameter;
• Lemma 2 1(c) is stated with $c \le \hat c(N)$, as its proof shows, instead of the printed $c < \hat c(N)$.

A formalization in which "success is impossible" quantified only over pure equilibria, in which the comparison game was allowed to choose its own no-engagement equilibrium, or in which "every maximal success equilibrium" ranged over an empty set would be trivial; the goal quantifies over all mixed equilibria of the comparison games and asserts existence of a maximal success equilibrium. Not formalized: Proposition 1 (social optimum), Lemma 1, Corollaries 1–3, Propositions 5, 6, 8, the asymmetric-information extension of Appendix B, and the case $P_l > 0$. Proofs of any milestone are welcome, as are general lemmas on mixed equilibria of binary-action symmetric games.

Selected references

• A. Brav, A. Dasgupta, R. Mathews, Wolf Pack Activism, Management Science 68(8):5557–5568, 2022; accepted manuscript May 2021, LSE Research Online eprint 112118, https://ssrn.com/abstract=2529230. https://doi.org/10.1287/mnsc.2021.4131
• S. Grossman, O. Hart, Takeover Bids, the Free-Rider Problem, and the Theory of the Corporation, Bell Journal of Economics 11(1):42–64, 1980. https://doi.org/10.2307/3003400
• N. Nisan, T. Roughgarden, É. Tardos, V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 1. https://doi.org/10.1017/CBO9780511800481

Motivation

Many service systems match heterogeneous customers to heterogeneous resources: jobs to machines in a data centre, patients to beds, orders to couriers, donors to recipients. A recurring question is whether such a system, run first-come-first-served among compatible pairs, has a stationary distribution that can be written down. Two lines of work answered it for special structures: the order-independent queue of Krzesinski (2011, cited as [20] in the paper), where the service rate of the population does not depend on the order of customers, and the multi-type job and server model of Visschers, Adan and Weiss (2012, [22]), where customers are matched to compatible servers under an assignment rule. Redundancy systems with cancel-on-completion fit the first framework and those with cancel-on-start the second (arXiv:1902.02137v1, p. 3); matching models fit the second.

Ayesta, Bodas, Dorsman and Verloop (arXiv:1902.02137v1, later published in Operations Research, 2022) introduce the token-based central queue, which contains both. Their Theorem 1 states that, under an assignment condition and an order-independent condition, the stationary distribution has a product form. The paper's performance results (generating functions of queue lengths, Laplace transforms of waiting and sojourn times) and its applications (heterogeneous M/M/K, multi-server job models, redundancy, matching) are derived from it.

Setting

There is a finite set $\mathcal C$ of customer types and a finite set $\mathcal T=\{t_1,\dots,t_K\}$ of tokens. Type-$c$ customers arrive in a Poisson process of rate $\lambda_c>0$; $\lambda=\sum_c\lambda_c$. A type-$c$ customer can hold only tokens from its compatibility set $\mathcal T_c$ and is served only while it holds one. An arrival that finds a compatible free token claims one, chosen by a randomised assignment rule; otherwise it waits at the end of a central queue as an inactive customer. When a customer leaves, its token passes to the longest-waiting compatible inactive customer, or becomes free if there is none.

The state $x=(T_1,n_1,\dots,T_i,n_i)$ lists the tokens $T_1,\dots,T_i$ held by the active customers in order of arrival and the number $n_j$ of inactive customers that arrived between the holders of $T_j$ and $T_{j+1}$; $(0)$ is the empty state and $\phi(x)=i+\sum_j n_j$. With $\mathcal U(S)=\{c:\mathcal T_c\subseteq S\}$, write $\lambda_{\mathcal U(S)}=\sum_{c\in\mathcal U(S)}\lambda_c$, and let $\lambda_t(S)$ be the rate at which arrivals claim token $t$ when $S$ is the set of busy tokens.

The holder of $T_j$ leaves at rate $\mu_{T_j}(x)=\eta(\phi(x))\,s_j(T_1,\dots,T_j)$ with $s_j\ge0$ and $\eta(n)>0$ for $n\ge 1$; let $k(T_1,\dots,T_i)=\sum_{j\le i}s_j(T_1,\dots,T_j)$, so $\mu(x)=\eta(\phi(x))k(T_1,\dots,T_i)$.

• Condition 1 (assignment condition): $\Pi_\lambda(\{T_1,\dots,T_i\})=\prod_{j=1}^i\lambda_{T_j}(\{T_1,\dots,T_{j-1}\})$ does not depend on the order of $T_1,\dots,T_i$.
• Condition 2 (order-independent condition): $k(T_1,\dots,T_i)$ does not depend on the order of $T_1,\dots,T_i$.

Formalization targets

Goal: Theorem 1 (p. 7)

With $\Pi_k(T_1,\dots,T_i)=\prod_{j=1}^i k(T_1,\dots,T_j)$ and $\alpha_j=\lambda_{\mathcal U(\{T_1,\dots,T_j\})}/k(T_1,\dots,T_j)$, if the series below converges, then

$$\pi(x)=\pi((0))\,\frac{\Pi_\lambda(\{T_1,\dots,T_i\})}{\Pi_k(T_1,\dots,T_i)}\prod_{j=1}^{i}\alpha_j^{n_j}\prod_{j=1}^{\phi(x)}\frac{1}{\eta(j)},\qquad \pi((0))^{-1}=1+\sum_{x\neq(0)}\frac{\Pi_\lambda}{\Pi_k}\prod_j\alpha_j^{n_j}\prod_{j=1}^{\phi(x)}\frac1{\eta(j)},$$

is a probability distribution that satisfies the global balance equations $\pi(x)\sum_y q(x,y)=\sum_y\pi(y)q(y,x)$ of the queue's transition rates $q$.

Milestones

The paper's proof runs through the identities below, listed in attack order: (1), the departure-rate identities (4), (5), (7), the total exit rate $\lambda+\mu(x)$, the explicit form (8)–(9) of the global balance equations, the partial balance equations (12), (13), (14) with the rearrangement of $\Pi_k$ and the telescoping identity (29) from Appendix A, and (9) for the product form.

Significance

The product form gives the stationary law of a multi-class, multi-server system with compatibility constraints, with a normalising constant expressed as an infinite series. The paper derives from it the joint generating function of the numbers of waiting customers per type (Theorem 2), the numbers in system (Theorem 4), and the transforms of time-till-token and sojourn time (Theorems 6, 7), and shows that the heterogeneous M/M/K queue, redundancy with cancel-on-start or cancel-on-completion and a family of matching models are special cases.

The result is proved in the paper; nothing here is open. To our knowledge no part of it has been machine-checked. A formal proof would check the bookkeeping of the transition structure, where the printed text has slips (below), and would give a reusable development of product-form verification by partial balance for queues with order-dependent descriptors.

Difficulty

The algebra of the partial balance equations is long but routine once the predecessors of a state are listed correctly. The difficulty is that list. A departure frees a token that passes to the first compatible waiting customer, so the predecessors of a state are indexed by where the departing customer stood, how the waiting customers were split around it, and whether the token was released or reclaimed. The paper's printed list of reclaiming predecessors, $\mathrm{shift}_{k,n}(x,T_j)$, is stated for $1\le k$ and $k+1<j$, while the balance equations sum over $0\le k\le j-1$. The obvious reading of the printed tuple at $k=j-1$ counts customers twice. A second slip sits in Appendix A, in the rearrangement of $\Pi_k$. A proof that copies the paper's backward formulas into the balance equations proves the wrong identity: the goal is balance for the forward transition rates, from which the predecessor list has to be derived.

Formalization scope

• Types and states. Types and tokens are Fintypes with decidable equality (finitely many tokens, as in Theorem 1). A state is a list of (token, count) pairs with distinct tokens. Infeasible descriptors (a waiting customer that could have claimed a free token) are included; the weights vanish on them.
• Rates. All rates are real numbers. transitions lists the forward transitions of §4.1 with their rates, and rate y x is the total rate from y to x. The reclaim probabilities use $\lambda_{\mathcal U(\{T_1,\dots,T_l\}\setminus\{T_j\})}/\lambda_{\mathcal U(\{T_1,\dots,T_l\})}$ for a customer waiting behind $T_l$. The departure rates are defined by (3), with $s$ taking the prefix $[T_1,\dots,T_j]$.
• Added assumptions, disclosed.
  • Every type has a compatible token ($\mathcal T_c\neq\emptyset$): the descriptor has no place for a customer that can never be served.
  • $k>0$ on non-empty sequences of distinct tokens: the weights divide by $k$.
  • "Stable" is summability of the weights, the reading of §4.4.
• Not stated. Uniqueness of the stationary distribution is not part of the goal. The paper obtains it from irreducibility and a theorem of Foster, and the full state type contains infeasible states outside the irreducible class.
• Corrections. The shift states for $k=0$ and $k=j-1$ and the $\Pi_k$ rearrangement are corrected, as recorded in the items.
• Trivial readings ruled out. The goal is not "the weights satisfy the typed-in equation (8)": it is global balance for the forward rates, with explicit summability so that no unconditional sum is a junk value.
• Infrastructure. The development needs finite sums and products over list prefixes, list surgery (insert, remove, merge portions) and permutation invariance. It reuses the published equilibrium-equation predicate FullBalance. Proofs of any milestone are welcome, and so are general lemmas on partial balance for lists of transitions.

Selected references

• U. Ayesta, T. Bodas, J. L. Dorsman, I. M. Verloop, A token-based central queue with order-independent service rates, arXiv:1902.02137v1, 2019; Operations Research, 2022. https://arxiv.org/abs/1902.02137v1 (the version read for this mission)
• A. E. Krzesinski, Order independent queues, in R. J. Boucherie, N. M. van Dijk (eds.), Queueing Networks, International Series in Operations Research & Management Science 154, Springer, 2011, pp. 85–120 (reference [20] of the paper).
• J. Visschers, I. J. B. F. Adan, G. Weiss, A product form solution to a system with multi-type jobs and multi-type servers, Queueing Systems 70(3), 2012, pp. 269–298 (reference [22]).
• K. Gardner, S. Zbarsky, S. Doroudi, M. Harchol-Balter, E. Hyytiä, A. Scheller-Wolf, Queueing with redundant requests: exact analysis, Queueing Systems 83(3–4), 2016, pp. 227–259 (reference [14]).
• F. G. Foster, On the stochastic matrices associated with certain queuing processes, The Annals of Mathematical Statistics 24(3), 1953, pp. 355–360 (reference [12]; the ergodicity criterion behind uniqueness).