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.

Two-stage conditional-error adaptation — Examples

1 · Prerequisites

2 · Summary

The worked example uses a finite null model to select one of two stage-2 sample sizes from interim information while retaining the selected-size conditional p-value law; the rejection probability equals the original conditional-error budget. A second calculation uses independent normal stage statistics. Its original equal-weight inverse-normal test has size $α$ , while an interim-selected, unit-norm weight rule with an unchanged critical value has size $3 α / 2$ . The calculation shows why normalized weights alone do not replace conditional recalibration.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

Calibrated selected sample size and an uncalibrated weight change

Statement

In the finite null model below, the selected stage-2 sample size is a function of interim information, and each selected-size p-value retains its conditional null calibration. The rejection rule at the original conditional error has null rejection probability $1 / 2$ , equal to the original budget. In the normal model, for any fixed critical value $c > 0$ , the equal-weight inverse-normal rule rejecting when $(Z_{1} + Z_{2}) / \sqrt{2} \geq c$ has size $α = \int_{c}^{\infty} ϕ (t) d t \in (0, 1 / 2)$ . Choosing unit-norm weights from the sign of the interim statistic $Z_{1}$ and retaining $c$ raises that probability to $3 α / 2$ .

Facts & Assumptions

Given: AC; a finite uniform null probability space for the first model; independent fair binary coordinates $I, B_{0}, B_{2}, B_{3}$ ; and, for the second model, independent standard-normal variables $Z_{1}, Z_{2}$ with density $ϕ (x) = C e^{- x^{2} / 2}$ , where $C = (\int_{R} e^{- t^{2} / 2} d t)^{- 1}$ . Thus $ϕ$ is even, continuous, strictly positive, and has total mass one. Write $Φ (x) = \int_{- \infty}^{x} ϕ (t) d t$ .

[A1]

AC supplies the conditional-expectation classes inherited by the results used here. The Axiom of Choice

[F1]

For a countable-valued interim-measurable $N$ , calibration within every selected-size stratum implies conditional superuniformity of the selected p-value. Selected-size conditional validity yields a conditionally superuniform p-value

[F2]

If a stage-2 p-value is conditionally superuniform given $F_{1}$ , rejection at the original conditional error $A$ has conditional rejection probability at most $A$ ; when $P_{0} (R_{0}) \leq α$ , its overall null rejection probability is at most $α$ . A conditionally superuniform stage-2 p-value preserves conditional error

[F3]

A p-value statistic is measurable, takes values in $[0, 1]$ , and is valid under the null when its null CDF is superuniform. Valid p-values

[F4]

If an integrable variable is independent of $F_{1}$ , its conditional expectation given $F_{1}$ is its ordinary expectation (under AC). Conditioning a known variable and an independent variable

[F5]

Conditional expectations are almost-sure classes, so changing a version does not alter event probabilities. Conditional expectation as an ae class

Verification

Given: The two null models and notation stated above; verify the calibrated finite-size rejection probability and the changed-weight normal rejection probability.

1.1A1F1F2F3F4F5givenconstructalgebra

Put $Ω = {0, 1}^{4}$ with the uniform law and let $I, B_{0}, B_{2}, B_{3}$ be the independent fair-bit coordinates. Define $p_{j} = 1 / 2$ when $B_{j} = 0$ and $p_{j} = 1$ when $B_{j} = 1$ , for $j \in {0, 2, 3}$ . Each $p_{j}$ is measurable with values in $[0, 1]$ , and its null CDF is $0$ for $u < 1 / 2$ , $1 / 2$ for $1 / 2 \leq u < 1$ , and $1$ at $u = 1$ , so each is a valid p-value by [F3]. Let $F_{1} = σ (I)$ , select $N = 2$ on $I = 0$ and $N = 3$ on $I = 1$ , and take the original rejection event $R_{0} = {p_{0} \leq 1 / 2}$ . Independence and [A1, F4] give its conditional error $A = E_{0} [1_{R_{0}} ∣ F_{1}] = 1 / 2$ almost surely; [F5] makes the resulting event probabilities version-independent. For each $m \in {2, 3}$ and $H \in F_{1}$ , independence of $B_{m}$ from $I$ gives $P_{0} (H \cap {N = m} \cap {p_{N} \leq u}) = c (u) P_{0} (H \cap {N = m})$ , where $c (u) = 0$ for $u < 1 / 2$ , $1 / 2$ for $1 / 2 \leq u < 1$ , and $1$ for $u = 1$ ; in every case $c (u) \leq u$ . Thus [F1] makes $p_{N}$ conditionally superuniform. Rejection at $A = 1 / 2$ is exactly the event that the selected bit is zero. Since $P_{0} (R_{0}) = P_{0} (B_{0} = 0) = 1 / 2$ , set $α = 1 / 2$ in the overall conclusion of [F2] to obtain $P_{0} (p_{N} \leq A) \leq 1 / 2$ ; the selected bit is fair, so equality holds and the original budget is attained.

1.2F3givenconstructalgebra

The positive density makes $Φ$ continuous and strictly increasing. Define the one-sided stage p-values $p_{i} = 1 - Φ (Z_{i})$ , so $Z_{i} = Φ^{- 1} (1 - p_{i})$ ; for $0 < u < 1$ , $P_{0} (p_{i} \leq u) = P_{0} (Z_{i} \geq Φ^{- 1} (1 - u)) = u$ , and the endpoint inequalities are immediate, so they are valid by [F3]. Fix $c > 0$ and set $α = \int_{c}^{\infty} ϕ (t) d t$ , with $0 < α < 1 / 2$ by positivity and evenness. Under the fixed equal-weight inverse-normal rule, reject when $W = (Z_{1} + Z_{2}) / \sqrt{2} \geq c$ . The orthogonal change of variables $w = (z_{1} + z_{2}) / \sqrt{2}$ , $v = (z_{1} - z_{2}) / \sqrt{2}$ has absolute Jacobian $1$ and satisfies $z_{1}^{2} + z_{2}^{2} = w^{2} + v^{2}$ , so the joint density transforms to $ϕ (w) ϕ (v)$ and integration over $w \geq c$ gives the fixed-rule null rejection probability $α$ .

2.1givenstep 1.2constructalgebra∎

Choose $N_{2} = 1$ when $Z_{1} \geq 0$ and $N_{2} = 2$ when $Z_{1} < 0$ . Without recalibrating $c$ , use weights $w (N_{2}) = (1, 0)$ in the first case and $(0, 1)$ in the second; each has squared norm one. Since $c > 0$ , the adapted rejection event is the disjoint union ${Z_{1} \geq c} \cup {Z_{1} < 0, Z_{2} \geq c}$ , whose probability by independence is $α + (1 / 2) α = 3 α / 2 > α$ . Thus unit-norm weights selected with the stage-2 size do not by themselves preserve the fixed-rule error probability.

Remarks

The normal counterexample uses extreme weights so its size calculation is exact. Sugiura–Uesaka give the more direct sample-size-weight warning: in the weighted inverse-normal rule, replacing the prespecified second-stage size by its interim-selected value can exceed the target null rejection probability. The finite calibrated model above illustrates the separate condition that must be checked: the selected second-stage p-value law under the null.