ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-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.

Two-look O’Brien–Fleming-type spending

Example

Assume AC, take $K = 2$ , $t_{1} = 1 / 2$ , $t_{2} = 1$ , and $α = 0.05$ . Let $Φ (x) = P_{0} (Z_{1} \leq x)$ be the standard normal CDF, and write $z_{p}$ for the unique real number with $Φ (z_{p}) = p$ . Use the two-sided O’Brien–Fleming-type spending curve $A_{O F} (0) = 0, A_{O F} (t) = 2 [1 - Φ (\frac{z_{0.975}}{\sqrt{t}})] (0 < t \leq 1) .$ Its first spend is $a_{1} = 2 [1 - Φ (z_{0.975} \sqrt{2})]$ . The first symmetric two-sided boundary is $c_{1} = z_{1 - a_{1} / 2}$ . The second boundary is the unique finite $c_{2} \geq 0$ satisfying $P_{0} (∣ Z_{1} ∣ \geq c_{1} or ∣ Z_{2} ∣ \geq c_{2}) = 0.05,$ where ${Corr}_{0} (Z_{1}, Z_{2}) = 1 / \sqrt{2}$ . The two-sided boundaries come from this absolute-value crossing equation, not from doubling the one-sided boundaries.

Facts & Assumptions

Given: AC, $K = 2$ , $t_{1} = 1 / 2, t_{2} = 1$ , $α = 0.05$ , the canonical Gaussian null law, and the displayed O’Brien–Fleming-type spending curve. Verify the spending conditions and identify the two symmetric boundaries.

[F1]

Canonical group-sequential alpha-spending design: An admissible spending function is nondecreasing from $[0, 1]$ into $[0, α]$ , with endpoint values $0$ and $α$ ; the symmetric two-sided crossing event at look $j$ is ${∣ Z_{j} ∣ \geq c_{j}}$ .

[F2]

Recursive group-sequential boundary calibration: At a positive increment the symmetric two-sided boundary solves $P_{0} (R_{k - 1} \cup {∣ Z_{k} ∣ \geq c_{k}}) = A (t_{k})$ .

[F3]

Group-sequential boundaries exist uniquely and spend alpha exactly: Every positive spending increment has a unique finite boundary and $P_{0} (R_{k}) = A (t_{k})$ at each look.

[F4]

Standard normal and normal laws: The standard normal law is the probability measure with density $ϕ (x) = e^{- x^{2} / 2} / \sqrt{2 π}$ .

[F5]

The standard normal density has total mass one: The density $ϕ$ is positive and has integral one.

[F6]

Continuity from below for measures: For an increasing sequence of measurable sets, the measure of their union is the supremum of their measures.

[F7]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ : A continuous real function on a closed bounded interval takes every value between its endpoint values.

[A1]

The Axiom of Choice: Assume the Axiom of Choice.

Verification

1.1F4F5A1algebra

Define $Φ (x) = \int_{- \infty}^{x} ϕ (s) d s$ . For $x < y$ , positivity in [F5] gives $Φ (y) - Φ (x) > 0$ , while $ϕ (s) \leq 1 / \sqrt{2 π}$ gives $Φ (y) - Φ (x) \leq (y - x) / \sqrt{2 π}$ . Thus $Φ$ is strictly increasing and continuous.

2.1F4F5F6F7step 1.1algebra

The density $ϕ$ is even, so $Φ (0) = 1 / 2$ . Applying [F6] to the increasing upper half-lines $(- n, \infty)$ gives $Φ (x) \to 0$ as $x \to - \infty$ ; applying it to the increasing lower half-lines $(- \infty, n]$ gives $Φ (x) \to 1$ as $x \to + \infty$ . Hence [F7] gives a unique quantile $z_{p}$ for each $p \in (0, 1)$ , and $z_{0.975} > 0$ .

3.1givenF1step 1.1step 2.1algebra

For $0 < t \leq 1$ , $z_{0.975} / \sqrt{t}$ decreases as $t$ increases; since $Φ$ increases, $A_{O F} (t)$ is nondecreasing. Its values are positive and at most $2 [1 - Φ (z_{0.975})] = 0.05$ , and its limit at $0$ is $0$ by the upper-tail limit in step 2.1. Thus the declared $A_{O F} (0) = 0$ makes it admissible. At $t_{1} = 1 / 2$ , its value is $a_{1} = 2 [1 - Φ (z_{0.975} \sqrt{2})]$ , with $0 < a_{1} < 0.05$ .

4.1givenF1F2F3F4step 2.1step 3.1algebra∎

By symmetry of the density in [F4], $P_{0} (∣ Z_{1} ∣ \geq c) = 2 [1 - Φ (c)]$ for $c \geq 0$ . Therefore $c_{1} = z_{1 - a_{1} / 2}$ has first-look crossing probability $a_{1}$ . The canonical covariance matrix is $Σ = (\begin{array}{cc} 1 & 1 / \sqrt{2} \\ 1 / \sqrt{2} & 1 \end{array})$ , so its determinant is $1 / 2 > 0$ and the correlation is $1 / \sqrt{2}$ . Applying [F2]–[F3] at the second look gives the unique finite $c_{2}$ satisfying the displayed cumulative two-sided crossing equation, with total probability $A_{O F} (1) = 0.05$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

49 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

David L. DeMets and K. K. Gordon Lan, Interim Analysis: The Alpha Spending Function Approach, Statistics in Medicine 13 (1994), PDF pp. 6–7 (standard reference, not scraped)
Michael J. Grayling, James M. S. Wason, and Adrian P. Mander, Group Sequential Clinical Trial Designs for Normally Distributed Outcome Variables, The Stata Journal 18(2) (2018), PDF pp. 2–4 (standard reference, not scraped)
Giorgos Minas, Multivariate Global Testing and Adaptive Designs, PhD thesis, Chapter 5 §§5.3–5.3.1, printed pp. 72–73 (standard reference, not scraped)