Pipeline-generated

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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Holm Step-Down Familywise Error Control — Examples

1 · Prerequisites

2 · Summary

The worked example applies Holm's rank-specific cutoffs to four ordered p-values and compares the resulting rejection set with the one-step Bonferroni cutoff for the same fixed family. It illustrates only the arithmetic for one observed vector. The theorem's strong FWER guarantee still requires valid p-values under each true null.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Holm step-down versus one-step Bonferroni

Example

For a fixed four-hypothesis family, take the observed, already ordered p-value vector $(1 / 250, 3 / 200, 3 / 100, 1 / 5)$ and $α = 1 / 20$ . Holm's rank cutoffs are $1 / 80$ , $1 / 60$ , $1 / 40$ , and $1 / 20$ . The first two comparisons pass and the third fails, so Holm rejects $H_{01}$ and $H_{02}$ and retains $H_{03}$ and $H_{04}$ . The one-step Bonferroni comparison uses $α / 4 = 1 / 80$ for every hypothesis; it rejects only $H_{01}$ .

Facts & Assumptions

Given: A family $(H_{01}, H_{02}, H_{03}, H_{04})$ fixed before observing the p-values, the ordered vector $p = (1 / 250, 3 / 200, 3 / 100, 1 / 5)$ , and $α = 1 / 20$ . In this example, one-step Bonferroni means rejecting index $i$ exactly when $p_{i} \leq α / 4$ . Determine both rejection sets and state the limit of this numerical illustration.

[F1]

Holm step-down procedure: Holm rejects an initial ordered prefix, comparing rank $j$ with $α / (m - j + 1)$ and stopping at the first failed comparison.

[F2]

Holm step-down controls strong FWER: if every p-value is valid for its fixed null, then the Holm procedure has FWER at most $α$ for every parameter, without an independence assumption.

Verification

technique · direct arithmetic

1.1givenF1algebra

At rank $1$ , $1 / 250 < 1 / 80$ . At rank $2$ , $3 / 200 \leq 1 / 60$ because $180 \leq 200$ . At rank $3$ , $3 / 100 > 1 / 40$ because $120 > 100$ . By [F1] the procedure stops at rank $3$ and rejects exactly indices ${1, 2}$ .

2.1givenstep 1.1algebra

The one-step Bonferroni cutoff is $1 / 80$ . The first p-value is below it; the second is above it because $3 / 200 > 1 / 80$ is equivalent to $240 > 200$ , and the third and fourth are larger still. Thus Bonferroni rejects exactly ${1}$ , so the two observed rejection sets differ.

3.1F2step 1.1step 2.1∎

This computation determines decisions for one observed vector only. It does not establish that the p-value statistics are valid under their nulls or calculate an error probability; those distributional hypotheses are needed for the guarantee in [F2].