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.

Risk-set likelihood and time-varying hazard-ratio check

Example

At one untied failure time $t$ , suppose the risk set is $R (t) = {1, 2, 3}$ , the failing subject is $2$ , and the covariate values at that time are $Z_{1} (t) = 0$ , $Z_{2} (t) = 1$ , and $Z_{3} (t) = 2$ . The partial-likelihood contribution is $\frac{e^{β}}{1 + e^{β} + e^{2 β}} .$ For a separate survival comparison, take baseline hazard $λ_{0} (t) = 1$ on $[0, 1]$ , $β_{0} = \log 2$ , and fixed covariates $z = 1$ and $z^{'} = 0$ . Their hazard ratio is $2$ , while their event-risk ratio by time $1$ is $1 + e^{- 1}$ . If instead $Z_{1} (t) = t$ and $Z_{2} (t) = 0$ , their instantaneous hazard ratio is $2^{t}$ , so the between-path hazard ratio varies over time even though $β$ is fixed.

Verification

Given: Use the Cox partial likelihood, survival, and hazard-ratio definitions in [F1]–[F3], and the predictability definition in [F4]. Verify the risk-set contribution and the two hazard comparisons.

[F1] Cox proportional-hazards model and partial likelihood: for untied failures, the partial likelihood uses each event subject's exponential weight divided by the sum of exponential weights over its risk set.

[F2] Cox proportional-hazards model and partial likelihood: at times with positive baseline hazard, the fixed-value hazard ratio is $e^{β^{T} (z - z^{'})}$ .

[F3] Cox proportional-hazards model and partial likelihood: for a constant covariate value $z$ , the event survival function is $S (t ∣ z) = \exp {- e^{β_{0}^{T} z} Λ_{0} (t)}$ .

[F4] Progressively measurable and predictable processes: deterministic Borel functions of time are predictable.

1.1givenF1algebra

Substituting $w_{j} (t) = e^{β Z_{j} (t)}$ for the three risk-set members in the no-tie partial-likelihood formula of [F1], subject $2$ contributes $e^{β} / (1 + e^{β} + e^{2 β})$ .

1.2givenF2F3algebra

For constant covariate $z$ , the survival formula [F3] with $λ_{0} (t) = 1$ gives $P (T \leq 1 ∣ z) = 1 - e^{- e^{β z}}$ . At $β_{0} = \log 2$ , the risks for $z = 1$ and $z^{'} = 0$ are $1 - e^{- 2}$ and $1 - e^{- 1}$ , so their ratio is $(1 - e^{- 2}) / (1 - e^{- 1}) = 1 + e^{- 1} < 2$ , although their hazard ratio from [F2] is $e^{β_{0} (z - z^{'})} = 2$ .

2.1givenF2F4algebra∎

By [F4], the deterministic paths $Z_{1} (t) = t$ and $Z_{2} (t) = 0$ are predictable. Substitution into the relative hazard factor of [F2] at $β_{0} = \log 2$ gives $e^{(\log 2) t} = 2^{t}$ , which equals $1$ at $t = 0$ and $2$ at $t = 1$ . Thus a fixed regression coefficient does not force the hazard ratio between changing covariate paths to be constant.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

Lu Tian, STAT331 Unit 5: Cox's Proportional Hazards Model, PDF pp. 7–14 (standard reference, not scraped)
Lu Tian, STAT331 Unit 7: Cox's Model: Extensions, PDF pp. 8–11 (standard reference, not scraped)
Qiqing Yu, Survival Analysis (Lecture Notes), §5.2, PDF pp. 58–63 (standard reference, not scraped)