LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Binary monotonicity excludes defiers

Statement

In the binary setup of Binary-instrument principal strata and LATE, assume monotonicity $A (1) \geq A (0)$ almost surely. Then the always-taker, never-taker and complier events are pairwise disjoint and cover $Ω$ up to a null set; the defier event has probability zero.

Facts & Assumptions

Given: $A (0), A (1) \in {0, 1}$ and $A (1) \geq A (0)$ almost surely. Prove the principal-stratum partition.

[A1]

The potential treatments are binary and satisfy monotonicity almost surely. (Binary instrumental-variable potential-outcome setup)

[F1]

The four principal-stratum events are defined by the four possible pairs $(A (0), A (1))$ . (Binary-instrument principal strata and LATE)

Proof

1.1givenA1F1algebra

Since each coordinate is either $0$ or $1$ , the pair $(A (0), A (1))$ has only the four values $(0, 0), (0, 1), (1, 0), (1, 1)$ . Monotonicity in [A1] excludes $(1, 0)$ outside a null set. By [F1], the remaining three events are exactly the never-taker, complier and always-taker events.

2.1step 1.1F1∎

Distinct ordered pairs define disjoint events, and every pair outside the null exceptional set belongs to one of the three remaining events. Therefore these three strata form a partition up to a null set and the defier event is null.

Depends on

Used by

Dependency tree · two levels

5 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

Hernán and Robins, Causal Inference: What If, Chapter 16, §16.4 and Technical Point 16.7, printed pp. 217–225 (standard reference, not scraped)
Hyunseung Kang, Causal Inference: Identification Under Unmeasured Confounding (Instrumental Variables), Monotonicity-Based IV Assumptions and Compliance Types (standard reference, not scraped)