Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
This mission develops Chapter 21 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the symmetrization lemma of Minsky and Papert.
Let be multilinear, meaning that every variable has degree at most in . For , let
where is the Hamming weight of (its number of 1s). Then there is a univariate polynomial with (total degree) such that for every .
Symmetrization reduces questions about multivariate polynomials that represent symmetric Boolean functions, such as parity or OR, to questions about univariate polynomials. Those questions can then be settled by counting sign changes or by Markov's inequality.
Formalization Note The statement that " is a polynomial" is formalized as agreement with a univariate polynomial on the points , the only points where is defined. For these the average is taken over a nonempty set.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 27 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Fix integers . There is a single colouring rule , chosen before the graph, that assigns to an ordered pair of vertices a colour that depends only on the two vertices, their sides of the bipartition, and their neighbour lists , with the following property.
Let be an undirected simple graph on the vertex set with a bipartition (every edge joins the two sides) and maximum degree at most , and let be any duplicate-free list of the neighbours of each vertex . Then the map is a proper edge colouring of :
In the source the colour of an edge with on the left is , where is the position of in the neighbour list of . The lemma is the colouring step of the simulation of sparse Hamiltonians: the edges of each colour class form a matching, whose Hamiltonian is simulated separately before the pieces are combined by a product formula.
Formalization Note The source's "efficiently computable" has no machine model, so the running time of the rule is not formalized; what is kept is that one rule serves every graph and reads only the two endpoints' local data (two neighbour-list queries per edge). Colours are pairs of natural numbers rather than elements of so that the rule is total at ; the bound is on the colours actually used on edges.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 9 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the classical post-processing step of period finding over the reals (Childs, Lemma 9.1).
Write for the integer nearest to the real number . Let be a real number (the period, possibly irrational), let be a positive integer (the size of the cyclic group used for Fourier sampling), and let be relatively prime integers with and ; Fourier sampling returns the integers and . If , then:
Thus, from two samples with coprime multipliers, one learns from the continued fraction expansion and then an approximation of to within .
Formalization Note The nearest-integer function is Mathlib's round (ties rounded up; the source leaves ties unspecified and its proof uses only that the rounding error is at most ). Convergents are Mathlib's Real.convergent, which coincide with the convergents of the regular continued fraction. The ranges are those the source's proof uses (they come from and the proof's appeals to and ); the proof's " without loss of generality" is not imposed. Under these hypotheses the denominator is at least , so no division by zero occurs.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 33 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be the number of gates of a quantum circuit and let . In the adiabatic simulation of the circuit, the interpolated Hamiltonian leaves invariant the -dimensional computational subspace spanned by the history states , and on it acts, by and , as the real symmetric matrix
whose entry is , whose first off-diagonal entries are , and whose other entries vanish. Let be its eigenvalues, counted with multiplicity, and the gap between the smallest and the second smallest.
Lemma. The gap is uniformly in : there are a constant and a threshold such that
This bound on the minimum gap along the whole interpolation path is what makes an adiabatic evolution time sufficient, and hence shows that adiabatic quantum computation can efficiently simulate the circuit model.
Formalization Note The matrix is the shared definition clockPathMatrix k s on ; the gap is spectralGap, the second smallest minus the smallest eigenvalue of the Hermitian matrix with multiplicity (so a degenerate ground level would give gap ). The constants and are quantified before and .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 6 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the correctness statement of the standard quantum algorithm for the Abelian hidden subgroup problem.
Let be a finite Abelian group written additively (), with characters , , and quantum Fourier transform , . Let be a finite set, a subgroup, and a function hiding :
The standard algorithm starts in (registers of dimensions and ), prepares , computes in superposition with one query, , (measures the second register,) applies to the first register and measures it. For every the outcome occurs with probability
Since , the algorithm samples uniformly from the labels of the elements of ; each sample gives a linear constraint on , which is how the algorithm generalizes Simon's algorithm, period finding and discrete logarithms.
Formalization Note The finite set is given an arbitrary additive group structure so that computing is the unitary , which maps to as in the source. The intermediate measurement of the second register (step 4) is omitted: it does not change the distribution of the first register, so the output law is the first-register marginal of the state before the final measurement. The source's claim that can then be found efficiently from few samples is asserted without proof and is not part of this statement.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 29 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
For let
and for let . For and a phase vector , the quantum signal processing sequence is
with factors . For a polynomial write for the polynomial with complex-conjugated coefficients (so for real ).
Lemma. Let and . There exists such that for every
if and only if
This characterization is the core of quantum signal processing: it says exactly which polynomial transformations of a signal can be implemented by interleaving the signal rotation with -rotations, and it is later lifted, via qubitization, to polynomial transformations of block-encoded operators.
Formalization Note The matrix identity is required for all , the domain on which is defined in (29.6). The degree condition uses Mathlib's degree with values in , so is written ; the parity of is written as parity , which is the same residue and avoids natural-number subtraction. Parity is the polynomial identity .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 4 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be a unitary matrix acting on a finite-dimensional space, and let be a unit eigenvector of with eigenvalue , where :
Fix , put , and suppose can be written exactly with bits, i.e. for a natural number (necessarily ). Run phase estimation: start in , apply the quantum Fourier transform to the first qubits, apply the controlled power , then apply to the first qubits and measure them in the computational basis (bit strings read most significant bit first). Then
This is the exact case of phase estimation, the subroutine underlying Shor's algorithm, quantum counting and many Hamiltonian algorithms.
Formalization Note The final state is the shared phaseEstimationState, with ; the probability of outcome on the first register is the marginal . The source's general-case claim (an -bit approximation with additive error 'with high probability') supplies no probability constant and is not stated.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 3 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the analysis of Simon's algorithm.
Let and identify with ; write for bitwise addition modulo and . An input is with , and Simon's promise says there is a nonzero with . A query is the unitary . One run of the subroutine prepares
(one query, Hadamard gates) and measures the first register. Then:
Together these say that Simon's algorithm finds with an expected queries and polynomially many other operations, an exponential speed-up over classical randomized algorithms.
Formalization Note Item 2 uses the expected stopping time of an i.i.d. sequence drawn from the PMF whose masses are the first-register marginals of ; its existence is part of the conclusion. The intermediate measurement of the second register is omitted, as the source allows. The constant in item 4 also absorbs , where a circuit with no input wires cannot output the constant . The input strings are fed to the circuit row-major through .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 8 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be a squarefree integer with , and let . For write for the principal ideal generated by .
For all ,
Thus the map is multiplicatively periodic, with the units as its periods; this periodicity, with period the fundamental unit, underlies the periodic function used in Hallgren's algorithm for Pell's equation.
Formalization Note is Mathlib's ℤ√d, the principal ideal is Ideal.span {ξ}, and a unit is IsUnit. The statement holds also for (both sides then force ), so no nonzero hypothesis is added.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 26 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let , , and let be a finite workspace. Consider the Hilbert space with computational basis , where is the query input, the query output, the workspace and the oracle register. The compressed phase oracle is
Here is the Hadamard gate, is the compression unitary of §26.1 (it swaps and and fixes for ), and (the identity when ). Let be the projection onto the basis states whose oracle register contains a zero, i.e. for some . Then for every state (unit vector),
Iterated over queries, this shows that the compressed-oracle probability of having recorded a zero is . Combined with Lemma 26.1, this gives the query lower bound for unstructured search against a random oracle.
Formalization Note is an arbitrary unit vector of the full space; no reachability condition is imposed, and the proof uses none. The register order is , as in (26.30).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 18 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is the impossibility of perfect quantum bit commitment.
In de Wolf's model, a quantum bit-commitment protocol is represented by the two joint pure states that Alice and Bob share at the end of the commit phase when Alice honestly commits to the bit or . Here is Alice's space and is Bob's. Restricting to pure states loses no generality. The protocol is perfectly concealing if Bob's reduced density matrix does not depend on , where is the partial trace over Alice's register.
Let and let be unit vectors in with
Then there is a unitary on Alice's space such that
So after committing to , Alice can turn the joint state into the honest commitment to by acting on her own register only. The protocol is then not binding at all, and no quantum bit-commitment protocol is both perfectly concealing and perfectly binding.
Formalization Note Alice's space is indexed by Fin dA and Bob's by Fin dB. The joint space is indexed by Fin dA × Fin dB with Alice's register first. is traceLeft (pureDensity phi), and is Matrix.kronecker U 1 with in Matrix.unitaryGroup. When or no unit vector exists, so the statement is vacuous in those cases, as in the source.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 22 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
This is Kutin's symmetrization lemma for the collision problem.
Fix and consider strings , , encoded by the indicator variables if and otherwise (). A triple of natural numbers is valid if , , and . For a valid triple define the string
which is -to-one on its first positions and -to-one on the rest. For permutations of let and let be its indicator variables.
Let be any real polynomial in the variables , and for a valid triple set
Then there is a real polynomial in three variables with (total degrees) such that
Applied to the acceptance probability of a -query algorithm (a polynomial of degree at most in the ), this reduces the collision lower bound to degree bounds for a polynomial in three integer variables, to which Paturi's lemma is applied.
Formalization Note Indices and values are 0-based in Lean (Fin n); the defining formulas of are kept in 1-based form and the value is shifted by one. The polynomial is an arbitrary MvPolynomial (Fin n × Fin n) ℝ, not necessarily multilinear, and degrees are total degrees.
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 24 of Lecture Notes on Quantum Algorithms by Andrew Childs. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
Let be a finite-dimensional complex inner product space and let and be orthogonal projections on . Put , a unitary. For , let be the orthogonal projector onto the span of the eigenvectors of whose eigenvalues are with . If is a unit vector with , then
The lemma is the key step in showing that the phase-estimation algorithm built from a dual adversary solution rejects inputs with : the start state has little weight on eigenvectors of small phase.
Formalization Note and are given as the orthogonal projections onto submodules and ; is Mathlib's reflection through the subspace. The eigenvalue set is , which is the same set as with restricted to .
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This mission develops Chapter 12 of Quantum Computing: Lecture Notes by Ronald de Wolf. The chapter's selected results describe the mathematical guarantees below.
The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.
In the setting of Claim 3 (a feasible solution of the dual SDP for with objective value , the states , , the projectors , and the unitary ), let . For every there is a vector in the span of the eigenvectors of whose eigenvalues , , satisfy , such that
Equivalently, the component of in the eigenspaces of with eigenphase has norm at most . Together with Claim 3, this lets phase estimation with precision distinguish from .
Formalization Note The eigenphase is the principal argument Complex.arg, which takes values in ; the span of eigenvectors is the supremum of the eigenspaces of over the eigenvalues with . The informal "close" is pinned to the bound the source's proof establishes, and it is stated for every (the proof's own hypothesis; the source adds "we may assume " only to call the bound small).
These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.
Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.
This entry records a deterministic bound for 3SUM on polynomially bounded integers, using the campaign's shared word-RAM model with -bit words. Three distinct input positions must sum to zero; repeated values are allowed. The exact exponent is .
Designing a revenue-maximizing auction for several items is hard once buyers have budgets. Myerson's optimal auction (Myerson 1981) solves the single-item problem without budgets, under a known prior on the buyers' values. With several items, correlated values or budget constraints, no comparable characterization is known, and the Bayesian formulation requires a prior the seller rarely has.
Bandi and Bertsimas (2014) replace the prior by an uncertainty set: a set of valuation matrices that the seller considers possible. The seller then maximizes worst-case revenue over , subject to incentive compatibility, budget feasibility and individual rationality. This is the approach of robust optimization (Ben-Tal and Nemirovski 1998; Bertsimas and Sim 2004) applied to mechanism design. The paper's central object is a mechanism built from linear optimization problems, the robust optimal mechanism ROM. It looks like a Vickrey–Clarke–Groves mechanism with reservation prices that depend on both the buyer and the item.
There are buyers and divisible items . A valuation vector is an real matrix , with buyer 's value for one unit of item . The uncertainty set is a set of such matrices, and are public budgets. Writing for with row replaced by , a mechanism assigns to each bid vector an allocation and payments . It is feasible for the robust auction LP (5) if, for all and :
ROM has two stages. ROM.a runs before any bid. It picks a valuation and a nominal allocation solving the robust optimization problem (12). For each buyer it picks a minimizer of (14), and an optimal solution of a linear program (13). It then sets reservation prices (15). ROM.b runs on the bids :
The Lean development uses the same names: ROMData for the chosen optimizers, IsROMa, IsROM, rStar, PSet, QSet, alloc, pay, and IsFeasibleMechanism for (7)–(10).
For every uncertainty set of nonnegative valuation matrices, every nonnegative budget vector and every choice of optimal solutions of (12), (13), (14), (16), (17):
This is the feasibility half of the paper's Theorem 1; its proof (p. 1025) says "the feasibility follows from Propositions 3–5".
The result shows that a mechanism specified by the paper's optimization problems is incentive compatible, budget feasible and individually rational over an arbitrary uncertainty set. No distributional assumption is made, and multiple items and budgets are allowed. Proposition 2 also records the identity between the total reserved revenue and the optimal value of the auxiliary program (13).
Status. The paper's main claim, Theorem 1, says that ROM is optimal for (5), i.e. that it maximizes worst-case revenue. That claim is false as printed, and so is Proposition 6 (the worst case of ROM is attained at ). Small counterexamples refute both:
The feasibility half is true, and this mission formalizes exactly that half. No result of this paper is on Prove2Me yet, and no machine-checked proof of it is known.
The difficulty lies in the definitions and in how many problems interlock, not in any single deep step. ROM is defined through five optimization problems, none with a unique solution. The payments (21) of a buyer depend on the optimizer chosen in (17), which may differ between a truthful and a deviating bid vector. Incentive compatibility must therefore rest on properties of optimal values, not of particular optimizers. The robust constraints of (12) and (18) range over the whole of , which may be infinite. Relating to the multipliers of (13) requires replacing the robust constraint by a finite one before linear programming duality applies. Budget feasibility requires comparing two polyhedra whose budget rows differ by a term involving and . Neighbouring statements in the same section (Theorem 1, Proposition 6) are false, so no step can be taken on the paper's word.
Buyers are Fin n and items Fin m. A valuation matrix is Fin n → Fin m → ℝ, the uncertainty set an arbitrary Set of them, and is Function.update v i u_i. Every optimizer is a field of ROMData. IsROMa/IsROM assert optimality for exactly the page's problems, built from the same , , , . Every statement holds for every such choice, never for one canonical selection. Allocation and payments are for bids outside (step 1 of ROM.b); constraints (7)–(10) are imposed only on .
Committed conventions and additions to the page:
IsROM, and its satisfiability has been checked on a one-buyer, one-item instance.A trivializing formalization is ruled out: the optimizers are not fixed to degenerate values (such as or a canonical ), constraint (8) ranges over all deviations that stay in with the true values multiplying both allocations, and the hypotheses are jointly satisfiable.
A complete development needs finite-dimensional LP duality and complementary slackness (for Proposition 2), and finite-sum manipulation over Fin n with one index removed. LP duality lemmas in matrix form are reusable well beyond this mission. Contributions are welcome on any milestone, and on general LP duality statements stated in a form that applies directly to (33)–(34).
A planner often chooses a first action before uncertain inputs are known and a corrective action afterward. If the uncertain input has no trusted probability law, a distributionally robust model tests the first action against all laws consistent with known support and moment information. The corrective action may depend on the realized input. This combination produces a difficult optimization problem: the adversary chooses a probability law, while the planner chooses a function of the input. Bertsimas, Sim, and Zhang study a class in which the support and moment bounds have second-order-cone representations. Their particular question is whether a tractable affine corrective rule can recover the exact worst-case cost.
Earlier work on moment-based distributionally robust optimization developed other ambiguity sets and reformulations. The related Prove2Me drafts MinimaxSLP and TractableDRO address mean and second-moment equality classes or bounds on positive parts of affine functions. Their model conventions differ from this paper's lifted SOC support, so this mission develops its own definitions. The affine-policy result of Bertsimas, Iancu, and Parrilo concerns a different multistage robust model. The paper places these contributions in its account of robust and distributionally robust decision rules (pp. 604–605).
Write for the first-stage decision and for the observed uncertainty. After observing , the planner chooses a free second-stage vector . The constraint data depend affinely on : and . The fixed recourse matrix is , and gives the second-stage cost. The recourse value is
The support set restricts possible realizations. An SOC ambiguity set contains probability laws on for which , , and for each auxiliary function . The paper assumes that and each epigraph can be represented using products of second-order cones (Definition 3). Its exact worst-case expected recourse cost is .
The model introduces an auxiliary vector with lifted support . The lifted ambiguity set consists of joint laws on supported on with and . Proposition 1 states that the primary marginals of these joint laws are exactly . A regular linear decision rule has . An extended linear decision rule has . Their best worst-case costs are and , with feasibility enforced at every point of or respectively (§3.1).
Theorem 2 gives the comparison that holds for the two rule classes:
Theorem 1 identifies with the robust program (9). Its variables are , , and , constrained by at every ; its objective is . This result assumes relative complete recourse and Assumption 1, which represents the actual lifted support by a product of second-order cones and supplies a strict Slater point.
The mission's goal is Theorem 4. Under complete recourse and one second-stage decision variable, the extended affine class gives the exact value for every first-stage vector:
The equality is stronger than the bounds alone: it says that optimizing over this finite-parameter decision-rule class loses no worst-case value in the stated regime (Theorems 1, 2, and 4).
Theorem 4 gives a precise case where the lifted affine approximation is exact. This matters because the unrestricted corrective decision is a function, while the affine class is described by finitely many coefficients. The paper observes that, with one recourse variable, the associated dual polyhedron has only extreme points; the robust reformulation can therefore be handled using a finite collection of constraints in this regime (p. 610). Proposition 3 marks a boundary: relative complete recourse by itself does not ensure that any extended affine rule is feasible.
The results are proved mathematically in the published paper and its electronic companion; the proofs of Theorems 1 and 4 are located in the companion, which is not held with this mission's source PDF. The Lean statements here are open proof obligations. A completed development would add reusable interfaces for free-variable linear recourse, SOC-supported moment ambiguity sets, lifted joint laws, and extended-real optimization values. It would also make the assumptions behind the paper's real-valued expectations and recourse costs explicit.
Replacing the adaptive function by an affine function of alone can fail even when the recourse LP is feasible for every realization: a single affine rule must satisfy every pointwise constraint simultaneously. Adding enlarges the rule class, but the lifted support contains all , not just . Thus its feasibility condition is stronger than feasibility on a convenient graph. Theorem 4 asserts exactness despite that universal lifted-support constraint. The direct comparison does not by itself give the reverse inequality; the robust moment reformulation must describe the same worst-case value under its Slater and recourse hypotheses (§§2.2–3.1).
Finite vectors are functions on Fin n, so the paper's indices become zero-based. Laws are probability measures on finite real-vector spaces. The original and lifted ambiguity sets include integrability of all primary coordinates; the lifted set also includes integrability of all auxiliary coordinates, and the original set includes integrability of each . This is a finite-first-moment reading of the paper's expectations. It excludes laws whose constrained linear moments exist while an unconstrained coordinate has infinite absolute moment. These conditions ensure that expected affine rule costs are genuine. The paper's Theorem 3 itself explicitly asks for finite coordinate first moments.
The recourse LP is represented as a separate reusable definition with free , constraints , and dual feasibility , . Statements using its real value require primal and dual feasibility. Theorem 2 states primal feasibility on the support at its chosen ; Theorem 1 uses relative complete recourse on ; Theorem 4 uses complete recourse for every right-hand side. Theorems 1 and 4 also state dual feasibility explicitly because primal feasibility alone does not ensure it. Assumption 1 is explicit in both, including equality between its cone representation and the previously defined . Its bound means strict inequality in every auxiliary coordinate, and strict cone feasibility means membership in the interior of the product cone.
The values , , , and (9) lie in the extended reals. Each printed “min” is an infimum, and no optimizer is presumed. A value is never formed by subtracting infinities. The SOC support, the epigraphs, and all rule feasibility conditions retain their pointwise meanings. Neither an empty ambiguity set nor an impossible rule class is silently replaced by a favorable real default. Contributions to LP value regularity, integrability, moment duality, and SOC geometry are all useful beyond this mission. The goal must continue to compare the original with the actual lifted-rule value ; replacing either by an easier surrogate would remove its content.
How much of relativity is already contained in Hamiltonian particle mechanics? The note by Carcassi and Aidala argues that the metric tensor need not be postulated as a property of space-time: it emerges as the linear relation between the conjugate (kinetic) momentum of a particle and its velocity, . Writing the symplectic form in position–momentum or position–velocity variables, the metric and the electromagnetic force tensor appear as components of the symplectic structure, and the geodesic equation with the Lorentz force falls out of Hamilton's equations.
Space-time is a single coordinate chart with coordinates ; phase space is with canonical coordinates , , and canonical Poisson bracket . The data are
The kinetic momentum is , the velocity , and the Hamiltonian (extended phase space) is ; it generates the evolution along the affine parameter . Christoffel symbols are and . The note also introduces the symbol , which appears in the symplectic form in position–velocity variables.
as an identity of functions on phase space, where . Hamilton's equations alone, with no geometric postulate, yield the covariant Lorentz-force law.
The milestones follow the equations of the note: the inverse-metric derivative (2), the brackets of kinetic momenta (8), the position equation (9), the symbol and its raised form (10)–(11), the velocity brackets (13), the position–velocity form of the geodesic equation (14), the antisymmetrized covariant derivatives (15), and the statement that makes the metric a Hessian (16).
The results make precise the claim that the metric and the force tensor characterize the geometry of the tangent bundle as seen by Hamiltonian mechanics. The symbol is not a tensor, and eq. (16) shows that frames with have a Hessian metric; the note ends with the open question of which frames have , and whether such frames exist in curved space-time.
Each statement is a finite computation, but the computations combine the Leibniz rule for the Poisson bracket, derivatives of the matrix inverse, and repeated relabeling of dummy indices. Eq. (16) needs a Poincaré-lemma argument (closed one-forms on are exact), applied twice.
Everything is stated in one global chart (Fin n → ℝ); partial derivatives are Fréchet derivatives along coordinate directions, and all index sums are explicit finite sums. Smoothness of and and nondegeneracy of are standing assumptions (the definition IsSmoothMetric). Phase-space functions are functions of , and is the canonical Poisson bracket , so no flow or ODE solution is needed. The differential-form computations of eqs. (3), (6), (10) and (12), and the transformation law of on p. 8, are not included as targets.
Carcassi, Landini and Aidala (arXiv:2411.00972) argue that classical mechanics is the high-entropy limit of quantum mechanics, in the same way that non-relativistic mechanics is the low-speed limit of relativistic mechanics. The usual mathematical recipe is reinterpreted as sending the entropy of pure states to , i.e. as . The paper backs this with explicit formulas: Gaussian entropy–uncertainty curves, the black-body spectrum, the trace identity for the maximally mixed state, classical and quantum "stretching maps" on phase space, and a Lindblad master equation that implements the quantum stretch. This mission formalizes those mathematical claims.
We use one degree of freedom with phase space .
The goal (Section 4.3, Fig. 3, p. 11): for all and ,
This is the quantitative form of "taking is equivalent to ": the quantum Gaussian entropy curve converges to the classical one.
Milestones, in the order of the paper:
The goal makes the slogan "classical = high-entropy quantum" precise for Gaussian states: the classical entropy–uncertainty law is exactly the limit of the quantum one under the entropy rescaling the paper constructs. The milestones are the computational facts the argument rests on. The paper derives them by hand and none has been machine-checked. Several are reusable well beyond this paper: entropy under scaling of densities, moment scaling under dilations, and the action of the Lindblad generator on anti-normally ordered monomials in the Weyl algebra.
The goal is an asymptotic expansion of at infinity. The naive term-by-term limit has the form and must be organised as a difference quotient or Taylor expansion of . The measure-theoretic milestones need change of variables for the dilation on and , plus careful integrability bookkeeping for . The Lindblad milestone needs the commutator identities and in a noncommutative ring.
Real.log returns at , which agrees with the convention at the Heisenberg point .ℝ × ℝ with Lebesgue measure, and Husimi distributions live on ℂ. Densities are real functions. The entropy milestone assumes , , and integrability of and , i.e. finite entropy, which the paper uses implicitly. The moment identities hold for every function, since an integral that does not converge is on both sides.ℂ-algebra with , and the adjoint of each jump operator is passed explicitly. This avoids unbounded operators. The hypothesis is satisfiable, e.g. by differentiation and multiplication by on . No bounded operators satisfy it, so do not specialise to a C*-algebra.Quantum states are standardly modelled as rays in a complex Hilbert space, following von Neumann's 1932 axiomatisation. Carcassi, Aidala and Calderón (arXiv:2308.06669) examine which parts of this definition can be justified by physical requirements. They argue that the inner product space structure is physically required — it is exactly what is needed to describe statistical mixtures of states and their entropy — while completeness in infinite dimensions is not: it forces the state space to contain states with infinite expectation values, coordinate changes that turn finite expectations into infinite ones, and time evolutions that do so in finite time. The paper suggests Schwartz spaces as a possible alternative.
The physical conclusions of the paper (its Propositions 19 and 31) are arguments, not mathematical theorems. Behind them, however, sits a set of precise mathematical statements in Section VI and Appendix A. This mission formalizes those statements.
Let be a complex inner product space, not necessarily complete. For , is the operator . A finite mixture of pure states is an operator with finitely many unit vectors and weights summing to . The von Neumann entropy of such an operator is over its eigenvalues, and denotes the entropy of the equal mixture .
On the position side, is the Hilbert space of square-integrable complex wave functions. An orientation-preserving diffeomorphism (smooth, strictly increasing, with smooth inverse) acts on wave functions by
which is the transformation law of a wave function under the change of coordinate . The -th absolute position moment of a state is ; finite moments of all orders are the natural minimal requirement for the statistics of position to be well defined.
A unitary transformation of that is nothing but a change of the position coordinate can map a state with all moments finite to one with infinite expected squared position. The goal is stated existentially, leaving the particular change of coordinates free.
The goal makes precise one of the paper's three claims about completeness: being an isomorphism of Hilbert spaces does not respect finiteness of expectation values, even for a transformation as innocuous as a smooth change of coordinates. Propositions 20 and 21 make precise the companion claim that completeness forces the inclusion of states outside the domain of every unbounded observable, and that unitaries do not preserve such domains. Propositions 7–10 make precise the paper's case for the inner product: equivalence of superposition with non-unique decomposition of mixtures, and the entropic meaning of the transition probability.
All statements are mathematically elementary relative to modern functional analysis, and none of them, to the knowledge of the proposer, has a machine-checked proof. Formalizing them pins down hypotheses the paper leaves implicit: two statements needed corrections to be true (see the notes on Propositions 8 and 20).
Most of the work is infrastructure rather than a single hard step. Proposition 24 requires the change-of-variables formula for Lebesgue integrals and a construction of the induced operator on equivalence classes, including surjectivity. Equation (29) requires developing the error function (limits at , smoothness, positivity of its derivative) and differentiating . Proposition 10 requires computing the spectrum of a rank-two operator through the eigenvalue API for self-adjoint operators on a finite-dimensional space. Proposition 20 rests on the closed graph theorem. The moment statements require Gaussian integrability and a comparison of with at infinity.
All statements live in the namespace UnphysicalHilbert. State spaces are complex inner product spaces (InnerProductSpace ℂ H), completeness assumed only where the paper assumes a Hilbert space. Finite sets of states are finite indexed families; a finite-rank density operator is a finite strictly convex combination of pure states. The entropy of the equal mixture is computed on the span of the two vectors, on which the operator acts. is Lp ℂ 2 volume, unitaries are linear isometric equivalences, and finiteness of a moment means Lebesgue integrability of .
Two departures from the text are deliberate and flagged in the item notes: Proposition 8 assumes instead of (the latter admits a counterexample in ), and Propositions 20–21 assume the operator is closed (without some such hypothesis an everywhere-defined discontinuous functional is a counterexample). Proposition 5 assumes the coefficients are nonzero, which its proof uses. The time evolution of eq. (30) and the remarks on Schwartz spaces in Section VIII are not formalized, because the paper does not state them as propositions. The existential goal cannot be satisfied trivially: the operator is pinned to the change-of-variables formula, and must be a unit vector with all moments finite.
Contributions of reusable infrastructure are welcome, in particular: the error function, the unitary on induced by a diffeomorphism, and the spectrum of .
The Hubble constant is the present expansion rate of the Universe. Its value measured locally with distance-ladder methods disagrees with the value inferred from the early Universe under the standard CDM model (the Hubble tension). The H0DN Collaboration (A&A 708, A166, 2026) combined geometric distances, Cepheids, the tip of the red giant branch, Miras, carbon stars, Type Ia and Type II supernovae, surface brightness fluctuations, the fundamental plane, Tully–Fisher relations and megamasers into a single Local Distance Network, reporting the baseline value .
That number comes from one statistical step. All equations of the network are linear (or linearized) in the parameters, the measurement errors are correlated, and the parameters are obtained by generalized least squares with a non-diagonal covariance matrix (Appendix B of the paper). The paper relies on three mathematical facts: the covariance-weighted solution is the Best Linear Unbiased Estimator (Aitken 1935); weighting by the inverse covariance gives the lowest variance among weighted least-squares solutions; and replacing the inverse of a singular covariance matrix by its Moore–Penrose inverse (Penrose 1956) is "completely equivalent to analytically making sure that only linearly independent equations are used". This mission formalizes exactly those facts.
Timeline of the mathematics used:
The data vector has one entry per equation of the network (host-distance, host-group, calibrator and Hubble-flow equations; in the baseline). The parameter vector collects host distance moduli, group distance moduli, reference absolute magnitudes and . The coefficient matrix gives the theory prediction , and the data have covariance matrix .
For a symmetric positive-definite weight matrix the quadratic form of Eq. (B.2) is
and gives the of Eq. (B.1). When has full column rank, the GLS estimator matrix is and the GLS estimate is . A linear estimator has covariance . A matrix is a Moore–Penrose inverse of if , , and and are symmetric.
In the network the equations are built from only distinct measurements ( in the baseline): with the vector of distinct measurements, of positive-definite covariance , and of full column rank. Then is singular whenever .
For with , and of full column rank, the estimate is unbiased, and for every such that is unbiased for every true parameter, and every ,
With the tension between independent measurements:
The result itself. These statements are what makes the reported and its error bar meaningful as statistical quantities: the estimate is unbiased, its reported uncertainty is the covariance , no other linear unbiased combination of the same data is more precise, and the pseudoinverse shortcut used in the public code neither adds nor removes information compared with an explicit reduction to independent equations. The same facts underlie every covariance-weighted combination of correlated measurements.
Formalizing it. All of these results are classical and proved in the statistics literature. This mission adds machine-checked versions stated in the form used by the paper, including the pseudoinverse equivalence of Appendix B.2, which the paper states without proof. The astrophysical inputs (data selection, linearization, the numerical value of ) are outside the scope of formal proof.
Each statement is classical, but the formal versions are not one-liners. The goal connects measure-theoretic expectation, variance and covariance with matrix algebra: variances of linear combinations of square-integrable random variables must be expanded through bilinearity of covariance before a Loewner-order inequality applies. The pseudoinverse equivalence fails without the full-column-rank hypothesis on , and has to handle a singular for which does not exist. Existence of the Moore–Penrose inverse needs a spectral or rank-factorization argument; it is not available as a ready-made matrix operation.
Everything is over with arbitrary finite index types. "Full column rank" is stated as injectivity of . Positive (semi)definiteness uses Mathlib's Matrix.PosDef / Matrix.PosSemidef, which include symmetry. Mathlib's matrix inverse returns on singular matrices; every statement that uses carries hypotheses under which that matrix is invertible. The Moore–Penrose inverse is a predicate (the four Penrose equations), and the uniqueness milestone makes it a well-defined object. The probabilistic goal assumes only mean zero, finite second moments and a given covariance matrix (no Gaussianity). Unbiasedness of the competing estimator is required for every value of the true parameter, which rules out estimators that are unbiased only at one parameter value.
The numerical items check only the arithmetic from the published central values and uncertainties to the quoted significances and percentages; "rounds to " is stated as (or the corresponding percentage interval). They say nothing about whether the inputs are correct.
The shared definitions (quadratic form, GLS estimator, estimator covariance, Moore–Penrose predicate) can be reused for any weighted least-squares development. Contributions are welcome on all milestones, as well as on a reusable construction of the matrix pseudoinverse.
The rotation curves of spiral galaxies indicate that galaxies sit inside extended dark halos whose mass dominates the visible matter (Faber–Gallagher 1979). If the halo is a gas of elementary particles moving at galactic velocities ( km/s), those particles stream through every laboratory on Earth. In 1985 Goodman and Witten asked whether a detector then being proposed for neutrinos — the superconducting-grain detector of Drukier and Stodolsky, which registers nuclear recoils of tens of eV and up through elastic neutral-current scattering (Drukier–Stodolsky 1984) — could see halo particles by the same mechanism.
Their answer, worked out with a handful of explicit formulas, was yes for three broad classes of candidates: particles with coherent weak interactions, particles with spin-dependent interactions of weak strength (with the photino as the example), and strongly interacting particles. The paper is the starting point of direct dark-matter detection: the recoil-energy kinematics, the counting-rate formula and the split into spin-independent and spin-dependent couplings introduced here are still the standard framework of every nuclear-recoil experiment.
A halo particle of mass and speed scatters elastically from a target nucleus of mass number , mass , at rest. In a non-relativistic elastic collision momentum and kinetic energy are conserved, and the recoil kinetic energy deposited in the nucleus is bounded by
A kilogram of detector contains target nuclei. Halo particles of mass density have number density and flux , so the counting rate with cross section is , quoted in events per kilogram per day. The paper normalises with the reduced cross section .
For a constant invariant amplitude the elastic cross section is
The three candidate classes differ only in (or ):
Standard halo values are g/cm and km/s, and the benchmark detector sensitivity is 1 event/kg/day.
With g/cm and km/s:
The milestones follow the paper's equations in order: the recoil bounds and the 1–2 GeV lower mass limit (p. 3059); the counting-rate formula, Eq. (1); the coherent reduced cross section, Eq. (2), and the resulting /kg day rates; the photino rate, Eq. (3); the quark-model matrix elements, Eq. (4), and the factor-100 flavour asymmetry; and the hard-sphere cross section and rate, Eq. (6).
The result. The paper turned dark-matter direct detection from an abstract possibility into a quantitative experimental programme: it fixed the minimal detectable mass from kinematics, gave a single counting-rate formula into which any particle-physics model can be inserted, and showed that coherent (spin-independent) scattering on heavy nuclei is enhanced by while spin-dependent scattering needs odd nuclei. These estimates set the scale of rates, from events/kg/day for coherent weak particles down to 1 event/kg/day for photinos, against which later experiments were designed.
Formalizing it. The statements are elementary but they are exactly the kind of order-of-magnitude chain where a unit conversion, a missing factor of 2 or , or a convention for the nuclear mass silently changes a number. A machine-checked version records every convention explicitly, checks each printed coefficient against modern values of the constants, and separates genuine theorems (the kinematic bound) from numerical consequences of the formulas.
The only genuinely geometric statement is the recoil bound, which must hold for every direction of scattering in three dimensions, not just head-on collisions. All other milestones are exact identities between the definitions plus verified numerical bounds involving , real powers and scientific-notation constants spanning more than fifty orders of magnitude. The obstacle is keeping these bounds tight enough: several of the paper's coefficients are reproduced only to a few percent, so loose estimates of or of over a range of will not close the inequalities, and the detectability statements require monotonicity arguments over whole mass intervals rather than evaluation at one point.
All quantities are real numbers in a fixed unit system: masses and energies in GeV with , velocities as fractions of in kinematic statements and in cm/s in rate statements, densities in g/cm, cross sections in cm, squared amplitudes in GeV converted to cm by . The constants are , in grams, , and at their modern values, the paper's , and nuclear mass with GeV (the paper writes GeV; the nucleon mass reproduces its printed coefficients).
Approximate equalities "" in the paper are encoded as the existence of an exact coefficient with for which the formula holds identically in all parameters, so a statement cannot be satisfied by a coefficient unrelated to the definitions. "Of order " is encoded as . Eq. (2) is used without the nuclear form factor, as in the paper's sentence about lead; the reduced Table II rates with loss of coherence and Eqs. (5) and (7) are outside the scope of this mission.
The development needs only real analysis from Mathlib: inner-product geometry in for the recoil bound, and bounds on and on real powers for the numerics. Contributions of reusable lemmas for certified numerical bounds on rpow expressions are welcome.
Single-field slow-roll inflation predicts primordial curvature fluctuations that are very close to Gaussian. The leading departure from Gaussianity is the three-point function (the bispectrum) of the curvature perturbation . Maldacena (2003) computed it from first principles: he derived the cubic action for scalar and tensor fluctuations, evaluated the tree-level correlators with the standard choice of vacuum, and gave closed formulas at leading order in slow roll, with exact numerical coefficients and full momentum dependence. For the three-scalar correlator, earlier estimates included only part of the effect.
The paper also points out a structural property. When one momentum is much smaller than the other two (the squeezed limit), the three-point function is fixed by the tilt of the two-point function. Today this is called Maldacena's consistency relation. It is the standard test of single-field inflation against cosmic microwave background and large-scale-structure data, and the starting point of a large literature on soft theorems in cosmology.
Units are . The background is a spatially flat FRW metric with a homogeneous scalar field obeying
and . A starred quantity is evaluated at horizon crossing. Write and . Momentum conservation means that are the side lengths of a (possibly degenerate) triangle. All correlators below are written without the overall factor .
For fixed , as through momentum triangles (which forces ),
This is the statement that "(4.5), with (4.6) goes over to (4.7) in the overlapping region of validity."
The consistency relation ties a three-point observable to a two-point observable with no free parameters. If it is observed to fail, all single-field models in the Bunch–Davies vacuum are ruled out. The shape-function bound in (4.9) is what lets the paper conclude that the local-type of single-field slow-roll models is of order the slow-roll parameters, too small to detect from the CMB alone.
All results here are established physics. As far as is known, none of the explicit formula manipulations, the contour integrals, or the consistency checks between the general and squeezed formulas has a machine-checked proof. This mission produces checked versions of each of them, so that later formal developments of cosmological perturbation theory can cite exact statements rather than prose.
The algebraic limits are elementary once the formulas are written down. The analytic content is in the two contour integrals. The integrand of (4.4) and (4.11) oscillates and does not decay on , so the integrals exist only with the prescription. The integrand of (4.11) also has a non-integrable singularity at , whose divergence is purely imaginary, so only the real part has a limit as the cutoff goes to zero. The shape bound is a degree-zero rational inequality on the triangle region; it is false outside the triangle region.
def with , , and the factor dropped. Background values at horizon crossing enter as real parameters ρd, φd, φdd . At leading order in slow roll, the different horizon-crossing times and that appear in (4.7), (4.12), (4.14), and (4.17) coincide.IsMomentumTriangle. The graviton–scalar–scalar and three-graviton correlators use vectors in EuclideanSpace ℝ (Fin 3) and polarizations as real symmetric, traceless, transverse matrices. A squeezed limit is taken along , .Elko (from the German Eigenspinoren des Ladungskonjugationsoperators) is a class of spin-1/2 fields of mass dimension one, introduced by Ahluwalia and Grumiller (JCAP 07 (2005) 012) as a candidate for fermionic dark matter. Elko spinors are eigenstates of charge conjugation, so they are neutral. Because of their mass dimension they obey only a Klein–Gordon-type equation, and their allowed self-interactions are restricted to a quadratic and a quartic term.
Pereira and Guimarães (2017) propose that one homogeneous Elko field, coupled to gravity in the Einstein–Cartan framework (gravity with torsion) and subject to a symmetry-breaking potential, drives the whole expansion history: inflation, then a matter-dominated era, then late-time acceleration. The paper has two parts. The first is an analytic reduction of the field equations to a closed system of ordinary differential equations (Section 2 and Appendix A). The second is a numerical study of that system with a benchmark set of parameters (Section 3). This mission formalizes the analytic part and the closed-form estimates of Section 3.1.
Units are and . The background is a spatially flat FRW metric with lapse and scale factor . The Hubble rate is . The Elko field is , where is a constant spinor normalized so that . Only the real function carries dynamics. Homogeneity and isotropy leave two torsion functions and . The minisuperspace Lagrangian (A.13) is
Its Euler–Lagrange equations in (gauge ) are (A.14)–(A.17). They force and the torsion relation
Substituting gives the Friedmann equations with torsion (2.2)–(2.3) and the motion equation (2.4). Throughout, the factor appears, and it is always positive. The potential of Section 3 is
Assume (2.5), (2.2) and (2.3) on an open time set , with differentiable there. Then on
and with given by (2.9)–(2.10). Wherever , the motion equation (2.8) also holds:
The result itself. The reduced system (2.6)–(2.10) is the object the paper integrates numerically for every cosmological era. In the limit it differs from the standard single-scalar-field equations (1.1)–(1.3) only by the factor and by the torsion term in (2.8). That term acts like the friction term that is added by hand in reheating models. The identification of and in (2.9)–(2.10) is what defines the equation-of-state parameter , which the paper uses to argue for dust-like behaviour after inflation.
Formalizing it. The paper says the reduction is reached "after some algebraic manipulations" and does not show them. A formal proof checks every coefficient of (2.2)–(2.10) and of (A.14)–(A.17) against the Lagrangian (A.13). It also makes explicit the condition that is needed to recover the motion equation from the Friedmann equations. The numerical claims of Section 3.1 are closed-form evaluations and can be checked exactly.
The identities are elementary, but they are not purely pointwise. Equation (2.3) contains on both sides, through , and itself depends on and . Solving for therefore requires differentiating (2.5) along the trajectory. This is valid only because (2.5) holds on an open set of times, not just at one instant. Similarly, deriving (2.4) means differentiating the constraint (2.2) in time and cancelling a factor . The Euler–Lagrange milestone needs partial derivatives of in each of its slots, composed with time derivatives along the trajectory. A careless treatment of which arguments are frozen gives wrong coefficients.
All objects are real-valued functions of time . Time derivatives are Mathlib deriv, and hypotheses are imposed on an open set . Partial derivatives of the Lagrangian are deriv in one argument with the others fixed at their trajectory values. The constant is an arbitrary real number; is assumed only where appears. The spinor structure of Elko is not modelled: as in the paper, only the scalar amplitude enters. The symbol "" in Section 3.1 is encoded as agreement within relative error.
Out of scope: the derivation of the Lagrangian (A.13) from the Einstein–Cartan action (A.1)–(A.12); the slow-roll approximations (3.2)–(3.5), which the paper states only as approximations in the regime ; and every output of the numerical integration of Section 3 and Appendix B, such as e-folds, the late-time behaviour, the oscillation of around , and the present-day density.
A trivializing formalization is ruled out: the torsion function is constrained by (2.5) on all of , and are fixed by (2.9)–(2.10), not left free.
Infrastructure needed: only basic one-variable calculus in Mathlib (deriv, DifferentiableAt, product and quotient rules), together with field arithmetic using the positivity of . The same reduction pattern (eliminate an algebraically determined auxiliary field, then differentiate a constraint) occurs in other torsion and scalar–tensor cosmologies.
The Hubble constant is the present expansion rate of the universe. It is the slope of Hubble's law , which relates a galaxy's recession velocity (km s) to its distance (Mpc). Two families of measurements currently disagree. Local, distance-ladder measurements calibrated with Cepheid variables give km s Mpc (SH0ES: , Riess et al. 2022). The value inferred from the cosmic microwave background under CDM is (Planck 2018). Calibrations with the tip of the red giant branch (TRGB) fall in between: (Freedman 2021). This disagreement is the Hubble tension. If it is real, it points to physics beyond CDM.
The review Freedman & Madore 2023 surveys this landscape and makes a series of quantitative claims about it. Some are agreement or disagreement claims ("agrees at better than ", "differs at the level"). Others convert magnitudes to distances ("a 1.5% measurement", "corresponds to a 6% shift in "). The central one, in §10, is a sensitivity argument: the claimed tension falls below if the local uncertainty has been underestimated by a factor of about . This mission takes these claims literally and checks them against their stated numbers.
A measurement is reported as . Two independent uncertainties are combined in quadrature, . This is the field's standard convention, used here for a quoted . The tension between independent measurements and , in units of standard deviations, is
The distance modulus of an object at distance parsecs is , and conversely pc (). A modulus difference therefore multiplies distances by . Through Hubble's law, (with in pc), the same difference divides the inferred by .
These are the "" SH0ES–Planck tension, the "less than " for , and the "" for . Every rounded value ("", "") is read as the half-open interval of reals that round to it.
The statements make the review's arithmetic exact and auditable. Each verbal claim of the form "" or "" becomes an explicit inequality under an explicit convention (quadrature, half-open rounding intervals). A reader can then see which claims follow from the quoted numbers and which do not. For example, under the quadrature convention the §4.1 statement that the TRGB value "differs only at the level" from Planck evaluates to about . That claim is therefore not included as a milestone. The definitions (quadrature, tension, distance modulus, Hubble's law) are reusable for any distance-ladder mission. None of these statements has a machine-checked proof yet.
The mathematics is elementary. The difficulty is certified real-number bounds involving square roots and real powers with non-integer , where a careless rounding direction flips a conclusion. Bounds on reduce to comparing with for large . This requires care with exponent sizes, or an analytic bound on / .
All quantities are real numbers (ℝ). Distances are in parsecs inside distanceFromModulus, and hubbleConstant converts to Mpc. Velocities are in km s. Uncertainties are taken at face value as independent Gaussian standard deviations. Statistical and systematic errors are combined in quadrature, and no asymmetric errors are used. A rounded figure is encoded as the half-open interval of values rounding to it. "Better than " is a strict inequality. "At the level" is . Real.logb 10 and Real.sqrt are total functions; every statement uses them only on positive arguments. Solutions should go through the given definitions rather than replacing them with decimal approximations.