ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

A weighted two-sided randomization test with tied scores

Example

Let three units have fixed outcomes $y = (0, 1, 2)$ under every assignment, and randomize exactly one unit to treatment. The assignments select unit 1, 2, or 3 with probabilities $1 / 2$ , $1 / 3$ , and $1 / 6$ , respectively. Use the treatment-minus-control mean as signed score and its absolute value as the predeclared two-sided ordering about zero. The upper-tail p-value is $2 / 3$ for either outer assignment and $1$ for the middle assignment. It is superuniform despite the unequal assignment weights and the tied outer scores; an independent uniform tie randomizer gives an exactly uniform p-value.

Facts & Assumptions

Given: The three-unit complete randomization described above, its fixed potential-outcome schedule, and an independent $U$ uniform on $[0, 1]$ .

[F1]

Finite randomized treatment-assignment models: the outcomes are fixed under the design and the only assignment randomness has the specified finite law.

[F2]

Fisher sharp null and predeclared test orderings: a two-sided ordering about null center zero uses $T (z, y) = ∣ S (z, y) ∣$ and includes ties in the upper tail.

[F3]

Fisher sharp-null randomization p-values are valid: the weighted upper-tail value is superuniform under every Fisher sharp-null schedule, and independent uniform randomization within tied mass is exactly uniform.

[A1]

The auxiliary $U$ is independent of the treatment assignment and satisfies $P (U \leq u) = u$ for $u \in [0, 1]$ .

Verification

Given: The outcomes, assignment weights, treatment-minus-control mean, and auxiliary randomizer stated above.

1.1givenF1algebra

The assignment weights are nonnegative and sum to one, and each unit's outcome is the same under all three assignments, so this is a finite assignment law satisfying the Fisher sharp null.

2.1givenF2step 1.1algebra

If unit 1, 2, or 3 is treated, the signed differences are respectively $0 - (1 + 2) / 2 = - 3 / 2$ , $1 - (0 + 2) / 2 = 0$ , and $2 - (0 + 1) / 2 = 3 / 2$ . The two-sided scores are therefore $3 / 2, 0, 3 / 2$ .

3.1F1step 2.1algebra

Each outer assignment has inclusive upper-tail mass $1 / 2 + 1 / 6 = 2 / 3$ ; the middle score is the minimum, so its inclusive upper-tail mass is $1$ . The nonrandomized p-value therefore equals $2 / 3$ with probability $2 / 3$ and $1$ with probability $1 / 3$ . Its distribution function is $0$ below $2 / 3$ , $2 / 3$ on $[2 / 3, 1)$ , and $1$ at $1$ , which is at most its argument throughout $[0, 1]$ .

3.2givenA1step 2.1algebra

At either outer assignment the strict-tail mass is zero and the tied mass is $2 / 3$ , so $p^{+} = (2 / 3) U$ . At the middle assignment the strict-tail mass is $2 / 3$ and the tied mass is $1 / 3$ , so $p^{+} = 2 / 3 + U / 3$ .

4.1A1F3step 3.1step 3.2algebra∎

For $0 \leq u \leq 2 / 3$ , the outer assignments contribute $(2 / 3) P (U \leq 3 u / 2) = u$ . For $2 / 3 \leq u \leq 1$ , they contribute $2 / 3$ and the middle assignment contributes $(1 / 3) P (U \leq 3 u - 2) = u - 2 / 3$ ; hence $P (p^{+} \leq u) = u$ on the entire unit interval. Together with step 3.1, this verifies the theorem's superuniform and uniform conclusions for this assignment law.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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.