Skip to content

Trust levels and honest limits

Each of the six checks is modelled on a piece of mathematics, but "based on a theorem" can mean very different things: the rule might follow the theorem exactly, borrow only its shape, or have no theorem behind it at all. Before you rely on a verdict, or explain one to an auditor, you need to know which. This page says, for each check, what a pass actually guarantees, what it does not, and how the trust field in every decision record tells you that.

It is written for evaluators, domain owners and auditors. It assumes you have met the six checks on The six checks. The mathematics itself, and the status of each result in the wider literature, are on Where each result stands.

The three trust levels

Every check in a decision record has a trust field with one of three values:

Level Field value What it means
proven lean The rule the check applied is taken from a result that the project's companion math catalog states in the Lean proof assistant.
published paper The rule rests on a written (not machine-checked) result, or on a cautious policy choice that such a result motivates.
practical operational The rule is a practical stand-in with a hand-chosen constant, or a standard statistical method with no catalog result behind it.

Three facts keep these tags honest:

  • The library never runs Lean. Not at build time, not at decision time. lean is a pointer to a statement in the catalog, not a proof that your data meets that statement's assumptions.
  • The tag is about this outcome, not about the check in general. The neighbour-agreement check is lean when it passes and paper when it holds, because the catalog statement covers only the "enough evidence" direction.
  • lean is not "more reliable" than operational. The unusual-cases check is operational, yet its guarantee is the most directly usable of the six. A lean tag can point at a theorem whose constant is far too large to use. Read the tag together with the check's metrics and the table below.

The catalog is a separate collection of mathematical results, each with a number (for example "Kesten–Stigum reconstruction, catalog result 229"). Some catalog claims would settle questions the wider literature treats as open; Where each result stands gives both views for every result.

What each check guarantees, honestly

Check (record name) Trust when it passes / holds What a pass gives you What a pass does not give you
Policy shape (certificate) lean / never holds in a record The written policy nests repetition at most 3 deep and compiled within the state limits. Exact. That the policy is correct, or that every action is reachable. A policy breaking a limit raises an exception at build time, so records always show this check passed.
Progress (game) lean / operational From the start, the service can keep the workflow coming back to even-priority states (for text policies: states that propose an action, or final states) whatever the environment does in states marked environment=True; and some reachable cycle has average payoff at least 0. Exact for the game the chart is turned into. That the service will actually send the events that keep the workflow moving in states it controls; that the payoff answer holds against the environment (it assumes the best route); that a chart left at priority 0 everywhere is free of loops you would not want.
Neighbour agreement (reconstruction) lean / paper Links per case × agreement² is above 1.05: the related cases are coherent enough that, in the tree model behind the theorem, their labels carry information. That the related cases support this action (agreement is squared, so consistent disagreement passes too); that your graph behaves like the theorem's tree; that a case below the line is hopeless when there are 5 or more labels.
Knife-edge (threshold) operational / operational in practice The link density is more than a size-dependent distance from your cut-off. Which side of the cut-off you are on. The window borrows the shape of a theorem (Friedgut–Kalai) but uses constant 2 instead of the proven \(2^{19}\), and centres it on your cut-off rather than the theorem's.
Unusual cases (conformal) operational / operational If this case and the calibration cases come from the same process, the chance this check holds it is at most \(\alpha\) (10%). A standard, proven statistical guarantee. That the action is right; that unusual cases are caught at any particular rate; anything at all if the calibration set is empty (passes by default) or has fewer than 9 scores.
Support (support) operational / operational At least min_support (0.5) of the related cases carry the outcome the proposed action implies. A practical rule with an explicit constant; no theorem. That the action is right; that the share is weighted by how strongly cases are linked; anything at all when support is not measured (passes unless require_support is set).

Only the support check looks at direction, and only when measured

Neighbour agreement, the knife-edge check and the unusual-cases check ask whether the evidence is strong, clear and familiar, not which way it points. The support check asks whether the related cases carry the outcome the proposed action implies. In fraud_review the same dense ring of accounts lets a suspicious event act block (support 0.81) and holds a clean event's pass (support 0.19). If your evidence carries no support share, the support check passes and the direction comes entirely from the event your service sends.

Two more limits apply across checks:

  • The checks are not independent evidence. Neighbour agreement and the knife-edge window read the same graph; a thin graph usually fails both.
  • Several shipped examples hard-code the case's unusualness score below every calibration score, so the unusual-cases check never fails in them. They show the plumbing, not what the check does on your data.

Why the knife-edge check is practically never lean

The threshold check would be tagged lean only if the theorem's own window, with its proven constant \(2^{19}\), were narrower than 1. With \(\varepsilon = 0.1\) that width is

\[ w_{\mathrm{thm}}(n) = \frac{2^{19}\,\ln 5}{(\ln n)^2}, \]

which drops below 1 only when \(\ln n > \sqrt{2^{19}\ln 5} \approx 918.6\), that is \(n > e^{918}\). At \(n = 50\) it is 55,137; at \(n = 80\) it is 43,943. A width larger than the whole range \([0, 1]\) would hold every decision, so the record reports it (theorem_width, theorem_vacuous: true) and the decision uses the same formula with constant 2 (operational_width, 0.210 at \(n = 50\)). The full table of window sizes is on the knife-edge page.

Numbers the library reports but never promises

Some helpers beside the decision path return a mathematical constant next to their answer. These are reference values, not guarantees of the code that ran:

Value in the result What it is What the code actually does
Max-Cut factor_claimed 0.8786 (\(\alpha_{\mathrm{GW}}\)) The best ratio any polynomial algorithm can promise, assuming the Unique Games Conjecture A spectral cut with local search; guarantees at least half the edges. See Unique Games.
Vertex cover factor_claimed 2 The factor of the maximal-matching method on any graph Exactly that method. On bipartite graphs an exact answer is available in polynomial time (König's theorem), and the method does not use it.
k-median 1.736 (\(1 + 2/e\)) A hardness lower bound: no polynomial algorithm does better unless P = NP No k-median algorithm runs. The number is a floor on what you may claim, not a ratio anyone achieves.
Prophet factor_claimed 0.5 from single_item_max_of_samples, lean_factor \(2^{-310}\) 0.5 is a proven guarantee for that rule (bar = the best of one past sample per arrival, Rubinstein–Wang–Weinberg), in expectation, when values are independent and non-negative and each sample is drawn like its arrival; \(2^{-310}\) is the catalog's constant for a harder setting Exactly that rule. single_item_one_sample (an arbitrary scalar bar) reports factor_claimed=None: no ratio is guaranteed for it. See Prophet inequalities.
Two-row table sampler mixer_status: exact_hypergeometric Exact draws from the Fisher exact test distribution Not uniform over tables. Larger tables use a switch chain whose mixer_status says not_paper_fpras. See Contingency tables.
WL cap max_wl_k 2 A cost budget Requests above it are refused and labelled exptime_trap, meaning "too expensive under our budget". See Questions the library refuses.

Results the library deliberately does not use at all are listed on What we left out and why.

Reading a record as an auditor

The held discharge in clinical_triage (the third decision in uv run grounded-decision examples clinical_triage --json) shows how to read the tags together with the metrics:

Check passed trust Key metrics How to read it
certificate true lean star_height: 0, dfa_states: 4 Chart built directly, no policy text, so no nesting to measure; 4 states, within the 256 limit.
game true lean parity_win: true, nonnegative_mean: true Every state keeps the default priority 0 and payoff 0, so any run is acceptable; the check confirms the chart, it does not test the workflow.
reconstruction false paper degree: 1.6, lambda_hat: 0.0, d_lambda_sq: 0.0 5 related patients who agree no more than chance. Held by policy below the line.
threshold false operational n: 5, p_hat: 0.4, p_threshold: 0.15, operational_width: 1.243 Graph too small to locate density; window is capped at ±0.5.
conformal true operational p_value: 1.0, n_cal: 40 Score lower than every calibration score.
support true operational support: 0.8, min_support: 0.5 4 of the 5 similar visits were uneventful, the outcome a discharge implies. Not enough to act on alone.

The decision was held because two data checks failed. Nothing in the record claims the discharge was wrong; it says the related cases were too few and too mixed to act on without a person.

Where next