Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The proximal stochastic subgradient method is the workhorse of large-scale learning: to minimize a regularized population risk with , it samples a data point, takes a step against a sampled subgradient of , and applies the proximal map of the regularizer . Its sample complexity is classical for convex problems ( samples for function accuracy ) and for smooth nonconvex problems ( samples for gradient norm , Ghadimi–Lan 2013). For problems that are both nonsmooth and nonconvex, however, no complexity bound was known for any reasonably broad class before Davis–Drusvyatskiy 2019.
Many such problems — robust phase retrieval, nonlinear least squares with an loss, conditional value-at-risk minimization with smooth losses, covariance estimation — are weakly convex: they become convex after adding a quadratic . This mission formalizes the complexity guarantee of Davis and Drusvyatskiy for the proximal stochastic subgradient method on weakly convex problems.
Timeline. Nurminskii (1973) showed that for weakly convex and the stochastic subgradient method has limit points that are stationary, without a rate. Ghadimi and Lan (2013) proved the rate for smooth . Davis and Drusvyatskiy (arXiv 2018, SIAM J. Optim. 2019) proved the first rate for the proximal stochastic subgradient method under weak convexity, measured by the gradient of the Moreau envelope; this is Theorem 3.4 of their paper.
Work in with the Euclidean norm. Let be closed (its epigraph is closed) and convex, with nonempty domain , and let be -weakly convex: is convex. Set .
The subdifferential of a function at a point of its domain is the set of vectors with as ; it is empty off the domain. For the Moreau envelope and the proximal map 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 starts at and, for , samples and sets . It returns with drawn from with probability .
For and stepsizes ,
and with , ,
In the order the proof uses them: Lemma 2.1 (subdifferential characterization of weak convexity), the existence of with (§3.2), Lemma 3.2 ( is a proximal point of ), Lemma 3.3 (one-step contraction towards ), Lemma 2.2 (the envelope is with ), and the one-step descent estimate (3.14).
The result. A small certifies that is within of a point with and . Theorem 3.4 therefore gives a sample complexity of for reaching an -nearly stationary point, matching the smooth rate, for a method that is run in practice without modification. The underlying observation — the method is an approximate descent method on the Moreau envelope — is reused in the paper's model-based analysis (Theorem 4.3) and in subsequent work on stochastic nonsmooth nonconvex optimization.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A complete development produces reusable infrastructure: the Fréchet subdifferential of extended-valued functions, weak convexity and its subgradient characterization, Moreau envelopes of weakly convex functions and their differentiability, nonexpansiveness of convex proximal maps, and the bookkeeping of iterates driven by i.i.d. samples under a product measure.
The obvious argument — show that decreases in expectation — fails: neither nor need tend to zero, and the latter is discontinuous in . Progress must be measured on the Moreau envelope, which requires comparing the iterate with the proximal point of , not of . In Lean, the heaviest single ingredient is Lemma 2.2 (differentiability of the envelope of an extended-valued weakly convex function), and the direction of Lemma 2.1, which in the paper rests on Rockafellar–Wets' characterization of convexity by monotonicity of the subdifferential.
EuclideanSpace ℝ (Fin d). An extended-valued function is a pair (domain , real values on ); closedness is closedness of . The subdifferential is the published regular subgradient NonconvexSplitting.Shared.IsRegularSubgrad of the -extended lift.prox a z is a function constrained, for every , to return a minimizer over of ; this determines it uniquely.Distributed programs often establish a conversation among several participants, then exchange messages without waiting for each send to be received. A specification of each participant in isolation does not by itself say whether their actions will fit together. Multiparty asynchronous session types address this by describing the intended conversation once as a global type and checking each participant against a projected local type. Honda, Yoshida and Carbone develop this calculus and state a progress result for a restricted class of well-typed programs: if execution has not finished, another reduction is available. The restriction matters because independently initiated sessions can interfere and deadlock even when their communications are individually typed. Honda, Yoshida and Carbone (2016)
A program is a process before execution: it contains no message queues or restricted session channels, even after structural rearrangement, and it has no free session channels or process variables. A requester on a shared name starts a session with participants numbered through . Each participant receives the same vector of fresh session channels. An asynchronous send appends a message to the appropriate FIFO queue; a receive reads the queue head. Requests, sends, delegations and selections are emitting prefixes. Accepts, receives and branches are receiving prefixes. The reduction relation includes these communications, conditionals, guarded declaration unfolding, and closure under parallel composition, restriction and structural congruence . Honda, Yoshida and Carbone (2016), Figs. 1–3 and Def. 2.1
A global type specifies which numbered role sends a value or choice to another role on channel index , followed by the remainder of the conversation. It may also contain parallel components and guarded recursion. A partial projection gives role its endpoint type. Global types must be linear: causally ordered actions on a common channel have both input and output dependency chains. A global type is coherent when it is linear and projects to all its participants; the runtime typing is coherent when each session family comes from such a global type. Honda, Yoshida and Carbone (2016), Defs. 3.12, 4.1–4.2 and 5.9
The runtime judgement records the types of the process and the queue channels it mentions. Type contexts remember messages already in transit and compose with endpoint types. A process is queue-full when the channels in equal the channels occurring in . A prefix is active when it is outside another prefix and outside either branch of a conditional, after permitted declaration unfolding. A process is well-linked when every reachable process has each active shared-name prefix in a redex. A process is simple when it has a typing derivation whose session environments obey the singleton and emptiness restrictions of Definition 5.25, with no delegation input or output rule. Honda, Yoshida and Carbone (2016), pp. 28–37
The goal is Corollary 5.30. For every simple, well-linked program whose free names have shared sorts, and every reachable process ,
Here is inaction, and includes completed sessions whose empty queues disappear by structural congruence. The milestones are the closed-typing preservation clause of Theorem 5.19(3), the linearity and message agreement clauses of Theorem 5.22, and the immediate-step claim of Proposition 5.29(1). Those are statements of the paper and give separate targets before the progress corollary. Honda, Yoshida and Carbone (2016), pp. 34–37
For the specified class of programs, progress excludes a reachable state that is neither finished nor reducible. It combines static endpoint information with the operational facts about queues and shared-name synchronisation. The communication-safety milestone also states that a value receive is paired with a value message of matching arity, channel reception with a channel vector of matching length, and branching with an offered label. These claims describe behavior of the paper's asynchronous multiparty calculus, rather than a property of a particular implementation. Honda, Yoshida and Carbone (2016), Theorem 5.22 and Corollary 5.30
The paper supplies mathematical proofs, but this mission's statements have no completed machine-checked proofs. Formalizing the result requires a precise account of the calculus, including queue messages, scope, recursive calls, type contexts, projection and the limited form of simplicity. The definitions can support later work on subject reduction and session fidelity in the same model. A contribution may prove any milestone or the goal, or improve the shared definitions while preserving the source's hypotheses and conclusions.
Typing each participant does not immediately give a reduction of their parallel composition. A send can be present while a receive is blocked by an earlier queue message, and a session initiation can be blocked by a shared-name prefix in a different session. Communication safety must relate active prefixes to a unique queue and its actual head message. Progress additionally needs the restrictions on derivations and shared-name links to rule out interference among sessions. The rules for structural congruence and declaration unfolding make the location of a redex depend on more than the outer syntactic constructor. Honda, Yoshida and Carbone (2016), §§5.4–5.5
Lean uses natural numbers for role identifiers, shared names, channels, labels and process variables. Channel indices are one based, following . A global type, value sort and endpoint type are separate syntax classes; finite branch families are lists with nonempty, distinct labels where a well-formed type is required. Recursion is read equi-recursively by an endpoint bisimulation, and global-type linearity is checked on every finite unfolding. Projection returns an optional endpoint type so undefined projections cannot acquire a default value. The session typings are finite maps represented by association lists, with distinct roles and disjoint channel domains. The judgement's subscript lists queue channels, while the domain of lists all sessions under typing.
The formalization uses named process binders and a structural-congruence relation containing alpha conversion. Received-value and call substitution is capture avoiding under explicit freshness conditions. Expression evaluation is fixed to the ordinary Boolean connectives used in the paper's typing rules. Runtime typing includes the queue rules and the partial composition of type contexts. The restricted typing system for simplicity retains runtime queue rules and excludes both delegation directions. The paper prints “[RCV]” in Definition 5.25(2), but its appendix explicitly excludes “[SREC]”; this draft follows the appendix and records that reading in its audit notes. The result quantifies over actual programs and makes simplicity imply typability, so a free, blocked input or an untyped syntax check cannot satisfy the goal. Honda, Yoshida and Carbone (2016), Def. 5.25 and Appendix B.8
Every prefix rule acts on a singleton entry (Notation 4.5); process-variable signatures carry one singleton entry per session vector, as in [VAR]; [SREC] receives the channel names it binds, without substitution (Remark 2.2). Proposition 5.29(1) and Corollary 5.30 are false as printed for open terms: a free name of sort bool used as a conditional guard, or a free process variable, is a stuck simple process. The formal statements therefore add that the free names of the process have shared sorts and, for Proposition 5.29(1), that it has no free process variables (a program has none by definition).
The development needs Mathlib's finite sets, lists and reflexive-transitive closure, plus its own definitions of the process calculus and typing judgements. The Lean declarations in this proposal are draft statements and definitions for review; they are not proofs of the paper's results.
Multiparty communication protocols involve several participants who send messages over shared session channels. An implementation may send a later message before an earlier one has been received, so a written sequence of interactions does not by itself prevent a receiver from taking the wrong message. Honda, Yoshida, and Carbone use global types to specify the whole conversation and a linearity condition to rule out conflicting uses of a channel. Their condition is part of the type system that supports subject reduction and session fidelity in the same paper. Honda, Yoshida, and Carbone, 2016
Global types can contain recursion. Reading their full behaviour as a regular tree may therefore involve infinitely many copies of the same interaction. Proposition 3.13(1) says that checking just one finite unfolding suffices to determine whether every later finite unfolding satisfies the paper's linearity condition. This mission formalizes that proposition and the definitions on which its statement depends. Honda, Yoshida, and Carbone, 2016, §3.5 and Appendix A
A global type describes actions among roles on channels identified by positive indices . Its constructors are a value communication , a labelled branch , parallel composition , recursion , a recursion variable , and termination . The carried value type may contain shared names whose sorts include another global type, or it may be a located end-point type. The formal syntax represents end-point sends, receives, selections, branches, recursion, variables, and termination because shared global types can occur within the sorts carried by those types. Honda, Yoshida, and Carbone, 2016, Figs. 4 and 6
An action node is an occurrence of a communication or branching action in the tree of a finite unfolding. Each node has a sender, receiver, and channel index. The action order holds when one action lies before another in the same continuation or branch, according to Definition 3.7. Actions in different branches or parallel components have no order solely because they appear next to each other in the syntax. Honda, Yoshida, and Carbone, 2016, pp. 15–16
The paper refines that order into three dependency relations. An II step matches receivers; an IO step connects a receiver to a later sender; and an OO step matches both sender and channel. An input dependency is a chain of IO steps ending in II. An output dependency is a nonempty chain of OO or IO steps. A finite type is linear when every ordered pair of actions on the same channel has both dependencies, including the corresponding condition on the global types carried within its values. The last II step matters because a chain ending at an output has not checked the ordering of the final input. Honda, Yoshida, and Carbone, 2016, Defs. 3.11–3.12
Write for the finite result of unfolding every recursion in times and replacing remaining recursion variables by . For a single recursion , the paper gives and . Unfolding does not enter carried types. The one-time unfolding is . Honda, Yoshida, and Carbone, 2016, p. 20 and Notation A.1
The milestone is the direction the paper calls the “if-direction”: for a well-formed global type and a positive unfolding index, linearity at that index implies linearity at the first one.
The mission goal is Proposition 3.13(1), the equivalence between the first unfolding and any positive unfolding.
The lower bound is essential. The paper explicitly begins its Appendix A induction at and gives examples that satisfy linearity at the zeroth unfolding but fail after one unfolding. Proposition 3.13(2), the paper's decidability claim, is outside this mission: formalizing computational decidability would require an effective representation and decision procedure rather than a classical Decidable instance. Honda, Yoshida, and Carbone, 2016, p. 20 and Appendix A
The proposition turns a property stated over arbitrarily deep recursive behaviour into a fixed finite test. It supports the paper's decidability result and supplies the channel-ordering premise used later in coherent global types and runtime typing. Without the stabilization claim, checking a recursive global type by inspecting one finite copy would leave later channel conflicts unresolved. Honda, Yoshida, and Carbone, 2016, Props. 3.13–3.14 and Def. 4.2
The result is already proved in the paper. The formalization work is to give the paper's finite unfolding, action order, dependency chains, and recursive carried-type condition exact Lean meanings, then verify the equivalence against those meanings. The local mission currently contains open theorem statements and compiled definitions; it does not claim a machine-checked proof of Proposition 3.13(1). Those definitions can also be reused when formalizing the paper's coherence and subject-reduction results.
The main obstacle is the interaction between recursion and causality. Unfolding creates further occurrences of actions, while an input dependency requires a chain with a specific final II edge and an output dependency allows only OO or IO edges. The action order also depends on a node's place in a branch, continuation, or parallel component. Merely comparing channel labels across two unfoldings does not establish the required dependencies. The carried-type condition adds another level: unfolding the outer type leaves its carried types intact, but their own linearity must still be checked. Honda, Yoshida, and Carbone, 2016, Defs. 3.7, 3.11–3.12 and Appendix A
Lean represents roles, labels, type variables, and channel indices by natural numbers, with channel indices interpreted as one-based. Branches are lists; WellFormed G records nonempty branches with distinct labels, closed guarded recursion, positive channel indices, and distinct sender and receiver, also checking carried global types. Both theorem statements assume it to make the paper's standing syntax conventions explicit. The sort grammar includes Boolean and natural-number sorts, shared-name sorts, and coded additional base sorts for the paper's ellipsis. The recursion constructor is named mu and the sort type SType because rec and Sort have special meanings in Lean.
Node names are finite child-index paths. Prec is the transitive closure of the five clauses of Definition 3.7. Every II, IO, or OO step includes this order. Input dependency requires at least one step, resolving the printed against the same sentence's mandatory final II step. Carried types are reached through value and end-point type syntax, and nested carriers are included transitively. Linear checks each such carried type at every finite unfolding. The definitions also encode the paper's positive-index and non-reflexive interaction conventions in WellFormed. A linearity predicate that ignores carried types or treats separate parallel components as ordered would change the target theorem. Honda, Yoshida, and Carbone, 2016, pp. 12–13, 16, 19–20
Useful contributions include results about finite unfolding and the action order, preservation of labels at recurring positions, and dependency-chain properties under unfolding. The two folding claims in Appendix A are not listed as milestones here because a faithful folding operation for nested recursion and multiple occurrences has not yet been specified. Their absence is a scope limit on the attack path, not an assumption in the goal.
Scheduling jobs on parallel machines to minimize the total weighted completion time is a basic model of service and computing systems. Two features of practice are hard to combine with performance guarantees: jobs are not known in advance but arrive over time, and their processing times are random, with only their distributions known when they arrive. Machines are moreover often unrelated: a job's processing time distribution depends arbitrarily on the machine, and some jobs cannot run on some machines at all.
Gupta, Moseley, Uetz and Xie (arXiv:1703.01634, Math. Oper. Res. 2020) give the first performance guarantee for this combination: a simple greedy policy whose expected cost is within a factor depending only on the variability of the processing times of the best nonanticipatory policy, which knows all jobs in advance.
Timeline. For deterministic jobs arriving over time, Hall, Schulz, Shmoys and Wein (1997) gave an 8-competitive algorithm on unrelated machines. Megow, Uetz and Vredeveld (2006) introduced the stochastic online model and analysed greedy policies on identical machines with modified release dates. Skutella, Sviridenko and Uetz (2016) gave LP-based approximation algorithms for offline stochastic scheduling on unrelated machines, with guarantees linear in the squared coefficient of variation. The present paper (conference version IPCO 2017) treats the online, stochastic, unrelated case with release dates.
There is a finite set of machines and jobs . Job is released at an integer time , jobs are indexed so that , and job has weight . If job runs on machine its processing time is a random variable with values in ; on forbidden pairs the page writes , and every job has an allowed machine. On allowed pairs and the variance is finite. Different jobs are independent; one job's times on different machines need not be. The squared coefficient of variation is , and bounds it on every allowed pair.
A policy decides, for each job, a machine and a start time; jobs are nonpreemptive and a machine runs one job at a time. It is nonanticipatory if its decisions up to time use only what is known at : the processing time of a job is learned when the job completes. is the least expected cost of a nonanticipatory policy that knows all jobs, release dates and distributions in advance.
The greedy algorithm (§6.1) is first defined for deterministic times . On machine job gets the modified release date . On arrival, job is assigned to a machine minimizing an explicit upper bound on the increase of the objective (Definition 4), and each machine runs WSPT (largest first) among its jobs whose modified release dates have passed. Run on with it yields the nominal schedule . The stochastic greedy policy (§6.3) keeps and the nominal order on each machine, and starts the th job on machine at , never before its nominal start. Its expected cost is , and
The goal is stated against every admissible nonanticipatory policy, for every tie-breaking of the greedy algorithm.
The result. Theorem 4 is the first constant-factor guarantee, for fixed , for stochastic online scheduling on unrelated machines with release dates, and it is achieved by a combinatorial policy that needs no LP solution. For deterministic jobs (, ) it gives a deterministic 7.216-competitive algorithm (Theorem 3), improving the ratio 8 of Hall et al.; for exponential processing times () the factor is . The order matches earlier offline results on unrelated machines and online results on identical machines.
Formalizing it. The result is proved on paper and has no machine-checked proof. A formalization needs nonanticipatory policies with machine choice, a time-indexed LP relaxation with countably many variables and its weak duality, and a dual-fitting argument. It also exposes a gap: the second sentence of Lemma 7, the bound , fails as printed. On one machine with jobs , , the greedy schedule has while . The step counts a job at integer slots, up to one more than . A complete proof of the goal has to close this gap.
Three parts are hard. First, the comparison is with an optimal adaptive policy, so the lower bound has to come from a relaxation that every nonanticipatory policy satisfies in expectation. Writing the time-indexed LP for policies that choose machines at start time, idle deliberately and start at real times, and showing it is a relaxation, requires nonanticipation and job independence to decouple a job's machine from its own processing time. Second, the dual fitting runs through a speed-scaled instance with a non-integer speed , so the dual's integer slots and the schedule's real times do not align; this is where the printed objective bound breaks. Third, the obvious stochastic policy, WSEPT list scheduling without forced idleness, fails: Remark 2 of the paper gives an instance where it has against . The analysis therefore has to work with deliberately delayed starts.
Machines are a Fintype, Nonempty type; jobs are Fin n in release order. Processing times are ℕ-valued measurable functions on a probability space, with finite second moment and mean at least one on eligible pairs, and with jobs independent (iIndepFun over jobs of the machine-indexed vectors). Forbidden pairs are an eligibility relation, never a zero or junk mean. Release dates are natural numbers: the relaxation of §6.2 has integer slots , and (13) is false for a fractional release date. Weights are nonnegative; is any upper bound on the squared coefficients of variation, which is at least as strong as the page's maximum.
is never written as an infimum. The goal and (13) quantify over every admissible policy: a map from realizations to machines and real start times that is feasible (eligible machine, start at or after release, disjoint half-open processing intervals per machine), nonanticipatory, and has integrable completion times. A non-integrable comparator would have Bochner integral and would make the bound trivial or false; the integrability requirement rules this out. The greedy algorithm is a predicate on an outcome (assignment and start times): cost-minimal assignment, no start before the modified release date, no unnecessary idleness, and the WSPT priority. Every tie-breaking is covered, and the goal fixes . The stochastic policy is the recursion itself. LP feasibility includes summability of every series, and LP optima appear only through "for every feasible point there is a feasible point" statements.
A complete development needs: weak duality for / with countably many variables; the identity for the expected occupation variables of a nonanticipatory policy (reusable for any time-indexed stochastic scheduling relaxation); Lemma 10, a self-contained probability inequality; and the dual fitting. Contributions are welcome on each milestone and on a repaired objective bound for Lemma 7.
Sampling from a distribution described relative to a Gaussian reference law is common in Bayesian inverse problems, where an unknown function or initial condition is inferred from noisy observations. Such a distribution is naturally infinite dimensional before it is approximated on a computer. A numerical method must therefore behave reliably as the approximation dimension grows. Hairer, Stuart and Vollmer study this question for Metropolis–Hastings chains and prove that the preconditioned Crank–Nicolson (pCN) chain admits a Wasserstein mixing bound with an iteration count independent of the projection dimension Hairer, Stuart and Vollmer (2014). This mission formalizes their globally Lipschitz case, Theorem 2.12.
The central practical concern is concrete: refining a discretization should improve the target approximation without forcing the number of Markov steps needed for a fixed contraction to grow with the number of coordinates. A bound on each finite dimensional chain separately would not settle that concern, because its constants could deteriorate with dimension. The theorem requires one set of constants for the infinite dimensional chain and every finite dimensional projection.
Let be a separable real Hilbert space. Its Gaussian reference measure has mean zero and a covariance eigenbasis . The subspace is the span of the first eigenvectors, and is the law of the orthogonal projection of a -distributed vector onto . The potential determines the target measures
where and normalize each measure. The paper's finite dimensional chain has state space , rather than the whole space with unused coordinates Hairer, Stuart and Vollmer (2014), (1.1)–(1.2).
At step size , the pCN proposal from is , with drawn from or as appropriate. The move is accepted with probability ; rejection leaves the state at . Write and for these transition kernels Hairer, Stuart and Vollmer (2014), (1.3), (1.5)–(1.6).
The potential is globally Lipschitz, is -integrable, and the acceptance probability has a positive lower bound in specified balls centered at outside a bounded region. These are Assumptions 2.10 and 2.11 Hairer, Stuart and Vollmer (2014), p. 12. The allowed ball radius is either a positive constant or with and .
For , set . Choose the Lyapunov function , where , or, in the growing-radius case, with . The weighted cost is , and is its infimum over couplings.
Theorem 2.12 asserts that and each are the unique invariant probability measures of and . It also asserts that, for every sufficiently small , there is one integer satisfying both bounds for all probability measures on the respective spaces and for every Hairer, Stuart and Vollmer (2014), p. 12:
Here is the same formula restricted to . The milestone list includes the uniform Lyapunov, contraction and smallness claims and the cited weak Harris theorem; the Gaussian projection comparison of Lemma 3.1 is a further stated lemma of the mission. Fernique's Gaussian exponential-moment result is linked to its existing published formalization.
The result bounds the number of pCN iterations needed for a fixed Wasserstein contraction uniformly over the finite dimensional approximations. It also identifies the intended target as the only invariant probability measure, so the contraction describes convergence toward the measure used by the inverse problem. The weighted Wasserstein cost permits this statement on an unbounded Hilbert space, where an ordinary total variation small-set argument would impose a different kind of regularity Hairer, Stuart and Vollmer (2014), §§2.2–2.3.
The paper proved Theorem 2.12 in 2014. The remaining work here is a machine-checked development of the pCN kernels, Gaussian projections, Wasserstein estimates, and weak Harris application. A formalized Fernique theorem already exists in the platform library; the pCN estimates and Theorem 2.12 are open draft statements in this proposal. They will be reusable in the locally Lipschitz pCN regime and in analyses of other Metropolis kernels that satisfy the same abstract contraction conditions.
The pCN proposal contracts the starting points, but the accept–reject step can break that direct coupling: one chain may accept a proposal while the other rejects it. A bound on the proposal distance alone therefore does not imply a bound on the transition laws. The probability of that mismatched decision must be controlled near each pair of starting points, while the acceptance lower bound must remain uniform on the projected spaces. Large starting points also require a Lyapunov estimate to enter the bounded region used by the weak Harris theorem Hairer, Stuart and Vollmer (2014), §§3.1.1–3.1.3.
The Lean development represents as a complete separable real inner product space with Borel measurable structure, as a centered Gaussian probability measure, and the chosen Hilbert basis as diagonalizing its covariance. Second countability is stated explicitly for the measurable pCN construction; for a separable metric space it follows from the standing setting. The projected law is the pushforward by the orthogonal projection onto , a reading of the Karhunen–Loève formula in the paper. A measurable map is essential here: Mathlib's pushforward returns zero for a nonmeasurable map.
The target is Mathlib's normalized tilted measure. The theorem explicitly concludes that both the infinite dimensional and projected targets are probability measures, so the possible junk zero from a nonintegrable tilt cannot satisfy the result. Wasserstein costs and Lyapunov expectations use extended nonnegative integrals. This avoids the junk zero of a nonintegrable Bochner integral and the junk values of a real infimum. Couplings are measures with the prescribed marginals. The acceptance kernel uses the paper's , including the first proposal and its rejection probability.
“Sufficiently small ” means . The iteration count is chosen before and before the input probability measures. Positive radius, positive power exponent and positive exponential coefficient exclude empty acceptance balls and the constant Lyapunov function. The projection is retained as the zero dimensional subspace. Contributions that establish the Gaussian comparison, the three pCN estimates, or the abstract weak Harris statement are within scope.
A local quantum system is built from degrees of freedom placed at sites of a lattice. Its Hamiltonian may contain many terms, each acting on a small group of sites. Even though a term is local, time evolution can spread an observable beyond its original support. A Lieb–Robinson bound limits the size of a commutator between the evolved observable and one supported elsewhere. It gives a quantitative way to say that information propagates with an effective finite velocity. The Appendix C bound of Haah, Hastings, Kothari and Low treats interactions with exponential spatial decay and makes the effect of almost commuting Hamiltonian terms explicit.
The paper studies quantum simulation, where a system's real time evolution is approximated by a circuit. Lemma 12 is an analytic ingredient: it controls how far a local observable can spread during the simulated evolution. The mission targets that lemma and the displayed estimates in its proof, with the constants printed in the pinned arXiv version. The paper proves the results; the remaining task here is to give the stated finite system version machine checked proofs.
Let be a finite set of sites equipped with a metric . Each site has the same local Hilbert space , and the whole system has product basis indexed by configurations . An operator supported on is a matrix of the form : it may change the configuration on , but acts as the identity on every site outside . The matrix norm throughout is the spectral operator norm.
For every , let be a Hermitian operator supported on , and define the time independent Hamiltonian . The sum includes all subsets, including the empty set. Let
For site sets, write when , and when is nonempty. The diameter is for nonempty . The paper imposes two quantitative conditions. First, for some , every pair of terms has a small commutator:
Second, for some , the interactions decay in the weighted sense
Neither condition bounds each by one. This matters because the result is meant to include large but nearly commuting terms. These conventions are from Appendix C.1 of the source.
The goal is Lemma 12. For an operator supported on and an operator supported on a disjoint set , and every real , the proposed formal statement is
The coefficient of in the exponential is proportional to . The goal keeps the paper's explicit factor , its inside the exponential, and the full sum over sites in . The statement is for , as the displayed formula is undefined at ; a family satisfying (14) with also satisfies it for any positive .
The milestones follow the source's numbered displays: the initial estimates for and in (28), their integral inequalities (24) and (27), the linked set series (32), the four estimates of Proposition 13, and the bound on its th line in (37). Here takes a supremum over supported operators of norm at most one, and . The milestone list is a map of the quantities that the proof controls, while the goal itself mentions only the physical operators and the two hypotheses.
The bound shows that a commutator is small when the support of is far from , with a rate determined by the decay parameter and the small commutator parameter . It applies to finite systems of any size with the same constants in (14) and (15). This makes it useful for reasoning about local approximations of time evolution in the quantum simulation setting of the paper. The authors also explain why a velocity proportional to can occur under their hypotheses, so a linear dependence on is not generally available. See the discussion immediately after Lemma 12 in Appendix C.1.
Formalizing the result would supply a reusable finite matrix model of local observables and a checked version of the analytic estimates for near commuting interactions. The source paper provides a proof, but this proposed statement and its milestones currently have no machine checked proof in the mission. The definitions of support, Heisenberg evolution and linked interactions may also be reused in later formalizations of quantum lattice dynamics.
The obvious global norm bound ignores the distance between supports. Merely bounding also loses spatial information and can grow with the whole system. The sharper statement simultaneously tracks where an interaction overlaps the current support and how the small commutator factor enters repeated interactions. A rigorous treatment must control a supremum over local operators, time dependent matrix exponentials, and an infinite series of finite linked set sums without changing any of the paper's constants.
Sites form an arbitrary finite metric space, a disclosed generalization of the lattice setting used for the main algorithm. A common local dimension is used at every site; qubits occur at . Operators are complex matrices on the configuration space , with Mathlib's scoped L2 operator norm. Every term is Hermitian and explicitly supported on its stated set, and is the sum over all subsets. Time is real and is constant in time. The paper mentions a piecewise continuous time dependent extension, which this mission does not state.
The goal explicitly requires . The printed sentence of Lemma 12 omits this, but its derivation on page 24 assumes it; without disjointness the right side is zero at while the left side need not be. The positive condition is likewise explicit. These are the two repairs to the printed lemma, and they are recorded on each relevant item. The milestones (24) and (27) are restricted to , the direction for which the displayed forward integral uses and .
For an empty set, the Lean point to set distance and the local set distance are taken to be zero; a supported operator on the empty set is a scalar, so its commutators vanish. uses a real supremum of a nonempty, bounded set, and (32) states an actual sum with HasSum. The integral milestones involve continuous finite dimensional evolution. The support definition includes nonconstant single site operators, and the case is part of the goal. These choices prevent the result from being obtained through a vacuous support predicate, an entrywise norm, division by zero at , a default value of an unbounded supremum or divergent sum, or omitted disjointness. Contributions that establish the support calculus, matrix evolution estimates, integral inequalities, or linked set bounds are all within scope.
Reservoir computing learns an input/output system from data in two stages. A dynamical system, the reservoir, is driven by the input sequence and its state is recorded; then only a linear readout of that state is trained, by least squares. The echo state network (ESN) is the most widely used reservoir: its state evolves by , with the matrices and the vector drawn at random and never trained. ESNs predict chaotic systems well in practice (Jaeger & Haas, Science 2004), and they are known to be universal: for every fading-memory input/output map some ESN approximates it (Grigoryeva & Ortega, Neural Netw. 2018). Universality does not explain the practice, where the reservoir weights are random and fixed in advance. Gonon, Grigoryeva & Ortega (Ann. Appl. Probab. 2023) prove that an ESN whose weights are drawn from an explicit distribution that does not depend on the target approximates every sufficiently regular target, with an explicit error bound. This mission formalizes that result, Theorem 2, and the chain of results its proof rests on.
Time runs over . Inputs take values in a set with , where is the closed Euclidean ball of radius . The input is a -valued process with law . The target is a functional , the present output as a function of the whole input history. All norms are Euclidean.
Regularity. Fix weights with . is -Lipschitz with constant if . Assumption 1 asks, in addition, for every : with , the truncation has a Fourier representation on , with and .
The random ESN. Fix , , and a bound with almost surely. Draw i.i.d. uniform on and, independently, i.i.d. uniform on . With the block shift on and the embedding of into the first block, and the matrix with rows , put
The ESN is , , with and state space .
For every satisfying Assumption 1 there is a readout , a function of the random weights alone, such that the ESN has the echo state property (a unique state sequence for every input) and
with .
Theorem 2 is the first approximation bound for echo state networks whose recurrent and input weights are sampled from a generic distribution rather than constructed from the target. The bound separates three error sources: a Monte Carlo term decaying like , a truncation term in the sampling radius , and a memory term in the window length . Because the readout can be taken to be the least-squares readout, the bound also controls the trained networks used in practice, and it is the input to the paper's rate and universality corollaries (Corollaries 4 and 5).
Status: the result is proved on paper. No part of it is formalized; the only reservoir-computing material on the platform is the published definition ReservoirESN (the state equation), which this mission reuses. A formal proof would supply the first machine-checked random-feature approximation bound with explicit constants.
The obvious argument fails in two places. First, the classical integral representations of Barron type place the inner weights on unbounded sets, which cannot be sampled uniformly; Proposition 2 needs a change of variables that makes the weight compactly supported while keeping it square integrable, and this costs the factor and the condition (5). Second, a ReLU network is not contractive, so the echo state property of the ESN cannot be taken from the standard contraction criterion; it has to be derived from the block structure of , which makes the difference of the two state halves follow a nilpotent linear recursion.
is EuclideanSpace ℝ (Fin (T+1) × Fin d), block holding ; input sequences are ℕ → EuclideanSpace ℝ (Fin d) with index , and is the published ReservoirESN.IsSolution. Points of are pairs with norm . The uniform laws are Lebesgue measure conditioned on the ball or interval; i.i.d. rows have the product law. The input is independent of the weights (§4.1) and -valued with (§5.1): expectations are iterated lower Lebesgue integrals over and the product law, and probability- statements bound the product measure of the bad set. The scalar output case is used, as in the paper. Assumption 1 is required for every , as printed.
A readout allowed to depend on the input would make every bound trivial; in every statement the readout is a measurable function of the inner weights alone.
Departures from the print, each disclosed in the item: the last term of Proposition 6 is the norm of , which the page prints outside the expectation; the state space of the linear reservoir (52) is a parameter , as in §2.1, and its solution is assumed to be a random process; Proposition 3 omits "" (the explicit value (33) is used); measurability of the Fourier density is stated where the page leaves it implicit.
A complete development needs Fourier integrals on Euclidean spaces, change of variables under linear maps, product measures and Fubini–Tonelli, and an importance-sampling variance bound. The static results (Propositions 2, 3, Corollary 1) are reusable for random-feature models beyond reservoir computing. Proofs of any milestone, and alternative arguments, are welcome.
Bilevel optimization asks for an outer decision while an inner optimization problem responds to that decision. In hyperparameter selection, for example, the outer objective evaluates a model whose parameters are chosen by a training problem. A two-timescale algorithm updates both levels in one stochastic loop, so its outer step uses an inner solution that has not yet settled. The resulting error bound must account for both the outer decision and the inner tracking error. Hong, Wai, Wang and Yang study this setting and give finite-time bounds for their two-timescale stochastic approximation (TTSA) algorithm in the strongly convex outer case Hong et al., arXiv:2007.05170v4, §§1–3.
The paper states its main rates using , with numerical constants omitted. Appendix A gives explicit bounds for the two errors. This mission targets those displayed bounds, retaining their constants and the actual stochastic update. The selected source is the arXiv v4 preprint: page numbers and theorem labels below refer to that version Hong et al., Theorem 1 and App. A.
Let be closed and convex. For an outer point , the inner solution minimizes . The outer objective is , and is an optimal outer point. The inner objective is strongly convex in , which gives a unique inner minimizer. The paper’s derivative and Lipschitz assumptions control how that minimizer and the outer gradient change as and move Hong et al., Assumptions 1–2, pp. 5–6.
The algorithm keeps iterates and . With deterministic step sizes and stochastic estimates , it updates
where is the Euclidean nearest-point projection onto . The inner estimate targets . The outer estimate targets the surrogate gradient
with a bias bounded by . Assumption 3 bounds the conditional variances given the histories and . The surrogate at is the paper’s Hong et al., Algorithm 1, (5)–(7c), p. 6.
The two quantities being bounded are the outer error and inner tracking error . At , the convention is . The constants and are the exact functions of the derivative bounds in (13); is finite by the paper’s standing assumption after (14). The products and are those of (48) Hong et al., pp. 8–9, 20.
The first target is the explicit inner bound (55): for every ,
The goal also includes the explicit outer bound displayed after (59):
These formulas use the paper’s step-size conditions (20a)–(20b), the bias condition , and a positive outer modulus . The milestones are the source’s Lemma 2 (12a), (14), (50), Lemma 10, (55), Lemma 11 and Lemma 4 (29). They supply independently stated targets for the two error quantities and the deterministic product estimates Hong et al., pp. 7–8, 13, 20–22, 34.
The bounds separate the effect of initialization from persistent stochastic error. Each product carries an initial-error term, while the remaining terms show how the current step sizes, variance and bias govern the residual error. This makes the dependencies on , , the strong convexity moduli and the estimator variances explicit, rather than hiding them in rate notation. The paper uses this strongly convex case as one part of its broader complexity analysis Hong et al., §3, Table 1.
The source proves the claimed rates on paper; this local development currently provides compiled Lean statements with open proofs. Completing it would add reusable formal interfaces for conditional stochastic-gradient assumptions, a moving strongly convex minimizer, and weighted products of varying contraction factors. The local mission does not claim a machine-checked proof of Theorem 1 yet.
The outer estimate depends on , while the inner tracking error is measured against the minimizer at the preceding outer iterate. Treating the outer estimate as an ordinary unbiased gradient at loses both the surrogate-gradient discrepancy and the bias. A distance contraction for the inner step alone also does not settle the outer error, because the target moves with . The assumptions must keep the two histories and their conditional estimates distinct Hong et al., (7a)–(7c), (17), App. A.
Lean represents both spaces by EuclideanSpace ℝ (Fin d) with , and Hessian blocks by continuous linear maps with operator norm. The mixed block maps inner directions to outer directions. The inner solution map is required to minimize on every ; the projection is characterized as a nearest-point map on the closed convex set. These clauses prevent an arbitrary solution map or arbitrary outer update from satisfying the theorem. The used in (2) is defined by the displayed surrogate formula (5), so boundary points of have the same meaning as in the source.
The run starts at deterministic and uses measurable estimates with integrable squared norms. Conditional expectations are almost-sure statements relative to the sigma-algebras generated by the iterates, and are Bochner integrals. These regularity assumptions prevent totalized conditional expectation or integral operations from giving spurious zero values. The supremum defining is taken over and has an explicit bounded-above hypothesis; is nonempty because . The goal uses positive, nonincreasing step sizes, in line with the ratio conditions and the auxiliary lemmas. The paper prints in the ratio of (20a), while its application of Lemma 10 with needs ; the stronger ratio is disclosed in the Lean hypotheses. The initial error uses , and real exponents use nonnegative bases.
The definition file and the seven milestone theorems are open for proof contributions. Theorem 1’s two explicit bounds are the mission goal. Lemma 3 (28) is excluded because its printed product uses a factor where (55) uses ; (55) is the selected inner target Hong et al., pp. 13, 21.
A seller who owns several goods and faces buyers with private values must decide how to sell them. The revenue-maximizing mechanism is known in closed form only for one good: for a single buyer it is a posted price, and for several buyers it is Myerson's optimal auction (Myerson 1981). With two or more goods the optimal mechanism may use lotteries, may be impossible to describe compactly, and may behave non-monotonically in the value distribution. This makes simple mechanisms with provable revenue guarantees the practical question: how much of the optimal revenue does a seller lose by selling each good separately with its own optimal one-good mechanism?
Hart and Nisan (arXiv:1204.1846v3) answer this for one buyer and two independent goods (their Theorem A): selling separately earns at least half of the optimal revenue. Their Theorem 18 (p. 29), proved in Appendix A.7 as Theorems 33 and 34, extends the factor to any number of buyers. This mission formalizes the dominant-strategy half, Theorem 33, in which the buyers may be arbitrarily correlated with one another, as long as the two goods are independent.
One seller sells goods to buyers. Buyer 's value for good is a number ; a valuation profile is , and is buyer 's valuation vector. The profile is random, , with a commonly known joint law.
A mechanism gives each buyer an allocation (the probability that receives each good) and a payment , as functions of the reported profile, subject to feasibility: for every good . Buyer 's payoff is , and the seller's revenue is .
The expected revenue is , and
For two goods write and for the vectors of the buyers' values for good 1 and good 2, so . is the optimal dominant-strategy revenue from good 1 alone, sold to the same buyers. Finally .
If and are independent, then
No independence among buyers is assumed: the values for the same good may have any joint law.
With independent buyers and two independent goods, so that all values are independent (footnote 27), the same inequality holds for Bayesian Nash implementation: .
The result. Theorem 33 shows that the factor- guarantee of separate selling does not depend on there being a single buyer, nor on the buyers being independent, provided incentive compatibility is required in dominant strategies. It reduces a two-good, -buyer design problem, whose optimum is not characterized, to two one-good problems, each of which can be handled by known single-good auction theory. Remark (a) on p. 29 records that the dominant-strategy statement holds for correlated buyers, while Remark (b) there explains, via Crémer and McLean (1988), why the Bayesian Nash analogue cannot be extended to correlated buyers.
Formalizing it. The result is proved in the paper; to our knowledge no machine-checked version exists. A formal proof requires multi-agent mechanisms on , the Lebesgue integral of a possibly non-integrable revenue, conditioning on an independent coordinate of a product law, and the subdomain property of Remark (b). The definitions here (feasible multi-buyer mechanisms, IC-DS, IR-DS, , and the Bayesian Nash counterparts) are reusable for any multi-buyer revenue-maximization result.
The obvious first idea is to apply the one-buyer Theorem A buyer by buyer. It fails: the feasibility constraint couples the buyers, so a multi-buyer mechanism does not decompose into single-buyer mechanisms, and the revenue extracted from one buyer depends on the reports of all the others. Any reduction to one-good problems must produce, from a two-good mechanism, one-good mechanisms that remain feasible and dominant-strategy incentive compatible for every buyer at once. On the measure-theoretic side, payments of an incentive compatible mechanism may be negative and non-integrable, so expectations must be handled in the extended reals, and the passage from bounds that hold for each fixed value of one good to a bound in expectation needs the product structure of the law of .
x : Fin n → ι → ℝ≥0 (x j i ); a random profile is given by its law, a probability measure on that space. One good is ι = Unit, two goods are ι = Fin 2 (good 1 is index 0). The law of two independent goods is twoGoodsN μY μZ, the image of the product law ; μY and μZ are arbitrary probability laws on , so correlation among buyers is allowed.Function.update x j x'. Feasibility is part of admissibility; without it a mechanism could sell each good to every buyer.EReal difference of the integrals of and , never a Bochner integral, which would vanish on non-integrable revenues. takes values in .Contributions of every kind are welcome: proofs of the milestones, of Theorem 34, and general lemmas on multi-buyer mechanisms.
In a welfare sharing game, several players choose resources and receive shares of each resource's welfare. A rule for splitting welfare is useful only if the resulting players' incentives admit stable choices. The paper by Gopalakrishnan, Marden, and Wierman characterizes the distribution rules that guarantee a pure Nash equilibrium for every game formed from a specified class of local welfare functions. Its Appendix C supplies a complementary structural result: generalized weighted Shapley rules give the game a vector-valued potential. That structure provides a way to analyze equilibrium existence and dynamics without enumerating all possible unilateral deviations individually.
The scalar weighted-potential case was known for weighted Shapley values in the work of Hart and Mas-Colell, as Appendix C recounts. The 2014 paper extends the setting to an ordered system of priority blocks. A single scalar component cannot generally express the priority structure, so Appendix C uses a finite vector whose components are compared in order. This mission isolates that explicit potential theorem from the paper's separate characterization theorem.
Let be the players and the resources, with . Player chooses an action , possibly containing several resources. For a profile , let be the users of resource . Each resource has a local welfare function and a distribution rule , giving player 's share when the resource is used by coalition . The game's utilities are separable:
A weight system specifies positive weights and an ordered partition of the players. For a nonempty coalition , let be its members in the earliest block meeting . The Möbius coefficient of a welfare function is
The generalized weighted Shapley value distributes the contribution of among players in in proportion to their weights. The generalized weighted marginal contribution rule instead evaluates the difference in a welfare function when a player is removed from the part of a coalition in that player's block and later blocks. These are the two formulas in Tables 1–2 of the source paper. The ground welfare functions used by the two rules, and , may differ. Their coefficients are related by (12): for every nonempty .
A generalized weighted potential is a vector with a fixed component assigned to each player. For any unilateral change by that player, all earlier components stay equal, and the player's utility change equals a positive multiple of the change in the assigned component. This is the precise potential identity used in this mission.
The local target is equation (83): local resource potentials whose changes agree with each player's utility share combine into a game-level potential. The coefficient target is the equality between the Table 1 marginal-contribution rule and its Table 2 Möbius-basis expansion. The closed-form target identifies exactly which vector component each player can change.
The goal is Theorem 3, using its closed form (85). Write . If each is simultaneously the generalized weighted Shapley rule for and the generalized weighted marginal contribution rule for , with their coefficients related by (12), then
is a generalized weighted potential with player weights . The goal specifies this potential itself, rather than merely asserting that some potential exists.
The theorem gives an explicit structural certificate for all games built from these sharing rules. A maximum of a vector potential in lexicographic order is stable against improving deviations, so the identity supports the equilibrium guarantee in the main characterization result. Its formula also gives a concrete object for studying changes in allocations or comparing priority systems; these are uses of the result, not additional claims of this mission. The closed form is particularly useful because each component is an evaluation of a ground welfare function on a specified suffix of the priority partition, as the paper explains on p. 11.
The mathematical result was proved in 2014. The remaining formalization work is to construct a machine-checked proof of the exact vector identity, including the coalition basis calculation and the passage from local resource changes to whole-game utility changes. The local platform index contains related scalar and ordinal potential theorems, but no declaration with this paper's priority-block model and closed-form vector potential.
The obvious scalar-potential analogy does not by itself track ordered priority classes. Adding a player in one class can leave some vector components unchanged while affecting a later component. The proof obligation therefore includes the exact component order and a player-specific change identity, uniformly over coalitions and actions. A second difficulty is reconciling two descriptions of the same distribution rule: Table 1 uses a welfare difference, while Table 2 expands welfare in Möbius coefficients over coalitions. The equality must hold even when the welfare at the empty coalition is arbitrary.
There is also a printed inconsistency. Definition 1 and (83) call the assigned component the “first nonzero” component, but the proof only establishes that earlier components are unchanged. The assigned component can also be unchanged on a particular deviation, while a later one changes. Formula (84) disagrees with the closed form (85) in a two-block example. The mission follows the fixed per-player component supported by the proof and states (85); the precise counterexample is in the moderation notes.
Players and resources are represented by Fin n and Fin m, coalitions and actions by Finset, and real-valued welfare and utility functions by functions into . The standing model has and strictly positive player weights. The potential predicate requires , matching Definition 1's positive vector dimension. The ordered partition is a map from players into blocks; empty blocks are allowed, and Fin K provides zero-based indices. A vector component is indexed in reverse block order, so component 1 sees only the final block and component sees the whole coalition. For a nonempty , is its earliest occupied block; its empty-case value is empty and is never used in (12).
Rules are compared only for players belonging to the coalition in which they are evaluated. The named Shapley and marginal rules return zero off that coalition; arbitrary input rules may have other unused values there. No budget-balance or hypothesis is added; the empty-coalition value cancels in marginal differences. Action sets may be empty because this mission proves a potential identity for feasible deviations, without asserting that a feasible profile or equilibrium exists. The formalization does not replace the goal by a vacuous existence claim: it fixes the potential to the explicit closed form (85) and requires the full change identity at every feasible unilateral deviation.
The development needs finite-set sums, powersets, ordered finite indices, real arithmetic, and the paper-specific welfare rules. The local-to-global separability statement and finite coalition-basis calculation can be reused in related sharing games. Contributions proving the stated milestones, or strengthening the result under correctly stated extra assumptions, are in scope.
An extremal graph problem asks how many copies of a chosen small graph can occur when a different graph is forbidden. The usual Turán problem counts edges; counting paths or cycles gives a more detailed view of the structure that can survive a forbidden subgraph. Gerbner, Győri, Methuku and Vizer study these generalized Turán numbers for paths and cycles in their paper on even-cycle problems. Their Theorem 23 asks for the leading number of paths when a specified odd cycle is absent. The answer has the same leading term as a balanced complete bipartite graph, despite the fact that excluding one odd cycle is weaker than requiring a graph to be bipartite. Gerbner et al., Theorem 23
The spectral theorem cited by the authors gives a useful threshold for this setting. For a graph with no cycle of length , it bounds the adjacency spectral radius once the vertex count exceeds . This threshold is explicit and stays visible in the finite-size milestone. Gerbner et al., Theorem 32, citing Nikiforov (2008).
A simple graph has finitely many vertices and no loops or parallel edges. For , is the cycle on vertices, and is the path on vertices. Thus has edges, following the paper's convention. A copy of in is a subgraph of isomorphic to ; copies are unlabelled, so reversing a path does not create a second copy. Write for their number. Gerbner et al., pp. 2–3
For a set of lengths, a graph is -free if it has no subgraph isomorphic to for any . The mission mainly uses : exactly one odd cycle length is forbidden, while shorter and longer cycles may still occur. The generalized Turán number is the maximum
The adjacency matrix records whether each pair of vertices is adjacent. Because the graph is undirected, this is a real symmetric matrix. Its spectral radius is the largest absolute value of an eigenvalue of . The graph is the complete bipartite graph with parts of sizes and ; the balanced choice uses . Gerbner et al., §§7.1–7.2
For each fixed and , as ,
The equality gives both sides of the asymptotic estimate. The term may depend on the fixed parameters and tends to zero as the number of vertices grows. Gerbner et al., Theorem 23, p. 8
The milestone list records the balanced complete bipartite lower bound, the comparison between paths and walks in equation (7), a spectral bound on the walk sum, Nikiforov's stated spectral estimate, and the resulting finite-size upper bound. In particular, the last two targets retain the paper's constants:
The milestone statements identify which assertions concern every graph and which require the forbidden-cycle condition. Gerbner et al., pp. 30, 32
For fixed and ,
and Remark 3 records the inequality for every graph , which links this count to Theorem 23. Gerbner et al., Theorem 24, p. 11; Remark 3, p. 32
Theorem 23 fixes the leading coefficient for the maximum path count for every fixed path length and forbidden odd-cycle length in its range. A balanced complete bipartite graph reaches that coefficient asymptotically, so the result identifies an extremal construction at first order. The lower-bound milestone formalizes this construction with balanced parts, including the one-vertex rounding needed when is odd. The matrix and spectral milestones can also be reused when counting walks or paths under different graph restrictions. Gerbner et al., §7.2
The paper proves these results on paper. In this mission, the definitions and theorem statements are checked by Lean, while proofs of the draft theorems remain to be supplied. A completed development would make the path-count theorem and its stated spectral dependency machine checked in the pinned Mathlib environment. It would also expose where a general graph identity suffices and where the odd-cycle prohibition matters.
Counting paths directly is difficult because the available information about a graph with one forbidden odd-cycle length does not control each vertex degree tightly enough to determine a sharp path count. Counting walks is easier algebraically, but walks may revisit vertices, so their number is generally larger than the number of paths. A graph-wide spectral bound is needed to control the walk total sharply, and the cited Nikiforov estimate has to be carried with its forbidden-cycle hypothesis and vertex threshold. A generic bound based only on the maximum degree would not yield the coefficient in Theorem 23. Gerbner et al., §§7.1–7.2
Graphs on vertices are represented as SimpleGraph (Fin n). Mathlib's cycleGraph a and pathGraph l represent and the path on vertices, and copyCount counts unlabelled subgraph copies. The finite set of real adjacency eigenvalues defines through a maximum of absolute values. On an empty vertex type this value is zero. The extremal number is a natural-number supremum over feasible graphs; for the odd-cycle family the feasible set is nonempty and finite, so this supremum is attained.
The goal has and , exactly as Theorem 23 states. The lower-bound item chooses parts of sizes and . Equation (7) requires : for the claimed factor of two is false. The finite spectral and path bounds require . These conditions are explicit in the Lean statements. Natural subtraction appears only in expressions whose hypotheses make the intended quantity meaningful, including ; the bipartite part size is computed with natural division. The asymptotic statements use real sequences tending to zero and eventual comparisons or equality.
The result must include the lower bound as well as the upper bound. It uses unlabelled path copies, an attained extremal maximum, and a forbidden family consisting of the specified odd cycle. An upper bound alone, labelled copies, or a supremum over an empty class would change the theorem. The needed infrastructure consists of graph-copy counts, adjacency-matrix walk counts, finite-dimensional spectral facts, and the cited odd-cycle spectral theorem. The page states Theorem 24 "for any "; the Lean statement and Remark 3 require and , the only values for which and are cycles. Contributions proving the milestones or developing reusable interfaces for those objects are within scope.
A suffix tree of a text answers pattern-matching and string-analysis queries (longest repeats, maximal repeats, matching statistics) in time close to optimal, but it occupies machine words. For highly repetitive collections, such as many genomes of one species or the versions of a document, this is far more than the information the text contains. A standard measure of that information is , the number of runs (maximal blocks of one repeated symbol) of the Burrows–Wheeler transform of . On repetitive collections is orders of magnitude smaller than , and indexes using words are of direct practical interest in bioinformatics and in versioned document stores.
Gagie, Navarro and Prezza (arXiv:1809.02792v2, 2019) build a compressed suffix tree in words (their Theorem 9, p. 28). A compressed suffix tree in the style of Abeliuk, Cánovas and Navarro (Algorithms 2013) needs the longest common prefix array in compressed form, and stores it differentially, as . The paper's route to compressing is one exact combinatorial fact: has a bidirectional macro scheme of size at most (p. 28). A cited conversion of macro schemes into run-length grammars (Lemma 18, from Gagie, Navarro and Prezza, LATIN 2018) then gives the grammar. This mission formalizes that combinatorial fact and the lemmas it rests on.
A text , , is a string over the alphabet whose last symbol T[n]=\=1T[i..]T[i]T[i+1]\cdots T[n]SA[1..n][1..n]$ listing the starting positions of the suffixes in increasing lexicographic order.
The Burrows–Wheeler transform is if and if : the symbol preceding the -th smallest suffix, read cyclically. The LF mapping is
where counts the symbols of smaller than and counts the occurrences of in . A position starts a run if or ; is the number of run starts, written .
Let be the length of the longest common prefix of two strings. Then
The differential suffix array is , .
A bidirectional macro scheme (BMS) of size on a sequence of any symbol type (Definition 6, p. 28, after Storer and Szymanski) is a partition into consecutive blocks, each either an explicit symbol (a block of length 1) or a pointer to another occurrence of the same content. The source map sends a position at offset inside a pointer block to . The scheme is correct if, from every position , some iterate , , is an explicit symbol.
This is the sentence following Lemma 16 on p. 28, proved by Lemma 17. It fixes no constant beyond the paper's own count, and it is the exact input Lemma 18 needs.
The result. The bound ties the compressibility of the array, a structure of size that does not obviously inherit the repetitiveness of the BWT, to the number of BWT runs. Through Lemma 18 it yields a run-length grammar of size for (Lemma 19, p. 29), and the paper's compressed suffix tree supports its navigation primitives on that grammar. The same pattern, runs of the BWT inducing copies in a differential array, drives the paper's -word access to and (§5), of which Lemma 12 is the first step.
Formalizing it. The result is proved in the paper; to our knowledge none of it, nor the basic theory of suffix arrays and the Burrows–Wheeler transform, has a machine-checked proof on this platform. The mission produces a self-contained Lean development of the BWT and LF mapping from their counting definitions, of the and arrays, and of macro schemes with their correctness condition. The single-cycle property of and the identity are folklore results that underlie every FM-index; they are formalized here from the counting formula, not assumed.
The obvious proof of the goal counts blocks: at most explicit symbols and at most regions. The counting is easy; the content lies in the two properties the count presupposes. First, the copies must be correct: a whole region must coincide with the stretch starting at , which needs to map a run onto consecutive positions and differences to be preserved, and it needs three consecutive equal BWT symbols, not two, because involves the suffixes in cells , and . Second, the scheme must be correct as a whole: following pointers must never cycle. A scheme in which two regions point at each other satisfies every local condition and still fails. Ruling this out requires the global fact that is one cycle through all of , which in turn rests on the lexicographic order of suffixes and the uniqueness of the terminator \$$. Connecting the counting definition of LFSA[LF(p)]=SA[p]-1$ is itself a nontrivial argument about ranks of symbols among sorted suffixes.
Positions are 1-based natural numbers, as in the paper. The text and the suffix array are functions read only on , symbols are natural numbers, and \=1[1..n]BWTLFT[0]T[n]LCP\operatorname{lcp}DLCPDSAij\ne i[1..n]fp_i+k\le np_0=-2p_1=1LFLFSA[LF(p)]=SA[p]-1SA[p]>1SA[p]=1$ it holds only cyclically.
The paper's space and time claims (Theorem 9, Lemma 19) and the cited grammar conversion (Lemma 18) are out of scope; the goal is their explicit combinatorial content.
Every sequence has a macro scheme of size (all symbols explicit), and a set of pointers that only point at each other satisfies every local condition, so a formalization that bounds the size of an arbitrary partition, or that drops the condition that every chain of copies reaches an explicit symbol, would be empty or false; both are excluded by the definition used. , and are not defined through the properties the milestones assert.
Contributions welcome: proofs of the milestones, and reusable lemmas about the LF mapping and lexicographic order of suffixes, which the paper's other missions (locating with sampled phrases, counting distinct substrings) also use.
A text index answers questions about occurrences of a pattern without scanning the whole text. One reason to compress such an index is that many stored texts are repetitive: multiple versions of a document or genome often share long passages. The Burrows–Wheeler transform (BWT) rearranges a text's symbols in a way that groups related contexts. A small number of equal-symbol runs in the BWT is therefore a useful measure of repetition. Gagie, Navarro, and Prezza use the number of runs to state space bounds for text searching and suffix-tree operations in Fully-Functional Suffix Trees and Optimal Text Searching in BWT-runs Bounded Space.
This mission isolates one exact counting result underneath those data-structure bounds. A length- substring is called an -mer. The number of different -mers measures how many local patterns the text contains; repeated occurrences of the same string count once. Lemma 9 of the 2019 preprint bounds this number directly in terms of BWT runs. The result makes a relation between two notions of text repetition precise: clustering in the BWT and diversity of fixed-length substrings.
Let be a text over the ordered alphabet . Its final symbol is a unique terminator \=1i\in[1..n]T[i..n]iSA[1..n][1..n]SA[p]p$th suffix. This is the setup of §2 of the source preprint, pp. 7–9.
The BWT symbol at position is the character just before the suffix at . When that suffix is the whole text and has no preceding character, its predecessor is read cyclically as T[n]=\$$. The BWT partitions into maximal runs of equal symbols; rT[i..j]$ is primary when its interval contains a sampled text position, as in Definition 5, p. 16.
For , let be the set of length- strings occurring in :
The braces matter: two windows with identical contents give one element. The final allowed window includes the terminator. The text is not padded in this definition.
Lemma 8, p. 17 states that every nonempty substring of has an occurrence with the same contents that is primary. With denoting sampled text positions, the assertion is
The mission's milestones also capture the suffix-array interval of a pattern, the sampled occurrence of each individual character, and the bound stated in the proof of Lemma 9. These give precise intermediate claims in the paper's route to the count.
The main goal is Lemma 9, p. 17:
Here is calculated from the BWT of the text's suffix array. Both inequalities on are part of the source statement. The bound concerns distinct strings of a fixed length, not the number of substring windows.
The theorem gives an explicit upper bound on the number of different length- strings that can appear when the BWT has few runs. In §4.2 the authors use it to bound the text area holding all distinct length- substrings; that area supports the alphabet-mapping component of their compressed index. This exact combinatorial assertion remains meaningful independently of a machine model or a choice of data structure. Its role in the broader construction is described around Lemmas 8 and 9, pp. 16–17.
The result is proved in the paper. The work here is to give its objects and claims machine-checkable statements and then close their proofs in Lean. The mission has not already supplied a machine-checked proof of these claims. A completed development would also provide reusable definitions of suffix arrays, BWT run boundaries, and finite sets of distinct substrings for later formalizations of compressed text indexes.
The count is immediate only after every substring can be represented by an occurrence containing a sampled position. A direct count of all starting positions cannot yield the claimed bound: may be large even when is small. The difficult step is therefore the primary-occurrence claim of Lemma 8. Its statement has to preserve both parts of “occurrence”: the replacement interval must have the same length and symbols, and it must stay inside the text. The suffix-array range used there depends on lexicographic order, while sampled positions are defined through changes between adjacent BWT symbols. Connecting those two views of the text is the central obstacle.
The Lean representation uses for symbols and 1-based positions. The functions and are read only on . An IsText hypothesis enforces , membership in , and the unique final terminator \=1SA[1..n]nTSAn$. Runs are counted by their starting cells; samples are the corresponding text positions from both ends of every run. The model follows the first sentence of Definition 1, including the last character of the final run. The source's following explanatory clause omits that endpoint.
The set of -mers is a finite set of lists formed from every valid window. It is not restricted to primary windows, which would make the goal a different and easier statement. A primary substring carries valid endpoints and a sampled position inside them. The formal statements do not assume that the desired primary occurrence exists; that is precisely the content of Lemma 8. The paper's space and time results are outside this mission: the goal is their explicit substring-counting content.
A complete proof needs elementary facts about list prefixes and lexicographic order, finite interval images, the BWT's run partition, and cardinalities of substring windows near samples. The definitions and interval lemmas can be reused by other missions on suffix arrays and compressed strings. Contributions proving any of the listed milestones or strengthening the surrounding reusable string infrastructure are within scope.
Which cycle lengths a graph must contain is a classical question of extremal graph theory. A graph on vertices is pancyclic if it has cycles of every length from to ; Bondy's meta-conjecture (Bondy 1971) and a long line of results ask which density or expansion conditions force pancyclicity or, more modestly, force the set of cycle lengths to contain a long interval. For sparse graphs, expansion is the natural hypothesis: random graphs and explicit expanders are sparse, yet very well connected.
Friedman and Krivelevich, Cycle lengths in expanding graphs (arXiv:1912.11011v2; Combinatorica 41, 2021), study two expansion conditions. For the usual vertex expanders they show that cycle lengths are numerous and well spread, but they also note that an expander need not contain any interval of cycle lengths of non-trivial length. Section 4 of the paper therefore introduces a different, two-set expansion condition, the β-graph, and shows that it does force a complete interval of cycle lengths of length linear in . This mission formalizes that result, Theorem 3.
Timeline.
All graphs are finite and simple. For a graph and a vertex set , the external neighborhood of is
Let have vertices and let . is a β-graph if every two disjoint vertex sets with are joined by an edge. For , the complete graph is a β-graph for every ; when , only the complete graph is. No graph on zero vertices is a β-graph.
The set of cycle lengths of is . A cycle of length has distinct vertices.
The proof works with the tree : two complete -ary trees of depth (every internal vertex has children, every leaf is at distance from the root) whose roots are joined by a path of length . A graph contains a copy of a tree if there is an injective map from the vertices of to those of sending edges to edges.
Logarithms are to base .
For every there exist positive constants and such that every β-graph on vertices satisfies
The goal fixes the shape of the bound, not its constants: the proof's choice is , and is a multiple of . As the interval widens towards . The upper end is tight up to the constant: the disjoint union of with isolated vertices is a β-graph.
In the order of the proof (pp. 15–18):
The result. Theorem 3 proves the conjecture of Hefetz, Krivelevich and Szabó in a stronger form: β may be any constant below instead of tending to zero with , and the lower end is of optimal order. Since spectral expanders satisfy the β-graph condition (by the expander mixing lemma an -graph with is a β-graph), the theorem gives long intervals of cycle lengths in pseudo-random graphs. The method, embedding two large trees joined by a path and closing the cycle across their leaf sets, is a template for producing cycles of prescribed length in expanding graphs.
Formalizing it. The result is proved on paper. As far as the platform's records show, none of it is formalized: Mathlib has trees, walks, cycles and graph copies, but no tree-embedding theorem for expanders and no result on cycle lengths of this kind. The main piece of new infrastructure is Haxell's theorem (milestone 3), which the paper cites without proof. Its proof (in Haxell's paper and in Balogh–Csaba–Pei–Samotij) is a few pages of inductive embedding with a Hall-type invariant. A formal proof of Theorem 4.1 would be reusable for any embedding argument for bounded-degree trees, for example in Ramsey and size-Ramsey problems for trees and paths. The printed proof also has a rounding gap (below), so the formal proof will have to settle a slightly different argument from the printed one.
The β-graph condition only speaks about pairs of large sets, while cycles are built edge by edge, so short and long cycles both need a mechanism. The obvious approach, finding a long path and then shortcutting it, does not control which lengths occur. The proof instead needs a robust embedding theorem for trees with about leaves inside a subgraph with good expansion of small sets, and that is Theorem 4.1, a deep result.
A second difficulty is quantitative. In the printed verification of claims (1) and (2) on p. 17, a complete -ary tree of depth is counted as having about vertices, as if exactly. In fact can be almost , and for claim (2) the honest count only covers rather than . For the gap is larger. Theorem 3 is unaffected, because its constants are only and pruning the trees to leaves repairs the count. But a solver following the printed proof will need to repair that step. The two claims are therefore not posed as milestones.
Graphs on vertices are SimpleGraph (Fin n). Vertex sets are Set with Set.ncard, and every inequality involving β, a logarithm or is stated in ℝ after casting. Logarithms are Real.logb 2. Cycles are Mathlib's Walk.IsCycle, so every cycle length is at least . "Contains a copy" is SimpleGraph.IsContained (injective and edge-preserving, not induced). The subgraph of Lemma 4.1 is the induced subgraph on a set , with . The tree is defined on words of length at most over (two tagged copies) plus path vertices.
Conventions of the goal:
Infrastructure needed: Haxell's theorem (reusable well beyond this mission), counting leaves and vertices of complete -ary trees, and turning an embedded plus one edge into a Walk.IsCycle. Contributions to any milestone are welcome, in particular a proof of Theorem 4.1 and a repaired version of claims (1) and (2) with pruned trees.
In a structured bandit problem a learner repeatedly chooses a decision from a set and observes a noisy reward whose mean is an unknown function from a known class . Classical analyses of such problems measure the complexity of by the eluder dimension (Russo and Van Roy, 2013; 2014) or the star number, and prove regret bounds for posterior sampling (Thompson sampling) or optimistic algorithms in terms of these quantities.
Foster, Kakade, Qian and Rakhlin (2021) introduced the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the minimax regret of interactive decision making. Section 6.2 of that paper connects the DEC to the older parameters: it shows that the square-loss DEC is bounded by the disagreement coefficient of the class, a quantity introduced in Foster, Rakhlin, Simchi-Levi and Xu (2020) and itself bounded by the star number and the eluder dimension. The bound is certified by posterior sampling, so it also explains why posterior sampling works for these classes.
Let be a set of decisions. A model assigns to each decision a reward distribution; here a model enters only through its mean-reward function and an optimal decision . The class collects the mean-reward functions of a model class . A reference model , not necessarily in , has mean reward .
A prior is a finitely supported distribution over . The posterior sampling strategy plays , the law of when .
The prior-dependent square-loss DEC (display (70) of the paper) is
the best trade-off between regret and squared estimation error that a decision distribution can achieve against a model drawn from the prior.
For a class of functions and a distribution on , the disagreement coefficient (Definition 6.3) is
where is drawn independently of . It measures how much mass puts on decisions where some function of the class is large although it is small in . The shifted class consists of the differences , .
For every , posterior sampling certifies
In the formal statement, the objective of (70) evaluated at is bounded by for every and every upper bound of the disagreement coefficients of the shifted classes.
Theorem 6.2 bounds the DEC of any structured bandit class by its disagreement coefficient. With the bounds of the disagreement coefficient by the star number and the eluder dimension (Lemma 6.1 of the paper, from Foster et al. 2020) and the minimax theorem, it yields Theorem 6.1, which recovers the regret bound of Russo and Van Roy for posterior sampling as a special case, and gives a bound in terms of the star number. The decoupling lemma (Lemma E.2) is a general tool: it controls a coupled quantity by a decoupled second moment, and applies wherever an algorithm's decision and the function evaluated there are drawn from the same distribution.
The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the disagreement coefficient and of the decoupling lemma, on which formal versions of eluder-dimension and star-number bounds can build.
The obvious argument fails at the decoupling step. The quantity evaluates each function at its own decision, while the estimation error controls only , with independent indices. For a finite set of decisions, Cauchy–Schwarz bridges the two at the price of a factor ; for an infinite decision space this gives nothing. The disagreement coefficient replaces the cardinality, but it controls disagreement only at one pair of scales at a time (the size of and the norm of ), while the coupled quantity involves all scales at once; obtaining only a loss from this is the technical core of Lemma E.2.
The goal is not trivialized by a junk value: the disagreement coefficient is a genuine supremum under the stated hypotheses (a sorry-free check accompanies the definitions), rules out negative logarithms, the class is the whole class rather than the prior's support, and the reference model is not assumed to lie in the class.
Contributions welcome: proofs of the milestones in attack order; a general layer-cake lemma for finite sums; a formal disagreement coefficient bound by the star number or the eluder dimension (Lemma 6.1), which would lead to Theorem 6.1.
Interactive decision making covers bandits, contextual bandits and reinforcement learning: a learner repeatedly chooses a decision, observes a reward and an observation drawn from an unknown model, and tries to accumulate nearly as much reward as the best decision for that model. Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) introduced the Decision-Estimation Coefficient (DEC), a single quantity that gives lower bounds on the regret of every algorithm and, through the Estimation-to-Decisions (E2D) meta-algorithm, matching upper bounds. This mission formalizes the upper-bound side in its strongest form: E2D run with Hellinger confidence sets (Option II of Algorithm 1) has regret controlled by the localized DEC, the same quantity that appears in the paper's lower bounds (Theorems 3.1 and 3.2).
The basic E2D guarantee (33) in terms of the global DEC is already posed on Prove2Me as an open goal (FoundationsRL.GeneralDM.e2d_general_regret_bound_v2, the restatement in Foster and Rakhlin's lecture notes, arXiv:2312.16730, Proposition 26). It is not posed again here.
A decision space is a finite set. An outcome consists of a reward and an observation and ranges over a finite set , and is its reward. A model assigns to every decision a probability distribution on . Its mean reward is , and is a decision maximizing . The learner knows a model class that contains the true model . At round it plays a distribution on , and its regret is
Write for the squared Hellinger distance. For a reference model and the DEC is
The localized class keeps only the models whose optimal value exceeds that of by at most .
E2D with Option II receives at each round an estimate from an online estimation oracle. It keeps the confidence set of models whose accumulated Hellinger error against past estimates, , is at most . It plays a minimizer of the DEC problem over at . Assumption D.1 asks that, with probability , the oracle's Hellinger error on the rounds where is at most a known bound . It also asks that .
With , rewards in and , with probability at least ,
The bound is the paper's most general upper bound. Together with the lower bounds of §3, it shows that the localized DEC characterizes the regret of interactive decision making up to the estimation term. With an aggregating estimator satisfying (App. A.3), it recovers the finite-class guarantee of Theorem 3.3. The companions extend E2D to general divergences, randomized estimators and adversarially chosen contexts. That last setting contains SquareCB for contextual bandits.
All results of this mission are proved in the paper. None was machine-checked before. Formalizing them produces a checked reduction from decision making to estimation for finite decision and outcome spaces, stated against the published DEC and localized-class definitions, so that later bounds on the DEC of specific classes (bandits, tabular RL) can be combined with it.
The non-localized bound follows from the per-round step (138) by summation. The localized bound does not: the per-round DEC is taken over the confidence set , and replacing it by a localized class requires that every model surviving in have optimal value close to that of the current estimate . The confidence set constrains Hellinger errors against past estimates, not optimal values, and the estimate itself is in general not a member of the class. Bridging these is the content of Lemma D.2 and the containment. The first round is a boundary case: there the confidence set is the whole class, so the containment holds only if the radius is at least the full range of the rewards.
Fintype), a finite outcome set , and models m : S → Y → ℝ with every m π a probability vector. Expectations are finite sums. Contexts in Theorem 8.1 range over an arbitrary type.decGf, and dec for the supremum over ) and the localized class are the published FoundationsRL.GeneralDM definitions, referenced and not redefined.IsOptionIIRun (lines 7 and 8 and ). "With probability at least " becomes the hypothesis EventD1, the event of Assumption D.1. Line 8's arg min is relaxed to "certifies the minimax value from above", as Remark 4.1 permits. Rounds are 0-based, and is evaluated at the paper's index.IsOptionIIRun. The open bound (33) is not restated.decGf in the class are reusable beyond this mission.Retailers observe demand signals (point-of-sale data, local forecasts) that their suppliers do not. Whether a retailer should pass such a signal upstream is a central question of the supply chain information-sharing literature. In a single chain, sharing helps the manufacturer plan, but the retailer may lose from it. Competition between chains adds a second effect: sharing in one chain changes how the rival chain responds to its own signal.
Ha, Tian and Tong (MSOM 2017) study this question when the manufacturer's planning decision is production cost reduction: a manufacturer that knows more about demand can invest in lowering its unit cost more efficiently. They find that the equilibrium of the information-sharing game between two competing chains depends on a single efficiency parameter in a three-regime pattern. This mission formalizes that pattern for quantity (Cournot) competition.
Earlier work on information sharing in competing chains (for example Ha, Tong and Zhang, Management Science 2011, on production diseconomies of scale) found related threshold structures under different upstream technologies. The present paper replaces the production cost with a cost-reduction investment.
There are two identical supply chains , each with one manufacturer and one retailer. Retailer faces the inverse demand
where is a demand shock with mean and variance , and is the competition intensity. Manufacturer has unit production cost and lowers it by at effort cost ; a small means efficient cost reduction. Retailer observes a signal with accuracy ; under the linear information structure, .
In stage one, each chain fixes its arrangement : the retailer shares its signal with the manufacturer () or not (). Then the manufacturer sets a wholesale price and a cost reduction, and the retailer a quantity. For each arrangement profile the quantity stage has a linear equilibrium with explicit response coefficients (Lemma 2(a)). These give closed-form ex-ante profits , and for the retailer, the manufacturer and the chain.
The value of information sharing to chain is . In stage one, manufacturer offers retailer the smallest side payment that makes sharing acceptable to the retailer, and chooses or . The result is a symmetric game between the two manufacturers (Table 1). Manufacturer 's payoff is for and for . The standing assumptions are , and .
For fixed , and there are thresholds
such that the set of pure-strategy equilibria of the stage-one game is
In the middle regime, both manufacturers are strictly better off at than at .
A companion item states the Cournot half of Proposition 7(c): for no side payment is needed and is the unique equilibrium.
Proposition 7(a) separates three regimes of cost-reduction efficiency. When cost reduction is efficient (), sharing is dominant. At intermediate efficiency the stage-one game is a coordination game: both chains sharing is Pareto-better for the manufacturers, but both not sharing is also an equilibrium. When cost reduction is inefficient, no chain shares. Competition matters through the gap : a chain whose rival shares tolerates a less efficient cost reduction before it stops sharing, and the thresholds fall as signals become more accurate or competition more intense.
The paper proves these facts by hand-checked algebra, often stated as "we can verify". The formalization turns each such step into a checked statement: the fixed-point identities behind Lemma 2(a), the closed forms of Lemma 3, the reduction of the sign of to the polynomials and , and the monotonicity and location of their roots. None of these results has a machine-checked proof yet. The definitions (response coefficients, profits, side payment, stage-one game) are reusable for the Bertrand half of the paper and for other two-chain information-sharing models.
The obvious approach expands and as rational functions of and tries to read off their signs. That does not finish by itself. After cancelling positive factors, the signs are those of and , which are quadratics in with coefficients polynomial in . The thresholds are defined implicitly by a root of each quadratic crossing . Showing that and are initial intervals of needs the relevant root to be strictly decreasing in , to exceed below and to change sign at . The strict ordering needs a comparison of two roots involving and on . The equilibrium analysis then needs the retailer comparison, to know when the side payment is positive. Table 1's payoff entries are valid only in that case.
Everything is over , in the namespace CompetingChains.Cournot. A general definition TwoPlayerGame gives pure-strategy Nash equilibria of a two-player normal-form game. The definition Setting records the paper's reduced form: the standing assumptions, the response coefficients of Lemma 2(a), the best responses (7) and (9), the ex-ante profit functions of p. 17, the equilibrium profits , , , the stage-one payoff and its set of pure equilibria. The Bayesian stages enter only through these closed forms. The arrangements are an inductive type {S, N}. Manufacturer 2's payoff at is manufacturer 1's payoff at . The chain profit is defined as retailer plus manufacturer profit. The stage-one payoff uses as printed on p. 21, and agrees with Table 1 whenever the side payment is positive.
Conventions and added hypotheses, each disclosed in the items:
The coefficients, profits, and payoffs are definitions, never free parameters. A statement with free coefficients, a goal whose thresholds lack , or one that only asserts membership of would be trivial or weaker, and is not what is posed. No published platform definition states this model, so none is referenced.
Not in scope: Lemma 2's uniqueness (delegated by the paper to earlier work), the wholesale-price and cost-reduction lines of Lemma 2(a), the Bertrand half (Propositions 6(b), 7(b)), the single-chain analysis of §4, Proposition 8 and the numerical study. Proofs of any item are welcome. The polynomial root analysis behind Proposition 6(a) is the main open piece of work.
In random-feature models, also called extreme learning machines or random neural networks, the inner weights of a one-hidden-layer network are drawn at random and only the linear readout is trained. Training is then a least-squares problem, which is why such models, and their dynamic counterparts reservoir computing and echo state networks, are used in practice. The question is how well such a network can approximate a target when it is not allowed to choose its inner weights. Gonon, Grigoryeva and Ortega (Ann. Appl. Probab. 33 (2023) 28–69) answer it with explicit, non-asymptotic bounds. Their first result, Theorem 1, covers static ReLU networks on an arbitrary separable Hilbert space. The later results of the paper, on finite-dimensional inputs and on echo state networks, are built on it.
Timeline:
is a separable real Hilbert space with inner product , and is the rectifier. The inner weights , , are i.i.d. with law . For a readout matrix the random ReLU network is
The target is assumed to have a Fourier representation on the ball of radius : for , with complex measures whose total variations have finite second moments (condition (15)). The sampling law has the product form . Two further quantities enter: , and the density , where . The input is an -valued random variable with law and , independent of the inner weights.
If , condition (i) or (ii) on holds, and the integrals (16) of and are finite, then there is a readout , a measurable function of , with
and for every , with probability at least , . Here and
Milestones 2–6 are stated for a single output component (), to which the proof reduces.
Theorem 1 says that only the readout has to be trained. With inner weights drawn from an essentially arbitrary product law satisfying (i) or (ii), a least-squares readout achieves error with a constant computable from the Fourier data of and the sampling law (Remark 3, p. 38). The finite-dimensional rates of Section 4.2 (Proposition 3, Corollary 1) follow from it, and so do, through the reservoir functional's Fourier representation, the echo state network bounds of Sections 5–6.
The result is proved on paper but has no machine-checked proof. A formal proof needs integral representations of Fourier-type functions by ReLU units, Radon–Nikodym arguments for signed measures on product spaces, and the variance identity for i.i.d. averages. A side product of formalizing it is a correction: the printed constant is false for small and has to be replaced by , which agrees with it for .
There is an obvious argument: sample features from and use Maurey's empirical method. It does not apply, because the features here are ReLU ridge functions of a real-valued bias drawn from , not complex exponentials. The proof must first rewrite the oscillatory representation as an integral of rectifiers, (18)–(20). That step uses the realness of , which is not given and follows only from being real near . The signed measure obtained this way must then be absolutely continuous with respect to the sampling law , with a density whose second moment is controlled by (16). In case (ii), may vanish outside a bounded interval, and the support of has to be matched to it.
A complete development needs the following:
The variance identity (25) and the bound (26) are independent of the Fourier setting and reusable. Contributions to any milestone are welcome, and so are alternative proofs of (19) and (20).
An echo state network with output feedback is a recurrent model whose previous output is fed back into its next hidden-state update. In reservoir computing only the linear output weights are trained, while the internal weights are fixed, typically after being drawn at random. This raises a quantitative question: if the internal rows are sampled from a fixed law, can a network with blocks of random rows and a suitable linear readout approximate a given input–output rule, and at what rate in ? Gonon, Grigoryeva and Ortega answer this for targets generated by contracting reservoir systems. Their Theorem 4 (p. 63) gives, with explicit constants, a probability bound and an excess-risk bound of order , plus a term decaying geometrically in the length of the observation window. The input set is not required to be bounded: the bound depends on the input process only through over the window.
Inputs are vectors in a set and an input history is , with . A target reservoir is a map , with the closed Euclidean ball of radius , such that is an -contraction for every , with . Its reservoir functional is , where for all . The output dimension is .
The approximating network has blocks of rows. Each row is a vector , and the rows of are i.i.d. with law . With an activation and a readout matrix , the system is
with and ; its functional is . For each and a signed measure defines the integral map
The constant measures the size of these densities, and is the approximation error of . The input process is independent of , is an integrable target, and the loss is Lipschitz with constant . The echo state event of (87) is the event that for all and , where .
The milestones are the displayed estimates of the proof, in attack order:
There is a readout , a function of alone, such that for every and every , with probability at least , the event holds and
where is evaluated at fixed network weights.
The bound separates three sources of error: sampling blocks of random rows (rate ), the approximation of by the integral map (), and the finite initialization of the feedback recursion (). Only the readout depends on the target; the internal weights are generated without it. The theorem also bounds the probability that the random feedback map leaves the state ball on which the recursion is controlled, which is the form in which the echo state property enters. Via Theorem 3 (p. 62), which specializes the densities through the paper's Proposition 2, it gives approximation rates for ReLU output-feedback networks.
The paper proves the result on pp. 63–68. No part of it is formalized. A complete development would give machine-checked Rademacher symmetrization and contraction estimates for random features, uniform-over-a-ball bounds for sampled integral maps, and a treatment of finite feedback recursions on product probability spaces, all reusable outside reservoir computing.
A pointwise approximation of by the sampled map does not control the feedback system, because the next feedback value is itself the random output of the previous update. The comparison must hold uniformly over the state ball and over the whole input window, and the event that the recursion leaves the ball must be charged to an explicit probability. The uniform bound requires symmetrization and the Ledoux–Talagrand contraction principle for a supremum over a continuum of states, with per-index contractions; Lipschitz continuity of alone does not supply the vanishing at zero that principle needs. The input is unbounded, so the input dependence must be tracked through and integrated at the end.
States, inputs, outputs and rows are Euclidean spaces (EuclideanSpace); a row is indexed by and the rows by . Time is the index ; the equation (78) is the published ReservoirESN.IsSolution. The rows have law on their own space and lives on a separate probability space; the probability is under the product law, which encodes the independence of §6.1. Signed measures are their Radon–Nikodym densities with respect to , with integrability and first-moment hypotheses. , and are extended nonnegative integrals and suprema, converted to reals only under their finiteness hypotheses; the risk integrals are finite under the loss Lipschitz bound, integrable target and input-moment assumption; the supremum in (87) is unfolded. is assumed jointly measurable, the standing convention that makes and random variables; the standing assumptions and (p. 30) and (§6.1) are hypotheses.
Trivialization ruled out. The readout is a measurable function of the rows only and is chosen before and . A readout allowed to look at the input would make the claim a different and much weaker statement.
Correction of the print. The goal and milestones (91), (93), (96) assume : the contraction principle cited at (91) needs contractions vanishing at zero, while the printed theorem states only that is Lipschitz. ReLU, the paper's application, satisfies it. The goal retains the printed full risk difference. Its proof passes through (88), where an indicator depending on is moved inside a risk integral; this step needs further justification. The milestone quotations keep the printed text.
Contributions are welcome on each milestone, on general Rademacher symmetrization and contraction lemmas for suprema over compact parameter sets, on measurability of suprema of continuous random fields, and on the printed form of the risk bound.
Which cycle lengths a graph must contain is a long-standing theme of extremal graph theory, studied for graphs of given minimum degree, chromatic number or density. A natural class in which to ask it is that of expanders: graphs in which every not-too-large vertex set has many neighbours outside it (Hoory, Linial and Wigderson). It is known that an -expander on vertices has a cycle of length and a cycle of length (Krivelevich's survey, Corollary 3.2 and Theorem 7.4, arXiv:1812.11562); the question is what happens between these extremes.
One cannot hope for a full interval of cycle lengths: the complete bipartite graph is an -expander without odd cycles, and subdividing every edge of a bounded-degree expander times gives an -expander all of whose cycle lengths are divisible by . L. Friedman and M. Krivelevich (Cycle lengths in expanding graphs, Combinatorica 41 (2021); arXiv:1912.11011v2) show that this is the only obstruction: the cycle lengths of an -expander are well spread, in the sense that every window of consecutive integers between logarithmic and linear length contains one. This mission formalizes that theorem (Theorem 1 of the paper) together with the lemmas of its §2.
Let be a finite simple graph on vertices. For , the external neighbourhood is .
All logarithms are base . In Lean these objects are extNbhd, IsKAlphaExpander, IsAlphaExpander, cycleLengths, ball, contract, level and levelSet, in the namespace CycleLengthsExp.WellSpread.
For every there are positive constants , and such that for all large , every -expander on vertices satisfies
The goal fixes only the shape of the dependence on , not the constants, so an improvement of the constants does not invalidate it.
The result. Theorem 1 says that, up to an additive error of order , an -expander contains every cycle length from up to a constant fraction of . The additive error is optimal in its dependence on by the subdivision example, and the logarithmic lower end is necessary because expanders can have logarithmic girth. It implies that is linear in for every -expander; the companion mission of this series (Theorem 2 of the paper) improves the dependence on in that count. The lemmas of §2, especially the robust sub-expander lemmas 2.2 and 2.6, the disjoint-paths lemma 2.3 and the depth-first-search lemma 2.5, are general-purpose statements about vertex expanders that do not depend on the cycle-length question.
Formalizing it. The theorem is proved on paper; none of it is machine-checked. Mathlib has walks, paths, cycles, distances and induced subgraphs, but no vertex expansion, no Menger theorem, no depth-first-search path lemma and no breadth-first-tree construction. This mission produces formal statements of all of these at the level of generality the paper uses, and a complete development would supply reusable lemmas about vertex expanders on finite simple graphs.
The obvious argument fails at the step of hitting a prescribed length. Expansion easily gives long paths and long cycles, but controlling the length of a cycle to within an additive requires a structure with many cycles whose lengths differ by small, controlled amounts. The paper builds it from two breadth-first trees joined by many short disjoint paths, a long path routed through bounded-size subtrees, and a pigeonhole selection that avoids spoiling too many subtrees; the explicit constants of Lemma 2.7 then have to be propagated through Theorem 1. Lemma 2.3 additionally needs Menger's theorem, which is not in Mathlib, and Lemma 2.5 is a depth-first-search argument whose formal invariant is not short.
SimpleGraph (Fin n); the ball-growth milestone uses any finite vertex type. Sizes are Set.ncard; inequalities involving , , or logarithms are stated in ℝ. is (n + 1) / 2. Logarithms are Real.logb 2.G.induce U, the edges of , never the edges of a tree.G.dist u v for in one component. The first inequality of the lemma is false as printed (the path with ) and is not posed. Lemma 2.7, item 4, is posed with as printed, although its proof gives .Walk.IsCycle, never closed walks; Lemma 2.1 never uses G.diam, which is for a disconnected graph; and no statement divides by .Collections of genomes, versioned documents and source-code histories are highly repetitive: most of each new item is a copy of something already stored. Full-text indexes such as the suffix array and the FM-index answer pattern queries on such collections, but their size grows with the text length , not with the amount of distinct content. The number of runs in the Burrows–Wheeler transform (BWT) of the text is a standard measure of repetitiveness, and the run-length FM-index of Mäkinen and Navarro counts the occurrences of a pattern in words. Until the work of Gagie, Navarro and Prezza, however, locating those occurrences, i.e. reporting their text positions, required space proportional to for a sampling step , which defeats the purpose on repetitive data.
Timeline.
A text is a sequence over the alphabet whose last symbol T[n]=\=1SA[1..n][1..n]T[SA[p]..n]SA[ISA[i]]=i. The BWT records the character preceding each sorted suffix, $$BWT[p]=T[SA[p]-1]\ (SA[p]>1),\qquad BWT[p]=T[n]=\\ (SA[p]=1),$$ so that is read as . The LF mapping is the counting formula , where counts BWT symbols smaller than and counts copies of in .
A run is a maximal block of equal consecutive BWT symbols, and is their number. A text position is sampled when its character is the first or last BWT character in its run (Definition 1); at most positions are sampled. Definition 3 cuts into phrases that begin exactly at the sampled positions. For a text position , the phrase head of is the greatest sampled position . The permutation (Definition 2) returns the text position in the preceding suffix-array cell, and the differential arrays are and . A text position starts a phrase of when is the first position of a run.
Let , let be the phrase head of , let , and let be the sample stored at . Then
and , respectively, so that is defined.
A companion item, from the proof of Lemma 2 (p. 12), states that a BWT interval holding both and a non- symbol contains an occurrence of at the first or last position of a run.
The goal says that the numbers , one pair per sampled position, determine the neighbours of every suffix-array cell, after one predecessor search over the sampled positions. Combined with the toehold of Lemma 2, which provides one known cell inside the interval of a pattern, it lets an index list all occurrences in space. This is the locating half of Theorem 1 of the paper. The same mechanism reappears throughout the paper: Lemma 4 generalises it to neighbours, Lemma 5 to the LCP array, and Lemmas 12 and 14 drive the access structures for and in §5.
The results are proved in the paper; none of them has a machine-checked proof. The mission contributes a formal model of suffix arrays, BWT, LF and runs that is independent of any data-structure encoding, a checked proof of the LF identity from the counting formula, and the exact correctness statement behind the -index. The handling of the wrap-around phrase (see below) is a case the paper's proof leaves implicit.
The obvious argument follows the three cells backwards under LF for steps. It rests on two facts that are easy to state and not routine to prove. First, must be derived from the counting formula : this is a stable-sorting argument about suffixes that begin with the same symbol, and it uses the uniqueness of \$$. Second, LF must map adjacent cells of a run to adjacent cells, and one must check that the neighbouring cells never leave the run while the middle cell walks from T[k]T[i+1]i\le k[1..k]T[i+1]T[i]qk-i$ must be tracked through natural-number arithmetic.
Positions are 1-based natural numbers, as in the paper. and are functions read only on . is a hypothesis, IsSuffixArray: it maps injectively into and sorts the suffixes strictly in Lean's lexicographic order on lists. Since \=1ISA[i]0iDSADISA$ are integer-valued.
Pins and guards:
The space and time claims of Lemmas 2–3 and Theorem 1 ( words, time on a word RAM) are out of scope; the goal is their explicit combinatorial content. Two trivializing formalizations are ruled out: defining LF as "the cell holding ", which would make milestone 1 a tautology; and defining the phrase head by iterating LF, which would build the proof into the definition. The phrase head is the maximum of the sampled positions .
A full development needs elementary facts about lexicographic order on lists, counting over finite intervals, and iterates of LF. The suffix-array and BWT layer is reusable beyond this mission; two parallel missions on the same paper share the same core definitions. Proofs of the milestones in any order are welcome, as are alternative routes, e.g. through Lemma 14 and for the left half of the goal.
In interactive decision making, an algorithm chooses actions while learning which model governs its observations. A low-regret guarantee for one algorithm does not by itself say whether every algorithm could do better. The Decision-Estimation Coefficient (DEC) was introduced to express the cost of choosing useful decisions while distinguishing plausible models. Foster, Kakade, Qian and Rakhlin's Theorem 3.2 gives the corresponding lower bound: when a localized model class has large DEC, an adaptive algorithm must incur expected regret under at least one model in the class. This mission formalizes that result for finite decision and outcome alphabets.
The paper's protocol covers bandits, partial monitoring, and reinforcement-learning examples through a common model that maps each decision to a distribution over rewards and observations. Its lower bound concerns the protocol itself, rather than any one algorithm or application. The theorem therefore gives a common test for the limits of learning in several interactive settings. The finite-alphabet representation here retains adaptive decision kernels, which are central to the theorem.
Let be the set of decisions, the set of joint reward–observation outcomes, and the reward map. A model assigns a probability distribution on to each . Its mean reward is , and is a maximizing decision. The gap function is .
At round , an adaptive algorithm assigns a distribution on decisions using the full preceding history. It samples a decision from that distribution and receives an outcome drawn from . The joint law of the length- history is . Following equation (1) of the paper, regret sums the gaps averaged under the algorithm's chosen distribution at each round. Thus its expectation is over the history law, while the inner gap is averaged under . This formulation retains the algorithm's dependence on earlier outcomes.
For probability distributions on , write for squared Hellinger distance. For a reference model and , the DEC of a class is
The uniformly localized class contains those for which for every decision. The density-ratio bound is the supremum of event likelihood ratios over both models, decisions and events, with a lower cutoff of . It may be infinite. These conventions are equations (2), (5), and (12), and the definition immediately before Theorem 3.1 in the source.
Suppose is nonempty, every model is a probability kernel, and for every and . For , set and . The goal is the following supremum form of Theorem 3.2, equation (13):
The paper writes the result with a maximum over and a supremum over , and says that one model attains the resulting bound. Its proof explicitly permits a limit sequence when the inner supremum is not attained. The displayed statement records exactly the resulting bound on the supremum of expected regret. It implies an arbitrarily close model-specific bound for each fixed and .
The milestones follow the statements the paper's proof (App. C.1.3, pp. 90–91) uses, in attack order: the multiplicative Hellinger comparison of Lemma A.11; the difference comparison of Lemma A.12; the Hellinger bound on adaptive history laws, with ; the DEC comparison at the reference model's average play , (129); the localized gap comparison (132); and the final inequality for . Their source wording and page citations are preserved in the milestone list.
The theorem supplies a quantitative obstruction to uniformly small expected regret. It uses the same coefficient that appears in the paper's upper-bound framework, so a model class with matching upper and lower DEC estimates can have its regret scale characterized through one object. In particular, the coefficient is sensitive to the model neighborhood relevant at horizon ; replacing it by a global coefficient would lose the theorem's stated localization. The paper applies this framework to bandit and reinforcement-learning classes.
The goal and milestone declarations here are open Lean statements with checked syntax and types. A complete formalization would supply proofs of the Hellinger comparisons, the history-law inequality, and the lower bound itself. The history and density-ratio definitions are reusable for other adaptive finite-alphabet lower bounds; the published FoundationsRL mean reward, Hellinger distance and DEC definitions are reused directly.
A fixed sequence of decision distributions does not describe the theorem's algorithms: later decisions depend on outcomes produced by the unknown model. The comparison must therefore use two different laws on entire histories generated by the same adaptive kernels under two models. A bound on a single round's divergence cannot simply be multiplied by without accounting for the dependence of future decision distributions on past observations. The DEC itself involves a minimum over decision distributions and a supremum over models, which need not be attained.
The Lean representation uses finite and ; probability laws and expectations are finite vectors and sums. This is a finite-alphabet specialization of the paper's measurable-space setting. Histories are functions from round indices to decision–outcome pairs. The algorithm is a family of kernels from every possible past history to a decision distribution. Its law is the product of its decision probabilities and the model's outcome probabilities. Rounds are indexed from zero in Lean, corresponding to the paper's rounds .
Every model in and every algorithm kernel is normalized and nonnegative. The mean reward range , nonempty model class, maximizing selector, and positive horizon are explicit hypotheses. They keep the real-valued supremum and infimum in the published DEC from taking Lean's default values on empty or unbounded sets. An event with positive numerator and zero denominator has infinite likelihood ratio; remains allowed because the theorem uses . Its logarithm therefore has a finite, positive argument for . The goal uses the exact constants and . The proof's constant is printed on p. 90 as ; the formalization uses , the hypothesis of Lemma A.13 (98) from which is derived. Without it the history bound fails for two nearly equal models, and with it still holds, so the goal is unaffected. The intermediate results that select a model approaching a supremum carry an arbitrary slack , the paper's "limit sequence".
Contributions should preserve the adaptive history law and equation (1)'s decision-distribution regret. A statement restricted to predetermined decisions would leave out the central quantifier of Theorem 3.2. The published FoundationsRL definitions of , and provide the shared finite model interface; the new history and density-ratio layer can support further lower bounds in this series.
Online selection problems ask an algorithm to accept or reject elements as they arrive, while keeping the accepted set feasible. The decisions are irrevocable, and the arrival order can be chosen after the random activity of the elements is known. A guarantee for one constraint is therefore useful only if it remains meaningful when several constraints apply at once. In Feldman, Svensson and Zenklusen's paper, the constraints include matroid independence, matching, and knapsack capacity. A set satisfying two such requirements lies in the intersection of their feasible families. Theorem 1.9 establishes how their online guarantees combine: the two selectability factors multiply.
The result belongs to a sequence of statements in the paper. The authors first define greedy online contention resolution schemes and their selectability guarantee in Definitions 1.3–1.5. They then state the combination theorem in the introduction and identify the intersection construction in Definition 2.10. Lemma 2.11 supplies the precise selectability assertion for that construction. This mission isolates those claims so that later formalizations of specific constraints can reuse them without repeating the probability argument.
Let be a finite ground set and a family of feasible sets. A fractional point determines a random active set : each belongs to independently with probability . Thus a particular set has weight
A greedy online contention resolution scheme, or greedy OCRS, chooses a down-closed family . As active elements arrive, it accepts an element when adding that element to those already accepted remains in . In a randomized scheme, the choice of is random and independent of . The family contains the empty set, as the procedure begins with no accepted elements.
An element is selectable for a realized active set and family if every with still permits : . This condition covers every possible set that might have been accepted before arrives. A greedy OCRS is -selectable for a relaxation when the probability of this event is at least for every and every . The probability includes both draws when the family is randomized. Here and .
For two feasible families , the combination of their greedy OCRSs independently draws and , then uses . This is a family of sets satisfying both constraints. The proof also uses , the indicator that for every lying in . For selectability itself, .
For , let the first scheme be -selectable and the second -selectable. The mission asks for a greedy OCRS on the intersection with
The target records existence of the combined scheme, independent of a particular proof of its selectability. The paper also claims preservation of polynomial-time efficiency; the finite mathematical model here does not assign a complexity measure to a family sampler or membership oracle, so that clause is outside this target.
The lemma names the combined scheme: independently draw both greedy families and use their intersection. It asserts the same bound for that specific scheme. The earlier milestones record the two order properties of and the finite product-measure correlation inequality appearing in the lemma's proof. Their statements keep the original quantifiers over active sets and families visible.
The theorem turns guarantees for individual constraints into a guarantee for simultaneous constraints. If a matroid scheme and a matching scheme meet the same scale parameter , their intersection is governed by the product of their selectability factors. The factor loss is explicit, which lets subsequent algorithmic results track it without redefining the combined scheme. The lemma additionally fixes the actual distribution over intersected families, avoiding ambiguity about how two randomized procedures are coupled.
Mathlib already provides a general finite FKG inequality, but it does not state the paper's OCRS objects, the selectable event, or the intersection theorem. This mission adds those interfaces and the specialized correlation statement. The source results are proved in the cited paper; the local theorem files in this proposal are statements for later machine-checked proofs. A complete formalization would connect the finite active-set weights to Mathlib's lattice correlation theorem and then establish the randomized family bookkeeping. The finite probability definitions can also serve other OCRS results in the same paper.
The obvious argument would multiply the two probabilities that is selectable for the separate families. Both events depend on the same active set , so they are not independent even when the families are drawn independently. Moreover, selectability for the intersection checks only sets belonging to both families, whereas the original bounds check each family separately. The formal statements must keep these two dependencies distinct. The paper's two monotonicity claims and its FKG display identify the needed intermediate assertions, but their use with an arbitrary random choice of families still requires careful finite-sum reasoning.
The ground set is a finite Lean type and subsets are Finsets. Feasibility is a predicate on those finite sets. Fractional points are real-valued functions, and each input relaxation is represented as a set of such functions with an explicit coordinate bound . The scale and selectability parameters belong to . The point ranges over , not over an independently chosen intersection of scaled sets, so the case retains the paper's meaning. The finite products define the law of ; no measure-theoretic integral is used.
A randomized scheme is a probability weight on possible greedy families for every input point. The combined weight is the product of the two original weights summed over pairs with the required intersection, expressing independent draws. The family distribution is independent of the active-set draw. This sampling convention is necessary for the stated product guarantee and is made explicit here although Definition 2.10 does not spell it out. Each greedy family contains and lies in its own feasible family. These requirements exclude the empty-family and unconstrained-family encodings that would make selectability trivial. The unit-cube bounds prevent negative active-set weights.
The Lean declarations focus on the finite selectability guarantee. They abstract a polytope by its set of fractional points and use the paper's unit-cube condition; they do not formalize a polyhedral representation or test that its binary points equal the feasible sets. A full development of the paper's algorithmic setting would additionally represent online arrival orders, family sampling algorithms, membership oracles, and polynomial running time. Contributions establishing the finite probability lemmas, the specialized FKG statement, and Lemma 2.11 are directly useful here. The general active-set and selectability definitions are reusable across the paper's other missions.
Hypergraph Turán problems ask how many edges a -uniform hypergraph on vertices can have without containing a fixed sub-hypergraph. For graphs () the theory is well developed; for exact answers are rare and are known mostly for small, dense configurations such as the Fano plane or expanded triangles. Paths are the natural sparse test case. For graphs, Erdős and Gallai (1959) showed that a graph on vertices without a path of length has at most edges. For hypergraphs there are several notions of path: Berge paths (Győri, Katona and Lemons, 2010), loose paths (Mubayi and Verstraëte, 2007, asymptotic bounds) and the most restrictive notion, linear paths. The case of two edges was solved by Frankl (1977), and the case asymptotically by Frankl and Füredi (1987).
Füredi, Jiang and Seiver (arXiv:1108.1247v1, published in Combinatorica 34 (2014), doi:10.1007/s00493-014-2838-4) determined the Turán number of every -uniform linear path exactly, for and large, together with the unique extremal families. It is one of the few exact hypergraph Turán results for an infinite family of forbidden hypergraphs.
The vertex set is . A family is a set of subsets of ; it is -uniform if , the set of all -element subsets.
A linear path of length is a sequence of distinct sets such that
The -uniform linear path of length is written ; a family contains it if some of its members form a linear path. The Turán number is the maximum size of a -uniform family on that does not contain .
Two counting functions describe the answer:
For a set of elements, is the number of -sets meeting (the star family of ), and adds the -sets of that contain two fixed vertices (the even family).
The proof is phrased in the language of the delta-system method: -stars (sets pairwise meeting in a common kernel), the kernel degree (the largest for which an -star with kernel exists), -homogeneous families (k-partite families whose intersections follow a single intersection-closed pattern of subsets of , each intersection being the kernel of an -star), the rank of , the kernel graph of , and the -blowup of a graph .
For every and there is such that for all :
and in each case a -uniform, path-free family of that size is exactly the star family of some -set (odd case), respectively the even family of some -set and two distinct vertices (even case).
In the order the proof uses them:
The theorem gives the exact extremal number and the unique extremal configuration for every linear path when , and its proof yields a stability statement (Theorem 5.1 of the paper): a path-free family of nearly extremal size is close to a star family. The method is the standard template for exact results on sparse hypergraphs: delta-system decomposition, an asymptotic bound from a graph theorem applied to a kernel graph, then stability and cleaning.
The result is proved in the paper. As far as the platform's catalog shows, none of it is formalized: Mathlib has the intersecting Erdős–Ko–Rado theorem () but not the -intersecting version with uniqueness for large , not Erdős' matching theorem, not the Erdős–Gallai circumference theorem, and no delta-system machinery. A formalization would produce reusable libraries for each of these, and the first machine-checked exact hypergraph Turán number for an infinite family.
The obvious argument — bound the number of members through each vertex and sum — gives only with a wrong leading constant, because a path-free family can have vertices of almost full degree. Exactness needs three layers that do not reduce to one another. First, the intersection semilattice lemma (Lemma 3.1) is a deep structural theorem with a doubly exponential constant; it is cited, not proved, in the paper. Second, the asymptotic bound passes through the Erdős–Gallai circumference theorem, itself a nontrivial graph result. Third, the exact value requires a stability argument with several error terms (, ) that must be balanced, followed by Erdős' matching theorem and the 2-intersecting Erdős–Ko–Rado theorem for large , both with uniqueness. The structural lemmas of §§3–4 are elementary but involve greedy embeddings in which disjointness of the new vertices has to be maintained carefully.
Vertices are Fin n; families are Finset (Finset (Fin n)); -uniformity is 𝓕 ⊆ univ.powersetCard k. A linear path is an injective map Fin ℓ → Finset (Fin n) into the family with consecutive members meeting in exactly one vertex and non-consecutive members disjoint. The Turán number is a Finset.sup of cardinalities over all path-free -uniform subfamilies, a finite attained maximum for ; at the feasible set is empty and Lean returns zero, which no theorem here uses. Partitions into parts are part maps Fin n → Fin k; stars are finsets of distinct petals; the rank is a minimum computed with sInf, exact because intersection patterns consist of proper subsets of . "Sufficiently large " and every are explicit existential constants chosen before and the family.
Hypotheses added relative to the page: Theorem 3.8 assumes the homogeneous family is nonempty (the empty family is homogeneous for every pattern, and the proof starts from a member). Lemma 4.2 states , implicit in the paper's definition of a blowup using new vertices; it excludes a false zero-threshold case at . Lemma 4.3 is stated for an arbitrary choice of a vertex in each member, a generalization of the printed lemma, whose proof uses only . Bound (1) is posed for . Claims 2–3 are stated stand-alone with the -set existentially quantified.
Trivializing formalizations are ruled out: the goal asserts the value and the uniqueness of the extremal family, the Turán number is a true maximum rather than a junk supremum, the linear path requires intersections of size exactly one and disjointness of non-consecutive members, and all constants are quantified before .
Needed infrastructure: the delta-system method (Lemma 3.1), Erdős–Gallai for circumference, Erdős' matching theorem and -intersecting Erdős–Ko–Rado for large . Each is reusable well beyond this mission, and contributions of any of them are welcome.
Quantum information often describes a system through a state shared among many small registers. One would like to replace the state on a few registers by a product of their individual states, because product states are easier to estimate and optimize over. The usual finite quantum de Finetti theorems obtain such approximations from permutation symmetry. A physical preparation, however, need not be symmetric. Berta, Borderi, Fawzi and Scholz give a quantitative statement that instead selects the retained registers at random and conditions on measurements of other registers. Their Theorem 2.5 is the target here.
The authors place this result alongside their hierarchy for constrained bilinear optimization, but the theorem without symmetry is independent of the hierarchy. In §2.6 they compare its polynomial dependence on the local dimension and the number of retained registers with the earlier no-symmetry approximation discussed in their reference [12]. The result identifies exactly what random selection and measurement can supply when a global permutation-invariance hypothesis is unavailable.
Let be a quantum system of dimension , and let be an arbitrary density operator on copies of . Choose a uniformly random permutation of these copies. Its first positions form an ordered tuple of systems to retain; the remaining positions form an ordered tuple available for measurement. There is no symmetry condition on .
A measurement on has finitely many outcomes and positive operators whose sum is the identity. Measure the first systems , where , and condition the retained state on the observed outcomes. Write for that conditional state and for its marginal on the th retained system. The trace norm measures the error between and . The expectation is over the uniform permutation and the measurement outcomes, with their Born-rule probabilities.
The distortion with side information of a fixed measurement is the largest ratio between an input trace norm and the norm left after measuring only its factor. The input ranges over Hermitian operators on , over every finite-dimensional side system , with zero partial trace on both and . The paper's is the infimum of this distortion over all measurements on equation (10). A state two-design is a finite family of rank-one projectors whose average second tensor power is the projector onto the symmetric subspace with the normalization in Lemma D.1. The projectors give an explicit measurement with distortion at most .
The principal target is the explicit form of Theorem 2.5. For , put . With the two-design measurement, some satisfies
Here the in the expectation is the outcome string for the first members of . The same is chosen before taking that expectation. This rate is stated with its constants and its two consecutive inequalities; an existence assertion without the error bound would lose the theorem's content.
The milestone path also states the telescoping trace-norm inequality of equation (12), the measurement estimate of Lemma D.1, and the final averaged inequality on p. 11. A companion milestone treats any fixed POVM with its own distortion. That formulation captures the proof's arbitrary-measurement step without treating the infimum as if every measurement attained it.
For an arbitrary multipartite state, random ordering and conditioning give one measured prefix length at which the selected registers have small expected distance from a product. The explicit rate is polynomial in and and decays as . It therefore gives a quantitative approximation guarantee under a selection rule that can be applied without first establishing exchangeability Berta et al., §2.6.
The theorem is proved in the paper; the work here is to express its state, measurement, conditional distribution, and norm bound in Lean and to connect the estimate to reusable finite-dimensional quantum-information definitions. The local statements are currently proof obligations, not machine-checked proofs. The published density-operator, trace-norm, and partial-trace definitions are reused. Once proved, the statements can serve as a precise interface for subsequent formal work on randomized subsystem selection and information-theoretic decoupling.
Randomly choosing systems does not turn the original state into a product state. A direct bound on the distance to a product can be large even when each one-system marginal is simple, because correlations among the retained systems remain. Equation (12) breaks the total error into successive correlation terms; the paper controls their average by measuring other systems and using information-theoretic estimates. A second difficulty is that a measurement can erase distinctions between different input operators. The two-design estimate supplies a dimension-dependent bound on that loss, uniformly over the size of a side system.
The printed theorem leaves the measurement unspecified while using the minimum distortion over all measurements. A trivial measurement cannot satisfy that reading. The proof explicitly permits the measurement built from a state two-design, with replacing ; that is the measurement used in the goal proof of Theorem 2.5, p. 10.
The system has basis Fin dB; copies have basis Fin n → Fin dB. The formalization writes , assumes , and ranges over . A state is a positive semidefinite complex matrix with trace one. Permutations act on the copy coordinates, and their finite uniform average models the paper's random ordered tuples. Measurement outcomes are finite words; the conditional state divides the unnormalized post-measurement state by its probability. A zero-probability outcome uses Lean's zero inverse and contributes zero to the weighted expectation. The existence of a state and of a nonempty two-design rules out zero-dimensional and empty-outcome instances in the goal.
The fixed-measurement distortion and take values in extended nonnegative reals, so a measurement that destroys a nonzero operator has infinite distortion. The logarithm is base two except for . The definitions use the paper's unnormalized trace norm, with no factor . No mutual-information estimate or Pinsker inequality is assumed in the goal: both belong to possible proofs. Contributions proving the stated milestones, the positivity and normalization of the conditional states, or reusable trace-norm facts for finite tensor products all advance the target.