ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Discrete median bootstrap with ties

Example

Use the lower empirical median, defined as the second order statistic for a sample of size three, and consider observed data $(0, 0, 1)$ . Enumerating all $3^{3} = 27$ bootstrap index tuples gives the exact conditional bootstrap law and demonstrates how the declared lower-quantile convention handles ties. The percentile and basic procedures below are endpoint algorithms, not coverage assertions.

Facts & Assumptions

Given: The observed sample $(0, 0, 1)$ , its empirical masses $P_{n} ({0}) = 2 / 3$ and $P_{n} ({1}) = 1 / 3$ , the finite-index empirical bootstrap, and the interval algorithms.

[F1]

Conditional bootstrap coordinates are IID from the empirical law. Finite-index bootstrap draws are conditionally IID from the empirical law

[F2]

The lower empirical quantile returns the order statistic with index $\max (1, ⌈ B p ⌉)$ . Lower empirical quantile of bootstrap values

[F3]

The percentile interval returns the two empirical bootstrap quantiles at $α / 2$ and $1 - α / 2$ . Percentile bootstrap interval

[F4]

The basic interval reflects those two bootstrap quantiles about the observed estimate. Basic bootstrap interval

Verification

1.1F1givenalgebra

By [F1], the number $K$ of ones in a size-three bootstrap sample has the binomial law with parameters $3$ and $1 / 3$ . The lower median is $1$ exactly when $K \geq 2$ , so $P^{*} (bootstrap median = 1 ∣ 0, 0, 1) = (\binom{3}{2}) (1 / 3)^{2} (2 / 3) + (1 / 3)^{3} = 7 / 27.$ The other $20$ of the $27$ equally likely index tuples give median $0$ .

2.1F2F3F4step 1.1givenalgebra∎

List the $27$ conditional median values with multiplicity: twenty zeros and seven ones. With $α = 1 / 3$ , [F2] gives $Q_{27} (1 / 6) = 0$ and $Q_{27} (5 / 6) = 1$ . Thus [F3] returns $[0, 1]$ , while [F4] with observed median $0$ returns $[- 1, 0]$ . These are the outputs under the specified tie and quantile conventions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

University of Washington STAT 581, Chapter 8: Bootstrap and Jackknife Estimation of Sampling Distributions, §2, Example 2.1 (standard reference, not scraped)
Bradley Efron and Robert Tibshirani, The Bootstrap Method for Assessing Statistical Accuracy, Behaviormetrika 12 (1985), §7 (standard reference, not scraped)