Skip to content

The mathematics behind the checks

Every decision this library makes passes six yes/no checks, and a few optional helpers answer questions such as "is this A/B lift real?" or "may we promise a better approximation?". Each check and helper is modelled on a mathematical result, and the result is often stronger, narrower or less settled than the code's use of it. This section says, for each one, which result it is, what that result actually states, how far the code departs from it, and what that means for a decision you rely on.

It is written for readers who want the exact guarantee: data scientists choosing parameters, engineers reviewing a check's behaviour, and researchers checking the claims. You need probability, graphs and algorithms at about first-graduate-course level for the precise statements; the opening sections of every page need none. If you have not met the six checks in plain words, start with The six checks.

How to read this section

Every result page follows the same order: the question in plain words, an intuition, a worked example with numbers from a command you can run, the precise statement with its hypotheses, a box saying where the result stands, what the code does and every way it differs, and the practical limits. How to read these pages explains that layout, the shared notation, what "catalog result N" means and the three trust levels (proven, published, practical) that appear on records.

Two kinds of status are kept apart on every page:

  • In the wider literature: whether the result is a theorem, an open problem, or true only if a conjecture holds (for example the Unique Games Conjecture).
  • In this project's math catalog: what the companion collection of manuscripts claims, and whether a formal statement in the Lean proof assistant exists. Several catalog claims would settle problems the literature regards as open; the pages report them as claims, neither endorsed nor dismissed.

Where each result stands puts both, plus what the code actually uses, in one table. The short version: no decision depends on any catalog claim beyond what the code uses, and the code never runs Lean.

Where the mathematics sits in a decision

flowchart LR
    E[Event] --> S[Policy step] --> PA[Proposed action]
    subgraph build["Checked once, when the module is built"]
        C1["Policy shape<br/>star height, result 134"]
        C2["Progress<br/>parity and mean-payoff games, result 104"]
    end
    subgraph each["Checked on every decision, from the evidence"]
        C3["Neighbour agreement<br/>Kesten–Stigum, result 229"]
        C4["Knife-edge<br/>sharp thresholds, result 186"]
        C5["Unusual cases<br/>conformal prediction, no catalog result"]
        C6["Support<br/>a practical rule, no catalog result"]
    end
    PA --> AND{All six pass?}
    C1 --> AND
    C2 --> AND
    C3 --> AND
    C4 --> AND
    C5 --> AND
    C6 --> AND
    AND -- yes --> ACT[act]
    AND -- no --> HOLD["abstain: hold for a person,<br/>proposed action kept on the record"]
    H["Helpers you call yourself:<br/>router and compare"] -.-> APP[Your code]

The six checks

Check (name in records) Plain question Mathematics What the code actually tests Trust tag Theory page
Policy shape (certificate) Is the policy simple enough to audit? Star height of regular expressions (catalog result 134) The policy as written nests repetition at most 3 deep and compiles to at most 256 states proven Policies that stay simple
Progress (game) From its start, can the workflow keep making progress? Parity games (Zielonka) and mean-payoff games (Karp) (catalog result 104) A parity game on the compiled policy (two players where states are marked environment-owned) and a one-player mean-payoff game; text policies must keep reaching an action or a final state proven on pass, practical on hold Workflows that keep going
Neighbour agreement (reconstruction) Do the related cases agree strongly enough to tell us anything? Kesten–Stigum reconstruction on trees (catalog result 229) Evidence strength \(d\lambda^2 > 1.05\) proven on pass, published on hold Recovering a label from related cases
Knife-edge (threshold) Is the link density too close to our cut-off to trust? Friedgut–Kalai sharp thresholds (catalog result 186) Density more than a hand-set, \(n\)-dependent distance from your cut-off practical Knife-edge densities
Unusual cases (conformal) Is this case like the ones we were right about? Split conformal prediction (standard statistics) Conformal p-value above 0.10 practical Coverage for unfamiliar cases
Support (support) Do the related cases point the same way as the proposed action? None: a counting rule with an explicit constant At least half (min_support) of the related cases carry the outcome the action implies; passes when not measured practical Do the related cases support this action?

Only the support check looks at direction

Neighbour agreement, the knife-edge check and the unusual-case check ask whether the related cases are informative, whether the density is near the cut-off, and whether the case is unusual. None asks whether the evidence supports the action proposed. The support check does, and has no theorem behind it: in fraud_review, a clean event on a dense fraud ring is held because only 3 of the 16 accounts were cleared. Evidence without a support share passes that check, and the direction then comes entirely from the event your code sends.

Where the check settings come from

The margin, window width, decision line, alpha and support minimum in the table above are not constants you have to know in advance. They are learned from labelled history by Learn-then-Test (standard statistics, no catalog result): the learner keeps only settings whose error rate among acted-on decisions is certified below your target by exact binomial tests (fixed-sequence testing by default), and picks the one that acts most often. Because the certificate covers the whole pipeline as it ran in history, blind spots such as the direction problem above show up as measured error rather than staying hidden. See Learning settings with a guarantee for the statement and its assumptions, and Where every number comes from for the plain-language version.

The helpers beside the checks

These run only when your code calls them. Their results are plain dictionaries, not decision records, and they never change a verdict unless you feed them into one.

Helper Plain question Mathematics What the code runs Theory page
dispatch with max_cut, vertex_cover, k_median What approximation may we promise, and should we fund a search for a better one? Unique Games hardness (catalog results 102, 125) A spectral cut with local search (at least half the edges), the matching 2-approximation, and the \(1+2/e\) floor as a reference; ratios assuming the Unique Games Conjecture are reported, never claimed Approximation limits
dispatch with wl How strong a graph fingerprint can we afford? Weisfeiler–Leman refinement (catalog result 133) Colour refinement and a pair-colour stand-in; dimension capped at 2 as a cost budget Graph fingerprints
dispatch with rational_zeros Can we promise to solve polynomial equations over the rationals? Hilbert's tenth problem (catalog result 004) Refuses at once Questions with no algorithm
best_coordinate Which single noisy feature keeps the most information about a target? Courtade–Kumar (catalog result 119) The column that agrees most with the target Keeping one bit
compare_outcome_laws Did the outcome distribution move more than we tolerate? Stability of optimal-transport maps (catalog result 374) One-dimensional \(W_2\) against a hand-set budget Did the distribution move?
sample_two_row, sample_switch Is the A/B lift real, given the totals? Contingency tables with fixed margins (catalog result 115) Exact hypergeometric draws (the Fisher null) for two rows; an uncertified switch chain otherwise Is the A/B lift real?
single_item_max_of_samples, single_item_one_sample One slot, irrevocable choices: what can a threshold rule keep? Prophet inequalities (catalog result 111 for the matroid factor, reported only) First value at or above the bar; with the bar at the largest of one past sample per arrival, half the prophet in expectation (Rubinstein–Wang–Weinberg); with a scalar bar, no factor One slot, no take-backs

How to call the router is in Using the router.

Reading paths

Catalog references in code

Each catalog result the library uses is recorded in src/grounded_decision/certificates.py as a CatalogRef: the result number, a title, lean (whether a Lean statement exists) and a short note. A result not in that file cannot appear on any record.

Result Name in code Where it appears Trust in practice
134 REF_STAR_HEIGHT catalog of the policy-shape check lean
104 REF_MEAN_PAYOFF catalog of the policy-shape and progress checks lean on pass, operational on hold
104 REF_TRUFFET_BAN same two checks; records that a known-unsound step is never run not a test outcome
229 REF_RECONSTRUCTION catalog of the neighbour-agreement check lean on pass, paper on hold
186 REF_SHARP_THRESHOLD catalog of the knife-edge check operational (the catalog width is vacuous)
102 REF_UGC defined only; the router's approximation results carry catalog_optimal instead not a check
125 REF_K_MEDIAN the k_median result's detail text names catalog 125 not a check
133 REF_WL the WL refusal text names catalog 133; the reference itself is not attached to results not a check
119 REF_COURTADE catalog key of best_coordinate results not a check
374 REF_OT catalog key of compare_outcome_laws results not a check
115 REF_TABLES defined only; table samplers report mixer_status instead not a check
111 REF_PROPHET catalog key of single_item_max_of_samples and single_item_one_sample results not a check
004 REF_HILBERT10 value of the rational_zeros refusal not a check

Two of the notes in certificates.py say more than the code delivers, and the theory pages follow the code: the note on 115 says "exact uniform" for two-row tables, but the sampler draws the hypergeometric (Fisher) distribution, which is not uniform (tables); the note on 111 calls the single-item rule a "1/2 rule", but that factor holds only for a correctly chosen bar (prophet).

trust_for(ref) returns lean when ref.lean is true and paper otherwise, but each check sets its own tag from its outcome, as the last column shows. uv run grounded-decision interfaces prints a machine-readable summary of the checks and helpers, naming the catalog result behind each check.

What is not here

The catalog contains many more results than these. Why the others are left out, and what adding one would require, is on What we left out and why.