Alphabeta Math
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 · 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. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Event observation, censoring, truncation — Examples

1 · Prerequisites

2 · Summary

The examples compute exponential event contributions for exact, right-censored, interval, current-status, delayed-entry, and right-truncated observations. A finite pair of dependent censoring models has the same observed (U,δ) law but different event-time distributions, and a uniform example computes how left truncation changes the selected law.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

Informative censoring can hide distinct event-time laws

Statement refuted

If two studies have the same observed right-censored law of (U,δ), then they have the same event-time law of T, even when censoring may depend on T.

Facts & Assumptions

Given: Right-censored data are U=min⁡(T,C) and δ=1{T≤C} as in Event-time observation, censoring, and truncation schemes. In Model A, P(T=1)=P(T=3)=1/2, with C=4 when T=1 and C=1/2 when T=3. In Model B, P(T=1)=P(T=2)=1/2, with C=4 when T=1 and C=1/2 when T=2. In both models, a separate study selects T∼Unif(0,3) subjects only when T>1.

[F1]

Right-censored observation records the minimum and the event indicator; left truncation selects only individuals with T>L. Informative censoring requires its joint observation law to be modeled. Event-time observation, censoring, and truncation schemes

[A1]

Model A and Model B are the two finite joint laws for (T,C) specified in Given.

[A2]

The separate truncation example has unconditional density 1/3 on (0,3) and inclusion event T>1.

Counterexample

1.1F1A1algebra

In Model A, the outcome T=1 has probability 1/2 and gives (U,δ)=(1,1) because C=4. The outcome T=3 has probability 1/2 and gives (U,δ)=(1/2,0) because C=1/2<T.

1.2F1A1algebra

In Model B, T=1 again gives (U,δ)=(1,1) with probability 1/2, while T=2 gives (U,δ)=(1/2,0) with probability 1/2.

1.3A2algebra

For the truncation example, P(T>1)=∫13(1/3) dt=2/3.

2.1step 1.1step 1.2algebra

Both observed laws assign probability 1/2 to each of (1,1) and (1/2,0), although the censoring time is a deterministic function of T in each model.

2.2A2step 1.3algebra

Conditional on inclusion, the event-time density is (1/3)/(2/3)=1/2 on (1,3) and zero outside, whereas the unselected density is 1/3 on (0,3). Thus left truncation changes the sampled event-time law.

3.1step 2.1A1algebra

The event-time laws differ: PA(T≤2)=1/2 and PB(T≤2)=1. Equal observed laws with different event-time laws contradict the refuted statement.

4.1step 3.1step 2.2F1∎

The finite censoring construction refutes the claim about equal observed laws, and the uniform calculation shows that truncation changes the sampling distribution by selection. Informative censoring requires its joint observation law to be modeled.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Exponential event-time observations with censoring and delayed entry

Example

Let T have exponential density fλ(t)=λe−λt on [0,∞), where λ>0. Use fixed administrative censoring times where specified, and use delayed entry at L=1 only for subjects selected by T>1. Compute the event-model factors for right-censoring, interval observation, current status, delayed entry, and right truncation.

Facts & Assumptions

Given: The exponential event-time density above; the observation conventions in Event-time observation, censoring, and truncation schemes; and the conditional likelihood formulas in Likelihood contributions under censoring, truncation, and delayed entry.

[F1]

Right censoring records U=min⁡(T,C) and δ=1{T≤C}; interval observation records L<T≤R; current status records 1{T≤C}; delayed entry selects T>L. Event-time observation, censoring, and truncation schemes

[F2]

Under the stated continuous event law, the right-censored event term is fλ(U)δSλ(U)1−δ; the interval term is Fλ(R)−Fλ(L); the current-status term is Fλ(C)δSλ(C)1−δ; delayed entry divides the event term by Sλ(L). Likelihood contributions under censoring, truncation, and delayed entry

Verification

1.1givenalgebra

Integrating the density gives Fλ(t)=1−e−λt and Sλ(t)=e−λt for t≥0; in particular Fλ(0)=0 and Sλ(0)=1.

2.1F1F2step 1.1

With fixed censoring time C=2, an event observed at U=1 has event factor fλ(1)=λe−λ and censor factor 1. A censored observation at U=2 has event factor Sλ(2)=e−2λ and censor factor 1 relative to the point-mass censoring law.

2.2F2step 1.1algebra

An interval observation 1<T≤2 has probability Fλ(2)−Fλ(1)=(1−e−2λ)−(1−e−λ)=e−λ−e−2λ.

2.3F2step 1.1algebra

At fixed inspection time C=1, current status δ=1 has event factor Fλ(1)=1−e−λ, and δ=0 has event factor Sλ(1)=e−λ.

2.4F2step 1.1algebra

After delayed entry L=1, with fixed censoring time C=3, an event observed at U=2 has conditional event factor fλ(2)/Sλ(1)=λe−2λ/e−λ=λe−λ. A censored observation at U=3 has conditional event factor Sλ(3)/Sλ(1)=e−2λ.

2.5F2step 1.1algebra

If instead the sample is right-truncated at R=2, the selected-sample density is λe−λt/(1−e−2λ) for 0≤t<2, since P(T<2)=Fλ(2)=1−e−2λ. This is a conditional event-time density, not a right-censoring contribution.

3.1step 2.1step 2.4step 2.5∎

The censoring and truncation examples use different event factors: ordinary right censoring uses fλ(u) or Sλ(u), delayed entry divides by Sλ(1), and right truncation divides by P(T<2).

Sources