Corrections to: Sharp Bounds for Complier Average Potential Outcomes in Experiments with Noncompliance and Incomplete Reporting

Respondents in the replication data, by assignment $Z$ and viewing $D$ . The outcome $Y$ is coded as in the source study.
$Z$	$D$	Respondents	Outcome recorded	$Y = 1$	$Y = 0$	Outcome missing
0	0	415	379	167	212	36
0	1	80	79	40	39	1
1	0	320	294	130	164	26
1	1	185	177	110	67	8

Section 4, second paragraph: ‘we are able to fill in the necessary missing information ... Application of Corollary 1 yields ...’, read as the claim that the replication data and the assumptions of Section 2 point identify the complier average potential outcomes; the two witnesses are the validator's constructions and are not in the paper

p. 679 (PDF p. 3), Section 4, second paragraph; the assumptions are on p. 678 (PDF p. 2), Section 2

Section 4, p. 679, with the Section 2 assumptions, p. 678. The two explicit seventeen-atom laws have the stated integer completions, positive completed counts, Bernoulli parameters, conditional product construction, stratum probabilities, source table, full and respondent moments, and different complier means. They satisfy random assignment including response potentials and have the same recorded-data law; neither complier mean is a real-valued function of that law in all admissible models. The usual measure-theoretic conditions are assumed.

Historical component credits

Counterexample proved AronowAudit.P028.missing_outcome_counterexample Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; All standing assumptions hold for the concrete product laws: the atom type gives exclusion and binary bounds, finiteValid gives monotonicity and a positive first stage, and the other credited lemmas certify assignment and probability validity.
Proved AronowAudit.P028.finite_assignment_independent Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an algebraic supporting lemma, not a claim that an arbitrary BinaryLaw is a probability law. Positivity and normalization for the target witnesses are supplied by R185-05 and R185-08.
Proved AronowAudit.P028.missing_witness_assumptions Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; finiteValid includes the first-stage identity as a conjunct, but the theorem verifies it for two fixed objects instead of assuming an identification result.
Proved AronowAudit.P028.missing_witness_observed_cells Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Products with the independent positive assignment coin turn the latent finite sums into the stated assignment-conditional probabilities.
Proved AronowAudit.P028.missing_witness_same_observed_law Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Its component is already included in the counterexample or product-law certificate used here; no separate helper conclusion is packaged.
Proved AronowAudit.P028.missing_witness_complier_means Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Its component is already included in the counterexample or product-law certificate used here; no separate helper conclusion is packaged.
Proved AronowAudit.P028.missing_outcome_not_identified Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Quantifying the negation over a subclass does not narrow a non-identification counterexample: any identifying functional for the full class would distinguish these two admissible laws. Rational versus real representation loses no witness cases.
Proved AronowAudit.P028.missing_witness_reported_moments Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The universal quantifier ranges only over the two specified witness laws, exactly as required by N2 and N4; this is not offered as a general missing-data identity.
Proved AronowAudit.P028.missing_witness_corollary_comparison Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The full-population calculation and the available-case plug-in calculation remain distinct. Together with R185-06 the equalities give precisely N4 and N5.
Proved AronowAudit.P028.finite_joint_normalized Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Its component is already included in the counterexample or product-law certificate used here; no separate helper conclusion is packaged.
Proved AronowAudit.P028.missing_witness_joint_probability Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The positive normalized rational array is an ordinary finite probability distribution; no additional Measure-valued construction is needed for this concrete witness.

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:e5d876eaab1ea17acb5dc3c85f6c843137ce00cfc3013330beb381c3de33a43a

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): Two exact witnesses (validator's constructions; not in the paper): two probability laws that satisfy every assumption of Section 2 with binary outcomes, give the same law of everything that is observed when the outcome is recorded for some units only, and have different complier average potential outcomes. Notation for both witnesses. $Z \in \{0,1\}$ is assignment, with $\Pr[Z = 0] = 99/200$ and $\Pr[Z = 1] = 101/200$. $S \in \{A, N, C\}$ is the principal stratum, with $(D(0), D(1)) = (1,1)$ on $A$ (always-takers), $(0,0)$ on $N$ (never-takers) and $(0,1)$ on $C$ (compliers), and $$\Pr[S = A] = p_a = \tfrac{16}{99}, \qquad \Pr[S = N] = p_n = \tfrac{64}{101}, \qquad \Pr[S = C] = p_c = \tfrac{2047}{9999}.$$ $Y(0), Y(1) \in \{0,1\}$ are the potential outcomes ($Y(d,z) = Y(d)$). $R(0), R(1) \in \{0,1\}$ are potential response indicators: $R(z) = 1$ when the outcome is recorded under assignment $z$. $Z$ is independent of $(S, Y(0), Y(1), R(0), R(1))$. Observed variables: $D = D(Z)$, $Y = Y(D)$, $R = R(Z)$; the outcome is seen only when $R = 1$, so the observed data are $(Z, D, R, R \cdot Y)$. Source table. For the cell $(Z = z, D = d)$ let $s_{zd1}$, $s_{zd0}$, $m_{zd}$ be the numbers of recorded ones, recorded zeros and missing outcomes, and let $n_0 = 495$, $n_1 = 505$: cell $(0,0)$: $167,\ 212,\ 36$; cell $(0,1)$: $40,\ 39,\ 1$; cell $(1,0)$: $130,\ 164,\ 26$; cell $(1,1)$: $110,\ 67,\ 8$. (So $415 + 80 = 495$, $320 + 185 = 505$, and 71 of 1000 outcomes are missing.) Construction. A witness is fixed by a completion $x = (x_{00}, x_{01}, x_{10}, x_{11})$ with integers $0 \le x_{zd} \le m_{zd}$ ($x_{zd}$ is the number of missing outcomes of cell $(z,d)$ that are ones). Put $t_{zd1} = s_{zd1} + x_{zd}$, $t_{zd0} = s_{zd0} + m_{zd} - x_{zd}$, $a = t_{011}/80$, $b = t_{101}/320$ and $$\mu_0 = \frac{t_{001}/495 - t_{101}/505}{p_c}, \qquad \mu_1 = \frac{t_{111}/505 - t_{011}/495}{p_c}.$$ Given $S = A$: $Y(0) = 0$ and $Y(1) \sim \mathrm{Bernoulli}(a)$. Given $S = N$: $Y(0) \sim \mathrm{Bernoulli}(b)$ and $Y(1) = 0$. Given $S = C$: $Y(0)$ and $Y(1)$ are independent Bernoulli variables with means $\mu_0$ and $\mu_1$. Given $S$ and $(Y(0), Y(1))$: $R(0)$ and $R(1)$ are independent Bernoulli variables with success probabilities $q_{0,\,D(0),\,Y(D(0))}$ and $q_{1,\,D(1),\,Y(D(1))}$, where $q_{zdv} = s_{zdv}/t_{zdv}$. Lower witness: $x = (0, 1, 26, 0)$, so $a = 41/80$, $b = 39/80$, $\mu_0 = 1423/10235$, $\mu_1 = 6749/10235$. Upper witness: $x = (36, 0, 0, 8)$, so $a = 1/2$, $b = 13/32$, $\mu_0 = 7633/10235$, $\mu_1 = 7642/10235$. Each witness is a law with 17 atoms of positive rational mass on $(S, Y(0), Y(1), R(0), R(1))$, times the law of $Z$; the atoms and their masses are listed in the validator's models.json. Claims. (N1) In each witness the masses are positive and sum to 1; $(Y(0), Y(1), D(0), D(1), R(0), R(1))$ is independent of $Z$; $D(1) \ge D(0)$ on every atom; $\mathrm{E}[D(1) - D(0)] = P_c = 2047/9999 \ne 0$; $Y(0), Y(1) \in \{0,1\} \subset [0,1]$; $0 < \Pr[Z = 1] < 1$. So assumptions (i)–(iv) of Section 2 and bounded outcomes hold, and random assignment holds for the response potentials as well. (N2) In both witnesses, for all $z, d, v \in \{0,1\}$, $$\Pr[D = d, R = 1, Y = v \mid Z = z] = \frac{s_{zdv}}{n_z}, \qquad \Pr[D = d, R = 0 \mid Z = z] = \frac{m_{zd}}{n_z}.$$ Hence the two witnesses have the same law of the observed data $(Z, D, R, R \cdot Y)$. In particular both have $\Pr[D = 1|Z = 0] = 16/99$, $\Pr[D = 0|Z = 1] = 64/101$, respondent arm means $\mathrm{E}[Y|Z = 0, R = 1] = 207/458$ and $\mathrm{E}[Y|Z = 1, R = 1] = 240/471$, and respondent cell means $\mathrm{E}[Y|D = 1, Z = 0, R = 1] = 40/79$ and $\mathrm{E}[Y|D = 0, Z = 1, R = 1] = 130/294$. (N3) $\bigl(\mathrm{E}[Y(0)|D(1) > D(0)],\ \mathrm{E}[Y(1)|D(1) > D(0)]\bigr)$ equals $(1423/10235,\ 6749/10235)$ in the lower witness and $(7633/10235,\ 7642/10235)$ in the upper witness. The two pairs differ in both coordinates. (N4) The full-population arm means differ between the witnesses: $(EY_0, EY_1) = (208/495,\ 266/505)$ in the lower and $(27/55,\ 248/505)$ in the upper; in each witness the formula of Corollary 1 evaluated at the witness's own full-population moments returns the pair in (N3). (N5) The formula of Corollary 1 evaluated at the respondent moments of (N2), with the take-up probabilities of all units, gives the same pair in both witnesses, $$\left(\frac{1594452863}{3629163146},\ \frac{896530960}{1244058109}\right) \approx (0.4393,\ 0.7207),$$ which is the pair of complier means of neither witness. Consequence. The law of the observed data $(Z, D, R, R \cdot Y)$ together with assumptions (i)–(iv) and bounded outcomes does not determine $\mathrm{E}[Y(0)|D(1) > D(0)]$ or $\mathrm{E}[Y(1)|D(1) > D(0)]$: there is no function of the observed law that equals either complier mean in every model satisfying the assumptions. The printed inference from the replication data to the two point values therefore needs an added condition on response (P028-T2).

: SAP.P028.T1WholeStatement

Theorem: SAP.P028.T1

Statement hash: 7fdc462bfb445d7eb837882fde5d94ca072e307b704bca0e0befa86d2dac17ad

Statement definition: SAP.P028.T1WholeStatement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:49:53Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Manifest annotation reconciliation: Effective use follows the source-bound dependency observation; original annotations are retained in the crosswalk.

AronowAudit.P028.finite_joint_normalized: observed used

AronowAudit.P028.missing_witness_complier_means: observed used

AronowAudit.P028.missing_witness_same_observed_law: observed used

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T2

Section 4, second paragraph, the inference from the replication data to the complier means 0.43 and 0.72, as repaired by Sol: identification of the complier average potential outcomes from incompletely recorded outcomes under a stated response condition

p. 679 (PDF p. 3), Section 4, second paragraph; Corollary 1 is on p. 678 (PDF p. 2)

Section 4, p. 679, repaired using Corollary 1, p. 678. Joint moments identify complier means without positive treatment cells. The stated mean equalities justify mixed respondent formulas; conditional response independence suffices. Cellwise mean ignorability justifies reweighting but need not justify the mixed formulas. With unrestricted response the stated bounds depend only on the recorded-data law. All source-table values and approximations hold; both endpoints of each source interval are attained, so no valid interval can be narrower. The usual measure-theoretic conditions are assumed.

Historical component credits

Proved AronowAudit.P028.response_joint_moment_identity Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; These are exactly clause (i)'s identities: Boolean treatment indicators equal D or 1-D, and no positive treatment-assignment cell is required. The identities alone do not assert that the unrecorded full outcome moments are observed. The record also recognizes the boundedness generalization, but labels it faithful_with_notes rather than broader_than_claim.
Proved AronowAudit.P028.missing_moment_difference_bounds Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.response_mixed_identification Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The explicit M1/M2 hypotheses are assumptions of the corrected claim itself; they are not hidden assumptions of the printed point-identification assertion. All needed respondent means have positive events. No premise asserts that these response assumptions hold in the experiment.
Proved AronowAudit.P028.observed_y_measurable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.observed_y_integrable Historical support retained; baseline fidelity: ok; manifest: not used; not used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.null_cell_joint_moment Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.missing_probability_as_mean Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.recorded_joint_moment_bounds Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.normalized_arm_set_integral Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.normalized_arm_real Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.normalized_arm_integral Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.independent_response_factor Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.independent_arm_response_factor Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.arm_event_cell_indicator Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.arm_event_cell_outcome Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.independent_response_arm_mean Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This proves the M1 component of clause (iii). Joint response-arm positivity is equivalent to positive conditional response since the arm mass is already positive; no target case is excluded. Claim-stage verdict retained after reading the record.
Proved AronowAudit.P028.independent_response_cell_mean Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, moment-factorization, or scalar-bound component is already incorporated by the selected response theorems.
Proved AronowAudit.P028.response_independence_sufficient Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The row covers the q,r>0 component of clause (iii) described by row_says. Its conclusion gives M1, M2 and response positivity; together with R182-08 it yields the mixed identification formulas. The separate M1 result without q,r>0 belongs to the other split part. Boundedness is already in the corrected target setting and adds no restriction to it.
Proved AronowAudit.P028.response_cell_reweighting Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Both representation choices are exactly equivalent to the target conventions, since the conditioning arms and any cell to which the premise applies have positive mass. This row proves the three positive equalities of clause (iv); it does not itself supply the separate non-implication witness about unweighted respondent arm means.
Proved AronowAudit.P028.response_sensitivity_bounds Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The four endpoint expressions match clause (v) with treatment as the first subscript and assignment as the second. Recorded moments depend on (Z,D,R,RY) and missing probabilities on (Z,D,R), so the explicit expressions use only the observed-data law. There is no sharpness or sampling-confidence conclusion in this row; numerical endpoint attainment is assigned to T1.
Proved AronowAudit.P028.response_source_table_calculations Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The eight right-hand fractions agree with the target's worked instance, in order: the four sensitivity endpoints, the two mixed available-case values and the two reweighted-cell values. No response assumption, existence of a compatible observed law, or endpoint attainment is asserted by this arithmetic-only row.

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:bb8b86d8685cad9cd917f8aa5c8738674fe3cbbfd195a15063beadeb2a3ce53e

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): Sol's repair (validated.json, P028-N005, smallest_repair), verbatim: "State the target population, outcome/viewing coding and analysis denominators, and qualify the application by a sufficient response assumption for the moments actually estimated. For the mixed available-case approach, mean equality between respondents and the full population is needed for both assignment-arm outcome means and the two noncomplier-cell outcome means; response independent of (Y,D) within each assignment arm is one sufficient stronger condition. If assuming only mean-ignorable response within (D,Z) cells, reweight the observed cell means by full-sample cell probabilities before applying Corollary 1 and recompute. Without an added response assumption, replace the point-identification inference with missing-outcome sensitivity bounds." Mathematical content, with every hypothesis (validator's derivation.md, sections ‘Exact completions and the Corollary 1 identity’ and ‘Repair and dependency’). Setting: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$; in addition a response indicator $R \in \{0,1\}$ on the same space (the outcome is recorded when $R = 1$; $Z$ and $D$ are recorded for every unit). Write $C = \{D(1) > D(0)\}$, $P_c = \Pr(C) = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0] > 0$, $c_d = \mathrm{E}[Y(d)|C]$, $q = \Pr[D = 1|Z = 0]$, $r = \Pr[D = 0|Z = 1]$, so that $P_c = 1 - q - r$. (i) [Corollary 1 in joint-moment form; no condition on $R$ and no positivity of cells.] $$P_c\, c_0 = \mathrm{E}[Y(1 - D)|Z = 0] - \mathrm{E}[Y(1 - D)|Z = 1], \qquad P_c\, c_1 = \mathrm{E}[Y D|Z = 1] - \mathrm{E}[Y D|Z = 0].$$ (ii) [Mixed available-case version: take-up from all units, outcome means from respondents.] Suppose $q > 0$, $r > 0$, $\Pr[R = 1|Z = z] > 0$ for $z = 0, 1$, $\Pr[R = 1|D = 1, Z = 0] > 0$, $\Pr[R = 1|D = 0, Z = 1] > 0$, and (M1) $\mathrm{E}[Y|Z = z, R = 1] = \mathrm{E}[Y|Z = z]$ for $z = 0, 1$; (M2) $\mathrm{E}[Y|D = 1, Z = 0, R = 1] = \mathrm{E}[Y|D = 1, Z = 0]$ and $\mathrm{E}[Y|D = 0, Z = 1, R = 1] = \mathrm{E}[Y|D = 0, Z = 1]$. Then $$c_0 = \frac{\mathrm{E}[Y|Z = 0, R = 1] - q\,\mathrm{E}[Y|D = 1, Z = 0, R = 1] - r\,\mathrm{E}[Y|D = 0, Z = 1, R = 1]}{P_c}, \qquad c_1 = c_0 + \frac{\mathrm{E}[Y|Z = 1, R = 1] - \mathrm{E}[Y|Z = 0, R = 1]}{P_c}.$$ (iii) [A sufficient stronger condition.] If, for each $z \in \{0,1\}$, $R$ is independent of $(Y, D)$ conditionally on $Z = z$ and $\Pr[R = 1|Z = z] > 0$, then (M1) holds, (M2) holds whenever $q > 0$ and $r > 0$, and the response probabilities required in (ii) are positive; so the conclusion of (ii) holds. (iv) [Mean-ignorable response within $(D, Z)$ cells.] Suppose that for every $(d, z)$ with $\Pr[D = d|Z = z] > 0$, $\Pr[R = 1|D = d, Z = z] > 0$ and $\mathrm{E}[Y|D = d, Z = z, R = 1] = \mathrm{E}[Y|D = d, Z = z]$. Then, with the term of an empty cell omitted in each expression, $EY_z = \sum_{d} \Pr[D = d|Z = z]\,\mathrm{E}[Y|D = d, Z = z, R = 1]$ for $z = 0, 1$ and $$c_0 = \frac{\Pr[D = 0|Z = 0]\,\mathrm{E}[Y|D = 0, Z = 0, R = 1] - r\,\mathrm{E}[Y|D = 0, Z = 1, R = 1]}{P_c}, \qquad c_1 = \frac{\Pr[D = 1|Z = 1]\,\mathrm{E}[Y|D = 1, Z = 1, R = 1] - q\,\mathrm{E}[Y|D = 1, Z = 0, R = 1]}{P_c}.$$ Under this hypothesis alone the unweighted respondent arm means $\mathrm{E}[Y|Z = z, R = 1]$ need not equal $EY_z$, so the formula of (ii) is not justified by it. (v) [No response condition: sensitivity bounds.] With no condition on $R$, $$\frac{\mathrm{E}[R Y (1 - D)|Z = 0] - \mathrm{E}[R Y (1 - D)|Z = 1] - \Pr[R = 0, D = 0|Z = 1]}{P_c} \ \le\ c_0\ \le\ \frac{\mathrm{E}[R Y (1 - D)|Z = 0] + \Pr[R = 0, D = 0|Z = 0] - \mathrm{E}[R Y (1 - D)|Z = 1]}{P_c},$$ $$\frac{\mathrm{E}[R Y D|Z = 1] - \mathrm{E}[R Y D|Z = 0] - \Pr[R = 0, D = 1|Z = 0]}{P_c} \ \le\ c_1\ \le\ \frac{\mathrm{E}[R Y D|Z = 1] + \Pr[R = 0, D = 1|Z = 1] - \mathrm{E}[R Y D|Z = 0]}{P_c},$$ and every quantity on the outer sides is a function of the law of the observed data $(Z, D, R, R \cdot Y)$. Worked instance (the source table of P028-T1, read as a population law; validator's output.txt). (ii) gives $\left(\tfrac{1594452863}{3629163146}, \tfrac{896530960}{1244058109}\right) \approx (0.4393, 0.7207)$; (iv) gives $\left(\tfrac{16568969}{38014837}, \tfrac{295510}{414829}\right) \approx (0.4359, 0.7124)$; (v) gives $c_0 \in \left[\tfrac{1423}{10235}, \tfrac{7633}{10235}\right] \approx [0.1390, 0.7458]$ and $c_1 \in \left[\tfrac{6749}{10235}, \tfrac{7642}{10235}\right] \approx [0.6594, 0.7467]$, and each of the four endpoints is attained by a witness of P028-T1, so for this observed law the bounds of (v) cannot be narrowed without a response condition.

: SAP.P028.T2WholeStatement

Theorem: SAP.P028.T2

Statement hash: 5b42146f5bccd19b85c8dc4a4ee87d51f9493c0c91cf9ee6f99d9b58841da2d5

Statement definition: SAP.P028.T2WholeStatement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:49:53Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Manifest annotation reconciliation: Effective use follows the source-bound dependency observation; original annotations are retained in the crosswalk.

AronowAudit.P028.arm_event_cell_indicator: observed used

AronowAudit.P028.arm_event_cell_outcome: observed used

AronowAudit.P028.independent_arm_response_factor: observed used

AronowAudit.P028.independent_response_cell_mean: observed used

AronowAudit.P028.independent_response_factor: observed used

AronowAudit.P028.missing_moment_difference_bounds: observed used

AronowAudit.P028.missing_probability_as_mean: observed used

AronowAudit.P028.normalized_arm_integral: observed used

AronowAudit.P028.normalized_arm_real: observed used

AronowAudit.P028.normalized_arm_set_integral: observed used

AronowAudit.P028.null_cell_joint_moment: observed used

AronowAudit.P028.observed_y_measurable: observed used

AronowAudit.P028.recorded_joint_moment_bounds: observed used

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T3

Section 4 (Application), second paragraph, as printed, with the sentence of Section 2 on estimation by sample analogues

p. 679 (PDF p. 3), Section 4, second paragraph, with footnote 2; p. 678 (PDF p. 2), Section 2, second paragraph

No current theorem is supplied for this target.

Historical component credits

Not applicable Excluded association; baseline fidelity: None; manifest: not applicable; Solution use unverified; Historical excluded association.

Formal result: omitted

Scope: No credited Lean rows and no Lean formalization for this target; the printed empirical inference is not packaged using the separately credited T1 counterexample.

Omission: not formalized

Reason: No credited Lean rows and no Lean formalization for this target; the printed empirical inference is not packaged using the separately credited T1 counterexample.

Omission explanation

Assumptions and verification

Claim revision: catalog:828b7d784c884d827d18f1fbbb5d43d215e7d014ce6032998ce384d504c63113

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): As printed. Section 4, second paragraph, p. 679 (PDF p. 3): “Point identification is possible when additional information about the joint distribution of $Y$, $D$, $Z$ is known. Since the replication data set is publicly available for the study$^2$, we are able to fill in the necessary missing information: $\Pr[D = 1|Z = 0] = 0.163$, $\Pr[D = 0|Z = 1] = 0.634$, $\mathrm{E}[Y|D = 1, Z = 0] = 0.506$ and $\mathrm{E}[Y|D = 0, Z = 1] = 0.442$. Application of Corollary 1 yields $\mathrm{E}[Y(0)|D(1) > D(0)] = 0.43$ and $\mathrm{E}[Y(1)|D(1) > D(0)] = 0.72$. Our inferences are considerably tightened by knowledge of additional features of the distribution that were not reported.” Footnote 2, p. 679: “The replication data set for Mullainathan et al. (2010) is archived at http://isps.research.yale.edu/data/D049/.” The paragraph that precedes it, Section 4, first paragraph, p. 679: “We consider the encouragement study reported by Mullainathan et al. (2010), which randomly assigned an encouragement to watch a mayoral debate ($Z$) in order to assess the effect of watching ($D$) on changed views about at least one candidate ($Y$). The experiment had two-sided noncompliance, as both $\Pr[D = 0|Z = 1] > 0$ and $\Pr[D = 1|Z = 0] > 0$. The authors report estimates of $EY_0 = 0.45$, $EY_1 = 0.51$ and $P_c = 0.21$. While the CACE can be estimated as 29 percentage points, the authors do not provide sufficient information for point estimation of complier average potential outcomes. We now estimate sharp bounds on complier potential outcomes by application of Proposition 1. The bounds are rather wide: $\mathrm{E}[Y(0)|D(1) > D(0)] \in [0, 0.71]$ and $\mathrm{E}[Y(1)|D(1) > D(0)] \in [0.29, 1]$. Thus, although the CACE is identified, very little information is conveyed on complier potential outcomes by the published results.” The paper's statement on estimation, Section 2, p. 678 (PDF p. 2), after the LATE display: “where each component may be estimated using sample analogues to population quantities.” The hypotheses the paper attaches are those of Section 2 (assumptions (i)–(iv) and bounded outcomes, transcribed in the standing assumptions) and Corollary 1 (P028-T9). No response indicator, analysis population or assumption about unrecorded outcomes is printed anywhere in the paper.

Unit certificate (omission has no certified theorem). 20261104T182914Z

Declaration review: omission_ok; 2026-11-04T18:38:19Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Not supplied by this export. Manifest uses are reported separately; actual use is unverified.

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T4

Proof of Proposition 1, the sentence between Eq. (3) and the three-line display, corrected: upper limit $1 - P_c$ (printed 1) and ‘the implied value of $EY_c(0)$ ’ (printed $EY_c(1)$ )

p. 678 (PDF p. 2), proof of Proposition 1

proof of Proposition 1, p. 678 (PDF p. 2), corrected intermediate system. For 0 < p < 1 the corrected system is equivalent to the mixture equations and the printed intervals, with the stated substitutions, endpoint translations, unique noncomplier mean, and strict weakening caused by the printed residual constraint.

Historical component credits

Proved AronowAudit.P028.corrected_reframing Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Fidelity sweep: ok
Proved AronowAudit.P028.noncomplier_mean_from_equation Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained.
Proved AronowAudit.P028.control_substitution Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained.
Proved AronowAudit.P028.control_unit_interval Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained.
Proved AronowAudit.P028.contribution_interval Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained.
Proved AronowAudit.P028.third_lower_identity Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained.
Proved AronowAudit.P028.corrected_interval_system Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained. At p>1 both interval systems are infeasible, but the statement is nonvacuous on the target domain.
Proved AronowAudit.P028.endpoint_translation Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained.
Proved AronowAudit.P028.printed_contribution_interval Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained.
Proved AronowAudit.P028.printed_lower_redundant Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is an acceptable generalization: every case of the credited target component is retained. This row is the auxiliary redundancy inequality; strict non-equivalence is supplied at target level by specializing the two exact interval characterizations.

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:91e0a5716a71dbf3ad802722be107d5a190adc82291653b2caf30556ee737515

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): Corrected text (validated.json, P028-E001: smallest_repair and prior_correction.corrected_text). The sentence after Eq. (3) reads: “such that $0 \le EY_c(0) \le 1$, $0 \le EY_c(1) \le 1$, and $0 \le EY_1 - P_c EY_c(1) \le 1 - P_c$. Then substituting the implied value of $EY_c(0)$ from Eq. (3) into the system of inequalities and rearranging terms, we obtain” followed by the three displayed lines, which are unchanged: $$0 \le EY_c(1) \le 1,$$ $$(EY_1 - EY_0)/P_c \le EY_c(1) \le 1 + (EY_1 - EY_0)/P_c,$$ $$(EY_1 + P_c - 1)/P_c \le EY_c(1) \le EY_1/P_c.$$ Sol's repair, verbatim: "Replace $0\le EY_1-P_cEY_c(1)\le1$ by $0\le EY_1-P_cEY_c(1)\le1-P_c$; replace “the implied value of $EY_c(1)$” by “the implied value of $EY_c(0)$”." Mathematical content, with every hypothesis. Let $p, e_0, e_1, x_0, x_1$ be real numbers with $0 < p < 1$ (they stand for $P_c$, $EY_0$, $EY_1$, $EY_c(0)$, $EY_c(1)$), and put $\tau = (e_1 - e_0)/p$. (i) [The reframing is an equivalence.] There is a real number $n$ with $$p\,x_0 + (1 - p)\,n = e_0, \qquad p\,x_1 + (1 - p)\,n = e_1, \qquad 0 \le x_0 \le 1,\quad 0 \le x_1 \le 1,\quad 0 \le n \le 1$$ if and only if $$p\,x_0 + e_1 - p\,x_1 = e_0, \qquad 0 \le x_0 \le 1,\quad 0 \le x_1 \le 1,\quad 0 \le e_1 - p\,x_1 \le 1 - p.$$ When such an $n$ exists it is $n = (e_1 - p\,x_1)/(1 - p)$. (ii) [Substituting the implied value of $x_0$.] $p\,x_0 + e_1 - p\,x_1 = e_0$ if and only if $x_0 = x_1 - \tau$. If $x_0 = x_1 - \tau$, then $0 \le x_0 \le 1 \iff \tau \le x_1 \le 1 + \tau$. Moreover $0 \le e_1 - p\,x_1 \le 1 - p \iff (e_1 + p - 1)/p \le x_1 \le e_1/p$. (iii) [The intervals of Proposition 1.] Hence the system of (i) holds if and only if $x_0 = x_1 - \tau$ and $$\max\left\{0,\ \tau,\ 1 - \frac{1 - e_1}{p}\right\} \le x_1 \le \min\left\{1,\ 1 + \tau,\ \frac{e_1}{p}\right\}$$ (note $(e_1 + p - 1)/p = 1 - (1 - e_1)/p$), which is the treated interval of Proposition 1. Subtracting $\tau$ from its endpoints gives the control interval: $$\max\left\{0, \tau, 1 - \frac{1 - e_1}{p}\right\} - \tau = \max\left\{0,\ -\tau,\ 1 - \frac{1 - e_0}{p}\right\}, \qquad \min\left\{1, 1 + \tau, \frac{e_1}{p}\right\} - \tau = \min\left\{1,\ 1 - \tau,\ \frac{e_0}{p}\right\}.$$ (iv) [What the printed constraint gives.] $0 \le e_1 - p\,x_1 \le 1 \iff (e_1 - 1)/p \le x_1 \le e_1/p$. If $e_1 \le 1$, the lower half is implied by $x_1 \ge 0$, so the printed third constraint adds only $x_1 \le e_1/p$ and does not give the lower limit $(e_1 + p - 1)/p$ of the third displayed line; the system with the printed constraint is implied by, and is not equivalent to, the system with $0 \le n \le 1$ (P028-T5).

: SAP.P028.T4Statement

Theorem: SAP.P028.T4

Statement hash: fe4489e06a2f4e73c78fd3a5584c852207cb31824bca7a4d56db65437189e807

Statement definition: SAP.P028.T4Statement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:49:53Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T5

Proof of Proposition 1, the system printed after Eq. (3) (‘such that ... and $0 \le EY_1 - P_c EY_c(1) \le 1$ ’), offered as a reframing of Eqs. (1)–(2) with their constraints; the witness is the validator's and is not in the paper

p. 678 (PDF p. 2), proof of Proposition 1, between Eq. (3) and the three-line display

proof of Proposition 1 after Eq. (3), p. 678. The exact candidate (1/2,3/4,3/4,0,0) satisfies the printed system and fails the constrained mixture equations: its forced noncomplier mean is 3/2. The two printed feasible coordinate sets are [0,1], while the corrected mixture sets and Proposition 1 intervals are [1/2,1]. The input triple has the specified realization with half compliers of outcome one, half never-takers of outcome one half, and independent fair assignment. The usual measure-theoretic conditions are assumed.

Historical component credits

Counterexample proved AronowAudit.P028.misprinted_constraint_counterexample Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This row correctly supplies a disqualifying point and the numerical Proposition 1 endpoints. It does not itself characterize the whole feasible ranges asserted in E5, which remains a target-level coverage gap.
Proved AronowAudit.P028.misprinted_witness_admissible_inputs Limited support; baseline fidelity: narrower; manifest: not used; not used in Solution; {'source': 'adjudication+second review', 'adjudicator': 'P028/P028_Results.lean:1715 asserts only the existence of a bounded randomized model with p=1/2, arm means 3/4, and complier means 1. T5(E6) specifically asserts a half-complier, half-never-taker population with both potential outcomes constant within each stratum and an independent fair assignment coin. Neither the never-taker mass, the constant noncomplier potentials, nor assignment probability 1/2 is exported or implied by CausalModel. For example, half compliers with potentials (1,1), half always-takers with potentials (1/2,1/2), and independent assignment probability 1/3 satisfy every exported condition but have none of the required never-takers and use an unfair coin. This confirms the missing conclusions for E6, while leaving the weaker admissibility-of-inputs assertion valid.', 'suggested_fix': "Strengthen the existential conclusion to include M.μ.real (neverEvent M) = 1/2, M.μ.real (armEvent M z) = 1/2 for both z, and the almost-everywhere stratum-specific potential values Y(d)=1 on compliers and Y(d)=1/2 on never-takers for both d. Together with the existing complier mass and randomAssignment field, these specify E6's population law; the always-taker mass is then zero.", 'second_review': "P028/P028_Results.lean:1715 exports an existential bounded model with P_c=1/2, arm means 3/4 and complier means 1, while T5(E6) specifies a half-complier, half-never-taker law with stratum-constant potentials and independent fair assignment. Neither the never-taker mass, its potential values, nor assignment fairness follows from that conclusion or CausalModel's randomAssignment and armPositive fields at P028/P028_Results.lean:234 and :235. Half compliers with potentials (1,1), half always-takers with potentials (1/2,1/2), and independent assignment probability 1/3 satisfy every exported condition, so the missing specifications are substantive. Strengthen the existential conclusion to specify E6's law; attainingMeasure and attainingModel at P028/P028_Results.lean:901 and :927 already provide the intended construction, making a statement repair appropriate.", 'severity': 'major'}

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:26518c6a1fd7da4e2dc134ba61cb35c7432d8f536d66de234c64848ccc45b93c

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): Exact witness (validator's; not in the paper) that the system printed after Eq. (3) is not equivalent to Eqs. (1)–(2) with the constraints $0 \le EY_c(0) \le 1$, $0 \le EY_c(1) \le 1$, $0 \le EY_n \le 1$. Take $$P_c = \tfrac12, \qquad EY_0 = EY_1 = \tfrac34, \qquad EY_c(0) = EY_c(1) = 0.$$ Claims. (E1) Eq. (3) holds: $\tfrac12 \cdot 0 + \tfrac34 - \tfrac12 \cdot 0 = \tfrac34$. (E2) The three printed constraints hold: $0 \le EY_c(0) = 0 \le 1$, $0 \le EY_c(1) = 0 \le 1$ and $0 \le EY_1 - P_c EY_c(1) = \tfrac34 \le 1$. (E3) The value of $EY_n$ given by Eq. (2) is $[EY_1 - P_c EY_c(1)]/(1 - P_c) = (3/4)/(1/2) = 3/2 > 1$; so no $EY_n \in [0,1]$ satisfies Eqs. (1)–(2) with these complier means, and the corrected constraint fails: $EY_1 - P_c EY_c(1) = \tfrac34 > \tfrac12 = 1 - P_c$. (E4) The printed third constraint gives only $EY_c(1) \ge (EY_1 - 1)/P_c = -\tfrac12$, whereas the third displayed line of the proof has $EY_c(1) \ge (EY_1 + P_c - 1)/P_c = \tfrac12$. (E5) For $(P_c, EY_0, EY_1) = (\tfrac12, \tfrac34, \tfrac34)$ the set of values of $EY_c(1)$ admitted by the printed system (Eq. (3) with the three printed constraints) is $[0, 1]$, while the set admitted by Eqs. (1)–(2) with their constraints, which is the treated interval of Proposition 1, is $[\tfrac12, 1]$; since $(EY_1 - EY_0)/P_c = 0$ the same holds for $EY_c(0)$. (E6) The triple is attained under the assumptions of Section 2: a population with a fraction $\tfrac12$ of compliers with $Y(0) = Y(1) = 1$ and a fraction $\tfrac12$ of never-takers with $Y(0) = Y(1) = \tfrac12$, assigned by an independent fair coin, has $P_c = \tfrac12$ and $EY_0 = EY_1 = \tfrac34$. Consequence. The printed reframing admits complier means that no model with the given $(P_c, EY_0, EY_1)$ has, and the third displayed line of the proof does not follow from the printed third constraint. Proposition 1 itself is not contradicted: its intervals for this triple are $[\tfrac12, 1]$ and $[\tfrac12, 1]$.

: SAP.P028.T5WholeStatement

Theorem: SAP.P028.T5

Statement hash: c65a4eb0103737a8e21fa289fbf4139e0d162bb0fe14deef876efe1f0c70d868

Statement definition: SAP.P028.T5WholeStatement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:49:53Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Manifest annotation reconciliation: Effective use follows the source-bound dependency observation; original annotations are retained in the crosswalk.

AronowAudit.P028.misprinted_witness_admissible_inputs: observed not used

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T6

Proof of Proposition 1 with the full-compliance case $P_c = 1$ supplied, and the substitution in the proof of Corollary 1 written without a non-complier mean, as repaired by Sol

p. 678 (PDF p. 2), proof of Proposition 1 (‘Define $EY_n \equiv \mathrm{E}[Y|D(1) = D(0)]$ ’ and ‘Since $EY_n = [EY_1 - P_c EY_c(1)]/(1 - P_c)$ ’); p. 679 (PDF p. 3), proof of Corollary 1

Proposition 1 proof, p. 678, and Corollary 1 proof, p. 679. A bounded causal model has positive complier probability at most one, and full compliance is allowed. The noncomplier contribution gives the mixture identities, the partial- and full-compliance branches, cell-compatible observable formulas, both bounds, and singleton boundary intervals. Positive pure cells give the printed probability-times-mean expression; empty cells have zero product moment. The usual measure-theoretic conditions are assumed.

Historical component credits

Proved AronowAudit.P028.boundary_proof_repair Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Covers target clauses (i)–(iv) and the product-moment complier-mean formulas of (v). Endpoint bounds and singleton identities are covered by separate credited rows; the theorem does not assume its mixture conclusions in the model.
Proved AronowAudit.P028.full_compliance_endpoints Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Exactly target (vii). This is the required p=1 component, so fixing p to one is not an additional restriction on the component credited to this row.
Proved AronowAudit.P028.stratum_cases Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.stratum_measurable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.arm_measurable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.potential_arm_measurable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.potential_arm_integrable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.arm_mean_population Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.population_mixture Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.noncomplier_probability_partition Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.bounded_set_moment Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.noncomplier_contribution_bounds Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.complier_mean_bounds Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary unit-interval bound, rather than the full endpoint interval. The conditioning denominator p is strictly positive by the model’s monotonicity and nonzero first stage.
Proved AronowAudit.P028.pure_cell_product_moments Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.arm_joint_moment_partition Historical support retained; baseline fidelity: ok; manifest: not used; not used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.noncomplier_contribution_observable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.noncomplier_event_probability Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.noncomplier_outcome_moment Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.noncomplier_mean_positive_formula Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.complier_probability_le_one Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.full_compliance_population Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary mixture, probability, regularity, or bounds component is already incorporated by boundary_proof_repair and the selected bound theorems.
Proved AronowAudit.P028.bounds_from_mixture_moments Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary real algebra for target (vi), not an assertion that mixture equations have been derived from the causal assumptions. They are exported for causal models by boundary_proof_repair; the contribution hypotheses imply p≤1.

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:9136f932870754c404062bf495d6c284d95cc5dcdf9239d27f2268c096168588

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): Sol's repair (validated.json, P028-E002, smallest_repair), verbatim: "Prepend to Proposition 1's proof: 'If P_c=1, every unit is a complier, so EY_c(0)=EY_0 and EY_c(1)=EY_1; the displayed intervals reduce to these singletons. Henceforth suppose 0<P_c<1.' If Corollary 1 is also to cover empty treatment-assignment cells, replace pure-cell probability-times-mean terms by m=E[Y·D|Z=0]+E[Y·(1-D)|Z=1] and use EY_c(z)=(EY_z-m)/P_c, avoiding a noncomplier mean." Mathematical content, with every hypothesis (validator's derivation.md, sections 1 and 3–5). Setting: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. Write $C$, $A$, $N$ for the compliers, always-takers and never-takers, $p = P_c = \Pr(C)$, $e_z = EY_z$ and $c_d = \mathrm{E}[Y(d)|C]$. (i) [The assumptions allow the boundary.] $0 < p \le 1$, so $c_0$ and $c_1$ are defined; the assumptions do not imply $p < 1$ (P028-T7). (ii) [Mixture equations with no mean over a possibly empty group.] Define the non-complier contribution $m = \mathrm{E}[\mathbf{1}_A\,Y(1)] + \mathrm{E}[\mathbf{1}_N\,Y(0)]$. Then $$0 \le m \le 1 - p, \qquad e_0 = p\,c_0 + m, \qquad e_1 = p\,c_1 + m.$$ (iii) [$m$ in observable terms.] $m = \mathrm{E}[Y \cdot D \mid Z = 0] + \mathrm{E}[Y \cdot (1 - D) \mid Z = 1]$, where $Y$ is the observed outcome and the products are ordinary multiplication. (iv) [The two cases.] If $p < 1$, then $\Pr[D(1) = D(0)] = 1 - p > 0$, $EY_n = \mathrm{E}[Y|D(1) = D(0)]$ is defined, $m = (1 - p)\,EY_n$ with $0 \le EY_n \le 1$, and (ii) is Eqs. (1)–(2) of the printed proof. If $p = 1$, then $m = 0$, $c_0 = e_0$ and $c_1 = e_1$. (v) [Corollary 1 without a non-complier mean; an optional extension to empty cells.] For every $p \in (0, 1]$, $c_0 = (e_0 - m)/p$ and $c_1 = (e_1 - m)/p$ with $m$ as in (iii); no cell $(D = d, Z = z)$ is required to have positive probability. When $\Pr[D = 1|Z = 0] > 0$ and $\Pr[D = 0|Z = 1] > 0$, $m = \Pr[D = 1|Z = 0]\,\mathrm{E}[Y|D = 1, Z = 0] + \Pr[D = 0|Z = 1]\,\mathrm{E}[Y|D = 0, Z = 1]$, and this is the formula printed in Corollary 1; the product moment of an empty cell is 0. (vi) [The bounds for every $p \in (0, 1]$, with no division by $1 - p$.] Put $\tau = (e_1 - e_0)/p$. From (ii) and $0 \le c_0 \le 1$, $0 \le c_1 \le 1$: $c_1 = c_0 + \tau$; $0 \le e_1 - p\,c_1 \le 1 - p$, that is, $1 - (1 - e_1)/p \le c_1 \le e_1/p$; and $0 \le e_0 - p\,c_0 \le 1 - p$, that is, $1 - (1 - e_0)/p \le c_0 \le e_0/p$. Hence $c_0$ and $c_1$ lie in the two intervals of Proposition 1. (vii) [The printed intervals at the boundary.] For all real $e_0, e_1 \in [0, 1]$, at $P_c = 1$ the intervals of Proposition 1 are the singletons $\{e_0\}$ and $\{e_1\}$: $$\max\{0,\ e_0 - e_1,\ e_0\} = \min\{1,\ 1 - e_1 + e_0,\ e_0\} = e_0, \qquad \max\{0,\ e_1 - e_0,\ e_1\} = \min\{1,\ 1 + e_1 - e_0,\ e_1\} = e_1.$$

: SAP.P028.T6WholeStatement

Theorem: SAP.P028.T6

Statement hash: 9bfadf12bcf0a962d2f782e49c0cc5e86614b614ca6fbc17ddd0bc3cfb23de15

Statement definition: SAP.P028.T6WholeStatement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:49:53Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Manifest annotation reconciliation: Effective use follows the source-bound dependency observation; original annotations are retained in the crosswalk.

AronowAudit.P028.arm_mean_population: observed used

AronowAudit.P028.arm_measurable: observed used

AronowAudit.P028.bounded_set_moment: observed used

AronowAudit.P028.complier_probability_le_one: observed used

AronowAudit.P028.full_compliance_population: observed used

AronowAudit.P028.noncomplier_contribution_bounds: observed used

AronowAudit.P028.noncomplier_contribution_observable: observed used

AronowAudit.P028.noncomplier_event_probability: observed used

AronowAudit.P028.noncomplier_mean_positive_formula: observed used

AronowAudit.P028.noncomplier_outcome_moment: observed used

AronowAudit.P028.noncomplier_probability_partition: observed used

AronowAudit.P028.population_mixture: observed used

AronowAudit.P028.potential_arm_integrable: observed used

AronowAudit.P028.potential_arm_measurable: observed used

AronowAudit.P028.pure_cell_product_moments: observed used

AronowAudit.P028.stratum_cases: observed used

AronowAudit.P028.stratum_measurable: observed used

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T7

Proof of Proposition 1, ‘Define $EY_n \equiv \mathrm{E}[Y|D(1) = D(0)]$ ’ and ‘Since $EY_n = [EY_1 - P_c EY_c(1)]/(1 - P_c)$ ’, used without the condition $P_c < 1$ ; the witness is the validator's and is not in the paper

p. 678 (PDF p. 2), proof of Proposition 1; the assumptions are in Section 2 on the same page; the related ratio is in the proof of Corollary 1, p. 679 (PDF p. 3)

proof of Proposition 1, p. 678 (PDF p. 2), and Corollary 1 proof, p. 679. An explicit two-atom randomized full-compliance law has the stated outcome means, null noncomplier and pure-cell events, zero proof denominators and numerators, undetermined noncomplier mean, and valid singleton Proposition 1 intervals.

Historical component credits

Counterexample proved AronowAudit.P028.full_compliance_counterexample Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Zero joint pure-cell masses are equivalent to zero assignment-conditional probabilities because both arms have probability 1/2. Null-event and zero-denominator assertions faithfully express failed side conditions without asserting that Lean division is undefined.
Proved AronowAudit.P028.full_compliance_witness_intervals Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; This is exactly the concrete F6 evaluation; it is not credited as the general full-compliance repair.
Proved AronowAudit.P028.full_compliance_independent Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Triviality of constant-vector independence is a genuine F1 witness fact; it is not used to assert independence for nonconstant vectors.

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:6849a029f904e5ef2efbc17ceec99dad4b5150a5d11a7f5f033ad6271c84b19b

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): Exact witness (validator's; not in the paper): a model that satisfies every assumption of Section 2 and in which the non-complier group is empty, so that the proof's definition of $EY_n$ conditions on a null event and its division is by $1 - P_c = 0$. The probability space has two atoms, each of probability $\tfrac12$. Atom 1: $Z = 0$, $D(0) = 0$, $D(1) = 1$, $Y(0) = 0$, $Y(1) = 1$; observed $D = 0$, $Y = 0$. Atom 2: $Z = 1$, $D(0) = 0$, $D(1) = 1$, $Y(0) = 0$, $Y(1) = 1$; observed $D = 1$, $Y = 1$. Here $Y(d, z) = Y(d)$, $D = D(Z)$ and $Y = Y(D)$. Claims. (F1) The assumptions hold: $(Y(0), Y(1), D(0), D(1))$ is constant, hence independent of $Z$; exclusion holds by the definition of $Y(d,z)$; $D(1) = 1 \ge 0 = D(0)$; $\mathrm{E}[D(1) - D(0)] = 1 \ne 0$; $Y(0), Y(1) \in [0, 1]$; $\Pr[Z = 0] = \Pr[Z = 1] = \tfrac12 > 0$. (F2) $P_c = 1$, $EY_0 = 0$, $EY_1 = 1$, $EY_c(0) = \mathrm{E}[Y(0)|D(1) > D(0)] = 0$ and $EY_c(1) = \mathrm{E}[Y(1)|D(1) > D(0)] = 1$. (F3) $\Pr[D(1) = D(0)] = 0$, $1 - P_c = 0$ and $EY_1 - P_c EY_c(1) = 0$: the conditioning event of $EY_n \equiv \mathrm{E}[Y|D(1) = D(0)]$ has probability zero, and the printed quotient $[EY_1 - P_c EY_c(1)]/(1 - P_c)$ has numerator 0 and denominator 0. (F4) With $P_c = 1$, Eqs. (1) and (2) read $EY_c(0) = EY_0$ and $EY_c(1) = EY_1$ and hold for every real number put in the place of $EY_n$; so Eq. (2) does not determine $EY_n$, and the step ‘Since $EY_n = [EY_1 - P_c EY_c(1)]/(1 - P_c)$’ is not available. (F5) $\Pr[D = 1|Z = 0] = \Pr[D = 0|Z = 1] = 0$: the cells $(D = 1, Z = 0)$ and $(D = 0, Z = 1)$ are empty, $\mathrm{E}[Y|D = 1, Z = 0]$ and $\mathrm{E}[Y|D = 0, Z = 1]$ are conditional means on null events, and the ratio in the proof of Corollary 1 has denominator $\Pr[D = 1|Z = 0] + \Pr[D = 0|Z = 1] = 0$ and, whatever values are assigned to the two empty-cell means (for instance $\tfrac13$ and $\tfrac23$), numerator 0. (F6) The conclusion of Proposition 1 holds in the witness: at $(P_c, EY_0, EY_1) = (1, 0, 1)$ the printed intervals are $[0, 0]$ and $[1, 1]$, which contain $EY_c(0) = 0$ and $EY_c(1) = 1$. Consequence. The assumptions of Section 2 do not imply $P_c < 1$, and the printed proof of Proposition 1 has no branch for $P_c = 1$; the proposition's intervals are nevertheless correct there (P028-T6). The witness does not satisfy the premise of Corollary 1 on its ordinary reading (two of the four cell means do not exist), so it is not a counterexample to the corollary.

: SAP.P028.T7Statement

Theorem: SAP.P028.T7

Statement hash: 1782054f1e44b31929bac57ecfe09592de93e5fe0e3d267aabb3c03b42e11217

Statement definition: SAP.P028.T7Statement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:46:52Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T8

Proposition 1, with its printed proof, Eqs. (1)–(3)

p. 678 (PDF p. 2), Section 3

Proposition 1, Section 3, p. 678 (PDF p. 2). Both complier means lie in the printed intervals, which are nonempty for every compatible triple and attain every value through bounded randomized models, including full compliance.

Historical component credits

Proved AronowAudit.P028.proposition1_valid Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; {'source': 'adjudication', 'decision': 'rejected', 'what': "P028/P028_Results.lean:1089 exports all four inequalities in Proposition 1's two printed intervals and the identified difference between the complier means. CausalModel at line 224 encodes the three monotone treatment types, exclusion, joint random assignment, and nonzero first stage on an arbitrary probability space; boundedOutcomes at line 281 uses the bounded-potential-outcome reading specified in the standing assumptions. Positive assignment arms implement existence of the printed ordinary arm means, and there is no p<1 restriction. Sharpness is the separate component covered by proposition1_sharp, so its separation from this validity statement omits no conclusion assigned to this component."}
Proved AronowAudit.P028.sharpness_moment_certificate Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.compatible_mixture_moments Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.attaining_integral Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.attaining_arm_probability Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.attaining_model_bounded Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.attaining_model_moments Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.realize_mixture_moments Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.proposition1_sharp Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; {'source': 'adjudication', 'decision': 'rejected', 'what': 'P028/P028_Results.lean:1109 quantifies over every admissible triple and every point x1 of the printed treated interval, and concludes existence of an actual bounded randomized causal model with those three moments and complier means x1 and x1-effect. Proposition 1 says that only EY1, EY0, and Pc are known, so it does not require preserving a particular assignment probability or noncomplier-stratum split. The finite witness therefore suffices for sharpness, and endpoint_translation at line 131 converts every control-interval point to a treated-interval point; full compliance remains included.'}
Proved AronowAudit.P028.proposition1_compatible_triples Historical support retained; baseline fidelity: ok; manifest: not used; not used in Solution; Auxiliary construction or compatibility certificate is incorporated in the selected validity, nonemptiness, and sharpness declarations.
Proved AronowAudit.P028.proposition1_interval_nonempty Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; {'source': 'adjudication', 'decision': 'rejected', 'what': 'P028/P028_Results.lean:1692 directly states nonemptiness of the treated interval exactly when |e1-e0|<=p for bounded arm means and 0<p<=1. Although the row refers to both printed intervals, endpoint_translation at line 131 identifies each control endpoint with the corresponding treated endpoint minus the same effect. Translation preserves endpoint order, so the control nonemptiness assertion is the same condition and no conclusion or input case is materially lost.'}

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:aa4353cfb95bc820244321fabc96a285cb32dc5838880901a41af2fb61efac00

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): [Setting, Section 2, p. 678 (PDF p. 2)] The proposition is stated under the setting of Section 2: assumptions (i) random assignment, (ii) exclusion restriction, (iii) non-zero first-stage effect, (iv) monotonicity, the definitions $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, $EY_0 \equiv \mathrm{E}[Y|Z = 0]$, and ‘we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$’ (transcribed in full in the standing assumptions). [Sentence introducing it, Section 3, p. 678] “Proposition 1 asserts the intervals for complier potential outcomes identified under incomplete reporting.” [p. 678] Proposition 1. When only $EY_1$, $EY_0$ and $P_c$ are known, sharp bounds exist for the complier average potential outcomes. The average control potential outcome for compliers, $\mathrm{E}[Y(0)|D(1) > D(0)]$ lies in $$\left[\max\left\{0,\ -\frac{EY_1 - EY_0}{P_c},\ 1 - \frac{1 - EY_0}{P_c}\right\},\ \min\left\{1,\ 1 - \frac{EY_1 - EY_0}{P_c},\ \frac{EY_0}{P_c}\right\}\right].$$ Similarly, the average treated potential outcome for compliers, $\mathrm{E}[Y(1)|D(1) > D(0)]$, lies in $$\left[\max\left\{0,\ \frac{EY_1 - EY_0}{P_c},\ 1 - \frac{1 - EY_1}{P_c}\right\},\ \min\left\{1,\ 1 + \frac{EY_1 - EY_0}{P_c},\ \frac{EY_1}{P_c}\right\}\right].$$ [Proof as printed, p. 678] Proof. Define $EY_n \equiv \mathrm{E}[Y|D(1) = D(0)]$, $EY_c(0) \equiv \mathrm{E}[Y(0)|D(1) > D(0)]$ and $EY_c(1) \equiv \mathrm{E}[Y(1)|D(1) > D(0)]$. By the law of total probability, $$P_c EY_c(0) + (1 - P_c)EY_n = EY_0, \qquad (1)$$ $$P_c EY_c(1) + (1 - P_c)EY_n = EY_1, \qquad (2)$$ given the constraints that $0 \le EY_c(0) \le 1$, $0 \le EY_c(1) \le 1$, and $0 \le EY_n \le 1$. Since $EY_n = [EY_1 - P_c EY_c(1)]/(1 - P_c)$, we may reframe the problem as $$P_c EY_c(0) + EY_1 - P_c EY_c(1) = EY_0, \qquad (3)$$ such that $0 \le EY_c(0) \le 1$, $0 \le EY_c(1) \le 1$, and $0 \le EY_1 - P_c EY_c(1) \le 1$. Then substituting the implied value of $EY_c(1)$ from Eq. (3) into the system of inequalities and rearranging terms, we obtain $$0 \le EY_c(1) \le 1,$$ $$(EY_1 - EY_0)/P_c \le EY_c(1) \le 1 + (EY_1 - EY_0)/P_c,$$ $$(EY_1 + P_c - 1)/P_c \le EY_c(1) \le EY_1/P_c,$$ which yields the interval for $EY_c(1)$ asserted by the proposition. The interval for $EY_c(0)$ follows via substitution from the equality in Eq. (3). $\square$ [The hypotheses printed are the setting of Section 2. No condition $P_c < 1$ is printed. The sentence after Eq. (3) is transcribed as printed, with the upper limit 1 and ‘the implied value of $EY_c(1)$’; its corrected form is P028-T4.]

{Ω : Type*} [MeasurableSpace Ω] : SAP.P028.T8Statement Ω

Theorem: SAP.P028.T8

Statement hash: 46783ebd8551cb43e12541c5e54de3baec83c20be46f3e9729b464fe4b11bf1a

Statement definition: SAP.P028.T8Statement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:46:52Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Manifest annotation reconciliation: Effective use follows the source-bound dependency observation; original annotations are retained in the crosswalk.

AronowAudit.P028.attaining_arm_probability: observed used

AronowAudit.P028.attaining_integral: observed used

AronowAudit.P028.attaining_model_bounded: observed used

AronowAudit.P028.attaining_model_moments: observed used

AronowAudit.P028.compatible_mixture_moments: observed used

AronowAudit.P028.realize_mixture_moments: observed used

AronowAudit.P028.sharpness_moment_certificate: observed used

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T9

Corollary 1, with its printed proof

p. 678 (PDF p. 2), Section 3 (statement); p. 679 (PDF p. 3) (proof)

Corollary 1, Section 3, p. 678 (PDF p. 2), and its proof, p. 679 (PDF p. 3), under the Section 2 assumptions. The four ordinary finite treatment-assignment cell means and probabilities determine both complier average potential outcomes. They reconstruct the arm means and positive complier probability, the pure-stratum means and masses, the printed noncomplier ratio, both mixture equations, and both displayed complier formulas. Any two models with the same eight cell summaries have the same complier means. The usual measure-theoretic conditions are assumed; only observed cell moments are required, with no moment condition on unused counterfactual outcomes. Positive conditioning events express existence of the ordinary means in the premise.

Historical component credits

Proved AronowAudit.P028.corollary1 Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; {'source': 'adjudication', 'decision': 'rejected', 'what': "P028/P028_Results.lean:1154 exports both printed complier formulas, the pure-cell stratum identities, and the proof's noncomplier-mean ratio. The claim assumes E[Y|D=d,Z=z] is known for all four cells, and its definitions specify ordinary cell means only for positive-probability cells, so hcell at line 1155 makes an existing premise explicit. One-sided noncompliance and full compliance fail that premise rather than being newly excluded by Lean. Explicit formulas in observed moments faithfully represent the claim's point identification, without needing a separate epistemic predicate."}
Proved AronowAudit.P028.potential_cell_measurable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.potential_cell_integrable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.joint_outcome_population Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.observed_d_measurable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.cell_measurable Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.joint_moment_cell_integral Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.cell_probability_as_mean Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.cell_probability_population Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.pure_cell_probabilities Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.weighted_cell_mean Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The positive-cell premise is exactly the target’s existence condition for its ordinary conditional mean; totalized division at zero is not used to establish the identity.
Proved AronowAudit.P028.cell_probability_partition Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.positive_cell_mass Historical support retained; baseline fidelity: ok; manifest: not used; not used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.two_sided_cells_positive Historical support retained; baseline fidelity: ok; manifest: not used; not used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.
Proved AronowAudit.P028.corollary_moment_identity Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; Auxiliary regularity, probability, or pure-cell component is incorporated by corollary1 and the selected moment identities.

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:7b1361b58493156361e306b5a7fc19cc3a912ab459035cd62c7c0b903bc4c647

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): [Setting, Section 2, p. 678 (PDF p. 2)] The corollary is stated under the setting of Section 2: assumptions (i)–(iv) and the definitions of $P_c$, $EY_1$, $EY_0$ (transcribed in full in the standing assumptions). [Sentence introducing it, p. 678] “For contrast, we state sufficient conditions for point identification in Corollary 1, following the well-known result in, e.g., Imbens and Rubin (1997).” [p. 678] Corollary 1. If $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$, for $d, z \in \{0, 1\}$, are known, the complier average potential outcomes are point identified. $\mathrm{E}[Y(0)|D(1) > D(0)]$ is equal to $$\frac{EY_0 - \Pr[D = 1|Z = 0]\,\mathrm{E}[Y|D = 1, Z = 0] - \Pr[D = 0|Z = 1]\,\mathrm{E}[Y|D = 0, Z = 1]}{P_c}$$ and $\mathrm{E}[Y(1)|D(1) > D(0)] = \mathrm{E}[Y(0)|D(1) > D(0)] + (EY_1 - EY_0)/P_c$. [Proof as printed, p. 679 (PDF p. 3)] Proof. The average outcome for non-compliers, $\mathrm{E}[Y|D(1) = D(0)]$, is equal to $$\frac{\Pr[D = 1|Z = 0]\,\mathrm{E}[Y|D = 1, Z = 0] + \Pr[D = 0|Z = 1]\,\mathrm{E}[Y|D = 0, Z = 1]}{\Pr[D = 1|Z = 0] + \Pr[D = 0|Z = 1]}.$$ Substitution of $\mathrm{E}[Y|D(1) = D(0)]$ into Eqs. (1) and (2) yields the result. $\square$ [The hypotheses printed are the setting of Section 2 and the premise that $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ are known for $d, z \in \{0, 1\}$. Eqs. (1) and (2) are those of the proof of Proposition 1, transcribed in P028-T8.]

: SAP.P028.T9WholeStatement

Theorem: SAP.P028.T9

Statement hash: f890b7f9fca8b38fadd045dd0f60e8ba5d237fee2a0cf77a111b448dd34b78e5

Statement definition: SAP.P028.T9WholeStatement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:46:52Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Manifest annotation reconciliation: Effective use follows the source-bound dependency observation; original annotations are retained in the crosswalk.

AronowAudit.P028.cell_measurable: observed used

AronowAudit.P028.cell_probability_as_mean: observed used

AronowAudit.P028.cell_probability_partition: observed used

AronowAudit.P028.cell_probability_population: observed used

AronowAudit.P028.corollary_moment_identity: observed used

AronowAudit.P028.joint_moment_cell_integral: observed used

AronowAudit.P028.joint_outcome_population: observed used

AronowAudit.P028.observed_d_measurable: observed used

AronowAudit.P028.potential_cell_integrable: observed used

AronowAudit.P028.potential_cell_measurable: observed used

AronowAudit.P028.pure_cell_probabilities: observed used

Source and evidence metadata · sap-2026-11-08-assured-release

P028-T10

The ‘LATE theorem’ display of Section 2 (unnumbered), with the Introduction's statement that the three reported figures do not identify the average potential outcomes for compliers

p. 678 (PDF p. 2), Section 2, second paragraph; p. 677 (PDF p. 1), Section 1, first paragraph

Section 2 LATE display, p. 678, and Section 1, p. 677. The population and observed treatment first stages equal the positive complier probability. With the usual measure-theoretic conditions (in particular finite observed arm means), the complier moments exist, the reduced form and both LATE ratios hold, and measurable sample analogues give the Wald IV statistic. Two bounded randomized models share the three reported figures and CACE but have different complier levels. No moments on unused potential outcomes are assumed.

Historical component credits

Proved AronowAudit.P028.late_identity Limited support; baseline fidelity: narrower; manifest: used; used in Solution; {'source': 'adjudication+second review', 'adjudicator': "P028/P028_Results.lean:1221 exports the observed first stage, reduced form, and both LATE ratios, but only for models carrying global potential-outcome integrability at line 232. T10 attaches assumptions (i)–(iv) to the display and expressly places boundedness afterward; finiteness of its arm means and CACE does not imply integrability of counterfactual outcomes never realized by a stratum. For example, equal masses of always-takers with potentials (K,0) and compliers with potentials (0,1), independently assigned by a fair coin, have p=1/2, arm means (0,1/2), and CACE=1 when Pr(K=k)=1/[k(k+1)]. Every displayed identity is well-defined in this model, yet E|Y(0)| is infinite, so the Lean theorem excludes it. The row's disclosure of integrable potential outcomes describes its restriction but cannot add that hypothesis to the target claim.", 'suggested_fix': 'Parameterize the theorem and its quantities by a causal model without integrableY, and require only integrability of the two fixed-assignment realized outcomes ω ↦ potentialArmOutcome z (M.S ω, M.Y false ω, M.Y true ω), z=false,true. These are the finite arm-outcome moments needed here and allow arbitrary unused Y(0) on always-takers and Y(1) on never-takers.', 'second_review': "P028/P028_Results.lean:1221 exports the first stage, reduced form, and both LATE ratios, but its CausalModel parameter includes global integrability of both potentials at P028/P028_Results.lean:232. T10's claim text puts the LATE display under (i)–(iv), before boundedness, and finite displayed means do not constrain never-realized counterfactual outcomes. For independent fair assignment to half always-takers with potentials (K,0) and half compliers with (0,1), where Pr(K=k)=1/[k(k+1)] for k≥1, the arm means are (0,1/2), P_c=1/2 and CACE=1, while Y(0) is not integrable. Generalize to a base model with integrability of the two fixed-assignment realized outcome functions defined at P028/P028_Results.lean:371; disclosing the stronger premise in row_says does not repair the statement's major restriction.", 'severity': 'major'}
Proved AronowAudit.P028.first_stage_population Limited support; baseline fidelity: narrower; manifest: used; used in Solution; The narrower component is already incorporated by late_identity on precisely the same globally integrable model domain.
Proved AronowAudit.P028.random_assignment_moment Limited support; baseline fidelity: narrower; manifest: used; used in Solution; The narrower component is already incorporated by late_identity on precisely the same globally integrable model domain.
Proved AronowAudit.P028.cace_difference Limited support; baseline fidelity: narrower; manifest: used; used in Solution; The narrower component is already incorporated by late_identity on precisely the same globally integrable model domain.
Proved AronowAudit.P028.late_population_ratio Limited support; baseline fidelity: narrower; manifest: used; used in Solution; The narrower component is already incorporated by late_identity on precisely the same globally integrable model domain.
Proved AronowAudit.P028.observed_first_stage Limited support; baseline fidelity: narrower; manifest: used; used in Solution; The narrower component is already incorporated by late_identity on precisely the same globally integrable model domain.
Proved AronowAudit.P028.three_figures_do_not_identify_levels Historical support retained; baseline fidelity: ok; manifest: used; used in Solution; The existential pair establishes failure of identification from the three specified figures; neither equality of the full observed law nor ambiguity at every triple is required. This is a positive nonidentification result, not a purported refutation of the LATE display.

Formal result: whole

Formal statement · Proof · Definitions

Assumptions and verification

Claim revision: catalog:36ce68d11ebe295ebc74c64e3d02c8677e2d18b93ed4a191f56595dad0a4e45c

Standing assumptions: The work is a three-page letter (Statistics and Probability Letters 83 (2013) 677–679) with one proposition and one corollary, each with a short printed proof, and one application. Everything below was read from the rendered page images (the staged pages, and the staged PDF re-rendered at 260 dpi when this list was fixed). [Setting: Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [LATE display and bounded outcomes: Section 2, second paragraph, p. 678 (PDF p. 2)] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities. The associated estimator is logically equivalent to the Wald instrumental variables estimator (Angrist et al., 1996). We make one additional assumption to ensure partial identification: we require that outcomes are bounded. Without loss of generality, fix $Y \in [0, 1]$.” [Typography] The page prints the expectation operator upright in most places ($\mathrm{E}[Y|Z = 1]$) and in italics in assumption (iii) ($E[D_i(1) - D_i(0)]$); it is one operator. $EY_1$, $EY_0$, $EY_n$, $EY_c(0)$, $EY_c(1)$ and $P_c$ are names of real numbers, not products. [What the paper does not print] The paper does not define the observed treatment $D$ and the observed outcome $Y$ that appear in $\mathrm{E}[Y|Z = z]$, $\mathrm{E}[D|Z = z]$, $\mathrm{E}[Y|D = d, Z = z]$ and $\Pr[D = d|Z = z]$ (the relations $D = D(Z)$ and $Y = Y(D(Z))$ are not displayed). It does not say that both assignment arms have positive probability. It does not assume $P_c < 1$: (iii) and (iv) give $0 < P_c \le 1$ only, and ‘two-sided noncompliance’ is stated in Section 4 for the application alone. It does not say whether ‘$Y \in [0, 1]$’ bounds the observed outcome or both potential outcomes. It does not define ‘known’, ‘sharp’, ‘identified’ or ‘point identified’. It has no response or missing-data indicator and no assumption about outcomes that are not recorded. [Remarks for the formalizer, not printed in the paper] The reading the audit's validators settled on is: one probability space (a generic unit) carrying $Z \in \{0,1\}$ with $0 < \Pr[Z = 1] < 1$, potential treatments $D(0), D(1) \in \{0,1\}$ and potential outcomes $Y(0), Y(1) \in [0,1]$ (exclusion is built in: $Y(d,z) = Y(d)$), with $(Y(0), Y(1), D(0), D(1))$ independent of $Z$, $D(1) \ge D(0)$, $\mathrm{E}[D(1) - D(0)] \ne 0$, and observed $D = D(Z)$, $Y = Y(D(Z))$. The unit index is suppressed as generic-unit population notation; the validator of finding P028-N002 (rated a clarity note) established that the printed reason for dropping it (‘given (i), labels are exchangeable’) does not follow from (i) and is not needed, and that no identical-distribution or random-sampling assumption has to be added. Principal strata: compliers $C = \{D(1) > D(0)\} = \{D(0) = 0, D(1) = 1\}$, always-takers $A = \{D(0) = D(1) = 1\}$, never-takers $N = \{D(0) = D(1) = 0\}$; monotonicity excludes $\{D(0) = 1, D(1) = 0\}$, so $D(1) - D(0) = \mathbf{1}_C$, $P_c = \Pr(C) = \mathrm{E}[D(1) - D(0)] = \mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]$ and $0 < P_c \le 1$; $\Pr(A) = \Pr[D = 1|Z = 0]$, $\Pr(N) = \Pr[D = 0|Z = 1]$ and $\Pr(A) + \Pr(N) = 1 - P_c$. A conditional mean given an event is the elementary one and is defined only when the event has positive probability. Lean's division is total ($x/0 = 0$), so a statement that a printed quotient or conditional mean is undefined has to be stated as the failure of a side condition (a zero denominator, a null conditioning event), not as a property of the quotient's value. Boundedness is used only in Proposition 1; the LATE display and Corollary 1 need integrable outcomes only. [Why the list has ten targets] Three findings rated as errors concern a mathematical statement or rest on an exact formal counterexample. P028-N005 (Moderate): the application presents point estimates of the complier means although 71 of 1000 outcomes are missing and no response assumption is stated; the validator confirmed this with two exact laws that agree on everything observed and disagree on the complier means, so the counterexample (T1), the formal content of the corrected claim (T2) and the passage as printed (T3) are targets. P028-E001 (Minor): a misprinted upper limit and a wrong symbol in the proof of Proposition 1; corrected statement (T4) and the validator's counterexample to the printed intermediate system (T5). P028-E002 (Minor): the proof of Proposition 1 does not cover $P_c = 1$; corrected statement (T6) and the validator's counterexample to the unqualified proof step (T7). The fourth error, P028-E003 (Minor), is a volume number in the reference list and has no mathematical statement to correct. P028-N002 and P028-N007 are clarity notes; P028-N003, P028-N004 and P028-N006 were not confirmed; P028-N001 is undetermined. Of the seven headline claims, H1 (Proposition 1, T8), H3 (Corollary 1, T9) and H2 (the LATE identity and the statement that the three figures do not identify the complier means, T10) are mathematical statements. H4 (the count of 6 of 20 studies), H5 and H6 (the application's estimates) and H7 (the reporting recommendation) are an empirical count, empirical estimates and a recommendation, and are not targets; the formal content behind H6 is reached through P028-N005.

Effective claim (source TeX): [Setting, Section 2, first paragraph, p. 678 (PDF p. 2)] “We follow the setup of Angrist and Pischke (2009, Chapter 4). Let $Y_i(d, z)$ be the potential outcome of unit $i$ under treatment $d \in \{0, 1\}$ and assignment $z \in \{0, 1\}$, let $D_i(z)$ be the potential treatment of unit $i$ under assignment $z$, and let $Z_i$ be the treatment assigned to unit $i$. The causal effect for unit $i$ is then $Y_i(1, Z_i) - Y_i(0, Z_i)$. We assume (i) random assignment: $[Y_i(d, z), D_i(z) : d, z \in \{0, 1\}] \perp\!\!\!\perp Z_i$; (ii) exclusion restriction: $Y_i(d, z)$ does not depend on $z$, so we may write $Y_i(d, z) = Y_i(d)$; (iii) non-zero first-stage effect: $E[D_i(1) - D_i(0)] \ne 0$; (iv) monotonicity: $\forall i$, $D_i(1) \ge D_i(0)$. We make two notational simplifications. First, given (i), labels are exchangeable and so we drop notational dependence on $i$. Second, we define $P_c \equiv \Pr[D(1) > D(0)]$, $EY_1 \equiv \mathrm{E}[Y|Z = 1]$, and $EY_0 \equiv \mathrm{E}[Y|Z = 0]$.” [Section 2, second paragraph, p. 678] “This setting implies that the ``LATE theorem'' (Angrist and Pischke, 2009, Theorem 4.4.1) holds: the CACE, $\mathrm{E}[Y(1) - Y(0)|D(1) > D(0)]$, is equal to $$\frac{\mathrm{E}[Y|Z = 1] - \mathrm{E}[Y|Z = 0]}{\mathrm{E}[D|Z = 1] - \mathrm{E}[D|Z = 0]} = \frac{EY_1 - EY_0}{P_c},$$ where each component may be estimated using sample analogues to population quantities.” [Section 1, first paragraph, p. 677 (PDF p. 1)] “When reporting results from experiments with noncompliance, including encouragement designs, researchers often include estimates of the average outcomes in treatment, average outcomes in control and the difference in average take-up between assignment statuses. These figures are sufficient for estimating a complier average causal effect (CACE), sometimes referred to as a local average treatment effect (Angrist et al., 1996). Although sufficient information is typically estimable from the data (Imbens and Rubin, 1997), these three figures alone do not provide enough information to identify the average potential outcomes for compliers.” [The hypotheses printed for the display are the setting of Section 2, assumptions (i)–(iv). The bounded-outcome assumption is introduced after the display and is not attached to it.]

: SAP.P028.T10WholeStatement

Theorem: SAP.P028.T10

Statement hash: eeecc71103e1e65fa876c967d12f8566cf5c86f5f2b15728b046f3258c018ab0

Statement definition: SAP.P028.T10WholeStatement

Certificate. 20261104T182914Z

Declaration review: faithful; 2026-11-04T18:46:52Z; binding v2

Evidence scope: Certification checks formal proof objects. Statement fidelity is a model judgment. Author review is separate.

Proof dependencies: Independently extracted

Manifest annotation reconciliation: Effective use follows the source-bound dependency observation; original annotations are retained in the crosswalk.

AronowAudit.P028.cace_difference: observed used

AronowAudit.P028.first_stage_population: observed used

AronowAudit.P028.late_population_ratio: observed used

AronowAudit.P028.observed_first_stage: observed used

AronowAudit.P028.random_assignment_moment: observed used

Source and evidence metadata · sap-2026-11-08-assured-release

Target	Where	Method	Status	Agreement
Introduction: reporting survey	p. 677 (PDF p. 1), Introduction, second paragraph and footnote 1	I could not compare the reported count of 6 of 20 studies because the study list and coding sheet were unavailable.	Blocked	Not compared
Application: marginal summaries and CACE	p. 679 (PDF p. 3), section 4, first paragraph	I translated the source-study outcome construction from Stata. The data reproduce the outcome means to rounding, but give a first stage of about 0.20 and a CACE of 28 points; the reported 0.21 and 29 points agree with the source chapter (P028-N007).	Recalculated	Agrees in part
Application: sharp bounds	p. 679 (PDF p. 3), section 4, first paragraph; formula in Proposition 1, p. 678 (PDF p. 2)	I applied Proposition 1 to the reported 0.45, 0.51 and 0.21, obtaining [0, 0.7143] and [0.2857, 1].	Recalculated	To rounding
Application: joint-distribution summaries	p. 679 (PDF p. 3), section 4, second paragraph	I translated the source-study outcome construction from Stata and recalculated the four summaries. All four agree to rounding when the three unsure or refused control viewing responses are excluded (P028-N007).	Recalculated	To rounding
Application: point-identified potential outcomes	p. 679 (PDF p. 3), section 4, second paragraph; Corollary 1, p. 678 (PDF p. 2)	I applied Corollary 1 to the reported outcome means 0.45 and 0.51 and the unrounded take-up rates, cell means and first stage from the data, obtaining 0.4294 and 0.7239. This reconstructs both printed values; the original calculation is unavailable (P028-N007).	Recalculated	To rounding

Summary

What was and was not checked

Headline claims and related corrections

Sources that could not be obtained

Corrections

Minor (4)

As printed

The problem

Evidence a derivation

What survives

Corrected

As printed

The problem

Evidence an exact counterexample

What survives

Corrected

As printed

The problem

Evidence a check of the printed page

What survives

Corrected

As printed

The problem

Evidence an exact counterexample

What survives

Corrected

Clarity notes

As printed

Intended meaning

Corrected

As printed

Intended meaning

Corrected

Formal statements (Lean)

Reproduction