Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Prove that a uniform randomized classical polynomial-time algorithm estimates the maximum Quantum Max-Cut energy within a factor of on every graph with nonnegative rational edge weights.
The output is a nonnegative rational number satisfying for every prescribed random tape and . The expectation is over the algorithm’s internal fair random bits, separately for each input graph; running time is polynomial on every run. Here .
The QMC reference attributes this value jointly to ALMPS25’s partially entangled matching algorithms and BBKL26’s later matching bound. The ESA 2025 paper alone states 0.611; this 0.614 target also cites the public BBKL26 preprint. Reference table. Source 1 · Source 2.
The goal uses the campaign’s shared classical numerical-output model. A complete proof must justify finite-bit computation, precision, randomization and the stated ratio. The algorithm may use any valid construction.
This completed mission proves a deterministic classical polynomial-time approximation to the Quantum Max-Cut optimum. Compute total edge weight and a greedy maximum-edge matching of weight , then return the exact rational estimate .
The proof establishes and certifies the concrete classical Turing-machine computation, including parsing, exact rational arithmetic, and output encoding. Empty graphs and zero weights are included.
The mathematical ingredients are published in Anshu, Gosset, and Morenz, TQC 2020, Lemma 5 / Eq. (9) and Eq. (25). This is a derived numerical construction from those ingredients. Accepted Lean proof.
This completed mission proves existence of a classical polynomial-time numerical approximation to Quantum Max-Cut. Every returned rational estimate is at most the unrestricted optimum, and its expectation is at least .
The accepted proof uses the verified deterministic construction and monotonicity. The historical benchmark is Gharibian–Parekh, APPROX/RANDOM 2019, Theorem 6; the verified construction here uses published star and matching estimates from Anshu, Gosset, and Morenz, TQC 2020, Lemma 5 and Eq. (25).
Accepted Lean proof. Polynomial bit complexity, exact rational output, and empty or zero-weight graphs are included.
This completed foundation proves a deterministic classical polynomial-time numerical estimator for Quantum Max-Cut. If is total edge weight, the algorithm returns the exact rational .
The verified guarantee is and , for all nonnegative rational weights, including empty graphs and zero weights. Its proof includes the campaign's actual input/output encodings and polynomial-time Turing-machine certificate.
Accepted Lean proof. The Quantum Max-Cut normalization is the published convention of Anshu, Gosset, and Morenz, TQC 2020.
Quantum Max-Cut asks for a high-energy state of an antiferromagnetic spin system specified by a weighted graph. Vertices carry qubits, and an edge rewards the two qubits for occupying their antisymmetric singlet state. A single qubit participates in several interactions, so maximizing each edge separately generally gives incompatible demands. The problem supplies a concrete setting in which to compare efficiently generated quantum states with the best state allowed by quantum mechanics.
The relevant quantity is an approximation ratio: a constant fraction of the optimum that one algorithm guarantees on every input graph. The target concerns the whole input family, rather than favorable examples or numerically observed performance. Gharibian and Parekh established an efficient product-state guarantee of 0.498 in 2019. Parekh and Thompson subsequently established a 1/2 product-state guarantee. Later algorithms use entanglement to improve the general-graph ratio, including 0.595, 0.611, and the 0.614 efficient guarantee of Bakshi, Basu, Kothari, and Li. These mathematical results provide targets for formalization; their existence does not supply Lean proofs in the shared model.
An input consists of a finite vertex set and a nonnegative rational weight for each unordered pair . A zero weight represents an absent edge. The associated Hamiltonian is
Here exchanges qubits and , and are the Pauli matrices. This fixes the normalization: a singlet earns energy on a unit-weight edge, and an antiparallel computational-basis pair earns . A quantum state is represented by complex amplitudes indexed by bitstrings. Its squared norm is the sum of the squared absolute values of those amplitudes. The energy is evaluated by a finite sum of squared amplitude differences under coordinate swaps, equal to the Hamiltonian expectation in this convention.
A prepared state may use additional qubits, called ancillas. The input graph occupies the first output wires. The Hamiltonian acts only on these wires, while the other wires are retained. This convention includes mixed states on the graph qubits and averages over quantum measurement outcomes without selecting a favorable outcome.
The first open campaign target is . Prove that there exists one uniform polynomial-time quantum algorithm satisfying
The optimum ranges over all normalized quantum states on the graph qubits, including entangled states. The formal statement expresses the same comparison by requiring the output energy to dominate times the energy of every normalized comparison state. One algorithm and one polynomial runtime bound must work for every input graph. The output may depend on the graph and cannot depend on the comparison state used to test the inequality.
The target is an exact existential guarantee in the campaign's shared model. It does not prescribe a rounding method or a restricted output-state family. The foundation is already proved; is the next open value, and remains a later challenge.
The target follows the historical general-graph guarantee of Gharibian and Parekh (2019), Theorem 6, as summarized in the Quantum MaxCut reference. This mission requests a proof of algorithmic existence under the common finite H/T/CNOT circuit model. The cited paper motivates the numerical target; transferring ideal real-valued rounding into this exact gate model still requires preparation and precision justification.
A successful Lean development connects a finite classical computation, its output preparation circuit, and the energy guarantee. The existing server-accepted proof supplies a fully verified starting point. Contributions may follow any mathematically sound route to the common existential theorem; a stronger guarantee also suffices.
The central obligation is to exhibit an algorithm and prove both its runtime and its worst-case energy guarantee. The assertion that some state attains the optimum does not provide an algorithm for finding or preparing it. Likewise, a short circuit description alone is insufficient unless the circuit can be generated uniformly in polynomial time from the encoded graph.
The optimal state may have entanglement across many vertices. A proposed algorithm therefore has to be compared against all quantum states, rather than only against product states or its own output family. Local edge gains must be justified under the simultaneous state preparation on the entire graph. The formalization also needs to account for exact rational input comparisons, empty graphs, zero-weight edges, and any ancillary wires.
The foundation is pinned to Lean 4.33.1 and its selected Mathlib environment. The computational model is a uniform classical polynomial-time generator of finite circuits over H, T, and CNOT, followed by execution of the generated circuit. Every wire starts in the all-zero state. CNOT requires distinct control and target wires. The definition uses Mathlib's explicit polynomial-time Turing-machine predicate, not a freely assumed efficiency label.
Rational numerators and denominators have fixed binary encodings. The graph order, circuit width, and gate wire indices are encoded in unary, and every gate is listed explicitly. Unary wire indices add only polynomial overhead because register width is already unary. Thus the input cannot hide an exponentially large vertex set, and a short output cannot hide an exponentially large ancillary register or an implicit circuit. The expected-energy inequality retains all output branches. It is not a claim that each individual run attains the bound or that the output energy can be simulated classically in polynomial time.
The ratio is exact in this fixed gate model. An argument using ideal arbitrary real rotations needs a separate preparation and precision justification; approximate universality by itself does not preserve an exact sharp threshold. The shared model contains no custom axioms or unproved supporting lemmas. The open goal theorem intentionally has an unfinished proof. Contributions establishing the state semantics, energy inequalities, concrete circuit generators, and their genuine runtime certificates all support the final existence theorem.
The Quantum MaxCut reference records the progression from the general-graph guarantee of GP19 to and later improvements. The campaign begins with a completed Lean proof at , then asks for as its first open target. Published mathematical values and the campaign's verified record are distinct: this mission has no accepted proof yet.
Quantum Max-Cut asks for a high-energy state of an antiferromagnetic spin system specified by a weighted graph. Vertices carry qubits, and an edge rewards the two qubits for occupying their antisymmetric singlet state. A single qubit participates in several interactions, so maximizing each edge separately generally gives incompatible demands. The problem supplies a concrete setting in which to compare efficiently generated quantum states with the best state allowed by quantum mechanics.
The relevant quantity is an approximation ratio: a constant fraction of the optimum that one algorithm guarantees on every input graph. The target concerns the whole input family, rather than favorable examples or numerically observed performance. Gharibian and Parekh established an efficient product-state guarantee of 0.498 in 2019. Parekh and Thompson subsequently established a 1/2 product-state guarantee. Later algorithms use entanglement to improve the general-graph ratio, including 0.595, 0.611, and the 0.614 efficient guarantee of Bakshi, Basu, Kothari, and Li. These mathematical results provide targets for formalization; their existence does not supply Lean proofs in the shared model.
An input consists of a finite vertex set and a nonnegative rational weight for each unordered pair . A zero weight represents an absent edge. The associated Hamiltonian is
Here exchanges qubits and , and are the Pauli matrices. This fixes the normalization: a singlet earns energy on a unit-weight edge, and an antiparallel computational-basis pair earns . A quantum state is represented by complex amplitudes indexed by bitstrings. Its squared norm is the sum of the squared absolute values of those amplitudes. The energy is evaluated by a finite sum of squared amplitude differences under coordinate swaps, equal to the Hamiltonian expectation in this convention.
A prepared state may use additional qubits, called ancillas. The input graph occupies the first output wires. The Hamiltonian acts only on these wires, while the other wires are retained. This convention includes mixed states on the graph qubits and averages over quantum measurement outcomes without selecting a favorable outcome.
The requested bound is . The goal is the existence statement
The optimum ranges over all normalized quantum states on the graph qubits, including entangled states. The formal statement expresses the same comparison by requiring the output energy to dominate the scaled energy of every normalized comparison state; it does not introduce a separate optimizer or a supremum. One algorithm and one polynomial runtime bound must work for every input graph. The output may depend on the graph but cannot depend on which comparison state is used to test the inequality.
This mission fixes the starting value . A later improvement can reuse its definitions while changing only the numerical value in the campaign template.
The bound is a known mathematical target, not a new approximation claim. The mission asks for a Lean proof of the stated algorithmic existence theorem. A successful development must connect a finite classical computation, its output preparation circuit, and the energy guarantee. Verifying only an energy inequality for an unspecified state leaves out the computational content.
The shared definitions give later work a stable meaning for input size, permissible preparation, and approximation ratio. They also make comparisons between different state families possible without changing the optimization problem. The weighted-star energy inequality of Anshu, Gosset, and Morenz is a useful established supporting result for a first proof. Supporting lemmas and reusable proofs can be developed separately while preserving the campaign's common existential target.
The central obligation is to exhibit an algorithm and prove both its runtime and its worst-case energy guarantee. The assertion that some state attains the optimum does not provide an algorithm for finding or preparing it. Likewise, a short circuit description alone is insufficient unless the circuit can be generated uniformly in polynomial time from the encoded graph.
The optimal state may have entanglement across many vertices. A proposed algorithm therefore has to be compared against all quantum states, rather than only against product states or its own output family. Local edge gains must be justified under the simultaneous state preparation on the entire graph. The formalization also needs to account for exact rational input comparisons, empty graphs, zero-weight edges, and any ancillary wires.
The foundation is pinned to Lean 4.33.1 and its selected Mathlib environment. The computational model is a uniform classical polynomial-time generator of finite circuits over H, T, and CNOT, followed by execution of the generated circuit. Every wire starts in the all-zero state. CNOT requires distinct control and target wires. The definition uses Mathlib's explicit polynomial-time Turing-machine predicate, not a freely assumed efficiency label.
Rational numerators and denominators have fixed binary encodings. The graph order, circuit width, and gate wire indices are encoded in unary, and every gate is listed explicitly. Unary wire indices add only polynomial overhead because register width is already unary. Thus the input cannot hide an exponentially large vertex set, and a short output cannot hide an exponentially large ancillary register or an implicit circuit. The expected-energy inequality retains all output branches. It is not a claim that each individual run attains the bound or that the output energy can be simulated classically in polynomial time.
The ratio is exact in this fixed gate model. An argument using ideal arbitrary real rotations needs a separate preparation and precision justification; approximate universality by itself does not preserve an exact sharp threshold. The shared model contains no custom axioms or unproved supporting lemmas. The open goal theorem intentionally has an unfinished proof. Contributions establishing the state semantics, energy inequalities, concrete circuit generators, and their genuine runtime certificates all support the final existence theorem.
Quantum Max-Cut is an optimization problem for a system of interacting qubits. An input graph specifies which pairs interact and the nonnegative weight of each interaction. The task is to prepare a quantum state with high energy relative to the maximum permitted by quantum mechanics. This makes approximation algorithms a way to compare feasible state preparations with an optimum that can require complicated entanglement.
A campaign tracking approximation ratios needs both a stable common statement and an actual proved starting value. This mission supplies the foundation at ratio . The value is a basic mathematical baseline, not a new approximation record. Stronger mathematical results are known: Gharibian and Parekh obtained 0.498, and Parekh and Thompson obtained a product-state guarantee of . More recent work gives an efficient 0.614 guarantee. These are literature targets for further formalization. Their numerical values are separate from the campaign's machine-checked record.
The input has vertices and a nonnegative rational weight on every unordered pair . A zero weight represents an absent edge. The Hamiltonian convention is
The operator exchanges two qubits, and are the Pauli matrices. In this normalization, a singlet on a unit-weight edge has energy , and an antiparallel computational-basis pair has energy . The Hamiltonian convention of Anshu, Gosset, and Morenz, Eq. (5) agrees with this convention.
A state is represented by complex amplitudes on bitstrings, normalized by the sum of their squared absolute values. Its energy is a finite sum of squared differences under swaps of bit coordinates. Preparation circuits can contain ancillary qubits. The graph occupies the first output wires; every other wire is retained, and the Hamiltonian acts only on graph wires. This describes expected energy on the graph even when the graph qubits are entangled with ancillas.
The goal is the existential algorithmic statement
Here is the maximum energy over all normalized quantum states on the graph. The formal statement avoids introducing a separate optimum: it requires the output energy to be at least one quarter of the energy of every normalized complex comparison state.
One algorithm and a single polynomial runtime bound must work for every input graph. The generated circuit may depend on that graph but cannot depend on the comparison state used to test the guarantee. Empty vertex sets and zero-weight graphs are included. The claim is about expected output energy, with all ancillary wires retained; it does not select a favorable measurement outcome.
A local Lean 4.33.1 development now proves this complete existential statement, including an explicit uniform classical circuit generator and its polynomial-time Turing-machine certificate. The proof's axiom check lists only Lean's standard axioms. Acceptance by the platform's proof verifier remains a separate publication step. The local proof must not be reported as an accepted platform result before that step succeeds.
This foundation establishes a usable point from which stronger ratios can be pursued without changing the meanings of input size, allowed preparation, or approximation. The mission is the next open challenge under the same definitions. Its mathematical feasibility does not supply an accepted Lean proof of its energy and runtime obligations. Later campaign entries can target further improvements while importing the common model unchanged.
A performance estimate for a quantum state does not establish a polynomial-time approximation algorithm. The complete claim also requires a uniform finite computation that generates the state-preparation circuit. A concise circuit description is insufficient when its parameters or gate list could require an unbounded search.
The input and output representations therefore contribute to the mathematical content. They must charge for vertex count, register width, individual gates, and rational input bit lengths. The physical comparison is also unrestricted: the reference state may be entangled across the entire graph. A proof against only a chosen output family would assert a different approximation guarantee.
The foundation uses Lean 4.33.1 with the selected Mathlib revision. Inputs have nonnegative rational weights. Rational numerators and denominators use fixed self-delimiting binary encodings. The graph order, output-register width, and gate wire indices use unary encodings. Every gate is explicitly listed. Unary wire indices introduce only polynomial overhead because register width is already charged in unary.
An algorithm is a uniform classical polynomial-time generator of finite H/T/CNOT circuits, followed by execution of the generated circuit. Every wire starts in the all-zero state. CNOT requires distinct control and target wires. Mathlib's explicit Turing-machine predicate supplies the runtime meaning; efficiency is not a freely assumed label.
The ratio is exact in this fixed gate model. The local proof uses exact allowed gates and does not require a gate-synthesis error allowance. In general, an ideal arbitrary-real-rotation algorithm needs its own connection to this preparation model. The shared definition bundle contains no approximation axiom or unproved supporting theorem. The separate proof establishes the state-energy, finite computation, and runtime obligations for this starting value.
Metabolic control analysis (MCA) describes how changes in enzyme activities propagate through a biochemical network. It is used to separate local biochemical sensitivity from global system-level control, which is relevant to pathway engineering, drug-target analysis, and quantitative interpretation of steady-state experiments. The summation and connectivity theorems are the algebraic backbone of this framework: they constrain how concentration control, flux control, and local elasticities can vary together. The source formalized here is Weijiu Liu, “Simple Proofs of the Summation and Connectivity Theorems in Metabolic Control Analysis,” arXiv:2501.12519v2 (2025), especially Sections 2–3: https://arxiv.org/abs/2501.12519.
Fix finite index types Fin n for reactions and Fin m for internal concentrations. A parameter vector is a function p : Fin n → ℝ, and a steady-state concentration map is s : (Fin n → ℝ) → (Fin m → ℝ). Each enzyme-catalysed rate is represented by a function f k : (Fin m → ℝ) → ℝ, with total rate v_k(p) = p_k f_k(s(p)). A stoichiometric matrix N : Matrix (Fin m) (Fin n) ℝ maps reaction rates to concentration dynamics; the steady-state condition is N.mulVec (fun k => v_k(p)) = 0 for every parameter vector.
The formal development defines the derivative matrix D from Mathlib's Fréchet derivative fderiv, with entries D k j = ∂f_k/∂s_j, and the sensitivity matrix S with entries S i l = ∂s_i/∂p_l. It then defines the dimensionless elasticity, concentration-control, and flux-control coefficients by logarithmic derivatives:
Here J = R v is any finite collection of linear fluxes obtained from a matrix R : Matrix (Fin q) (Fin n) ℝ.
Under differentiability of every f k and of s, the all-parameter steady-state identity, a left inverse for N * diagonal p * D, and the required nonzero concentration and rate values, prove
The Lean goal is the theorem MCAEndToEndMission.concentration_connectivity, stated as the normalized form of the published MCAEndToEnd.normalized_connectivity result.
If the steady-state map is homogeneous of degree zero, prove for every concentration index i
If the steady-state map is homogeneous of degree zero and each selected flux is nonzero, prove for every flux index r
Under the same differentiability, steady-state, inverse, and nondegeneracy assumptions, prove for every flux r and concentration index j
The four identities describe complementary conservation laws for local and global control. Concentration summation expresses invariance under a common rescaling of all enzyme parameters. Flux summation records first-degree homogeneity of fluxes in those parameters. Concentration connectivity relates parameter sensitivity to local concentration elasticity, while flux connectivity states that the induced flux-control vector annihilates the elasticity matrix. Together they provide consistency checks for analytic calculations and a reusable interface for later MCA results.
The mathematical results are already machine-checked in the published Lean definition MCAEndToEnd_formalization. This mission packages the four theorem statements as an auditable research-paper formalization with a clean dependency on that definition. It preserves the explicit derivative construction, chain-rule proofs, product-rule calculation, diagonal inverse identities, and all nondegeneracy conditions, so future work can reuse the declarations rather than treating the control coefficients as free matrices.
The main difficulty is keeping the matrix dimensions and derivative conventions aligned across three levels: reaction-rate derivatives, the steady-state concentration map, and linear flux combinations. The steady-state equation is an identity of functions, so its derivative must be obtained from Mathlib's chain and product rules before matrix algebra can be applied. Homogeneity is also only assumed for positive scalars, requiring a local derivative argument at c = 1; replacing it with an unrestricted algebraic scaling axiom would change the theorem. Finally, the connectivity statements require division by concentrations, enzyme rates, and fluxes, so all corresponding nonzero hypotheses are explicit.
The Lean representation uses finite-dimensional real vector spaces encoded as functions on Fin, finite sums, and Mathlib's fderiv and HasFDerivAt. The development is noncomputable but contains no sorry, admit, or axiom, and the complete file compiles under the pinned platform environment. The stoichiometric matrix, rate functions, state map, and flux map remain general; no numerical network or hard-coded special case is used. The left-inverse assumption is retained because it is the structural rank condition needed to derive concentration connectivity, while rate, concentration, parameter, and flux nonzero conditions govern the logarithmic normalizations. Reusable infrastructure includes the derivative-matrix interface, finite-dimensional continuous-linear-map expansion lemmas, steady-state linearization, homogeneous Euler identities, and diagonal inverse calculations.
The Fisher information of a real random variable measures how sharply its density is peaked: it is the information an observation carries about a translation parameter , and by the Cramér–Rao bound its reciprocal is the smallest variance of an unbiased estimator of . The Fisher information inequality (FII) says how this quantity behaves under the addition of independent noise. It was proved by Stam (1959) and Blachman (1965) as the key step in their proof of Shannon's entropy power inequality, and it remains a standard tool in information theory, in the information-theoretic proofs of the central limit theorem, and in statistical physics.
Liu and Viswanath (arXiv:cs/0604028) give two new proofs of the FII from data processing inequalities: one for mutual information (§2.1) and one for conditional variance (§2.2). This mission formalizes the inequality and the steps of the second, Bayesian estimation, proof.
Timeline.
Let be a real random variable whose law has a density that is absolutely continuous, with derivative . The score of is , and the Fisher information is
It depends on the law of only. If the law has no absolutely continuous density, . In Lean: IsACDensity μ f g (a density f of μ with derivative g), fisherInfo μ, and score μ, applied to the law P.map X.
For a real random variable and an observation , the conditional variance (minimum mean-square error) is the number
in Lean mmse P W X. Random variables form a Markov chain when and are conditionally independent given (IsMarkovChain).
The proof works with the Bayesian estimation model (22): for and ,
with standard Gaussian and mutually independent.
For independent real random variables with densities and all ,
No finiteness of , is assumed.
The FII gives the canonical form (choose , ), and through de Bruijn's identity it integrates to the entropy power inequality, which bounds the capacity of additive-noise channels and of Gaussian broadcast and wiretap channels. Lemma 1 is of independent use: it expresses the Fisher information of a Gaussian-perturbed variable through an estimation error, the link behind the I-MMSE identities.
The result has been proved since 1959; this mission produces a machine-checked proof. To the best of the curators' knowledge, neither Mathlib nor this platform has the classical Fisher information of a real law, the score of a sum, or the MMSE identities; they are formalized here for the first time. The equality case of the canonical form ("if and only if both are Gaussian") is not part of the mission: the paper states that its proofs do not give it.
Each step in the paper is a line, but each rests on analytic facts the text takes for granted. Eq. (6) requires differentiating the convolution density of under the integral sign with only an integrable score. Lemma 1 needs the Gaussian score and the orthogonality of the estimation error, which holds in while need not even be integrable (the conditional mean is that of the conditional law of given , which has Gaussian tails). The final step needs the limit , which is a lower-semicontinuity statement for Fisher information under weak convergence, including the case ; the inequality alone gives only half of it.
The naive reading of the paper's independence assumption fails: under pairwise independence of , eq. (28) is false (a counterexample is recorded on the milestone). The proof needs mutual independence, which it may assume since it chooses itself.
Random variables are measurable maps on a probability space (Ω, P); of a random variable is fisherInfo (P.map X), valued in ℝ≥0∞, and the coefficients are ENNReal.ofReal of the real squares, so . The Gaussian law is Mathlib's gaussianReal 0 v, with the variance. In (6) the conditional expectation is Mathlib's condExp on the -algebra generated by . In mmse the conditional mean is the mean of the regular conditional law condDistrib W X P, as in the paper's ; it agrees with condExp for integrable and needs no integrability, so no statement about mmse assumes any. VAR is the expected conditional variance (a number), not Mathlib's condVar (a random variable).
The definition of cannot be trivialized: the mission's sanity checks prove , , and that every absolutely continuous representation of a density gives the same value. A finiteness hypothesis on in the goal would make it a special case and is ruled out.
Reusable beyond this mission: the definitions of Fisher information and score of a real law, the MMSE, and the elementary Markov-chain predicate; the score-of-a-sum identity (6) and the Gaussian-smoothing limit are standard lemmas of information theory. Contributions are welcome on each milestone and on supporting lemmas (convolution densities, the Gaussian score, the orthogonality principle for conditional laws).
Tensor networks represent the state of a many-body quantum system on sites as a contraction of small tensors, one per vertex of a graph. They underlie the matrix product state, PEPS and MERA methods of condensed-matter physics and quantum chemistry. Many physical systems have a global symmetry: a group acting by the same unitary on every site, under which the state is invariant, . Particle-number conservation () and spin isotropy () are the standard examples.
Singh, Pfeifer and Vidal (arXiv:0907.2994) observe that such a state can be written with symmetric tensors, each invariant under the simultaneous action of on its indices, and they describe the structure of these tensors. Every symmetric tensor splits into degeneracy tensors, which carry all the free parameters, and structural tensors, which depend only on the group. This is the basis of symmetry-exploiting numerical codes for and (arXiv:1008.4774), and it identifies the symmetric part of a tensor network with a spin network, the object used in loop quantum gravity (Rovelli–Smolin 1995).
Fix a group and a catalogue of irreps: a set of charges and, for each, an irreducible unitary matrix representation on , with distinct charges labelling inequivalent irreps. The charge is the trivial irrep, , .
Fusion data decomposes tensor products, Eq. (9): . For each pair there is a finite set of channels with output charge and an isometry , the Clebsch–Gordan coefficients, which intertwines with . The isometries are orthonormal and complete. Conjugation data gives, for each , a charge and a unitary with .
A tensor has a finite set of legs, each outgoing or incoming. The index of a leg is , where is a charge, labels a basis vector of a finite degeneracy space and labels a basis vector of (Eq. (4)). The group acts on an outgoing leg by (Eq. (5)) and on an incoming leg by its complex conjugate. is symmetric when it is invariant under the simultaneous action on all legs, as in Eq. (7).
A fusion tree for a root leg is a binary tree whose leaves are the other legs, each exactly once. Fix leg charges . A labelling assigns a channel to every inner node, and so an intermediate charge to every inner branch; it is admissible when the tree fuses into the root's charge. The structural tensor composes the isometries along the tree. It is defined from the fusion data alone: the paper's for two legs, for three legs, and for four legs.
For every valid tree and all degeneracy spaces, the map from unconstrained degeneracy families to tensors
is a bijection onto the symmetric tensors. For two trees with the same root, there are unitary matrices , fixed by the symmetry before any tensor is chosen, with
These are the paper's three claims: holds all the degrees of freedom, is determined by the symmetry, and a change of tree is an F-move.
The decomposition lets a numerical code store only the degeneracy tensors. Contractions then become blockwise products, and quantum numbers are preserved exactly during approximate simulation. The paper reports 5 and 35 times fewer parameters for and MERA (p.4). The statement also shows that, for fixed charges, a symmetric tensor network is a linear superposition of spin networks, with the degeneracy tensors as coefficients.
The paper gives no proofs: it cites Schur's lemma and the Wigner–Eckart theorem. None of this is formalized on the platform. A related open item, NonAbelianDMNRG.Recursion.eq_43, poses the two-leg case (Eqs. (6), (8)). Other platform results cover a tensor-product decomposition up to linear (not unitary) equivalence and a Wigner–Eckart factorization for polynomial irreps of . The mission adds fusion trees, labellings by intermediate charges, recoupling unitaries, and a general uniqueness statement for every number of legs and every choice of directions.
For fixed charges, a block of is an invariant vector in a tensor product of irreps and conjugate irreps, and such vectors correspond to intertwiners from one irrep into a tensor product of irreps. The main step is to show, by induction over an arbitrary tree, that the composed Clebsch–Gordan isometries form an orthonormal family that exhausts this space. Schur's lemma then gives uniqueness. Leg order is arbitrary, so the trees are not planar, and the two trees in the change-of-tree clause need not differ by a single move. The direct route, which composes elementary F-moves of Eq. (13), does not apply. Unitarity of instead follows because both families of structural tensors are orthogonal with the same norm, and this holds only for a common root. Carrying the leg directions through the conjugation unitaries , and the dependent index types , adds a second layer of work.
is an arbitrary Group with no topology. Compactness is used only for complete reducibility, which unitarity provides, so compact groups with their continuous irreps are an instance. Irreps are unitary matrix representations G →* Matrix.unitaryGroup (Fin (dim a)) ℂ. The catalogue may be infinite and is part of the data, with irreducibility and pairwise inequivalence as fields. Multiplicity freeness is not assumed: channels play the role of the paper's pairs (footnote [10]). The leg index is encoded as a finite set of degeneracy labels , each carrying a charge, together with . Degeneracy spaces may be empty.
The intermediate index of Eqs. (11), (12), (15) is contracted inside . No intermediate degeneracy index is attached to : the paper itself writes without , and Fig. 2(iv) shows the inner edge only in the structural part.
A trivializing reading is excluded: is a definition computed from the fusion data before the degeneracy spaces and are introduced, is unconstrained, and is quantified before any tensor. A proved instance shows that the hypotheses can be met with a nonzero symmetric tensor.
Useful infrastructure beyond this mission: Schur's lemma for unitary matrix representations of an arbitrary group, unitary complete reducibility, and the orthonormality and completeness of composed isometries over trees. Contributions to these lemmas are welcome, as are proofs of the milestones in any order.
General relativity has a dynamical causal structure: whether one event can influence another depends on the metric, which is itself a physical variable. Quantum theory, in its standard formulations, presupposes a fixed causal structure: states evolve in a given time, and systems are composed in a given order. A theory of quantum gravity is expected to combine the indefiniteness of quantum theory with the dynamical causal structure of general relativity. L. Hardy's paper Towards Quantum Gravity: A Framework for Probabilistic Theories with Non-Fixed Causal Structure (2006) proposes an operational framework for probabilistic theories in which no causal structure is given in advance, and in which the question "is this probability determined?" is answered by the theory instead of by reference to a background spacetime.
In ordinary physics one knows that a probability is well defined by appeal to causal structure: given the boundary conditions in the past light cone of a region and the settings chosen there, the probabilities in the region are fixed. The paper replaces that appeal by a single mathematical object, the causaloid, from which every well-defined conditional probability between two regions can be decided and computed. This mission formalizes that claim, the conclusion of §4.5.
An experiment is described by a set of locations . At each location there is a set of settings and, for each setting , a set of possible outcomes under . A label at is a pair . A finite set determines a region , and a label of is a family of labels . An experiment model gives, for every choice of settings at all locations and every outcome family under , a probability , with for every .
For a region , what happens outside it (its settings and outcomes) is a generalised preparation , and is the probability of the label in together with outside. A finite set of labels of is sufficient if every is one fixed linear combination of the , :
It is fiducial if no proper subset is sufficient. The vectors of the elementary regions form matrices ; for a composite region with fiducial set , the vectors of the labels in form matrices . The causaloid is this list of matrices, eq. (30), and from it the causaloid product computes
For disjoint regions , a label of and a label of , put
with over all outcomes under . The conditional probability is well defined if the ratio of to takes one value under every preparation for which the denominator is nonzero.
For every model and every choice of elementary fiducial sets, a causaloid exists, and for every causaloid of the model and every pair of disjoint regions:
every value satisfies (37), and if then . The statement also records that the joint probability and the probability of the conditioning event are and , that the sums over converge, and that exactly when the conditioning event is impossible under every preparation.
In proof order: existence of a finite sufficient set and of a fiducial subset (§4.2, (13)–(15)); a fiducial set has linearly independent states (§4.2, p.12); the expansion (22) of over ; a fiducial set (21); the composite vector (24); the causaloid product (25)–(27); the existence of a causaloid for every region (28)–(30); and the three clauses of §4.5, (35), (36), (37).
Correction. As printed, (35) names the ratio . Since its denominator sums over the outcomes of region 2, the ratio is , the probability (7) that §3 sets out to find. With one setting at each of two locations, binary outcomes and , , , , one has , while the printed ratio is . The mission states the corrected form; (36) and (37) are unchanged. The paper has no numbered theorems; results are cited by section and equation.
The result is the operational content of the framework: the causaloid alone answers both questions the paper sets for a physical theory (p.9), whether a probability is well defined and what it is, and it does so for any pair of regions with no causal order on the locations. The paper's later sections use this to treat quantum theory as a particular causaloid (§5) and to propose the framework as a setting for quantum gravity (§6–§7); those parts are outside this mission.
The claim is proved in the paper by a short linear-algebra argument; no machine-checked version exists. Formalizing it fixes what "well defined", "just sufficient" and "the causaloid" mean precisely, exposes the misprinted conditional in (35), and checks the argument in the generality the paper allows: arbitrary sets of locations, settings and outcomes, with no finiteness beyond that of the fiducial sets.
Each step is elementary; the work is in the quantifiers. Passing from "just sufficient" to "spanning states" requires the states to range over every generalised preparation, including the labels of the other region, and fails if the vector is allowed to depend on the preparation. The vector is an infinite sum when region 2 has infinitely many outcomes; its convergence follows only by expressing through a basis of states. The direction "parallel ⇒ well defined" is immediate, but "well defined ⇒ parallel" needs the identity also at preparations where the denominator vanishes, and that holds only because probabilities are nonnegative: for a signed array the equivalence fails.
Locations are an arbitrary type with decidable equality; settings and outcomes are arbitrary types, labels are dependent pairs, and normalization is HasSum. A region is a Finset of locations. A generalised preparation is a total label whose values on the region are ignored. Fiducial sets are finite, and "just sufficient" means inclusion-minimal. The causaloid is the structure of matrices (30), with no reference to any model; a separate predicate says it is a causaloid of a given model. Well-definedness is a statement about ratios of actual probabilities over the preparations with nonzero denominator, never "" by definition, which would make (36) empty. Lengths are Euclidean.
No product form of the probabilities and no causal order on the locations is assumed anywhere. The development needs finite-dimensional linear algebra, unconditional sums in , and finite products over Finsets; the definitions of sufficient and fiducial sets are stated for an arbitrary real table and are reusable for other operational frameworks. Proofs of the milestones, and alternative arguments for (21) and (24), are welcome.
An extension of a Lie algebra by a Lie algebra is a Lie algebra containing as an ideal with quotient . Extensions are how larger Lie algebras are assembled from smaller ones: central extensions produce the Virasoro and affine Kac–Moody algebras from vector fields on the circle and loop algebras, semidirect products build the Lie algebras of symmetry groups of physical systems, and every finite-dimensional Lie algebra is an extension of a semisimple one by its radical.
When the kernel is abelian, extensions with a fixed -module structure on are classified by the second Lie algebra cohomology . For a non-abelian kernel, no longer acts on — only on modulo inner derivations — and the classification needs non-abelian data. In infinite-dimensional Lie theory (Lie algebras of vector fields, current algebras, Banach–Lie algebras of operators) the extension must moreover respect a topology, so that it can be integrated to an extension of infinite-dimensional Lie groups.
Timeline (as surveyed in Neeb, pp. 1–2):
Throughout, is a topological field of characteristic (the discrete topology is allowed), topological vector spaces are Hausdorff, and a topological Lie algebra is a Lie algebra with a vector-space topology for which the bracket is continuous.
A topologically split extension of by is a short exact sequence of continuous Lie homomorphisms with a continuous linear section of such that is a homeomorphism . Two extensions are equivalent if a continuous Lie homomorphism between the middle terms is the identity on and commutes with the projections to . denotes the set of equivalence classes.
Continuous -cochains are continuous alternating -linear maps ; is the space of continuous linear maps. For a linear map with continuous, the curvature is and the covariant differential is the Chevalley–Eilenberg formula with in place of a module action.
A pair with is a continuous factor system if and ; the set of these is . Each one defines the twisted product , the space with the bracket
The group acts on factor systems by the gauge action , where . An admitting some with is a continuous outer action; if , and the class is a continuous -kernel. collects the extensions whose outer action lies in . Finally makes the centre a -module by , with cocycles , coboundaries and cohomology ; and .
and for every continuous outer action the map , , is onto with fibres the cosets of in the affine space over . Hence
The Lean goal states this without quotient types: is gauge invariant, every extension is equivalent to a twisted product, and two twisted products are equivalent exactly when their factor systems lie in one -orbit; for fixed , surjectivity, the coset description of the fibres, the affine structure of , and the simply transitive action of through a base point (Corollary II.8).
The theorem reduces the classification of non-abelian extensions to two problems: which continuous -kernels occur, and, for each, the cohomology of with coefficients in the centre of . The first problem is answered in the same paper by the obstruction class (Theorem IV.4), whose definition rests on Lemma I.9. For an abelian kernel the result recovers the classical bijection ; for centreless it shows that an extension is determined by its outer action. The topological version is the infinitesimal input for integrating extensions of infinite-dimensional Lie groups.
The algebraic case (discrete topologies) is classical; the topological statement is the paper's. Neither is machine-checked: Mathlib has Lie algebra extensions and low-degree Chevalley–Eilenberg cochains for genuine modules, but no outer actions, no factor systems for non-abelian kernels and no topological Lie algebras. The mission produces these objects together with a checked proof of the classification; the algebraic Mori–Hochschild theorem is the special case of discrete topologies.
The obvious approach transfers the abelian proof. It fails because is not a representation: in general, so the cochains do not form a complex, and the gauge action is affine with the quadratic term . The needed identities — the curvature formula, invariance of , and taking central values — hold only under and require careful bookkeeping of signs and of the factor . A second difficulty is topological: every map produced (the factor system of an extension, the equivalences, the cochain extracted from an equivalence) must be shown continuous, which is where the splitting hypothesis enters, since need not be topologically isomorphic to without it.
All objects live in the namespace NeebLieExt. carries [Field K] [TopologicalSpace K] [IsTopologicalDivisionRing K] [CharZero K]; , and extension middle terms are Lie algebras with [IsTopologicalAddGroup] [ContinuousSMul K], the class IsTopLieAlgebra (continuous bracket), and [T2Space] for , ; ranges over an arbitrary universe. Cochains are plain functions with predicates IsCochain2, IsCochain3 (multilinear, alternating, jointly continuous); is a linear map into Mathlib's LieDerivation K n n with jointly continuous evaluation; is written out in degrees 1–3 (dS1, dS2, dS3). The twisted bracket is the function twistedBracket S ω on n × g — Mathlib's bracket on n × g is the direct product and is never used for twisted products. and are not quotient types: the goal states surjectivity and the exact description of the fibres. The paper's hypothesis is dropped, since every clause holds without it. Lemma II.5 prints the map as ; the formalization uses , as the proof does.
A trivializing reading is excluded: equivalences must fix and the -coordinate, and uses -valued ; without either, the fibre statements would be false.
Contributions are welcome on the gauge-action identities (Lemma I.9), the construction of the factor system of a split extension (Lemma II.4), and the isomorphism criterion (Lemma II.5); a reusable library of continuous cochains, outer actions and twisted products would serve the obstruction theory of §IV and the Lie group version.
A decoherence-free subspace (DFS) is a subspace of a quantum register on which a given noise process acts trivially, so that information stored there is protected without active error correction. Weak collective decoherence is the simplest noise with such subspaces: every qubit couples to the environment through the same operator, which after a fixed single-qubit rotation is the collective operator (Zanardi and Rasetti 1997; Lidar, Chuang and Whaley 1998). It models closely spaced qubits subject to a common fluctuating field, for instance ions in a trap.
Storage alone is not computation. To use a DFS, one needs Hamiltonians that never leave it and that enact every unitary on it. Chapter 9 and Appendix B of Bacon's thesis (arXiv:quant-ph/0305025v1), following Kempe, Bacon, DiVincenzo and Whaley (arXiv:quant-ph/0004064; arXiv:quant-ph/0112013), show that a short list of nearest-neighbour two-qubit Hamiltonians suffices, and that it acts on each DFS separately.
Take qubits with computational basis , . The collective operator is diagonal, , where is the Hamming weight (the number of ones) of . Its eigenspaces are the decoherence-free subspaces
with orthogonal projectors . Appendix B labels the same subspaces by .
The two-qubit Hamiltonians that commute with are exactly the matrices
in the basis . From them the thesis picks the exchange interaction (the swap of two qubits) and the diagonal operators , , , and forms the nearest-neighbour set
The Lie algebra generated by is the closure of under real scalar multiplication, addition and the commutator . In the Lean development it is written , with bracket ; a Hamiltonian is generated exactly when .
For every , every and every -qubit matrix ,
So contains acting on and annihilating every other DFS ("independence"). Theorem 9.2.1 also displays the equality . That equality is false: for , lies in and acts nontrivially on the one-dimensional , where . The goal is the containment, which both theorems state in words and Appendix B proves.
Exponentiating gives every special unitary on each separately, with the identity on all other DFSs. Encoded universal computation on weak collective DFSs therefore needs only nearest-neighbour interactions that never leave the protected subspaces. Chapter 10 applies this to ion traps. The same inductive scheme, with Lemmas from Appendix D, handles strong collective decoherence and the exchange interaction alone (Theorem C.2.1, the companion mission IX of this series).
The result is published and proved on paper. This mission formalizes it; no machine-checked proof of it is known. The work also corrects the overstated equality (9.11), and the base case and commutant characterization are self-contained finite computations.
The generators do not act independently on the DFSs. Every element of acts simultaneously on all the DFSs it preserves, and the obvious inductive step falls short. Lifting from to qubits gives operators that act at once on the daughter subspaces of and . These are the paths through the lattice of partial weights in Appendix B. The proof must first separate these simultaneous actions (the "independence step"), and then glue on two overlapping subspaces into on their span. That needs a quantitative supply of elements of , not just closure arguments, and it must work for every and every weight , including the one-dimensional DFSs at and .
Lean represents the register by the index type Fin n → Fin 2, and operators by Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ. Qubits are numbered ; the book numbers them . Two-qubit matrices are indexed by Fin 2 × Fin 2 with the first qubit first, and they are placed on qubits by tensoring with the identity elsewhere. is LieSubalgebra.lieSpan ℝ of , with the matrix commutator (LieRing.ofAssociativeRing, a local instance). It allows real scalars only and has no generator, and is exactly the nearest-neighbour set (9.10). Adding all pairs or single-qubit terms would weaken the theorem. The support hypothesis is what makes the statement about one DFS at a time, so dropping it, or replacing the containment by the false equality, changes the theorem.
A complete development needs the following: the commutant computation (milestone 1), the two-qubit base case (milestone 2), the independence step, and a lemma that combines on two non-orthogonal subspaces. The last of these is the Enlarging and Mixing Lemmas of Appendix D, posed in mission IX. The block-matrix and Lie-span infrastructure is reusable for other symmetry-restricted universality results. Contributions to any of these are welcome.
A decoherence-free (DF) subspace is a subspace of a quantum system's state space on which the coupling to the environment acts trivially, so that quantum information stored there is not degraded. D. Bacon's thesis develops the theory in finite dimension: by its Theorem 5.3.1 a subspace is decoherence-free exactly when every system operator in the system–environment coupling acts on it as a scalar (arXiv:quant-ph/0305025, §5.3, p.72). DF subspaces were proposed for collective noise on several qubits (Zanardi–Rasetti 1997, Lidar–Chuang–Whaley 1998), where a symmetry of the coupling produces the degeneracy the criterion needs.
Chapter 12 of the thesis asks whether such protection can exist inside a single atom coupled to the free electromagnetic field. Lemma 12.1.1 gives a negative answer in the generic case: if the atom's levels have distinct energies and no level is completely isolated from the others, there is no DF subspace at all. A DF subspace in an atom therefore requires a degeneracy of the energy spectrum, and the thesis continues (§12.2) with coherent population trapping in a Λ-system as an example of what survives in a semiclassical setting.
The atom has levels , an orthonormal basis of , with real energies and system Hamiltonian
The spectrum is non-degenerate when the are pairwise distinct. The atom couples to field modes through operators with complex coupling coefficients () (eqs. (12.1)–(12.2)). The thesis shows that the OSR algebra of this coupling is generated by
(sumSigma g and sumSigma (star g) in Lean). The transition matrix of (12.4) has for , and for (Gmat); means the field drives a transition between levels and .
A Hamiltonian preserves a subspace (Definition 5.3.2, PreservesSubspace) if some spectral decomposition has every eigenvector either in or orthogonal to . A DF subspace in the strict sense (IsDFSubspace g ω S) is a nonzero subspace such that, for constants , every satisfies
and preserves , so that states of evolve unitarily inside .
If is injective and for every there is with , then
The statement holds for every number of levels and every coupling with the stated transition property; no particular atom is fixed.
, and if a nonzero satisfies both conditions of (12.3) then and . The thesis also remarks that the two conditions are "really one condition"; that converse fails for complex , and the milestone states the implication (the counterexample is in the item).
If is injective and preserves , then is the span of the levels that it contains.
The lemma is a no-go statement: for an atom with a generic spectrum and no isolated level, no choice of encoding in the atom's levels avoids decoherence from the free field. Its proof also gives the positive converse the thesis draws afterwards: a DF subspace of a multilevel atom can only have support on degenerate levels. This is the reason the later chapters look for protection in symmetric multi-particle couplings and in engineered degeneracies rather than in single atoms.
The result is proved in the thesis in a few lines; it has not been machine-checked. Formalizing it pins down two points the text leaves informal: the meaning of "preserves a subspace" for a Hamiltonian whose spectral decomposition is chosen, and the exact relation between the two conditions (12.3) and the single eigen-condition (12.4), whose printed equivalence holds only in one direction.
The mathematical content is short; the work lies in the definitions. The first idea is to treat (12.4) as the DF condition and argue from the spectrum of alone. That is not enough: is symmetric but not Hermitian, a complex symmetric may have eigenvectors that are not eigenvectors of , and the eigenvalues of say nothing about . What excludes DF subspaces is the second requirement, preservation by , which the eigen-condition alone does not see. Proving the uniqueness of the eigenbasis from Definition 5.3.2 as stated (an existential over orthonormal bases with real eigenvalues) is the main formal step.
The Hilbert space is Fin N → ℂ with levels as standard basis vectors (0-based in Lean, 1-based in the thesis) and inner product . Operators are Matrix (Fin N) (Fin N) ℂ; is Matrix.diagonal of the real energies, and non-degeneracy is Function.Injective ω. Coupling coefficients are a function g : Fin N → Fin N → ℂ of which only the entries with are used. The quantized field of (12.1) is not modelled: the DF condition is (12.3), which the thesis derives from that coupling through Theorem 5.3.1. In Definition 5.3.2, "entirely outside of " is read as orthogonal to ; the reading "not in " would make every Hamiltonian preserve every subspace.
The zero subspace satisfies every condition vacuously, so a DF subspace is required to be nonzero. For the transition hypothesis cannot hold and for the statement is vacuous; this is the thesis's situation, not a trivialization. Proved sanity checks (not uploaded) confirm that both hypotheses are needed: an isolated level with distinct energies, and a degenerate pair of levels coupled with , each carry a DF subspace, and the Λ-system of §12.2 satisfies the transition hypothesis.
Needed infrastructure: matrix units and mulVec computations, orthonormal families in Fin N → ℂ, and the eigenvectors of a diagonal matrix with distinct entries. The last is reusable beyond this mission. Proofs of the two milestones and of the goal are welcome, as are alternative formulations of Definition 5.3.2 through Module.End.HasEigenvector together with their equivalence.
A quantum computer is built from a fixed, usually finite, repertoire of gates: unitary operations that the hardware can apply to one or two of its physical subsystems. Whether such a repertoire is universal, meaning that sequences of its gates approximate every unitary evolution of the whole register, decides whether the hardware can run arbitrary quantum algorithms at all. This mission formalizes the tool that Chapter 4 of D. M. Bacon's thesis (Decoherence, Control, and Symmetry in Quantum Computers, arXiv:quant-ph/0305025v1, §4.3.1, p.52) introduces for universality proofs: universality of a gate set on a many-body register follows from universality on the pairs of subsystems along a connected graph.
The question has a short history. Deutsch (1989) exhibited the first universal gate set, built from three-qubit gates (doi:10.1098/rspa.1989.0099). DiVincenzo (1995) showed that two-qubit gates suffice (doi:10.1103/PhysRevA.51.1015). Barenco et al. (1995) proved universality of the controlled-not together with all single-qubit gates (doi:10.1103/PhysRevA.52.3457), and Deutsch–Barenco–Ekert and Lloyd (1995) showed that almost every two-qubit gate is universal when qubits can be permuted (doi:10.1098/rspa.1995.0065, doi:10.1103/PhysRevLett.75.346). Lemma 4.3.1, the subspace-merging step, is cited in the thesis from Aharonov and Ben-Or (arXiv:quant-ph/9906129).
A register consists of subsystems of dimensions ; its Hilbert space is the tensor product
A gate set is a set of unitary operators on . The set densely generated by , written (Lean: denseGen G), is the closure of the set of all finite products of gates; a set of operators is densely generated when , i.e. each element of is approximated to every accuracy by sequences of gates (the book's Definition 4.3.1).
For a subspace , (Lean: SUOn W) is the set of special unitaries on that fix the orthogonal complement pointwise: " acting on ".
For distinct subsystems and an operator on , (Lean: embedPair d a b V) acts as on factors and as the identity on the others. Subsystems are computationally connected for (Lean: CompConnected) when every with is densely generated by . The graph of computationally connected subsystems (Lean: compGraph d G) has the subsystems as vertices and the computationally connected pairs as edges.
For every , every dimension vector with all , and every gate set :
The conclusion is containment, not equality, because gates may carry global phases. The two hypotheses and are corrections of the printed lemma, which states neither and is false without them (see Formalization scope).
If and densely generate and , then
with equality when and densely generate nothing beyond and .
The lemma turns a global question (does a gate set approximate all of , a group whose dimension grows exponentially in ?) into finitely many local ones: universality on individual pairs of subsystems, plus connectivity of a graph. Two-qubit universality of a controlled-not with single-qubit gates (§4.3.2), nearest-neighbour architectures, and qudit registers of mixed dimensions all reduce to it. Lemma 4.3.1 is used again whenever control on overlapping subspaces must be combined, for instance in encoded universality over decoherence-free subspaces.
Both lemmas are classical results with informal proofs: the thesis says only "Proof: See [4]" for Lemma 4.3.1 and "Follows simply from induction using Lemma 4.3.1" for Lemma 4.3.2. Neither has a machine-checked proof on the platform. The related platform results SuperconductingQC.closure_singleQubit_iSWAP_eq_top and SuperconductingQC.closure_twoLevelUnitaries_eq_top concern exact generation by specific qubit gate sets, not dense generation from a connectivity graph over arbitrary dimensions. A formal proof would also pin down the hypotheses the printed statement omits.
Both conclusions are statements about closed subgroups of the compact group . The naive argument, that products of elements of and obviously fill , does not work at the level of explicit products: no short factorization of a general element of into such pieces is available, the overlap may be a single line, and the hypothesis gives only dense, not exact, generation. Some passage from group-level information to infinitesimal information about the closed group and back is required, and that infrastructure (closed subgroups of matrix groups and their Lie algebras) is thin in Mathlib.
The induction behind Lemma 4.3.2 is not a direct application of Lemma 4.3.1 either: Lemma 4.3.1 speaks of subspaces, Lemma 4.3.2 of tensor factors, and the translation between them breaks down when a factor has dimension . The printed lemma's "follows simply from induction" hides exactly the cases that make the uncorrected statement false.
Hilbert spaces are ι → ℂ with Fintype ι; operators are Matrix ι ι ℂ with the entrywise topology; gates are elements of Matrix.unitaryGroup ι ℂ. The register's basis is indexed by (i : Fin n) → Fin (d i); subsystems are numbered from . denseGen G is the closure of the image of Submonoid.closure G. Subspaces for Lemma 4.3.1 live in EuclideanSpace ℂ ι, so orthogonal complements are those of the standard inner product. "Not disjoint" means nonzero intersection, and "the union " means the span.
The printed Lemma 4.3.2 writes the subsystem structure as ; the formalization reads it as , which the statement itself requires. Two corrections are made: (for the one-vertex graph is connected with no edges, and gives only ), and (for the gates and connect the path –– but generate only ). Computational connectedness asks only that be densely generated by all of , which the book's condition implies, so the formal lemma is at least as strong as the book's.
The trivializing readings are ruled out: the closure is taken (exact generation by a finite set is false), SUOn ⊥ = {I} and denseGen ∅ = {I}, and the hypothesis of the goal is satisfiable (two qubits with all unitaries).
A complete development needs: the closed-subgroup theorem for matrix groups (or an elementary substitute for compact subgroups of ), the Lie algebra and its generation by on overlapping subspaces, and the reindexing of tensor factors. The subspace-merging lemma and the treatment of denseGen are reusable for every other universality statement in this series (Missions VIII and IX state Lie-algebraic universality on decoherence-free subspaces). Contributions of intermediate lemmas, for instance that denseGen G is a closed subgroup or that embedPair of a unitary is unitary, are welcome as proof sketches.
In a housing market, introduced by Shapley and Scarf (J. Math. Econ. 1974), every agent owns one indivisible good and the agents reallocate the goods among themselves. The model underlies kidney exchange programmes, where a patient–donor pair "owns" its donor and pairs exchange donors along cycles (Roth, Sönmez, Ünver, QJE 2004). A natural design requirement is that a pair should never be hurt by bringing a better donor: if other agents come to value an agent's good more, that agent should not end up worse off. Biró, Klijn, Klimentova and Viana (arXiv:2102.00167) called this respecting improvement and established it for the strict core under strict preferences. Schlotter, Biró and Fleiner (arXiv:2110.06875) settle it for the core when preferences are arbitrary partial orders, and show that a witnessing allocation can be computed in linear time. This mission formalizes that result, Theorem 2 of the paper.
Timeline. 1974: Shapley and Scarf show that the core of a housing market with strict preferences is nonempty, via Gale's Top Trading Cycles (TTC). 1977: Roth and Postlewaite show that the strict core is then a single allocation. 2004: Abraham, Cechlárová, Manlove and Mehlhorn give a linear-time TTC for strict preferences. 2021: Biró et al. prove respecting improvement for the strict core under strict preferences. 2024 (arXiv v3; Math. Oper. Res. 2025): Schlotter, Biró and Fleiner prove it for the core under partial orders, with an algorithm.
A housing market has a finite set of agents; each agent ranks the houses by an irreflexive partial order , where means that prefers the house of to the house of (in Lean, H.lt c a b). Agent finds the house of acceptable if . An allocation is a permutation of giving every agent an acceptable house. An arc is -augmenting if , and is in the core if the -augmenting arcs contain no cycle: no group of agents can trade among themselves so that each strictly gains.
Fix an agent . A market on the same agents is a -improvement of if only agent changes its preferences, and it does so by raising 's house: (i) the order among houses other than 's is unchanged, (ii) a house below stays below , and (iii) no house moves above . A -improvement is the result of a sequence of -improvements.
The size of a market is the length of its description: each is given by its Hasse diagram on the acceptable houses, and , counting vertices and arcs (Appendix A, p.30).
For every core allocation of and every -improvement of there is a core allocation of with
and there is a constant such that the program hmImproveProg (Algorithm HM-Improve) computes such an from the Hasse diagrams of and and in at most unit operations.
The proof runs through algorithm HM-Improve. Each agent that now envies is rerouted through a new agent on the arc , giving a market ; becomes a sub-allocation with sources and sinks; sources move along envy arcs or are declared irrelevant; finally TTC reallocates the irrelevant agents. The milestones are: TTC returns a core allocation (Appendix A); the improving agents may be taken distinct (p.11); new augmenting arcs enter (p.12); the initial sub-allocation (p.12); the iteration keeps a sub-allocation (p.12); Lemma 1 (stability); Proposition 2 (monotonicity); Lemma 2; the Claim of Lemma 3; Lemma 3 (the output is in the core); is never irrelevant (p.19); TTC runs in (p.30); Lemma 4 ( time).
Theorem 2 gives Corollary 1: the core of housing markets strongly satisfies the RI-best property, so an agent can only gain, in its best attainable core outcome, from making its good more attractive. Proposition 1 of the paper shows that the worst attainable core outcome can decrease, so the property is specific to the best house. For kidney exchange with partially ordered preferences over donors, this is an incentive guarantee for recruiting better donors.
The result is proved in the paper but has no machine-checked proof. Formalizing it produces a verified linear-time TTC for partial-order preferences, a verified incremental core-maintenance algorithm, and a corrected definition of improvement. The printed definition (clauses (i) and (ii) only) allows a house incomparable to to move above ; under it Theorem 2 is false. With , ranking above above , ranking above ( unacceptable), and having and incomparable in but above in , the swap is in the core of and every core allocation of gives a worse house. The mission adds clause (iii), which for strict orders follows from (ii), and requires .
The existence part is an invariant argument over all runs of a nondeterministic algorithm, with an output assembled from two pieces. The obvious first idea, to repair only along new augmenting cycles, fails: a cycle in may run through agents that must give up their houses, and their displacement propagates. HM-Improve controls this by keeping the envy graph acyclic while it only deletes arcs and agents, and the Claim of Lemma 3 has a case (an irrelevant whose is still relevant) that its printed proof does not treat.
The time part requires an amortized analysis of a concrete program. Two points are not in the paper. First, can be of order (raising above houses that were above others creates covering pairs), so the program must not read except at . Second, maintaining the envy graph as an agent moves up its preference order needs a peeling procedure on the Hasse diagram, so that each vertex and arc is processed once.
Preferences are IsStrictOrder relations on all of , with no totality. Allocations are permutations with acceptability; the core is acyclicity through Relation.TransGen. IsImprovementAt carries clauses (i)–(iii) and ; IsPImprovement allows sequences of any length. Sub-allocations are partial functions Y : Ñ → Option Ñ on the agents outside ; a -augmenting arc excludes the loop at a sink, which the literal definition would include and which would make every sub-allocation with a sink unstable. The lemmas hold for every set the page allows (from Algorithm 1's up to , which the program uses), and the early exit of Algorithm 1, line 1, is omitted. The algorithm is a transition relation HMStep, and the lemmas quantify over all its runs.
Time is the unit-cost RAM count of the concrete programs ttcProg and hmImproveProg, written in a tick monad in which every array access, comparison, stack operation and loop iteration costs one and an allocation of cells costs ; the constant is quantified before and the instance. A bare existential over Lean functions would make the time clause free, so the program is part of the statement. The input is a Hasse-diagram presentation with vertex, out- and in-neighbour lists (HassePres, Represents), and the bound is in , not .
Reusable beyond this mission: the partial-order housing market layer, the linear-time TTC for partial orders, and the charging discipline. Proofs of any milestone are welcome, in particular the abstract chain (Lemma 1, Proposition 2, Lemmas 2–3), which needs no reasoning about programs.
A mode-locked laser emits a train of pulses whose spectrum is a frequency comb: many optical modes, equally spaced in frequency. The common phase offset of these modes, the carrier-envelope phase, is the quantity that has to be stabilized when femtosecond combs are used to define optical frequency standards (Jones et al., Science 2000; Udem et al., PRL 1999). Its quantum noise sets a floor on that stabilization.
Pfister (2007) describes multimode squeezing in an optical parametric oscillator by graph states: each field mode is a vertex, and each two-mode (or single-mode) squeezing interaction of the Hamiltonian is an edge (or self-loop). The adjacency matrix of the graph is, up to the coupling constant, the matrix of the linear Heisenberg equations of the modes, so the squeezed observables are read off its eigenvectors. For the complete graph without loops (the Hamiltonian of eq. (1), studied in Pfister et al., PRA 2004) this produces continuous-variable GHZ entanglement. Adding a self-loop of the same sign at every vertex gives the Hamiltonian of eq. (4), and the paper's claim is that squeezes exactly one observable: the sum of the phase quadratures of all modes, i.e. the carrier-envelope phase. Physically, is a degenerate OPO pumped by a mode-locked pulse train whose repetition rate matches the cavity's free spectral range (Sec. c), which makes it the easiest of the paper's Hamiltonians to implement. A complementary analysis of the same system, in terms of "supermodes", appeared independently (de Valcárcel, Patera, Treps, Fabre, PRA 2006).
Fix modes. The annihilation operators and creation operators are elements of a complex algebra satisfying the canonical commutation relations
The amplitude and phase quadratures of mode are and . The total amplitude is and the phase sum is .
For a real symmetric matrix (an adjacency matrix with loops on the diagonal), the graph Hamiltonian is , with the nonlinear coupling constant. The Hamiltonian of eq. (4) is
which is for the all-ones matrix .
The Heisenberg generator of is . A Heisenberg evolution generated by is a family of complex-linear maps (), written , with on the mode operators and for . An operator is squeezed when as .
For every Heisenberg evolution generated by , every and every real :
and, for in the complex span of ,
The second pair of clauses is the paper's "the only squeezed operator here is the phase sum", together with the total-amplitude case of Fig. 3 obtained by reversing the sign of the coupling.
The theorem identifies a single collective observable, the carrier-envelope phase of the signal comb, as the squeezed mode of a broadband degenerate OPO pumped by a matched pulse train, with the noise reduction rate enhanced by the number of modes . It also shows what is lost relative to the GHZ Hamiltonian : the amplitude differences, which are GHZ entanglement witnesses, become constants of the motion, so generates squeezing but not GHZ entanglement. The paper then proposes measuring the squeezed phase sum by balanced heterodyne detection (Sec. d, outside this mission).
The result is a short computation in the paper, stated without a framework for the operators or the evolution. The formalization fixes one: it proves the claim for every algebra containing a solution of the canonical commutation relations and every linear Heisenberg-picture evolution, rather than for one Hilbert-space representation, and it makes "only squeezed" a precise iff over quadrature combinations. No part of this paper has a machine-checked proof; the milestone on graph Hamiltonians also contains the Heisenberg equations of the GHZ Hamiltonian , which a later mission can reuse.
The algebra is routine: commutators of quadratic expressions in the mode operators, and the spectrum of the all-ones matrix. The step that needs care is passing from the eigen-equations of the generator to the time evolution. In a Hilbert-space setting one writes , but the mode operators are unbounded, and in a normed algebra the relation has no nonzero solution (Wielandt–Wintner), so the usual Banach-space uniqueness theorem for does not apply. Uniqueness has to come from separating points with continuous linear functionals in a locally convex space. The "only squeezed" clause further requires decomposing an arbitrary quadrature combination along , and the differences, and comparing growth rates of in a Hausdorff space without any norm.
Lean namespace PfisterCEP. The operators live in {A : Type*} [Ring A] [Algebra ℂ A] with [TopologicalSpace A] [IsTopologicalAddGroup A] [ContinuousSMul ℂ A] [ContinuousSMul ℝ A] [T2Space A] [LocallyConvexSpace ℝ A]; the topology is on the additive group only, and multiplication need not be continuous. Modes are indexed by Fin N; is a separate family ad subject to the canonical commutation relations (IsCCR), not star ∘ a. "H.c." is written out. and are real, with ; has no sign restriction except in the "only squeezed" clauses. The evolution τ : ℝ → A →ₗ[ℂ] A is constrained only by IsHeisenbergFlow (initial value and the Heisenberg equation on the mode operators).
The statement cannot be trivialized through its hypotheses: no normed-algebra structure is assumed, the evolution is not defined by an exponential formula, and the Weyl algebra with any Hausdorff locally convex topology on its additive group, together with the exponential of the generator on the span of the modes, satisfies every hypothesis with nonzero operators.
Needed infrastructure: commutator calculus for quadratic polynomials in CCR generators, the eigen-decomposition of the all-ones matrix (Mathlib's Matrix.charpoly_vecMulVec covers the characteristic polynomial), derivatives of curves in topological vector spaces, and Mathlib's SeparatingDual for locally convex Hausdorff spaces. The ODE-uniqueness milestone and the graph-Hamiltonian Heisenberg equations are reusable beyond this mission. Proofs of any milestone, and alternative routes to the goal, are welcome.
A quantum memory stores a qubit in a noisy medium for a long time. The toric code of Kitaev stores it in the ground space of many physical qubits on an torus, so that only errors along a path winding around the torus can change the stored information. Errors are detected by measuring local check operators, the syndrome, and corrected by a classical decoder. In practice the syndrome measurements are themselves faulty, so a decoder has to work from a history of unreliable measurements.
Dennis, Kitaev, Landahl and Preskill, Topological quantum memory (arXiv:quant-ph/0110143, J. Math. Phys. 43 (2002)), study this setting. Most of the paper is a physical argument that maps decoding to a random-bond Ising model and a three-dimensional gauge theory, with numerical estimates of the critical error rate. Section V is the part the paper calls "a rigorous bound" (p. 18): a Peierls-type argument showing that minimum-weight decoding succeeds with probability tending to 1 as whenever the qubit error rate and the measurement error rate are below . The introduction states this as the paper's guarantee (p. 2). The surface-code and toric-code threshold literature that followed builds on this bound and on the decoding problem it defines.
Bit-flip errors and their syndromes are recovered separately from phase errors and theirs, and the two problems are identical (p. 11), so one of them suffices. The syndrome history lives on a spacetime lattice: sites with and . A link joins to . Links in the and directions are horizontal: an error there is a qubit flip between two measurement rounds. Links in the direction are vertical: an error there is a faulty syndrome bit. Each horizontal link is in error with probability , each vertical link with probability , all independently. The lattice has sites, horizontal links and vertical links (p. 20).
A chain is a set of links, added by symmetric difference. Its boundary is the set of sites met by an odd number of its link endpoints. The error history is a chain drawn with probability if , else , eq. (44). Only is observed. A maximum-likelihood decoder returns a chain with the same boundary and maximal probability; for this is the minimal-weight chain of eq. (46).
Recovery fails when contains a cycle that winds an odd number of times around the spatial torus in the or the direction. is the probability of this event. Write , , and let be the connective constant of , where counts -step self-avoiding walks.
There are and such that, for all , all with
and every maximum-likelihood decoder,
Consequently storage is reliable under (60): if grows at most polynomially in , the failure probability tends to uniformly over decoders. The same holds under (63) and under (64).
The paper's chain of displays: (49) and (50) for a cycle in ; (52), the bound for one cycle; the topological facts that a spatially winding cycle contains a winding self-avoiding polygon with at least horizontal links; the union bound (54); the failure bound (55); the polygon count (58) in and its use on the torus; (59); the termwise bound (61); and , which makes (63) and (64) consequences of (60).
The bound shows that the toric code has a positive accuracy threshold for storage even when every syndrome bit is unreliable, and that below it the failure probability decays exponentially in , the square root of the block size. It also shows that minimum-weight matching, an efficiently computable decoder, achieves a threshold. Later fault-tolerance thresholds for topological codes use the same Peierls-type counting.
The paper proves the bound with explicit constants only up to quoted counting results. A formalization makes the model exact: the periodic spacetime lattice, the failure event, the decoder with arbitrary tie-breaking, and at the ends of . Two printed details need correction: (62) is stated with a strict inequality, which fails at , where both sides are zero, and (52) is asserted for open paths as well, which fails for some tie-breaking rules. The mission states the corrected forms.
The probabilistic part, (49) to (55), is elementary. It needs a swap argument against the decoder's optimality, a union bound over polygons, and the topology of cycles on a 3-torus with multiple edges at small or . The difficulty is counting. The bound (59) needs the number of self-avoiding polygons on the torus with links to be at most a polynomial in times , uniformly in and . A torus polygon that winds around the torus lifts to an open self-avoiding walk in , not to a polygon, so the polygon bound (58) does not apply directly. A polynomial correction for self-avoiding walks in three dimensions is, to current knowledge, not proved: Hammersley–Welsh and Kesten give only subexponential factors. Clauses (63) and (64) further need the numerical estimate as a theorem, a margin well below the published rigorous upper bounds.
Everything is finite: probabilities are finite sums over the chains, with no measure theory. Sites are ZMod L × ZMod L × ZMod T with NeZero for , and links are (site, Fin 3) pairs, so self-loops and parallel links on small tori are kept. The decoder maximizes directly rather than minimizing the logarithmic weights, which are undefined at . The goal quantifies over every maximum-likelihood decoder. is the exact infimum , never the decimal. Polynomials are encoded as or , with and quantified before every other variable, and is .
The failure event is "contains a cycle with odd spatial winding". It is not "", which is far too large, and not the homology class of , which is smaller and would give a weaker theorem.
Needed infrastructure: -chains on the cubic torus and their boundary, winding parities, self-avoiding walks and polygons in and on the torus, submultiplicativity of , and Hammersley-type polygon concatenation. The walk and polygon counts are reusable beyond this mission. Proofs of the elementary milestones (49)–(55) and (61) are welcome independently of the counting results.
Entanglement shared between distant parties is the resource behind quantum key distribution and quantum teleportation. Sent directly through optical fibre, a photon survives a distance with probability , so the expected number of photons needed to deliver one entangled pair grows exponentially in . A quantum repeater splits the channel into short segments and stitches them together, aiming at a cost that grows only polynomially in . Conventional repeaters do this with matter quantum memories at the intermediate nodes, which must hold their state while heralding signals travel between distant nodes.
Azuma, Tamaki and Lo (arXiv:1309.7207v1, 2013) proposed an all photonic quantum repeater: every intermediate node uses only single-photon sources, linear-optics elements, photon detectors and active feed-forward, with no matter memory. Their headline claim is that this design keeps the polynomial scaling: "the communication efficiency still scales polynomially with the channel distance" (abstract, p. 1). This mission formalizes that claim in the paper's own probabilistic model.
Timeline. Varnava, Browne and Rudolph (PRL 97, 120501, 2006) introduced loss-tolerant measurements on tree cluster states and showed they work for any per-photon loss below . Azuma, Tamaki and Lo (2013; Nature Communications 6:6787, 2015) built the memoryless repeater on these measurements. Pant, Krovi, Englund and Guha (arXiv:1603.01353, 2016) analysed rate–distance trade-offs and resource costs of such all-optical repeaters.
Alice and Bob, a distance apart, are joined by source nodes and receiver nodes, alternating and spaced apart. Each source node emits a cluster state with arms; each arm consists of a 2nd-leaf photon, sent to a neighbouring receiver node, and a 1st-leaf qubit, kept at the source. Each receiver node attempts linear-optics Bell measurements on pairs of arriving photons. It then directs the source nodes to measure the 1st-leaf qubits belonging to the successful Bell measurement in the basis, and all the others in the basis. Every photon is lost independently with probability .
The 1st-leaf qubits must be measured despite loss, so each is encoded in a tree cluster state with branching parameters : the 1st level holds qubits and each qubit of level has children. Its number of qubits is
The indirect -measurement success probability of a qubit on level satisfies, with and for ,
The loss-tolerant - and -measurements succeed with probabilities
and one Bell measurement succeeds with probability (C2). A trial of the repeater succeeds with probability
and the average number of single photons consumed per entangled pair is
In Lean these are indirectZSuccess ε0 l b k, treeSize l b, zSuccess, xSuccess, bellSuccess ε0, repeaterSuccess ε0 n m l b and expectedPhotons ε0 n m l b.
For every there are and such that for every there exist , and with
Since , this is for a fixed spacing. The goal asserts the shape of the bound only; the degree is left free because it must grow as .
The result separates a memoryless photonic repeater from direct transmission: for any loss probability below per segment, the cost per pair is polynomial rather than exponential in the distance. It is the theoretical basis for the all-photonic repeater line of work and for its experimental demonstrations, and it isolates the threshold as the single place where the loss tolerance of tree cluster states enters.
The paper itself reaches the conclusion through an upper bound (C9), approximate parameter choices (C10)–(C11), and a numerical fit (A4), , quoted from earlier numerical work. The mission states the claim exactly in the paper's model and invites a proof by another route, so a complete development turns a numerically supported conclusion into a machine-checked theorem. No part of it is formalized elsewhere as far as a search of the platform shows; Pant et al.'s depth-two tree probabilities are posed on the platform as a separate open goal for a different, operational model.
The obvious argument fixes a tree and lets grow. That fails: contains , so any fixed tree with makes decay exponentially in . The failure probabilities of the loss-tolerant measurements must shrink like , and the tree that achieves this must grow only polynomially in . This is where is needed: deep trees help only when a lost qubit is more likely to be recovered through its children than lost, and the trade-off between (which wants deep, narrow trees) and (which wants wide ones) has to be balanced quantitatively. The paper only settles this numerically. A second, milder difficulty is that must grow with to keep the Bell factor bounded below, and itself multiplies the cost.
All objects are real-valued functions of , natural parameters and a branching sequence of which only are read. Powers are natural-number powers with , the paper's convention for . (A3) is printed for ; it is used also at , since (A16) reads and (A12) gives the same formula at every level. The exponent uses truncated subtraction, irrelevant for . is a fixed parameter; the physical estimate (C6) is not part of the model.
is a real quotient, and Lean evaluates as . A goal stating only would be satisfied by a degenerate tree with , which gives and hence . The goal therefore asserts and requires , and every . The constants are chosen after and before ; with chosen after the statement would be trivial.
Only Mathlib's real analysis is needed: Bernoulli's inequality, , logarithms and ceilings. Error analysis ((A5)–(A17), (C14)–(C19)), the preparation cost of the cluster states ((B1)–(B5)), and the numerical examples are out of scope. Proofs of the milestones, alternative decompositions through sketches, and sharper bounds on the degree are welcome.
Schumacher's quantum data compression (Schumacher, 1995) encodes copies of a quantum source into about qubits, where is the von Neumann entropy of the source. The encoder is a fixed unitary transformation on qubits. As Bennett described (Physics Today, 1995), one realization of it is a sorting permutation: order the basis states by their number of 1's, so that the typical subspace becomes a block of consecutive basis states that can be kept while the rest is discarded. Cleve and DiVincenzo (arXiv:quant-ph/9603009v1, 1996) asked how to carry out this permutation as an actual quantum computation, and gave explicit reversible programs for it.
The difficulty they address is not computing the permutation, which is classical combinatorics, but computing it in place: a quantum computer must map to with every work register returned to , because leftover garbage would entangle the output with the input and destroy the superpositions that compression is meant to preserve (§III B, p.13).
An -bit string is the binary number ; is the first, most significant bit. Its weight is its number of 1's. The Schumacher coding function sends the strings of weight to the block of consecutive values starting at , keeping their numerical order inside the block (Eqs. (4)–(6)):
where the index number is the number of -bit strings of weight that are smaller than . In Lean these are weight, blockStart, index and schumacher n x.
The paper writes its programs in a pseudocode over integer registers (§III A). Statements are assignments , bit flips (where is bit of ), and conditionals if … then …; for loops have classical counters and constant ranges, both ends included. is the number formed by bits of . Three programs appear:
Correction. The restore loop is printed as if S ≥ m then X ← X + C(n,m) in all three programs. The text requires the loop to leave (p.17), which needs if S ≤ m. With the printed condition, and already fail: FINAL_SCHUMACHER_INVERSE maps to , and FINAL_SCHUMACHER maps to . The corrected restore loop of FINAL_SCHUMACHER_INVERSE reads
for m = 0 to n do
if S ≤ m then X ← X + C(n,m)
and the mission states every program with this one change; everything else is as printed.
For every and every ,
Both registers are in the conclusion: the data register is transformed in place and the counter is finalized to .
The goal is the correctness statement for the paper's main construction, which the authors call its essential result (p.7). It says that Schumacher's encoder is a classical reversible program using, besides the data, only a counter of bits, and that its inverse (the decoder) is obtained by running it backwards. Gate counts for the bit-level implementation (§IV, elementary gates) rest on these programs being correct.
The paper argues correctness informally and does not prove the time-reversal claim or the disjoint-bits claim. The printed restore loop is wrong, so a machine-checked proof also settles which program is correct. No part of this construction has a machine-checked proof that we know of. The platform has Schumacher's asymptotic coding theorem from another source (QAlgorithms.Papers.Independent.Renew46.P43.schumacherScheme), which is a statement about rates and fidelities, not about this permutation or these programs.
The combinatorics (Eqs. (9), (21), (23), bijectivity) is a form of the combinatorial number system, which Mathlib does not provide in this shape. The program proofs need an invariant across the unrolled third loop: after pass , is the weight of the remaining suffix of and the low part of the register is its index. In FINAL_SCHUMACHER_INVERSE the answer bits and the index share one register; the bound is what keeps them apart (milestone 6).
The obvious approach to the forward clause, showing that each statement of FINAL_SCHUMACHER is a left inverse of the matching statement of FINAL_SCHUMACHER_INVERSE, fails. The statement "if and then " is not injective on all integers, because a borrow can clear bit . Time reversal holds only along the actual trajectory, so the forward clause needs the trajectory invariant.
Registers are integers (ℤ). is the two's-complement bit Int.testBit X j. is , and , so . The p.18 remark that in the final pass "the comparison should not be performed at all" is read as "no quantum comparison is needed": the condition has a fixed outcome. Along every run, values stay in the range of the paper's signed -bit register, so nothing wraps around. The printed -bit width of is dropped, because reaches . Programs are lists of statements with one element per pseudocode line, loops unrolled in the printed order, run by a left fold. Statements are about basis states: the unitary of a classical reversible program is its permutation matrix. Every is allowed, including .
The function is defined directly by Eq. (6) as a block offset plus a rank count, never through a program. A formalization that defined as the output of FINAL_SCHUMACHER, compared on the untruncated , or dropped from the conclusion would be trivial or different, and is ruled out.
Useful contributions are a library for the combinatorial number system (rank of a fixed-weight word, Eqs. (9) and (23), bijectivity), which is reusable beyond this mission; trajectory lemmas for the unrolled programs; and proofs of milestones 5–7.
Many service systems match a set of agents with work to a set of servers in every time slot: devices sharing radio channels in cognitive radio, workers and tasks on an online service platform, customers and providers in a marketplace. When the matching is computed centrally and the service rates are known, the MaxWeight policy, which in every slot serves a matching maximizing , keeps the queues stable whenever any policy can (Tassiulas–Ephremides 1992). In the applications above there is no central planner. Each agent sees only its own queue, does not know the service rates, and learns only whether its own request was served.
Freund, Lykouris and Weng (arXiv:2206.03324v3, 2023; preliminary version at COLT 2022) give a fully decentralized learning algorithm for this setting, DAM.FE, and prove that it keeps the time-averaged weighted queue length bounded by a quantity that depends only logarithmically on the number of queues. Earlier learning results for this problem are centralized, or require a symmetric system; even in the centralized setting, the only asymmetric result, Q-UCB of Krishnasamy, Sen, Johari and Shakkottai (2021), assumes that each agent has a unique, well-separated optimal server. DAM.FE needs no such structure and allows zero service rates.
There are queues and servers . Queue receives a new job in each slot with probability . In each slot it either requests a server , sending a bid with the request, or requests nothing (). Server selects, among the queues requesting it, one with the highest bid, ; that request succeeds with probability , and the others fail. With and the indicators of an arrival and of a successful request, the queues evolve by
The set of flows is . The system has traffic slackness if for some , where . Every nonzero rate is at least a known .
DAM.FE works in epochs of slots. At the start of epoch each queue explores with probability , : it requests a uniformly random server with a very high bid for the whole epoch and records the outcomes after its first success. Otherwise it runs a decentralized auction, DAM.CONVERGE, on the weights built from optimistic estimates of the service rates, raising its private price for a server when it suspects it is not matched there. After slots it commits to its last server and bid for the rest of the epoch. The lengths , , are fixed by eq. (2) of the paper, and by eq. (5).
There is an absolute constant such that for every system, every as above, all tie-breaking rules and every horizon , if all queues follow DAM.FE then
The milestones are the paper's lemmas on the way to Theorem 2, in proof order.
Theorem 2 shows that agents who never communicate, never learn the rates in advance and receive only one bit of feedback per slot match the queue-length bound the authors prove for known rates, apart from a transient term that vanishes as . The dependence on the number of agents is through . That transient is what the decentralized learning costs. The paper's Section 5 replaces forced exploration by optimistic estimates under the extra assumption , and Section 6 extends the analysis to queues that arrive and depart.
The result is proved in the paper; no part of it has a machine-checked proof. The mission produces a formal model of decentralized bipartite queueing with bid-based contention, a pathwise formalization of a Bertsekas-style auction with private prices, and the Lyapunov-drift argument. Apart from the Lyapunov-drift step these pieces do not depend on each other: the auction lemmas (3.2, 3.4–3.8) are combinatorial statements about one epoch and the LP lemma 3.7 is pure duality. They can be proved before any probability is involved.
The obvious argument would compare DAM.FE epoch by epoch with a centralized MaxWeight schedule. It fails in three places. First, the queues do not share prices: each queue runs its own auction and infers from repeated failures that it is unmatched. The convergence bound with only logarithmic dependence on (Lemma 3.6) needs a potential argument over geometrically shrinking sets of active queues. Second, a failure can come from the random service coin rather than from a collision, so convergence holds only on the good checking event, whose probability must be bounded through the choice of . Third, exploration samples are corrupted when explorers collide, so the estimates are unbiased only because DAM.UPDATE discards everything before an explorer's first success (Lemma 4.1). The number of samples is then random, and concentration needs an optional-skipping argument. Using the estimates in the drift requires controlling the event that some estimate is wrong after .
Queues and servers are Fin N and Fin K, with ; is none. Time slots start at and epoch starts at . The randomness is a product probability space of mutually independent primitives: Bernoulli arrivals, one Bernoulli service coin per pair and slot, uniform perturbations , exploration coins and explored servers. The processes are deterministic recursions in this randomness. Tie-breaking is a parameter, universally quantified over all measurable rules. Expectations are Bochner integrals, and every statement also asserts that its integrands are integrable, so that no bound holds because the integral defaults to zero. is written . In eq. (2), is ; DAM.COMMIT requests through the last slot of the epoch; the confidence radius is infinite for a pair without samples.
The constant in Theorem 2 is quantified before the instance. A constant depending on , , , or would make the statement a stability claim, which the trivial bound already gives for bounded .
A complete development needs: optional skipping for i.i.d. sequences, Hoeffding's inequality for Bernoulli samples, conditional expectations given a random vector, and finite LP weak duality over . Proofs of the pathwise auction lemmas, and general lemmas about the auction step that the drift lemmas can reuse, are welcome.
In an online linear program, customers arrive one at a time and a firm must accept or reject each one at once, spending a shared inventory of resources. The model covers network revenue management, ad allocation and order fulfilment (Li and Ye, 2022). Its central performance measure is the regret: the gap between what an omniscient planner collects and what the best online policy collects. When the customer law is continuous, it was unknown how fast this gap grows with the horizon in more than one dimension.
Timeline:
Fix , a law of a pair and an endowment . Periods are counted backward from to , and customers are i.i.d. from . You begin with stock and write for the stock per remaining period, the inventory vector. In period you see and choose , accepting only if . A non-anticipating policy bases on the customers of periods only.
The offline benchmark and the regret are
The limiting dual is . The assumptions are: almost surely; ; almost surely; has a minimizer over ; and the Jacobian of exists, is full rank, and is continuous near .
There are and such that for all and every non-anticipating policy,
The goal fixes the order of quantifiers, and it does not fix , which depends on , and .
Together with Theorem 1, the goal pins the regret of the known-distribution problem at . It shows that the logarithm cannot be removed by any online policy, however clever, when the customer law has a continuum of marginal customers; the finite-type case has bounded regret, so the continuum is what costs.
The result is proved on paper; no machine-checked proof of it or of its milestones is known. A formal development produces non-anticipating policies with an integer offline benchmark, the primal-dual decomposition of regret, and uniform empirical-process bounds for random shadow prices.
The optimal policy has no closed form, so it cannot be analysed directly. The natural first idea, to compare it with a fixed-threshold or fluid policy, gives only an upper bound on its regret. The lower bound must instead show that any policy with small regret keeps its inventory near , and that near every decision rule pays because the empirical shadow price fluctuates at scale in every direction. The fluctuation claims are uniform in , since is random, and that uniformity needs empirical-process tools with only .
is EuclideanSpace ℝ (Fin m) with the componentwise order VLe, and balls are Euclidean. A sample of horizon is Fin n → ℝ × E m, where the index holds period . Policy is non-anticipating by type, and a decision is masked by feasibility. The offline values are offlineIP and offlineLP; regret is a difference of Bochner integrals of functions integrable under the assumptions. Shadow prices are all minimizers of the dual, with outer expectations in upper bounds and inner probabilities in lower bounds. Non-unique and non-measurable objects therefore cannot be used to weaken a claim.
Two trivializations are ruled out explicitly: at every assumption is vacuous and the regret is , so the goal assumes ; and a policy that reads later periods, or accepts infeasibly, could reach the offline value, which the type and the mask exclude.
Printed slips are corrected and declared item by item: the case split of in (35), and Lemma 4 at small .
Needed infrastructure: LP duality with box constraints, finite-horizon dynamic programming with a continuous state, Azuma–Hoeffding, empirical-process maximal inequalities, and convergence to a Gaussian process. The last two are reusable beyond this mission. Contributions to any milestone, and to general libraries behind them, are welcome.
Retailers, hospitals and data-center operators repeatedly decide how much to stock before demand is seen, and in practice the demand distribution drifts over time while external predictions of its mean (human judgement, forecasting software, machine-learned models) are available but of unknown quality. The newsvendor problem is the classical model of a single such decision (Arrow, Karlin and Scarf 1958, ref. [3] of the paper). Regret analysis of repeated newsvendor problems with i.i.d. demand is classical (Levi, Roundy and Shmoys 2007; Besbes and Muharremoglu 2013), and drifting means were studied by Keskin, Min and Song (ref. [27] of the paper). An, Li, Moseley and Ravi (arXiv:2305.07993) give a complete minimax treatment of the nonstationary newsvendor with general (possibly discrete) demand and order sets, and then ask how to use predictions whose accuracy is unknown. This places the problem in the learning-augmented algorithms literature (Lykouris and Vassilvitskii 2021), where a policy should exploit good predictions and remain robust to bad ones.
A model fixes a parameter interval , cost bounds , a nonempty set of allowed orders, and a family of demand laws on with mean , each sub-Gaussian. In periods the decision-maker sees costs , and a prediction , orders using only past demands, and then observes , independent over time. The expected cost is
assumed -Lipschitz in (Assumption 2). The regret of a policy is .
Nonstationarity is measured by the demand variation , the largest value of over all increasing sequences of periods ; the class requires . Prediction quality is measured by the total error , with unknown to the policy.
The Fixed-Time-Window Policy orders optimally for the average of the last demands; the Prediction Policy orders optimally for ; both round their estimate into . The Prediction-Error-Robust Policy (PERP) follows the predictions until reaches , and from then on follows the window average.
For every and with , where bounds the noise uniformly by , there is a constant such that for all , and every instance in with prediction error at most ,
The printed statement bounds the regret by with a constant independent of . A point-mass instance with and violates it, and at it bounds a positive regret by . The goal is the conclusion of the paper's own proof (Appendix G) and of the informal Theorem 2: may depend on the model, , and , never on , , or the instance.
Lemma 1, ; Observation 1a), the Prediction Policy has regret at most ; Observation 2, per-period regret is uniformly bounded; Observation 3, a plug-in policy has regret at most ; Lemma 3, Hoeffding's inequality for averages with constant ; Lemma 4, the drift of the window average is under ; Lemma 5, its noise is in expectation.
Theorem 2 shows that not knowing the prediction accuracy costs only a factor: by the paper's Proposition 2, is unavoidable even when is known. With perfect predictions the regret is , and with useless ones it matches the best prediction-free rate . Proposition 3 of the paper shows that when is also unknown no such adaptivity is possible, so the result marks the boundary of what predictions can buy.
The results are proved on paper; none is machine-checked. A formal development certifies a regret bound for a policy with a data-dependent switching time, including the edge cases the paper's proofs set aside (the ceiling in the window size, the switch at the first period after the window, small), and it exposes the two defects of the printed statement recorded above. The model layer (expected newsvendor cost, demand variation, product law of independent demands, nonanticipating policies, interval regret) is reusable for other nonstationary inventory and learning-augmented problems.
The obvious argument splits the horizon at PERP's switching time and applies the prediction bound before it and the window-average bound after it. That fails as stated: the switching time is random and depends on the whole demand path, so the expected regret after it is not the regret of the Fixed-Time-Window Policy on a fixed interval. The proof instead builds a good event on which every window average is accurate simultaneously. Hoeffding's inequality for each window and a union bound over windows give it probability , and (G.1) is exactly what makes the union bound work. On that event the switch can occur only if the predictions are genuinely bad, which forces . Off it, Observation 2 bounds the damage by a constant. Lemma 4 is a separate combinatorial step: the drift inside each window is controlled by through interleaved partitions, one per residue class of the period modulo .
Periods are ; demand paths are sequences indexed by under the product of the laws (Mathlib's Measure.infinitePi), and coordinates outside are never used. Orders come from an arbitrary measurable argmin selection, and every statement holds for each such selection. The clairvoyant term is the infimum of the cost over . Worst-case regret is stated as a bound for every instance of the class. The window size keeps its ceiling. Rounding into is , and PERP's test uses the unrounded estimates. Two sub-Gaussian conditions appear, each where the paper uses it: the tail condition (Assumption 1(b), Lemma 3) and the uniform noise bound (Lemma 5, (G.1)). The logarithm is natural.
The constant of the goal is quantified before , , , the selection and the instance; a constant chosen after them would make the bound empty. The selection must be measurable, since otherwise the expected cost is not defined.
Lemma 2 of the paper, the explicit constant for the Fixed-Time-Window Policy, is not a milestone: with the printed constant it is false when is large relative to (all orders are then arbitrary). Its asymptotic content enters the goal's proof through Lemmas 4, 5 and Observations 2, 3.
A complete development needs: Hoeffding for tail-sub-Gaussian variables (Mathlib's HasSubgaussianMGF route plus a tail-to-MGF step), integrability of the regret integrand, the residue-class partition argument, and the good-event decomposition. Contributions of each piece, and of the Fixed-Time-Window regret bound with a correct constant, are welcome.
A blockchain confirms a limited number of transactions per block. Users attach fees (bids) to their transactions; the block producer (the miner) chooses which transactions to include and collects some of the fees. The rule that maps bids to confirmations, payments and miner revenue is a transaction fee mechanism (TFM). Because the miner is itself a strategic party that can collude with users, inject fake transactions or drop real ones, a TFM must resist more deviations than an ordinary auction.
Roughgarden (arXiv:2012.00854, 2020) formalized the desiderata for Ethereum's EIP-1559. Chung and Shi (arXiv:2111.03151, SODA 2023) proved that no TFM can be both dominant-strategy incentive compatible for users and 1-side-contract-proof while giving the miner positive revenue: in that setting the miner's revenue must be zero. Chen, Simchi-Levi, Zhao and Zhou (arXiv:2209.13099, Operations Research 2025) relax dominant-strategy to Bayesian incentive compatibility, with valuations drawn i.i.d. from a known law, and construct a mechanism that escapes the zero-revenue barrier.
There are users and a block of size . User has a valuation ; valuations are i.i.d. draws from a law on , and . Users submit bids .
A TFM consists of an allocation rule (the probability that user is confirmed), a payment rule (paid by user if confirmed) and a miner revenue rule . User 's utility is ; the miner's utility is .
The properties studied are:
Mechanism 3 confirms transactions by weighted sampling without replacement with weights ; is the resulting inclusion probability. Its payment is the Myerson payment of this allocation plus a quadratic variation term
and the miner receives .
For any , and , Mechanism 3 is U-BNIC and 1-SCP. For any and , with , it is UIR and BF for every
Finally, there is an absolute constant such that for every the mechanism is -U-SP.
Theorem 4 shows that Bayesian incentive compatibility suffices to give the miner positive revenue while keeping users truthful, blocking miner–user collusion and Sybil attacks, and keeping the mechanism individually rational and budget feasible. The expected miner revenue is , a constant fraction of the optimum for fixed once . The auxiliary-variation decomposition (Theorem 2) is a general recipe that applies to any monotone allocation.
None of this has been machine-checked. A complete development would give a verified Myerson lemma for allocation rules with general block size. Mathlib has no such lemma, and the version already on the platform covers single-unit auctions only. It would also give a formal treatment of inclusion probabilities in weighted sampling without replacement (Plackett–Luce sampling), with monotonicity and the "adding an item" comparison. Both are used well beyond blockchains: in ranking, survey sampling and randomized auctions.
The printed definition (18), , is a slip: the paper's own proofs use , and under the first clause fails (for the uniform law a value-1 user gains by shading her bid). The mission states the corrected theorem.
The U-BNIC and 1-SCP clause reduces, through Theorem 2, to monotonicity of the sampling allocation and to Lemma 2, which is a second-moment computation. Monotonicity is the first obstacle. The inclusion probability is a sum over all injective draw sequences, and raising one weight raises some terms and lowers others, so a term-by-term comparison fails. The paper uses a coupling through a common uniform sequence (Algorithm 1). Lemma EC.4 needs the same coupling.
UIR and BF need a quantitative lower bound on that is uniform in the other bids and in . The obvious bound loses a factor that tends to zero as , and the explicit constant comes from a careful choice of . The U-SP clause for general is only sketched in the paper ("in a similar way"). Its fake-bid bookkeeping, with mechanisms at different bid counts and their own , has to be written out in full.
Users are Fin n. Bids, values and the other users' bids range over , and is a vector in whose -th entry is overwritten. is any probability measure on with and , a generalization of the paper's density assumption. Interim expectations are Bochner integrals against the product measure with coordinate overwritten. U-BNIC and U-SP require the integrands to be integrable, so that a non-existent expectation, which Lean evaluates to , cannot make them hold vacuously.
The allocation sums the outcome probabilities (24) over injective sequences, so gives . Payments are payments-if-confirmed and expected payments are . The auxiliary payment is written in the form (EC.137), . 1-SCP is the ex-post deviation of the miner together with one user's bid. The in U-SP is an absolute constant , chosen before , , , the and . Lemma 1, Lemma EC.3 and Theorem 2 are stated for allocations differentiable in the own bid, as their formulas presuppose.
Definitions: Model, Properties, Decomposition, Sampling, Mechanism3 and Constants, in the namespace BlockchainTFM. The Myerson-type lemmas and the sampling lemmas are reusable on their own. Contributions on the sampling coupling and on the envelope argument behind Lemma 1 are particularly welcome.
Many resource allocation problems arrive one request at a time: an ad exchange decides which campaign gets an impression, a network admits or routes a call, a cloud provider schedules a job. Each decision earns a reward and consumes several budgets, and it cannot be revisited. The usual benchmark is the offline optimum, the best total reward attainable with the whole request sequence known in advance. Dual-based algorithms handle the online problem by pricing the resources through Lagrange multipliers and treating each request greedily against those prices.
Balseiro, Lu and Mirrokni (arXiv:2011.10124) analyse a single algorithm of this kind, dual mirror descent. It updates the prices by online mirror descent and needs no knowledge of the request distribution. Earlier dual methods (Devanur–Hayes 2009, Agrawal–Wang–Ye 2014, Devanur et al. 2019) estimate prices from samples or solve auxiliary linear programs, and they assume linear or concave rewards. This paper allows non-concave rewards, non-linear consumption and non-convex or integral action sets. It shows that the same algorithm has sublinear regret under i.i.d. input, a constant competitive ratio under adversarial input, and good behaviour under several non-stationary inputs. This mission formalizes the i.i.d. result, Theorem 1.
There are resources and a horizon of periods. A request consists of a compact feasible set with , a reward function and a consumption function with values in and . The total budget is , where for every . For a request sequence the offline optimum is
Assumption 1 asks for constants such that and on , and such that is attained for every . Write and .
Algorithm 1 is given a reference function , a step size and an initial price vector , and starts with . In period it computes . It plays if and otherwise, and sets . It then takes the subgradient and updates
Its reward is . Assumption 2 requires that be differentiable or essentially smooth in , and -strongly convex in there.
For every and every probability law on ,
with and . The constant is the largest Bregman divergence over the points . The algorithm is fixed before , so the bound holds for the worst-case regret . With it is .
The theorem gives an regret bound for an algorithm that knows neither the request distribution nor the horizon's statistics. It holds without convexity of the rewards, the consumption or the action sets, and the constants do not grow with the number of resources once norms are matched to the problem ( in the primal, in the dual). Choosing different reference functions turns the same statement into bounds for projected subgradient descent () and for multiplicative weights (). The paper's lower bound of order (Lemma 1, from Arlotto–Gurvich) shows the rate cannot be improved in general.
The result is proved in the paper. As far as a search of the platform shows (October 2026), none of its statements has a machine-checked proof. Proved platform theorems give online mirror descent bounds under other hypotheses: closed domains, Legendre reference functions, Euclidean norms. This mission adds the online allocation model, a formal Algorithm 1 with its budget check, and the probabilistic argument that connects them.
The natural first attempt is to bound by the dual function at a fixed price and compare it with the algorithm period by period. This fails because the algorithm stops playing its proposed actions once a budget runs out, and that can happen at a random time. The proof therefore works up to the stopping time and needs three separate ingredients:
The expected dual objective is evaluated at random, history-dependent prices. So the measurability of the run, of the argmax selection and of must be handled explicitly. When is only essentially smooth, one also has to show that the mirror step stays in the open orthant, where exists.
Fin m, actions Fin d → ℝ, and periods Fin T counted from . A request type carries , , (DualMirrorAlloc.Requests).sSup). Under the model and Assumption 1 these sets are nonempty and bounded, so the suprema are the true values.act, md with the optimality property, and every selection is covered.fderivWithin). Assumption 2.1 keeps both branches: differentiable within the orthant, or essentially smooth relative to it. Strong convexity (2.2) is required where the derivative exists, is such a point, and the norms are written as and coordinatewise bounds.Measure.pi (fun _ : Fin T => P) for an arbitrary probability measure on a measurable space , with the algorithm fixed first.A complete development needs the following:
The online mirror descent bound (Proposition 5) and the model of Algorithm 1 can be reused for the paper's other input models. Proofs of any milestone are welcome, as are proofs of Proposition 5 by other means.