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.

✓ 2 results · all verified · 0 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. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Logrank and weighted logrank — Examples

1 · Prerequisites

2 · Summary

The first example gives crossing population hazards and survival curves with a positive-probability sample pattern whose two logrank contributions cancel, leaving a zero score and positive plug-in variance. The second enumerates a three-assignment design with unequal probabilities, calculates each absolute logrank score and exact p-value, and checks the full superuniform distribution. These examples distinguish an observed score from a survival-law equality claim and distinguish finite Fisher randomization from Gaussian calibration.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Crossing hazards with a zero observed logrank score

Statement

Use follow-up horizon $τ = 2.5$ . Let the event times be mutually independent, with group hazards $λ_{1} (t) = {\begin{cases} 2, & 0 \leq t \leq 1, \\ 1, & t > 1, \end{cases} λ_{0} (t) = {\begin{cases} 1, & 0 \leq t \leq 1, \\ 2, & t > 1. \end{cases}$ Let all censoring times be mutually independent and independent of the entire event-time family. In group 1, let each censoring time equal $1.5$ with probability $2 / 3$ and $2.5$ with probability $1 / 3$ ; in group 0 let it equal $2.5$ . Observe each subject through $U_{i} = \min (T_{i}, C_{i})$ and $δ_{i} = 1 {T_{i} \leq C_{i}}$ , using the event-censor tie convention in Two-group logrank and weighted logrank scores. Since every $C_{i} \leq τ$ , these records lie in $[0, τ] \times {0, 1}$ . A possible sample has $n_{1} = 4$ : one event at $t_{1} \in (0, 1)$ , two subjects censored at $1.5$ , and one subject censored at $2.5$ . It has $n_{0} = 2$ : one event at $t_{2} \in (2, 2.5)$ and one subject censored at $2.5$ . Compute the unweighted logrank score, its plug-in variance, and the empirical product-limit curves. Verify that this sample pattern has positive probability and that the population survival curves cross even though the observed score is zero.

Facts & Assumptions

Given: The group hazards, mutually independent event and censoring times with the stated censoring laws, the sample pattern, and the definitions in Two-group logrank and weighted logrank scores and Nelson–Aalen, Kaplan–Meier, and Greenwood estimators.

[F1]

Two-group logrank and weighted logrank scores: at event time $t_{j}$ , the score contribution is $O_{j} - d_{j} Y_{1 j} / Y_{j}$ and the plug-in variance contribution is the displayed risk-set formula; with one failure it is $Y_{1 j} Y_{0 j} / Y_{j}^{2}$ .

[F2]

Nelson–Aalen, Kaplan–Meier, and Greenwood estimators: in each group, the empirical product-limit estimate is ${\hat{S}}_{g} (t) = \prod_{0 \leq u \leq t : d_{g} (u) > 0} (1 - d_{g} (u) / Y_{g} (u))$ , where $Y_{g} (u)$ is the number at risk and $d_{g} (u)$ the number of failures at $u$ .

Proof

1.1givenalgebra

Integrating the hazards gives, for $t \geq 1$ , $S_{1} (t) = e^{- (t + 1)}$ and $S_{0} (t) = e^{- (2 t - 1)}$ ; for $0 \leq t \leq 1$ , $S_{1} (t) = e^{- 2 t}$ and $S_{0} (t) = e^{- t}$ . On $[0, 1]$ , $S_{1} (t) < S_{0} (t)$ for $t > 0$ . For $t \geq 1$ their ratio is $S_{1} (t) / S_{0} (t) = e^{t - 2}$ , so they meet at $t = 2$ and reverse order after it. Each event-time interval $(0, 1)$ and $(2, 2.5)$ has positive probability, and the specified censor-time values have positive mass. For every subject required to be censored at $c \in {1.5, 2.5}$ , $P (T > c) = S_{g} (c) > 0$ under its group hazard. Mutual independence of all event and censoring times therefore makes the finite intersection defining the sample pattern have positive probability.

2.1F1F2step 1.1givenalgebra∎

At $t_{1}$ , $(Y_{1}, Y_{0}, d, O) = (4, 2, 1, 1)$ , so the score contribution is $1 - 4 / 6 = 1 / 3$ and the plug-in variance contribution is $4 \cdot 2 / 6^{2} = 2 / 9$ . The two censorings at $1.5$ leave one group-1 subject at risk. At $t_{2}$ , $(Y_{1}, Y_{0}, d, O) = (1, 2, 1, 0)$ , so the score contribution is $0 - 1 / 3 = - 1 / 3$ and the plug-in variance contribution is $1 \cdot 2 / 3^{2} = 2 / 9$ . Hence $U = 0$ and $\hat{V} = 4 / 9 > 0$ , giving standardized score zero. By [F2], ${\hat{S}}_{1} (t) = 1 - 1 / 4 = 3 / 4$ for $t_{1} \leq t \leq 2.5$ because the only group-1 failure is at $t_{1}$ ; and ${\hat{S}}_{0} (t) = 1$ for $t < t_{2}$ , then $1 - 1 / 2 = 1 / 2$ for $t_{2} \leq t \leq 2.5$ . The censorings contribute no product factors. Thus the empirical curves reverse order at $t_{2}$ . The cancellation of the score and the crossing population hazards show why this one sample statistic does not establish equality of the survival laws.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

An exact logrank randomization p-value with unequal assignment weights

Statement

Fix a follow-up horizon $τ = 3$ and three subjects. For every allowed assignment $z \in {e_{1}, e_{2}, e_{3}}$ , where $γ (e_{k})_{i} = 1 {i = k}$ is the binary group map that treats subject $k$ , prescribe the full records $(U_{i} (z), δ_{i} (z)) = (i, 1)$ for $i = 1, 2, 3$ . Thus the subjects have uncensored event times $1, 2, 3$ under every assignment, satisfying the full-record sharp null. Exactly one subject is treated. The allowed assignments $e_{1}, e_{2}, e_{3}$ treat subject 1, 2, or 3, respectively, with probabilities $1 / 2, 1 / 3, 1 / 6$ . Predeclare unit weight and the two-sided absolute unweighted logrank score before observing the assignment. Enumerate all scores and inclusive assignment-tail p-values and verify superuniformity under this unequal assignment law.

Facts & Assumptions

Given: The full-record schedule $(U_{i} (z), δ_{i} (z)) = (i, 1)$ for every $i \in {1, 2, 3}$ and every allowed assignment $z \in {e_{1}, e_{2}, e_{3}}$ , the binary group map $γ (e_{k})_{i} = 1 {i = k}$ , horizon $τ = 3$ , the declared assignment law, and the predeclared unit-weight absolute logrank ordering in Two-group logrank and weighted logrank scores.

[F1]

Two-group logrank and weighted logrank scores: at each event time, using the binary group map $γ (z)$ , the score contribution is $O_{j} - d_{j} Y_{1 j} / Y_{j}$ , the treated event count minus the total event count times the treated fraction of the current risk set. Here $d_{j} = 1$ at every event time.

[F2]

The logrank ordering gives a valid Fisher randomization p-value: under a full-record sharp null, the inclusive assignment-tail p-value uses the actual assignment weights and is superuniform.

[F3]

Finite randomized treatment-assignment models: assignment weights are nonnegative and sum to one on the finite allowed assignment set.

Proof

1.1F1F2givenalgebra

The prescribed full record for each subject is identical under all three allowed assignments, so the full-record sharp-null hypothesis in [F2] holds. Under the map $γ (e_{1})$ , the event at time 1 contributes $1 - 1 / 3 = 2 / 3$ and the later risk sets contain no treated subject, so $U (γ (e_{1})) = 2 / 3$ . Under $γ (e_{2})$ , time 1 contributes $- 1 / 3$ , and time 2 contributes $1 - 1 / 2 = 1 / 2$ , giving $U (γ (e_{2})) = 1 / 6$ . Under $γ (e_{3})$ , time 1 contributes $- 1 / 3$ , time 2 contributes $- 1 / 2$ , and time 3 contributes zero, giving $U (γ (e_{3})) = - 5 / 6$ . These are the three distinct scores; their absolute values are $2 / 3, 1 / 6, 5 / 6$ .

2.1F2F3step 1.1algebra

The inclusive absolute-tail probability at $e_{1}$ is $1 / 2 + 1 / 6 = 2 / 3$ , at $e_{2}$ it is $1$ , and at $e_{3}$ it is $1 / 6$ , because the absolute scores are distinct and the assignment weights are $1 / 2, 1 / 3, 1 / 6$ . Therefore the p-value takes $2 / 3, 1, 1 / 6$ with respective probabilities $1 / 2, 1 / 3, 1 / 6$ .

3.1F2F3step 2.1algebra∎

Its distribution function is $0$ for $0 \leq u < 1 / 6$ , $1 / 6$ for $1 / 6 \leq u < 2 / 3$ , $2 / 3$ for $2 / 3 \leq u < 1$ , and $1$ at $u = 1$ . On each interval this is at most $u$ , including the endpoints. Thus the exact finite assignment calculation is superuniform under the declared unequal-weight law, as in [F2].