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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
The equivalence principle is one of the foundational methods of setting premiums for life-contingent contracts. It requires that the insurer's expected present value of future benefits equal the expected present value of future net premium income at policy inception. As a result, the expected present value of the net future-loss random variable is zero. Dickson, Hardy and Waters define the net future-loss random variable in Actuarial Mathematics for Life Contingent Risks (2009), §6.4, and state the equivalence principle in §6.5.1, equation (6.1) [1]. Promislow develops the corresponding stochastic premium principle in Fundamentals of Actuarial Mathematics (2015), §15.6.1 [2].
This mission makes that principle a rigorous theorem for a finite-term life assurance financed by level premiums payable annually in advance. It proves that a unique net premium exists when at least one premium is due and nonnegative discount factors are used, and it separately addresses the zero-term case where uniqueness fails. The formal treatment distinguishes realised loss from expected loss, keeps mortality and discounting assumptions explicit, and avoids treating survival-contingent benefits and premiums as independent.
Let represent the probability space, with a measurable natural-valued curtate future lifetime . Let denote the policy term, the annual discount factor, a deterministic death benefit and a level premium.
A unit -year term assurance pays once, at the end of the year of death, if death occurs within the covered term. Its realised benefit present value is , reusing the published definition from Actuarial Mathematics II. In conventional cashflow notation,
This is the discrete term-assurance structure from [3, §3.2.2, equation (3.8)]. Premiums are due at the start of each covered year while the insured remains alive. The realised present value of unit premium income is
The insurer's discounted net future loss at inception is then
The same curtate lifetime determines both premium income and death benefit outgo. No independence assumption is made between these two random variables.
Because the sums are finite, their measurability and integrability can be established from measurability of for any finite real . Linearity of expectation gives
For a positive term and , the first premium at time zero is certain: . All subsequent premium present values are nonnegative. Consequently,
The denominator in the premium formula is therefore strictly positive. Solving the linear expected-loss equation leads to the net level premium
The theorem also proves uniqueness: any real premium satisfying must equal . This is the formal analogue of the equivalence premium calculation in [1, equation (6.1)]. As a related worked example, [1, equation (6.2)] gives a net premium for an endowment contract using the ratio of benefit and premium-annuity values. The mission specialises the general principle to an -year term assurance.
Linearity yields the scaling identity
for any constant . In particular, a zero benefit produces a zero premium under the ratio definition. A nonnegative benefit gives a nonnegative premium when , although the core algebraic scaling theorem does not require positive .
The boundary is deliberately distinct. Neither a term-assurance benefit nor a premium can occur, so . Every quoted level premium has zero expected loss in this empty contract, and uniqueness does not follow. The ratio definition is therefore paired with explicit theorem hypotheses rather than falsely suggesting a unique zero-term premium.
At and , the certain initial premium remains payable at inception, while all covered death benefits are paid at strictly positive times and have zero discounted value. The net premium is zero. At , all payment sums remain finite and integrable for fixed , so no artificial upper bound is needed for these finite-term results.
The mission introduces three definitions: the realised finite premium annuity-due present value, the realised term-policy loss, and the equivalence net premium. Supporting theorems establish the initial premium lower bound, measurability and integrability, positivity of the expected premium annuity, linearity of expected loss, existence and uniqueness of the equivalence premium, benefit scaling, and the zero-term and zero-discount boundaries. The capstone combines positivity, zero expected loss, uniqueness and benefit scaling.
The only previously published actuarial definition imported is the -year term-assurance present value from Mission II. The mathematical arguments use finite sums and integration under a probability measure, rather than relying on unproved statements from other draft missions. All declarations in this owner Draft are mathematical proof targets. Their presence in a proposal does not mean that their proofs have been accepted.
Gerber [4, §5.3.1] independently develops annual-premium term insurance, including its realised loss and the net premium equations (5.3.9)–(5.3.11). Those results corroborate the payment timing and the equivalence-premium construction adopted here.
[1] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Cambridge University Press, book DOI 10.1017/CBO9780511800146. See §6.4, The present value of future loss random variable, and §6.5.1, Net premiums, particularly equations (6.1)–(6.2).
[2] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, ISBN 9781118782460. See §15.6.1, The equivalence principle, and §15.6, The stochastic approach to premiums.
[3] Open Actuarial Textbooks Project, Life Contingencies, Chapter 3, Basic Life Contingent Benefits, §3.2.2, equation (3.8), finite term assurance.
[4] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 5, Net Premiums, particularly §5.3.1, equations (5.3.9)–(5.3.11), on finite term insurance and net annual premiums.
Whole-life assurance and a whole-life annuity-due are two fundamental life-contingent contracts. The assurance provides one unit of benefit at the end of the year of death, whereas the annuity-due provides one unit at the start of each year that the life is still eligible for payment, including time zero. Under a constant positive effective annual interest rate, their realised present values satisfy an exact finite-geometric-series identity. This provides an unusually direct connection between insurance benefits, annuity values and the distribution of curtate future lifetime. The relationship and its expected-value and variance consequences are stated in Life Contingencies, Chapter 3, equations (3.13)–(3.14) [1].
This mission formally develops that equivalence in Lean, starting from the individual cashflows and ending with a capstone theorem that combines the pointwise, expectation and variance results. It also isolates the assumptions needed for these results, supplies reusable bounds and integrability lemmas, and treats the zero-interest boundary separately. Related treatments of whole-life insurance and life annuities are available in the actuarial textbooks of Promislow [2] and Dickson, Hardy and Waters [3]. The mission's declarations are proposed proof obligations, not claims that every theorem has already been proved.
Let be the natural-valued curtate future lifetime of the insured life. In outcome , death occurs during policy year . Let be a flat, deterministic annual effective interest rate and define
The unit whole-life assurance, payable at the end of the year of death, has realised present value
This is the assurance contract defined in [1, §3.2.1, equation (3.7)]. The unit whole-life annuity-due makes payments at dates and therefore has realised present value
The annuity cashflow and the flat-interest specialisation are discussed in [1, §3.3.1, equations (3.11) and (3.13)]. The difference in timing is essential: the assurance payment occurs at , one year after the last annuity-due payment at .
For , the finite geometric sum gives
Equivalently, writing for the annual effective rate of discount,
These are pathwise statements. They hold for every realised natural-valued lifetime and require no assumptions about a mortality law or independence between annual survival events. They formalise the finite-series relationship in [1, equation (3.13)], rather than relying on an approximation or a selected life table.
Now let be a probability measure on and suppose that is measurable. The assumption implies , and the realised values obey
These deterministic bounds establish integrability, including the required second moments, even where has unbounded support across outcomes. Taking expectations of the pointwise identity yields
If and denote the corresponding actuarial values for a life aged , then
Translation by a constant leaves variance unchanged, and scaling multiplies variance by the square of the factor. Thus
The EPV and variance identities are stated in [1, equation (3.14)]. In particular, the variance factor is squared. No independence assumption is imposed: the assurance and annuity values are functions of the same lifetime, and the variance identity follows from their exact affine relationship.
At zero interest, , the whole-life annuity-due has realised value
This is a separate pointwise theorem. The expression is undefined at , and an arbitrary distribution of need not give a finite undiscounted expected payment count or a finite variance. An expectation theorem at zero interest would require a suitable first-moment assumption on , while a finite variance requires a second moment.
The simple assurance–annuity equivalence also relies on a flat deterministic interest basis. Under a non-flat yield curve the discounted cashflow series has varying discount factors and the same fixed geometric multiplier does not generally exist. The source expressly makes this limitation in [1, §3.3.1].
The mission adds one definition, the whole-life assurance realised present value, together with eleven supporting theorems and one capstone. The supporting graph establishes discount-factor positivity, the finite geometric sum, assurance positivity, the pointwise and unit identities, a boundedness lemma, integrability of both contracts, and their expected-value and variance relationships. A separate theorem handles zero interest. The capstone combines the key pathwise identity, expected-value relation, variance scaling and unit identity.
The only imported published actuarial definition is the existing whole-life annuity-due present-value definition from the earlier mission. The assurance definition is introduced here. The proposed proofs should use the appropriate finite-sum and probability-measure results from the pinned Mathlib, and no unproved theorem from another actuarial mission should be treated as an available proof dependency. These formal dependencies are distinct from the published textbook references below.
[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal results: §3.3.1, equations (3.13)–(3.14), on the flat-interest annuity identity, EPV and variance. Assurance definition: §3.2.1, equation (3.7). Whole-life annuities: §3.3.1, equations (3.11)–(3.12).
[2] Promislow, S. David (2010), Fundamentals of Actuarial Mathematics, Wiley. Publisher book record, particularly Chapters 4, Life Annuities, and 5, Life Insurance. This provides wider actuarial background rather than an attribution of equations (3.13)–(3.14) to Promislow.
[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, particularly Chapters 4, Insurance Benefits, 5, Annuities, and 12, Yield Curves and Non-Diversifiable Risk. These chapters provide context for contract valuation and the distinction between flat and varying interest rates.
A whole-life annuity provides payments contingent on the annuitant remaining alive. A guaranteed life annuity adds a minimum number of payments, irrespective of early death. This alters the insurer's cashflows, since payments during the guarantee period are certain and subsequent payments depend on survival. It is an important contract structure for retirement income and provides a natural bridge between annuities certain, whole-life annuities and deferred life annuities. The payment definitions and expected present values are given in the Open Actuarial Textbooks Project's Life Contingencies, Chapter 3, §3.3.4, equations (3.19) and (3.20) [1]. Guaranteed payments are also covered within the broader treatments of life annuities in [2] and [3].
The objective of this mission is to formalise both annuities payable in advance (due) and annuities payable in arrears (immediate), including their exact cashflow decompositions, expected values and variances. It develops the mathematical justification for infinite survival-weighted sums when the distribution of lifetime is not bounded above. These are formal theorem targets to be proved, rather than results already established merely by publishing the statements.
Let be curtate future lifetime, where is the number of complete future years lived in outcome . Let be the number of guaranteed annual payments and let be a constant per-period discount factor. Each payment has unit amount, and an empty sum has value zero.
For an annuity-due, payments occur at times . The first payments at times are certain. Additional payments occur at times , if any.
For an annuity-immediate, payments occur at times . The first payments at times are certain. Additional payments occur at times , if any. The separate timing conventions are essential to the guaranteed-period boundary cases.
The guaranteed annuity-due has realised present value
For an annuity-immediate, the corresponding identity is
Here is the deterministic annuity-certain prefix and is the survival-dependent deferred continuation. The equations reproduce the underlying payment timing of [1, equations (3.19)–(3.20)]. They also connect to the deferred-annuity formulas in [1, equations (3.17)–(3.18)]. Additional pointwise theorems express each guaranteed value as its corresponding whole-life value plus the extra payments required when death occurs during the guarantee.
Let be a probability measure and assume that is measurable. For the analytical theorems, impose . Write . The expected present values are
and
The fixed prefix and survival-weighted tail are those in the guaranteed-annuity textbook formulas [1]. A formal proof must establish measurability and integrability and justify taking expectation through the infinite sum. The geometric bound supplied by makes these conclusions possible for a natural-valued lifetime distribution with unbounded support. No maximum attainable lifetime is assumed.
Since and are deterministic, adding them changes the expected values but does not change the variances:
These variance equalities are derived theorems, based on translation invariance of variance, rather than separate numbered statements in §3.3.4. The general survival-cashflow moment framework in [1, §3.1.1, equations (3.3), (3.5)–(3.6)] supplies background. No independence assumption between annual survival events is introduced.
When , both guaranteed annuities reduce to their corresponding whole-life annuities. When , the due annuity can still pay at time , while the immediate deferred continuation is empty and the guaranteed immediate payments remain. When , the due contract has its time-zero payment, and an immediate contract with still pays the certain instalments.
The finite realised-value identities hold algebraically for every real , including zero, one and negative values. The stated integrability, infinite expected-value and variance theorems deliberately use . In particular, an arbitrary undiscounted lifetime distribution need not have a finite expected payment count.
The mission introduces four definitions, fourteen supporting theorems and one capstone. The intended proof path establishes cashflow decompositions and zero-guarantee identities, develops geometric bounds and measurable survival events, proves the expected-value and variance relations, and then assembles the capstone from the supporting results.
The formal dependency graph reuses six published Prove2Me declarations: the curtate-survival event and its measurability theorem, together with whole-life and deferred present-value definitions for due and immediate annuities. These are technical dependencies, distinct from the bibliographic sources below. An unproved theorem from an earlier mission is not treated as an available proof dependency.
[1] Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, Basic Life Contingent Benefits. Principal source: §3.3.4, equations (3.19)–(3.20). Related foundations: §3.3.1 (3.11)–(3.12), §3.3.3 (3.17)–(3.18), and §3.1.1 (3.3), (3.5)–(3.6). The explanatory sentence after (3.20) calls the contract deferred, although the section heading and displayed expressions describe a guaranteed annuity.
[2] Promislow, S. David (2010), “Life Annuities”, Chapter 4 of Fundamentals of Actuarial Mathematics, Wiley, DOI: 10.1002/9781119971528.ch4. The chapter's published summary includes guaranteed payments.
[3] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2019), Actuarial Mathematics for Life Contingent Risks, third edition, Cambridge University Press, Chapter 5, Annuities. General context for life-annuity valuation.
Whole-life and deferred life annuities extend survival-contingent payments beyond a fixed policy term. A whole-life annuity may pay on each eligible anniversary until death, while a deferred annuity begins after a specified waiting period. Both are standard components of pension and life-contingency valuation.
Actuarial Mathematics I established how to value finite cashflows. Missions III and IV provide curtate survival events and temporary annuity schedules. This mission develops the infinite-horizon valuation step: it justifies the lifetime payment series and its expected present value, including the conditions under which expectation can be exchanged with the discounted survival series.
Let be a probability space and let be a measurable curtate future lifetime. Define the survival event at time by
For expected present value statements, assume a deterministic annual discount factor satisfying
This condition provides a geometric bound on the payments and justifies exchanging expectation with the discounted survival series. No particular life table or independence between survival dates is assumed, and need not have a finite upper bound.
With unit payments in advance, a life with realised curtate lifetime receives a payment at time zero and at each subsequent beginning-of-year date through time . Its present value can be written
Its expected present value, given by equation (3.11), is
A whole-life annuity in arrears pays at times , with no payment at time zero:
Equation (3.12) gives its expected present value:
The payment in advance at time zero is certain, and the remaining payments match the arrears stream. Thus their pointwise and expected values satisfy
For a deferral period , a deferred annuity in advance has its first possible payment at time , with no payments before then. Equation (3.17) gives its indicator representation:
and its expected present value is
A deferred annuity in arrears starts at time and requires survival to that date. Equation (3.18) gives
with expected present value
The timing conditions matter. If , there is a due payment at time , but no immediate payment at time . When , each deferred annuity is its corresponding whole-life annuity.
The discounted cashflows in equations (3.17) and (3.18) are the corresponding whole-life streams with the first potential payment dates removed. Pointwise, this gives
and
Taking expectations gives the source's deferred-annuity valuation differences: each deferred annuity's expected present value is the corresponding whole-life expected present value less that of the temporary annuity.
The finite prefix sums reproduce the temporary-annuity schedules from Mission IV without importing its unpublished declarations. Mission IV remains a Draft, so its new theorems are not available as published imports. The two published curtate survival results from Mission III can be used.
The four new definitions use a finite payment sum for each realised natural-valued lifetime. Each realised cashflow therefore has finite support, even when the possible lifetimes are unbounded. The milestones connect these finite realised sums with infinite survival-indicator series, prove the deferred and initial-payment decompositions, establish integrability under the geometric discount condition, and derive four infinite expected-value formulas.
The capstone combines these formulas and decompositions for the same probability measure, curtate lifetime, discount factor and deferral period. The measure need not arise from a particular mortality model.
The condition applies to the expected present value claims. Pointwise present value identities hold for any real , since each realised natural-valued lifetime is finite and so produces only finitely many payments. At , an arbitrary lifetime distribution can have infinite expectation, so finite expected values cannot be assumed. The condition used here is sufficient; it is not claimed to be the sharpest possible condition under the source's financial discount assumptions.
The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3 §3.3.1 equations (3.11)–(3.12) and §3.3.3 equations (3.17)–(3.18). The temporary prefixes are the payment schedules from §3.3.2 equations (3.15)–(3.16), and the general expectation-of-cashflows step is equation (3.3).
This mission covers whole-life and deferred annuities. Guaranteed-period benefits, flat-interest assurance–annuity equivalence and continuous-time intensity-based valuations are separate later projects.
A life annuity pays a series of amounts while its recipient survives. A term assurance pays at most once during the policy term, whereas a temporary life annuity may pay several times. The indicators for its payments can therefore overlap, so a correct second-moment calculation must retain the dependence between them.
This mission formalises temporary life annuities payable in advance and in arrears, using the finite contingent-cashflow framework established in Actuarial Mathematics I. It reuses the curtate survival-event definition from Actuarial Mathematics III.
Let be a probability space, and let be the measurable curtate future lifetime, counting completed years. The event that the life survives to time is
These events are nested. For all ,
Consequently their indicators satisfy
This matters for second moments: survival to one payment date and survival to another are not mutually exclusive. Their intersection is survival to the later date. No independence assumption is made.
A unit temporary life annuity payable in advance makes up to payments, at times . The payment at time is made if . With deterministic annual discount factor , its random present value is
The expected present value is
These are the temporary-annuity-in-advance identities in Chapter 3, equation (3.15). The first payment, at time zero, is certain whenever .
A unit temporary life annuity payable in arrears has potential payments at times , for . A payment is made only if :
Its expected present value is
These are the corresponding payment-in-arrears identities in equation (3.16). In particular, a life with can receive the first payment of the annuity in advance, but no payment from the annuity in arrears.
The general moment calculations in Section 3.1.1 apply to the payment schedules in equations (3.15) and (3.16). Intersections of survival events reduce to the requirement to survive to the later date.
For payments in advance, the finite double-sum second moment is
For payments in arrears, it is
These are ordered double sums. Every ordered pair of payment dates contributes, including the diagonal terms and both orders of each off-diagonal pair. The corresponding variances are
The double-sum second-moment results are formal specialisations of the general moment equations (3.5)–(3.6). They are not additional numbered results in Section 3.3.2, which gives the expectation and present-value identities in equations (3.15) and (3.16).
The main theorem packages the expected values, second moments and variances of both annuities under the same , , and . Its supporting milestones establish the nesting of survival events and the products of their indicators, the finite payment schedules, and the successive valuation identities.
Both definitions are instances of the generic finite present-value construction from Actuarial Mathematics I. The curtate survival event is imported from Actuarial Mathematics III. Together, these provide reusable foundations for later missions on deferred and guaranteed life annuities.
The finite sums cover , when both annuities have zero present value, and , when the advance annuity includes the certain payment at time zero and the arrears annuity pays only if the life has completed at least one year. Algebraically, the identities allow any real . In actuarial applications, is normally positive. This mission asserts neither convergence of an infinite whole-life annuity nor statistical independence of survival payments.
The primary source is Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Open Actuarial Textbooks Project, Chapter 3 §3.1.1 equations (3.5)–(3.6) and §3.3.2 equations (3.15)–(3.16).
This is a draft mission and has not yet been published. It formalises finite-term annual payments. Continuous payment timing, deferred whole-life payments, guaranteed-period annuities and infinite valuation are planned separately.
An endowment assurance pays a fixed benefit either when the policyholder dies during the policy term or when the policy reaches its maturity date. It therefore brings death-contingent and survival-contingent payments together in one valuation framework.
Actuarial Mathematics I established general identities for valuing finite contingent cashflows. Mission II formalised unit term assurance and the mutually exclusive events of death in different policy years. This mission extends those foundations to pure endowments and endowment assurances, covering payment dates, expected present values, second moments and variances.
Let be a probability space. The exact future lifetime takes nonnegative real values, while the curtate future lifetime records completed years. Their relationship is
For a term , the textbook's pure-endowment payment in equation (3.9) depends on strict survival:
The endowment-assurance formula in equation (3.10), by contrast, uses a maturity payment when , equivalently when . Define
These events differ if death occurs exactly at time . Given the relationship between exact and curtate lifetime,
Thus equation (3.9) uses exact lifetime and excludes death at , whereas equation (3.10) uses curtate lifetime and includes it, since then . This endpoint identity clarifies the textbook's conventions; it is not itself a numbered textbook result. No assumption is made that death at a policy anniversary has probability zero.
Under the strict exact-lifetime convention, a unit pure endowment payable at time has random present value
Equation (3.9) gives its expected value and variance:
Here is a deterministic annual discount factor. The Lean algebra permits any real , including the conventional case of a positive discount factor.
The endowment assurance pays a unit benefit at the end of the policy year of death if death occurs within the first years. Otherwise, it pays at time . As in equation (3.10), its present value is defined by
The theorem expresses this value as the sum of the unit term assurance from Mission II and the curtate maturity payment:
The death benefit and maturity benefit are mutually exclusive. This gives the expected value and second moment:
The variance is then
The formalisation proves measurability of the strict and curtate survival events, the exact boundary-event bridge, disjointness of death during the term from survival to maturity, and the pure-endowment expectation and variance. It also proves the endowment decomposition, expectation, second moment and variance. The formal capstone brings these results together under one probability measure, using the same exact and curtate lifetimes, term and discount factor. It states the boundary bridge explicitly and includes the pure-endowment mean and variance, along with the endowment present value, mean, second moment and variance.
The formalisation reuses Mission II's definition of term-assurance present value rather than reconstructing it. The main namespace remains ActuarialValuation, so later life-annuity missions can use the survival-event lemmas.
The edge cases require care. When , the endowment assurance pays immediately. The strict pure endowment, however, still depends on whether . Death at exactly is represented separately and is never excluded by an unstated continuity assumption. The finite real-valued Lean identities permit negative or zero discount factors as a mathematical generalisation, although ordinary actuarial applications use positive discount factors.
The primary source is the Open Actuarial Textbooks Project, Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 2 §2.4.3, Chapter 3 §3.2.3 equation (3.9) and §3.2.4 equation (3.10).
Mission II, Actuarial Mathematics II: Term Assurance Present Values and Moments, is under moderator review at drafting time. Its relevant published definitions and theorem IDs are referenced directly.
This mission formalises unit benefits over a finite term with deterministic annual discounting. It establishes a finite-horizon result, not an infinite-horizon theorem. It does not cover immediate death benefits, arbitrary benefit scales, lifetime-dependent interest, infinite whole-life present values or the full continuous-time theory of mortality.
A sender can encode a classical message in a quantum state, transmit that state through a noisy quantum channel, and let a receiver measure the output. For researchers studying classical communication over quantum systems, the question is whether evaluating one channel use captures the benefit of encoding across several uses. Hastings established that the relevant information quantity can violate additivity when joint inputs are allowed. Hastings, 2009.
The result contributed here concerns the size of that discrepancy in finite dimensions. It gives channels for which positive single-use information is arbitrarily small while both the absolute two-use additivity gap and the relative benefit of two uses are arbitrarily large. The paper's introduction states the gap, capacity, and separation consequences; the released Lean theorem packages the small-information, gap, and ratio conclusions into one common-witness statement. Revised manuscript, Section 1, headline Lean theorem.
A finite-dimensional quantum channel is a completely positive, trace-preserving linear map on complex matrices, where the positive integers are its input and output dimensions. A density matrix is a positive semidefinite matrix with trace one. Such matrices represent the possible input states. The released development represents a channel by finitely many rectangular Kraus matrices , satisfying , with action . Concrete channel definitions.
The von Neumann entropy in bits is , where are the eigenvalues of , using . A finite ensemble consists of density matrices and real probabilities with . The Holevo quantity is
The supremum includes all normalized finite ensembles. For two uses, acts on joint inputs, including states entangled between the uses. Write , , and, when , . These are the released definitions chi, chiTwo, gap, and twoUseRatio. Definitions.
The broader release also studies operational classical capacity : the supremum of achievable classical message rates in bits per use. Its independent definition uses actual density-matrix codewords, a normalized positive-operator-valued measurement decoder, and average Born decoding error tending to zero over all positive block lengths. Arbitrary block inputs and joint decoding are allowed. That coding development provides context for the result; it is a separate released branch outside this contribution's initial import. Released operational definition.
The headline statement is
One channel witnesses every inequality. The lower-bound thresholds are arbitrary real numbers; they are not restricted to positive values in the Lean statement. Input and output dimensions may depend on the thresholds. The goal imposes no hard-coded dimension bound or numerical constant. It is the exact statement of Nonadditivity.DeterministicConsequences.exists_small_chi_large_gap_and_ratio. Source.
The supporting separation statement uses a sequence of genuine finite channels with
The separation statement is already proved for the selected deterministic family. It gives the two information limits asserted in the manuscript's Corollary 1.3, with no analytic channel-existence assumption. The formal family is totalized at its first two indices by the one-dimensional identity channel; this finite prefix does not affect either limit. Its members have positive single-use Holevo information for every . Released family, positivity, and limits.
The theorem gives unbounded absolute Holevo additivity gaps and unbounded two-use ratios for the same witnesses, even while their single-use information is arbitrarily small. This supplies an existence result rather than an efficient method for finding small channels with practical parameters. The manuscript separately proves explicit sufficient input dimensions; those bounds are not conclusions of the headline theorem. Manuscript, Corollaries 1.2–1.3.
The mathematical result is proved, and its principal endpoints already have machine-checked Lean proofs in release v1.0.0. This contribution imports the existing deterministic separation theorem and its dependency library, preserving their source provenance and proofs. The reusable material includes density matrices, concrete channels, entropy, finite ensembles, tensor products, and the finite-channel construction. Independent review of the correspondence between the formal statements and the manuscript remains useful. Release and verification scope.
The broader release additionally proves from independently defined physical codes, implying . It also proves a common-witness theorem combining small positive information with arbitrary capacity gain and two-use ratio. Those operational results are separate released context, rather than targets or imported milestones of this contribution. They concern unassisted memoryless communication and do not assert distinct-channel capacity nonadditivity or a strong converse. Released coding identity, released operational consequence.
A separate information estimate for each channel factor does not control inputs entangled across an entire block. The construction needs bounds valid for every such joint input, while retaining the favorable two-use behavior. Likewise, convergence of averaged matrix moments alone need not control exceptional eigenvalues and therefore cannot replace the needed norm control. These are substantive uniformity requirements in the paper's construction. Manuscript, Section 1.
Regrouping tensor powers of one fixed channel is insufficient for a gap linear in the regrouping length: the manuscript shows for a fixed . The existential goal instead allows channel dimensions and the channel itself to vary. Fixed-channel limitation.
The imported representation is ActualConsequences.FiniteQuantumChannel: finite, nonempty input and output index types, a finite environment index type, and a concrete Kraus channel. Entropy is computed spectrally with natural logarithms internally; holevoBits divides by . Supremum and infimum uses are accompanied by the developed nonemptiness and boundedness results. Positive tensor powers are indexed by a natural number meaning uses. Strict positivity of the goal's prevents division-by-zero interpretations of its ratio. The channel and information quantities must retain these physical definitions; numerical records assigned the desired values would not formalize the result. Formal representation, bit conversion.
The headline proof uses the alternate deterministic finite-channel construction. It does not assert the prescribed-dimension result. The imported library provides complex matrix analysis, positivity and trace normalization, tensor products, entropy inequalities, finite ensembles, and the construction's finite group and moment infrastructure. The full manuscript remains outside the completed formalization: general Haar convergence interfaces and the broader finite-dimensional realization statement retain their documented limitations. The release's correspondence findings remain qualified; no complete semantic audit or independent human certification is claimed. Formalization status, statement review.
635aa93eb3a2310b79fd5371e2ce311914ec5887.A quantum channel describes a physical process that transforms a quantum state into another state. Comparing two channels means comparing their possible outputs, including outputs obtained when the input is entangled with a reference system. This distinction matters in quantum information: an experiment can retain a reference while sending the other part of an entangled state through an unknown process. The resulting measure of distinguishability should account for that experiment.
For states, several divergence measures approach relative entropy when their order parameter approaches one. For channels, optimization over inputs and arbitrarily many channel uses introduces an additional question: does this continuity survive those optimizations? Jinzhao Wang and Yuxiang Yang answer that question for the regularized, stabilized sandwiched Rényi divergence in Continuity of Regularized Channel Rényi Divergences, arXiv:2609.28635v1, Theorem 1. This mission contributes the completed result and its supporting formal infrastructure.
Let and be nonzero finite-dimensional complex Hilbert spaces. A density operator is a positive operator with trace one. Two channels are completely positive, trace-preserving linear maps with the same input and output spaces.
The relative entropy compares density operators and . The sandwiched Rényi divergence is an order-dependent comparison, defined for , . The state, channel, and regularized divergences are measured in bits. Operator-level analytic lemmas may use natural logarithms; the state wrappers divide by . Singular states are allowed; the support conventions retain infinite values rather than assigning a finite substitute. These are the state quantities in the paper's equations (1.2)–(1.3).
The stabilized channel divergence optimizes the state divergence over normalized pure inputs on , where is a copy of . The channel acts on and the identity acts on . Writing , the convention is
where denotes either state divergence. The paper places the reference first; the formalization places it second and proves the tensor-factor convention agrees. A block of uses employs and a reference copy of . Its pure input may be entangled across every use. Equation (1.4) specifies this stabilization.
The regularized divergences are defined independently as positive-block suprema:
Two supporting targets establish that these definitions are the actual asymptotic limits in equation (1.5). For every fixed , ,
and
The main goal is Theorem 1:
This is convergence from both sides. Each target includes infinite divergence. The block identities are supporting identifications, rather than extra premises of the main theorem.
The main result identifies a single limit after optimization over entangled inputs and unbounded block lengths. It permits near-one regularized Rényi quantities to approach regularized relative entropy for arbitrary channel pairs in the stated finite-dimensional setting. When the latter is infinite, the conclusion is convergence to positive infinity. The paper discusses applications to discrimination and asymptotic approximation; those operational conclusions are beyond this mission's targets. Wang–Yang, arXiv:2609.28635v1.
This is a contribution of a known, formally proved result, rather than an unsolved conjecture. The original public Lean development includes proofs of the definitions' supporting properties and both block identities. Its recorded verification reports Lean checking with a transitive axiom audit, Comparator statement comparison and Lean kernel replay, and independent Nanoda kernel checking. These records concern the original pinned development. They are unsigned and do not establish independent human review of correspondence to the paper. The converted contribution uses Lean 4.30.0 and Mathlib c5ea003. Its 95 Definition bundles and 27 theorem nodes have been published; every theorem has an ACCEPTED proof and public Proved status. Before upload, the exact statement and solution files compiled locally, their types and transparent definition values were compared with the frozen compatibility port, and a transitive axiom audit of every generated declaration found only propext, Classical.choice, and Quot.sound. These new checks are separate from the original Comparator and Nanoda records. Human review of correspondence to the paper is still required.
Pointwise continuity for a fixed pair of output states does not justify interchanging a limit with the supremum over all block inputs. That domain includes every positive block length, so finite-dimensionality of each block does not itself supply a uniform conclusion. The right-hand limit is particularly sensitive to the order of these operations. Singular inputs introduce a separate issue: support mismatch can force genuine infinity, and converting all expressions to ordinary real numbers would discard that case. The formalization must preserve these domains and conventions throughout, as documented in the paper-to-Lean mapping.
The Lean representation uses actual positive density operators, CPTP maps, reference systems, and tensor powers. State divergences have extended-real values; channel and regularized divergences take values in . Nonnegativity is proved for the admissible orders, so conversion to nonnegative extended reals preserves those values. Supremum definitions quantify over positive block lengths. The normalized block sequences are total at , which is irrelevant to convergence as .
The main formal statement uses a punctured neighborhood of one. A sufficiently small such neighborhood lies within , so totalized definitions at other real orders impose no assertion about their divergence interpretation outside the admissible range. No support inclusion, finite max-relative entropy, filter estimate, or Schatten estimate is assumed by the main theorem. Defining the limiting value to equal the desired conclusion, or replacing arbitrary channels by an easy special family, would not meet these targets.
The development builds on Mathlib and Lean-Quantum. Reusable components include extended-valued Fekete convergence, channel tensor identities, quantum testing quantities, prescribed-dilation approximation, and finite-dimensional Schatten bounds. The scope mapping records that the supporting decomposition estimate is formalized for , sufficient near one; it does not claim the paper's entire all-orders version. Contributions that improve reuse, verify the converted dependency graph, or extend separately stated results are welcome. The paper's later operational corollaries are excluded.
The asymmetric traveling salesman problem (ATSP) asks for a shortest closed walk through every vertex of a directed graph whose edge weights need not be symmetric. It models routing with one-way streets, scheduling with sequence-dependent setup times, and many other problems in which the cost of going from to differs from the cost of going back. Its standard linear relaxation, the asymmetric Held–Karp relaxation, is the lower bound used both by exact branch-and-cut codes and by approximation algorithms, and the central question about it is how far it can be from the integer optimum.
Timeline of the approximation ratio and of the integrality gap for ATSP:
The lower bound on the integrality gap remains (Charikar, Goemans and Karloff, 2006).
A digraph has finite vertex and edge sets; each edge has a tail and a head, and parallel edges and loops are allowed. For , and are the edges leaving and entering , and . An ATSP input is a strongly connected digraph with a weight function .
An edge multiset gives each edge a multiplicity ; is the set of vertices it touches. is Eulerian if every vertex has as many outgoing as incoming edges of , a subtour if moreover is connected, and a tour if it is a subtour with . Tours are exactly the closed walks visiting every vertex. The weight of is .
The asymmetric Held–Karp relaxation LP is
and its optimum is the Held–Karp lower bound.
The mission also uses the paper's intermediate objects: laminarly-weighted instances , in which is a laminar family of sets that are tight for a strictly positive feasible , on , and the weight of an edge is ; the value and the lower bound ; Subtour Partition Cover and -lightness; irreducible instances; vertebrate pairs; and quasi-backbones. Each is defined, with the paper's page reference, in the two definition files of the mission.
For every strongly connected digraph with , every and every feasible solution of LP, there is a tour with
This is the statement that the integrality gap of the asymmetric Held–Karp relaxation is at most .
The milestones are the results the paper's §11 combines, in the order it combines them:
The result shows that the asymmetric Held–Karp relaxation approximates ATSP within a constant factor, which settled a question open since the 1980s and made the relaxation a certified lower bound with bounded loss. The structural steps (reduction to laminarly-weighted instances, Subtour Partition Cover, irreducibility and vertebrate pairs) are the framework on which the later improvement to by Traub and Vygen is built.
The theorem is proved; to the best of available knowledge none of it has been formalized in a proof assistant. A complete development would give a machine-checked bound on the integrality gap of a central relaxation in combinatorial optimization, and its intermediate statements are reusable for the improved bounds that follow the same framework.
The obvious approaches do not give a constant. Repeated cycle covers lose a factor at each of logarithmically many rounds. Rounding the LP solution through thin trees needs a spanning tree that is thin in every cut, and only polylogarithmic thinness is known. The paper's route is long: the reduction to laminarly-weighted instances needs an uncrossed dual; the reduction from irreducible to general instances and the one from vertebrate pairs to irreducible instances are recursive, applying the assumed algorithm to instances built by contracting or inducing tight sets, so their hypotheses must hold on all instances and not only on the given one; and the lightness bound for vertebrate pairs (Theorem 10.1) rests on a flow-based construction with careful accounting against the laminar family.
Vertices and edges are finite types; edges carry tail and head maps, so parallel edges (created by contraction) are distinct edges, and loops are allowed and lie in no cut. Edge multisets are functions . Connectivity of a multiset and its components are defined by the reflexive–transitive closure of undirected adjacency along its edges.
Running times are not formalized. Every algorithmic statement is posed in its existential form, as §11 of the paper itself uses it to derive Theorem 11.1: "there is an algorithm returning a tour within " becomes "every instance has a tour within ", and an assumed algorithm becomes a hypothesis quantified over instances on all finite vertex and edge types. The algorithmic constants , , and are therefore not stated; the non-constructive constants , and of §11 are.
The Held–Karp lower bound is never defined as an infimum: comparisons with it are stated for every feasible , equivalently because the LP optimum is attained. Likewise and in the definition of irreducibility are expressed through walks, without an infimum.
Added hypotheses, each disclosed in the item's Formalization Note:
These choices rule out trivializing formalizations: no instance class in a hypothesis is empty (a two-vertex singleton instance is valid, irreducible and vertebrate), admissible partitions exist for every instance, and LP is feasible for every strongly connected input. The goal assumes none of the milestones.
Out of scope: the polynomial running times, §5's merge-procedure lemmas, the constructions of §7, and Corollaries 11.2–11.4 on the path version, which rest on external reductions. Contributions are welcome on every milestone, and on infrastructure that a complete development needs: LP duality and uncrossing for cut LPs, Eulerian multigraphs and their decomposition into closed walks, and circulations with lower bounds (Hoffman's theorem). The platform's proved LP strong duality (SmaleNinth.lp_strong_duality) is a natural starting point for Lemma 2.2.
The Volterra square-root model describes a nonnegative, time-dependent state whose present value depends on a weighted history. Ordinary square-root diffusions use a constant kernel and have a Markov state; replacing that kernel by a function of elapsed time allows persistent or singular memory. This matters for the transform formulas used to characterize distributions of such processes. Those formulas depend on a deterministic nonlinear integral equation, and require a solution that exists at every finite time. Abi Jaber, Larsson and Pulido isolate that requirement in Lemma 6.3 of Affine Volterra processes, arXiv:1708.08796v3 (2019).
The paper's Section 6 treats processes in the nonnegative orthant and its Section 7 specializes the framework to a Volterra Heston model. The present mission concerns the deterministic equation behind the Section 6 transform. The stochastic existence theorem and the transform identity are separate results in the same paper. Keeping this mission on the integral equation makes its analytic content usable independently of a chosen probability space.
Fix a finite coordinate set of size . A diagonal kernel consists of real functions for , with the -th entry of the matrix kernel equal to and all off-diagonal entries zero. A resolvent of the first kind for is a nonnegative measure for which the convolution equals one at positive times. The relevant regularity condition, labeled (2.5), requires local square integrability and positive-time translation bounds of order for some . Condition (3.4) requires a kernel to be nonnegative, nonzero, nonincreasing and continuous at positive times. It also requires its resolvent measure to have decreasing interval masses as increases. Each shifted function must satisfy (3.4) for , with its own resolvent. These are the assumptions of Theorem 6.1 and hence of its Lemma 6.3 (pp. 6, 14, 28–29).
Let be a complex row vector and let be a locally integrable complex row function. Let be a real matrix whose off-diagonal entries are nonnegative, and let . The -th square-root Riccati–Volterra equation is
The index selects column : in the paper's notation and the coupling is . The kernel acts only on the -th equation, while couples the coordinates. The coefficient from the stochastic process does not enter this equation (equation (6.3), p. 27).
The goal is the global existence, uniqueness and sign statement of Lemma 6.3. If and , then
For functions defined only up to null sets, the equation, uniqueness and sign conclusion are understood almost everywhere. The goal has no fixed time horizon and no hard-coded kernel: it covers every diagonal kernel satisfying the paper's conditions. The five milestones record the source's analytic support: the shifted resolvent bounds (3.9)–(3.10), the stability lemma C.1, maximal-solution Theorem B.1, global-solution Corollary B.3 and nonnegative-orthant invariance Theorem C.2. Their statements and locations are recorded in the milestone list.
Global solvability makes the square-root transform equation meaningful at any finite horizon. Uniqueness fixes the transform parameter determined by a kernel and forcing function. The nonpositive real part is the sign property needed in the paper's subsequent exponential-affine transform argument for nonnegative states (Theorem 6.1(ii), pp. 28–29). Without a global solution, that argument would only address a time interval before a possible blow-up.
The result is proved in the cited paper; this mission asks for a machine-checked development of that known theorem and its supporting integral-equation results. Its reusable output includes an notion of Volterra solution, the first-kind resolvent hypotheses, maximal lifetime, stability under changes of forcing and kernel, and a comparison statement for diagonal systems. The goal and milestones are presently proof obligations, not claims of existing machine-checked proofs.
Local solvability alone does not control the quadratic term for arbitrarily large time. In particular, a generic local fixed-point theorem can yield a maximal solution whose norm diverges at a finite horizon. Sign information for the real part is also coupled to the imaginary part through that quadratic term; checking each coordinate independently does not establish invariance of the nonpositive half-plane. The analysis has to preserve the kernel's first-kind resolvent conditions and the off-diagonal sign pattern of across the coupled system. Singular kernels allowed by (2.5) prevent replacing the problem with a standard ordinary differential equation.
Time is represented by real numbers and every local condition is restricted to positive bounded intervals. Vectors are functions on Fin d; matrix membership is componentwise. These finite-dimensional norms are equivalent to the Euclidean and operator norms used in the paper. The kernel regularity estimates are Big-O statements as tends to zero through positive values. A first-kind resolvent is a nonnegative measure supported on nonnegative times, with the convolution identity and interval-mass monotonicity stated directly. The convolution at positive time is an interval integral; the bound at zero in (3.10) uses the integral on , while the source describes a right-continuous extension when available.
Solutions are locally square integrable and satisfy their equations almost everywhere. The integrability of each asserted convolution is part of the solution predicate, so the default zero value of a nonintegrable Lean integral cannot create a spurious solution. A maximal lifetime is extended-nonnegative-real valued, allowing infinity, and a finite lifetime requires an infinite extended norm. Sign conditions on locally integrable forcing and on the solution are almost everywhere. Measurable time dependence of the nonlinear drift is made explicit for Theorem B.1 and Corollary B.3, where it is necessary to interpret their integrals. The condition of the square-root process is omitted from the goal because is absent from (6.3).
The development needs Mathlib's Bochner integrals, local predicates, measures, complex arithmetic and asymptotic filters. Proof contributions to the five source milestones and the goal are welcome, including infrastructure for nonconvolution Volterra resolvents where the paper cites earlier literature. The formalization must keep the coefficient , the column index , and every shift .
Kernel ridge regression is a standard nonparametric estimator with optimal statistical guarantees, but it needs the kernel matrix of the data: roughly time and memory. Random features (Rahimi and Recht, NeurIPS 2007) replace the kernel by an average over randomly sampled feature functions, turning the problem into ridge regression in dimension , at cost time and memory. The question is how many features are needed before the statistical accuracy of the exact kernel method is lost.
The first statistical analysis of a random-features estimator (Rahimi and Recht, NeurIPS 2009), for Lipschitz losses over a ball of fixed radius, needs features to reach an bound. Rudi and Rosasco (arXiv:1602.04474, NeurIPS 2017) showed that of order features already give the excess risk that exact kernel ridge regression attains with regularization (Caponnetto and De Vito 2007), assuming only that the best predictor in the reproducing kernel Hilbert space exists.
Let be a separable input space and a probability space. A random feature is a function , continuous in both variables with for some . It defines the kernel
whose reproducing kernel Hilbert space is . Data are drawn i.i.d. from a probability on with almost surely, . The expected risk is , and is a minimizer of over , assumed to exist.
Given features drawn i.i.d. from , independently of the data, the feature map is . With and , the random-features ridge estimator with parameter is
In the Lean development these are kernelOf, featureMap, empCov, empCross, rfWeights, rfEstimator and risk in the namespace RFRidge.Basic.
There are constants , independent of , and , and a threshold such that for every and , with and
features, with probability at least over the data and the features,
The constants are existential: the paper prints them without values, and the values in its appendix are not established by the printed proof. The goal therefore asserts the shape of the bound, which survives any later improvement of the constants.
The proof goes through an analytic decomposition of the excess risk on followed by concentration. The milestones are the results of that proof that are stated as printed:
Theorem 1 shows that, in the basic setting, random features reduce the cost of kernel ridge regression from time and memory to and without losing the minimax-optimal rate. It is the reference result on the statistical cost of random-features approximations, and the same decomposition yields the paper's faster rates under source and capacity conditions (Theorems 2 and 3) and the analysis of data-dependent feature sampling.
To the best of the mission's knowledge, none of these results has a machine-checked proof. Formalizing them requires real infrastructure: integral operators on defined by a kernel with an integral representation, operator inequalities for the continuous functional calculus, and Bernstein inequalities in Hilbert spaces. The Bernstein inequalities and the operator inequalities (Cordes, interpolation, Proposition 8) are reusable well beyond this paper.
The obvious argument controls uniformly and transfers it to the estimator. It needs of order to keep the rate, because a uniform kernel approximation ignores that the estimator only probes through a regularized operator. Getting features requires comparing the integral operators and relative to , in the operator norm weighted by , and this needs fractional powers of operators, operator monotonicity and concentration of random operators. A second subtlety is that the regression function need not lie in the closure of ; Lemma 2 shows that the orthogonal component does not affect any random-features estimator.
All models are posed in Lean 4 with Mathlib. The input space is a separable topological space with its Borel σ-algebra, the feature space is the type W, and is jointly continuous, jointly measurable for the product σ-algebra (an added hypothesis: without second countability it does not follow from continuity), and bounded by everywhere. The RKHS is Mathlib's RKHS ℝ H X ℝ, tied to the kernel by RKHS.kernel H x x' 1 = K x x'. Samples and features are indexed from ; the samples and features have the product law , and is rounded up. "With probability at least " is "the failure event has probability at most ", with and .
Operators: the paper's Hilbert spaces are real, but Mathlib's continuous functional calculus for bounded operators, which defines and , exists only on complex Hilbert spaces. The operator milestones are therefore posed on complex Hilbert spaces, and every inverse or power is the functional calculus of an explicit real function; the real statements follow by complexification. Lemmas 3–5 are stated for abstract positive operators satisfying exactly the relations their proofs use, and add (the range of Assumption 6), without which Lemma 5 is false. Proposition 8 states as a conclusion. Lemma 3 corrects a sign in the exponent of : its display prints where its proof uses ; the printed bound fails for scalar operators.
A trivializing formalization is ruled out: the goal mentions only the estimator, the risk and , never the operators of the proof, and its constants are fixed before and , so they cannot absorb or .
Not included: Theorem 4 (the analytic decomposition), Propositions 5 and 7 (which need Hilbert–Schmidt norms and traces), Lemmas 6–10 and Theorems 5–7 of Appendix A.3–A.4. Contributions of these intermediate results, of a Lean theory of integral operators of kernels, and of Hilbert-space concentration inequalities are welcome.
The projected stochastic subgradient method minimizes an expected loss over a closed convex set : it samples a data point, steps against a sampled subgradient, and projects back onto . For convex its sample complexity has been known for decades, and for smooth nonconvex the stochastic gradient method needs samples to reach gradient norm (Ghadimi–Lan 2013). Many problems in statistical learning and signal processing are neither convex nor smooth — robust phase retrieval, nonlinear regression with an loss, covariance estimation, conditional value-at-risk with smooth losses — but are weakly convex: they become convex after adding a quadratic .
Timeline. Nurminskii (1970s) showed that for weakly convex losses and no constraint the stochastic subgradient method subsequentially converges to a stationary point almost surely, without a rate. Ghadimi and Lan (2013) proved the rate for smooth . Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 2019) proved the first rate for the plain projected stochastic subgradient method on weakly convex problems, measured by the gradient of the Moreau envelope, and for any nonnegative stepsizes. This is Theorem 3.1 of their paper and the goal of this mission.
Work in with the Euclidean norm. Let be nonempty, closed and convex, and let be -weakly convex (): is convex. The problem is
where is on and off .
The subdifferential is the set of with as . For the Moreau envelope and the proximal point of are
Assumption A (stochastic subgradient oracle): on a probability space one can draw i.i.d. samples (A1); there are an open set and a measurable map with for all (A2); and for all (A3).
Algorithm 3.1 with starts at and, for , samples and sets with stepsizes . It returns with drawn from with probability .
For every and any stepsizes with ,
and with , ,
The result. The gradient of the Moreau envelope is a near-stationarity measure: small means that is within of a point with and . Theorem 3.1 therefore gives sample complexity for finding nearly stationary points of nonsmooth nonconvex constrained stochastic problems, matching the smooth case. Estimate (3.3) shows that the Moreau envelope is an approximate Lyapunov function for the method, and it holds for arbitrary nonnegative stepsizes; Theorem 3.4 of the same paper (the proximal extension) needs and a worse constant.
Formalizing it. The result is proved in the paper; no machine-checked version exists. A formalization requires the Fréchet subdifferential of extended-valued functions, the Moreau envelope and its smoothness under weak convexity (Lemma 2.2, which the paper cites as standard rather than proving), and a measure-theoretic treatment of the iterates of a stochastic algorithm on a product probability space. Lemma 2.1 and Lemma 2.2 are reused by the other missions of this series.
The obvious approach — show that decreases in expectation — fails: without smoothness, a subgradient step can increase by an amount of order , not , and no stepsize repairs that. The argument instead tracks the Moreau envelope, which is smooth even though is not; the difficulty moves into (i) Lemma 2.2, the -smoothness of the envelope of a weakly convex function, which is a nontrivial piece of variational analysis, and (ii) the conditional-expectation bookkeeping that turns a one-sample estimate into (3.3) along the random iterates, including the integrability of and , which the paper does not discuss.
EuclideanSpace ℝ (Fin d). An extended-valued function is encoded by its domain and its real values on the domain; is the pair , and is moreauEnv X f lam, a real infimum over . Lemma 2.2 supplies the attainment and differentiability under which this infimum is the paper's envelope.proj constrained by the published nearest-point predicate SpectralProjGrad.Shared.IsProjOnto X proj. It is not the proximal-point predicate of , so that remains meaningful; zero stepsizes are allowed, as in Algorithm 3.1.proj, a stochastic subgradient not tied to by (A2), expectations without integrability, or as a junk-valued infimum would be trivial or false; each is excluded by the statements' hypotheses and conclusions.Proofs of any milestone are welcome; Lemma 2.2 and the product-measure bookkeeping for (3.3) are the reusable parts.
Bayesian inverse problems for functions — the initial condition of a PDE, a permeability field, a diffusion coefficient — lead to posterior measures on an infinite-dimensional Hilbert space , given by a density with respect to a Gaussian prior . In practice is sampled by Markov chain Monte Carlo on an -dimensional discretisation , and the question that matters is whether the sampler's convergence rate survives the limit . For the standard random-walk Metropolis algorithm it does not (mission III of this series). The preconditioned Crank–Nicolson (pCN) algorithm, whose proposal preserves , was introduced to avoid this (Beskos, Roberts, Stuart and Voss 2008; Cotter, Roberts, Stuart and White 2013).
Hairer, Stuart and Vollmer (2014) prove that pCN has a Wasserstein spectral gap that is uniform in the dimension. Mission I of this series covers their result for globally Lipschitz potentials (Theorem 2.12). This mission covers Theorem 2.14, which needs only that be locally Lipschitz, with a local Lipschitz constant growing slower than any exponential. That class contains potentials of polynomial growth, which arise for nonlinear forward maps.
is a separable real Hilbert space with a centred Gaussian measure , and is an orthonormal basis of eigenvectors of the covariance of . is the span of , and is the image of under the orthogonal projection onto . For a potential the targets are
Fix a step size and put . One pCN step from draws and proposes . The proposal is accepted with probability ; otherwise the chain stays at . Its transition kernel is . The kernel is the same algorithm on with .
Distances between probability measures are Wasserstein lifts of a cost : over couplings of . A kernel is -contracting if implies for a fixed . A set is -small if for all .
The distance of this mission is a weighted path length (3.6). For unit-speed paths from to ,
with () or ().
There are two assumptions. Assumption 2.10 says that for every proposal within distance of the proposal mean is accepted with probability at least , where . Assumption 2.13 says that is -integrable and that for every .
Under Assumption 2.10 with (, ) and Assumption 2.13:
The essential point is that does not depend on .
The paper derives Theorem 2.14 from these, from Lemma 3.2 (Lyapunov functions) and from Proposition 2.6 (the weak Harris theorem of Hairer, Mattingly and Scheutzow 2011). The last two are posed in mission I of this series.
A Wasserstein spectral gap uniform in means that the number of pCN steps needed to reach a given accuracy does not grow with the discretisation level. In §4 of the paper this yields a strong law of large numbers and a central limit theorem for pCN ergodic averages, and, combined with Theorem 2.15, an -spectral gap and mean-square error bounds, all uniform in the dimension. The locally Lipschitz case is the one that covers potentials of polynomial growth.
The result is proved in the paper. It has not been formalized. A formalization would produce a reusable weak-Harris toolkit for Markov kernels on Polish spaces, and a machine-checked account of the path-metric construction, which the paper adapts from Hairer and Majda (2010) and Hairer, Mattingly and Scheutzow (2011). It would also check the paper's proof, whose printed Lemma 3.5 (3) contains a typographical slip in the exponent; the formalized bound is the one the proof derives.
With only locally Lipschitz, no single makes contracting. The probability that exactly one of two coupled chains accepts is controlled by , and far from the origin this exceeds any fixed multiple of . The weighted path distance makes far-out points "close" only when they are very close in norm. But then even the "both accept" move can increase the distance, because the weight changes along the move. Showing that the shrinkage of the proposal mean beats this, while the Gaussian noise term stays integrable uniformly in , is the content of Lemmas 3.5 and 3.6. The order of the choices (, then , then ) is essential.
IsGaussian with mean zero. is a HilbertBasis ℕ whose vectors are pairwise uncorrelated under the covariance bilinear form.Kernel.withDensity. Kernel powers are composition powers, and is Measure.bind.Many stochastic models have a present state that depends on a weighted history of past drift and noise. A stochastic Volterra equation captures this dependence through a kernel : a recent increment and an older increment can enter the current state with different weights. Classical affine diffusions arise from the special constant kernel . For those diffusions, conditional Fourier–Laplace transforms can often be found from finite-dimensional Riccati ordinary differential equations. The paper by Abi Jaber, Larsson and Pulido asks for an analogous transform when the kernel retains memory. Its Theorem 4.3 gives a formula for a continuous affine Volterra process under a stated Riccati–Volterra solution assumption.
The result matters for models in which the history cannot be replaced by the current state alone. The transform characterizes conditional distributions and integrated path functionals in the form used by the paper's later results. The present mission isolates Theorem 4.3 and four of its stated supporting claims. The paper proves these results; the mission seeks machine-checked proofs of their Lean statements.
Fix a positive integer and a deterministic, matrix-valued kernel whose entries are locally square integrable. The Volterra convolution of with a vector function is . Matrix convolutions retain the order of multiplication: .
Let be real symmetric matrices and real column vectors. Their affine covariance and drift are and . The matrix has the as columns. For a complex row , write ; the transpose is ordinary, with no complex conjugation.
An affine Volterra process is a continuous solution of
Here is a -dimensional Brownian motion on a usual stochastic basis, is deterministic, and stays in a state space . The continuous coefficient obeys on , where is positive semidefinite. This is Definition 4.1 and the standing setting of Section 4 of the paper.
The main target is Theorem 4.3. Fix a finite horizon , a complex row , and an integrable complex-row function . Suppose a square-integrable function solves the Riccati–Volterra equation
Define by the stochastic integral and drift in equations (4.4)–(4.5). The theorem identifies with a conditional mean plus a quadratic correction:
It also states that is a local martingale on . If it is a true martingale, then the exponential-affine transform formula is
The milestone list records Lemma 4.2's conditional and unconditional means, the mean Volterra equation stated in the proof of Theorem 4.3, the resolvent commutation claim in the proof of Lemma 4.4, and Lemma 4.4's equivalent Riccati equation. A second-kind resolvent of uses the paper's sign convention for ; the equivalent equation uses .
The conditional transform links a path-dependent stochastic equation to a deterministic nonlinear Volterra equation. It supplies a way to describe the law of a future state together with a linear functional of its past. The conditional-mean milestone separately gives a usable formula for , while the resolvent milestones identify the deterministic kernel relations needed by the transform.
The source provides proofs of these claims. The formalization task is to check their assumptions and equalities against a precise model of Brownian Itô integration, conditional expectation, and matrix convolution. Published Lean definitions for Brownian motion and an Itô integral relation are reused. The affine Volterra process, its Riccati equation, and these theorem statements are drafted here; their proofs remain open.
The conditional payoff involves the entire path before , while generally has no finite-dimensional Markov state. Consequently, the familiar affine-diffusion formula in terms of alone is not the target of Theorem 4.3. Deterministic matrix convolutions are order-sensitive, and the two resolvents of and have different kernels. Stochastic convolutions also have integrands that depend on the terminal time. The passage from fixed-time integral equalities to a continuous local-martingale process requires care about versions and filtration adaptation.
Processes use nonnegative real time, while deterministic kernels and interval integrals use real time. Finite-dimensional conditions are checked componentwise. Kernel and resolvent identities between locally integrable functions hold almost everywhere on positive time. Riccati equations hold almost everywhere on ; stochastic and conditional identities hold almost surely at each fixed time. The local-martingale claim uses the real and imaginary parts of the complex exponential, stopped at .
The process definition includes the Section 4 assumptions on symmetry, covariance positivity, continuity of , deterministic , and the usual stochastic basis. Brownian Itô terms are constrained by the published integral relation. Deterministic drift convolutions require integrable integrands. The theorem asserts integrability of the payoff and of as conclusions, preventing conditional expectation from defaulting to zero. In (4.6) the conditional means enter the -integral through a jointly measurable version in , so that integral cannot default to zero. The dimension is positive, and the theorem does not specialize the kernel to or insert a resolvent assumption into its goal.
A complete development will need reusable results on locally integrable matrix kernels and their resolvents, stochastic Fubini interchange, moment bounds for Volterra solutions, and conditional expectation of the resulting integrals. The moment bound is posed as Lemma 3.1 in the companion existence mission. This draft includes the four listed milestones; Lemmas 2.1 and 2.5 from the source are left for a fuller stochastic Fubini and semimartingale encoding. Contributions that preserve their general hypotheses and conclusions are welcome.
Many problems in statistical learning and signal processing take the form of minimizing an expectation plus a regularizer or constraint , where the only access to is through samples . The classical tool is the stochastic (proximal) subgradient method, which replaces at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss , and the stochastic prox-linear method linearizes only the smooth inner part of a composite loss . In experiments the richer models are markedly less sensitive to the choice of step size.
Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization, in which each step minimizes a sampled one-sided model of plus plus a quadratic penalty. Their main theorem (Theorem 4.3) covers weakly convex problems through the Moreau envelope. This mission formalizes the companion result for the convex setting, Theorem 4.1: when the models lower-bound in expectation without quadratic error and is convex, the expected function gap at a weighted average of the iterates decays like . As the paper notes (p. 22), for the stochastic proximal subgradient method this improves earlier bounds (Cruz 2017; Duchi–Singer 2009) because no subgradient norm of enters the estimate.
Work in with the Euclidean norm. The problem is
where is locally Lipschitz and is closed (its epigraph is closed) with nonempty domain . A function is -weakly convex if is convex; is ordinary convexity.
Assumption B (p. 18) fixes a probability space , an open convex set , real constants , a measurable model on and a measurable such that:
Algorithm 4.1 (p. 19) starts at and, for , samples and sets
The convex setting is and . Write for the step sizes and let be any minimizer of .
For every ,
and with the constant step , ,
The factor in front of is the constant the paper's proof establishes; see Formalization scope.
Theorem 4.1 is the function-value guarantee of the model-based framework. Theorem 4.3 measures progress by the gradient of the Moreau envelope, which is the right quantity for nonconvex problems but says nothing directly about suboptimality; under convexity, Theorem 4.1 gives the familiar rate for the gap itself. It applies to the stochastic proximal point and prox-linear methods as well as to the proximal subgradient method, and §4.2 of the paper uses it for minimizing an expectation of a pointwise maximum of convex functions, such as the conditional value-at-risk. The estimate (4.8) behind it is also the engine of the strongly convex rate (Theorem 4.2, a separate mission of this series).
The result is proved in the paper; nothing in it is open. To our knowledge none of these statements has a machine-checked proof. The formalization contributes a checked version of the one-step estimate (4.8) with its corrected constant, a reusable Lean encoding of Assumption B and of Algorithm 4.1 with extended-valued , and the passage from conditional one-step bounds to expectations over the product measure of the samples.
The argument is short on paper; the work lies in the measure theory the paper leaves implicit. The iterate is an argmin that depends on and on the fresh sample , and the one-step estimate holds only conditionally, with frozen. Turning it into an inequality between unconditional expectations requires measurability of the iterates, independence of from the past, and integrability of and , which the paper takes for granted. The convex function is extended-valued, so the function gap is meaningful only because every iterate and every average lies in .
A naive one-step argument that bounds and separately, each by a Lipschitz constant times , gives the constant in (4.8) and not the printed . The printed constant is false (see below), so the constant cannot be improved simply by tightening that one step.
EuclideanSpace ℝ (Fin d). The extended-valued is a real function together with its domain D; closedness of is closedness of , and convexity is ConvexOn ℝ D. is L and is Lfun.Measure.pi), Fubini–Tonelli over , measurability of the run, Jensen's inequality for a convex function on a convex set, and strong convexity of the subproblem. Proofs of any milestone are welcome, as are a general "conditional one-step bound to expectation over the run" lemma reusable by the other missions of this series.Many problems in statistical learning and signal processing minimize an expectation plus a regularizer or constraint , with access to only through samples . The standard tool is the stochastic (proximal) subgradient method, which replaces at the current point by a random linear function. Two other methods use richer local approximations: the stochastic proximal point method keeps the whole sampled loss , and the stochastic prox-linear method linearizes only the smooth inner map of a composite loss . The richer models are markedly less sensitive to the step size in practice.
Davis and Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) treat all three methods as instances of one scheme, stochastic model-based minimization: each step minimizes a sampled one-sided model of , plus , plus a quadratic penalty. Their main theorem (Theorem 4.3) concerns weakly convex problems. This mission formalizes the companion result for the strongly convex setting, Theorem 4.2: when the models lower-bound in expectation and is -strongly convex, the expected function gap at a nonuniformly weighted average of the iterates decays like . The weighting is the technique of Schmidt, Le Roux and Bach (2012) for the projected stochastic subgradient method; the paper extends it to the fully proximal, model-based setting (p. 23).
Work in with the Euclidean norm. The problem is
where is locally Lipschitz and is closed (its epigraph is closed) with nonempty domain . A function is -weakly convex if is convex; a negative modulus is -strong convexity.
Assumption B (p. 18) fixes a probability space , an open convex set , real constants , a measurable model on and a measurable such that:
Algorithm 4.1 (p. 19) starts at and, for , samples and sets
The strongly convex setting is and with , run with . Let be any minimizer of .
For every integer ,
together with integrability of the function inside the expectation. The paper prints ; see Formalization scope.
The result. Theorem 4.2 is the rate for a whole family of stochastic methods at once: the stochastic proximal point, prox-linear and proximal subgradient methods all satisfy Assumption B (§4.2 of the paper). The rate is in function values at an explicit averaged point, with explicit constants, and needs neither smoothness of nor bounded subgradients of : the regularizer enters only through the strong convexity of the subproblems. The order is the one Schmidt, Le Roux and Bach obtained for the projected stochastic subgradient method; Theorem 4.2 extends it to models that are not linear and to a general closed .
Formalizing it. The result is proved in the paper; it is not formalized anywhere to our knowledge. Formalizing it pins down the exact constant (the printed one does not follow from the paper's lemmas; see below), the measure-theoretic content of "iterates generated by Algorithm 4.1" (a measurable selection of the argmin, the product measure of the samples, conditional expectation as an integral over one fresh sample) and the integrability that the expectations presuppose. The one-step estimate (4.8) is shared with mission 4 of this series (Theorem 4.1, convex setting); a proof of it serves both.
The telescoping that turns the one-step bound into the rate is elementary once the weights are chosen. The work lies in two places. First, (4.8) itself: it combines the strong convexity of the subproblem, the one-sided accuracy (B2) used in expectation, the Lipschitz bound (B4) at the random point (so the exceptional null set must not depend on that point), Cauchy–Schwarz, and Lemma 4.1. Second, the passage from one step with held fixed to expectations over the whole run: this needs the independence of from (Fubini on the product measure) and integrability of , and along the run, none of which is stated on the page. A natural first attempt, bounding at the average by the average of before checking that the average lies in , is valid only because the weights sum to one and is convex by (B3).
EuclideanSpace ℝ (Fin d). The extended-valued is encoded by its domain D and its real values on D; closedness is closedness of . -strong convexity is -weak convexity: convexity of on D.Measure.pi; expectations are Bochner integrals, and every bounded expectation comes with an integrability conclusion, so a junk value cannot make a bound hold. in (4.8) is the integral over one fresh sample with held fixed.Many stochastic models use a process whose response to a disturbance depends on the time elapsed since that disturbance. An ordinary stochastic differential equation uses only the current state and instantaneous coefficients. A stochastic Volterra equation instead weights its past drift and noise through a convolution kernel. Such equations include the constant kernel as a familiar limiting case, while singular or decaying kernels allow different memory patterns. The paper Affine Volterra processes studies this class to obtain non-Markovian models that retain tractable affine transform formulas. Before any transform can be used for a nonnegative state variable, the underlying equation must actually admit a solution that stays nonnegative. Abi Jaber, Larsson and Pulido, §§1–3.
The mission focuses on the paper's existence and invariance theorem, Theorem 3.6 of the pinned preprint. It is a separate question from uniqueness or explicit transforms: the coefficients are only continuous with linear growth, so classical contraction arguments for Lipschitz coefficients do not directly settle it. The proof also has to preserve the boundary of the nonnegative orthant despite a drift and noise term that depend on the entire past. Abi Jaber, Larsson and Pulido, Theorems 3.3–3.6.
Fix dimensions . The kernel is a deterministic function from nonnegative time to real matrices. The drift maps to , and the diffusion coefficient maps to real matrices. Given a deterministic initial state and an -dimensional Brownian motion , a continuous adapted process solves
The deterministic and stochastic terms are matrix-vector convolutions: an event at time has an effect at time weighted by . A weak solution is allowed to choose its stochastic basis and Brownian motion. A strong solution is adapted to the completed filtration generated by its prescribed Brownian motion. All bases satisfy the usual completeness and right-continuity conditions. The equation is read at each fixed time almost surely, with having continuous sample paths. Abi Jaber, Larsson and Pulido, (1.1), §3.
The paper's condition (2.5) asks each scalar kernel entry to be locally square-integrable and to satisfy two estimates of order as : the integral of its square over , and the squared difference between its time shift by and itself over each finite interval. The exponent satisfies and may differ by entry. For the goal, is diagonal. Each diagonal entry is nonnegative, nonzero, nonincreasing and continuous on positive time. Its resolvent of the first kind is a nonnegative measure whose convolution with is the constant one; condition (3.4) also requires the interval mass to be nonincreasing in for every . Abi Jaber, Larsson and Pulido, (2.5), (2.13), (3.4).
The goal is Theorem 3.6. Write . Suppose is diagonal and satisfies (2.5) and (3.4) componentwise. Suppose and are continuous, satisfy , and obey the boundary condition for every :
Then the target is
The milestone list records the paper's moment bound, strong existence for Lipschitz coefficients, and general weak existence with a first-kind resolvent. They are numbered results from the same preprint and establish distinct parts of the existence framework. Abi Jaber, Larsson and Pulido, Lemma 3.1 and Theorems 3.3, 3.4, 3.6.
The conclusion says more than finite-time nonnegativity of a proposed process: it asserts that a stochastic basis, Brownian motion and continuous solution actually exist for every nonnegative initial condition under the stated kernel and boundary assumptions. This supports later use of the affine transform results on state spaces with nonnegative coordinates. The paper treats this existence theorem as one of the main inputs to its square-root and rough-volatility examples. Abi Jaber, Larsson and Pulido, §§3, 6.
The theorem is already proved in the source paper. The formalization task is to state and eventually verify that known result in Lean, including the exact memory-kernel condition and the stochastic basis chosen by weak existence. The published Brownian and Itô-integral definitions are reused. A verified solution would leave reusable definitions for Volterra kernels, first-kind resolvents, and weak convolution equations, as well as machine-checked statements for the supporting existence theorems.
For Lipschitz coefficients, the paper obtains a unique strong solution. The goal permits only continuous coefficients of linear growth. Approximating them by better-behaved coefficients does not by itself guarantee that a limit solves the original convolution equation or remains in the nonnegative orthant. The stochastic convolution depends on the full history through , and the boundary condition must be propagated through that memory. A direct appeal to an ordinary SDE invariance theorem therefore does not cover the claim. The first-kind resolvent and the monotonicity in (3.4) are central to the stated assumptions. Abi Jaber, Larsson and Pulido, proofs of Theorems 3.4 and 3.6.
Lean uses EthierKurtz.SDEState d, a Euclidean -vector, for states; real matrices for and ; nonnegative real process time; and real arguments for deterministic kernels and interval integrals. Local membership is componentwise, which is equivalent to membership under any norm on the finite-dimensional matrix space. The matrix norm in linear growth is the Euclidean operator norm. The big- bounds in (2.5) are taken as tends to zero from the right. Each diagonal kernel has its own exponent and its own positive resolvent measure. A general matrix first-kind resolvent is encoded entrywise as the difference of two measures finite on compact positive-time intervals, so it may have infinite total mass.
The weak-solution predicate existentially quantifies the stochastic basis, Brownian motion and continuous process. Each stochastic convolution has a witness satisfying the published Brownian Itô relation; an unconstrained process cannot witness the equation. Drift terms carry interval integrability, avoiding a default-zero value for a nonintegrable integral. The stochastic basis is complete at time zero and right-continuous. The goal asserts orthant membership at every fixed time almost surely; continuous paths yield an orthant-valued version. The zero-time equation and empty-index cases are included. Contributions that formalize stochastic-convolution continuity, compactness of path laws, first-kind resolvent calculus, or invariance of the orthant are in scope.
Makespan minimization on identical parallel machines, , asks to assign jobs with processing times to machines so that the largest machine load is as small as possible. It is strongly NP-hard, and the question has long been how fast a -approximate schedule can be found. After rounding and scaling, a guess of the optimal makespan becomes a constant, the job sizes take only distinct values, and the problem becomes an integer program over machine packings: the configuration IP.
A short history of the running times for this problem:
Fix , a vector of job sizes and a capacity . The knapsack polytope is , and a configuration is an integral point of it:
A configuration describes one machine: jobs of size , of total load at most . The support of a vector is the set of its nonzero coordinates, . Throughout, . A configuration is simple if and complex otherwise; is the set of complex configurations.
Given the number of jobs of each size and the number of machines, the configuration IP [conf-IP] asks for multiplicities , one per configuration, with
Its LP relaxation [conf-LP] replaces by . The support of a solution is .
If [conf-IP] is feasible, it has a feasible solution with
A solution with these three properties is called thin.
The result. Theorem 1 says that, up to machines, every feasible configuration IP can be solved using simple configurations only. There are simple configurations, far fewer than configurations in general, so an algorithm can guess the support of a solution among a much smaller family. This is what yields the EPTAS for , and through the same structure PTASs for and for -norm and max–min objectives. Corollaries 5 and 6 are structural facts about knapsack polytopes in their own right: the integer hull has only simple vertices, and the configuration LP can be restricted to simple configurations.
Formalizing it. The results are proved in the paper; none of them has a machine-checked proof that this mission knows of. The development produces a reusable formal model of configurations and of the configuration IP and LP, a formal Eisenbrand–Shmonin support bound for this IP (a Carathéodory-type statement for integer cones that recurs across integer programming), and the sparsification lemma with its potential-function argument. The constants and are the paper's and are stated exactly.
The obvious argument applies the sparsification lemma repeatedly, replacing any complex configuration used twice by two configurations of smaller support, and then shrinks the support with the Eisenbrand–Shmonin exchange. The second step can undo the first: the exchange moves weight between configurations and may raise the multiplicity of a complex configuration above one again, so alternating the two steps has no evident termination measure. A proof has to control both properties at once. The counting behind the support bound needs the explicit inequality for every , which must be carried out with the exact constants rather than up to .
Fin d → ℕ with ; solutions of [conf-IP] are finitely supported functions (Fin d → ℕ) →₀ ℕ vanishing outside , and solutions of [conf-LP] are finitely supported real-valued functions, nonnegative and vanishing outside .Real.logb 2 and every bound is a real inequality; no floor is taken.Set.extremePoints). The asymptotic count of Corollary 5 is replaced by the explicit bound of its proof, with the added hypothesis (at the explicit bound is while ).The goal theorem refers only to [conf-IP], its solutions, supports and the simple/complex split; it does not mention the potential, the matrix or a minimality assumption, so it cannot be discharged by choosing a special solution in the hypotheses.
Needed infrastructure: finite sums over Finsupp, the pigeonhole principle on finsets, elementary bounds on Real.logb, and, for Corollaries 5 and 6, convex hulls and extreme points of finite sets in . The definitions of configurations and of the configuration IP/LP are reusable for other configuration-IP papers (bin packing, cutting stock, scheduling). Contributions of auxiliary lemmas on supports of integer conic combinations are welcome.
Many problems in statistics, signal processing and machine learning minimize an expected loss that is neither smooth nor convex: robust phase retrieval, blind deconvolution, covariance estimation with the loss, training of networks with ReLU activations, and composite problems with convex and smooth . A common structural feature of these objectives is weak convexity: adding a quadratic makes the function convex. For such problems the classical stochastic algorithms — the stochastic proximal point method, the stochastic prox-linear method, and the stochastic proximal subgradient method — were used in practice long before any nonasymptotic complexity guarantee was available for them.
Damek Davis and Dmitriy Drusvyatskiy (arXiv:1803.06523, SIAM J. Optim. 29(1), 2019) gave such guarantees for all of these methods at once. They abstract each method as minimization of a stochastic one-sided model of the objective, and prove that the expected squared gradient of the Moreau envelope at a randomly selected iterate decays at rate , i.e. a sample complexity of . This mission formalizes that main theorem (Theorem 4.3) and the lemmas its proof uses.
Timeline. Nurminskii (1973, 1974) showed that when the sample losses are -weakly convex and there is no regularizer, the stochastic subgradient method converges subsequentially to stationary points almost surely; no rate was given. Ghadimi and Lan (2013) proved complexity for smooth nonconvex stochastic problems. Davis and Grimmer (arXiv:1707.03505, 2017) gave a rate for a proximally guided variant of the stochastic subgradient method on weakly convex problems. Davis and Drusvyatskiy (2018) obtained the complexity for the basic proximal stochastic subgradient method and, through the one-sided model framework, for the stochastic proximal point and prox-linear methods.
Work on with the Euclidean norm. An extended-valued function has domain and is closed when its epigraph is closed. A function is -weakly convex when is convex. For the Moreau envelope and proximal map are
The problem is with closed and locally Lipschitz, where is accessible only through a random model , . Assumption B asks for constants , an open convex and a measurable such that: and on (one-sided accuracy); is -weakly convex for almost every ; and .
Algorithm 4.1 fixes and parameters , draws i.i.d. samples , and sets
It returns , with drawn with . With it is the stochastic proximal point method; with a linearization it is the proximal stochastic subgradient method; with it is the stochastic prox-linear method.
and for with ,
The result. By Lemma 2.2, , and the proximal point satisfies and . A small envelope gradient therefore certifies that is close to a nearly stationary point. Theorem 4.3 gives this certificate, with explicit constants, for every algorithm fitting Assumption B, in particular the first complexity bounds for the stochastic proximal point and stochastic prox-linear methods on weakly convex problems. Companion results in the same paper (Theorems 4.1 and 4.2, separate missions) specialize to convex and strongly convex models.
Formalizing it. The theorem is proved on paper; no machine-checked version exists, on this platform or in Mathlib, of Theorem 4.3, of Lemma 2.2 for extended-valued weakly convex functions, or of the one-sided-model framework. A formalization yields a reusable Moreau-envelope library for weakly convex functions with constraints (via the domain of ), and a template for iterate-level stochastic analysis on product probability spaces.
The algebra of each step is short; what is hard is making it rigorous. First, Lemma 2.2 must be proved for extended-valued closed functions: existence and uniqueness of the proximal point need strong convexity of the subproblem together with lower semicontinuity and a quadratic minorant, and differentiability of the envelope is not a consequence of a generic envelope theorem. Second, the conditional expectations in Lemma 4.2 must be realized on the product space of samples, with integrability of , and established along the iterates rather than assumed; the paper takes all of these for granted. Third, Assumption B gives the Lipschitz bound (4.2) only in one direction and only almost surely, and the argmin of Algorithm 4.1 exists only almost surely, so every pointwise step must be carried through null sets that depend on the current iterate.
EuclideanSpace ℝ (Fin d). The extended-valued (and ) is a pair ; closedness, weak convexity, the envelope (an infimum over ) and proximal points are defined in this encoding. The envelope parameter is written lam.A seller with several goods and a single buyer is the smallest setting in which multi-dimensional mechanism design differs from the one-good theory. For one good, Myerson's theorem (Myerson 1981) says the optimal mechanism posts a price. For two or more goods the optimal mechanism may use lotteries, may be non-monotone in the buyer's values, and is in general not known in closed form. Practitioners nevertheless use simple mechanisms, and the question that Hart and Nisan (arXiv:1204.1846v3) ask is quantitative: what fraction of the optimal revenue does a simple mechanism guarantee?
This mission concerns the simplest mechanism of all, bundling: one posted price for the set of all goods. When the goods are independent and identically distributed, bundling is known to become nearly optimal as the number of goods grows for a fixed distribution (Armstrong 1999; Bakos and Brynjolfsson 1999). That limit is not uniform over distributions. Theorem D of Hart and Nisan gives the uniform guarantee: for every and every distribution, bundling i.i.d. goods earns at least of the optimal revenue.
Timeline. Armstrong (1999) and Bakos–Brynjolfsson (1999) proved the asymptotic optimality of bundling for a fixed distribution. Hart and Nisan circulated the first version of this paper in 2012 (EC 2012), proving Theorems A–D; the version formalized here is arXiv:1204.1846v3 (2017), published in J. Econ. Theory 172 (2017). Li and Yao (2013) later improved separate selling for i.i.d. goods to , and Babaioff, Immorlica, Lucier and Weinberg (2014) showed that the better of separate selling and bundling is a constant-factor approximation for independent goods.
There are goods and one buyer with additive valuation , drawn from a known distribution. A mechanism assigns to every reported valuation an allocation vector (the probabilities of receiving each good) and a payment . The buyer's payoff is . The mechanism is incentive compatible (IC) if for all , and individually rational (IR) if for all . For a random valuation , the expected revenue is and the optimal revenue is
For one good, . The bundled revenue is the one-good revenue of the total value, , and the separate revenue is .
" i.i.d. goods" means that are independent with a common law on . Write and .
Two auxiliary objects appear in the milestones. A real random variable is stochastically dominated by if for every . The equal-revenue (ER) law is that of with for . The constant is the unique real solution of .
The constant is absolute: it is chosen before and before the distribution. This is the statement as printed; it fixes neither the constant nor the base of the logarithm.
The milestones follow the paper's proof: Myerson's formula (1); monotonicity of one-good revenue under domination (Proposition 11); the ER characterization (Lemma 20) and the tail of a weighted sum of two ER goods (Lemma 21); (Proposition 24); for two independent goods (Proposition 13 (i)); for i.i.d. goods (Proposition 14 (ii)); the decomposition Theorem 7; the power-of-two bound ; monotonicity of and in ; and the explicit bound above.
Theorem D says that for identically distributed goods the gap between the simplest mechanism and the optimal one grows at most logarithmically in the number of goods, uniformly over all distributions, including heavy-tailed ones with infinite mean. The i.i.d. hypothesis is essential: for independent goods with different distributions bundling can recover only a fraction (Example 27 of the paper). Together with Theorem C (separate selling, ) it places the two simple mechanisms on a common scale, and the decomposition Theorem 7 it rests on is a general tool for independent groups of goods.
The result is proved in the paper; no machine-checked version is known to exist. A formalization adds: a Lean model of multi-good mechanisms with IC, IR and expected revenue in the extended reals; a checked version of Myerson's one-good formula for arbitrary laws on ; the equal-revenue law and its two-good convolution; and a checked reduction from the decomposition theorem to the logarithmic bundling guarantee. Shorter arguments or a better constant are also welcome.
The obvious argument fails at the first step: revenue is not monotone in the valuation for two or more goods (Hart and Reny 2015), so one cannot bound by replacing each good by a dominating ER good. Every comparison therefore has to pass through one-dimensional quantities, and the multi-good step (Theorem 7) is a statement about expectations of a mechanism's payments conditioned on an independent block of goods. Proposition 14 (ii) must handle distributions where no optimal one-good price exists and may be infinite (the paper's proof speaks of "an optimal price"). Proposition 24 is an exact evaluation whose answer is defined only implicitly, through . The induction itself must track how block sums of i.i.d. goods are again i.i.d.
Valuations are laws: a -good random valuation is a probability measure on Fin k → ℝ≥0, and i.i.d. goods with law form Measure.pi (fun _ : Fin k => ν). Two independent groups have the product law on the disjoint union of their index types (jointLaw); the two-good statement Proposition 13 (i) uses this encoding on Unit ⊕ Unit. A mechanism is a pair of functions; the admissible class requires , IC, IR, and a measurable payment rule, the last being the without-loss-of-generality pin of the paper's footnote 12. The expected revenue of one mechanism is an EReal difference of two lower integrals, never a Bochner integral (which would be for non-integrable payments). is a supremum in ℝ≥0∞, so infinite revenues are represented. is a real parameter with the hypothesis , not a Lambert- value. Logarithms are natural in Theorem D and base 2 (Real.logb 2) in the proof's explicit bounds, as printed; every statement with a logarithm keeps .
The paper states Theorem D as a lower bound on an infimum of ratios ; the formal goal is the multiplicative inequality, which agrees with it wherever the ratio is defined and requires when . A formalization in which may depend on or on the distribution, or in which is computed with a Bochner integral, would trivialize the statement and is ruled out by the binder order and the definitions above.
The definitions are a mission-local copy of the model shared by this series (missions 1–5), so they can be merged later. Not posed here: Theorem C, Proposition 25, Corollary 23, Lemma 22, Example 32, the GFOR notation, and the asymptotic optimality of bundling (Appendix A.5). Proofs of any milestone are welcome, as are reusable lemmas on posted prices, stochastic domination of sums of independent variables, and binomial medians.
The generalized Turán number is the largest number of copies of a graph in an -vertex graph containing no member of a family . With it is the classical Turán number; the systematic study of general began with Alon and Shikhelman (2016), and cycles are its most studied case: Bollobás and Győri bounded , and Gerbner and Palmer determined .
Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (J. Combin. Theory Ser. B, 2020; arXiv:1712.07079), count copies of one cycle in graphs avoiding another. For even cycles they show . Most extremal constructions there are bipartite, so they also study the bipartite generalized Turán number. For the first non-trivial pair, six-cycles in a graph avoiding eight-cycles, they determine its leading term exactly. This mission formalizes that result, Theorem 12 of the paper.
All graphs are finite and simple. A -cycle is a cycle with vertices. A copy of in is a subgraph of isomorphic to ; is the number of copies, so a cycle is counted once regardless of its starting point and direction. A graph is -free if no subgraph of it is isomorphic to (induced or not). A graph is bipartite if its vertices can be split into two classes and with every edge joining to .
The proof works with a fixed bipartition of a -free graph and uses the following notions.
In Lean, is exBip n (cycleGraph 6) {8}, and is Mathlib's copyCount.
This is two-sided: for some constant and all large .
Theorem 12 is the only case of the paper where a bipartite generalized Turán number of two even cycles is determined up to a lower-order term. Theorem 10 gives the order in general, and Remark 2 gives bipartite upper and lower bounds whose ratio tends to 1 only as . Theorem 12 settles exactly. The authors conjecture that the non-bipartite number has the same asymptotics, but this is open. The argument also links graph counting to Berge hypergraphs: Claim 7 reduces the fat 6-cycles to a Berge--free hypergraph, whose total edge size is controlled by Corollary 7.
Theorem 12 is proved in the paper. As far as a search of the Prove2Me catalogue shows, neither it nor any of its claims has a machine-checked proof. Formalizing it means:
The obvious bound fails. Every 6-cycle in a bipartite graph has three vertices in each class, and each pair of them has some common neighbours. If no pair had more than three common neighbours, each triple in would lie on at most six-cycles, giving roughly cycles, not . The leading constant needs two refinements. First, triples on more than cycles must be shown to be rare. Second, cycles through pairs with many common neighbours (fat pairs) must be bounded separately, by . That second bound is the main obstacle. A fat pair alone can lie on many cycles, so counting fat pairs is not enough. What makes the bound work is the near-disjointness of the common neighbourhoods (Claims 4–6) together with a hypergraph Turán estimate.
Vertices and copies. Graphs are SimpleGraph (Fin n), or a general finite type in milestones about a single graph. Copies are unlabelled (copyCount, the number of subgraphs isomorphic to ): has copies of , not .
Bipartiteness. In it is Colorable 2. In the milestones it is an explicit bipartition that excludes edges inside a class. -freeness is (cycleGraph 8).Free G.
The maximum. is a supremum of natural numbers over a nonempty finite set, since the empty graph is admissible. It is therefore a true maximum; a sanity file proves this.
Cycles inside the proof. Labelled 6-cycles are injective maps from with consecutive images adjacent. Claim 8 counts fat 6-cycles labelled, which changes only the constant.
Landau terms. Every is an explicit constant, quantified before and the graph. The goal uses Mathlib's IsBigO of against .
Corrections to the printed text.
Ruled-out encodings. Some encodings would make the statements trivial or wrong, and none of them is used:
Infrastructure. A complete development needs:
The Berge-cycle and -free bounds can be reused beyond this mission. Contributions are welcome at any level: proofs of individual claims, of Corollary 7, or the final assembly.
A seller who knows the distributions of a buyer's values for several goods can, in principle, design a mechanism that offers lotteries and prices conditional on the buyer's reported values. Finding the best such mechanism can be difficult even with two goods. Separate selling is much simpler: choose a one-good price for each item and let the buyer decide item by item. The question is how much revenue this simplicity can cost when the goods' values are independent. Hart and Nisan establish a guarantee that declines only with the square of the logarithm of the number of goods, even though the distributions need not be identical or bounded. Their result is Theorem C of Approximate Revenue Maximization with Multiple Items, stated on p. 7 and proved on p. 26.
The paper grew from the problem of comparing easy selling formats with fully optimal mechanisms. For one good, a posted price characterizes optimal revenue. With multiple goods, the choice of a mechanism becomes genuinely multidimensional: its allocation rule can correlate the disposition of the goods and use lotteries. The guarantee in this mission applies uniformly over all independent distributions on nonnegative valuations, so a seller does not need a regularity, density, or finite-moment assumption to use it.
There is one seller, one risk-neutral buyer, and goods. The buyer's valuation vector is ; receiving a set of goods gives the sum of the values of its members. The seller knows the joint law of the random vector , but not its realization. In this mission the coordinates are independent, with possibly different probability laws .
A direct mechanism consists of an allocation rule for each good and a real payment . At a truthful report , the buyer's payoff is . The mechanism is incentive compatible if truthful reporting is at least as good as every alternative report, and individually rational if for every . The seller's expected payment is its revenue. The optimal revenue is the supremum of revenue over such mechanisms. Payments are taken to be measurable, following footnote 12 on p. 12 of Hart and Nisan.
For one good, equals the supremum of over prices , as in display (1) on p. 12. The separate revenue is . The bundled revenue is , where the sum is treated as one good. Both formats are defined through one-good revenue, even when the full optimum can use multidimensional allocations.
The goal is the inequality form of Theorem C, with one constant that works for every number and every family of independent goods:
Here has law , and the joint law is their product. The paper phrases the headline as a guarantee for an approximation ratio; the displayed inequality is the form used in its proof on p. 26. It handles zero and infinite optimal revenues without introducing a ratio with an undefined denominator.
The milestone list records the one-good posted-price formula, monotonicity under first-order stochastic domination, the equal-revenue comparison of Lemma 20, Proposition 13(ii)'s comparison of separate and bundled revenue, the two inequalities of Theorem 7, and the two-good base case of Theorem A. It also records the power-of-two estimate and the zero-padding assertion stated in the proof of Theorem C. Each milestone is attached to its source page in the pinned preprint.
The theorem gives a distribution-independent performance floor for a mechanism that can be run using one price per good. It applies to unequal and unbounded independent distributions, for which expected values can be infinite while one-good optimal revenues remain finite. The comparison is with the best incentive-compatible and individually rational multi-good mechanism, including randomized allocations, rather than with another simple selling format. The result is proved in the 2017 preprint; the open work here is a machine-checked formalization of that known result and its selected supporting statements.
The formal development also supplies reusable objects: a law-based direct-mechanism model, extended-real expected revenue, product laws for independent groups of goods, and first-order stochastic domination of one-good laws. These are useful for other comparisons among separate selling, bundling, and optimal mechanisms in the same paper. The mission does not pose the paper's distinct i.i.d. bundling theorem, multi-buyer results, or tightness examples.
The main obstacle is that optimal multi-good revenue is not monotone in the values of the goods. Increasing each coordinate of a valuation vector does not, by itself, give a valid comparison between the optimal revenues of the two vectors' laws; Hart and Nisan, p. 23 explicitly warn against that inference. One-good revenue does have the needed monotonicity, but the full optimum can depend on how the goods interact in an incentive-compatible mechanism. Theorem 7 is a substantive bridge between these two regimes. Infinite expected values also make a real-valued integral or an ordinary ratio unsuitable for the general statement.
Goods are indexed by finite types, and valuations lie in . Each good's law is a probability measure; independence means the product law, while Theorem 7 allows dependence among coordinates within each of its two independent groups. A one-good law is represented by a singleton coordinate type. Revenue takes values in , and the expectation of a mechanism's possibly negative payment is represented in extended reals. The supremum defining optimal revenue ranges only over feasible, incentive-compatible, individually rational mechanisms with measurable payments. Theorem C quantifies before and the laws, and the restriction keeps the logarithmic coefficient in its stated domain.
The equal-revenue law is represented by the density on , mapped to nonnegative reals. First-order stochastic domination compares the upper-tail probabilities at nonnegative thresholds, which is equivalent to testing every real threshold for nonnegative valuations. A complete proof will need measure-theoretic facts about that law, the posted-price characterization, product measures, and operations on extended nonnegative revenue. Contributions to those reusable facts and to the selected milestone theorems are within scope.
The Turán number is the largest number of edges in an -vertex graph with no copy of . Its generalized version, introduced systematically by Alon and Shikhelman (JCTB 2016), replaces edges by copies of a second graph : is the largest number of copies of in an -vertex graph containing no member of the family . When both and the forbidden graphs are cycles, these numbers measure how many long cycles a graph can carry while some cycle lengths are excluded and they refine the Bondy–Simonovits even-cycle theorem (JCTB 1974), which bounds the number of edges of a -free graph by .
Gerbner, Győri, Methuku and Vizer (arXiv:1712.07079, J. Combin. Theory Ser. B 2020, DOI 10.1016/j.jctb.2020.05.005) study for cycles. Their Theorem 10 gives ; Theorem 14, the subject of this mission, adds a girth condition: when all cycles of length are forbidden together with , the order of magnitude of the number of 's is . The case answers the question of how many 's a -free graph of girth can have.
All graphs are finite and simple. A copy of a graph in is a subgraph of isomorphic to , and is the number of copies. is the cycle of length ; is the path on vertices (of length ).
For a set of integers, each at least , let ; a graph is -free if it contains none of these cycles as a subgraph. Write . The generalized Turán number is
For vertices , is the number of paths with edges between and . A pair is fat if , and a copy of is fat if all of its pairs of opposite vertices are fat.
The -theta graph joins two vertices by internally disjoint paths of length . For a graph , the theta- graph replaces each edge of by an -theta graph with and adds isolated vertices up to ; here for and for .
For integers and with ,
Both bounds are part of the goal; the constants depend on only.
Theorem 14 locates at for every admissible triple, so in graphs of girth forbidding one further even cycle (with ) caps the number of -cycles at the count achieved by a blown-up -cycle of long paths. The paper uses it to settle the order of magnitude of for every family with , and (Theorem 20), and its case recovers Theorem 10.
The result is proved in the paper; nothing here is open mathematically. To the best of a platform search (2026-10-08), no part of it is formalized: Mathlib has copyCount, cycleGraph and pathGraph, but no generalized Turán numbers, no theta graphs and no counting of paths between two vertices. The mission produces a machine-checked proof of the theorem and of the counting lemmas of §5, which are reusable for other generalized Turán problems with cycles.
The lower bound is an explicit construction, and its difficulty is bookkeeping: proving that a subdivided multigraph has no cycles other than those of lengths and , and counting the -cycles. The upper bound is the substance. A direct count of 's through codegrees, which works for , fails here because paths of length between a pair are not controlled by a single neighbourhood. The paper's route separates fat from non-fat cycles and runs a greedy multiplicity procedure; Claim 14 then grows a by an induction on the cycle length in steps of , which needs the precise intersection pattern of Claim 12 and the detour paths of Claim 13. For the argument goes through layered neighbourhoods and Lemma 27. The argument divides by , so for a different route (Theorems 10 and 11 of the paper) is needed.
Graphs are SimpleGraph (Fin n) for the extremal function and graphs on an arbitrary finite type for the lemmas. Copies are unlabelled (copyCount, subgraphs isomorphic to the pattern); and are Mathlib's cycleGraph a and pathGraph l. exCyc n H A is the supremum, over -free graphs on Fin n, of the copy count; the set is finite and contains the empty graph's count whenever every length in is at least , so it is a maximum. The forbidden family of the goal is Set.Icc 3 (2 * l - 1) ∪ {2 * k}, every length from to together with . , and are Mathlib's asymptotic relations along atTop, with constants fixed before and the graph. counts injective vertex sequences (paths, not walks). The theta graph thetaCycle n m l is an explicit graph on Fin n.
Added or pinned hypotheses, all disclosed in the items: in the goal (the page writes only ; at the family is empty and the statement fails); in Claim 12; where the page divides by ; Lemma 27 with the explicit bound of its proof, which is uniform in ; Claim 15 under the full family , which its proof needs. Claim 14 assumes only girth , not -freeness, since on the page its conclusion at is the contradiction.
The statements rule out the trivializing readings: the goal is two-sided, so an upper bound alone does not close it; exCyc is a genuine maximum, not a junk supremum; copies are unlabelled; the constants come before and the graph; the forbidden family contains all short cycles, not only .
A complete development needs path counting in graphs of large girth (uniqueness of short paths), layered neighbourhoods, the degeneracy argument of Lemma 27, a random bipartition argument for Lemma 25, and cycle structure in theta graphs. Contributions of any milestone, and of general-purpose lemmas on paths and cycles in SimpleGraph, are welcome.
An extremal graph question asks how many copies of one pattern can occur when other patterns are forbidden. When the counted pattern is a cycle, the answer depends strongly on which shorter cycles may occur. Excluding only an even cycle and excluding all cycles up to a given length are different constraints. The latter imposes a girth condition, meaning that nearby vertices cannot be connected by the many short alternative routes that otherwise create small cycles. For odd cycles, this makes a direct application of ordinary edge-count bounds inadequate: many graphs with relatively few edges can still arrange those edges into many copies of a fixed cycle.
Gerbner, Győri, Methuku and Vizer study generalized Turán numbers for cycles and paths. Their Theorem 17 bounds the number of copies of a particular odd cycle when every cycle of lengths through , and one further even cycle of length , is forbidden. The lower and upper exponents differ; the theorem supplies a nontrivial interval for the possible growth rate rather than an exact asymptotic formula. The preprint, Theorem 17 is the source used here; its printed page numbers agree with its PDF pages.
Write for the simple cycle on vertices. For a set of integers at least , let . A graph is -free if no member of the family occurs as a subgraph of . The copies need not be induced: an extra edge between vertices of a copy does not erase that copy. When , write for this family. Thus excludes every cycle of length from to and also excludes the single cycle . This notation follows §1 of the paper.
For graphs and , let be the number of unlabelled copies of in : subgraphs of isomorphic to , counted once each. The generalized Turán number is
The graph with no edges is eligible for the forbidden families in this mission, and the finite vertex set makes the maximum well defined. For a vertex and integer , is the set of vertices whose graph distance from is exactly . Vertices in another connected component lie in no with finite .
The lower-bound milestone also uses a hypergraph, a set of hyperedges that are subsets of a common vertex set. It is -uniform when every hyperedge has exactly vertices. A Berge cycle of length alternates distinct vertices and distinct hyperedges; consecutive vertices lie in their connecting hyperedge. Hypergraph girth at least means that no Berge cycle has length less than . These definitions are used in Theorem 29 and §6.2.
Fix integers . The goal is the two-sided statement of Theorem 17, p. 7:
Both estimates concern with and fixed. The paper does not claim that either exponent is optimal for every pair , and these formulas should not be read as an equality of growth rates.
The milestones record the source statements needed on the two sides. Theorem 29 gives -uniform hypergraphs of prescribed Berge girth with at least hyperedges. The lower-bound paragraph of §6.2 turns such hypergraphs into graphs with many copies. Lemma 27 bounds the edges of a graph under a path-restricting partition condition. The local layer identity and Claim 18 control edges in the distance layers and . The final milestone is the low-cycle-vertex conclusion from the paper's deletion passage on p. 28.
The upper exponent is strictly below , so the theorem rules out quadratic growth for this generalized Turán number under the stated forbidden family. The lower exponent shows that the number of permitted odd cycles nevertheless grows faster than linearly. Together they locate the problem between two explicit power laws. These statements belong to a wider set of cycle-count results in the paper, where changing the forbidden family or the parity of its extra cycle changes the resulting bounds; see Theorems 17 and 18.
The paper proves these bounds. The work here is to state its objects and claims so that Lean can check future proofs: the maximum over admissible graphs, unlabelled cycle counts, Berge-cycle girth, and graph distance layers. The present proposal supplies proof targets; their Lean declarations have placeholders for proofs. The finite graph and hypergraph definitions can also serve later formalizations of generalized Turán and girth questions. The exact growth rate between the two exponents is left open by this theorem.
Counting cycles from an ordinary upper bound on the number of edges loses the relation between a cycle and its position around a vertex. The no-short-cycle condition constrains individual distance layers, but a layer can still contain edges that close a . Controlling those edges uniformly across all graphs and vertices is the central issue in the upper bound. A bound with a constant chosen after seeing the graph would say little about the asymptotic maximum; Claim 18 instead requires a constant depending only on and . The lower side has a different requirement: the construction must preserve both the abundance of odd cycles and every exclusion in . The precise assertions are in §6.2, pp. 27–28.
Graphs on vertices are represented as simple graphs on , and is Mathlib's cycle graph. A copy is a subgraph isomorphic to , counted without labels. The extremal number is the supremum of its finite, nonempty set of attainable natural-number counts; in this setting that supremum is the paper's maximum. Distance layers use extended graph distance, which assigns unreachable pairs infinity. The family of forbidden lengths is exactly ; it does not omit any short cycle.
The hypergraph representation is a finite set of distinct finite vertex sets. Berge-cycle existence requires injective lists of vertices and hyperedges, and girth at least is expressed by absence of lengths through rather than a numerical infimum with an exceptional value on acyclic hypergraphs. Theorem 29's threshold is chosen after and before . Claim 18's constant is chosen after and before the graph or vertex. The upper and lower asymptotic bounds are both present, with real exponents; neither is replaced by a one-sided or purely existential statement.
Lemma 27 is given with the explicit edge bound from its proof, uniform in the number of partition classes. The final deletion milestone uses an existential constant because the page mixes several powers of its intermediate constant ; this is recorded in the accompanying audit notes. A complete proof development needs Mathlib's simple-graph copies, paths, graph metric, finite-set counting, and asymptotic notation, plus the hypergraph interface defined for this mission. Proofs of the goal and any of these milestones are welcome.
In a cost sharing game (or, symmetrically, a revenue sharing game) self-interested players each pick a set of resources, every resource generates a welfare that depends on who uses it, and a distribution rule splits that welfare among the users. Network formation, atomic routing, coverage and distributed-control problems all fit this model (Anshelevich et al. 2004; Marden and Wierman, Distributed welfare games, 2013; see §2 of the paper). The designer controls only the distribution rule, and the first requirement on a rule is that the games it induces have a pure Nash equilibrium; without one, equilibrium-based efficiency guarantees say nothing.
Which rules guarantee equilibria? The Shapley value and its weighted and generalized-weighted versions do, because they induce potential games (Hart and Mas-Colell 1989). Chen, Roughgarden and Valiant (2010) and Marden and Wierman (Overcoming the limitations of utility design for multiagent systems, 2013) showed that, among budget-balanced rules, these are the only ones that work for every welfare function, by exhibiting one worst-case welfare function (Proposition 1 of the paper, p. 9). Marden and Wierman (Distributed welfare games) also showed that when players may choose only one resource, other budget-balanced rules can work. That left open what happens when the designer knows the welfare functions in advance, and whether dropping budget-balance enlarges the set of good rules. Gopalakrishnan, Marden and Wierman 2014 answered both questions: for any fixed set of welfare functions, with or without budget-balance, the equilibrium-guaranteeing rules are exactly generalized weighted Shapley values on suitable ground welfare functions.
Players are with ; resources are with . A local welfare function is and a distribution rule is , where is the share of player when sharing with the coalition (and for ). Each player has a nonempty action set . In an allocation , the users of are and player receives
Resources with equal welfare functions use the same rule. For a nonempty set of welfare functions, is the class of all such games with every , any number of resources and any action sets. A rule is budget-balanced for if .
A weight system consists of positive weights and an ordered partition of into priority classes. For nonempty , with the first class meeting . With the basis coefficients , the generalized weighted Shapley value is
The distributed welfare of a rule is , display (10).
with the distributed welfare of . One weight system serves all of .
The "if" direction (Appendix A, p. 16). For a single and a budget-balanced guaranteeing equilibria: when contains no contributing coalition (Lemma 1) and for non-contributing (Lemma 2); (Lemma 3). The basis rules of the recursion (27) are budget-balanced for the inclusion functions (Lemma 5), recover (Lemma 7), obey an inclusion–exclusion principle (Corollary 1), and are generalized weighted Shapley basis rules (Lemma 8). Across welfare functions the basis shares are consistent pairwise (Lemma 9) and around cycles (Lemma 10); the induced relation on players is a partial order modulo equivalence (Lemma 11), and one universal weight system replaces all (Lemma 13).
Proposition 2: for welfare functions normalized by , iff and . Theorem 2: the same characterization with generalized weighted marginal contributions on .
The theorem settles the design space completely: a designer who wants equilibria in every game over known welfare functions must use a generalized weighted Shapley value, and the only freedom is the weight system and the ground welfare functions, which control budget-balance. Since these rules induce (generalized weighted) potential games, potential games are necessary for guaranteed equilibrium existence in this model, and computing shares inherits the exponential cost of Shapley values. Theorem 2 gives the marginal-contribution form, which needs one marginal contribution per share.
The paper proves Theorem 1 with a full appendix of counterexample constructions; none of it has a published machine-checked proof. The mission asks for a Lean proof of the characterization, of the reusable structure behind it (necessary conditions, basis decomposition, inclusion–exclusion for basis rules, consistency of weight systems), and of the Shapley–marginal-contribution correspondence.
The "if" direction is a potential argument. The "only if" direction is not: every necessary condition is proved by building, from a hypothetical violation, a specific game with no equilibrium, and the games grow more elaborate as the conditions do. Lemma 8 needs the inclusion–exclusion principle to isolate a single basis share, using many weighted copies of resources; Lemma 10's proof combines best-response cycles over welfare functions and is partly omitted on the page ("We omit the proof for brevity", p. 51), so it is the hardest milestone. A tempting shortcut, applying the worst-case result of Chen et al. and Marden–Wierman (Proposition 1, p. 9), fails: it uses one worst-case welfare function, while here is arbitrary and may not contain it.
Players are Fin n, resources Fin m, an action is a Finset (Fin m) (the empty action is allowed). The family of rules is one function f : Welfare n → Rule n, which encodes that equal welfare functions get equal rules. GuaranteesPNE 𝕎 f quantifies over every m > 1, every assignment Fin m → 𝕎 (repetitions allowed: the counterexamples rely on many copies of one welfare function) and every family of nonempty action sets. A weight system stores a block index Fin K per player (empty blocks allowed) and positive weights. Rules are compared only at . Contributing coalitions exclude (Appendix A's normalization ). The recursion (27) divides by and is used only for contributing ; where it reads with , the paper's convention off is a hypothesis.
The ground welfare in Theorem 1 is the distributed welfare (10), written out, never an arbitrary function: an existentially quantified ground welfare would make the right side easier and the theorem a different one. The weight system is quantified before the welfare functions, and empty action sets are excluded; with them no game would have an equilibrium and the theorem would claim that no rule is a Shapley value.
Disclosed readings: Lemma 11's "partial order" is antisymmetry modulo the equivalence , as the proof states; in (74) the first block is read on as its positive-share block . Proposition 2 carries so that the paper's basis support, which ranges over all coalitions, agrees with the local support of nonempty coalitions.
A complete development needs: finite games and pure equilibria on resource-selection models, Möbius inversion on Finset lattices, the potential argument for generalized weighted Shapley values (shared with the companion mission on generalized weighted potential games), and counterexample games built from copies of resources. The game model and the basis-rule recursion are reusable for other cost-sharing results. Proofs of any milestone, and alternative arguments for the necessary conditions, are welcome.