Skip to content

Where each result stands

Before you rely on a check or quote a number from these pages, you need to know three things about the mathematics behind it: is it an established theorem, an open problem, or true only if a famous conjecture is true; what does this project's own math catalog claim about it; and how much of either does the code actually use. This page answers those three questions for every result the library touches, in one place.

It is written for engineers, data scientists and researchers who want the exact guarantee. The terms "catalog result", "Lean statement" and the trust levels are explained in How to read these pages; the plain-language versions of the checks are in the checks.

How to read the table

Each row has five parts:

  • Plain question: what the result answers, in product terms.
  • Wider literature: what is published and broadly accepted, tagged theorem, open, or assuming UGC (true if the Unique Games Conjecture holds; that conjecture is itself open). References are to the standard papers, so you can check them.
  • Catalog claim: what this project's companion math catalog states, and how it is checked: Lean (a formal statement exists in the catalog, which is kept outside this repository) or manuscript (a written manuscript only). Several catalog claims would settle problems the wider literature regards as open. They are reported here as claims of this catalog, neither endorsed nor dismissed.
  • What the code uses: what actually runs, which is usually much narrower than either.
  • Trust tag: the trust value the library writes into records, or "not a check" for helpers you call yourself.

The code relies on less than the catalog claims

No decision in this library depends on any catalog claim being true beyond what is listed under "What the code uses". In particular, the library never runs Lean, never uses a catalog constant as a service guarantee, and holds a decision whenever a check fails, so a mistaken catalog claim can make the library more cautious than necessary but cannot by itself make it act.

Summary

Result (catalog N) Plain question Wider literature Catalog claim What the code uses Trust tag
Kesten–Stigum reconstruction (229) Do the related cases carry enough signal to recover the hidden label? Theorem above the line \(d\lambda^2>1\), every \(q\). That nothing can be recovered below it: theorem for \(q=2\); known only in some regimes for \(q=3,4\); false for \(q\ge5\). Exact line for 3-state symmetric and 4-state ferromagnetic channels, including at equality. Lean covers the 3-state "above the line" direction only. Passes when \(d\hat\lambda^2 > 1.05\), with \(d\) the mean degree of your graph and \(\hat\lambda\) from edge agreement. lean on pass, paper on hold
Sharp thresholds (186) Is the evidence density so close to the cut-off that noise could flip the answer? Theorem: window width \(O(\log(1/\varepsilon)/\log n)\) (Friedgut–Kalai) and \((\log n)^{-2+o(1)}\) for graph properties (Bourgain–Kalai). Width \(O((\log n)^{-2})\): open. Width at most \(2^{19}\log(1/(2\varepsilon))/(\log n)^2\) for every relabeling-invariant increasing graph property. Lean. Reports that width (larger than 1, so vacuous, at every practical \(n\)); decides with prefactor 2 instead, centred on your cut-off. operational in practice
Conformal prediction (no catalog result) Is this case unusual compared with recent cases? Theorem: split-conformal p-values are valid when the cases are exchangeable. None. \(p = (1+\#\{s_i \ge s\})/(1+n_{\mathrm{cal}})\); passes when \(p > 0.10\). operational
Star height (134) Is the policy's loop structure simple enough to audit? Generalized star-height problem: open (no language is known to need height 2). Ordinary star height: decidable, unbounded (theorem). Every regular language has generalized star height at most 3. Lean. Rejects a policy whose written expression nests more than 3 stars. Never rewrites. lean
Parity and mean-payoff games (104) Can the workflow keep running forever without being trapped? Zielonka's algorithm and Karp's mean-cycle algorithm: theorem. Parity games in quasipolynomial time: theorem. Two-player mean-payoff games in polynomial (or quasipolynomial) time: open. Deterministic quasipolynomial algorithms for mean-payoff, stochastic and parity games; a counterexample to Truffet's elimination step. Lean covers the counterexample and a randomized algorithm. One-player games only, solved exactly. A built-in "stay put" move makes the check pass whenever an even-priority state is reachable. lean on pass, operational on hold
Max-Cut and Vertex Cover limits (102) Should we fund a search for a better worst-case approximation? Unique Games Conjecture: open (the related 2-to-2 theorem is proved). Beating 0.8786 for Max-Cut or 2 for Vertex Cover is hard assuming UGC; unconditionally NP-hard only beyond 16/17 and below \(\sqrt2\). Proves the Unique Games Conjecture and direct NP-hardness reductions for both thresholds. Lean. Spectral cut plus local search (at least half the edges), matching-based 2-approximation; records 0.8786 and 2 as reference values, not guarantees of this code. not a check
Metric k-median (125) What worst-case factor may we promise when opening \(k\) sites? No polynomial algorithm beats \(1+2/e\approx1.736\) (theorem, under a standard complexity assumption). No known polynomial algorithm achieves it; published polynomial ratios are well above it. A polynomial \((1+2/e+\varepsilon)\)-approximation. Manuscript (pin lean=False; a Lean statement covers a related recovery result). Reports 1.736 as a floor: never claim a better worst-case factor. Runs no k-median algorithm. not a check
Weisfeiler–Leman (133) How strong a graph fingerprint can we afford? \(k\)-WL runs in about \(n^{k+1}\log n\) time for fixed \(k\) (theorem); some graphs need \(k\) linear in \(n\) (theorem). Complexity with \(k\) as input: not settled, to our knowledge. EXPTIME-complete when \(k\) is part of the input; unconditional \(n^{ck}\) time lower bounds. Lean. Caps \(k\) at 2 as a cost budget; refusals are labelled exptime_trap, meaning "too expensive under our budget". not a check
Courtade–Kumar (119) Which one-bit summary of noisy bits keeps the most information? Open conjecture; proved for very noisy channels. A single coordinate attains the bound. Proves the conjecture. Lean. Picks the column that agrees most with your target. Needs no theorem for a single-label target. not a check
Brenier map stability (374) Did the outcome distribution move more than we can tolerate? Hölder stability of optimal-transport maps is theorem for some exponents; the sharp exponent is not settled, to our knowledge. Exponent \(1/3\) is sharp in dimension 2 and higher; square-root stability fails. Lean. One dimension only, where map error equals \(W_2\) exactly; the gate is \(W_2 \le \texttt{scale}\cdot\tau^3\), a hand-set budget. not a check
Contingency tables (115) Is the A/B lift real, given the totals? Fisher's exact test and permutation tests: theorem. Uniform sampling and approximate counting of tables with arbitrary margins in polynomial time: open beyond a fixed number of rows. Exact uniform sampling and approximate counting for arbitrary margins. Lean. Two-row tables: exact hypergeometric draws (the Fisher null, not uniform). Larger tables: a switch chain with no certified mixing. not a check
Prophet inequalities (111) One slot, irrevocable choices: how much value can a simple rule keep? Single item: ratio 1/2 with known distributions, or with one sample from each distribution (theorem). One sample per element for every matroid against an adversary that sees everything: not established, to our knowledge. Constant \(2^{-310}\) for every matroid, one sample per element, almighty adversary. Lean. Single item; threshold is one scalar sample. No worst-case ratio is guaranteed for this rule; 0.5 is reported as the classical benchmark. not a check
Hilbert's tenth problem over the rationals (004) Can any procedure decide whether a polynomial has a rational root? Over the integers: no (theorem, Matiyasevich). Over the rationals: open. No such algorithm exists. Manuscript (pin lean=False). The router refuses the request; nothing is attempted. not a check

The sections below give each row in more detail, with references.

Kesten–Stigum reconstruction (229)

  • Wider literature. On a tree where each case copies its parent's label through a noisy symmetric channel with correlation \(\lambda\), the root can be partly recovered from distant cases whenever \(d\lambda^2 > 1\) (Kesten and Stigum, 1966; the "census" estimator). This direction holds for every number of labels \(q\). The converse, that nothing can be recovered when \(d\lambda^2 \le 1\), is a theorem for \(q = 2\) (Bleher, Ruiz and Zagrebnov, 1995; Evans, Kenyon, Peres and Schulman, 2000). For \(q = 3\) and \(q = 4\) it is known only in some regimes, for example large degree (Sly, 2009). For \(q \ge 5\) it is false: recovery is possible below the line (Mossel, 2001; Sly, 2009).
  • Catalog claim. The exact threshold \(d\lambda^2 > 1\), with non-reconstruction at equality, for 3-state symmetric and 4-state ferromagnetic channels on regular and Poisson trees. The Lean statement covers the 3-state "above the line" direction only.
  • Code. reconstruction_report passes when \(d\hat\lambda^2 > 1 + m\) with \(m = 0.05\). \(d\) is the mean degree of your related-cases graph (not a tree's branching number), and \(\hat\lambda = (q\,p_{\mathrm{same}} - 1)/(q - 1)\) from the fraction of linked pairs that agree. It measures how informative the related cases are, not which outcome they support.

Sharp thresholds (186)

  • Wider literature. For a monotone property invariant under relabelling, the probability of the property rises from \(\varepsilon\) to \(1 - \varepsilon\) across a window of width \(O(\log(1/\varepsilon)/\log n)\) around the property's own critical probability (Friedgut and Kalai, 1996). For graph properties, Bourgain and Kalai (1997) improved this to \((\log n)^{-2+o(1)}\). A width of order \((\log n)^{-2}\) is conjectured and open.
  • Catalog claim. The \((\log n)^{-2}\) width with explicit constant \(2^{19}\), Lean.
  • Code. The window is centred on your cut-off \(p^\star\), a policy choice, not on a critical probability, and uses prefactor 2: \(w = 2\log(1/(2\varepsilon))/(\log n)^2\) with \(\varepsilon = 0.1\). The check holds when \(\lvert\hat p - p^\star\rvert \le \tfrac12\min(w,1)\). This is a dead band shaped like the theorem, not the theorem applied.

Conformal prediction (no catalog result)

  • Wider literature. If the calibration scores and the new case's score are exchangeable, the split-conformal p-value is valid: \(\Pr(p \le \alpha) \le \alpha\) (Vovk, Gammerman and Shafer, 2005; Papadopoulos and co-authors, 2002).
  • Code. An empty calibration set gives \(p = 1\) and passes, unless Limits(require_conformal_calibration=True), which holds instead. With \(\alpha = 0.10\), a hold is possible only when \(n_{\mathrm{cal}} \ge 9\).

Star height (134)

  • Wider literature. Star height counts nested Kleene stars. Ordinary star height (no complement) is unbounded (Eggan, 1963; Dejean and Schützenberger, 1966) and decidable (Hashiguchi, 1988). With complement allowed ("generalized"), it is open whether any regular language needs height 2 or more.
  • Catalog claim. Every regular language has a generalized expression of star height at most 3, Lean.
  • Code. Computes the height of the expression as written and rejects the policy at compile time above max_star_height = 3. The cap keeps policies readable; it does not make compilation faster, and the code never searches for a lower-height equivalent.

Parity and mean-payoff games (104)

  • Wider literature. Zielonka's recursive algorithm (1998) solves parity games exactly in exponential worst-case time; parity games are solvable in quasipolynomial time (Calude, Jain, Khoussainov, Li and Stephan, 2017). Karp's algorithm (1978) finds the maximum mean cycle in \(O(n\lvert E\rvert)\) time, which solves one-player mean-payoff games. Two-player mean-payoff games are in NP ∩ coNP; a polynomial algorithm is open.
  • Catalog claim. Deterministic quasipolynomial algorithms for mean-payoff, stochastic and parity games; a finite counterexample to a step of Truffet's tropical elimination. Lean covers the counterexample and a randomized quasipolynomial algorithm.
  • Code. Compiles a policy chart to a game (states marked environment=True belong to the environment; only final states get a self-loop), solves parity with Zielonka and one-player mean payoff with Karp, separately. Text policies get priority 2 on states that propose an action or have no way out and 1 elsewhere, so a policy that can loop forever without proposing anything fails. The check assumes the service sends the right event in the states it controls, and the payoff part is best-case. Truffet's step is never used.

Max-Cut and Vertex Cover limits (102)

  • Wider literature. Goemans–Williamson (1995) achieves 0.8786 for Max-Cut. Doing better is NP-hard beyond 16/17 (Håstad, 2001) and hard up to 0.8786 assuming UGC (Khot, Kindler, Mossel and O'Donnell, 2007). For Vertex Cover, any maximal matching gives a factor of 2; doing better than 2 is hard assuming UGC (Khot and Regev, 2008), and NP-hard below \(\sqrt2\) (Khot, Minzer and Safra, 2018). The Unique Games Conjecture is open; the related 2-to-2 Games Theorem is proved (Khot, Minzer and Safra, 2018).
  • Catalog claim. A proof of the Unique Games Conjecture, plus direct NP-hardness reductions for Max-Cut beyond 0.8786 and Vertex Cover below 2, Lean.
  • Code. Max-Cut: top Laplacian eigenvector plus local search, which guarantees at least half the edges are cut. Vertex Cover: both ends of a maximal matching (factor 2; on bipartite graphs an exact answer is available in polynomial time by König's theorem, which this code does not use). 0.8786 is recorded as a reference value only.

Metric k-median (125)

  • Wider literature. No polynomial algorithm achieves a factor below \(1 + 2/e \approx 1.736\) unless a standard complexity assumption fails (Jain, Mahdian and Saberi, 2002). That is a lower bound: no known polynomial algorithm achieves it. A \((1+2/e+\varepsilon)\) factor is known in time exponential only in \(k\) (Cohen-Addad and co-authors, 2019).
  • Catalog claim. A polynomial-time \((1+2/e+\varepsilon)\) algorithm for metric k-median with candidate facilities. Manuscript; the pin is lean=False.
  • Code. k_median_note() returns 1.736 as a floor. Never publish it as an achievable ratio.

Weisfeiler–Leman (133)

  • Wider literature. \(k\)-dimensional Weisfeiler–Leman refinement runs in about \(n^{k+1}\log n\) time for fixed \(k\) (Immerman and Lander, 1990), so it is polynomial for every fixed \(k\). Some non-isomorphic graphs are told apart only when \(k\) grows linearly with \(n\) (Cai, Fürer and Immerman, 1992), and the number of refinement rounds can be \(n^{\Omega(k)}\) (Berkholz and Nordström, 2016).
  • Catalog claim. With \(k\) given in binary as part of the input, WL equivalence and identification are EXPTIME-complete; for large fixed \(k\), any algorithm needs \(n^{ck}\) time. Lean.
  • Code. max_wl_k = 2. Cost grows like \(n^{k+1}\), so the cap is a budget. The refusal label exptime_trap names the router's envelope, not an EXPTIME-hardness result for fixed \(k\).

Courtade–Kumar (119)

  • Wider literature. For uniform bits \(X\) and a copy \(Y\) with each bit flipped independently with probability \(\varepsilon\), the conjecture says every Boolean function satisfies \(I(f(X);Y) \le 1 - h_2(\varepsilon)\) (Courtade and Kumar, 2014). A single coordinate achieves equality. It is open in general and proved for high noise (Samorodnitsky, 2016).
  • Catalog claim. A proof of the conjecture and of the related Hellinger conjecture, Lean.
  • Code. best_coordinate returns the column with the highest agreement with your target (or its complement). The advice "keep a coordinate, do not train a one-bit mixer" is licensed only in the conjecture's setting: uniform independent bits and a target that is the noisy copy of the whole vector.

Brenier map stability (374)

  • Wider literature. The optimal-transport (Brenier) map from a fixed source depends Hölder-continuously on the target in \(W_2\); published exponents include \(1/6\) and improvements under extra assumptions (Mérigot, Delalande and Chazal, 2020; Delalande and Mérigot, 2023). The sharp exponent is not settled, to our knowledge.
  • Catalog claim. For a uniform source on a convex body in dimension 2 or more, map error is at most \(C\,W_2^{1/3}\), and no larger exponent works, Lean.
  • Code. Works in one dimension, where the map error equals \(W_2\) exactly, so the 1/3 exponent plays no mathematical role. The gate is \(W_2 \le \texttt{scale}\cdot\tau^3\) (6.25 with the example's scale=50, tau=0.5): a hand-set budget.

Contingency tables (115)

  • Wider literature. Conditioning on both margins, the null distribution of a two-row table is hypergeometric (Fisher's exact test). Counting tables with given margins is #P-hard; polynomial uniform sampling and approximate counting are known for a fixed number of rows (Dyer, Kannan and Mount, 1997) and open for arbitrary margins.
  • Catalog claim. Exact uniform sampling in expected polynomial time and an approximation scheme for counting, for arbitrary margins, Lean.
  • Code. Two-row tables: sequential hypergeometric draws, mixer_status="exact_hypergeometric". That is the Fisher exact test / permutation null, not the uniform distribution on tables. Larger tables: a switch chain whose stationary law is uniform but whose mixing is not certified (not_paper_fpras).

Prophet inequalities (111)

  • Wider literature. One item, values arrive one at a time, choices are final. With known distributions, a single threshold earns at least half the expected maximum (Krengel and Sucheston, 1977; Samuel-Cahn, 1984). With one sample from each distribution, using the largest sample as the threshold also earns half (Rubinstein, Wang and Weinberg, 2020). Matroids with known distributions: half (Kleinberg and Weinberg, 2012).
  • Catalog claim. One sample per element suffices for every matroid, against an adversary who sees all samples, values and random seeds, with factor \(2^{-310}\), Lean.
  • Code. single_item_max_of_samples sets the bar at the largest of one past sample per arrival and takes the first value at or above it: the Rubinstein–Wang–Weinberg rule, so factor_claimed=0.5 holds in expectation under that theorem's assumptions (proof in the module docstring). single_item_one_sample uses one scalar threshold (for example yesterday's median); that rule has no worst-case ratio (values that are large with small probability defeat it), so it reports factor_claimed=None. Neither uses the catalog's matroid factor.

Hilbert's tenth problem over the rationals (004)

  • Wider literature. No algorithm decides whether an integer polynomial has an integer root (Matiyasevich, 1970, completing work of Davis, Putnam and Robinson). Whether one exists for rational roots is open.
  • Catalog claim. No algorithm exists for rational roots either. Manuscript; the pin is lean=False.
  • Code. dispatch refuses the rational_zeros subgoal. The refusal does not depend on the catalog claim: even if an algorithm existed, an unbounded search has no place in a request path.

Next