Skip to content

What we left out and why

The library was written alongside a large collection of mathematics manuscripts, the math catalog, and uses only a dozen of its results. If you have read about a striking result in the catalog and wondered why the library does not use it, or a reviewer proposes adding one, this page gives the answer: the test a result must pass to affect a decision, the notable results that failed it, and what adding one would take.

It assumes you know what the catalog is and what "catalog result N" means; if not, read How to read these pages first.

The test

A catalog result is used only if it changes something a product can do within months to about two years. Three questions, in order:

  1. Does it change a decision? It must give an algorithm the library can run on realistic inputs in request time, a limit the library can enforce (a cap, a frozen approximation factor), or a reason to refuse a request. A result whose only honest use is a footnote stays out.
  2. Is its constant usable as a promise? A guarantee of \(2^{-310}\) of the best value, or a factor of \(10^{12}\), is true (if the result is) and useless to a customer. Such a constant may be reported next to a practical rule, labelled as unused; it is never put in Limits or presented as a guarantee.
  3. Is it sound to run? A procedure with a known counterexample is banned, not merely unused.

One that passed: Kesten–Stigum reconstruction (catalog result 229) gives a one-line test, \(d\lambda^2 > 1 + m\), that runs in constant time and changes whether a decision acts. One that failed: three-machine scheduling (result 124, below) claims a polynomial-time algorithm whose own manuscript says it supplies no practical performance guarantee.

Results left out

Each row gives the published status alongside the catalog's claim, as on every theory page: the catalog's claim is reported, neither endorsed nor dismissed.

Catalog result What it is about In the wider literature Catalog claim Why the library leaves it out
175, Talagrand's expectation-threshold questions How far apart two ways of measuring when a random set family appears can be Posed by Talagrand (2010) as conjectures; parts of that programme have since been proved (for example Park and Pham, 2022). We have not checked whether these exact statements are published. The two thresholds differ by at most a factor \(25\cdot512^4 \approx 1.72\times10^{12}\); a related cover statement with \(k = 2^{75} \approx 3.78\times10^{22}\) sets. Lean statement, per the manuscript. A factor of \(10^{12}\) and \(2^{75}\) sets change no decision; the knife-edge check already reports one vacuous width (result 186).
124, three-machine unit-job scheduling Jobs of unit length with precedence constraints on three identical machines: minimize the finishing time Open: whether this is solvable in polynomial time is a long-standing open problem from Garey and Johnson's list. A deterministic polynomial-time algorithm. Lean statement covering a machine whose running time is polynomially bounded. The manuscript itself says the proof "supplies no practical performance guarantee" (it uses a fixed leaf allowance of 10,000 and a very large exponent). A polynomial is not a running time.
120, maximum matching in almost-linear time Largest set of disjoint edges in a general graph, in time \((n+m)^{1+o(1)}\) Bipartite graphs: almost-linear time is a theorem (through almost-linear maximum flow, Chen, Kyng, Liu, Peng, Probst Gutenberg and Sachdeva, 2022). General graphs: the classical bound is \(O(m\sqrt n)\) (Micali and Vazirani); almost-linear time is not established, to our knowledge. A randomized almost-linear algorithm for general graphs and for \(f\)-factors. This package records no reference saying how it is checked. The leading constant is unspecified, and no implementation exists that beats standard matching code at the sizes the library sees. The library needs only a maximal matching (for the Vertex Cover 2-approximation, result 102).

Results used only as reported numbers

Two catalog constants appear in the library's output but never decide anything. They are listed here because people try to promote them.

Catalog result Constant Where it appears What decides instead
186, sharp-threshold width \(2^{19}\log(1/(2\varepsilon))/(\log n)^2\), larger than 1 for every \(n\) below about \(10^{399}\) theorem_width on every knife-edge check record The same formula with prefactor 2, a hand-chosen dead band (Knife-edge densities)
111, one-sample matroid prophet inequality \(2^{-310} \approx 4.8\times10^{-94}\) lean_factor on every prophet helper result Single-item threshold rules: the max-of-samples bar with its proven 1/2 in expectation, or a scalar bar with no factor (One slot, no take-backs)

A banned procedure

Truffet's tropical-elimination step for mean-payoff games is not "unused": it is banned. The catalog (result 104) records a finite counterexample, with a Lean statement, in which a two-step run of the step ends with a feasible but not optimal answer. The game check never runs it; it uses Karp's mean-cycle algorithm, which takes \(O(n\,\lvert E\rvert)\) time on a chart with \(n\) states and \(\lvert E\rvert\) transitions, capped at 200 states. The catalog reference REF_TRUFFET_BAN is attached to the game check so the absence is visible in every record. See Workflows that keep going.

Banned, unused and reported: the difference

Kind Meaning In certificates.py? Example
Used Runs, or enforces a limit or refusal Yes 229, 134, 004
Reported Appears in output as a labelled, unused number Yes, with a note saying it is not a guarantee 186 width, 111 factor
Unused Not imported at all No 175, 124, 120
Banned Known to be unsound; never run Yes, so the ban is auditable Truffet step (104)

"Unused" never means "false". It means the result cannot change a decision today.

What adding a result requires

src/grounded_decision/certificates.py is the allow-list: a result not listed there cannot appear on any record. To add one:

  1. A CatalogRef with the result number, a title, lean (whether a Lean statement exists) and a note stating exactly what the library claims from it, including any gap (stand-in, frozen factor, refusal, unused constant).
  2. Code that implements or enforces it, or an explicit refusal.
  3. A test that locks the behaviour (tests/test_router_compare.py and tests/test_docs.py are the models; the latter fails if a catalog result in certificates.py is missing from these pages).
  4. A theory page in this section with the "Where this result stands" box, and a row in Where each result stands.
  5. A runnable example.

Do not add a reference whose only content is a constant no product can use. Do not put such a constant in Limits.