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.

✓ 1 result · all verified · 1 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; all 1 also cleared it.

Cox PH and partial likelihood — Examples

1 · Prerequisites

2 · Summary

The worked example calculates a no-tie risk-set contribution, distinguishes an instantaneous hazard ratio from a cumulative event-risk ratio, and shows how time-varying covariate contrasts produce time-varying hazard ratios. Tied-event likelihoods require an explicitly stated grouped-time or coarsened-order convention.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

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.