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.
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?
Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by . The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most , giving an -approximation.
Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.
An instance consists of a finite type of elements, a finite type indexing available sets, an assignment , and a nonnegative cost . Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are
The frequency of an element is the number of sets containing it, and denotes the maximum frequency over all elements.
The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given covers is strictly stronger than coverability of the family.
Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when is empty, and the -approximation bound reads , which the certificate's tightness clause forces to be rather than anything false.
The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.
A primal-dual certificate is a pair where covers , is dual-feasible, and every has a tight dual constraint, .
For any primal-dual certificate and any fractional cover ,
Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover costs at most times the fractional optimum and a fortiori at most times the integral optimum.
The one substantive step of the goal is split out as its own target: for a primal-dual certificate,
Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most times. With this and weak duality, the goal is two lines.
A greedy certificate at ratio is a cover and a nonnegative with and for every . For such a certificate and any fractional cover ,
Instantiating is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.
Every dual packing is bounded by every fractional cover, ; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.
This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no -approximation result to build on.
The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.
Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.
Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.
This is the second mission in the magic-squares formalization programme, and it takes up the case the first one deliberately left open.
Counting semi-magic squares — arrays of nonnegative integers whose rows and columns all share a common line sum, with the diagonals unconstrained — is the "honest" version of the enumeration problem. For order three the magic count (mission I) is only a quasi-polynomial: it vanishes unless and equals on . The semi-magic count has no such periodicity. MacMahon computed it in 1915:
It is an honest polynomial in of degree , and that degree is not an accident: Ehrhart and Stanley proved that for every order the function is a polynomial of degree satisfying the reciprocity law . The order-three formula above is the smallest nontrivial instance of that theorem, and the only one small enough that every step of the derivation can still be exhibited explicitly.
So this mission is the natural companion to mission I: same objects, same platform vocabulary, but the counting step is genuinely harder — the parameter space is four-dimensional rather than two, and the parametrization is not injective until it is normalized.
Fix and a line sum . A square of order is an array of nonnegative integers.
For the whole family is governed by the six permutation matrices. Split them into the three even ones — the identity and the two -cycles — whose supports are the transversals
and the three odd ones — the transpositions — with supports
Adding them with multiplicities (even) and (odd) gives
whose six line sums all equal ; so this is a semi-magic square of line sum whenever the multiplicities sum to .
This is the goal because it is the weakest statement that still pins down the answer: it asserts the shape of without naming the parametrization, and it survives verbatim as the case of Stanley's theorem that is a polynomial of degree .
sm3_canonical). Every semi-magic
square arises from the display above, and the representation becomes unique
after normalizing: put , , , subtract the
corresponding even permutation matrices, and the residual odd multiplicities
satisfy . The normalization is necessary — without it the
single relationidentifies distinct -tuples — and it is exactly what makes the count a
partition rather than an inclusion–exclusion.
2. Bijection (sm3_bij). The map from normalized coefficient vectors to
semi-magic squares is a bijection, so .
3. Stars and bars (comps_card). The number of -tuples of nonnegative
integers summing to is ; the case is what the
count needs.
4. Evaluating the parameter count (sm3_params_card). Partitioning the
normalized vectors according to the first zero among writes
as
which collapses to by two applications of Pascal's identity.
The result itself. is the case of a theorem that launched a subject: Stanley's proof that counts lattice points in the Birkhoff polytope makes an Ehrhart polynomial, and the order-three formula is the first nontrivial value of it. Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717) revisited exactly this computation on the way to their quasi-polynomial theorem for the magic counts, and Beck and Zaslavsky later pushed the same technique to the panmagic and symmetric refinements. Getting machine-checked therefore validates the whole hierarchy at its base.
Formalizing it. Nothing here is open; the mathematics is a century old. What is missing is the formalized artifact, and the difficulty is concentrated in two places that are formalization difficulties rather than mathematical ones.
First, surjectivity of the permutation-matrix parametrization. The usual proof quotes Birkhoff–von Neumann, which in turn needs Hall's marriage theorem. For order three one can instead do it by hand: subtract the three even transversal minima and show that the residual satisfies . That last step is a six-case argument in linear arithmetic — if then each of the three ways for the transversal to have minimum zero forces — and it is precisely the kind of step that is invisible on paper and must be made explicit in a proof assistant.
Second, the counting step. The parameter set is a filtered finset of
functions Fin 6 → Fin (t+1), while the formula is stated with binomial
coefficients over . Connecting them requires stars-and-bars, proved
from scratch (by induction on the number of parts plus the hockey-stick
identity), because the available library results count sub-multisets rather
than compositions. And the final collapse to MacMahon's form is a chain of
Pascal identities that must be applied in the right order to stay inside
, where subtraction is truncated.
Two traps deserve to be named.
Uniqueness needs the normalization. The representation by six multiplicities is not injective: . Any formalization that counts -tuples directly will overcount, and the correction is not a subtraction but a choice of canonical representative. Deciding "first zero among " is what turns the count into a genuine partition.
Truncated subtraction. The decomposition is expressed over , so every identity — in particular the recovery of the multiplicities from a square — must be stated with the admissibility inequalities as explicit hypotheses. A truncated subtraction is only correct because normalization forbids the truncation, and that side condition has to be discharged rather than assumed.
Fin n; semiMagicCount n t is the cardinality of a
finset of arrays over Fin (t+1) — lossless, since every entry is at most
.Counting magic squares — arrays of nonnegative integers whose rows, columns and two main diagonals all share a common line sum — is one of the oldest problems in enumerative combinatorics, and the testing ground on which the general theory was built. MacMahon computed the order-three count in 1915 by hand; sixty years later Stanley, and then Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717), showed that for general order the counting functions are quasi-polynomials in the line sum, by identifying them with Ehrhart quasi-polynomials of rational polytopes. The order-three case is the oldest nontrivial instance of that theory and the one where every step can still be checked by hand.
The subject therefore has a curious status: the enumerative answer for has been known for over a century, and the structural facts behind it (a magic square is determined by two corner entries; opposite cells sum to twice the centre) are folklore — but none of it has a machine-checked proof. This mission formalizes the classical derivation end to end.
Fix an order and a type of entries. A square of order is an array with entries in ; its row sums, column sums, and the two diagonal sums (main and anti-diagonal) are the sums of the entries along those lines.
No distinctness of entries is required. Let denote the number of semi-magic and the number of magic squares of order with nonnegative integer entries and line sum . Every entry of such a square is at most , so these are finite counts.
For the whole family is parametrized. If has line sum then the centre cell equals , and writing and the eight line identities force
All nine entries are nonnegative exactly when
and substituting , turns these into : the ball of radius in .
together with the companion vanishing when . This is the count of magic squares of line sum with nonnegative integer entries (entries need not be distinct). It is the goal because it is the weakest stable statement: it asserts only the shape of the answer, not the intermediate parametrization, and it survives verbatim as the case of the general quasi-polynomial theorem.
That the map is a bijection from the magic squares of line sum onto the admissible parameter pairs, and that the latter are counted by the -ball cardinality. This is the route the mission actually takes; the count is its corollary.
, the analogous count for semi-magic squares, is a genuinely different and harder quasi-polynomial. It is listed as a stretch target, not a milestone.
The result itself. MacMahon's formula is the base case of the Ehrhart-theory reading of magic-square enumeration; Beck--Cohen--Cuomo--Gribelyuk's quasi-polynomial theorem for general degenerates to it at , so it is the sanity check any generalization must pass. The parametrization behind it is what makes the "how many" question finite-dimensional at all: it reduces a search over arrays to a count of lattice points in a two-dimensional ball. Downstream, the same parametrization governs the classification of normal magic squares (the Lo Shu square and its symmetries) and the associativity identity .
Formalizing it. The mathematics is classical and proved; nothing here is
open. What is missing is the formalized artifact. The order-three structural
lemmas — the centre identity, the opposite-cell identity, and the two directions
of the parametrization — are already machine-checked on this platform. The
remaining work is the counting step: exhibiting a concrete bijection between
two finsets whose elements live in different types (arrays over Fin (3e+1)
versus pairs of naturals) and evaluating a finite sum. That is where the
formalization, not the mathematics, is hard.
The obvious attack — "each magic square is determined by , so just count
the pairs" — fails at exactly one point, and it is not a mathematical point. The
counting function is defined as the cardinality of a finset of arrays with
entries in Fin (3e+1) (a finite type, so that Finset.univ exists), whereas
the parametrization lives over . Proving the counts agree therefore
requires a honest Finset.card_bij in both directions:
mkMagic3 from an admissible pair, coerce every entry into
Fin (3e+1) using the bound , and show the round trip is
the identity.Neither direction is deep, but the coercions are unforgiving: a truncated
subtraction in mkMagic3 is only correct because admissibility forbids the
truncation, and that side condition must be discharged explicitly rather than
assumed. The second difficulty is the cardinality of the ball: the
identification needs the elementary identity
, after which the count is
.
Fin n; the anti-diagonal uses Fin.rev, and broken
diagonals use addition modulo . Counting functions are cardinalities of
finsets of arrays over Fin (t+1) — lossless, since every entry is at most
— and return natural numbers.mkMagic3 is defined over with truncated subtraction. Every
row/column/diagonal identity therefore carries the admissibility inequalities
as explicit hypotheses; no identity is asserted unconditionally.Square, IsSemiMagic,
IsMagic, IsPanMagic, IsAssociative, IsNormal, magicConstant, and the
four counting functions ), the symmetry/affine toolbox, and
the order-three structural lemmas. Contributions are welcome on the
semi-magic count , on panmagic and associative refinements, and on the
extension to general .An online algorithm must commit to decisions before it knows the rest of its input, and it is judged by competitive analysis: the ratio between its cost and the cost of an optimal solution computed with full knowledge of the input. A recurring obstacle in this area is that each problem seems to need its own ad hoc potential-function argument. Buchbinder's thesis develops a single method that replaces those arguments — formulate the offline problem as a covering linear program, let the online algorithm raise the dual variables of its packing dual, and read the competitive ratio off the ratio between the primal and dual increments. The same recipe then yields algorithms for online set cover, weighted caching, ad-auction revenue, routing, and load balancing.
This mission formalizes the chapter where the method is introduced on its smallest example, the ski-rental problem. A customer needs skis for an unknown number of days: renting costs per day and buying costs once. The customer must decide, each morning, whether to rent again or buy, without knowing how many ski days remain. Despite its size the problem is the canonical rent-or-buy dilemma, and it has two classical tight results: a deterministic -competitive algorithm, and a randomized algorithm whose competitive ratio tends to , due to Karlin, Manasse, McGeoch and Owicki (1994). The primal-dual derivation of both is the content of Chapter 3.
An instance is a pair : the purchase price , a positive integer, and the number of ski days, which the online algorithm does not know. An offline solution either buys at once, paying , or rents on every day, paying ; so the offline optimum is
Chapter 3 casts this as a linear program (Figure 3.1, p. 18). The primal is a covering program with one buy variable and one rent variable per day :
Its dual is a packing program with one variable per day:
The online structure enters in a single way: a new ski day appends a new covering constraint to the primal and a new variable to the dual, and previously raised primal variables may never be decreased. That monotonicity is what "previous decisions cannot be regretted" means formally.
The fractional primal-dual algorithm maintains , initially . On each new day, while it sets , then raises
and sets ; once has reached it does nothing further. The free parameter is then pinned to the value that makes reach exactly after days,
The coefficient is the exact finite- ratio , left in closed form rather than replaced by a constant. This is deliberate: increases to , so and therefore for every finite . A goal asserting -competitiveness at finite would be false, and a goal asserting some rounded constant would be invalidated by any sharpening. The closed-form coefficient is the weakest statement that is stable under improvement.
The classical constant is recorded here, as a limit of the coefficient sequence, and nowhere else.
Chapter 3's other result, independent of the fractional development.
The ski-rental bounds themselves are classical and tight, and nothing here is mathematically open. What the chapter contributes, and what this mission captures, is the derivation: it is the template instantiated by every later chapter of the thesis, so the artifacts built here — a covering/packing LP pair, its weak-duality instance, a monotone online variable with a closed-form growth law, and the primal-to-dual increment ratio as the source of the competitive factor — are the vocabulary in which the rest of the series will be stated.
On status: the mathematics is proved, published, and standard. It is not, to the best of a search of Mathlib at revision 0df444a, formalized — that revision contains no competitive-analysis or online-algorithm framework, no ski-rental development, and no general linear-programming weak-duality theorem. So the work this mission asks for is formalization of a known proof, not new mathematics, and the reusable output is infrastructure that does not currently exist in the library.
The offline problem is trivial, and a newcomer's first move — prove is the optimum and stop — solves the wrong problem. The content is entirely in the online constraint. Three specific places where the obvious argument stalls:
The optimum is never observed. The algorithm's cost must be compared against without being available to it. The comparison is routed through the dual instead: the dual objective the algorithm accumulates is a lower bound on every feasible primal solution, hence on the optimum, and the algorithm's own primal cost is a fixed multiple of that dual objective.
The growth law is piecewise. The update fires only while . Summing the per-day increments therefore does not telescope uniformly: days before reaches contribute each and later days contribute nothing, and the index at which the switch happens is exactly — which is a theorem about the recurrence, not an assumption.
The constant is forced, not chosen. is not a free tuning parameter; it is the unique value for which the geometric sequence hits at , which is in turn what makes the dual solution feasible (). Dual feasibility and the choice of are the same fact.
Conventions this development commits to. The purchase price is a natural number with , because Chapter 3 uses simultaneously as a price, as a day index ("buy skis on the th day"), and as the exponent in ; costs are real numbers, with and coerced. Days are indexed from , so day of the prose is index , and Fin k indexes the days. Real division is total, so ; the hypothesis is what keeps every reciprocal in the development genuine, and without it would evaluate to and the recurrence would collapse to the constant zero sequence. The algorithm's x < 1 guard is part of the formalized definition, not an informal aside: without it the cost would keep growing past day .
A documented discrepancy in the source. The prose on p. 17 relaxes the integer program by letting and each range over ; Figure 3.1 on p. 18 prints only , . This mission takes the prose version, and , as the canonical fractional program, and also records the nonnegativity-only region exactly as printed. Two separate theorems establish that both have least value , so the discrepancy is resolved inside the mission rather than silently chosen. Solvers should note which of the two predicates a given statement uses.
Ruling out a trivializing formalization. The offline optimum is defined independently, as , and is not derived from the algorithm's own behaviour; a separate theorem certifies that this value really is the least attainable objective value of the canonical program, so the goal cannot be satisfied by redefining the benchmark. The goal inequality is also tight — both sides are equal to times the number of days on which — so it cannot be weakened into vacuity without becoming false.
Infrastructure, and what is reusable. The development needs only Mathlib big operators over Fin k, basic real analysis for the limit, and IsLeast. Two items are explicitly infrastructure rather than ski-rental content: the specialized weak-duality theorem for this covering/packing pair, and the Figure 3.1 optimum. Both are candidates for generalization by the later mission on Chapter 2's general linear-programming duality, and a solver who proves the general form there should expect this instance to be derivable from it rather than duplicated.
Out of scope here. The final paragraph of p. 19 rounds the fractional solution into a randomized algorithm by sampling a threshold uniformly and buying on the day whose increment of contains . That step needs a probability space and an expectation argument, and is deferred to the immediate follow-up mission, Primal-Dual Online Algorithms II: Randomized Rounding for Ski Rental. Contributions here should not anticipate it.
Bayesian filtering estimates an unobserved state from measurements arriving over time. A filter combines what the state dynamics predict with what the newest observation says. In neural decoding, for example, the state may describe an intended movement while the observation contains activity from many recorded neurons. The observation can have many more coordinates than the state and need not follow a linear Gaussian observation model.
The Discriminative Kalman Filter (DKF) uses a Gaussian approximation to the state conditional on the newest observation. It combines that approximation with a Gaussian state transition and a correction for the stationary state distribution. The resulting recursion retains a mean vector and covariance matrix. Burkhart et al. developed this construction and proved an asymptotic justification in Theorem 2 of Appendix B.
The historical starting point is the linear Gaussian filter of Kalman (1960). The 2020 DKF paper changes how observation information enters the update and establishes a corresponding approximation theorem. The present mission concerns formal verification of that published theorem.
The state space is for a positive finite dimension . Write for the ordinary multivariate Gaussian density with mean and symmetric positive-definite covariance . Densities and their distances are with respect to Lebesgue measure.
The state model has a matrix and positive-definite covariance matrices satisfying
Its stationary density and transition density are
For an integrable density , prediction gives
The discriminative update combines a previous filtering density with a density for the state given the current observation:
This expression is a probability density when its nonnegative weight has a finite, strictly positive integral. Dividing by is part of the standard DKF under consideration.
For Gaussian inputs with parameters and , define
The DKF step returns mean and covariance when the precision is invertible and the covariance is positive definite. The recursive filter starts from mean zero and covariance , using the current observation's functions and as the Gaussian input mean and covariance. These are the updates in equation (2.7) of the paper.
Fix sequences of probability densities , indexed by positive integers, whose exact normalized updates
are well defined for every index. Fix Gaussian density sequences , a point , and a probability measure . The five assumptions are
Here denotes weak convergence, characterized by convergence of expectations of every bounded continuous real function; is the unit point mass at . The measure need not have a density and may be degenerate.
The main goal is the complete conjunction of Theorem 2's conclusions, with separate milestones for each:
is a well-defined Gaussian density for all sufficiently large .
A sixth milestone is Lemma 1 (DKF equation): the normalized Gaussian-input update has the explicit mean and covariance above whenever valid, and the two input weak limits imply its eventual validity and convergence to . It includes both the exact equation and the asymptotic assertion from the source.
In addition to neurodecoding with intracortical brain-computer interfaces, the DKF has also found applications in optimization and sequential data augmentation (see references). The original study was successfully reproduced by Casco-Rodriguez, et al. in ReScience C.
The inverse stationary density can grow in the tails, so small errors in the input densities do not immediately control the error after division and renormalization. Normalizing constants must remain finite and nonzero. The candidate Gaussian covariance must also become positive definite as a conclusion of the assumptions, rather than through an extra validity assumption imposed at every index.
There is a second distinction between convergence to a point mass and approximation in . Two sequences may concentrate at the same point while retaining different shapes at shrinking scales. The C5 target therefore requires the full approximation argument, beyond the weak-convergence conclusions.
Lean represents states as Fin d → ℝ and covariance matrices as real square matrices. The Gaussian density is the standard determinant-and-quadratic-form formula. The definition of Gaussian PDF includes positive-definite covariance and equality of densities almost everywhere. Thus null-set changes do not constrain the theorem artificially.
Probability density validity explicitly includes nonnegativity almost everywhere, integrability and total integral one. The quantity is an extended nonnegative integral. The update's validity explicitly requires measurable weight and a finite, strictly positive normalizer. Total expressions outside that domain supply no assumed probability interpretation; C3 establishes validity on a tail.
All density sequences use positive integer indices. The limit measure is a Mathlib probability measure. Weak convergence is tested against Mathlib bounded continuous functions using the actual measures generated by the densities. The stationary model, standard recursive DKF, exact update and approximate update are defined independently of the theorem conclusions.
The mission addresses deterministic Theorem 2 of Appendix B. The random-sequence extension in Remark 4, conditions implying a Bernstein–von Mises theorem, and induction over filtering time are separate developments. The proof plan follows the appendix through C1–C2, Lemma 1, C3–C4, and the five-term comparison for C5.
A foundation model trained on tokenized electronic health record (EHR) timelines can be used to predict clinical outcomes without ever being finetuned for a specific prediction task: condition the model on a patient's observed timeline, autoregressively sample many possible futures, and report the fraction of sampled futures in which the outcome of interest occurs. This generative approach to inference powers a growing family of EHR foundation models— including Event Stream GPT (McDermott et al., 2023), Foresight (Kraljevic et al., 2024), ETHOS (Renc et al., 2024), and Curiosity (Waxler et al., 2025)—and it is attractive for its zero-shot approach to predicting a variety of outcomes.
It is also expensive. Reproducing one published pipeline required more than A100 GPU-hours of inference. Worse, the estimator built from sampled futures takes values in , so its resolution is tied to the sampling budget: for an outcome of prevalence , sampled futures fail more than of the time to rank a patient at ten times average risk above an average one. The most consequential clinical decisions turn on exactly such low-prevalence, high-impact outcomes.
Solo et al. (arXiv:2602.03730) observe that Monte Carlo discards almost everything the model produces: at every step the model emits a full next-token distribution and the sampler keeps only the token it drew. The paper introduces two estimators that consume the discarded probabilities instead, and proves that doing so costs no bias and—for one of them—never costs variance.
Let generate token sequences from a countable vocabulary , with designated outcome token . The next-token probabilities may depend on the complete preceding history. The time threshold is initially unexceeded. Its crossing may depend on several kinds of time-spacing tokens and on their accumulated duration.
For a sampled timeline , is the first position occupied by , or if it never appears. The time is the first position at which the threshold has been exceeded. Assume almost surely. Timelines are retained through the actual threshold crossing, even if the outcome appears earlier. Thus is not reassigned after an outcome.
The threshold is reached almost surely, but the number of tokens required may be arbitrarily large. No deterministic bound or finite expected token count is assumed. For REACH, assume also that removing the outcome token and renormalizing defines a sampler that reaches the same threshold almost surely.
For independent original timelines, the Monte Carlo estimator is
The SCOPE estimator is
For REACH, sample independent outcome-free timelines by setting the next-token probability of to zero and renormalizing the probabilities of the other tokens. Using the original model probabilities along those timelines, define
The targets are:
Expectations and variances use each estimator's specified sampling law.
The claims concern the probability assigned by the generative model. They provide unbiasedness and a comparison of sampling variance. SCOPE is kept unclipped, as in the paper's unbiasedness result. All five target statements have accompanying local Lean proofs.
A pathwise finite stopping time need not have a common finite bound or a finite mean. An expectation involving the stopped SCOPE sum therefore needs justification beyond finite-sum linearity. REACH uses a different sampling law, so its unbiasedness and variance comparison also require a proved connection between the original event and the two-stage experiment. The equal-probabilities milestone records that connection explicitly.
Lean represents each sampled timeline by a finite list ending at its first threshold crossing. Arbitrary finite lengths are included in the same sample space. Path probabilities are products of next-token probabilities, and the laws are countable sums of these path masses. Requiring each law to have total mass one expresses almost-sure termination of that sampler; it is not a uniform length bound. The vocabulary can be finite or countably infinite.
The stopping predicate examines a complete prefix and is not restricted to a single terminal token. The original law continues through outcomes until the threshold. A separate almost-everywhere hypothesis excludes equal outcome and threshold times. The code proves that the actual threshold time is finite almost surely and that the strict event is the event used by the internal calculations.
The two-stage experiment explicitly samples conditionally independent Bernoulli trials using the original hazards. Its conditioning information retains the complete indexed pool of outcome-free timelines. The Rao–Blackwell target uses Mathlib's conditional expectation. The variance target uses Mathlib's variance, and proves square integrability rather than assuming it.
Essentially every quantitative model written as a rate of change — a mechanical system, a chemical reaction network, a population model, a control loop — is an ordinary differential equation (ODE) together with an initial condition. Before anything can be computed about such a model, two questions must be settled: does a solution through the given initial state exist, and is it the only one? The classical answer is the Picard–Lindelöf theorem: a Lipschitz right-hand side yields a unique local solution. Uniqueness is not a technicality — it is what licenses speaking of the trajectory through a point, hence of a flow, and so it underwrites the entire qualitative theory of dynamical systems that the source text builds afterwards (vector fields, tubular flow, -limit sets, Poincaré–Bendixson, Grobman–Hartman, stable manifolds).
This mission is the first in a series formalizing Augusto Armando de Castro Júnior's lecture notes Curso de Equações Diferenciais Ordinárias (2009), a graduate ODE course that develops the theory directly in Banach spaces, not only in . The book proves existence and uniqueness once, in that general setting, and then reuses it throughout; this mission formalizes that foundation.
Let be a real Banach space, , , and . Write for the closed ball and
A map is Lipschitz with respect to the second variable with constant if
the same serving for every (Definição 2.1.1 of the source).
Given , the Cauchy problem (initial value problem) with initial data asks for a curve , defined on a nondegenerate interval , such that for all , , and for all — one-sided derivatives at the endpoints of (Definições 1.0.1 and 1.1.1). Equivalently, by the Fundamental Theorem of Calculus, is continuous with graph in and satisfies the integral equation
Finally, put and .
The goal theorem is Teorema 2.1.2 (Picard) of the source: if is continuous, bounded, and Lipschitz in the second variable, then the Cauchy problem , has a solution on , and any two solutions on that interval whose graphs stay in coincide there:
The milestones are the results the source uses to get there, in its own order: the contraction fixed point theorem (Teorema 0.2.10), the equivalence between the Cauchy problem and the integral equation (Capítulo 2, opening paragraphs), the sufficient condition for Lipschitz dependence via a bounded partial derivative (Proposição 2.1.4), and the global version on a whole interval (Corolário 2.1.3).
Picard's theorem is what makes the initial value problem well posed in the sense of Hadamard's first two requirements. Downstream in the same book it is the hypothesis behind maximal solutions and the escape-from-compacts property (§2.3), continuous and differentiable dependence on initial conditions and parameters (Chapter 3), and the local flow of a vector field (Chapter 4). Without uniqueness none of these statements can even be phrased.
As for formalization status: Mathlib already contains a Picard–Lindelöf development
(IsPicardLindelof, ODE_solution_unique and relatives) and a Banach fixed point theorem
(ContractingWith.exists_fixedPoint). The work this mission asks for is therefore not the
discovery of a proof but a faithful bridge: stating the source's hypotheses as the source states
them — a closed ball, a supremum bound , the radius , Lipschitz in the
second variable with one constant for all times, uniqueness among solutions whose graph stays in
the domain — and deriving them from, or proving them alongside, the library's own formulation.
Such bridges are where unfaithful formalizations usually hide, and they are reusable by every
later mission in the series.
The obvious route is "cite the library and close the goal". It does not go through unchanged, for three reasons. First, the hypothesis shapes differ: the library packages its assumptions in a structure with its own choice of ball, bound and time radius, and matching with a supremum-defined requires the boundedness argument to be redone at the interface. Second, uniqueness here is asserted for solutions in the sense of this mission's definition — derivative within the interval, one-sided at the two endpoints, graph inside — so a Grönwall-type uniqueness statement must be transported to that formulation, including the endpoint cases. Third, the source works with an arbitrary Banach space and only assumes bounded, rather than assuming finite dimension; compactness arguments are unavailable by design.
The remaining genuine mathematical content sits in the milestones: the iterate estimate used by the source to make some iterate of the Picard operator a contraction, and the mean value inequality on a convex open set behind Proposição 2.1.4.
Conventions this proposal fixes, all visible in the definitions item:
A complete development needs the Bochner and interval integrals, the contraction mapping API, the mean value inequality for Fréchet derivatives, and the ODE files. Contributions of independent interest to the series: the Picard iterate factorial estimate, and the conversion between the library's Picard–Lindelöf hypotheses and the ones above.
Mathlib/Analysis/ODE/PicardLindelof.lean and Mathlib/Analysis/ODE/Gronwall.lean,
https://github.com/leanprover-community/mathlib4.In 1918 Emmy Noether published Invariante Variationsprobleme (Nachrichten der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Math.-phys. Klasse, 235–257), answering a question raised by Hilbert and Klein about the status of energy conservation in the general theory of relativity. The paper proves two theorems that tie the symmetries of a variational integral to structural properties of its Euler–Lagrange equations: continuous symmetries depending on finitely many parameters produce divergence identities ("conservation laws"), while symmetries depending on arbitrary functions produce identities among the Euler–Lagrange expressions themselves, so that some of the field equations are consequences of the others. The first theorem is the source of the correspondence between time translation and energy, space translation and momentum, rotation and angular momentum; the second underlies the Bianchi-type identities of generally covariant theories and the gauge identities of field theory.
This mission formalizes the two theorems of §1 of the paper, together with the chain of identities of §2 and §3 by which Noether derives them, in the case of first-order Lagrangians.
Fix integers (independent variables), (dependent variables). Points of the base are , and a field is a map , written componentwise . Write for the derivative of a scalar function on along the -th coordinate direction, and
for the divergence of a vector field on .
A Lagrangian is a function of the point , of the field value , and of the array of first derivatives . Along a field one writes , and the integral under study is . The momenta are
and the Lagrange expressions — the left-hand sides of the Euler–Lagrange equations — are
An infinitesimal transformation is given by generators on the independent variables and on the dependent ones. Noether's equation (9) replaces them by the variation at fixed ,
and the corresponding variation of the Lagrangian is
Two vector fields organise the boundary terms: the partial-integration vector of equation (3), and Noether's
Invariance of enters through Noether's equation (11), the pointwise identity
which the paper derives in §2 from the vanishing of over every region.
The goal theorem is Theorem I of the paper, in the first-order case, in the form Noether states as equation (13). Given generators , , each satisfying the invariance identity (11) with its own from (9), one has for every and every
The milestones are the intermediate statements of the paper, in the order in which it proves them: the central identity (3), the passage from the invariance of the integral to the pointwise identity (11), the single-generator divergence identity (12), the conservation law on solutions of the Euler–Lagrange equations (§3), the converse of Theorem I (§3), and Theorem II in the form of the dependency relations (16) for a group depending on arbitrary functions entering to first order.
Theorem I is the general statement behind every "first integral from a symmetry" argument in mechanics and field theory; Theorem II is the statement that a variational theory invariant under a group of arbitrary functions has field equations that are not independent — of them follow from the rest — which is the group-theoretic form of the failure of a proper energy conservation law in general relativity that Hilbert had asserted. The two theorems are used constantly and stated loosely; a formal version fixes exactly which hypotheses are needed and what the conclusion says.
Mathlib contains the differential-calculus and measure-theoretic infrastructure used here (Fréchet derivatives, integration on , compactly supported test functions, and the standard vanishing lemma for locally integrable functions tested against smooth compactly supported functions), but no calculus of variations: there is no Euler–Lagrange operator, no first-variation formula, and no Noether theorem. This mission supplies the first-order, finite-dimensional-base version of that material, with definitions that later missions (higher-order Lagrangians, the -th order identity (6), mixed groups) can extend.
The algebraic core — the central identity (3) and the passage to (12) — is a product rule plus a reindexing, and the real work is elsewhere.
Two steps are genuinely analytic. First, Noether's inference from "the integral of the integrand vanishes over every region" to "the integrand vanishes pointwise" (equations (10)–(11)) requires the regularity of the integrand to be used explicitly. Second, Theorem II's equation (16) requires integrating by parts against an arbitrary function and then applying the fundamental lemma of the calculus of variations in : the arbitrary functions of the group must be specialized to compactly supported test functions before the boundary terms can be discarded.
The remaining difficulty is bookkeeping: every statement must carry the differentiability hypotheses that make each derivative in it meaningful, since in Lean an undefined derivative silently evaluates to zero rather than failing.
The formalization is in the first-order setting: the Lagrangian depends on , on , and on the first derivatives of only. The base is with fixed but arbitrary, and fields are globally defined maps ; no boundary conditions, no manifolds, and no jet bundles are used. The group is not formalized as a group: as in §2 of the paper, only its infinitesimal generators , enter, and the invariance hypothesis is Noether's identity (11). The linear independence of the divergence relations, which Noether argues from the essentiality of the parameters, is not part of the formal statements.
Derivatives are Fréchet derivatives: is the derivative of at applied to the -th standard basis vector, and partial derivatives of the Lagrangian are derivatives of the corresponding partially applied function. Because Lean's derivative operator returns at points of non-differentiability, each statement carries explicit differentiability hypotheses for exactly the functions whose derivatives it mentions; a solver may not assume more.
The statements are not vacuous: the hypotheses of every milestone are satisfied, for instance, by smooth Lagrangians and smooth fields, and the invariance hypothesis (11) is satisfied by the classical examples (a Lagrangian independent of with , ). Degenerate parameter values are admitted and behave as expected: for or the sums are empty and the identities reduce to , and for the goal quantifies over an empty index set.
Contributions of independent interest that this mission would welcome: a reusable statement of the fundamental lemma of the calculus of variations on in the form needed for (16), and the higher-order analogue of the central identity, Noether's equation (6).
Transformer sequence models modulate attention scores by a function of the relative position between a query and a key: the attention logit between token and token is scaled by a fixed profile . Realizing this modulation the naive way means evaluating once per pair and materializing an adjustment over the whole sequence — quadratic in the sequence length . Rotary Position Embedding (RoPE) Su et al. 2021 avoids this entirely: it rotates the query at position and the key at position independently, each by an angle depending only on its own position, so that the pairwise quantity falls out of the dot product of the two separately rotated vectors — is never evaluated pairwise, and no matrix is ever built. This is what lets RoPE stay a linear, per-token preprocessing step compatible with efficient (sub-quadratic) attention implementations, rather than an modulation. The catch is that RoPE's specific log-linear frequency schedule bakes in one particular profile: a monotone, decaying . That schedule is a poor fit whenever the correlation structure of the data is not monotonically decaying with distance — the leading example being periodicity: in sequential recommendation, interactions separated by exactly one day or one week are more correlated than interactions separated by, say, half a day, and a decaying profile cannot express that "attention comes back" at the period.
Chen, Ainslie, Choromanski et al., ClockRoPE: Random Fourier Rotations for Temporal Routine Modeling (arXiv:2607.26369), ask a more general question first: which attention-modulation profiles can be realized at all by this same per-token, pairwise-iteration-free rotation trick — rotate each token once, on its own, and let the pairwise profile emerge from the dot product — and by what rotation-frequency schedule? Their answer is a random-features construction — sample the rotation frequencies from the kernel's own Fourier transform, rather than fixing them log-linearly — that realizes any continuous, normalized, positive-definite profile in expectation, with a quantified concentration rate, all while keeping the exact same per-token rotate-then-dot-product computation RoPE already uses. ClockRoPE is the periodic instance of this general theory, later deployed in a production-scale generative-retrieval system.
Fix an embedding dimension and group a vector into consecutive feature pairs for . For an angle , let
be the (Givens) rotation matrix. A real kernel is positive definite if for every finite family of points and complex coefficients , has nonnegative real part; it is normalized if . When is also continuous and Lebesgue-integrable, its Fourier transform
is (by Bochner's theorem) a genuine probability density on : this is the distribution the mission's rotation frequencies are sampled from.
Given a query at position , a key at position , and i.i.d. frequencies , the Random Fourier Rotation (RFR) estimator is
is exactly the modulated attention logit computed by rotating query/key feature pairs with per-pair, sampled RoPE frequencies — the same operation standard RoPE performs, but with drawn from instead of fixed by a log-linear schedule.
for every . This is the mission's central target: it upgrades the mean identity below into a quantitative, non-asymptotic guarantee that the sampled estimator is close to the target profile with high probability, at a rate that is exponential in the embedding dimension .
The expectation identity that the concentration bound above sharpens; it is the feasibility half of the claim ("this construction is correct on average") that the convergence half needs as its starting point.
For a continuous, positive-definite, -periodic with and Fourier coefficients ,
The periodic specialization needed to apply the goal and first milestone with a discrete frequency distribution over harmonics — the regime ClockRoPE actually deploys, since daily/weekly routines are periodic rather than merely decaying.
The result gives a general recipe — sample, don't hand-design — for turning any admissible attention-modulation profile into a RoPE-compatible rotation schedule, with a concentration guarantee that says how many feature pairs are needed before the sampled schedule reliably approximates the target profile. Crucially, the recipe changes only which frequencies the per-token rotation uses — it never touches the computational shape of RoPE itself: each query and key is still rotated once, independently, by an angle depending only on its own position, and the target pairwise profile is still recovered purely from the dot product of the two rotated vectors. So realizing an arbitrary positive-definite this way costs exactly what realizing RoPE's own log-linear profile costs — linear in the sequence length, with no pairwise evaluation of and no matrix ever materialized — rather than the quadratic cost a direct, per-pair implementation of an arbitrary modulation function would require. This subsumes standard RoPE's log-linear schedule as one instance and explains, via the periodic corollary, why a schedule built from the kernel's own spectrum (rather than an arbitrary log-linear one) is the right way to encode periodicity: nothing about the construction, or its efficiency, is specific to decay. The paper reports this translated into measured gains in a production-scale generative-retrieval system, which is unusual weight of practical evidence behind a Bochner/Herglotz-style spectral argument.
At the time of writing, none of these three results have a machine-checked proof; this mission asks for the first formalization of all three, together with the shared scaffolding (feature-pair extraction, the rotation estimator, and the notion of a positive-definite kernel) they are stated over.
The natural first attempt at the concentration bound is a direct union bound or a naive variance argument, but the estimator is a sum of terms that are each bounded (each rotated pair lies on a fixed-radius circle) rather than governed by a variance bound that shrinks with under a fixed frequency; the source proof instead applies McDiarmid's bounded-differences inequality, treating each sampled frequency as one coordinate of the input and bounding the one-coordinate change in by via the maximal distance between two points on the unit circle — not by directly bounding a variance term. Establishing Proposition 3.1 itself already requires care: it requires justifying that , defined purely as an integral transform of , is in fact a legitimate probability density (Bochner's theorem), and then a real/complex bookkeeping argument identifying the real inner product of rotated pairs with the real part of a product of complex exponentials.
The mission works over the reals and represents feature pairs as functions
Fin (2 * n) → ℝ sliced into Fin n-indexed pairs, matching the " feature pairs,
dimension " convention used throughout; rotations are ordinary
Matrix (Fin 2) (Fin 2) ℝ values built with Matrix.mulVec/Matrix.dotProduct, and
expectation over i.i.d. -distributed frequencies is formalized as integration
against the product measure MeasureTheory.Measure.pi of n independent copies of
the measure with density (MeasureTheory.Measure.withDensity) — this is
mathematically equivalent to, and more directly usable in Lean than, introducing an
abstract probability space with named i.i.d. random variables.
Since a general continuous positive-definite kernel need not have an
integrable Fourier transform (the periodic case in Corollary 3.3 is exactly the
counterexample: its "Fourier transform" is a discrete measure, not a density) — the
goal and first milestone add Integrable f as an explicit hypothesis beyond what the
paper states in prose, so that is genuinely a density rather than a junk value.
This is not a strengthening of the target profiles the paper cares about in practice
(Gaussian, Laplace, and the cosine/Gaussian priors used by ClockRoPE itself are all
integrable) and mirrors the paper's own split between the density case (Propositions
3.1–3.2) and the discrete, purely-periodic case (Corollary 3.3). A formalization that
dropped this hypothesis and instead let the Fourier integral silently evaluate to
Lean's junk value (0 for non-integrable integrands) would make the goal statement
possible to "prove" vacuously and must be avoided.
Definitions needed: a positive-definite-kernel predicate, the real-valued Fourier transform of a kernel, feature-pair extraction, the rotation matrix, and the RFR estimator itself — all reusable by any future mission formalizing RoPE-family positional encodings (e.g. STRING, nD-RoPE) or other random-Fourier-feature results. McDiarmid's inequality, if not already in Mathlib in the needed form, is itself a independently reusable contribution.
An o-minimal structure is a setting in which every definable subset of the line is tame: a finite union of points and open intervals. This single axiom rules out oscillation, space-filling behavior, and other pathologies, and it makes one-variable definable functions tractable. The central consequence is the Monotonicity Theorem: every definable function on an interval is piecewise constant or strictly monotone and continuous, with only finitely many pieces.
The result originates in the work of Pillay and Steinhorn on o-minimality and is presented systematically in Lou van den Dries, Tame Topology and O-minimal Structures, Chapter 3 (Cambridge University Press, 1998). A concise expository account is given in Mário Edmundo, O-minimal structures (arXiv:math/0012051). This mission formalizes the one-dimensional monotonicity theorem and its supporting lemmas in Lean 4 against Mathlib, as a verified entry point to o-minimal geometry.
Let be a type equipped with a dense linear order without endpoints : an irreflexive, transitive, trichotomous relation in which every strict inequality admits an interpolant and every element has strict predecessors and successors. Finite Cartesian powers are represented as coordinate tuples , with coordinate projections, deletion, and append operations defined explicitly.
An o-minimal structure over is a family of collections of subsets of , closed under finite unions and intersections, containing diagonals and the order relation, closed under products, coordinate reindexing, and existential projection, and satisfying the o-minimality axiom: every member of is a finite union of points and open intervals. A definable function with domain and codomain is a dependent function on the corresponding subtypes whose domain, codomain, and graph are all members of .
For in , the open interval is the set of coordinate tuples whose single coordinate lies strictly between the two endpoint values, with endpoint variants allowing and . A function is strictly increasing (respectively strictly decreasing) on when implies (respectively ) in the first output coordinate. Continuity at a domain point is the graph-based epsilon-delta predicate: belongs to exactly when the graph meets every sufficiently small box around in the graph of a locally oscillation-free correspondence. Finiteness and infinitude of one-dimensional sets are expressed through first-coordinate listings.
An open cell is good when restricted to is constant, or strictly increasing and continuous there, or strictly decreasing and continuous there. The number of cut points is finite and depends on , , and ; no bound on is asserted.
The result itself. The Monotonicity Theorem is the foundation of one-dimensional o-minimal geometry. It implies that definable sets have finitely many connected components, that definable functions have finite limits at endpoints, and that higher-dimensional cell decomposition can proceed by induction on dimension. Without it, the correspondence between definability and geometric tameness remains unestablished.
Formalizing it. The classical proofs are known and appear in the references above; what is missing is a machine-checked version with explicit definability bookkeeping. This mission produces Lean 4 declarations for the order, interval, monotonicity, graph, and continuity predicates together with the theorem and its lemmas, all verified against the pinned Mathlib revision. The definability infrastructure (products, projections, fiber extraction) is reusable for subsequent cell-decomposition missions. Status honesty: the one-dimensional interval-extraction lemmas are machine-checked; the local constancy-or-injectivity lemma, the injective-to-monotone lemma, the finite-partition assembly, and the goal theorem itself remain open targets.
The naive argument fixes a point and inspects nearby values, but definability does not by itself provide any neighborhood on which behavior is uniform. The fiber dichotomy illustrates the obstruction: knowing that each fiber is definable does not decide whether some fiber contains an interval or every fiber is finite, and the two cases require different constructions (a constancy interval versus an injective-selection interval). Similarly, injectivity alone does not yield monotonicity without partitioning the domain by local sign patterns and applying o-minimality to select a uniform pattern on a subinterval. Each step fails until the relevant definable set is exhibited and the one-dimensional interval lemma is applied to it.
Lean represents one-dimensional points as functions , with order, intervals, and finiteness stated through the first coordinate. Definability is always the structure membership predicate , never an informal attribute. Continuity is the graph-based predicate applied to ; a submission that discharges a continuity goal from the domain inclusion alone, or that replaces the continuity predicate by the domain set, does not satisfy the statement. The goal quantifies over cut points with , , and strict increase at each step; the intervening sets are the open intervals determined by consecutive finite endpoints.
Contributions welcome: direct proofs of the open leaves (fiber definability, the finite-fiber injective-interval construction, the injective-to-monotone step, the finite-partition assembly), sharper statements with explicit endpoint bounds, and reusable o-minimal infrastructure beyond this mission. Out of scope: higher-dimensional cell decomposition, differentiability, and integration of definable functions.
The fundamental lemma is a family of identities between orbital integrals on a reductive group and stable orbital integrals on a smaller group attached to it, its endoscopic group. Langlands isolated these identities in the 1970s as the last missing ingredient in the comparison of trace formulas, and Langlands and Shelstad formulated them precisely in 1987; Waldspurger reformulated the statement for Lie algebras and proved that the Lie algebra form implies the group form. The Lie algebra statement was proved in equal characteristic by Bao Chau Ngo in Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), by a global geometric argument built on the Hitchin fibration; Waldspurger's earlier work transfers the result to mixed characteristic. The identity is the engine behind the stabilization of the trace formula and behind the computation of the cohomology of Shimura varieties.
Both sides of the identity carry a normalizing factor built from the discriminant, and the exact power of relating the two normalizations is fixed by a purely root-theoretic computation carried out in Ngo's §1.10-§1.11. That computation is the subject of this mission. It is self-contained, it uses no geometry, and it is the first piece of the paper that can be stated in Lean today.
Let be a split reductive group over a field with maximal torus , character lattice , cocharacter lattice , root system and Weyl group . Write for the Cartan subalgebra, so that each root has a differential , a linear form on . Ngô's discriminant is the product
a -invariant polynomial function on and hence a function on the space of characteristic polynomials.
An endoscopic datum is an element of the dual torus . The endoscopic group attached to it is the group whose root system is
with Weyl group and its own discriminant . Choose a subset containing exactly one root out of each pair of opposite roots outside , and set
Finally let be a non-archimedean local field with valuation and residue cardinality , and recall Ngô's normalizing factors and .
for a point of the endoscopic Cartan with image . Equivalently with : this is exactly what lets one pass between the two forms of the fundamental lemma, and .
The identity above is the image under of the divisor identity of 1.10.3, which in turn rests on the fact that — which depends on a choice of — is nevertheless -invariant, and on the fact that really is a root subsystem. The milestone list follows that order.
Theorem 1 of Ngô's paper, the Langlands-Shelstad conjecture for Lie algebras, is the identity for corresponding regular semisimple stable classes, under the hypothesis that twice the Coxeter number of is smaller than the residue characteristic. Nothing in that statement can be written in Lean today: reductive group schemes over a discrete valuation ring, endoscopic data, Kostant sections, orbital integrals and affine Springer fibers are all absent from Mathlib. What can be written, faithfully and without any placeholder, is the root-theoretic layer that fixes the transfer factor, and that is what this mission asks for. It is a genuine prerequisite: the two displayed forms of Theorem 1 differ precisely by the identity above.
The mission also produces reusable infrastructure — the discriminant of a root system, the notion of a closed subsystem and its Weyl group, the endoscopic subsystem cut out by an element of the dual torus — none of which currently exists in Mathlib, and all of which any future formalization of endoscopy will need.
Only one of the four milestones is a routine manipulation. Splitting into pairs and collecting squares is bookkeeping; that is -invariant is immediate because permutes . The content is in Lemma 1.10.2: is not stable under , so carries to , where counts the roots of sent into ; the claim is that is always even. The naive attempt — check it on the generating reflections of — is exactly where a careless argument goes wrong, since it is false for reflections in roots outside . Ngô's argument identifies the sign with , the ratio of the sign characters of and , and observes that both compute the determinant of acting on the same reflection representation.
Root systems are modelled with Mathlib's RootPairing ι R M N: the module plays the role
of , the module the role of and of the Cartan on which the differentials
are evaluated, and is the linear form . The endoscopic
subsystem is cut out by an element of the dual torus, taken as a group homomorphism
from the cocharacter lattice to an arbitrary commutative group, and is expressed over
coefficients as in the definition of a root datum. Products over and are
finite products over a Fintype index, and a choice is a Finset satisfying an
exclusive-or condition, which automatically rules out the degenerate case .
The identity 1.10.3 is stated as an identity of functions on the Cartan rather than as an identity of divisors, so the unit is carried explicitly rather than discarded. Lemma 1.10.2 is stated over for an honest root system, since the sign argument uses the reflection representation. The goal 1.11.3 is stated for an additive valuation with values in , which is what makes the two sides comparable when a discriminant vanishes.
There is no trivializing formalization here: the hypotheses of every item are satisfiable — any root system with any closed subsystem and any choice of gives an instance — so none of the statements is vacuous, and none of them is an identity between two occurrences of the same expression.
Contributions of the surrounding theory are welcome: a positive system compatible with a subsystem, the sign character of a Weyl group, and the reducedness of the discriminant divisor (the remaining half of Lemme 1.10.1) are all natural next steps.
A coset partition of a group is a finite family of left cosets that are pairwise disjoint and cover . In 1974 Herzog and Schönheim asked whether the indices of such a partition, with , can be pairwise distinct. They cannot when — there a coset partition is an exact covering system of the integers, and Davenport–Rado and Mirsky–Newman showed the largest modulus must repeat — but for general groups the question is still open, even for finite solvable groups.
Progress has come in two styles. Structural: Berger, Felzenbaum and Fraenkel settled finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333 and finite pyramidal groups in Fund. Math. 128 (1987) 139–144. Order-bounded: Ginosar and Schnabel (2011) settled every whose order has at most two prime divisors, and Margolis and Schnabel (2019) verified all .
The paper formalized here, Z.-W. Sun, J. Algebra 273 (2004) 153–175, takes a third route: it constrains the subgroups rather than the group, and simultaneously weakens "partition" to "uniform cover". Its hypothesis — that the be subnormal — costs nothing in the nilpotent case (every subgroup of a nilpotent group is subnormal) yet applies to arbitrary, possibly infinite, ambient groups . It also answers negatively an open question of the same paper, generalizing one of Erdős: the indices of such a cover cannot all be large if each occurs only boundedly often.
Let be a group, written multiplicatively. For a finite system
of left cosets, the covering function counts memberships,
If is constant, say , then is a uniform cover of of weight ; the case is exactly a coset partition. A uniform cover is trivial when for every , and this is the only degenerate case that must be excluded. Uniform covers are genuinely more general than partitions: one may have no disjoint subcover at all.
A subgroup is subnormal if some finite chain reaches , each term normal in the next. Normal subgroups are subnormal; in a nilpotent group every subgroup is; and shows a subgroup of a solvable group need not be.
Write for the indices, always assumed finite, and
for their least common multiple, whose prime divisors are exactly those of . Let and denote the least and greatest prime divisors of , let be Euler's totient, and let
be the largest multiplicity with which an index is repeated. The Herzog–Schönheim conjecture says .
The goal theorem is Theorem 4.3(i) of the source: for a nontrivial uniform cover of any group by cosets of subnormal subgroups of finite index, some index divisible by the largest prime is repeated at least times,
In particular . Two weaker consequences are separate targets. Since , this gives the Herzog–Schönheim conjecture for subnormal uniform covers,
and the quantitative step behind it is a Burshtein-type inequality, which after clearing denominators reads
The result itself. It is the widest structural class in which Herzog–Schönheim is known, and the only one that does not require to be finite: subnormality of the is a condition on the subgroups, so itself is arbitrary. It strictly contains the nilpotent case of Berger–Felzenbaum–Fraenkel, and being quantitative it also yields the Burshtein conjecture in this setting — a bound no purely qualitative statement gives. Because the conclusion is a lower bound on growing with , it answers the paper's open question: one cannot make all the indices of a uniform cover large while keeping every multiplicity bounded.
Formalizing it. Nothing here is open, and the mission is the machine-checked version of a known
proof. What it adds is a formal vocabulary for uniform covers — Mathlib has
Mathlib/GroupTheory/CosetCover.lean (B. H. Neumann's theorems, ) but no
notion of covering multiplicity — and the arithmetic of subnormality, in particular that
divides when the are subnormal. Mathlib has
Subgroup.IsSubnormal with the basic closure properties but nothing about indices of subnormal
subgroups, and that divisibility is the whole reason subnormal covers behave. The totient measure
this proof runs on is already formalized: Sun's Lemma 3.1 is Berger–Felzenbaum–Fraenkel's equation
(14), already proved on the platform as BFFPyramidal.muMeasure_divisorClosure_image_mul, and
this mission reuses that definition file rather than duplicating it.
Status disclosure. Complete Lean proofs of the goal and of every milestone below already exist and will be submitted at launch, so this mission is not an open frontier: its value is the verified artifact, the reusable vocabulary, and the fact that the development turned up two places where the published argument needs repair or can be simplified (see Formalization scope). Alternative proofs, sharper variants, and the analytic parts excluded below remain genuinely open contributions.
The reciprocal identity is the first thing anyone writes down and it is not enough: a uniform cover of weight satisfies , and pairwise distinct can do that.
The real obstruction is that a cover does not descend to a quotient. A part need not lie in one coset of a chosen normal subgroup, so the induction that proves the finite nilpotent case has nothing to induct along once may be infinite and the are merely subnormal. Sun's replacement is a lower bound for the size of a union of cosets, Theorem 3.1: if for all and , then the number of cosets of inside is at least the number of divisible by some . The union is compared not with the but with a purely numerical shadow of itself in , and it is here that subnormality enters, through the divisibility (Lemma 2.1) — for arbitrary finite-index subgroups Poincaré gives only the inequality , which is too weak.
The second difficulty is arithmetic and is where the source spends its effort. Turning Theorem 3.1 into a bound on multiplicities (Theorem 3.2) requires computing the density of a union , and the identity the paper uses (Lemma 3.4) expresses that density as times an infinite sum of reciprocals over -smooth elements of the union. Along that route the full series is needed: truncating it loses precisely the geometric factors that produce the divisor sum in the conclusion.
It is worth saying, though, that this analytic detour is avoidable — a solver need not take it. Theorem 3.2 can also be reached by a purely finite argument: bound the density from below by injecting each index into the divisor , which is sharp in the same cases as the series argument. Lemma 3.4 remains a faithful and separately interesting milestone of the paper, but it is not on the critical path to the goal. The naive version of the finite estimate — bounding the density below by — is genuinely false, as shows, so the injection is the content, not a one-liner.
The development commits to the following conventions, worth stating because the prose leaves them implicit.
Covers are indexed families rather than sets of cosets: IsUniformCover K a w asserts that for
every the number of indices with is exactly w, counted as
Nat.card of a subtype so that no decidability hypothesis is needed. Indexing by Fin k keeps
multiplicities visible, which matters because every conclusion counts indices, not distinct
subgroups. Nontriviality is never folded into the definition; it appears as the explicit
hypothesis ∃ i, K i ≠ ⊤, and without it every statement here is false (take , ).
is an arbitrary group — not assumed finite. Finiteness enters only through
Subgroup.FiniteIndex on each , which the source assumes implicitly when it writes "the
(finite) indices". Indices are Subgroup.index and is H.relIndex (K i). For a
subgroup that is not assumed normal, G ⧸ H is still the type of left cosets and
Nat.card (G ⧸ H) = H.index; Theorem 3.1 is stated with that type, since the it is applied
to is not normal.
Densities are never limits. The density of a union is taken as the
finite ratio for an explicit common multiple ,
which is exactly equal to the asymptotic density and keeps Lemma 3.4 free of any analysis on the
left-hand side; the right-hand side genuinely is an infinite sum and is stated with HasSum over
.
Inequalities are cleared of denominators and stated in wherever possible, so that appears as . Readers should check the direction: subtraction truncates, so is only the intended quantity because every here is prime, hence .
⚠️ Parts (ii)–(iv) of the source's Theorem 4.3 are out of scope. Those bound the primes
dividing the indices, their number, and by and similar, and they rest on Mertens' third theorem,
, which Mathlib does not have. It is worth
being precise about what Mathlib does have, since the gap is narrower than it looks: the prime
counting function Nat.primeCounting, Chebyshev's and with the machinery around
them (Mathlib/NumberTheory/Chebyshev.lean), Euler products
(Mathlib/NumberTheory/EulerProduct/), and the constant itself
(Real.eulerMascheroniConstant) are all present — what is missing is Mertens' asymptotic tying
them together, and the asymptotics. Supplying that is a substantial number-theory
project in its own right, so this mission stops at the arithmetic core, part (i), which is what
implies Herzog–Schönheim. Contributions adding the analytic parts are welcome and would complete
Theorem 4.3.
Two things the development established that the paper does not state. First, Lemma 2.1 is true in a stronger form: needs only subnormal, not both, and needs no finiteness hypothesis at all (with Mathlib's convention that an infinite index is ). Second, Theorem 4.1's passage from the largest prime to the smallest can be isolated as a self-contained arithmetic inequality, , which is tight at prime powers; it is listed as its own milestone for that reason.
Reusable beyond this mission: the uniform-cover vocabulary, the subnormal index divisibility of Lemma 2.1, and Theorem 3.1's union bound, which applies to any attack on Herzog–Schönheim including the still-open solvable case. The source also leaves Conjecture 4.1 open — that for a nontrivial uniform cover by subnormal subgroups the largest index is repeated at least times, its least prime factor — which would be a natural follow-on target.
This mission curates the formalized output of Alethean — an Autonomous Logic Engine for Theorem Hunting, Exploration, And Navigation (alethean.org). Alethean autonomously generates research directions, develops them into research papers, and formalizes their results in Lean 4 — an "ever-expanding registry of absolute mathematical truths," built with the Aristotle reasoning engine. "The unconcealed truth between conjecture and proof."
The corpus's public home is the Alethean Lean 4 Catalog — the central registry of formalized theorems across the ecosystem, browsable as research packages (each with its article, research paper, interactive view, future directions, and Lean 4 proof files). This mission is the platform-side mirror of that registry: 2,799 definition bundles and 7,517 theorems compiled and verified against the pinned toolchain (Lean v4.30.0, Mathlib c5ea003), spanning analytic number theory, combinatorics, probability, information theory, quantum information, tropical algebra, and machine-learning theory.
The corpus arrives fully proved. The goal theorem is the corpus's universal error-detection bound for random checksums — the capstone of the Almost-Lossless compression thread (Compression Beyond the Pigeonhole Bound): appending an independent random checksum makes the probability of silent corruption at most , uniformly over all source strings and all inner decoders. The milestones are capstone theorems from across the corpus: sphere-packing and VC-dimension bounds, second moments of central -values, tropical Arrow-type impossibility, sums-of-three-cubes obstructions, and more.
Every milestone is a verified platform theorem: study the proofs, reuse them as imported lemmas, or rebuild them from first principles. The interesting open work is extension: the corpus's research-direction papers (browsable at alethean.org under Future Directions) state quantitative sharpenings — explicit constants, wider parameter ranges — that are not yet formalized. Pick a direction, formalize its statement, and the verification pipeline does the rest.
53c2925a02)c5ea00351c28e24afc9f0f84379aa41082b1188faether-catalog.A coset partition of a group is a finite family of left cosets of subgroups that are pairwise disjoint and cover . Asking which multisets of indices can occur is a question with two independent origins. For the cosets are arithmetic progressions and a coset partition is an exact covering system of the integers; Erdős asked whether the moduli of such a system can be pairwise distinct, and Davenport and Rado, and independently Mirsky and Newman, showed they cannot — the largest modulus must repeat. For general groups, Herzog and Schönheim (1974) asked the same question: in any coset partition with , must two of the indices coincide? That question is still open.
Progress has come by restricting the group. Berger, Felzenbaum and Fraenkel proved the conjecture for finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333, and the paper formalized here extends it to a wider class defined by a chain condition. Later work bounds the order instead of the structure: Ginosar and Schnabel (2011) settle every whose order has at most two prime divisors, and three prime divisors when , while Margolis and Schnabel (2019) verify all . The conjecture remains open even for finite solvable groups.
Let denote the least prime factor of and the greatest, and let be Euler's totient function.
A finite group is pyramidal if it admits a chain of subgroups
in which every step has index equal to the least prime factor of the order of the preceding term:
A subgroup whose index is the smallest prime dividing the order is automatically normal, so the chain is a composition series; consequently every pyramidal group is solvable, and every supersolvable group is pyramidal. Pyramidality is therefore a chain condition sitting between supersolvability and solvability.
Given a coset partition of , write
The goal theorem is the multiplicity lower bound of Berger–Felzenbaum–Fraenkel. If is pyramidal and the cosets , , partition with , then at least
of the subgroups have the same order.
Two consequences are separate targets. Since whenever , the bound yields the Herzog–Schönheim conjecture for pyramidal groups:
and it likewise settles Burshtein's conjecture in this setting, which concerns the case and bounds the primes dividing in terms of the largest multiplicity.
The bound is quantitative where the Herzog–Schönheim conjecture is qualitative: it does not merely assert that a repetition exists but forces a repetition of prescribed multiplicity, growing with the largest prime factor of . That is what makes it strong enough to also imply Burshtein's conjecture, which no purely qualitative statement does.
The class it covers is also of independent interest. Nilpotent groups are pyramidal, so the result subsumes the authors' earlier theorem, and it reaches groups that are solvable but far from nilpotent. It remains, more than three decades later, among the structural (as opposed to order-bounded) cases in which the conjecture is known.
No part of this development is currently formalized: Mathlib has the ingredients — Sylow theory, Hall subgroups of solvable groups, Euler's totient with Gauss's identity — but neither coset partitions as a structure, nor pyramidality, nor any case of Herzog–Schönheim. The mission produces the first machine-checked proof of a structural case of the conjecture, together with a reusable formal vocabulary for coset partitions.
The reciprocal identity is immediate and useless on its own: distinct indices can satisfy it, so no counting argument over the indices alone can succeed.
The natural attack — induct along the chain, quotienting by — fails because a coset partition does not descend to a quotient. A part need not lie inside a single coset of : if then it meets every coset of , and the induced family on is a cover with multiplicity rather than a partition. Controlling that dichotomy is the first obstacle, and it is precisely where the definition of pyramidality is used, the index being the least prime factor of rather than an arbitrary one.
The second obstacle is that the conclusion counts subgroups of equal order, so the induction must carry a lower bound on the size of a union of cosets that is sensitive to the orders and not merely to their number. The paper's device is a measure on the naturals with , evaluated on the divisor closure of the set of orders; Gauss's identity makes interact correctly with divisibility, and the required inequality is genuinely a statement about the group, not about the multiset of orders. The final step splits off the Sylow -subgroup against a Hall complement, which exists only because pyramidal groups are solvable.
The development commits to the following conventions, all fixed in Lean and worth stating because the prose leaves them implicit.
Coset partitions are indexed families rather than sets of cosets: IsCosetPartition K a asserts
that for every there is a unique index with . Indexing by Fin t
keeps multiplicities visible, which matters since the conclusion counts indices, not distinct
subgroups; and uniqueness encodes disjointness and covering simultaneously. Groups are finite via
[Finite G], and orders and indices are Nat.card and Subgroup.index.
Pyramidality is stated as the existence of a length and a chain c : ℕ → Subgroup G with
c 0 = ⊤, c n = ⊥, and Subgroup.relIndex (c (k+1)) (c k) = Nat.minFac (Nat.card (c k)) for
k < n. Normality of each step is a consequence, not a hypothesis, and is deliberately not assumed.
The greatest prime factor is maxPrimeFac m = m.primeFactors.sup id, which is for
; the floor in is natural-number division, so the goal statement is
(maxPrimeFac l * Nat.totient l) / l + 1 ≤ …. Note that the bound is vacuous at — there
and — so is a necessary hypothesis and is present in every
statement that needs it; a formalization omitting it would be trivially true and is ruled out.
A complete development needs, beyond the goal: the coset intersection lemma; the least-prime-index dichotomy; uniqueness of the Sylow -subgroup of a pyramidal group; the scaling law for the divisor-closure measure; the union lower bound; and solvability of pyramidal groups. The coset-partition vocabulary and the union bound are reusable for any other case of Herzog–Schönheim, including the still-open solvable case, and contributions of alternative proofs or sharper variants are welcome.
Quantum algorithms for stochastic optimization are usually presented one paper at a time: a schedule is fixed, a quantum mean estimator is substituted for a classical minibatch, and a new rate is derived from scratch. The derivations are near-identical, and the step that actually differs — the price of one gradient query — is buried inside each proof rather than exposed as a parameter.
This mission publishes a Lean 4 development in which the oracle is a parameter, not an assumption. One rate theorem, instantiated at different oracle contracts and cost models, yields the classical rate, the inexact-gradient rate, and the quantum rate. All constants are explicit; nothing is asymptotic.
The published results it reproduces or corrects:
Let be a real inner-product space, an objective, and a map supplied as a parameter in place of the gradient. The smoothness hypothesis is the descent-lemma inequality
written ; this is exactly what rate proofs consume, and it is implied by a Lipschitz gradient. Write for the initial gap, for the target accuracy, for the gradient-noise scale, for the mean-squared smoothness constant, and for the ambient dimension.
A cost model converts a target accuracy into a query count as a power law with exponent . Its member is the classical minibatch bill, scaling as ; its member is the quantum mean-estimation bill, scaling as . That single exponent is where classical and quantum part company.
The goal theorem is the exact crossover between the two SPIDER bills. Writing and for the dominant terms of the quantum and classical query totals,
the target asserts, for and ,
Every supporting rate is also published and proved: the two SPIDER query totals, SPIDER's correctness, the SGD and PL rates, the exact and inexact gradient-descent rates, the two variance-purchase bills, and the two query counts.
The results. The crossover makes the dimension-versus-accuracy trade-off of quantum stochastic optimization quantitative rather than folkloric. Two readings follow directly: at fixed the quantum advantage disappears as , so the speedup lives at moderate accuracy, not asymptotically; and at fixed the advantage requires . Note what cancels — , and the -exponent all drop out, leaving only against .
The formalization. Because the oracle and the cost exponent are parameters, the classical and quantum rates are one theorem evaluated twice rather than two proofs. This mission is unusual in that its frontier is already closed: every node arrives with a machine-checked proof, transplanted from a green build. What it offers the platform is a reusable, fully-proved layer for first-order convergence analysis — function classes, cost models, a one-step descent recursion, accumulation laws including a stopped-time version, and the SPIDER schedule — on which further rates can be built by instantiation.
The apparent difficulty is not where a newcomer expects. Deriving a rate from the one-step recursion is routine telescoping. What is delicate is keeping the constants honest while the oracle varies: a rate proof that quietly assumes an exact gradient, or a global lower bound on , will produce the right-looking exponent from the wrong hypotheses.
Two specific places carry real content. Evaluating an error recursion at a random return time breaks the unconditional variance bound, because conditioning on destroys independence; the stopped-time accumulation law is what repairs it. And reproducing a published constant exactly — rather than up to — is what certifies that the parametrized machinery has not silently degraded the bound it generalizes.
Smoothness is QuadUpper on an explicitly supplied g; no differentiability or convexity is assumed anywhere, and the only lower-bound hypothesis is at the terminal iterate rather than globally. Cost models are an inductive family with a power-law member, so the classical and quantum instances are and of one definition. Half-integer powers are written with Real.sqrt, so no real exponentiation appears in any statement. Stochastic results use a genuine Filtration and a conditional oracle contract; the tower property is derived, not assumed.
Two honesty notes. Several statements carry hypotheses that Lean marks unused; these are recorded as such in the individual nodes rather than presented as load-bearing. And the library records a discrepancy in Sidford--Zhang's Algorithm 7 parameter block, documented in its own STATUS notes; the formalization follows the corrected parameters.
lean-optrates, github.com/shiy1022/lean-optrates at commit 4c0b8498, Apache-2.0, by Yueheng Shi. The platform copy renames the root namespace OptRates to ShiOptRates; no statement or proof is otherwise altered.Discrepancy theory asks how unbalanced a two-coloring of a combinatorial structure must be in the worst case. Concretely: given sets over an -element ground set, color each element or so that every set is as close to balanced as possible. The question is classical (Beck–Fiala 1981; Spencer 1985) and the answer for general (dense) set systems is one of the sharpest gaps between a naive probabilistic bound and the truth known in combinatorics: assigning colors uniformly at random only guarantees discrepancy , yet a coloring with discrepancy always exists — the logarithmic factor is an artifact of the naive argument, not of the problem. This mission formalizes that removal, following T. Rothvoß's lecture-note exposition of J. Spencer's entropy method (MIT 18.095, "Discrepancy theory"), the standard modern presentation of the technique (see also Matoušek, Geometric Discrepancy, Ch. 4). The entropy method is the ancestor of the whole "partial coloring" family of arguments used throughout discrepancy theory and combinatorial algorithm design, so a machine-checked account of its base case is reusable well beyond this one theorem.
Fix and an matrix with entries in , thought of as the incidence matrix of sets over an -element ground set: iff element lies in set . A coloring is a map , and the discrepancy of row under is , the signed imbalance of set . The discrepancy of the matrix is the value achieved by the best coloring, minimizing the worst row.
The entropy method bounds this via the partial coloring lemma: rather than coloring all elements at once, one repeatedly colors a constant fraction of the currently uncolored elements while keeping every row's contribution small, then recurses on what remains. Each round is itself produced by an entropy/pigeonhole argument: quantize each row's signed sum (under a uniformly random coloring) into "shells" of width (where is the number of active elements); a short computation shows this quantization carries very little Shannon entropy once the shell width exceeds a threshold; subadditivity of entropy across the rows then bounds the joint quantization entropy, which by pigeonhole forces an exponentially large set of colorings landing in the same joint shell; Kleitman's theorem on the diameter of a large subset of the Hamming cube then extracts two such colorings that are far apart in Hamming distance, and their difference is the sought partial coloring.
Goal.
This is the qualitative, constant-suppressed form of Spencer's theorem: it asserts discrepancy with a single universal constant, and deliberately leaves that constant unspecified. This is the right goal for this mission because it is the weakest statement that is still stable: any future improvement to the constant (down to Spencer's sharp , or beyond) refines this theorem rather than invalidating it.
The removal of the factor is the entire content of Spencer's theorem: it is what separates discrepancy theory from a corollary of concentration inequalities, and the partial-coloring/entropy method it introduced underlies later results throughout the field (Beck–Fiala-type bounds, the Komlós conjecture literature, and constructive/algorithmic discrepancy minimization). Formalizing it is formalizing the base case that every later partial-coloring argument specializes.
This mission's goal theorem, spencer_discrepancy_sqrt_n_bound, is already proved (zero sorrys), by a from-scratch entropy-method development: the per-row shell-entropy bound, the joint pigeonhole-and-Kleitman assembly for one round, and the outer geometric iteration and induction combining rounds into a full coloring. What remains open in this mission is shannonEntropy_shellFin_le (Lemma 9 in Rothvoß's notes) — the per-row entropy bound is currently imported as an assumption by the one-round lemma lemma8_partial_coloring_round, which is therefore only conditionally proved pending it. A separate, harder mission on this platform (Komlos.spencer_six_deviations) targets Spencer's sharp constant via a tighter, non-standard numeric derivation; that is a distinct, substantially harder target and this mission does not duplicate it.
The obvious argument is: fix a target bound , use a Chernoff/Hoeffding bound to show each row fails with probability at most , union-bound over the rows, and take a coloring outside the bad event. This works to prove a single good coloring exists — but it is not strong enough to survive being iterated to remove the entire uncolored set, because a per-row union bound loses a factor of that a fixed cannot always absorb once the active column count is close to : for the scaling family where the row count and the active set shrink together, the naive union bound's failure probability grows linearly in , not exponentially, exactly canceling the exponential decay one is trying to exploit. The fix is to bound the joint entropy of all rows' quantizations at once (subadditivity of Shannon entropy), rather than union-bounding row-by-row failure events; this is genuinely a different technique, not a tightening of the same one, and it is the reason the entropy method is presented as its own tool rather than a Chernoff-bound corollary.
Matrices are Fin n → Fin n → ℝ with an explicit ∀ i j, A i j = 0 ∨ A i j = 1 hypothesis; colorings are represented two ways in this development — Fin m → Bool internally (via the platform definition RSign converting to ) during the entropy/Kleitman argument, and directly as Fin n → ℝ constrained to pointwise in the goal theorem's statement, matching the usual -coloring convention. The row-sum shell quantization is the platform definitions rowSumB, shellIdx, shellFin (an integer-valued "round to nearest shell" construction, packaged into a fixed Fin (2m+3) type for entropy purposes). The active column set during the outer iteration is tracked as a shrinking Finset (Fin n) of the original index type throughout, rather than moving between different Fin m types round to round, which keeps the induction free of type-level bookkeeping.
Reusable, already-Proved infrastructure this development builds on: shannonEntropy_pi_le (subadditivity across independent rows), shannonEntropy_pigeonhole, choose_sum_le_exp_mul_binEntropy, and kleitman_diameter, all already Proved on the platform independent of this mission. The one genuinely open piece — and the mission's standing invitation — is shannonEntropy_shellFin_le (Lemma 9): a self-contained Shannon-entropy computation about the shellFin quantization that does not depend on anything else in this mission and can be attempted independently.
Quantum low-density parity-check codes encode quantum information using sparse parity constraints. A standard way to construct them is to translate binary chain complexes into Calderbank--Shor--Steane codes and to combine complexes by tensor product. Homology identifies the logical operators of the resulting code, while the smallest Hamming weight of a nontrivial homology class controls one of its distances. Determining how this distance behaves under a tensor product is therefore a basic structural question, not merely a parameter calculation.
Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an arbitrary finite binary chain complex and the other is the one-complex induced by a binary matrix. Their paper was published as “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). Its main distance result is Eq. (13) in the arXiv version: for this particular tensor factor, the usual product upper bound is always exact. The result extends the familiar two-complex setting of quantum hypergraph-product codes to the local structure occurring in complexes of any dimension.
A based binary chain complex consists of finite-dimensional vector spaces over , each equipped with a specified coordinate basis, and linear boundary maps
such that . Its degree- homology is . The homological distance is measured in the chosen basis:
Following the paper, the minimum of an empty set is . Thus when is trivial.
The endpoint convention is also the one stated explicitly after Eq. (1). For an -complex, is the zero matrix and is the zero matrix. Consequently
and
For an binary matrix , the one-complex has in degree one, in degree zero, and boundary . Its two distances are
and
In particular, unless has full row rank, in which case . The degree- chain group of is
with the standard tensor-product boundary. Over the usual sign in that boundary has no effect.
The first milestone is Eq. (11) for two arbitrary finite-length based binary chain complexes:
Let and . The second milestone is Theorem 1, including both of its cases:
and
The goal is Eq. (13):
No full-rank hypothesis is imposed on .
The equality determines the product distance exactly from four component distances. General tensor-product arguments immediately provide the upper bound, but an exact formula requires ruling out lower-weight homology classes that mix the two direct-sum blocks. Once established, the formula can be applied repeatedly to tensor products of one-complexes, which is the step used in the paper to obtain higher-dimensional quantum hypergraph-product code families and to compute their distances.
For formalization, the mission contributes reusable definitions of finite based binary chain data, homological distance valued in , the one-complex of a binary matrix, and the relevant tensor-product boundary maps. Mathlib contains Hamming weight and general homological-algebra infrastructure, while QECLean contains a closely related based length-three homological-code interface. Neither the selected Mathlib environment nor the inspected QECLean development currently supplies this rank-sensitive exact distance theorem.
The central issue is that Hamming weight depends on the chosen bases and is not preserved by arbitrary homological isomorphisms. A Künneth isomorphism describes the product homology and readily produces low-weight representatives, which is enough for the upper bound, but it does not by itself exclude a still lighter representative obtained by cancellation between the two tensor blocks. The lower bound must also remain valid at the endpoints of the complex and in singular cases where one or more homology groups vanish and the relevant distance is .
The theorem cannot be reduced to a dimension calculation. It must reason about supports and Hamming weights of based representatives while respecting the quotient by boundaries, and it must cover both and .
The Lean development works over ZMod 2. A finite basis in degree is
represented by Fin (dimension i), and a chain group is the function space
from that coordinate type to ZMod 2. BasedBinaryChainComplex stores the
dimension and boundary in every nonnegative degree, the chain condition, and a
finite length above which all dimensions are zero. Thus the first milestone
quantifies over genuinely arbitrary finite lengths for both and
, rather than over a local window or a one-complex specialization.
If the stored length is , the zero-dimensional source in degree
makes the unique zero map, just as the
zero-dimensional target below degree zero makes
the unique zero map. Hence both singular endpoint
cases in Eqs. (1) and (4) are represented directly.
Distances use WithTop ℕ. Their definitions are actual minima of Hamming
weights of nontrivial representatives, with ⊤ produced by the empty-set
case; infinite distance is not an extra hypothesis or a separately hard-coded
branch. Coordinate types may be empty, which covers missing endpoint blocks.
The binary matrix is represented as a linear map between two finite based
function spaces. Its row and column coordinate types need not be nonempty,
and no injectivity or surjectivity assumption is added.
The degree- product group is indexed by the disjoint union of all coordinate products for . Consequently its Hamming norm is the sum of the weights of all tensor-degree blocks. The product boundary is the standard signed tensor boundary; its sign disappears over . A formal proof verifies that every pair of consecutive product boundaries composes to zero; the cancellation of the two mixed terms uses characteristic two. Thus the product distance is taken from an actual chain complex, rather than from unrelated adjacent linear maps. A basis-free tensor product or an abstract homology group alone is insufficient for the target, because either would discard the weight data on which the statement depends. The mission does not formalize the asymptotic code-family construction later in the paper, the transposed cohomological distance, or the CSS-code parameter translation. Those are natural downstream missions; they should reuse rather than alter the present based-chain definitions.
Computability theory studies which questions admit algorithms and how the unsolvable questions compare with one another. A decision problem can be represented by a set of natural numbers: the question on input is whether belongs to the set. Even when there is no algorithm that always answers this question, there may be an algorithm that eventually recognizes every positive instance. Understanding the relative difficulty of such problems is the setting of the Friedberg–Muchnik theorem.
The original paper by Richard M. Friedberg appeared in 1957 under the title Two recursively enumerable sets of incomparable degrees of unsolvability (solution of Post's problem, 1944). It supplies the historical paper source for this formalization. A. A. Muchnik's independent contribution appeared in Russian in 1956. Friedberg, PNAS 43(2), 236–238; Muchnik, Math-Net bibliography, 1956 entry.
A set is computably enumerable, abbreviated c.e., if membership has a semidecision procedure: on input , the procedure halts exactly when . The older terminology is recursively enumerable, abbreviated r.e. The Lean predicate CEnumerable A uses Mathlib's REPred for this property. A computable set has a decision procedure that terminates on every input and answers membership correctly; this is expressed separately by ComputableSet A using ComputablePred.
For each set , define its characteristic function by
An oracle for answers requests for this function's values. It always supplies an answer, even if membership in cannot be computed without an oracle. The declaration setOracle A represents this total function inside Mathlib's type of partial functions from natural numbers to natural numbers.
Write when an algorithm with access to the membership oracle for computes on every input. This is Turing reducibility, expressed by SetTuringReducible A B. The algorithm may make several queries, with later queries depending on earlier answers. Incomparability requires both and ; it is stronger than saying the two sets merely have different degrees. These conventions specify the mathematical reading of the supplied Lean definitions.
The goal is the following unconditional existence statement:
Its Lean name is Computability.friedberg_muchnik. No enumeration, pair of sets, or oracle program is supplied as a hypothesis. Both sets must be obtained as witnesses to the conclusion. The statement matches Theorem 26.2 in Arnold W. Miller's Lecture notes in Recursion Theory, Section 26, with the theorem on page 51 and its proof on pages 51–54. Miller, December 3, 2008 version.
The target establishes that the c.e. problems have incomparable levels of computational difficulty. Its witnesses cannot be computable: a computable membership procedure would also work in the presence of any other oracle simply by making no queries, contradicting the required nonreducibility. The stronger historical consequence is a positive solution of Post's problem: a c.e. degree can lie strictly between the computable degree and the halting degree. Miller records this consequence separately as Corollary 26.3 on page 54. Miller, Section 26.
The mathematical theorem is established; the work requested here is its Lean 4 formalization. A completed development must construct witnesses, prove their computable enumerability, and exclude oracle computations in each direction using Mathlib's actual reducibility relation. The provided goal currently ends in sorry. Successful compilation of this statement checks its formulation and imports; it does not constitute a proof of the existence result.
The main obstacle is preserving decisions about oracle computations while both sets are still being enumerated. An additional element in one set can change an oracle answer used by an earlier computation, undermining the attempt to separate the other set from it. There are infinitely many candidate programs in both directions. Thus a formal treatment has to justify the eventual stability of the relevant computations as well as the effectiveness of the enumeration. This is the setting of the finite injury argument developed in Miller's proof of Theorem 26.2. Miller, pages 51–54.
The sets are arbitrary Set ℕ, including the natural number zero in their ambient domain. The oracle answers use natural numbers, with one for membership and zero for nonmembership. Classical reasoning is used to define the oracle for an arbitrary set; it supplies no assertion that this function is computable. Each oracle is nevertheless total. Replacing it with a partial membership recognizer would change the meaning of the target.
The foundation consists of Mathlib.Computability.RE and Mathlib.Computability.TuringDegree, together with the supplied definitions in namespace Computability. SetTuringEquivalent records reducibility in both directions. degreeOfSet maps a characteristic-function oracle to its Turing degree, and CEnumerableDegree says that a degree has a c.e. representative. These additional definitions are retained as useful interfaces, while the root theorem itself is expressed directly with sets and TuringIncomparable.
A complete proof will need representations of effective finite stages and oracle computations, and lemmas relating those representations to the imported predicates. Such infrastructure can support later formalizations involving oracle use, computable enumerations, and priority constructions. Contributions should establish these connections with Mathlib's definitions and finish the unconditional target. The theorem must not be replaced by mere degree inequality, weakened reducibility, or a conditional assertion that assumes the required incomparable sets already exist.
The Kerr metric (Kerr, 1963) is the exact solution of the vacuum Einstein equations that describes the exterior gravitational field of a rotating mass. It is the working model for astrophysical black holes: gravitational-wave templates, black-hole imaging and the classification results of the uniqueness theorems all take it as their starting point. Its form in the coordinates of Boyer and Lindquist (1967) is the one found in every textbook, and the statement that this line element has vanishing Ricci tensor is the single most-cited computation of the subject. That computation is long, it is almost never printed, and in practice it is trusted because computer-algebra systems agree on it. The parent project of this mission builds a certified-discovery pipeline for exact solutions of Einstein's equations in which a symbolic verifier is the oracle; this mission asks for the Kerr instance of that oracle's verdict to be re-established inside a proof assistant, so that the pipeline's benchmark result rests on a kernel-checked proof rather than on a simplification routine.
Timeline: Kerr (1963) found the metric in Kerr-Schild and in his original coordinates; Boyer and Lindquist (1967) introduced the coordinates in which the metric below is written and described its maximal analytic extension; Carter (1968) established the separability structure that underlies the closed-form inverse. None of these results has, to the authors' knowledge, a machine-checked proof.
Fix real parameters and . A point of is written ; in Lean it is a function Pt := Fin 4 → ℝ. Write , and
The Boyer-Lindquist Kerr metric is the symmetric matrix of functions
with all other entries zero (signature , ). Its closed-form inverse has , and a block with denominator . The regular coordinate domain is
For any matrix of functions with candidate inverse , the coordinate partial derivative is the one-variable derivative at of the slice , and the coordinate Christoffel symbols and coordinate Ricci tensor are
These four definitions (pd, christoffel, ricci, ricciOf) form the definition bundle KerrBL_CoordGeometry; the metric, its inverse and the regular domain form KerrBL_Kerr_Metric.
KerrBL.vacuum_Kerr)For all real and every with :
The goal deliberately bundles the inverse identity and the two differentiability clauses with Ricci-flatness. Without the first, ricciOf g ĝ with a wrong could vanish trivially; without the other two, the derivative in the definition of could be Mathlib's default value at a non-differentiable slice. With them, the last clause is a statement about the genuine coordinate Ricci tensor.
The milestones follow the three layers of the proof: (I) the inverse identity; (II) the bridge from the generic definitions to explicit closed forms, through derivative certification of the metric, the Christoffel bridge, derivative certification of the generic Christoffel symbols, and the Ricci bridge ; (III) the vanishing of the explicit expression for each of the eight components that are not structurally zero, as rational identities in the seven variables under , , , and finally the vanishing of all sixteen generic components.
The result itself is classical: the Boyer-Lindquist Kerr family is a vacuum solution wherever the coordinates are regular. What the mission adds is a proof in which the trusted base is explicit and small: a 45-line generic layer defining , and , and the transcription of five metric components from a hash-locked source file, with source-lock lemmas proving that the compact definitions equal the transcriptions. Everything else, including roughly 120 kB of generated closed forms, is bridged by proof; a wrong closed form can make a bridge theorem unprovable but never a false theorem provable. The generic layer and the bridge pattern are reusable for any coordinate metric in four dimensions, and the pattern of certifying a computer-algebra derivation through polynomial witnesses checked by linear_combination is reusable for any rational-function identity.
Status: the theorem is proved in the classical sense since 1963 and verified by every computer-algebra system; the machine-checked coordinate proof is what this mission records. At launch every node of the mission carries an accepted proof.
The obvious argument is to compute. The difficulty is size and control, not ideas. The Ricci components of Kerr are rational functions whose numerators have up to a few hundred monomials in seven variables; a normalisation tactic applied to the raw expression does not terminate in practice, and a naive -based unfolding of the double sums over produces terms whose elaboration alone exceeds the server budget. The proof therefore has to be organised: opaque atoms for and so that denominators are monomials, per-term clearing lemmas over a common denominator, and a single polynomial identity per component certified by explicit quotient witnesses of the relations , , . Mathlib's derivative also needs care: deriv returns where a function is not differentiable, so every derivative used in the Ricci formula must be accompanied by a HasDerivAt witness, and the differentiability of the generic Christoffel symbols has to be transferred from their closed forms by a locality argument on the open regular domain.
The Lean representation commits to the following. Points are Fin 4 → ℝ with , , , ; there is no manifold, no chart, no periodicity of and no range restriction on . Derivatives are Mathlib's deriv of coordinate slices. The candidate inverse is data; its correctness is a theorem. The parameters are arbitrary reals: the mission proves Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain used by the formalization, not a global Lorentzian-manifold theorem and not a statement restricted to the black-hole regime , . The axis is excluded (the inverse carries ) although the metric is smooth there; the loci and are excluded. Nothing is asserted about signature, uniqueness, symmetry of (all sixteen components are proved separately) or any coordinate-independent curvature quantity. A trivialising formalization is ruled out by the goal's first clause: the Ricci tensor of the specification layer takes the inverse as an argument, and the goal certifies that argument.
Independent blind read-back of the definitions and main statements, performed by a separate agent that saw only the Lean text, returned the following honest statement, recorded here verbatim: "For every pair of real numbers , and every point at which , and , all sixteen numbers obtained by evaluating the explicit coordinate formula [...] vanish, where is the explicitly transcribed Boyer-Lindquist Kerr component matrix, is an explicitly transcribed matrix that (by ginv_mul_g_Kerr, under the same hypothesis) satisfies at that point, and is Mathlib's one-variable deriv of the coordinate slice." The two should-fix findings of that read-back (inverse coupling; junk derivative values) are addressed by the first three clauses of the goal.
Infrastructure: three definition bundles (KerrBL_CoordGeometry, hand-written; KerrBL_Kerr_Metric, generated from the source file and human-auditable; KerrBL_Kerr_ClosedForms, generated and untrusted). Reusable beyond the mission: the generic layer, the locality lemma, and the bridge pattern. Natural extensions welcome after release: the two-sided inverse, the reduction to Schwarzschild, and curvature invariants such as the Kretschmann scalar.
Classical Eilenberg correspondence theorems connect algebraic descriptions of finite-state behavior with language-theoretic closure principles. The version developed by Juan Climent Vidal and Enric Cosme Llópez replaces one-sorted monoids by many-sorted algebras, so that operations may accept arguments of several prescribed sorts and return a value of another sort. This is the natural algebraic setting for typed term languages: a signature records the permitted input and output sorts of each operation, and a language is a family of sets indexed by sorts. The paper proves that two ways of organizing finite-state behavior—through finite-index congruences and through regular languages—determine the same ordered structure. The source is the final section of Climent Vidal and Cosme Llópez, Eilenberg theorems for many-sorted formations, published in the Houston Journal of Mathematics 45(2), 2019.
The companion manuscript A Kleene theorem for free many-sorted algebras develops the free-term and recognizability infrastructure used by this formalization. It supplies a concrete Lean representation of sorted signatures, free algebras, homomorphisms, terms, and finite many-sorted carriers. The present mission begins from that reusable core and formalizes the formation-level theorem of the HJM paper, rather than repeating the already completed Kleene development.
Fix a finite type of sorts and an -sorted signature . For an -sorted set , write for the free -algebra on . A congruence on a many-sorted algebra is a family of equivalence relations , one on each carrier sort, compatible with every basic operation. Its index is finite when the entire sorted quotient family
is finite. A sorted language is -saturated when membership in is constant on every -class. The syntactic congruence is the greatest algebra congruence that saturates , and is regular when has finite index.
A finite-index congruence formation selects, for every variable family , a nonempty filter of finite-index congruences on . The selection is closed under intersections, upward inclusion, and pullback along homomorphisms whose composite with the relevant quotient projection is surjective at every sort.
A regular-language formation selects regular languages in each . It contains every language saturated by the universal congruence; whenever it contains every language saturated by ; and it satisfies the corresponding pullback-saturation condition for quotient-surjective homomorphisms.
The two constructions are
and
The capstone is the paper's final formation theorem: the ordered sets of finite-index congruence formations and regular-language formations are order-isomorphic, with the isomorphism fixed to be exactly the two displayed constructions.
The milestones establish the universal property of the syntactic congruence, closure of finite-index congruences under the filter operations, the well-definedness of each construction, and the two recovery identities
These identities determine the inverse maps and prevent the goal from being satisfied by an unrelated abstract order equivalence.
The theorem packages a family of finite quotients and a family of regular languages as interchangeable data. On the algebraic side, closure is expressed by filters of congruences and quotient-surjective pullbacks. On the language side, the same information is expressed through saturation by syntactic congruences. The result therefore gives a systematic translation between quotient-based and language-based classifications in a typed, many-sorted setting.
Formalizing the theorem adds congruence, quotient-index, saturation, syntactic-congruence, and formation interfaces to the existing free many-sorted algebra library. These components are reusable for future formalizations of recognizability, Myhill–Nerode principles, finite algebra formations, and varieties or pseudovarieties of typed algebras. The mathematical theorem is already proved in the cited 2019 paper; the remaining task is to produce machine-checked Lean proofs of the source-faithful statements.
The two maps are simple to write down but their inverse laws are not pointwise tautologies. A finite-index congruence must be reconstructed from the family of all languages it saturates, and a language formation must be reconstructed from all selected finite-index congruences. In the many-sorted case, finiteness applies to the entire quotient family, including its support across sorts, and intersections and pullbacks must preserve this global condition. The quotient-surjectivity premise is also essential: replacing it by ordinary surjectivity of the original homomorphism would change the formation axiom.
The syntactic congruence creates a second layer of care. It must be characterized as the greatest compatible sorted equivalence saturating a language, not merely as the kernel of the language's characteristic function, which need not itself respect the algebra operations. Thus an argument that treats saturation as an arbitrary set-theoretic equivalence misses the algebraic compatibility required by the theorem.
The Lean development uses the existing MSKleene representation of sorted sets, signatures, argument tuples, algebras, homomorphisms, terms, and free algebras. Congruences are sort-indexed setoids with explicit compatibility for every signature operation. Their order is inclusion of relations. Intersection and the universal congruence are concrete constructions, while pullback is defined along an algebra homomorphism.
Finite index is represented by finiteness of the sigma-type of all quotient carriers, matching the paper's finite sorted-set convention; it is not weakened to separate finiteness of each inhabited component. The sort type is assumed finite in the finite-index filter and formation correspondence theorems, as required in the final section of the source. Languages are arbitrary sorted subsets of free term algebras, including empty components. No nonemptiness assumption on variable carriers or algebra sorts is added.
The syntactic congruence is defined internally as the supremum-style least upper bound of all congruences saturating a language, rather than postulated together with its universal property. The formation structures contain only the source closure axioms. In particular, neither correspondence map nor either inverse identity is stored as a structure field; doing so would trivialize the capstone. Contributions are welcome on the foundational universal-property and finite-index lemmas, the two formation constructors, and the recovery identities that assemble into the final order isomorphism.
The third mission in the series formalizing Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) turns to the second main topic of Chapter 1, covering spaces (Section 1.3, pp. 56–78). The first mission used the covering to compute , and the second proved van Kampen's theorem. This mission develops the general theory of covering spaces of a fixed space : the lifting properties (pp. 60–62), the classification of connected covering spaces by subgroups of (pp. 63–68), and deck transformations and group actions (pp. 70–72). Its goal is the classification theorem (Theorem 1.38, p. 67), Hatcher's "Galois correspondence" between path-connected covering spaces of and subgroups of , together with its companions Proposition 1.39 (deck groups and normal covers) and Proposition 1.40 (covering space actions and orbit spaces).
All statements live in the Lean namespace Hatcher used by the earlier missions.
A covering space of (p. 56) is a space with a map such that every has an open neighborhood whose preimage is a disjoint union of open sets each mapped homeomorphically onto ; may be empty, so need not be surjective. This is Mathlib's IsCoveringMap. For a covering space with basepoints we write
for the induced homomorphism (Hatcher.coverHom) and its image (Hatcher.coverSubgroup).
is semilocally simply-connected (p. 63, Hatcher.IsSemilocallySimplyConnected) if each has a neighborhood such that every loop at contained in is null-homotopic in . The bundle Hatcher_Covering also fixes: the structure CoveringSpace X (a total space and a covering map ) and its pointed version PointedCover X x₀ (with and associated subgroup PointedCover.subgroup); isomorphism of covering spaces (p. 67), a homeomorphism with , with or without preservation of basepoints (IsIsomorphic, IsPointedIsomorphic); the deck transformation group (p. 70, deckGroup), the self-homeomorphisms of commuting with ; normal covering spaces (p. 70, IsNormalCover); Hatcher's condition for a covering space action of a group on (p. 72, IsCoveringSpaceAction); and the orbit space with its quotient map (OrbitSpace, orbitProj).
Let be path-connected, locally path-connected and semilocally simply-connected, with basepoint . Then:
Together these say that is a bijection from basepoint-preserving isomorphism classes of path-connected covering spaces to subgroups, inducing a bijection from isomorphism classes to conjugacy classes of subgroups.
The result itself. The classification theorem is the central structural fact about covering spaces: the connected coverings of are "the same as" the subgroups of , with the universal cover corresponding to the trivial subgroup and normal coverings to normal subgroups. Proposition 1.40 is the standard method for computing fundamental groups of orbit spaces (, , lens spaces) and is used throughout Hatcher's later chapters.
Formalizing it. Mathlib (at this environment's revision) already has the lifting theory for covering maps: path and homotopy lifting (IsCoveringMap.liftPath, liftHomotopy), the monodromy action (IsCoveringMap.monodromy), the injectivity of (injective_path_homotopic_map, cited there as Proposition 1.31), the unique-lifting statement (IsCoveringMap.eq_of_comp_eq), and the lifting criterion itself (existsUnique_continuousMap_lifts_of_range_le, cited as Proposition 1.33). For quotient maps by a free properly discontinuous action it has IsQuotientCoveringMap, with the homomorphism and its kernel and surjectivity. Milestones 1, 4, 5 and 16 are therefore expected to be short reductions to Mathlib, and Mathlib's quotient-covering theory should carry most of milestones 14–15. Mathlib has no notion of semilocal simple connectivity, no construction of the universal cover or of the coverings , no classification theorem, and no deck transformation groups or normal coverings; milestones 6–13 and the goal are new.
The heart of the mission is the construction of the universal cover (pp. 63–65): the points are homotopy classes of paths from , the topology is generated by the sets for in the basis of path-connected open sets on which dies, and one must verify that this is a topology basis, that is a covering map, and that the result is simply connected. Proposition 1.36 then passes to a quotient by and checks that the projection remains a covering map. Both are elementary but long, and formalizing them requires a systematic treatment of path homotopy classes as points of a space.
Propositions 1.37 and 1.39 follow from the lifting criterion and unique lifting; the deck-group homomorphism in 1.39(b) sends a loop in to the deck transformation produced by the lifting criterion, and its kernel is computed by Proposition 1.31. Proposition 1.40(a) needs the quotient topology on and the evenly covered neighborhoods from condition ; part (b) is the observation that a deck transformation of a path-connected cover is determined by one value. Milestone 3 is orbit–stabilizer for the monodromy action.
CoveringSpace X bundles a total space in the same universe as with a covering map; the classification quantifies over covering spaces in this sense. Since the universal cover and the coverings are constructed from paths in , they live in that universe, so nothing is lost.MulAut.conj; "number of sheets equals the index" is stated as a bijection with the coset space.Normal instance in the statement; the final clause of 1.39 and 1.40(b) are stated as the existence of group isomorphisms, the latter with its action on prescribed.MulAction.orbitRel.Quotient with the quotient topology.Contributions welcome: a reusable construction of the space of path classes with its topology, the covering , and the deck-group homomorphism; the short reductions to Mathlib for Propositions 1.31, 1.33 and 1.34 are good first contributions.
Mathlib/Topology/Covering/Basic.lean (covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Basic.leanMathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting, monodromy, the lifting criterion). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.leanMathlib/Topology/Covering/Quotient.lean (quotient covering maps for group actions). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Covering/Quotient.leanOnce is known, the next question in Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; pi.math.cornell.edu/~hatcher/AT/AT.pdf) is how to compute fundamental groups of spaces built from pieces. Section 1.2 answers this with van Kampen's theorem (Theorem 1.20, p. 43): if a space is covered by open sets with a common basepoint and path-connected intersections, its fundamental group is the free product of the fundamental groups of the pieces, modulo relations coming from the intersections. It is the main computational tool of Chapter 1: it gives the fundamental groups of wedges of circles, graphs, surfaces, and every CW complex from its 2-skeleton (Propositions 1.26–1.28), and it underlies the classification of covering spaces in Section 1.3.
This is the second mission in the series formalizing Hatcher's book. The first mission established the covering-space lifting properties and in the Lean namespace Hatcher; this one covers the subsection "The van Kampen Theorem" of Section 1.2 (pp. 41–47) together with its warm-up Lemma 1.15 and Proposition 1.14 from Section 1.1 (p. 35).
Let be a topological space with a basepoint . A path is a continuous map , a loop at is a path with both endpoints , and is the group of homotopy classes of loops at under concatenation. A continuous map with induces a homomorphism , .
Let be a family of subsets of , each containing , with the subspace topology; write for . The inclusions induce
which are Hatcher.inclHom, and the inclusions and induce
which are Hatcher.interHomLeft and Hatcher.interHomRight.
The free product of a family of groups is the group of reduced words in the (Hatcher, pp. 41–42); in Lean it is Mathlib's Monoid.CoprodI, here Hatcher.FreeProd. Its universal property extends the to a single homomorphism
Hatcher.vanKampenHom. Since (both are induced by ), the elements
lie in the kernel of . Let be the normal subgroup generated by all of them, Hatcher.vanKampenNormal.
If is the union of path-connected open sets each containing , each is path-connected, and each is path-connected, then
Hence induces an isomorphism .
The result itself. Van Kampen's theorem is the gluing law for . With it Hatcher computes of wedge sums (free products), of graphs (free groups), of the closed orientable surfaces (Example 1.26), and shows that attaching -cells kills exactly the attaching loops (Proposition 1.26), so that every group is a fundamental group (Corollary 1.28). The surjectivity half alone gives Proposition 1.14, that spheres of dimension at least two are simply connected, and hence that is not homeomorphic to for (Corollary 1.16).
Formalizing it. Mathlib has the fundamental groupoid and fundamental group, induced homomorphisms (FundamentalGroup.map), free products of groups (Monoid.CoprodI) with their universal property, normal closures, and quotient groups. It has no version of van Kampen's theorem for topological spaces (its CategoryTheory/Limits/VanKampen concerns colimits in categories, not fundamental groups), and no computation of for ; on the platform, however, the theorem SP4Mission.sphere_simplyConnected (already proved in this environment) states that the unit sphere of is simply connected for , which is Proposition 1.14 with shifted indexing, so that milestone can be closed by a one-line reduction. The mission supplies the statements in Hatcher's form, on Mathlib's , so that later missions (covering spaces, cell complexes) can use them directly.
Surjectivity is a compactness argument: subdivide so each piece of the loop lies in one , then use path-connectedness of the intersections to connect the subdivision points back to . The formal difficulty is bookkeeping: producing the subdivision from an open cover of (Mathlib's exists_monotone_Icc_subset_open_cover_unitInterval is the tool) and showing the reparametrised concatenation is homotopic to the original loop.
The kernel computation is the hard part. Hatcher's proof takes a homotopy between two factorizations, subdivides the square into rectangles each mapped into a single , perturbs the grid so at most three rectangles meet at a corner (this is where triple intersections enter), and then shows that moving the loop across one rectangle at a time changes the factorization only by the two elementary moves that hold in . Every step is elementary, but the induction over the grid is long, and each elementary move requires an explicit path-homotopy in a subspace. The naive idea of proving by an induction on word length does not work: the relation between two factorizations of the same loop is only visible through a homotopy in , not through the words.
Proposition 1.14 is easy given Lemma 1.15 but requires exhibiting the cover of by two complements of antipodal points, showing each is simply connected (homeomorphic to via stereographic projection, which Mathlib has as stereographic), and showing their intersection is path-connected when .
Set X with the subspace topology, and is Mathlib's FundamentalGroup ↥(A α) ⟨x₀, _⟩. Hypotheses are stated explicitly on each theorem: IsOpen, IsPathConnected, ⋃ α, A α = Set.univ, and path-connectedness of pairwise (and, where Hatcher requires it, triple) intersections.List of loops, each tagged with the index of the piece it lies in, concatenated right-to-left with the constant loop as empty product (Hatcher.loopProd). Any bracketing gives the same homotopy class.Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1, and "" is Mathlib's SimplyConnectedSpace (path-connected with trivial fundamental group), which is what Hatcher means since is path-connected.Contributions welcome: the subdivision lemma for loops in an open cover, a reusable treatment of factorizations and their elementary moves, and the two-set special case as a corollary.
Mathlib/GroupTheory/CoprodI.lean (free products of groups). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/GroupTheory/CoprodI.leanMathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (fundamental group and induced homomorphisms). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.leanReflection positivity and infrared bounds form a standard finite-volume route from the geometry of a lattice reflection to quantitative control of long wavelength fluctuations. In the classical argument, reflection positivity supplies a Cauchy--Schwarz inequality for reflected observables, while Fourier diagonalization of the lattice Laplacian identifies the free covariance used in the infrared comparison. These ingredients underlie rigorous results on continuous-symmetry lattice systems in Fröhlich, Simon, and Spencer's development of infrared bounds and spontaneous symmetry breaking (1976), and the general theory of reflection positivity developed by Fröhlich, Israel, Lieb, and Simon (1978). Related technology appears in Fröhlich and Spencer's treatment of the two-dimensional Abelian spin systems and Coulomb gas (1981).
The analytic and model-specific theorems are substantial, but their finite algebraic interface is sharply separable. This mission isolates that interface so later clock, XY, and Gaussian-domination developments can share one checked notion of reflection, one spectral covariance convention, and one treatment of the constant mode.
Let be a finite set of configurations on one side of a reflection plane. A full split configuration is a pair , and reflection exchanges its two entries. A plus-half observable is a function lifted to through the first coordinate. Its reflected copy therefore depends on the second coordinate.
A split weight is specified by a finite feature index , real coefficients , and features :
For a finite family of plus-half observables , the reflected kernel is
A real matrix is positive semidefinite here when it is symmetric and its quadratic form is nonnegative on every real coordinate vector.
The spectral side uses a finite mode set with a distinguished zero mode . An infrared spectrum consists of a function that is nonnegative and vanishes exactly at . For , the free mode covariance is diagonal, equals zero at the constant mode, and has entry
away from zero. Covariance domination is tested only on source vectors whose zero-mode coordinate vanishes. The concrete spectral fixture is the periodic square lattice, with tensor-product discrete Fourier modes and the nearest-neighbor graph Laplacian.
The first target identifies the split reflection pairing with the explicit double sum over the two halves. Under , the resulting reflected kernel must be positive semidefinite:
Every such kernel must satisfy the two-observable chessboard inequality
For every Torus-4 frequency and site , the registered Fourier mode must satisfy the pointwise eigenvalue equation
The eigenvalues must be nonnegative and vanish exactly at the constant mode, and these laws must be packaged as the same spectrum type consumed by the infrared definitions.
The diagonal free covariance must be positive semidefinite for . If an interacting covariance is quadratically dominated by on sources with , then every nonzero Fourier mode must satisfy
Two finite counterfixtures are part of the target. They assert that an arbitrary full-vertex reflected two-point matrix need not be positive semidefinite, and that domination restricted away from the zero mode need not extend to full-matrix domination.
The resulting interface prevents three substitutions that otherwise look
notational but change the theorem. Reflection positivity is tested on
observables supported on one half rather than on an arbitrary matrix indexed
by all vertices. The infrared comparison excludes the constant mode rather
than forcing a fluctuating zero mode below a covariance with zero diagonal.
The graph-Laplacian eigenvalue is connected to the Fourier mode by an explicit
pointwise theorem rather than by assigning a function the name
laplacianEigenvalue.
Several ingredients already have machine-checked Lean proofs in the LeanProofs repository: the finite matrix Cauchy--Schwarz theorem, the Torus-4 DFT diagonalization and zero-mode theorem, and the diagonal free-covariance calculation. This mission reorganizes those results around a corrected consumer boundary and adds the split-half and off-zero adapters. It does not present the finite statements as new mathematics.
The main difficulty is maintaining the correct domain at each interface. A reflection of lattice sites does not by itself imply positive semidefiniteness of a correlation matrix indexed by every site; the tested observables and their support are part of the assertion. Likewise, a free covariance whose constant-mode entry is defined to be zero cannot dominate an arbitrary covariance on all source vectors. Finally, a Fourier multiplier used for a pseudospectral derivative is not automatically the eigenvalue of the nearest-neighbor graph Laplacian. The formal statements must keep these three objects distinct.
All configuration, feature, observable, and mode types are finite. Kernels, weights, coefficients, source vectors, and quadratic forms are real. Complex numbers occur only in the explicit discrete Fourier modes. Reflected pairings are unnormalized finite sums; no partition function or probability measure is introduced. The inverse temperature satisfies . The distinguished zero mode is part of the spectrum interface, and infrared domination is restricted to source vectors that vanish at that coordinate.
The mission does not assert reflection positivity of a clock or XY Gibbs measure, nonnegative Fourier coefficients of a physical cross-bond weight, Gaussian domination, a thermodynamic limit, a Kosterlitz--Thouless transition, or a universal jump. It also does not identify the Torus-4 graph spectrum with the Grid3 pseudospectral multiplier from the Fourier--Hodge packet. Those are separate future missions requiring additional model and analytic input.
The reusable outputs are the split-weight RP interface, the finite positive-semidefinite kernel API, the typed spectrum object, and the zero-mode-restricted domination predicate. Contributions should preserve the explicit half support and zero-mode restrictions; a proof obtained by adding the desired conclusion as a hypothesis is outside scope.
ReflectionPositivityInfraredBound.lean, exact repository
snapshot dbf503b2909cc17787d40a21eb75a0c9354cc6ef.
https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.leanKleene's theorem (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the regular ones — those built from finite languages by union, concatenation, and the Kleene star. Mezei and Wright (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra recognizable when it is the preimage of a subset of a finite algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of recognizable tree languages and finite tree automata of Gécseg and Steinby (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.
Many computational structures are inherently many-sorted: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (CVCL20), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the regular side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.
Fix a finite set of sorts . An -sorted set is a family of sets; it is finite when is finite. An -sorted signature assigns to each pair a set of operation symbols of arity and coarity . A -algebra is an -sorted set together with, for each , an operation , where . A homomorphism commutes with all operations sortwise.
The free -algebra on an -sorted set of variables has as its sort- carrier the set of -terms; every -sorted map extends uniquely to a homomorphism . Following automata-theoretic tradition, subsets of are called languages. For a sort , a language is -recognizable when there are a finite -algebra , a homomorphism , and a subset with . Write for the set of all such .
Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable and a language , -substitution replaces, in every term of an input language of sort , each occurrence of independently by a term of . The -iteration is , where and . For a finite -sorted set , the regular signature expands by an empty constant , a binary sum , a unary -iteration for each , and a -substitution operation for each . Its terms are the regular expressions over ; the power algebra carries a canonical -algebra structure, and interpreting a regular expression there yields a language . A language is -regular when for some finite and some regular expression of type ; write .
The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite , every finite -sorted signature , and every finite -sorted set . It splits into (Corollary 4.8) and (Proposition 4.10).
The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of , plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a -algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.
The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.
The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a sortwise budget: an -sorted family recording, for each sort , the set of state values still admissible at internal subterms. The induction is on , and each step removes the top state of one chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).
Proposed Lean representation: a type with [Fintype S]; an -sorted set as S → Type; a signature as a family List S → S → Type with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort- carrier Set (T_Σ Z s); -recognizability as the existence of a finite -algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: finite throughout; finite and finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly together with the operations of — not an unrestricted Boolean or closure algebra, which would trivialize the statement.
A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and -recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.
Searching an unsorted list of items for a single marked entry takes queries classically — there is no way to do better than checking items one at a time. Grover's algorithm (Grover 1996) shows that a quantum computer solves the same problem in queries, a quadratic speedup that applies to any problem expressible as unstructured search over a black-box oracle (this includes brute-forcing NP-complete problems and inverting one-way functions, which is why post-quantum cryptography doubles key lengths to compensate). Unlike Shor's algorithm, Grover's algorithm is provably optimal: Bennett–Bernstein–Brassard–Vazirani (1997) showed queries are necessary for any quantum algorithm solving unstructured search, so the quadratic speedup is the best any quantum algorithm can achieve on this problem.
Model an -item database as the standard basis of (EuclideanSpace ℂ (Fin N)),
with inner product . Fix a marked index
. The algorithm starts in the uniform superposition
a unit vector assigning equal amplitude to every item. Two reflections drive the search:
One Grover iterate is . The algorithm applies some number of times to and measures; a measurement outcome equal to counts as success.
and are each reflections about a unit vector, hence isometries; their composition is therefore norm-preserving on the whole space, not just at — the minimal fact needed for to be a legitimate quantum operation.
The geometric heart of the algorithm (Nielsen & Chuang, Quantum Computation and Quantum Information, Section 6.1.2): restricted to the real two-dimensional subspace spanned by and the component of orthogonal to it, acts as rotation by a fixed angle . Each iterate therefore advances the amplitude on the marked state along , exactly as claimed, with the rotation's initial offset (since at ).
Some number of iterations drives the probability of measuring the marked item above . The goal is stated existentially, without fixing to a specific rounded formula: the rotation angle can be made to land within of by an appropriate integer , and at that point . Pinning down to an explicit closed form (e.g. the nearest integer to ) is one valid strategy, but is not required by the statement — any correct choice of , and any correct proof it works, closes the goal.
Grover's algorithm is the second landmark quantum algorithm after Shor's, and the one with the
widest applicability: because it treats the search space as a black box, it accelerates any
brute-force search — SAT solving, collision finding, and generic key search among them — which is
the concrete reason NIST's post-quantum cryptography standards double symmetric key lengths rather
than replacing them outright. The mathematics itself has been fully settled since 1996, including
matching optimality lower bounds; nothing here is open. What this mission adds is a machine-
checked derivation of the amplitude formula and success bound directly from the definitions of
the oracle and diffusion operators as concrete linear operators on EuclideanSpace ℂ (Fin N) —
Mathlib has the finite-dimensional inner product space and rank-one operator machinery this needs
(InnerProductSpace.rankOne, EuclideanSpace.single), but no existing formalization of the
algorithm itself.
The obvious first attempt tries to track the full -dimensional state vector through iterations. This is intractable in general: 's action on an arbitrary basis vector depends on its overlap with both and . The move that makes the problem tractable is recognizing that preserves the two-dimensional real subspace — everything orthogonal to this plane is fixed by both and , and inside the plane is exactly a rotation matrix by angle . Establishing this invariance and then tracking only the rotation angle (rather than the full vector) is the standard reduction, and the one this mission's milestones are built around; skipping it and attempting a direct -dimensional induction does not scale.
Works over a general together with a marked index — no
assumption that is a power of two, since the rotation argument is agnostic to how the basis
states are physically encoded into qubits (that encoding is a separate, unrelated concern from the
search dynamics proved here). Supplying w0 : Fin N already forces ; no separate
nonemptiness hypothesis is added. The oracle and diffusion operators are built directly from
Mathlib's InnerProductSpace.rankOne rather than an ad-hoc pointwise definition, so their
reflection structure (and hence unitarity) is visible from the definition itself. A trivializing
formalization is ruled out explicitly: the goal is stated as an existential over rather than a
fixed closed-form iteration count, so a correct proof must still exhibit a genuine successful
and establish the bound — it cannot be discharged by an unrelated or degenerate choice. Contributions
extending this to multiple marked items, or proving the matching lower bound
(Bennett–Bernstein–Brassard–Vazirani 1997), are welcome as follow-up missions.