Motivation

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.

Setting

An authority chooses a formal control level $c$ before a CEO sees a temptation $x$. The temptation is uniform on $[0,\bar x]$, where $\bar x>0$. If the CEO diverts resources, the authority loses $(1-c)x$; if the CEO complies, it loses none to diversion. The authority also pays the direct cost $K(c)=\lambda/(1-c)$, with $\lambda>0$. The control domain is $0\le c<1$: full control has infinite cost in the paper.

A CEO has type $\eta\in\{0,\eta_H\}$, with $\eta_H>0$. The high type is drawn with probability $p\in(0,1)$ and the low type with probability $1-p$. For a CEO of type $\eta$, diversion gives utility $\beta\eta+\gamma(1-c)x$ and compliance gives utility $\eta$, where $\beta<1$ and $0<\gamma<1$. Define $\tau=(1-\beta)\eta_H/\gamma$. The high type diverts when $x$ exceeds her tipping point $x_T(c)=\tau/(1-c)$; the low type diverts for any positive temptation. The paper assumes $\tau<\bar x$ so that the high type can divert under some control levels.

Write $L(c)$ for the authority's expected loss: the expected amount diverted, averaged over both CEO types and the uniform temptation, plus $K(c)$. When $c<1-\tau/\bar x$, 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 $L$ 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.

Formalization targets

Proposition 1: optimal control and tipping point

Under the standing model assumptions and the two conditions of Lemma 1, let $q=\sqrt{2\lambda\bar x/(1+p)}$. Proposition 1 states that the unique optimal control and its high-type tipping point are

Both branches include equality at $q$; their values agree there. The formal goal states that the displayed control belongs to $[0,1)$ and has strictly less expected loss than every other admissible control. The paper's printed formula can be negative for sufficiently large $\lambda$, even when Lemma 1 holds. The goal therefore adds the necessary condition $2\lambda\bar x-p\tau^2\le\bar x^2$, 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.

Significance

The result describes when stronger reputational incentives accompany more formal control and when they allow the authority to reduce it. The threshold $q$ 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 $x$. The accompanying expression for $x_T$ 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.

Difficulty

A direct optimization of $\lambda/(1-c)$ alone misses the expected diversion term, while treating the high type as always compliant misses the change of behavior at $x_T(c)$. 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 $c=1$ also needs separate attention: ordinary real division assigns $\lambda/0$ a value, whereas the paper assigns infinite cost to full control.

Formalization scope

Lean uses real parameters $\bar x,\lambda,p,\beta,\gamma,\eta_H$ bundled in Params, together with the standing inequalities of §3. It represents uniform temptation by an interval integral of the diverted amount with density $1/\bar x$. 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 $\tau/(1-c)$, which can exceed $\bar x$ even though realized temptations cannot.

All optimization statements use $c\in[0,1)$. This agrees with the source convention $K(1)=\infty$ and avoids treating Lean's real division by zero as a finite control cost. The added inequality $2\lambda\bar x-p\tau^2\le\bar x^2$ is disclosed in the goal and is needed only to keep the printed interior formula nonnegative. There is no assumption that $\beta$ is nonnegative: the source only requires $\beta<1$. 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 $L$, or a goal about an unconstrained control, would lose the CEO choice and the authority's actual feasible set.

Selected references

• M. Penno, A Theory of Assurance: Balancing Costly Formal Control with Tone at the Top, SSRN working paper 2876700, revision of May 2019, §§3–4 and Appendix, pp. 6–13, 28–29. SSRN

Motivation

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).

Setting

A platform fixes a maximal commitment horizon $T > 0$. A vote function $v(q, t)$ turns a stake of $q \ge 0$ tokens locked for $t \in [0, T]$ units of time into votes, with $v(q, 0) = v(0, t) = 0$ (Definition 1). It values commitment if $\partial v/\partial t > 0$, and has non-increasing influence of tokens if $\partial v/\partial q > 0$ and $\partial^2 v/\partial q^2 \le 0$, for all $q > 0$ and $t \in (0, T]$ (Definitions 2, 3).

An agent with budget $q > 0$ and payoff function $\pi(q, t)$ chooses $t \in [0, T]$. A Sybil attack with $M$ identities assigns stakes $q_1, \dots, q_M \ge 0$ and commitments $t_1, \dots, t_M$. It is feasible if $\sum_m q_m \le q$ and every $t_m \in (0, T]$, and profitable if its payoff $\sum_m \pi(q_m, t_m)$ 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 $r$. A $t$-bond costs $P_t = e^{-rt}$ tokens, returns them at maturity, and carries one vote, so a budget $q$ buys $V = q/P_t = q e^{rt}$ votes. An agent of type $(\theta, u, r_i)$ — marginal pivotality $\theta$, value $u$ of the policy, outside return $r_i$ on her tokens — receives benefit $|u|\theta V$ and bears the opportunity cost $q(e^{r_i t} - 1)$, so for $t > 0$

Agent types are admissible when $|u|\theta > 1$ and $r_i > r$.

Formalization targets

Goal: Proposition 2

For every rate $r > 0$ and horizon $T > 0$,

The goal quantifies over every admissible agent type and every budget, and leaves $r$ and $T$ free.

Milestones

1. Equation (5): the closed form of $\pi_i$ above.
2. The bond vote function satisfies Definitions 2 and 3.
3. Proposition 1, cases 1–2: if $r_i < \theta|u| r$, the optimal bond length is $t^*_i = T$ when $r_i \le \theta|u| r\, e^{-T(r_i - r)}$, and $t^*_i = \ln(\theta|u| r/r_i)/(r_i - r)$ otherwise; it is the unique maximizer of $\pi_i(q, \cdot)$ on $[0, T]$ and does not depend on $q$.
4. Theorem 1, "if" direction: a payoff linear in $q$ for every $t \in (0, T]$, vanishing at $q = 0$ and at $t = 0$, is Sybil resistant.
5. The Sybil step of the proof of Proposition 2: under the hypotheses of milestone 3, no feasible attack earns more than $\pi_i(q, t^*_i)$.

Significance

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) ($t^*_i = 0$ when $r_i \ge \theta|u| r$) has no maximizer, because the payoff tends to $\theta|u| q > 0$ as $t \to 0^+$ but is $0$ at $t = 0$. The goal is stated so that it remains true for those agent types.

Difficulty

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 $t_i$. Under that reading the "if" half of Theorem 1 fails: an agent with a suboptimal $t_i$ gains by moving her whole budget to one identity with a better commitment. Comparing with the formula $t^*_i$ 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 $\pi_i$ at $t = 0$ also rules out arguments that take a maximum over the compact interval $[0, T]$.

Formalization scope

Everything is real-valued (ℝ), with Real.exp and Real.log. Identities are indexed by Fin M; $M = 0$ (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 $t \in [0, T]$, including $t = 0$ (not voting). Bond votes and payoffs are $0$ at $t = 0$, as the paper imposes. The hypothesis $r > 0$ is added: the paper never states the sign of $r$, and Definition 2 fails without it.

Fixing the single entity's commitment to $t^*_i$, 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.

Selected references

• V. Mohan, P. Khezr, C. Berg, Voting with time commitment for decentralized governance: Bond voting as a Sybil-resistant mechanism, SSRN 4259599 (version of 2024-02-20); Management Science, 2024. https://ssrn.com/abstract=4259599, https://doi.org/10.1287/mnsc.2023.01536
• J. R. Douceur, The Sybil attack, International Workshop on Peer-to-Peer Systems (IPTPS), LNCS 2429, 2002. https://doi.org/10.1007/3-540-45748-8_24
• V. Buterin, Moving beyond coin voting governance, 2021. https://vitalik.ca/general/2021/08/16/voting3.html

Mission: Motives — effective pure motives and the tannakian obstruction

Motivation

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

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

The fragment and its conventions

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

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

Formalization targets

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

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

Significance

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

Difficulty

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

Formalization scope

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

Selected references

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

The quantitative sensitivity question

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

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

Boolean functions and sensitive changes

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

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

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

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

Target: exponent at least 2.075

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

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

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

What this entry establishes

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

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

The difficulty in improving the bound

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

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

Formalization scope and reusable foundations

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

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

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

Selected references and credits

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

Motivation

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

Setting

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

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

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

Formalization targets

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

Formalization targets

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

Formalization targets

Original policy value and the reduced programs

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

Setting

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

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

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