LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite weighted upper-tail p-values and randomized ties

Statement

Let $(Ω, w)$ be a finite probability space, let $T : Ω \to R$ , and let $Z$ have law $w$ . Define $q (z) : = \sum_{ω \in Ω} w (ω) 1 {T (ω) \geq T (z)} .$ Then $\Pr (q (Z) \leq u) \leq u$ for every $u \in [0, 1]$ . If an auxiliary random variable $U$ is independent of $Z$ and uniform on $[0, 1]$ , define $q^{+} (Z, U) : = \sum_{ω \in Ω} w (ω) 1 {T (ω) > T (Z)} + U \sum_{ω \in Ω} w (ω) 1 {T (ω) = T (Z)} .$ Then $\Pr (q^{+} (Z, U) \leq u) = u$ for every $u \in [0, 1]$ .

Facts & Assumptions

Given: A finite probability space $(Ω, w)$ , a real score $T$ on it, and, for the randomized assertion, an independent $U$ with $\Pr (U \leq u) = u$ for $u \in [0, 1]$ .

[F1]

Finite probability spaces, outcome weights, events, and event probabilities: $w (ω) \geq 0$ and $\sum_{ω \in Ω} w (ω) = 1$ ; event probabilities are sums of the weights over the event.

[A1]

The auxiliary randomizer is independent of $Z$ and has the continuous uniform distribution on $[0, 1]$ , characterized by $\Pr (U \leq u) = u$ .

Proof

technique · direct finite enumeration of score levels

1.1givenF1construct

The positive-weight support is nonempty by [F1]. List its finitely many distinct score values in decreasing order as $t_{1} > \dots > t_{m}$ , let $d_{j} = \sum_{T (ω) = t_{j}} w (ω) > 0$ , and put $a_{0} = 0$ and $a_{j} = \sum_{k = 1}^{j} d_{k}$ . These cumulative masses satisfy $0 = a_{0} < a_{1} < \dots < a_{m} = 1$ .

2.1givenF1step 1.1algebra

If $T (Z) = t_{j}$ , then $q (Z) = a_{j}$ . For $u < 1$ , the indices with $a_{j} \leq u$ form an initial segment; if its last index is $j_{0}$ , then $\Pr (q (Z) \leq u) = \sum_{j \leq j_{0}} d_{j} = a_{j_{0}} \leq u$ , while an empty segment has probability zero. At $u = 1$ the probability is one. Thus $q (Z)$ is superuniform.

2.2givenA1step 1.1algebra

On the score level $t_{j}$ , the strict-tail mass is $a_{j - 1}$ and the tied mass is $d_{j}$ , so $q^{+} (Z, U) = a_{j - 1} + U d_{j}$ . By [A1], conditional on this score level its probability of being at most $u$ is zero for $u \leq a_{j - 1}$ , $(u - a_{j - 1}) / d_{j}$ for $a_{j - 1} < u < a_{j}$ , and one for $u \geq a_{j}$ .

3.1step 2.2step 1.1algebra∎

Multiplying these conditional probabilities by $d_{j}$ gives the lengths of $[a_{j - 1}, a_{j}] \cap [0, u]$ . These consecutive intervals partition $[0, 1]$ , so their lengths sum to $u$ . Therefore $\Pr (q^{+} (Z, U) \leq u) = u$ for every $u \in [0, 1]$ .

Depends on

Finite probability spaces, outcome weights, events, and event probabilities

Used by

Fisher sharp-null randomization p-values are valid Theorem

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gary W. Oehlert, A First Course in Design and Analysis of Experiments, Chapter 2, §2.4 (standard reference, not scraped)
Siva Balakrishnan, CMU 36-705 Lecture 28, §28.5 Fisher's Exact p-values (standard reference, not scraped)