Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Energy-efficiency and emission standards for products such as vehicles and appliances are set by regulators whose jurisdictions overlap a single manufacturer's markets. The best-known case is United States fuel-economy regulation. California has long been allowed to set stricter vehicle standards than the federal government, and the 2019 dispute between California and the federal administration over a single "50-state" standard put the question of split versus unified markets on the policy agenda. A manufacturer facing two different standards can sell two product versions (a split market), sell one version that meets the stricter standard everywhere (a unified market), or withdraw from the stricter market.
Han, Hu and Dawande (Curbing Emissions: Environmental Regulations and Product Offerings Across Markets, Manufacturing & Service Operations Management, 2022) model this as a game between an environmentally concerned regulator, an environmentally agnostic regulator, and a monopolist. They ask when the market splits, and whether negotiation between the regulators can unify a split market and lower total emissions. This mission formalizes their answer for one negotiation format, the exact global standard (§4.1.1), together with the base-model results it rests on. Citations refer to the authors' accepted manuscript of 28 July 2022, including its Online Appendices.
A monopolist sells in two markets of sizes . Regulator sets a minimum efficiency standard for products sold in . Consumers' valuations are uniform on . A consumer with valuation who buys a product of efficiency at price receives , where is the efficiency bonus, and buys when this is positive. Producing efficiency costs per unit plus a fixed setup cost per product.
Regulator maximizes consumer utility in minus . Here is a benchmark efficiency, is the perceived per-unit environmental impact, and the sum runs over both markets. Regulator maximizes consumer utility in only and therefore sets . The total emissions are .
Given , the firm chooses among three strategies: (differentiated products at and ), (one unified product at in both markets), and (one product at , sold in only). Each product is priced at . A base-model outcome is a standard together with a profit-maximizing strategy of the firm, such that cannot do better with another standard paired with any profit-maximizing response.
In the exact-standard negotiation, and agree on one standard for both markets and a transfer from to . Their total utility is (eq. (4)). The disagreement point is the pair of utilities at the split-market base outcome, and the negotiated pair maximizes the Nash product over the feasible pairs that split the gain equally.
Assume condition (1) of Lemma A.1, where is the larger root of an auxiliary quadratic:
Then a split-market base outcome exists. For every such outcome, the negotiation has a Nash bargaining solution, and every solution has standard
The regulators' total utility at strictly exceeds , and total emissions at are strictly lower than at the split-market outcome.
The result. Proposition 3 shows that, whenever the base model predicts a split market under the paper's sufficient condition, two regulators who negotiate an exact global standard with side payments always reach agreement. The agreed standard unifies the market and lowers total emissions. The negotiated standard coincides with the standard a neutral arbitrator would choose. This makes the exact global standard the benchmark against which the paper compares its other negotiation formats (a baseline global standard, and vertical negotiation with the firm). It also qualifies the policy debate: unification through an exact standard requires the stricter regulator to give up its power to exceed the common standard.
Formalizing it. The proofs in Online Appendix C are short computations in which several steps are "straightforward" or "easy to show". In particular, the existence and use of , the comparison between strategies at the regime boundaries, and the truncated branch of Proposition 2 are argued only briefly. A machine-checked development fixes the equilibrium notion, including how ties between strategies are treated, and verifies every inequality. To our knowledge none of these results has been formalized before.
The algebra of each step is elementary, but the base equilibrium is a bilevel object. optimizes over against a firm response that switches between three regimes at and , and 's utility is a different concave quadratic in each regime. Showing that the split outcome sits at requires comparing the maximum over the regime with the maxima over the and regimes. Only the third term of condition (1), through the implicitly defined , controls the comparison. Simply substituting the closed forms of Lemma A.1 into the negotiation does not prove the goal: the goal quantifies over every split-market base outcome, so the characterization of the base equilibrium must actually be established. The emissions comparison also needs a strict inequality. At the emissions in are equal and only changes, and the case must be excluded using condition (1).
All quantities are real numbers in one parameter record , and every statement assumes the standing assumptions of §3: , , , and . The formalization departs from or adds to the page in these places:
A trivializing formalization is ruled out: the goal does not take the disagreement point from Lemma A.1's closed form or compare two formulas. It reads the disagreement point off an arbitrary split-market base outcome, asserts that one exists, and characterizes the negotiated standard through the Nash-product maximization. A sorry-free verification file checks that the goal's hypotheses hold together at a concrete parameter point (, , , , , , ).
The development needs only real algebra: quadratics, square roots and case analysis over three strategies. The lemmas on piecewise-quadratic best responses, and on the reduction of a transferable-utility Nash bargaining problem to total-utility maximization, may be reused for other regulator–firm models. Proofs of any milestone are welcome. Propositions 4 and 5 (baseline global standard, vertical negotiation) and the unified half of Proposition 2 are outside this mission.
Boards and audit committees use formal controls to limit the resources that an executive can divert. Controls can also change the executive's decision: a CEO who values her future reputation may comply when the remaining opportunity to divert is too small. Penno's diversion model puts these two effects in one decision problem. It asks how much costly control the authority should buy when it does not know in advance which CEO type it will draw. The answer depends on the chance of drawing a reputation-sensitive CEO and on the strength of that CEO's career concerns. Penno calls their product tone at the top.
The source for this mission is the May 2019 revision of Penno's SSRN working paper. Its Proposition 1 gives an explicit optimal control level and the corresponding temptation threshold for the high CEO type. The result belongs to a theoretical accounting model; the mission concerns that model's mathematical assertion, rather than an estimate of actual control costs or misconduct.
An authority chooses a formal control level before a CEO sees a temptation . The temptation is uniform on , where . If the CEO diverts resources, the authority loses ; if the CEO complies, it loses none to diversion. The authority also pays the direct cost , with . The control domain is : full control has infinite cost in the paper.
A CEO has type , with . The high type is drawn with probability and the low type with probability . For a CEO of type , diversion gives utility and compliance gives utility , where and . Define . The high type diverts when exceeds her tipping point ; the low type diverts for any positive temptation. The paper assumes so that the high type can divert under some control levels.
Write for the authority's expected loss: the expected amount diverted, averaged over both CEO types and the uniform temptation, plus . When , both types can divert. At and above that boundary the high type never diverts, so only the low type contributes to expected diversion. The definition of in this mission starts from the CEO's utility comparison and integrates the resulting diverted amount. This preserves the decision mechanism underlying the two closed forms in the paper's appendix.
Under the standing model assumptions and the two conditions of Lemma 1, let . Proposition 1 states that the unique optimal control and its high-type tipping point are
Both branches include equality at ; their values agree there. The formal goal states that the displayed control belongs to and has strictly less expected loss than every other admissible control. The paper's printed formula can be negative for sufficiently large , even when Lemma 1 holds. The goal therefore adds the necessary condition , which ensures that the first branch remains an admissible control.
The milestone list follows the model's tipping point (5), the two expected-loss formulas, the convexity and increasing-loss assertions of Lemma 1, and the appendix's first-order and branch-threshold equations. These are source claims used to identify the optimizer, with their original indices and page provenance.
The result describes when stronger reputational incentives accompany more formal control and when they allow the authority to reduce it. The threshold separates an interior solution, where the high type can still divert at sufficiently large temptations, from a boundary solution that keeps the high type compliant throughout the support of . The accompanying expression for makes the behavioral meaning of each branch explicit. Penno uses the result to discuss the relation between tone at the top and formal control in the basic diversion model.
The paper supplies an analytic proof. This mission seeks machine-checked proofs of the same optimization claim and of its supporting statements. Its definition of expected loss also provides a small reusable example of a two-type decision model with a choice-dependent threshold inside an integral. The mathematical result is known from the paper; its Lean proof remains the work of the mission.
A direct optimization of alone misses the expected diversion term, while treating the high type as always compliant misses the change of behavior at . The loss is piecewise because the high type's tipping point can move past the upper end of the temptation interval. A complete argument must establish the two losses from the utility-based diversion rule, control their behavior on the correct intervals, and compare the candidate in the first interval with their shared boundary. The value also needs separate attention: ordinary real division assigns a value, whereas the paper assigns infinite cost to full control.
Lean uses real parameters bundled in Params, together with the standing inequalities of §3. It represents uniform temptation by an interval integral of the diverted amount with density . The CEO diverts exactly when her diversion utility is strictly greater than her compliance utility. At equality, the formal model takes compliance; that single threshold point has no effect on the integral. The high type's tipping point is the unconstrained value , which can exceed even though realized temptations cannot.
All optimization statements use . This agrees with the source convention and avoids treating Lean's real division by zero as a finite control cost. The added inequality is disclosed in the goal and is needed only to keep the printed interior formula nonnegative. There is no assumption that is nonnegative: the source only requires . The first part of Lemma 1 is strict convexity; its second part is expressed as strict increase, as stated in the appendix proof.
The development needs Mathlib's interval integrals, real square root, and real convexity and monotonicity predicates. Contributions that establish the integral closed forms, the behavior of the two loss regions, and the global optimality claim are within scope. A definition that merely hard-codes the appendix's closed forms as , or a goal about an unconstrained control, would lose the CEO choice and the authority's actual feasible set.
Blockchain platforms and decentralized autonomous organizations take governance decisions by token-weighted voting: an account's influence grows with the governance tokens it stakes. Two problems are associated with this design (Buterin 2021). The first is plutocracy: holders of many tokens control decisions. The second is the Sybil attack (Douceur 2002): accounts are pseudonymous, so one person can split her tokens over many identities. A rule that dampens the influence of large stakes — for example votes proportional to the square root of tokens — invites exactly this splitting, because the dampening is undone by holding many small stakes.
Mohan, Khezr and Berg (SSRN 4259599; Management Science 2024, doi:10.1287/mnsc.2023.01536) set up a model in which votes depend on two resources, staked tokens and time commitment. They characterize Sybil resistance (Theorem 1), show that token weighting alone cannot be both plutocracy- and Sybil-resistant (Theorem 2, the Plutocracy–Sybil dilemma), and propose bond voting, in which votes are bought with voting bonds that lock tokens until maturity. This mission formalizes the paper's main positive result: bond voting is robustly v-implementable (Proposition 2).
A platform fixes a maximal commitment horizon . A vote function turns a stake of tokens locked for units of time into votes, with (Definition 1). It values commitment if , and has non-increasing influence of tokens if and , for all and (Definitions 2, 3).
An agent with budget and payoff function chooses . A Sybil attack with identities assigns stakes and commitments . It is feasible if and every , and profitable if its payoff strictly exceeds what the agent obtains as a single entity (Definition 5). A payoff function is Sybil resistant if no budget admits a feasible and profitable attack (Definition 6), and a mechanism is robustly v-implementable if its vote function values commitment, has non-increasing influence of tokens, and is Sybil resistant (Definition 7).
Bond voting. The platform sets a voting bond rate . A -bond costs tokens, returns them at maturity, and carries one vote, so a budget buys votes. An agent of type — marginal pivotality , value of the policy, outside return on her tokens — receives benefit and bears the opportunity cost , so for
Agent types are admissible when and .
For every rate and horizon ,
The goal quantifies over every admissible agent type and every budget, and leaves and free.
The result. Proposition 2 shows that a second voting resource, time, can be added to token voting without reopening the Sybil problem: bond votes are linear in tokens, so splitting across identities earns nothing, while voters with a low opportunity cost of locking tokens, or a strong stake in the outcome, gain influence through longer commitments. Together with Theorem 2, which shows that token weighting alone cannot dampen large holdings without inviting Sybil attacks, it is the paper's case for bond voting as a governance mechanism.
Formalizing it. The result is proved on paper; it has no machine-checked proof. Formalization adds two things beyond a check. First, it fixes the definitions the paper leaves implicit: the payoff of a multi-identity attack, and which single-entity commitment a profitable attack must beat. Second, it states Proposition 1 precisely: the printed third case of equation (6) ( when ) has no maximizer, because the payoff tends to as but is at . The goal is stated so that it remains true for those agent types.
The mathematics is elementary real analysis; the difficulty is in the definitions. The naive reading of Definition 5(c) compares an attack with the agent's payoff at a fixed commitment . Under that reading the "if" half of Theorem 1 fails: an agent with a suboptimal gains by moving her whole budget to one identity with a better commitment. Comparing with the formula instead fails in the third case of (6). The statement holds when the attack must beat every commitment the agent could choose herself, and proving it then requires handling agent types with no optimal commitment, where Proposition 1 cannot be invoked. Discontinuity of at also rules out arguments that take a maximum over the compact interval .
Everything is real-valued (ℝ), with Real.exp and Real.log. Identities are indexed by Fin M; (no identities) and identities with zero stake are allowed. Derivatives in Definitions 2–3 are encoded with HasDerivAt witnesses, not with deriv, so a non-differentiable function cannot satisfy them by default values. The payoff of an attack is the sum of the identities' payoffs, as computed in the paper's proofs (pp. 16, 25). An attack is profitable only if it beats every single-entity commitment , including (not voting). Bond votes and payoffs are at , as the paper imposes. The hypothesis is added: the paper never states the sign of , and Definition 2 fails without it.
Fixing the single entity's commitment to , or proving Sybil resistance only for agent types covered by Proposition 1 cases 1–2, would be a trivializing formalization of the goal; the goal quantifies over all admissible types and all single-entity commitments.
Theorem 1 is stated "given Assumptions 1 and 2" for mechanisms with non-increasing influence of tokens; milestone 4 drops these hypotheses because its proof uses only linearity and the boundary conditions. Not formalized: Theorem 1's "only if" direction (its proof uses a fixed single-entity commitment and equates nonlinearity with strict concavity), Theorem 2 and Corollaries 1–4, Remarks 1–4, Proposition 3, and the numerical sensitivity analysis of §3.3. All definitions live in one file in the namespace BondVoting.Sybil; the attack and resistance definitions are stated for an arbitrary payoff function and can be reused for other voting rules, such as quadratic voting.
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 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.
Eleven items: three published definition bundles attached as references, seven milestone theorem drafts, and the goal theorem.
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.
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).
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.
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 using the same definitions and quantifiers.
A total Boolean function assigns an output bit to every input of bits:
For an input and a coordinate set , let denote the input obtained by flipping precisely the coordinates in . The sensitivity at an input counts the individual coordinates whose flips change the output:
The block sensitivity at an input, denoted , is the largest number of pairwise disjoint nonempty coordinate sets such that flipping any one of them changes the output at . The sets are tested separately, always starting from the same input. The corresponding global measures are
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.
For every real and every integer , establish the existence of a dimension and a total Boolean function with
The campaign predicate SensitivityCampaign.AchievesExponent (2.075 : ℝ) states this exact proposition. The decimal is interpreted exactly, as , rather than as an approximate floating-point value. The function and dimension may depend on both the exponent loss and the requested threshold .
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.
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.
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.
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.
f80a3f37-72fa-4d56-a094-3e4d351764f3. The present development reuses its foundation, including its earlier source credits.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.
The unknown state is either or . An organic message matches the state with probability . A fraction of all messages consists of misinformation. Its split is the fraction of misinformation advocating ; has distribution with density . Agents start with heterogeneous prior probabilities of state , distributed according to a continuous law . 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 and (§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 : the -average of the two face-value posteriors, weighted by the fractions of and 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 weighs these two narratives according to their densities under and the agent's prior (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 when a positive -mass of agents favors the wrong state; for DeGroot agents, who share a consensus, this is a single belief comparison. Write and for the -probabilities of Bayesian and DeGroot mislearning. The paper studies both true states; the formulas for mirror those for .
The main target is Theorem 1, p. 10. For every , set
For every continuous symmetric prior law on and every split law supplied by a density, the goal compares both states separately:
The first comparison is non-strict because both mislearning probabilities can be zero, although the preprint uses the word “lower.” The value of 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.
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.
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 (Lemma 2 and proof, p. 19).
Lean uses the paper's large-population formulas directly: is an integral over , and 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. is a probability measure concentrated on with no atoms. is given by a measurable nonnegative real density whose integral is one and whose support lies in . 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 under .
The formalized regime has so the cutoffs involving division by are defined as intended; the paper's misinformation-free case is an example outside this theorem. A belief of exactly counts as wrong, matching the weak cutoff inequalities. Mislearning for Bayesian society requires a positive -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 -mass; pointwise Bayesian milestones restrict to the support.
The model defines mislearning from posterior beliefs and the law of , 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 where the theorem needs them; the main comparison does not fix arbitrary smaller support intervals.
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.
There are symmetric suppliers, each with marginal cost . At a common retail price in an open positive interval , the demand for one product is and falls with price. Its demand sensitivity is
The paper assumes that , that has slope less than one, and that . These are the symmetric-price forms of its demand conditions A1, A3, and A4. The model also uses an aggregate diversion ratio : the fraction of the own-product demand response diverted to other suppliers. Under A1, . Hu, Zheng, and Pan, §§3.1–3.2, pp. 7–9.
Let be own-brand pass-through and for be cross-brand pass-through. The total response is . The suppliers' conduct parameters under wholesale and agency selling are respectively
The wholesale retail price and agency retail price are any solutions, in , of the two equations of Lemma 1 after the retailer's marginal cost is normalized to zero. The corresponding wholesale price is , and the agency commission rate is . The profits come from the respective wholesale and agency contract objectives. Finally, §5 defines
These are the quantities in Proposition 2. Hu, Zheng, and Pan, Lemma 1, p. 11; §5, p. 13.
For every pair of equilibrium prices satisfying Lemma 1's equations, Proposition 2(i) asserts that implies
The milestone list includes Proposition 1's comparison of and , 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.
When , the price part of Proposition 2(ii) gives the exact criterion
The milestone for this case is the authors' rewrite of condition (8) in terms of . 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.
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 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.
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 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.
Lean uses real-valued demand on an open, order-connected interval and a natural-number supplier count , cast to the reals in formulas. Derivatives are ordinary derivatives on . The smoothness assumption is there because A3 differentiates an expression containing . Positive demand is explicit; A1 requires . The strict bound follows from the strict total-demand decrease in A1, although the paper prints the weaker interval . The expressions divide only where their denominators are positive: , , and by A3. The paper uses in its proof, so that bound is also explicit. The retailer's marginal cost is fixed to 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 ; 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.
Many quantum information tasks use inputs of the form , 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 to - via their extremal points. Operationally, each extremal quantum channel factors as unitary Schur sampling an irrep-level unitary-equivariant quantum channel 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 . 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.
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.
20 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
33 results of the paper are not stated yet, because the library lacks an interface they need:
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 such moments thus becomes a dimension-free truncated moment problem, which we solve in closed form for and relax to a semidefinite program of size for arbitrary . The dual solutions are polynomial minorants of on , and two explicit families, binomial and -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.
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.
4 results of the paper are not stated yet, because the library lacks an interface they need:
This is a continuation of the expository article \cite{krp} with some new remarks. Let denote the set of all Gaussian states in the complex Hilbert space the convex set of all momentum and position covariance matrices of order in Gaussian states and let be the group of all unitary operators in conjugations by which leave invariant. Here we prove the following results. is a closed convex set for which a matrix is an extreme point if and only if for some in the symplectic group Every element in is of the form for some in Every Gaussian state in can be purified to a Gaussian state in Any element in the group is of the form where is a complex scalar of modulus unity, is the Weyl operator corresponding to and 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
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.
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.
7 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
32 results of the paper are not stated yet, because the library lacks an interface they need:
This paper describes a formalization of discrete real closed fields in the Coq proof assistant. This abstract structure captures for instance the theory of real algebraic numbers, a decidable subset of real numbers with good algorithmic properties. The theory of real algebraic numbers and more generally of semi-algebraic varieties is at the core of a number of effective methods in real analysis, including decision procedures for non linear arithmetic or optimization methods for real valued functions. After defining an abstract structure of discrete real closed field and the elementary theory of real roots of polynomials, we describe the formalization of an algebraic proof of quantifier elimination based on pseudo-remainder sequences following the standard computer algebra literature on the topic. This formalization covers a large part of the theory which underlies the efficient algorithms implemented in practice in computer algebra. The success of this work paves the way for formal certification of these efficient methods.
This mission is the statement-level formalization of Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination (arXiv:1201.3731v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
29 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §3.2, Lemma sgp_right_scale (§3.2, Lemma sgp_right_scale, PDF p. 12). 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.
12 results of the paper are not stated yet, because the library lacks an interface they need:
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.
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.
20 results of the paper are not stated yet, because the library lacks an interface they need:
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.
A firm has a unit continuum of shares. There are skilled and unskilled activist funds; each holds one block of size and cash , and . A block consists of a fraction of the fund's own capital and of delegated capital, on which the fund earns a fee . The difficulty of changing policy lies in with and is public. Only skilled funds can engage, each at cost . If funds engage, engagement succeeds iff ; the firm is then worth , otherwise . Write and let be the least natural number with .
A skilled fund's payoff is , where is its reinvestment return, its proprietary fraction and the value of the delegated capital it holds at the end. Three games differ only in and :
The fee value of an engager's capital when exactly funds engage and succeed is (Definition 5)
For each the skilled funds play a finite simultaneous game, the -subgame. A maximal success equilibrium (Definition 1) picks, for every , a Nash equilibrium of the -subgame whose probability of successful engagement is maximal among all its Nash equilibria, mixed ones included.
With , for every :
the first range is always non-empty, and the second is non-empty for some when . "Succeeds" means that every maximal success equilibrium of the flow game succeeds with probability one at (and one exists); "cannot" means every Nash equilibrium of the comparison game's -subgame has success probability zero.
Propositions 2 and 3 formalize the classical underprovision result and its aggravation by delegation: since , 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 , 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 (, ) and one endpoint in Lemma 2 are made explicit.
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 ; this uses that is strictly decreasing and the endpoint , 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 pure profiles rather than with one pivotal fund. Third, a maximal success equilibrium is a family indexed by , 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.
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 in the reallocation). Actions are Bool, with true = engage. Mixed profiles are weight functions; the success probability sums over the pure profiles. is sInf over ; casts to before subtracting. The proprietary game is the model with the proprietary fraction set to , all else unchanged (p. 15, footnote 14).
Conventions and additions, all disclosed in the items:
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 . Proofs of any milestone are welcome, as are general lemmas on mixed equilibria of binary-action symmetric games.
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.
There is a finite set of customer types and a finite set of tokens. Type- customers arrive in a Poisson process of rate ; . A type- customer can hold only tokens from its compatibility set 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 lists the tokens held by the active customers in order of arrival and the number of inactive customers that arrived between the holders of and ; is the empty state and . With , write , and let be the rate at which arrivals claim token when is the set of busy tokens.
The holder of leaves at rate with and for ; let , so .
With and , if the series below converges, then
is a probability distribution that satisfies the global balance equations of the queue's transition rates .
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 , the explicit form (8)–(9) of the global balance equations, the partial balance equations (12), (13), (14) with the rearrangement of and the telescoping identity (29) from Appendix A, and (9) for the product form.
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.
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, , is stated for and , while the balance equations sum over . The obvious reading of the printed tuple at counts customers twice. A second slip sits in Appendix A, in the rearrangement of . 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.
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.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 for a customer waiting behind . The departure rates are defined by (3), with taking the prefix .FullBalance. Proofs of any milestone are welcome, and so are general lemmas on partial balance for lists of transitions.An entrepreneur developing a venture repeatedly chooses between strategies that differ in speed, risk and cost: a safe, slow approach or a fast, risky one. Wang and Zenios model this as a drift–variance diffusion control problem (SSRN 3667132; published in Operations Research, 2021, doi:10.1287/opre.2021.2171): the controller chooses not only the drift of a Brownian state but also its variance, and pays a running cost for each choice. Earlier models in which a decision maker switches controls as a diffusion evolves, Radner and Shepp (1996) on corporate risk choice and Harrison and Sunar (2015) on multiple modes of learning, describe their optimal policies through numerical procedures; here the controller chooses drift and variance together, the trade-off between moving fast and moving reliably is the object of study, and the optimal policy is in closed form.
The paper's motivating example (p. 10) suggests that the optimal policy might be complicated: use the safe control near to avoid failure, the cheaper risky control in the middle, and the safe control again near to secure the reward. The paper's main result says this never happens.
There are two controls . Control gives drift , volatility (variance ) and costs per unit time. The state follows
on , , and stops on hitting (no payment) or (terminal cost , i.e. a reward ). The entrepreneur minimizes the expected total cost.
Write for the effective drift, for the critical cost (the cost at which control alone breaks even with no noise), and . As in the paper (p. 12), throughout.
A -interval policy (Definition 1) cuts at and uses control on , with . Its value is the function that is continuously differentiable on , satisfies , , and on each piece solves
A policy is optimal if its value lies below the value of every interval policy on .
With :
In words: an optimal policy either uses one control throughout or switches exactly once, and away from the critical point no optimal policy switches more than once.
The result reduces an infinite-dimensional control problem to a two-parameter family of candidates (which control first, and where to switch), and Theorem 2 identifies the optimum explicitly. Downstream, the paper reads managerial conclusions off the region picture: when both controls are inefficient, when to begin with the safe control and when with the risky one (§4, §8).
The theorem is proved in the paper; nothing here is open. No machine-checked version of any part of it is known. The mission produces a checked version of the analytic core: the closed-form value functions, the sign analysis of the switching functions, a one-dimensional comparison principle (the analytic content of the verification lemma), and the correction of the uniqueness half of Theorem 1 at the critical cost point.
The existence half is a long chain of explicit but delicate calculus. The slopes involve terms whose ordering (Lemma 1) is not visible from the formulas, and the switching point of the two-interval policy is the root of a function built from the derivatives of a piecewise exponential solution whose coefficients are ratios of exponential sums. Showing that keep their signs away from requires the sign facts of Lemma 22 in exactly the right region.
The uniqueness half looks immediate (two optimal policies have the same value, which cannot solve two different ODEs on an interval) but is false as printed: at the affine function solves both ODEs, and every interval policy is optimal. The correct statement must exclude that point, and its proof must show that, elsewhere, the optimal value is affine on no interval.
Mathlib has Brownian motion but no stochastic integral or Itô formula, so the problem is stated analytically, in the objects the paper's proofs manipulate. A policy's value is the unique solution of its ODE boundary-value system with pasting; the identity with the expected cost (Dynkin's formula, the second half of Lemma 12) is not formalized, and optimality is over interval policies, to which the paper restricts (p. 8). Conventions: , , , minimization; is the volatility and enters the ODE; is an explicit hypothesis; controls are a two-constructor type, policies are structures carrying , the controls, strictly increasing breakpoints from to and distinct adjacent controls.
Corrections relative to the page: Theorem 1's uniqueness half excludes ; Lemma 22 (204) is stated strictly; Lemmas 9–10 carry the hypotheses of condition (9) that their proofs use; the exclusivity claim of p. 13 is dropped (only exhaustiveness is stated); (73)'s in the control-2 equation is read as .
The encoding cannot be trivialized: the value fixes both boundary values and gluing, so no policy has arbitrarily low "values"; optimality quantifies over policies of every length and all their values at every point of ; and the policy structure forbids empty pieces and repeated adjacent controls, so is the true number of intervals.
Needed infrastructure: elementary real analysis (exponential inequalities, derivatives of explicit functions, the intermediate value theorem), a one-dimensional maximum principle for with piecewise-constant coefficients, and linear independence of . The comparison principle and the interval-policy layer are reusable for other one-dimensional switching problems. Proofs of any milestone are welcome, as is a formal Dynkin link once Mathlib has stochastic integration.
Service systems such as outpatient clinics, surgical suites and diagnostic units book requests one at a time. When a patient calls, the scheduler commits at once to a provider and a day, without knowing who will call next. Each provider has a planned working time per day, which can be stretched by overtime at a cost. Keyvanshokooh, Shi and Van Oyen (MSOM 2019; accepted manuscript SSRN 3352166) study this problem when the arrivals are adversarial, and analyse it by competitive analysis: an online policy is judged by the worst case, over all arrival sequences, of the ratio between its value and the value of an offline planner who knows the whole sequence.
The paper sits in the line of online primal-dual algorithms for packing problems: online b-matching (Kalyanasundaram and Pruhs 2000), AdWords (Mehta, Saberi, Vazirani and Vazirani 2005), ad auctions with budgets (Buchbinder, Jain and Naor 2007) and the general framework of Buchbinder and Naor 2009. In all of these, capacity is a hard limit. Overtime turns capacity into a soft limit with a price, and the algorithm must decide when to start paying it.
There are servers , days and customers , numbered in order of arrival. Server on day has a regular capacity and an overtime budget , and server pays per unit of overtime. Customer needs service time and brings reward at server , normalized so that .
The offline problem (P) chooses and overtime to maximize subject to: each customer is served at most once; ; and . Its optimal value is . The dual (D) of the LP relaxation minimizes subject to , and .
The instance parameters are
together with and .
HOOP-BOT (Algorithm 1) keeps prices (regular capacity, initially ) and (overtime, initially ). Customer is offered the server-date maximizing and is rejected if that value is negative. If it is accepted at , then:
The output may exceed capacity by one customer per threshold. The paper converts it into a feasible solution of value .
With , where
for every instance and every tie-break,
Theorem 1 is the paper's headline result: a worst-case guarantee for online scheduling in which capacity can be expanded at a price. In the proportional case and as , the paper reads it as a ratio of at least , to be compared with the upper bound of its Theorem 2. The guarantee underlies the rolling-horizon policy of §5 and the case study of §6.
The formal statements add three things. They fix the hypotheses: the page leaves , and the choice of implicit. They pin the conversion from almost-feasible to feasible solution, which the paper describes only inside a proof. And they settle the truth of the result. No part of this paper has been formalized before. The technical inequality is shared with the Buchbinder–Jain–Naor mission and is referenced from there.
The obvious argument is the usual primal-dual accounting: bound the dual increase by times the primal increase at every iteration, sum, and lose a factor when the at most two overflowing customers per server-date are dropped. The step that needs care is the first overtime iteration of a server-date. There the regular price has been capped at while the overtime price still has its initial value , so the identity that the per-iteration bound relies on is not yet in force. The initial dual value is also not a sum of per-iteration increments. Any proof of the goal has to deal with both points.
Everything is in ℝ. Indices are Fin n, Fin T and Fin m, with customers in arrival order; and are written customer first. The maxima in (1) are suprema over nonempty finite index sets. Algorithm 1 is defined step by step, exactly as printed (Steps 1–13, initially, the tests , and as printed). Its run is the fold of one step over the customers. The argmax tie-break is a parameter, and statements about the run hold for every selector that returns a maximizer.
Standing assumptions: ; ; ; ; ; (the paper's normalization); and . The page does not state the last one, but divides by , which vanishes at . depends on the whole instance, as it does in the paper.
"Admits competitive ratio " is formalized through Definition 1 and Proposition 4. There is a feasible of (P) with and , differing from in at most two customers per server-date, whose value is at least times the optimal value of (P), taken as the greatest objective value of a feasible solution. A statement about a closed-form allocation, a fixed tie-break or an initialization other than would be a different theorem and is excluded. The goal is posed exactly as printed, and the proposers record a counterexample to it. Lemma 1 and (15) are stated for the Rule (I) recursion along the customers allocated to one server-date, abstracted from the run.
Not formalized: the limit (12); Theorem 2 and Lemma 3 (the upper bound); Proposition 1, which fails as printed at the first overtime iteration; Propositions 3 and 5; and the case study. Welcome contributions include proofs of the milestones and reusable facts about multiplicative price updates.
Many problems in convex optimization, variational inequalities, game theory and signal processing are systems of monotone inclusions coupled by linear operators: several unknowns in different Hilbert spaces, each subject to its own maximally monotone, cocoercive and Lipschitzian operators, and tied together through linear maps and composite terms. Bùi and Combettes (arXiv:2002.06135, Mathematics of Operations Research, 2022) introduce a single model, Problem 1.1, that contains a large part of these formulations and design algorithms for it that are fully split (each operator is used separately, set-valued operators through their resolvents and single-valued ones through forward evaluations), block-iterative (only some blocks are updated at each iteration) and asynchronous (updates may use information computed up to iterations earlier).
The paper places itself after a line of primal-dual splitting methods: Briceño-Arias and Combettes (SIAM J. Optim. 2011, doi:10.1137/10081602x) for a two-operator monotone+skew model, Alotaibi, Combettes and Shahzad (SIAM J. Optim. 2014) for Fejér approximation of a Kuhn–Tucker set, Combettes and Eckstein (Math. Program. B168, 2018) for asynchronous block-iterative primal-dual decomposition, and the projective splitting methods of Johnstone and Eckstein (2020–2021). These earlier methods work in the primal-dual space . The new idea is to reformulate the problem as finding a zero of a saddle operator on a larger space and to approximate that zero set from outside by half-spaces.
Let and be finite index sets and let , be real Hilbert spaces, with Hilbert direct sums and . For every and the data are:
The parallel sum of is . Write and . The primal problem (1.1) asks for with
Its set of solutions is . The dual problem (1.2) asks for such that some satisfies and ; its set of solutions is . The Kuhn–Tucker set (2.13) collects the pairs satisfying the first condition at and .
On the saddle operator (2.11) maps to the product of the sets , , and . It splits as (Definition 2.4), where collects the cocoercive operators.
Algorithm 3.4 runs, at iteration , over activated blocks , . For it computes a resolvent step from the delayed iterate ; for it computes , from resolvents of , at the delayed iterate . Blocks that are not activated keep their previous values. From these quantities it forms a half-space containing , measured by a number that involves . If , it moves toward that half-space with relaxation ; otherwise the iterate stays put.
Under Assumptions 3.1–3.3 (step-size ranges tied to , and by (3.1); every block activated at least once in every consecutive iterations; delays at most ), if the dual problem has a solution, then every run of Algorithm 3.4 satisfies
together with the analogous statements for and . There exist and with such that
In attack order:
Theorem 3.5 gives weak convergence of a method that uses each operator of Problem 1.1 separately, needs no inversion of linear operators and no knowledge of , and updates nonempty subsets of blocks subject to the coverage windows and bounded delays of Assumptions 3.2–3.3. It produces primal and dual solutions together. Section 4 of the paper derives from it algorithms for variational inequalities over sums of sets and for multivariate convex minimization with infimal convolutions. The hypothesis is dual solvability. Remark 2.3 shows that primal solvability alone is not enough: there are instances with and .
The theorem is proved in the paper. A formalization adds machine-checked foundations that later work in splitting methods can reuse: the saddle operator and its maximal monotonicity; the Fejér outer-approximation principle in Hilbert space (Lemma A.4, cited by the paper from an encyclopedia entry); and the asynchrony lemma (Lemma A.3). To our knowledge none of these results has been formalized before.
The obvious approach would be to show that Algorithm 3.4 is a Fejér-monotone iteration toward in . That approach fails: for the general Problem 1.1, no half-space separating the current point from can be computed from separate operator evaluations (Remark 2.3(iii)). The algorithm instead targets in the larger space . The link back to , and is Proposition 2.2.
The second difficulty is asynchrony. The half-space at iteration is built from points computed at earlier iterations, with stale step sizes. To show that the weak cluster points are zeros of , one has to control these delays (Lemma A.3) and use the cocoercive and Lipschitzian terms uniformly over the step-size ranges (Lemmas A.1–A.2).
PiLp 2 over finite index types, and is a nested WithLp 2 product, so all norms and inner products are the Hilbert ones (not sup norms).E → Set E. Monotonicity, maximal monotonicity, zer, cocoercivity, resolvents and weak convergence are the published ThreeOpSplitting.Convergence definitions; inverses and sums of set-valued maps are the published DouglasRachfordPPA.GenDR ones.Most technology startups that exit successfully are acquired by incumbents rather than taken public. A founder therefore faces a timing question: sell early, while the company is still an invention that only a few incumbents can evaluate, or wait until the invention has been developed into an innovation that every potential buyer can value, at the risk of failing before that point. Arora, Fosfuri and Rønde (SSRN 3611808, forthcoming in Management Science, 2020) model this choice as a contest between three exit strategies: commit to an early sale, commit to a late sale, or keep both options open. The paper's first main result, Proposition 1, describes which startups choose which strategy as a function of their execution capability and of the cost of seeking early offers.
The question matters to entrepreneurship and innovation economics because the answer is not monotone: the paper finds that keeping options open is chosen by startups of intermediate capability, while both weak and strong startups prefer to commit. Commitment to an early exit can be valuable even when flexibility costs nothing, because flexibility changes how early buyers bid.
A startup has execution capability , its probability of surviving to the late market on its own. It holds resources . Trying the early market costs ; the remaining is spent developing the invention, which realizes the fraction of the late-market value, where is strictly increasing and continuous on with and .
There are buyers in the early market and in the late market, with . Buyer values the startup at : a common component and an idiosyncratic component drawn independently from the uniform law on , with distribution function . Each market is a sealed-bid second-price auction. With bidders, let and be the expected highest and second-highest idiosyncratic draws, computed from the order-statistic distribution functions and and their densities and . A buyer then expects and the seller .
The three exit strategies pay:
The startup's choice maximizes the three profits; on ties it prefers the less time-consuming strategy, so early before late before flexible. Let be the type at which ; it equals .
There exist costs such that
All thresholds except are existential, as on the page, so the goal does not depend on any computed constant.
The milestones follow the paper's own proof, Online Appendix A2:
Proposition 1 is the paper's characterization of exit timing. It explains why some founders publicly commit to an early sale, and it is the input to the paper's welfare analysis (§4), which compares the equilibrium timing with the efficient one in the two polar cases (iii) and (i). Without it, the comparative statics of Proposition 2 and the inefficiency results of Propositions 3 and 4 have no equilibrium to refer to.
The paper proves Proposition 1 on paper only. This mission produces a machine-checked version of the model and its proof. That includes the order-statistic facts for uniform valuations, which are standard (Krishna, Auction Theory, 2010, Appendix C) but which have no closed-form statement on the platform. The appendix's argument relies on "calculations show" steps and on convexity claims stated without proof; checking them in Lean is the main work beyond the paper. The platform holds no formalization of this model or of startup exit timing.
The obvious argument compares three explicit profit functions, but is not explicit: its lower integration limit moves with and has a kink where it leaves . The shape of (flat, then strictly decreasing, then strictly increasing) depends on the sign of an inequality between the ratio evaluated at the moving cutoff and a linear function of , and the paper settles this inequality at by an unstated calculation valid for every and . The comparison at holds uniformly in , and the slope comparison must hold across the kink. Finally, the cost thresholds are defined implicitly, and their order follows only by combining the single crossing in with the monotonicity of .
A tempting shortcut is to define the choice through the thresholds; that would make the goal true by definition and is ruled out (see below).
All quantities are real numbers; are natural numbers with , so the paper's branches are not formalized. ranges over (the paper's ) and over . The standing assumptions are bundled in one predicate. Three choices differ from the printed page and are disclosed in each item:
The tie rule early ≻ late ≻ flexible is the page's "least time consuming" convention.
are Lemma 1's closed forms, linked to the actual order statistics of a product of uniform laws by the theorem lemma_1. and are integrals, so Lemma 3 is a theorem rather than a definition. is eq. (2) with Lemma 4's cutoff; Lemma 4 itself, the early-market bidding equilibrium, is not formalized. The choice is defined from only, never from , or , so the goal cannot hold by unfolding a definition. Proposition 2, Lemma 6, Propositions 3–4 and the Online Appendix extensions A4–A6 are outside this mission.
Contributions are welcome at every level. Particularly reusable are:
Inventory integration (or pooling) serves several markets from one stock instead of one stock per market. Its classical value is statistical: when demands are not perfectly correlated, the pooled demand is relatively less variable, so less safety stock is needed for the same service level. Eppen (Management Science, 1979) quantified this for normal demand, and it is the starting point of the risk-pooling literature.
Retailers who mark down unsold stock face a second effect. Strategic consumers who expect a clearance sale may delay their purchase, and whether they wait depends on how likely they believe a unit will still be available at the low price. Integration changes that availability and therefore changes consumer behavior. Aflaki and Swinney (SSRN 2842182, 2020; Operations Research 69(4), 2021) model this interaction as a rational-expectations game between a firm and its consumers, in the line of Su and Zhang (Management Science, 2008) and Cachon and Swinney (Management Science, 2009). They split the value of integration into an operational part and a behavioral part, and characterize when the behavioral part is positive.
A firm sells one product over two periods: at full price in period 1 and at clearance price in period 2. It orders units at cost before the season, with . Market demand is normal. In the multichannel system each of two identical markets has demand and its own stock. In the integrated system one stock serves , where is the correlation.
Consumers have valuations with density on , distribution and . A unit bought in period 2 is worth , with and , and . Consumers believe a unit is available in period 2 with probability . They buy in period 1 exactly when , where
Given the belief about this threshold, the firm faces period-1 demand and solves a newsvendor problem. Its optimal profit is , with
where and .
The second-period fill rate is expected period-2 sales divided by expected period-2 demand. Period-2 demand is , and period-2 sales are the smaller of that demand and the leftover stock .
An equilibrium (Definition 1) is a triple in which maximizes profit given , , and . Write and for the equilibrium thresholds of the two systems. The behavioral value of integration is the second term of the paper's decomposition (6):
Let , the value of at which changes sign.
The goal asserts only the shape of the answer: the set where the behavioral value is positive is an initial segment, in correlation and in variability. It fixes no formula for the thresholds.
Propositions 1–3 cover consumer thresholds, the newsvendor best response, and existence and uniqueness of the equilibrium with . Equations (8) and (14) give the fixed-point form of the equilibrium fill rate. Three further milestones are the reduction to the coefficient of variation, the deterministic endpoint (, ), and Lemma 1, continuity of a unique fixed point. The last ones are Proposition 5 (i), quasiconcavity of and in and in , and the sign rule that when and when .
The result says when pooling helps through consumer behavior: when markets are not too positively correlated and not too variable. Above either threshold, integration encourages strategic waiting enough to reduce the total value of pooling below its classical operational value. A firm that ignored this effect would overrate integration in highly correlated or highly variable markets.
The formalization adds two things. It makes the equilibrium of a rational-expectations inventory game a checked object. It also records gaps in the printed statements. First, part (iii) and the sign rule on p. 13 need : for the sign of flips the sign of . Second, footnote 4 needs . Third, under the paper's ratio fill rate with normal demand, the equilibrium fill rate can be negative, which affects (8) and (14). The result is proved on paper. To the best of current knowledge, nothing in it has been formalized.
The equilibrium is an implicit fixed point. The fill rate is the solution of (14), in which the demand ratio depends on the fill rate itself, through the threshold valuation. Comparing with means comparing the fixed points of two different equations, one per system.
A direct approach would show that is monotone in or . That fails, because the equilibrium fill rate rises and then falls in variability. Only quasiconcavity holds, and the threshold structure must come from combining quasiconcavity with the behavior at the endpoints, where demand is deterministic. Quasiconcavity of an implicitly defined fixed point needs a second-order argument on (14), which involves Gaussian integrals with variable limits.
Everything is real-valued. The multichannel system is formalized as one market , taken once, since the two markets are identical and the equilibrium is symmetric (Proposition 3). The integrated system is the market given by the law , as in Proposition 2 (ii), not as a bivariate sum. The demand law with standard deviation is the Dirac mass, which is how the deterministic endpoint is stated.
The valuation density is integrable, has total mass one, vanishes off and assigns positive probability to every nonempty interior subinterval. Three conventions and additions are disclosed:
The goal is stated about equilibria of Definition 1 and about the behavioral value. It is not stated about (14), an abstract function of the coefficient of variation, or the sign of . The thresholds range over and , so the uniqueness claim cannot be met by an unconstrained threshold.
A complete development needs Gaussian integrals of piecewise-linear functions, the newsvendor solution for normal demand, fixed-point arguments for monotone maps, and implicit differentiation of parametric integrals. The normal newsvendor and the loss-function identity are reusable well beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Proposition 5 (i) that avoid differentiability assumptions on .
Many planning problems ask for a decision that varies over a time horizon and must satisfy a constraint at every instant, possibly with cumulative effects of past decisions. The applications in the source paper are a maximum-flow problem with time-varying pipeline capacities, a wireless coverage problem for a moving target region, and the approximation of Pareto curves of bi-objective semidefinite programs. Ahmadi and El Khadir (arXiv:1808.03994, Mathematics of Operations Research, 2021) model these as time-varying semidefinite programs (TV-SDPs), a common generalization of semidefinite programming and of the continuous linear programs of Bellman (1953), Tyndall (1965) and Levinson (1966), which are the case of diagonal matrices.
A TV-SDP is an infinite-dimensional problem: its variable is a function. The paper's main message is that, under a strict feasibility assumption, nothing is lost by searching only over polynomial solutions, and that the best polynomial solution of a fixed degree can be computed by an ordinary SDP through sum-of-squares certificates. The first statement, Theorem 4, is what justifies the second as a convergent approximation scheme, and it is the goal of this mission.
Fix integers . Let be the set of measurable functions that are bounded, . The data are polynomial: an objective of univariate polynomials, symmetric matrices with polynomial entries, and symmetric kernels with entries polynomial in . For define the matrix function
A function is feasible if and for almost every . The TV-SDP is
It is strictly feasible if some and satisfy for almost every . A polynomial solution is for polynomials .
The proof uses the mollifying operators , : with the bump for , otherwise, normalized so that ,
applied entrywise to vector- and matrix-valued functions. In Lean these are Ln, Sm, Data, F, Feasible, StrictlyFeasible, obj, opt, polySol, J, cJ, Mv, MvVec and MvMat in the namespace TVSDP.PolyOpt.
If the TV-SDP is strictly feasible, there are polynomial vectors such that every is feasible and
the limit taken in the extended reals, so is included.
The result. Theorem 4 says that the supremum of a strictly feasible TV-SDP over polynomial solutions equals its supremum over all bounded measurable solutions. Combined with the paper's Theorem 6, which computes the best degree- polynomial solution by an SDP, it shows that these SDP values form a nondecreasing sequence of lower bounds converging to . Without it, the polynomial restriction could have a strictly smaller value; Example 1 of the paper shows that this happens when strict feasibility fails, where the unique feasible solution is a step function.
Formalizing it. The result is proved in the paper, not formalized anywhere. A machine-checked proof also has to repair the printed argument: the operator integrates over only and is not normalized near the endpoints ( for ), so three auxiliary statements of §3.1 are false as printed (see Formalization scope), although Theorem 4 itself is true. Any complete proof therefore needs an argument that handles the endpoints, which the formal development would record.
The natural route is "perturb into the strict interior, smooth, approximate by polynomials", and each step preserves feasibility only up to a uniform error, so the margin must survive all three. The difficulty is uniformity on the closed interval: smoothing commutes with only approximately, the Volterra term couples times, and at and the mollifier of Definition 3 loses half its mass. Applying the printed Corollary 1 directly fails at the endpoints. In Lean, a further cost is the bookkeeping between "almost every " for feasibility and "every " for the smoothed and polynomial solutions.
Conventions committed to:
volume.restrict (Set.Icc 0 1)), never Lebesgue measure on .EReal supremum; the matrix inequality is positive semidefiniteness of .Trivializations ruled out: feasibility is a.e. on only, solutions in are bounded, is not a real sSup (which would be on an unbounded set), and polynomial solutions are genuine polynomials evaluated everywhere, not functions that agree with a polynomial almost everywhere.
Deliberately absent: the third sentence of Proposition 1 (uniform convergence for continuous ), Lemma 3(c) and Corollary 1. All three are false for the operator of Definition 3 because of the endpoint effect; for example, Corollary 1 fails for , at . The printed constant on p. 14 has in place of , and with it the Lipschitz display fails; milestone 6 uses the corrected constant. Measurability of is added in Lemma 3(a), where the paper uses it implicitly.
Infrastructure needed: interval mollification of bounded measurable functions, uniform convergence on , the Weierstrass approximation theorem for -valued functions (in Mathlib), and Loewner-order perturbation bounds. The mollifier and the Loewner perturbation lemma are reusable beyond this mission. Contributions of proofs for any milestone, of the missing endpoint-robust smoothing step, and of the paper's Example 1 are welcome.
A factory can respond to uncertain demand by allowing a plant to make more than one product. Those extra capabilities cost money, so the design question is where to place a limited number of plant–product links. The usual measure of a flexible production system is the number of units sold. When products have different contribution margins, however, two designs with the same sales may earn different profits: capacity used for a low-margin product cannot then serve a high-margin one. Wang, Wang and Zhang study this distinction through worst-case demand and show that a particular arrangement of two product classes is optimal within the family of long chains (Wang, Wang and Zhang 2020, §§1 and 4).
The result addresses a concrete design choice. A long chain gives every plant two product capabilities and connects the system in a cycle. If half the products have high margins and half low margins, should the two classes be grouped on that cycle or spread out? The paper's answer is that alternating high- and low-margin products gives at least as good a worst-case score as every other long-chain arrangement, for a broad class of scores.
A flexibility design is a set of arcs from plant to product . Plant has capacity , product has demand and margin , and units of product are made by plant . The maximum profit is the optimum of the finite linear program
Products fall into categories with margins . Write for the products with margin and for their total demand. A deterministic score in the paper's class has the form , with strictly increasing in its profit argument when category totals are fixed. Its robust score is for an uncertainty set of nonnegative demand vectors. This includes maximum profit and scores that subtract a demand-based benchmark from profit (Wang, Wang and Zhang 2020, §2.2).
A set is part-wise independently symmetric when it is a Cartesian product of its category projections and remains unchanged if products are permuted within any category. The perturbation version applies that property to for a fixed centre . Such sets preserve the high/low distinction while treating products within each class interchangeably (Wang, Wang and Zhang 2020, Definitions 2.1–2.2).
In the target system there are plants and products, , with unit plant capacities and exactly products in each of two margin classes . A long chain places the fixed products in any cyclic order and connects each plant to two consecutive products. An alternate long chain places high- and low-margin products alternately. The goal, Theorem 3, says that for every such pair of chains, every part-wise independently symmetric , and every robust score in the class above,
This is the paper's worst-case comparison, rather than a claim about a single demand instance or a single performance measure (Wang, Wang and Zhang 2020, Theorem 3, p. 21).
The paper defines a dual margin group index by an integer program that assigns product dual values from the finite menu , where . The parameter counts how many products in each category receive each nonzero menu value. Its feasible set is . Theorem 1 expresses every robust score in terms of these indices and residual demand vectors; Theorem 2(a) says that index dominance for every implies robust-score dominance. Lemma 2 evaluates the index of an alternate chain in three cases, and Proposition 1 compares it with every long chain (Wang, Wang and Zhang 2020, pp. 17–22). These are the mission's milestones, alongside the profit LP's duality and two cyclic-window statements used in the comparison.
Within balanced, unit-capacity, two-margin long chains, the theorem resolves placement of the high-margin products without choosing one demand distribution or one profit-based robustness score. The dominance holds across the paper's whole class of category-symmetric uncertainty sets and scores. It gives a design rule within that family; it does not claim that an alternate chain beats every possible two-capability graph. The paper separately studies limits of that broader comparison (Wang, Wang and Zhang 2020, §4.3).
The paper proves these results on paper. This mission asks for machine-checked proofs of the stated Lean targets. Its reusable output includes the finite bipartite profit LP, its dual, category-wise demand symmetry, and the DMGI representation. None of the mission's theorems is presented here as already machine-checked.
The LP optimum must be related to a dual optimum whose product variables belong to a small, margin-dependent set. That is stronger than merely invoking an objective-value duality statement. The robust representation then has to account for both a discrete assignment of dual values and the permissible permutations of demand residuals within each product class. The last comparison is combinatorial: a general long chain can have runs of high-margin products, and its relevant cyclic windows must be compared with the alternating chain across every feasible count vector (Wang, Wang and Zhang 2020, Appendix A).
The Lean development represents plants and products by finite index types, real capacities, demands and margins, and a design by a finite set of plant–product pairs. A separate general profit-LP definition is instantiated by the paper's margin-category system. Lean indices start at zero: category is the paper's category , and the added margin level is zero. The production variable is written x j i in Lean for the paper's . Category residuals are enumerated by increasing product index; part-wise symmetry makes that choice immaterial. A long chain uses a permutation of fixed products around a cycle, so the uncertainty set stays attached to the same high- and low-margin categories.
The system requires positive numbers of plants, products and occupied margin categories, nonnegative capacities, and positive strictly increasing margins. The paper treats margins as positive profits but does not state that inequality explicitly. The model also supplies to the DMGI program, matching the dual program and the use of dual feasibility in the paper's proof; equations (4) and (5) omit this line. For the robust minimum, is nonempty, compact and contained in nonnegative demand, and the deterministic score is continuous there. Nonemptiness and compactness are explicit mathematical additions needed for the paper's minimum and minimizer. Every DMGI theorem restricts to . These conditions prevent empty or unbounded real infima from supplying Lean's default zero. The case is included.
Contributions may establish the LP duality, dual extreme-point structure, robust representations, exact alternate-chain index, or cyclic-window comparison. The definitions use finite sums and real suprema and infima; establishing attainment is part of the theorem work.
A customer who is short of time may pay for a better place in a service queue. Unlike resale of a fixed ticket, this transaction changes the waits faced by later customers, and those customers' choices then change the value of the position being sold. Yang, Wang, and Cui study this feedback in an unobservable queue with a firm that repeatedly sells its place to arriving customers. Their single-scalper analysis identifies demand levels at which such a firm enters, rather than assuming that more customer traffic always makes entry more attractive (Yang, Wang, and Cui 2021, §§3–4).
The mission targets a precise claim about that entry decision. Low demand leaves few sales; very high demand forces more customers to balk and limits what a buyer will pay. The result is a possibly empty interval of demand volumes in which the scalper enters. The associated price and revenue results are useful milestones because they describe the economics of that interval using the same customer equilibrium as the entry theorem (Yang, Wang, and Cui 2021, Propositions 2–4).
The service system is an M/M/1 queue: potential customers arrive as a Poisson process at rate , and a single server completes service at exponential rate . Customers cannot observe the queue length or their positions. Every customer values completed service at and has a private delay cost per unit time. In this mission, is uniform on and . A queue-scalping firm may place one scalper in line. Under the head-queueing rule, the scalper can hold the first position without blocking service while waiting to sell it to a customer. After a sale, the scalper returns to the tail. The firm pays cost per unit time for the scalper and charges a nonnegative price per sale (Yang, Wang, and Cui 2021, pp. 5–9, Lemma 1).
Customers use two cutoffs. Customers below join without buying, customers from through join and buy, and customers above balk. The actual throughput is ; the share of joining customers who buy is . A customer with delay cost is indifferent between buying and not buying. A customer at can join and buy, while the corresponding utility is zero if any customers balk. These are the customer-equilibrium equations (1b)–(1d) of the paper, with , , and stable throughput (Yang, Wang, and Cui 2021, pp. 7–9).
Let be a buyer's expected delay and a nonbuyer's expected delay under the head-queueing rule. Their difference is the buyer's delay saving. Optimal revenue is the attained maximum of over nonnegative prices and compatible customer equilibria. If the firm stays out, its profit is zero. If it enters, its best profit is . At equality the model takes the no-entry decision, as in the proof's entry criterion (Yang, Wang, and Cui 2021, equation (1a), Proposition 4 and its Online Appendix proof).
For fixed , , and , Proposition 4 asserts that thresholds exist such that every positive demand volume has an optimal customer-equilibrium revenue and
The interval can be empty. The thresholds depend on the system parameters, rather than on the demand volume being tested (Yang, Wang, and Cui 2021, Proposition 4, p. 12).
Proposition 2 gives the optimal price in the all-join regime and the balking regime , and says that this price is unimodal. Proposition 3 says that optimal revenue is also unimodal, with a unique peak . The Online Appendix identifies the cutoff , reduces the pricing problem to the buying cutoff , gives the revenue expression in each regime, and shows that revenue less cost approaches at both extreme demand levels (Yang, Wang, and Cui 2021, Propositions 2–3, Online Appendix pp. 1–3).
The entry theorem classifies queue demand by the scalper's decision while allowing the equilibrium buying and balking rates to change with price. It explains why a queue with more arrivals can become less attractive to a scalper even though it offers more potential buyers. The price and revenue milestones also distinguish two operational regimes: one in which everyone joins, and one in which joining itself contracts as demand rises (Yang, Wang, and Cui 2021, §§4.1 and 9).
The paper proves these results mathematically; this mission asks for machine-checked proofs of the statements under an explicit model interface. The reusable output includes formulas for the two customer delay classes, a predicate for cutoff-based customer equilibrium, and an attained joint optimization predicate. A formal proof of entry must connect the closed-form revenue analysis to that optimization predicate. At the draft stage, the proposed theorem statements compile with sorry; they are not yet machine-checked proofs.
More arrivals directly create more opportunities to sell a place, but customer behavior also changes the number who join, the fraction who buy, and the price they will pay. Holding any one of these responses fixed gives the wrong entry question. The challenging point is to establish a single rise and fall of optimal revenue across the boundary between the all-join and balking regimes, while keeping the customer equilibrium and the price optimization tied together. The endpoint behavior matters as well: an interval theorem needs no entry at sufficiently low and sufficiently high demand, including the possibility that the entry interval is empty (Yang, Wang, and Cui 2021, Propositions 2–4 and Online Appendix A).
Lean represents as real numbers and the entry decision as either zero or one. Params.Standing records , , and . Proposition 4 additionally assumes ; the Online Appendix uses the negative limit , and at zero cost the high-demand nonentry threshold need not be finite. Statements concerning demand use . The positive cutoff makes the purchase-rate quotient meaningful, and stable throughput keeps the queue-delay denominators positive.
The delay formulas of Lemma 1 are taken as the model's delays; their underlying stationary queueing-process derivation is outside this mission. The uniform CDF is the identity on . The paper's optimization is represented by an attained maximum over prices and customer equilibria, rather than by a supremum of arbitrary real values. The entry goal includes existence of an optimizer at every positive demand, so missing feasible equilibria cannot make the result vacuous. Contributions that establish equilibrium cutoff uniqueness, exact reduction of the pricing problem, price and revenue optimality, and the resulting demand shape are all within scope. The definitions of the equilibrium and optimum can be reused in further analysis of queue position sales under the same rule.
An auditor may need to measure whether a decision rule approves members of one protected group more often than members of another. The decision, the relevant outcome, and useful proxy variables may be observed in a primary dataset, while protected class and the same proxies are observed in a separate auxiliary dataset. There is no record linking the two datasets person by person. Consequently, the two observed distributions do not determine a unique joint distribution, even if they are known without sampling error. Kallus, Mao, and Zhou study what can still be said about such fairness measures from the two marginals alone (arXiv:1906.00285v2, §§2, 4–5).
The issue is relevant whenever protected labels cannot be joined to individual decisions. Proxy methods can estimate group membership, but their errors do not disappear merely because the marginal distributions are known. A set of compatible disparity values makes the uncertainty visible. This mission treats the population result in Proposition 7 of the cited preprint; estimation from finite samples and the paper's empirical case studies are separate topics.
Let decision and true outcome . The protected class has two groups, with conventionally advantaged and disadvantaged. The proxy takes values in a measurable space ; it may be categorical, continuous, or mixed. The primary marginal is , and the auxiliary marginal is . Both share one proxy distribution , as required when they arise from a common population joint law.
For each proxy value , write and . Their decision marginal is . A coupling of two discrete probability vectors is a nonnegative array whose row and column sums equal those vectors. The paper's set contains all measurable conditional joint arrays that couple and at each , together with the fixed . It imposes no additional assumptions on the unknown association of class and outcomes.
The demographic disparity of a compatible joint is . Its partial identification set is
This set lists every disparity that the two observed marginals permit, rather than selecting a particular way to combine them.
For a group , decision , and proxy value , define the Fréchet–Hoeffding weight endpoints
For a class weight function , let . The goal, Proposition 7, is the equality
Equality makes the interval sharp: every compatible joint produces a value inside it, and every value inside it is produced by a compatible joint. The milestones state the finite coupling bounds, the weighted description of the disparity set, the constraints on admissible weights, the numerical bounds, and attainment of both endpoint values. The source is Proposition 1, Propositions 5–7, and the proof of Proposition 7 on pp. 10 and 14–15 of the preprint (arXiv:1906.00285v2).
The theorem gives an exact range for the difference in group approval rates when class and decision are never observed jointly. An interval that excludes zero has an interpretation that does not depend on choosing one compatible joint law. A wide interval identifies uncertainty due to data combination itself, before finite-sample error enters. A single point signals that the observed marginals identify the demographic disparity under these conventions.
Formalizing the known result adds a reusable definition of finite couplings and a precise model of compatible conditional joints over an arbitrary measurable proxy space. The proposition is proved in the paper; the Lean goal and its milestone statements are open formalization targets. The development also records the null-cell and denominator conventions that ordinary probability notation leaves implicit. It does not claim a machine-checked proof of Proposition 7 yet.
The observed data fix the class marginal and the joint decision–outcome marginal, but they do not fix their association within a proxy cell. Bounding one cell of a coupling does not by itself prove that an extreme disparity is simultaneously attainable under all marginal constraints. The true outcome remains in the compatible-joint model even though demographic disparity uses only . When a decision cell has zero probability, a conditional class weight on that cell is undefined, so pointwise weight statements require care. A set inclusion alone would miss the sharpness claim.
The Lean model uses Fin 2 for each binary outcome and a two-constructor type for protected class. It represents the two observed marginals by one probability measure on and measurable, normalized, nonnegative conditional vectors and . The set consists of measurable conditional couplings for every . Conditional probabilities in the candidate joint are ratios of integrals of that joint array. In particular, the denominator of is computed from , not inserted from the auxiliary marginal.
The theorem explicitly assumes and , since conditioning on a group of zero probability is undefined in the paper. The paper's conditional laws are defined almost everywhere; requiring a coupling at every selects a version and does not change the attainable disparities. On a cell with , weight identities and bounds are imposed only when that cell has positive probability; all weighted expectations multiply by the cell probability. The integrands arising from compatible joints and admissible weights are measurable and bounded on a probability space, so their real integrals are genuine expectations.
The identification set is built from compatible joint laws and their conditional disparity. Defining it directly as an interval or as the image of a chosen weight set would erase the content of the target. Finite coupling bounds and conditional-joint modeling can be reused outside demographic disparity. Contributions proving the milestone statements, handling measurable selections, and connecting coupling arrays to probability measures are within scope. Estimation, true-positive and true-negative disparities, and additional assumptions on the joint law are outside this mission.