ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Exponential and Weibull hazards with right-censored exposure

Example

Compare an exponential lifetime with rate $λ = 0.2$ and a Weibull lifetime with shape $k = 2$ and scale $η = 3$ . For right-censored exponential data, assume the three event times are iid $E x p (0.2)$ and use fixed censoring times $C_{i} = 5$ with observed records $(U_{i}, δ_{i}) = (2, 1), (5, 0), (3, 1)$ . The resulting subject pairs are iid because the censoring time is deterministic. The two exact event times are density observations under the continuous model, not point events of positive probability.

Facts & Assumptions

Given: Countable Choice, the exponential and Weibull families above, iid event times $T_{1}, T_{2}, T_{3} \sim E x p (0.2)$ for the likelihood calculation, an atomic lifetime law $P (T = 1) = 0.4$ , $P (T = 3) = 0.6$ for the jump calculation, and the fixed censoring design and right-censored records in the Example.

[F1]

Exponential and Weibull densities, survivals, and density hazards are as stated. Exponential and Weibull survival specifications define probability laws

[F2]

At an atom $t$ , $S (t) = S (t^{-}) (1 - q (t))$ ; for finite atomic support the survival values are the corresponding finite product. Survival jumps multiply by one minus the atomic hazard

[F3]

Under the iid, independent, parameter-distinct and common-domination hypotheses of Right-censored exponential likelihood and its boundary maximum, fix a censor parameter $ψ$ . The likelihood is $λ^{d} e^{- λ E} C_{ψ}$ , where $C_{ψ} = \prod_{i : δ_{i} = 1} {\overset{ˉ}{G}}_{ψ} (u_{i}) \prod_{i : δ_{i} = 0} g_{ψ} (u_{i})$ . If $C_{ψ} > 0$ , it is proportional in $λ$ to $λ^{d} e^{- λ E}$ , with unique maximum $d / E$ when $d > 0, E > 0$ . If $C_{ψ} = 0$ , it is zero for every $λ > 0$ .

[F4]

A likelihood is an explicitly chosen density version and is defined only up to reference-measure null sets; it is not the point probability of an exact continuous observation. Likelihood densities

[A1]

The censoring law is the point mass $G = δ_{5}$ , dominated by $ν = δ_{5}$ with density $g (5) = 1$ , and it has no event-rate parameter. Fixed censoring is independent of the event time. Event-time observation, censoring, and truncation schemes, The measure with density $f$ relative to $μ$

[F5]

A single-lifetime survival curve describes a nonrepairable unit; repeated failures of a repaired system require a recurrent-event model. Parametric survival and reliability models

[A2]

Countable Choice is used by the family, jump and likelihood results [F1]–[F3]. The Axiom of Countable Choice ( ${A C}_{ω}$ )

Verification

technique · direct

1.1A2F1givenalgebra

For $λ = 0.2$ , [F1] gives constant hazard $0.2$ ; its integral is $Λ (t) = 0.2 t$ , and the family survival is $S (3) = e^{- 0.6}$ . For $k = 2, η = 3$ , the density hazard is $2 t / 9$ , which is increasing on $t > 0$ , and $S (3) = e^{- 1}$ .

1.2A2F2givenalgebra

In the two-point lifetime law, $q (1) = 0.4 / 1 = 0.4$ and $q (3) = 0.6 / 0.6 = 1$ . Thus the jump-product formula gives $S (1) = 1 (1 - 0.4) = 0.6$ and $S (3) = 0.6 (1 - 1) = 0$ , matching the probabilities $P (T > 1)$ and $P (T > 3)$ .

1.3A1A2F3givenalgebra

For the fixed censoring design, $\overset{ˉ}{G} (2) = \overset{ˉ}{G} (3) = 1$ and $g (5) = 1$ , so the full censor-only factor is $C = \overset{ˉ}{G} (2) g (5) \overset{ˉ}{G} (3) = 1 > 0$ . The finite Borel dominator $ν = δ_{5}$ and its specified density satisfy [F3]'s domination hypotheses, while the iid event times and fixed censoring give iid independent subject pairs. Therefore $d = 2$ , $E = 2 + 5 + 3 = 10$ , and [F3] gives $L (λ) = λ^{2} e^{- 10 λ}$ with unique maximum $\hat{λ} = 2 / 10 = 0.2$ .

1.4F5given

The single-lifetime hazards above do not summarize repeated failures after repair.

2.1F1F4step 1.3

The event observations at $2$ and $3$ are evaluated through their Lebesgue density values. Accordingly, [F4] makes the likelihood a density evaluation, not the point probability of observing either exact time.

3.1step 1.1step 1.2step 1.3step 2.1step 1.4∎

Earlier steps 1.1, 1.2, 1.3, 1.4, and 2.1 verify the continuous hazard, atomic jump, censored exposure calculation, recurrent-event qualification, and density interpretation under their stated models.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

58 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

NIST/SEMATECH Engineering Statistics Handbook, Chapter 8, §§8.1.2 and 8.4.1.2, PDF pp. 12–17 and 159–161 (standard reference, not scraped)
Lu Tian, STAT331 Unit 2: Likelihood Construction, Inference for Parametric Survival Distributions, §2.2, PDF pp. 5–7 (standard reference, not scraped)