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.

Assignment randomization and bootstrap are different laws

Example

Take two fixed units with potential outcomes $y = (0, 2)$ under the Fisher sharp null, and suppose the observed assignment is $z^{(1)} = (1, 0)$ . The allowed assignment vectors are $z^{(1)} = (1, 0)$ and $z^{(2)} = (0, 1)$ , each with probability $1 / 2$ . Predeclare the statistic as treated outcome minus untreated outcome. Compare its law under the known assignment mechanism with its law when the two observed outcomes are pointwise bootstrapped with replacement and the observed assignment $z^{(1)}$ is held fixed in the contrast.

Facts & Assumptions

Given: Two fixed units, observed assignment $z^{(1)} = (1, 0)$ , the two allowed assignments with equal design probabilities, potential outcomes fixed at $(0, 2)$ under every assignment, and the predeclared treated-minus-untreated score.

[F1]

Finite randomized treatment-assignment models: units and potential outcomes are fixed, the assignment has the known finite probability law, and the assignment is the only randomness in the design.

[F2]

Fisher sharp null and predeclared test orderings: under the Fisher sharp null the response vector is constant over allowed assignments, and the score is fixed in advance; upper-tail ordering includes ties.

[F3]

Fisher sharp-null randomization p-values are valid: under every such finite sharp-null design, the inclusive weighted upper-tail rank p-value is superuniform using the actual assignment weights.

[F4]

Size-n bootstrap from the empirical law: pointwise bootstrap samples observed unit values with independent uniform index draws.

[F5]

Empirical-law bootstrap draws are conditionally IID: conditional on the fixed data, the bootstrap entries are IID from the empirical law.

[F6]

Finite-population average treatment effect and weak null: the weak zero-average-effect null restricts only the average unit effect, while the Fisher sharp null requires every unit effect to be zero.

[F7]

Sampling units and the resampling-unit contract: the conditional bootstrap law is a law on resampled data records, while a Bayesian posterior is a conditional law on parameter values under a specified prior and joint model.

[F8]

Valid p-values: a p-value statistic is valid for a null hypothesis when it is superuniform under every null law.

[F9]

Empirical measure of observed units: the empirical law assigns each indexed observation mass $1 / n$ , counting repetitions by index.

Verification

1.1givenF1F2construct

Define $T (z, y) = \sum_{i : z_{i} = 1} y_{i} - \sum_{i : z_{i} = 0} y_{i}$ . The sharp-null schedule fixes $y = (0, 2)$ , so $T (z^{(1)}, y) = - 2$ and $T (z^{(2)}, y) = 2$ .

2.1F1F2F3F8step 1.1algebra

The design randomization law therefore assigns probability $1 / 2$ to each of $- 2$ and $2$ . Its inclusive upper-tail p-value is $1$ at $z^{(1)}$ and $1 / 2$ at $z^{(2)}$ , a superuniform distribution under the assignment law, so [F8] identifies it as valid for this null; [F3] also gives the general validity statement.

3.1F4F5F9step 1.1step 2.1algebra

The observed unit values are $(0, 2)$ , so [F9] gives empirical mass $1 / 2$ to each. By [F4] and [F5], an ordered size-two bootstrap pair takes $(0, 0), (0, 2), (2, 0), (2, 2)$ with probabilities $1 / 4$ each. The same difference score has bootstrap law with masses $1 / 2$ at $0$ and $1 / 4$ at each of $- 2, 2$ , which differs from the design law in step 2.1.

4.1F1F4F5F6F7step 2.1step 3.1∎

The two laws have different state spaces and sampling mechanisms: one resamples assignments under a known design, the other resamples observed unit records conditional on those records. By [F7], a Bayesian posterior, when defined, is instead a conditional law on parameter values under a specified prior and joint model; this example supplies no such prior or posterior. By [F6], its sharp-null calculation also asserts no validity under the weaker average-effect null.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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)
Bradley Efron and Robert Tibshirani, The Bootstrap Method for Assessing Statistical Accuracy, Behaviormetrika 12 (1985), §2, printed pp. 3–5 (standard reference, not scraped)
B. Efron and R. Tibshirani, The Bootstrap Method for Assessing Statistical Accuracy, Stanford LCS Technical Report 19 / BIO 101 (October 1985; full-text report copy) (standard reference, not scraped)