Lean-verified core of the Gaebler–Goel robust outcome test

Logical core of the "robust outcome test" (Gaebler & Goel, PNAS 2025), Lean-verified

Formalizing the central guarantee of A Simple, Statistically Robust Test of Discrimination — that combining the benchmark and outcome tests yields a test that is correct when both fire — on the site pin (Lean v4.29.1 / Mathlib v4.29.1).

The result (Theorem 1)

Two groups with group-specific decision thresholds $t_0, t_1$. Decision rate $\mathrm{DR}_g = \Pr(R\ge t_g\mid G{=}g)$, outcome rate $\mathrm{OR}_g = \mathbb E[R\mid R\ge t_g, G{=}g]$. Under the MLRP, if group 1 has both the lower decision rate and the higher outcome rate, then $t_0 < t_1$ — group 1 is held to a strictly higher (discriminatory) standard. So when the two tests agree, the conclusion is guaranteed correct.

What the proof actually does (SI §1.A)

It's a beautiful contrapositive with a case split on which group has the lower base rate. The argument rests on two imported MLRP consequences (the paper cites Shaked–Shanthikumar Thms 1.C.1, 1.C.5), stated at a common threshold:

• Eq. (3): stochastic dominance — the higher-base-rate group has the larger decision rate at every threshold;
• Eq. (4): the lower-base-rate group has the smaller tail-conditional mean at every threshold;

plus threshold-rule monotonicity (lowering a threshold raises the decision rate and lowers the tail mean). Assuming $t_1 \le t_0$: if group 0 is the lower-base-rate group, Eq. (3) + monotonicity force $\mathrm{DR}_0 \le \mathrm{DR}_1$ (benchmark test can't fire); if group 0 is the higher-base-rate group, Eq. (4) + monotonicity force $\mathrm{OR}_1 \le \mathrm{OR}_0$ (outcome test can't fire). Either way, $t_1\le t_0$ kills one of the two tests — so if both fire, $t_0 < t_1$.

formal proof

Honest scope

I formalized the combination step — the actual logical content of Theorem 1 — taking Eqs. (3) and (4) as explicit hypotheses, exactly as the paper itself imports them from Shaked–Shanthikumar rather than re-deriving them. What is not formalized: the MLRP ⇒ stochastic-dominance and MLRP ⇒ tail-mean-ordering theory underlying Eqs. (3)–(4). Mathlib has no monotone-likelihood-ratio / stochastic-order development, so that's a substantial separate build; the encoding makes the dependency explicit by stating those facts as named structure fields (MLRPInputs). I also did not touch the fully measure-theoretic Theorem S2 (risk-decision curves, KSD, tilted distributions). So this is the verified skeleton of the theorem, with the imported analytic inputs clearly delineated — not the full measure-theoretic development.

This is also a nice illustration of a more general pattern: a contested, unformalizable concept (what counts as "discrimination") resting on a crisp, formalizable mathematical core (this threshold-ordering guarantee). The formal layer can verify the logical engine precisely while staying agnostic about the normative interpretation layered on top.