Skip to content

How to read the theory pages

The theory pages explain which mathematical result sits behind each check and helper in this library, what that result actually says, and how far the code departs from it. They use a little shared notation and two kinds of "status" (what the wider literature knows, and what this project's own math catalog claims). This page explains both once, so the result pages can stay short. Read it before your first result page, or come back to it when a symbol or a trust level is unclear.

It assumes you have met the six checks in plain words; if not, start with the checks in plain language.

How each result page is laid out

Every result page follows the same order, so you can skip to the part you need:

  1. The question, in plain words, and the product situation where it comes up (a fraud ring, a pager rota, an A/B test).
  2. Intuition: a picture or a tiny example small enough to check by hand.
  3. A worked example with numbers copied from running the code. The page names the command, usually uv run grounded-decision examples <id>, so you can reproduce it.
  4. The precise statement: the theorem as the literature states it, with its hypotheses, followed by what this project's catalog claims and how that claim is checked. A box titled "Where this result stands" keeps the two apart.
  5. What the code does, and every way it differs from the theorem. This is the section to read if you rely on the behaviour.
  6. Limits: when the difference matters in practice, and how to choose the parameters (with a link to Choose parameters).
  7. Cross-links to the plain-language concept page, the example case pages, and the API reference.

Sections 1–3 need no mathematics beyond school algebra. Section 4 assumes probability, graphs and algorithms at the level of a first graduate course.

What "catalog result N" means

This library was written alongside a large companion collection of mathematics manuscripts, which these pages call the math catalog. It is the companion math catalog, kept outside this repository: it holds the manuscripts and, for many results, a formal statement written in the Lean proof assistant. Each result in the catalog has a three-digit number, for example 229. In code that number is called the family.

Only a handful of catalog results affect this library. Each one is recorded in src/grounded_decision/certificates.py as a CatalogRef (informally, a "pin"): the result number, a title, whether a Lean statement exists (lean=True), and a one-line note saying what the library is allowed to claim from it. A result that is not in that file has no effect on any decision. The full list of pins, with where each one is used, is on the overview.

When a page writes "Kesten–Stigum reconstruction (catalog result 229)", it means: the classical result is Kesten–Stigum reconstruction, and the catalog's version of it is result 229. The two are often not the same statement; the next section explains why that matters.

Two kinds of status

Many catalog results go beyond what is established in the published mathematical literature. Some claim to settle problems that the wider community regards as open (for example the generalized star-height problem, the Courtade–Kumar conjecture, or the Unique Games Conjecture). These pages never present such a claim as settled mathematics, and never dismiss it either. Each result page carries a box with two separate sentences:

In the wider literature: what is published and broadly accepted, with its status: a theorem, an open problem, or a result that holds assuming a conjecture (for example "assuming the Unique Games Conjecture").

In this project's math catalog (result N): what the manuscript claims, and how it is checked: a Lean statement (a formal statement of the result exists in the catalog), or manuscript only.

Then a third sentence says what the library actually relies on, which is usually much less than either. For example, the threshold check reports the catalog's window width but never uses it to make a decision, because that width is larger than 1 at every realistic size.

Where each result stands puts all of these side by side in one table.

Trust levels

Every check result in a DecisionRecord carries a trust field. It says how much of a mathematical result that particular check outcome leans on.

Trust level Field value What it means for you
proven lean The check's outcome matches a statement for which the catalog has a Lean statement. The library does not run Lean, at compile time or at decision time; the tag is a pointer to that statement, not a proof that your data meets its hypotheses.
published paper The outcome rests on a written manuscript result, or on a policy choice the manuscript motivates, without a Lean statement covering it.
practical operational The outcome comes from a practical rule with a hand-chosen constant (a stand-in). It is not a theorem about your data.

Three things to keep in mind when you read a trust tag:

  • The tag can change with the outcome. The reconstruction check is tagged lean when it passes (the catalog's Lean statement covers the "enough evidence" direction) and paper when it fails (holding at or below the line is a policy choice). The game check is lean on a pass and operational on a failure.
  • A Lean statement is about a model, not about your data. Result 229 is about labels copied with noise down a tree. Your related-cases graph is not a tree, and your agreement estimate is noisy. The tag tells you which statement the check is modelled on; the result page tells you how far your situation is from it.
  • lean does not mean "settled in the literature". See the previous section.

The concept page Trust and honesty explains how the tags appear in records and dashboards.

Notation

These symbols are used across the theory pages. Every page also defines the ones it uses in words.

Symbol Read as Code name Meaning
\(n\) number of related cases EvidenceSnapshot.n Dots in your related-cases graph (the corroboration graph).
\(d\) average links per case degree Mean degree of that graph, \(2\lvert E\rvert/n\) for \(\lvert E\rvert\) links.
\(\lambda\), \(\hat\lambda\) neighbour agreement lambda_hat How much more often linked cases share a label than chance would give; \(\hat\lambda\) is the estimate from your data. 0 means no better than chance, 1 means always the same.
\(q\) number of label values n_states 2 for yes/no labels (the default).
\(d\lambda^2\) evidence strength d_lambda_sq Average links per case times agreement squared. The reconstruction check passes when it exceeds \(1 + m\).
\(m\) margin reconstruction_margin Safety margin above the line \(d\lambda^2 = 1\); default 0.05.
\(\hat p\) observed link density p_hat Links present divided by links possible, \(\lvert E\rvert / \binom{n}{2}\).
\(p^\star\) your cut-off p_threshold The density your policy treats as the decision line. You choose it.
\(\varepsilon\) window tail epsilon Used in the threshold window formula; fixed at 0.1.
\(w\) window width operational_width, theorem_width Width of the knife-edge window around \(p^\star\); the check holds when \(\lvert \hat p - p^\star\rvert \le \tfrac12 \min(w, 1)\).
\(s\) unusualness score of this case label_score Higher means less like the cases you calibrated on.
\(n_{\mathrm{cal}}\) calibration-set size len(scores) How many past scores the conformal check compares against.
\(\alpha\) conformal level conformal_alpha Tolerated rate of flagging an ordinary case as unusual; default 0.10.
\(W_2\) Wasserstein-2 distance w2 In one dimension: the root-mean-square gap between matching quantiles of two samples.
\(\tau\) map tolerance tau The outcome-shift helper's tolerance, scaled by scale.
\(\alpha_{\mathrm{GW}}\) Goemans–Williamson ratio gw_alpha() 0.8786, the Max-Cut ratio of the Goemans–Williamson algorithm.
\(k\) WL dimension, or number of facilities max_wl_k, k Two unrelated uses; each page says which.

Conventions: \(\log\) is the natural logarithm (the code uses math.log) unless a page says "bits". "Polynomial time" means polynomial in the input size. "Assuming UGC" means "assuming the Unique Games Conjecture"; see Approximation limits for what that is.

Words you will meet

Most terms are defined on the page that uses them and collected in the glossary. The ones that recur across the theory pages:

  • Check: one of the six yes/no tests every decision runs. Any "no" holds the decision. In records each check is a "channel".
  • Stand-in: a simpler procedure run in place of the algorithm a theorem is about, and labelled as such in its output (for example the spectral Max-Cut heuristic in place of Goemans–Williamson).
  • Envelope: a tag on a router request naming its difficulty class (p_exact, fpras, ugc_opt, undec, exptime_trap). The router refuses requests whose tag rules them out. See Using the router.
  • Vacuous: a bound that is true but says nothing, such as a window wider than the whole range \([0, 1]\).

Where to go next