Assignment probabilities without row-level links: Identification, label design, and inference in randomized trials

CausalSmith

CausalSmith · AI Causal Scientist — CSWP-2026-023 · Partial ID · pinned commit 9135ac1 · PDF · Lean code · Slides · AI review · arXiv · GitHub

Assignment Probabilities Without Row-level Links: Identification, Label Design, and Inference in Randomized Trials

The verified identification and rate results are substantial, but the closest methodological comparisons and the definition of the proposed external-log interval need work before publication.

Main criticisms

Related work The closest design comparison, scalar quantization, receives only a general citation when the density assumption is introduced. Readers cannot tell which part of the inverse-budget rate and high-resolution companding calculation follows established quantization theory and which part comes from the paper's paired ATE distortion.
Inference with an independent score log The definition of the central projection procedure says, “For each b∈B_{n,m}, let I(b) be the interval given by its two quantile-transport average treatment effect endpoints.” Because sieve arrays need not arise from one score law, this sentence leaves the candidate interval and its zero-mass convention implicit.

6 findings — 2 major · 4 minor Read the entire review →

Referee report of 29 Sep 2026. This report was written for an earlier draft; the paper has been revised since, so some findings may already be addressed. One automated referee’s estimate — not peer review.

Submitted: 29 Sep 2026 (v1) · last revised 29 Sep 2026 (v5)
Cite as: CSWP-2026-023 · https://causalsmith.org/papers/pid_unlinked_propensity_ate_v1/

@techreport{causalsmith_pid_unlinked_propensity_ate_v1,
  title       = {Assignment probabilities without row-level links: {Identification}, label design, and inference in randomized trials},
  author      = {{CausalSmith}},
  year        = {2026},
  month       = sep,
  institution = {CausalSmith Working Papers},
  number      = {CSWP-2026-023},
  url         = {https://causalsmith.org/papers/pid_unlinked_propensity_ate_v1/},
  note        = {Version 5, 29 Sep 2026. Machine-generated; formal statements verified in Lean 4 at commit 9135ac1}
}

CausalSmith (2026). “Assignment probabilities without row-level links: Identification, label design, and inference in randomized trials.” CausalSmith Working Paper CSWP-2026-023, version 5 (29 Sep 2026). https://causalsmith.org/papers/pid_unlinked_propensity_ate_v1/

Cite by URL: https://causalsmith.org/papers/pid_unlinked_propensity_ate_v1/ Cites version 5 of 29 Sep 2026.

Abstract

We study a randomized trial in which treatment and outcome remain linked to a deterministic label of the assignment probability. The population score distribution is known in the identification and design experiments and sampled independently in the external-log experiment. Under bounded outcomes and fixed uniform overlap, we characterize the maximum width of the sharp average treatment effect interval across compatible released outcome laws for any measurable finite-label rule. Its exact cellwise expression is attained by a released law with Bernoulli one-half outcomes in every positive-mass arm-label cell, including for atomic score distributions and disconnected cells. Universal point identification holds precisely when the label determines the assignment probability almost surely. With a budget of $K$ labels, optimal worst-case ambiguity has order $K^{- 1}$ over score laws with a common positive density lower bound; an equal-width construction gives the upper bound for every score law. For continuous, strictly positive score densities, we derive the exact high-resolution constant and an asymptotically attaining interval-cell allocation. For trial size $n$ and a known score law, the minimax expected length of a uniformly honest interval has order $K^{- 1} + n^{- 1/2}$ over the lower-density class. With a fixed release and an independent score log of size $m$ , a projection interval attains excess-length order $n^{- 1/2} + m^{- 1/2}$ ; separate lower bounds establish both sampling directions at a fixed positive trial-to-log size ratio.

Introduction

Randomized assignment can use a probability that varies across people even when a released trial file records only treatment and outcome. We consider a release that attaches to each trial row a deterministic label of that assignment probability. In the identification, design, and known-score inference experiments, the analyst knows the population distribution of assignment probabilities. In the external-log experiment, that distribution is learned from an independent score sample. This observation scheme retains the link among label, treatment, and outcome, while the population score distribution supplies the probabilities represented within each label. The question is how much information the labels preserve about the average treatment effect (ATE), and how to choose them when their number is limited.

Under bounded potential outcomes and a fixed uniform overlap margin, the sharp ATE interval for a specified compatible released law follows from within-cell quantile rearrangement. We use the bounded-outcome specialization of Fan et al. (2014) for this fixed-law interval; Lemma 2 records the resulting endpoints. Our release-design criterion then takes the largest interval width across the released outcome laws compatible with a given score distribution and label rule. Theorem 2 expresses that width as a sum of paired absolute-deviation losses over label cells and constructs two causal laws attaining its endpoints under the same released law. The construction applies to arbitrary score distributions on the overlap interval and measurable cells, including atoms and disconnected sets. Theorem 3 gives the corresponding disclosure criterion: worst-case ambiguity is zero exactly when the label determines the score almost surely.

This criterion turns finite-label release into a design problem measured in ATE units. For a budget of $K$ labels, Theorem 4 bounds the smallest worst-case ambiguity above and below at order $K^{- 1}$ when the score density has a common positive lower bound. Its equal-width upper construction applies to every score distribution on the overlap interval. When the density is continuous and strictly positive, Theorem 5 gives the exact leading constant. Writing $ε$ for the overlap margin, $e$ for a score value, and $f$ for the score density, an asymptotically attaining sequence places interval boundaries at equal increments of $\int_{ε}^{e} f (t) / [t (1 - t)] d t$ . Thus label allocation responds to both score mass and the sensitivity of inverse assignment weights.

The design criterion also governs inference from independent released trial rows. With a known score law and a jointly chosen release and uniformly honest interval, Theorem 6 establishes minimax expected length of order $K^{- 1} + n^{- 1/2}$ over the common positive lower-density class, where $n$ is trial size. An equal-width release and midpoint inverse-probability weights attain the upper order. A label budget proportional to $n$ balances ambiguity from score variation within cells with trial sampling variation. This connects the partial-identification criterion to confidence-set analysis (Imbens et al., 2004; Stoye, 2009; Chernozhukov et al., 2007; Kaido et al., 2019).

We also study a fixed finite-label release when the score distribution is learned from an independent log of $m$ scores. The criterion here is worst-case expected positive excess length beyond the population sharp interval. For every measurable fixed release and score law on the overlap interval, Theorem 7 constructs a uniformly honest projection interval with excess length bounded at order $n^{- 1/2} + m^{- 1/2}$ . A trial-sample lower bound holds at every positive pair of sample sizes, and a positive score-log lower bound holds asymptotically uniformly over trial sizes. Together they establish that order when the trial-to-log size ratio tends to a positive constant. The result includes atomic score laws and quantile functions with flat pieces.

The setting connects partial identification under combined marginals (Manski, 1990; Tamer, 2010; Torgovitsky, 2019) with statistical matching (D’Orazio et al., 2006; Conti et al., 2017) and propensity-score subclassification (Cochran, 1968; Rosenbaum et al., 1984). The released label specifies a deterministic score cell, making within-cell association and the choice of cells central to the analysis. We document the scope of the Lean 4 verification in the appendix. We place the observation scheme among related work in the next section. The paper then develops the trial setup and sharp interval, characterizes information retained by labels, studies finite-label design and honest intervals, analyzes the independent score-log experiment, and closes with discussion and open questions.

Partial-identification analysis characterizes the target values compatible with an observed law (Manski, 1990; Horowitz et al., 1995; Tamer, 2010). For a known distribution of assignment probabilities and a fixed released trial law, the sharp average treatment effect interval developed below is the bounded-outcome, overlap specialization of Fan et al. (2014). Within each released label, its endpoints account for the possible association between outcomes and assignment probabilities.

Data-combination and conditional-transport analyses also characterize outcomes consistent with observed marginal or conditional distributions. In particular, Fan et al. (2025) obtain convex identified sets and transport-computable support functions for affine moment models with incomplete data. Here the fixed-law interval is one part of a release-design problem: the analysis ranges over compatible released trial laws to measure the largest attainable interval width, then chooses a finite-label rule to minimize that width. The score-based randomization model and this outer optimization are specific to the present problem.

Statistical matching and record-linkage studies analyze information recovered by linking separate files. Komarova et al. (2018) show that a positive bound on individual disclosure risk generally leaves their model parameter only partially pseudo-identified. Their object is a probabilistic matching rule based on personal identifiers and a disclosure constraint. Our released object is instead a deterministic function of the assignment score attached to every trial row; its information loss is measured by sharp ATE ambiguity, and point identification occurs exactly when the label determines the score almost surely.

Coarsening also appears in treatment-effect estimation with linked covariates. Under unconfoundedness, outcome smoothness, and restrictions on extreme scores, Kalavasis et al. (2024) construct a data-dependent coarse IPW estimator whose error accounts for propensity-score inaccuracy and sampling. Lee et al. (2026) obtain treatment-effect bounds and inference by pooling outcomes across small groups of observations with linked covariates, including settings with limited overlap. For identification and known-score design, our experiment retains a deterministic label in place of the row-level score and assumes a known score marginal; the independent-score-log extension learns that marginal from a separate sample. Under a positive density floor, the resulting optimal ambiguity is of order $K^{- 1}$ , and honest length in the known-score experiment is of order $K^{- 1} + n^{- 1/2}$ . These rates quantify label design under a different observation scheme and different regularity conditions.

The inference questions fit the literature on confidence sets for partially identified parameters (Imbens et al., 2004; Stoye, 2009; Chernozhukov et al., 2007; Kaido et al., 2019). With a known score distribution, the criterion is worst-case expected length for a jointly chosen label rule and uniformly honest interval. With an independent score log, the rule is fixed and the criterion is worst-case expected positive excess length beyond the population sharp interval from estimation with both released trial rows and the independent score log. These two criteria measure, respectively, the length of an honest interval under label coarsening and the additional length generated by the two sampled data sources.

Trial setup and the sharp identified interval

Throughout, generic positive constants may change from line to line, absolute values and Euclidean norms have their usual meanings, and $O (\cdot)$ and $o (\cdot)$ denote asymptotic bounds. Arm and label indices range over the sets defined below.

We consider a randomized causal population governed by a law $P$ . For an overlap margin $ε$ , the score $E$ takes values in the interval $E$ given by $[ε, 1 - ε]$ . The control and treatment potential outcomes $Y_{0}$ and $Y_{1}$ take values in the bounded outcome space $Y = [0, 1]$ . The assigned arm is $A$ , and the observed outcome is $Y$ . The population score law is $H$ ; a measurable release rule $g$ applied to the score determines the released label $R$ ; the joint law of the released trial variables is $P_{rel}$ . Our target is the average treatment effect $θ (P)$ for the population law $P$ , defined by $θ (P) = E_{P} [Y_{1} - Y_{0}]$ . For identification, release design, and known-score inference, $H$ is known to the analyst; in the external-log experiment it is learned from an independent sample of scores.

The population model combines overlap, a specified population score marginal, and score-based randomized assignment. The overlap margin is fixed throughout the analysis.

Assumption 1 [ass:overlap] (Overlap parameter).

The overlap parameter $ε$ satisfies $0 < ε < 1/2$ .

⊢ Lean

The uniform propensity-score overlap condition keeps both assignment probabilities positive throughout the score space (Fan et al., 2014). It also bounds the reciprocal assignment weights used in the endpoint formulas below.

Assumption 2 [ass:score-marginal] (Score marginal law).

The score $E$ has law $H$ under $P$ : $L_{P} (E) = H .$

⊢ Lean

This specifies the population covariate or propensity marginal used in the data-combination experiment (Fan et al., 2014). It supplies the score distribution within each released label, even though individual scores are not linked to outcomes in the released data.

Assumption 3 [ass:randomized-assignment] (Score-based treatment assignment).

$P (A = 1 ∣ E, Y_{0}, Y_{1}) = E almost surely .$

⊢ Lean

Conditional on the score, assignment is Bernoulli and unconfounded with respect to both potential outcomes (Fan et al., 2014). Thus the score determines how the population score law is weighted in each treatment arm.

The observed outcome and the release are connected to the potential outcomes and score by two further conditions.

Assumption 4 [ass:consistency] (Observed outcome consistency).

$Y = A Y_{1} + (1 - A) Y_{0} almost surely .$

⊢ Lean

Potential-outcome consistency identifies the observed outcome with the potential outcome under the assigned arm (Rubin, 1974). It connects each observed arm-label outcome distribution to the corresponding potential outcome.

Assumption 5 [ass:deterministic-release] (Deterministic score release).

$R = g (E) almost surely .$

⊢ Lean

The deterministic release condition is specific to this analysis: each score is assigned a label by the declared rule. The released label therefore identifies a score cell while retaining uncertainty about the pairing of scores and outcomes within that cell.

Assumption 6 [ass:released-law] (Released data law).

$L_{P} (R, A, Y) = P_{rel} .$

⊢ Lean

Observed-law compatibility requires a candidate causal law to reproduce the distribution available to the analyst, a standard restriction in data-combination identification (Fan et al., 2014). Here that distribution includes the label alongside assignment and outcome.

These conditions define the population laws under a release rule and, for a specified released distribution, the compatible laws.

Definition 1 [def:causal-law-class] (Causal-law class

P (H, g)

The causal-law class $P (H, g)$ consists of all laws $P$ satisfying Assumptions 2, 3, 4, and 5.

⊢ Lean

The class $P (H, g)$ in Definition 1 fixes the score law and release rule while allowing the joint distribution of scores and potential outcomes to vary subject to the stated population conditions.

Definition 2 [def:compatible-law-class] (Compatible-law class

M (H, g, P_{rel})

The compatible-law class is $M (H, g, P_{rel}) = {P \in P (H, g) : L_{P} (R, A, Y) = P_{rel}} .$ Here $P (H, g)$ imposes Assumptions 2, 3, 4, and 5, and the released-law condition is Assumption 6.

⊢ Lean

For a fixed released law, $M (H, g, P_{rel})$ in Definition 2 is the population class over which the identified set is formed.

We next fix the index sets used to describe released cells. Let $J$ denote a positive label count; a later release-design problem uses a positive label budget $K$ .

Definition 3 [synth_3] (Released-label alphabets).

For each positive integer $J$ , the released-label alphabet is $R_{J} = {1, \dots, J}$ . In particular, $R_{K} = {1, \dots, K}$ for a positive label budget $K$ ; a release into $R_{K}$ may use fewer than $K$ labels.

The alphabet $R_{J}$ in Definition 3 includes labels that may have zero probability under a particular release.

Definition 4 [synth_2] (Treatment-arm set).

The treatment-arm set is $A = {0, 1}$ , where $0$ denotes control and $1$ denotes treatment.

The arm index $a$ ranges over $A$ as defined in Definition 4. For each arm-label cell, the observed outcome law and the score law induced by assignment enter the endpoint calculation together. The endpoint formulas use the generalized quantile $Q_{F} (u) = in f {x : F ((- \infty, x]) \geq u}$ for $0 < u < 1$ , with support endpoints at $u = 0, 1$ . This convention also applies when $F$ has atoms; its formal definition appears in Definition 8.

Definition 5 [def:arm-cell-primitives] (Arm-cell quantities

p_{a}, C_{r}, q_{a r}, F_{a r}, G_{a r}, E_{a r}, W_{a r}

For each arm $a \in A$ and label $r \in R_{J}$ , define $p_{1} (e) = e, p_{0} (e) = 1 - e, C_{r} = {e : g (e) = r}, q_{a r} = \int_{C_{r}} p_{a} (e) H (d e) .$ When $P_{rel} (A = a, R = r) > 0$ , define the observed outcome law $F_{a r} = L_{P_{rel}} (Y ∣ A = a, R = r) .$ For $q_{a r} > 0$ , define $G_{a r} (d e) = \frac{1 { e \in C _{r} } p _{a} ( e ) H ( d e )}{q _{a r}}, E_{a r} \sim G_{a r}, W_{a r} = \frac{1}{p _{a} ( E _{a r} )} .$ The endpoint formulas apply to triples $(H, g, P_{rel})$ satisfying $P_{rel} (A = a, R = r) = q_{a r}$ for every arm and label. Their sums include cells with $q_{a r} > 0$ , for which $F_{a r}$ is defined.

⊢ Lean

For each arm-label cell, the observed outcome law and the score law induced by assignment enter the endpoint calculation together.

Definition 6 [def:mean-endpoints] (Mean endpoints

\underline{μ}_{a}, \overline{μ}_{a}

For a triple $(H, g, P_{rel})$ satisfying $P_{rel} (A = a, R = r) = q_{a r}$ for every arm and label, define $\underline{μ}_{a} = r : q_{a r} > 0 \sum q_{a r} \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (1 - u) d u, \overline{μ}_{a} = r : q_{a r} > 0 \sum q_{a r} \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (u) d u .$

⊢ Lean

In Definition 5, $p_{a} (e)$ is the arm-specific assignment probability, $C_{r}$ is the score cell assigned label $r$ , and $q_{a r}$ is its arm-label probability. The observed outcome law $F_{a r}$ and the assignment-weighted score law $G_{a r}$ are the two marginals available for a positive-mass cell. The reciprocal weight $W_{a r}$ converts an arm-specific outcome distribution into a potential-outcome mean; its association with outcomes within the cell determines the endpoint range.

Definition 7 [def:sharp-ate-set] (Sharp ATE interval

I (P_{rel}; H, g)

$I (P_{rel}; H, g) = [\underline{μ}_{1} - \overline{μ}_{0}, \overline{μ}_{1} - \underline{μ}_{0}] .$

⊢ Lean

The generalized quantile $Q_{F}$ in Definition 8 makes the same endpoint expressions apply to discrete and continuous cell distributions. Pairing outcome and reciprocal-weight quantiles in opposite or matching order gives the lower and upper mean endpoints.

Definition 8 [synth_4] (Generalized quantile).

For a probability law $F$ with compact support in $R$ , define $Q_{F} (u) = in f {x \in R : F ((- \infty, x]) \geq u}, 0 < u < 1.$ Set $Q_{F} (0) = in f supp (F)$ and $Q_{F} (1) = sup supp (F)$ . At an atom $x$ , this convention gives $Q_{F} (u) = x$ whenever $F ((- \infty, x)) < u \leq F ((- \infty, x])$ .

The interval $I (P_{rel}; H, g)$ in Definition 7 combines the attainable arm-specific mean endpoints into the fixed-law sharp identified interval for the average treatment effect. The mathematical antecedent is Fan et al. (2014); the displayed result here is proved under the paper’s stated model conditions.

Before reporting that interval for a proposed release, one can check whether the declared score law and released law admit a common causal population. The observable criterion uses the label masses and the treated masses within labels.

Theorem 1 [prop:compatibility] (Compatibility of released laws).

Suppose Assumption 1 holds. Let $H$ be a probability law on the score interval $E = [ε, 1 - ε]$ , let $g : E \to R_{J}$ be a measurable release rule, and let $P_{rel}$ be a probability law on $(R, A, Y)$ . The compatible causal-law class $M (H, g, P_{rel})$ of Definition 2 is nonempty if and only if, for every $r \in R_{J}$ , $P_{rel} (R = r) P_{rel} (A = 1, R = r) = H (C_{r}), = \int_{C_{r}} e H (d e) .$

⊢ Lean

Under Assumptions 3 and 5, the score mass of a cell gives its label probability, and score-weighting that mass gives its treated probability. The control probability then follows from the label total. Theorem 1 establishes that these equalities also suffice for a compatible causal law, so an archive can check the coherence of its declared release and randomization law before using the fixed-law interval.

Information retained by a score label

For a fixed score law and deterministic release, the sharp interval in Definition 7 can vary with the released outcome law. The worst-case ambiguity $D_{H} (g)$ , the largest such interval width over the causal laws in Definition 1, measures the information retained by the label across outcome laws.

Three criteria answer different questions. The sharp width measures identification for a specified released law; worst-case ambiguity maximizes that width over released laws at a fixed score law and release. With trial sampling and a known score law, Theorem 6 studies expected honest interval length. With an independently sampled score law, Definition 19 studies expected length in excess of the population sharp interval. The latter two criteria include sampling uncertainty; the sharp width does not.

Definition 9 [def:worst-case-ambiguity] (Worst-case ambiguity

D_{H} (g)

$D_{H} (g) = P \in P (H, g) sup len {I (L_{P} (R, A, Y); H, g)} .$

⊢ Lean

The supremum has a cellwise expression in terms of the score law and release rule. The next result also gives a released outcome law at which the width is attained.

Theorem 2 [thm:all-label-ambiguity] (Exact all-label ambiguity width).

Suppose that:

(Overlap.) The overlap condition in Assumption 1 holds.

(Score law.) $H$ is a probability law on $E = [ε, 1 - ε]$ .

(Release.) $g : E \to R_{J}$ is measurable.

Write $C_{r} = {e : g (e) = r}$ , $p_{1} (e) = e$ , $p_{0} (e) = 1 - e$ , and $q_{a r} = \int_{C_{r}} p_{a} (e) H (d e)$ . Let $P_{rel}$ be the released law $P_{rel} = r \in R_{J} \sum a \in {0, 1} \sum \frac{q _{a r}}{2} (δ_{(r, a, 0)} + δ_{(r, a, 1)}) .$ Thus its observed outcome law $F_{a r}$ is Bernoulli $(1/2)$ in every positive-mass arm-label cell.

The worst-case ambiguity $D_{H} (g)$ of Definition 9 satisfies $D_{H} (g) = r \in R_{J} \sum [c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - ce ∣ H (d e) + c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - c (1 - e) ∣ H (d e)] .$

For each $a \in {0, 1}$ and each cell with $q_{a r} > 0$ , let $E_{a r}$ have law $p_{a} (e) 1_{C_{r}} (e) H (d e) / q_{a r}$ , and let $W_{a r} = 1/ p_{a} (E_{a r})$ . Define $\underline{μ}_{a} = r : q_{a r} > 0 \sum q_{a r} \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (1 - u) d u, \overline{μ}_{a} = r : q_{a r} > 0 \sum q_{a r} \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (u) d u .$ The sharp ATE interval for $P_{rel}$ has length $D_{H} (g)$ . Moreover, there are two probability laws $P_{-}, P_{+} \in M (H, g, P_{rel})$ , as defined in Definition 2, such that $E_{P_{-}} [Y_{1} - Y_{0}] = \underline{μ}_{1} - \overline{μ}_{0}, E_{P_{+}} [Y_{1} - Y_{0}] = \overline{μ}_{1} - \underline{μ}_{0}, E_{P_{+}} [Y_{1} - Y_{0}] - E_{P_{-}} [Y_{1} - Y_{0}] = D_{H} (g) .$

⊢ Lean

Assignment tilts the score distribution within a label differently in the two arms. Pairing the Bernoulli outcome with reciprocal assignment weights in opposite or matching quantile order produces the mean endpoints in Theorem 2. Its two compatible causal laws attain those endpoints under the same released outcome law, so the paired absolute-deviation expression gives the exact worst-case width. Because the expression depends on $H$ and $g$ , it permits comparison of candidate releases without specifying an outcome regression. The result applies to arbitrary probability laws $H$ , including atomic laws, and to measurable releases with disconnected score cells.

For a concrete one-label release, take $ε = 1/4$ , let $H$ put mass $1/2$ on each of the scores $1/4$ and $3/4$ , and set $g \equiv 1$ . Use the released law in Theorem 2, so outcomes are Bernoulli $(1/2)$ in each arm. In either arm the lower and upper attainable potential-outcome means are $1/3$ and $2/3$ : assignment tilts the two scores, but the outcome can be matched to the larger or smaller reciprocal weight. The sharp ATE interval is therefore $[- 1/3, 1/3]$ , with width $2/3$ . If each score instead receives its own label, the score is recovered from the label and the ambiguity width is zero. This example isolates uncertainty from within-label score variation before any trial sampling is introduced.

The zero-width case has a direct disclosure interpretation. The following characterization expresses it both as recovery of the score from the label and as concentration of the score within every positive-mass cell.

Theorem 3 [thm:universal-point-identification] (Universal point identification).

Let $J \in N$ , let $H$ be a probability law on the score interval $E = [ε, 1 - ε]$ , and let $g : E \to R_{J}$ be a measurable deterministic release into $J$ labels. Under Assumption 1, write $C_{r} = {e \in E : g (e) = r}$ for each label $r$ . Each of the following is equivalent to $D_{H} (g) = 0$ , where $D_{H} (g)$ is defined in Definition 9:

There exists a measurable map $h : R_{J} \to E$ such that $e = h (g (e))$ for $H$ -almost every $e$ .

For every $r \in R_{J}$ with $H (C_{r}) > 0$ , there exists $x \in E$ such that $e = x$ for $H$ -almost every $e \in C_{r}$ .

⊢ Lean

The absolute-deviation terms in Theorem 2 vanish when each positive-mass cell carries a single score value. Score variation within a cell produces positive worst-case ambiguity, while score-degenerate cells yield universal point identification. For a finite-support score law with at most $J$ positive-mass atoms, giving each atom a distinct label achieves point identification. With more atoms than labels, at least one positive-mass cell contains score variation, so universal point identification fails.

Designing a finite-label release

The cellwise criterion in Theorem 3 makes label design an allocation problem. A release with $K$ labels groups score values, and Definition 9 measures the resulting worst-case ATE ambiguity. A lower bound on score density supports a comparison across score laws.

Assumption 7 [ass:density-lower] (Lower bound on score density).

The score law $H$ has density $f$ on the score interval $E$ , with $H (d e) = f (e) d e, f (e) \geq m_{f}$ for Lebesgue-almost every $e \in E$ .

⊢ Lean

The density $f$ and its floor $m_{f}$ , when the floor is positive, give the standard compact-support positive-density condition used in quantization (Lemaire et al., 2020). A positive floor assigns every subinterval a baseline amount of score mass, which permits a uniform lower bound on ambiguity.

The release budget, its optimal ambiguity, and the common comparison class are defined as follows.

Definition 10 [def:k-label-releases] (

K

-label release class

G_{K}

$G_{K} = {g : E \to {1, \dots, K} : g is measurable} .$

⊢ Lean

The release family $G_{K}$ allows any measurable partition with at most $K$ nonempty label cells. Its design criterion takes the infimum of worst-case ambiguity over that family.

Definition 11 [def:optimal-k-ambiguity] (Optimal

K

-label ambiguity

Δ_{K} (H)

$Δ_{K} (H) = g \in G_{K} in f D_{H} (g) .$

⊢ Lean

The optimal ambiguity $Δ_{K} (H)$ expresses the best worst-case ATE resolution available at the given label budget. For a uniform comparison, the density floor defines a class of score laws on the common overlap interval.

Definition 12 [def:score-lower-density-class] (Lower-density score class

H_{ε, m_{f}}^{lb}

Under Assumption 7, the class of score laws is $H_{ε, m_{f}}^{lb} = {H \in P (E) : H (d e) = f (e) d e, f (e) \geq m_{f} for Lebesgue-almost every e \in E} .$

⊢ Lean

The class is nonempty only in the feasible range $0 < m_{f} \leq (1 - 2 ε)^{- 1}$ ; this is the range in which the uniform lower bound below has content. Within this class, the label budget yields matching inverse-budget bounds. The constructive upper bound applies to every score law on the overlap interval.

Theorem 4 [thm:k-label-rate] (Bounds for optimal label ambiguity).

Suppose:

(Overlap.) The condition in Assumption 1 holds for $ε$ .

(Density floor.) $m_{f} > 0$ .

(Label budget.) $K \geq 1$ is an integer.

Let $ℓ = 1 - 2 ε$ and $E = [ε, 1 - ε]$ . For every $H \in H_{ε, m_{f}}^{lb}$ as defined in Definition 12, $\frac{m _{f} ℓ ^{2}}{2 ( 1 - ε ) K} \leq Δ_{K} (H) .$ For every probability law $H$ on $E$ , the equal-width release $g : E \to R_{K} = {1, \dots, K}$ defined by $g (e) = 1 + min {⌊ \frac{K ( e - ε )}{ℓ} ⌋, K - 1}$ is measurable and satisfies $Δ_{K} (H) \leq \frac{ℓ}{2 ε ( 1 - ε ) K}, D_{H} (g) \leq \frac{ℓ}{2 ε ( 1 - ε ) K} .$

⊢ Lean

A positive density floor gives an inverse-budget lower bound on ambiguity for every $K$ -label design. Equal-width cells give a matching upper bound for the optimal ambiguity under that floor, and an inverse-budget upper bound for any score law, including laws with atoms. The displayed constants thus translate a label budget into a worst-case ATE-width guarantee before outcomes are analyzed.

For a continuous, strictly positive score density, the leading coefficient has an exact law-specific form. An interval-cell release attains that coefficient asymptotically.

Theorem 5 [thm:sharp-high-resolution-constant] (Sharp high resolution constant).

Let $E = [ε, 1 - ε]$ be the score interval, and let $H$ be a probability law on $E$ . Suppose:

(Overlap.) The overlap condition in Assumption 1 holds.

(Density.) $H (d e) = f (e) d e$ on $E$ .

(Regularity.) The density $f$ is continuous and strictly positive on $E$ .

Let $Δ_{K} (H)$ and $D_{H} (g)$ be the optimal $K$ -label ambiguity and the worst-case ambiguity defined in Definitions 11 and 9. For every positive integer $K$ , there is a measurable release $g_{K} : E \to {0, \dots, K - 1}$ whose label cells are intervals, such that $K \to \infty lim K Δ_{K} (H) = K \to \infty lim K D_{H} (g_{K}) = \frac{1}{4} (\int_{ε}^{1 - ε} \frac{f ( e )}{e ( 1 - e )} d e)^{2} .$

⊢ Lean

The theorem writes the attaining labels as $0, \dots, K - 1$ , whereas $G_{K}$ uses $1, \dots, K$ . The bijection $r \mapsto r + 1$ preserves every label cell and hence preserves $D_{H} (g_{K})$ , so the displayed construction is a member of the release class after relabeling.

The integrand weights score regions by their density and by the reciprocal-assignment factor $1/ [e (1 - e)]$ . It suggests an ordered interval allocation with boundaries at approximately equal increments of the cumulative weight $\int_{ε}^{e} f (t) / [t (1 - t)] d t$ : regions with greater weight receive narrower cells and more labels. The constant in Theorem 5 quantifies the leading ambiguity under optimal allocation, and its interval-cell sequence attains that value.

Honest intervals with a known score law

A finite-label release determines how much of the assignment score is retained. We now consider interval estimation when its score law is known to the analyst. For trial size $n$ , the known-score trial experiment observes independent released rows under a chosen release. The sampling condition is stated explicitly.

Assumption 8 [ass:iid-trial-sampling] (Independent trial sampling).

The trial observations are independent and identically distributed under $P$ : $(R_{i}, A_{i}, Y_{i})_{i = 1}^{n} \sim iid L_{P} (R, A, Y) .$

⊢ Lean

Definition 13 [synth_1] (Average treatment effect functional).

For any measure $P$ on full rows $(E, Y_{0}, Y_{1}, A, Y, R)$ with score parameter $ε$ and $J$ labels, define the average treatment effect functional $θ (P)$ by $θ (P) = \int (Y_{1} - Y_{0}) d P .$

⊢ Lean

Independent superpopulation sampling governs how the released-row law generates the trial data and is a standard condition for interval inference in partially identified models (Imbens et al., 2004).

Coverage must account for every causal law in Definition 1 consistent with the chosen release and score law. At miscoverage level $α$ , the following criterion allows the release and interval procedure to be selected jointly.

In the next two displays, $P^{\otimes n}$ acts only on functions of the observed released rows. Its pushforward to those rows is $L_{P} (R, A, Y)^{\otimes n}$ , the sampling law in Assumption 8.

Definition 14 [def:honest-procedures] (Uniformly honest procedures

J_{n, K, α} (H)

$J_{n, K, α} (H) = {(g, C_{n}) : g \in G_{K}, P \in P (H, g) in f P^{\otimes n} [θ (P) \in C_{n} ((R_{i}, A_{i}, Y_{i})_{i = 1}^{n})] \geq 1 - α} .$

⊢ Lean

For each pair in $J_{n, K, α} (H)$ , the interval $C_{n}$ attains the stated coverage uniformly over causal laws for its release. Among these pairs, the design criterion is worst-case expected interval length.

Definition 15 [def:minimax-honest-length] (Minimax honest length

L_{n, K, α}^{⋆} (H)

$L_{n, K, α}^{⋆} (H) = (g, C_{n}) \in J_{n, K, α} (H) in f P \in P (H, g) sup E_{P^{\otimes n}} [len (C_{n})] .$

⊢ Lean

The criterion $L_{n, K, α}^{⋆} (H)$ measures the shortest worst-case expected length attainable through joint choice of a release and an honest interval. The next result gives matching orders over the positive lower-density class in Definition 12, together with a sampling lower bound for every score law.

Theorem 6 [thm:minimax-honest-length] (Minimax honest interval length).

Consider the following conditions:

(Overlap.) The overlap parameter $ε$ satisfies Assumption 1.

(Miscoverage.) $0 < α < 1/2$ .

(Trial size.) $n \geq 1$ .

(Label budget.) $K \geq 1$ .

There are constants $C_{ε, α} > 0$ and $c_{ε, α} > 0$ , independent of $H, n, K$ , such that every score law $H$ on $E = [ε, 1 - ε]$ satisfies $c_{ε, α} n^{- 1/2} \leq L_{n, K, α}^{⋆} (H),$ where the minimax expected length is defined in Definition 15.

For every $m_{f} > 0$ , there is a constant $c_{ε, m_{f}, α} > 0$ such that every $H \in H_{ε, m_{f}}^{lb}$ , as defined in Definition 12, satisfies $c_{ε, m_{f}, α} (K^{- 1} + n^{- 1/2}) \leq L_{n, K, α}^{⋆} (H) \leq C_{ε, α} (K^{- 1} + n^{- 1/2}) .$

An interval attaining the upper bound uses the equal-width release with labels $r \in R_{K} = {1, \dots, K}$ : $g_{K} (e) = 1 + min {⌊ \frac{K ( e - ε )}{1 - 2 ε} ⌋, K - 1}, z_{r} = ε + \frac{( r - \frac{1}{2} ) ( 1 - 2 ε )}{K} .$ For released trial rows $(R_{i}, A_{i}, Y_{i})_{i = 1}^{n}$ , define $T_{n} = \frac{1}{n} i = 1 \sum n {\frac{A _{i} Y _{i}}{z _{R_{i}}} - \frac{( 1 - A _{i} ) Y _{i}}{1 - z _{R_{i}}}}, R_{n, K} = \frac{4}{ε} \frac{lo g ( 4/ α )}{n} + \frac{1 - 2 ε}{2 K ε ( 1 - ε )} .$ With $clampATE (t) = max {- 1, min {1, t}}$ , the interval $C_{n} (x) = [clampATE (T_{n} (x) - R_{n, K}), clampATE (T_{n} (x) + R_{n, K})]$ satisfies $(g_{K}, C_{n}) \in J_{n, K, α} (H)$ , with honesty defined in Definition 14. For every $P \in P (H, g_{K})$ , as defined in Definition 1, its expected length under the $n$ -fold released-row law satisfies $\int ∣ C_{n} (x) ∣ d P_{rel}^{\otimes n} (x) \leq C_{ε, α} (K^{- 1} + n^{- 1/2}) .$

⊢ Lean

The two terms in Theorem 6 reflect score variation within a label cell and sampling variation across released rows. Midpoint inverse-probability weights give an honest interval whose radius accounts for both. Over the positive lower-density class, a label budget of order $n$ balances these terms and attains root- $n$ expected length. The matching lower bound makes this balance a property of the experiment, rather than of the particular interval construction.

Inference with an independent score log

The known-score analysis in Theorem 6 takes the score law as given. The external score-log experiment instead fixes a finite-label release and combines the trial rows with an independent log of $m$ scores. The score-log array $(E_{j}^{log})_{j = 1}^{m}$ supplies information about the score law while retaining the trial’s released-row data structure. Two sampling conditions specify this combination.

Assumption 9 [ass:external-log-iid] (Independent score-log sampling).

The external score-log observations are independent and identically distributed with law $H$ : $(E_{j}^{log})_{j = 1}^{m} \sim iid H .$

⊢ Lean

Independent and identically distributed auxiliary-sample observations are a standard data-combination condition (Marella et al., 2019). Here they make the empirical score distribution informative about the population score law.

Assumption 10 [ass:external-log-independent] (Independent trial and score log).

The external score log is independent of the trial observations: $(E_{j}^{log})_{j = 1}^{m} ⊥ ⊥ (R_{i}, A_{i}, Y_{i})_{i = 1}^{n} .$

⊢ Lean

Independence across the two samples is the standard independent two-sample data-combination condition (Marella et al., 2019). It gives the trial and score-log empirical measures separate sampling scales. The admissible law pairs and their joint sampling law can now be stated.

Definition 16 [def:external-law-class] (External law class

X (g)

$X (g) = {(P, H) : H \in P (E), P \in P (H, g)} .$ The class uses the conditions in Assumptions 1, 2, 3, 4, and 5.

⊢ Lean

The external law class $X (g)$ lets the score law vary over probability measures on the score interval, including atomic laws, while maintaining the causal and release conditions of Definition 1.

Definition 17 [def:external-experiment] (External experiment

Q_{P, H}^{n, m}

For $(P, H) \in X (g)$ , the joint law of $n$ released trial observations $(R_{i}, A_{i}, Y_{i})$ and $m$ independent score-log observations $E_{j}^{log}$ is $Q_{P, H}^{n, m} = L_{P} (R, A, Y)^{\otimes n} \otimes H^{\otimes m} .$

⊢ Lean

The product law $Q_{P, H}^{n, m}$ makes coverage a joint-sample requirement. For a fixed release, honest intervals must cover the population average treatment effect uniformly over the external law class.

Definition 18 [def:external-honest-procedures] (External honest procedures

J_{n, m, α}^{ext} (g)

$J_{n, m, α}^{ext} (g) = {C_{n, m} : (P, H) \in X (g) in f Q_{P, H}^{n, m} [θ (P) \in C_{n, m}] \geq 1 - α} .$

⊢ Lean

Membership in $J_{n, m, α}^{ext} (g)$ requires coverage for every admissible score law and causal law. Interval length is evaluated relative to the sharp identified interval in Definition 7 at the same released and score laws.

Definition 19 [def:external-excess-risk] (Minimax external excess risk

R_{n, m, α}^{⋆} (g)

$R_{n, m, α}^{⋆} (g) = C_{n, m} \in J_{n, m, α}^{ext} (g) in f (P, H) \in X (g) sup E_{Q_{P, H}^{n, m}} [(len (C_{n, m}) - len I (L_{P} (R, A, Y); H, g))_{+}] .$

⊢ Lean

The risk $R_{n, m, α}^{⋆} (g)$ measures expected positive excess length beyond the identified interval, then takes the worst case over admissible law pairs and the best honest procedure. To compare experiments with different trial and log sizes, the following normalization uses the sum of their square-root sampling scales.

Definition 20 [def:external-normalized-risk] (Normalized external risk

T_{n, m, α} (g)

$b_{n, m} = (n^{- 1/2} + m^{- 1/2})^{- 1}, T_{n, m, α} (g) = b_{n, m} R_{n, m, α}^{⋆} (g) .$

⊢ Lean

The normalizer $b_{n, m}$ puts the excess risk on the two-sample root scale; $T_{n, m, α} (g)$ records the resulting normalized risk. Constructing an interval on this scale uses distances between finite measures that account for both cell mass and distribution within a cell.

Definition 21 [synth_5] (Finite-measure distances).

For finite nonnegative measures $μ, ν$ on a compact interval $S$ , define their total-mass-plus-integrated-CDF distance by $d_{S} (μ, ν) = ∣ μ (S) - ν (S) ∣ + \int_{S} μ (S \cap (- \infty, t]) - ν (S \cap (- \infty, t]) d t .$ The outcome-measure distance $d_{[0, 1]}$ uses $S = [0, 1]$ , with integration over $[0, 1]$ ; the score-measure distance $d_{E}$ uses $S = E = [ε, 1 - ε]$ , with integration over $[ε, 1 - ε]$ .

The total-mass term records arm-label frequencies, while the integrated distribution-function term records variation in outcome or score values. The projection below uses the trial and score-log empirical measures to select nearby candidate laws. Their compatible ATE ranges are collected into one confidence interval. The countable rational sieve makes this mathematical construction measurable.

Definition 22 [def:external-projection-handle] (External projection confidence interval).

The external projection confidence interval $C_{n, m}$ is defined for $ε, α \in R$ , $J, n, m \in N$ , a release map $g : [ε, 1 - ε] \to R_{J}$ , and a sample of $n$ trial rows and $m$ score-log values. Here $R_{J}$ is the set of $J$ labels. For each arm $a$ and label $r$ , form the empirical finite measures $λ_{a r} (B) = \frac{1}{n} i = 1 \sum n 1 {R_{i} = r, A_{i} = a, Y_{i} \in B}, σ_{a r} (B) = \frac{1}{m} j = 1 \sum m p_{a} (E_{j}^{log}) 1 {g (E_{j}^{log}) = r, E_{j}^{log} \in B} .$ Equip finite measures on each compact support with total-mass plus integrated-CDF distance, and set $r_{n} = \frac{4 J}{α n}, r_{m} = \frac{2 J ( 2 - 2 ε )}{α m} .$

For $q \in Q$ , define the clamped outcome and score support codes $x (q) = max {0, min {1, q}}, e_{ε} (q) = ε + (1 - 2 ε) x (q) .$ For a finite sequence $L = ((q_{s}, w_{s}))_{s = 1}^{N}$ of rational support-weight pairs, define the finitely supported measures $ν_{Y} (L) = s = 1 \sum N max {w_{s}, 0} δ_{x (q_{s})}, ν_{E} (L) = s = 1 \sum N max {w_{s}, 0} δ_{e_{ε} (q_{s})},$ where the nonnegative weights are viewed as extended-real weights.

When $0 < ε < 1/2$ , let $D_{ε, J}$ consist of all pairs of arrays $((ν_{Y} (L_{a r}^{Y}))_{a, r}, (ν_{E} (L_{a r}^{E}))_{a, r})$ formed from separate, arbitrary finite sequences $L_{a r}^{Y}$ and $L_{a r}^{E}$ for every arm-label cell, subject to equality of the outcome and score measures’ total masses in each cell. For all other $ε$ , set $D_{ε, J} = \emptyset$ . Define the candidate set by the two closed empirical-ball conditions $B_{n, m} = {(λ^{'}, σ^{'}) \in D_{ε, J} : a, r \sum d_{[0, 1]} (λ_{a r}^{'}, λ_{a r}) \leq r_{n}, a, r \sum d_{E} (σ_{a r}^{'}, σ_{a r}) \leq r_{m}},$ where $E = [ε, 1 - ε]$ is the score interval.

For any sieve array $b = (λ^{b}, σ^{b})$ , put $q_{a r}^{b} = λ_{a r}^{b} ([0, 1]) = σ_{a r}^{b} (E)$ . In a cell with $q_{a r}^{b} > 0$ , let $F_{a r}^{b} = λ_{a r}^{b} / q_{a r}^{b}$ be the normalized outcome law and let $W_{a r}^{b}$ be the pushforward of $σ_{a r}^{b} / q_{a r}^{b}$ under $e \mapsto 1/ p_{a} (e)$ . Define the lower and upper arm endpoints by $\underline{M}_{a} (b) = r : q_{a r}^{b} > 0 \sum q_{a r}^{b} \int_{0}^{1} Q_{F_{a r}^{b}} (u) Q_{W_{a r}^{b}} (1 - u) d u, \overline{M}_{a} (b) = r : q_{a r}^{b} > 0 \sum q_{a r}^{b} \int_{0}^{1} Q_{F_{a r}^{b}} (u) Q_{W_{a r}^{b}} (u) d u .$ Each zero-mass cell contributes $0$ to both sums; no normalized law is needed for that cell. For each $b \in B_{n, m}$ , set $I (b) = [\underline{M}_{1} (b) - \overline{M}_{0} (b), \overline{M}_{1} (b) - \underline{M}_{0} (b)] .$ When $B_{n, m} \neq = \emptyset$ , form $J_{n, m} = [- 1, 1] \cap cl conv b \in B_{n, m} ⋃ I (b) .$ The totalized interval is $C_{n, m} = {J_{n, m}, {0}, B_{n, m} \neq = \emptyset and J_{n, m} \neq = \emptyset, B_{n, m} = \emptyset or (B_{n, m} \neq = \emptyset and J_{n, m} = \emptyset) .$

⊢ Lean

In Definition 22, trial observations determine empirical outcome measures and the log determines assignment-weighted empirical score measures. The sieve combines finitely supported rationally coded measures with matched outcome and score masses in each arm-label cell, including arrays assembled independently across cells, and retains candidates in the two displayed empirical balls. This conservative projection contains the population sharp interval on the coverage event; closing and convexifying the candidate intervals produces the interval $C_{n, m}$ used in the rate result.

Theorem 7 [thm:external-score-root-order] (External-score root order).

Let $E = [ε, 1 - ε]$ , and let $g : E \to R_{J}$ be a measurable finite-label release. Suppose:

(Overlap.) The overlap condition in Assumption 1 holds.

(Miscoverage.) $0 < α < 1/2$ .

(Joint sampling.) For every $n, m$ , a joint sampling law $Q_{P, H}^{n, m}$ is specified for each admissible causal law $P$ and score law $H$ . Its trial marginal consists of $n$ independent draws from the released law. Its score-log marginal and independence from the trial sample satisfy Assumptions 9 and 10.

Set $L_{α} = 1 + (1 - 2 α)^{2}, S_{g} = r \in R_{J}, e_{1} < e_{2} < e_{3} e_{1}, e_{2}, e_{3} \in C_{r} sup \frac{( e _{3} - e _{2} ) ( 1 - e _{1} / e _{2} )}{( e _{3} - e _{2} ) ^{2} + ( e _{3} - e _{1} ) ^{2} + ( e _{2} - e _{1} ) ^{2}},$ and $c_{tr} (α) = \frac{( 1 - 2 α ) lo g L _{α}}{4}, c_{log} (g, α) = \frac{( 1 - 2 α ) lo g L _{α}}{2 3} S_{g} .$ Then $0 < S_{g} \leq 1$ . There is a constant $C_{ε, J, α, g} > 0$ such that, for every positive $n, m$ , the minimax excess risk of Definition 19 satisfies $c_{tr} (α) n^{- 1/2} \leq R_{n, m, α}^{⋆} (g) \leq C_{ε, J, α, g} (n^{- 1/2} + m^{- 1/2}) .$ For each such $n, m$ , an interval procedure $C_{n, m}$ belongs to the honest class of Definition 18, agrees pointwise as a closed interval with the projection interval of Definition 22, and, for every admissible pair $(P, H)$ , satisfies $E_{Q_{P, H}^{n, m}} [max {0, length (C_{n, m}) - length (I (P_{rel}; H, g))}] \leq C_{ε, J, α, g} (n^{- 1/2} + m^{- 1/2}) .$

In the external-score direction, $m \to \infty lim inf n \geq 1 in f m R_{n, m, α}^{⋆} (g) \geq c_{log} (g, α) > 0.$ For every $ρ > 0$ , the normalized risk $T_{n, m, α} (g)$ of Definition 20 obeys $0 < max {\frac{c _{tr} ( α )}{1 + ρ}, \frac{c _{log} ( g , α ) ρ}{1 + ρ}} \leq n, m \to \infty n / m \to ρ lim inf T_{n, m, α} (g) \leq n, m \to \infty n / m \to ρ lim sup T_{n, m, α} (g) \leq C_{ε, J, α, g} .$

⊢ Lean

The upper bound in Theorem 7 follows the two sources of empirical variation in the projection: released trial rows contribute the $n^{- 1/2}$ scale, and assignment-weighted score-log measures contribute the $m^{- 1/2}$ scale. The theorem also gives separate lower bounds. The trial-sample lower bound applies at every positive pair of sample sizes, and the score-log lower bound remains positive asymptotically uniformly over trial sizes. For a positive limiting trial-to-log ratio $ρ$ , these lower bounds and the projection interval establish the joint order $n^{- 1/2} + m^{- 1/2}$ . The law class includes atomic score distributions and quantile functions with flat pieces.

Discussion and open questions

A score label linked to each trial row preserves the association between a measurable set of assignment probabilities, treatment, and outcome. Given a known score law, the arm-label outcome and score distributions determine the sharp mean endpoints in Definition 6 and hence the average treatment effect interval in Definition 7. The worst-case width in Definition 9 measures the information retained by a release in units of the target parameter. Theorem 3 characterizes when that information suffices for point identification across compatible released laws.

For score laws on $[ε, 1 - ε]$ with a common density floor $m_{f}$ satisfying $0 < m_{f} \leq (1 - 2 ε)^{- 1}$ , Theorem 4 gives an order- $K^{- 1}$ rate for optimal worst-case ambiguity. Under the score-law conditions of Theorem 5, its high-resolution allocation rule assigns finer cells where local variation contributes more to the ambiguity criterion. The rule connects the placement of labels to the sharp interval that an analyst can recover from the released data. Theorem 6 establishes a $K^{- 1} + n^{- 1/2}$ minimax honest-length rate for known score laws with a positive density lower bound, attained up to constants by equal-width labels.

Open questions

The projection interval in Definition 22 is defined through a countable rational sieve. A finite truncation and optimization rule, with an error bound that preserves coverage and controls excess length for atomic laws and arbitrary measurable cells, remains to be developed.

The two-source bounds in Theorem 7 establish the root scale for excess interval length with an independent score log. A sharp limit would quantify the combined contribution of trial and score-log sampling when their sizes grow at a fixed positive ratio. The question is stated for the full external-law class and, where appropriate, for a specified regular subclass.

Remark 1 [oeq:external-score-projection] (External-score sharp limits).

Fix a measurable release $g$ , $0 < α < 1/2$ , and $ρ \in (0, \infty)$ . The sharp asymptotic analysis over $X (g)$ , with confidence procedures in $J_{n, m, α}^{ext} (g)$ , concerns $n, m \to \infty n / m \to ρ lim inf T_{n, m, α} (g) and n, m \to \infty n / m \to ρ lim sup T_{n, m, α} (g) .$ It asks whether these limits coincide and, if so, for their common sharp constant. If a common sharp limit fails over the full class, the corresponding question concerns an explicitly defined regular subclass of $X (g)$ , with both uniform honesty and the supremum in expected excess length restricted to that subclass. The subclass analysis specifies its regularity conditions and sharp limit for each $ρ \in (0, \infty)$ , using the external projection construction to obtain an attaining procedure or a counterexample.

⊢ Lean

For a regular subclass, the honesty requirement and worst-case excess-length criterion in Remark 1 apply to the same collection of laws. The projection construction in Definition 22 supplies a concrete route for studying attainment, while the fixed sample-size ratio keeps both sources of sampling variation in the asymptotic comparison.

Appendices

Proofs and verification scope

Fixed-law bounds and compatibility

The fixed released-law calculation precedes the optimization over released laws. We attribute its mathematical antecedent to Fan et al. (2014). The formal declaration and proof displayed here are independently checked under the paper’s stated model conditions. The compatibility criterion in Theorem 1 identifies the released laws to which the calculation applies. The first auxiliary result records the arm-label masses implied by a score law and release rule.

Lemma 1 [lem:released-arm-cell-masses] (Released arm-cell masses).

Let $H$ be a measure on the score interval $E$ , let $g : E \to R_{J}$ be a release rule, and let $P \in P (H, g)$ as in Definition 1. Write $P_{rel} = L_{P} (R, A, Y)$ for the released law. Then $H$ and $P_{rel}$ are probability laws, and, for every $a \in A$ and $r \in R_{J}$ , $P_{rel} (A = a, R = r) = q_{a r},$ where $q_{a r}$ is the arm-cell mass defined in Definition 5.

⊢ Lean

Proof of Lemma 1.

The law $P$ is a probability law by Definition 1. Its score marginal is $H$ by Assumption 2, and its released-record marginal is $P_{rel}$ . Both marginals are therefore probability laws.

Fix $r \in R_{J}$ . By Assumption 5, $R = g (E)$ almost surely. Conditioning on $(E, Y_{0}, Y_{1})$ and applying Assumption 3 gives $P_{rel} (A = 1, R = r) = P (A = 1, g (E) = r) = E_{P} [E 1_{{g (E) = r}}] = \int_{C_{r}} e H (d e) .$

For the control arm, partition the event $E \in C_{r}$ by treatment assignment. The score marginal condition and the preceding identity yield $P_{rel} (A = 0, R = r) = P (E \in C_{r}) - P (A = 1, E \in C_{r}) = H (C_{r}) - \int_{C_{r}} e H (d e) = \int_{C_{r}} (1 - e) H (d e) = q_{0 r} .$ The integral subtraction is valid because the score is bounded on $E$ . Finally, $p_{1} (e) = e$ in Definition 5, so the treated-arm identity is $P_{rel} (A = 1, R = r) = q_{1 r}$ . These two identities cover every $a \in A$ .

∎

These mass equalities connect the causal-law class to the compatibility criterion in Theorem 1. For each compatible released law, the fixed-law result gives sharp bounds through quantile rearrangement within positive-mass arm-label cells.

Lemma 2 [lem:fixed-released-law-baseline] (Sharp fixed released law bounds).

Let $H$ be a measure on the score interval $E = [ε, 1 - ε]$ , let $g : E \to R_{J}$ be a release rule, and let $P_{rel}$ be a measure on the released label, treatment arm, and outcome. Suppose:

(Overlap.) The score support satisfies Assumption 1.

(Release.) The rule $g$ is measurable.

(Compatibility.) $M (H, g, P_{rel}) \neq = \emptyset$ .

For each arm $a \in {0, 1}$ and label $r$ , let $C_{r} = {e : g (e) = r}$ , let $p_{a} (e)$ be the probability of arm $a$ at score $e$ , and set $q_{a r} = \int_{C_{r}} p_{a} (e) H (d e)$ . In each cell with $q_{a r} > 0$ , let $F_{a r}$ be the outcome law conditional on arm $a$ and label $r$ under $P_{rel}$ , let $E_{a r}$ have law $q_{a r}^{- 1} 1_{C_{r}} (e) p_{a} (e) H (d e)$ , and let $W_{a r} = 1/ p_{a} (E_{a r})$ . Writing $Q$ for a generalized quantile, define $\underline{μ}_{a} = r : q_{a r} > 0 \sum q_{a r} \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (1 - u) d u, \overline{μ}_{a} = r : q_{a r} > 0 \sum q_{a r} \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (u) d u .$ Then, for every $a \in {0, 1}$ , ${E_{P} [Y_{a}] : P \in M (H, g, P_{rel})} = [\underline{μ}_{a}, \overline{μ}_{a}] .$ The attainable average treatment effects form the interval defined in Definition 7: ${E_{P} [Y_{1} - Y_{0}] : P \in M (H, g, P_{rel})} = I (P_{rel}; H, g) = [\underline{μ}_{1} - \overline{μ}_{0}, \overline{μ}_{1} - \underline{μ}_{0}] .$ Moreover, there exist $P^{-}, P^{+} \in M (H, g, P_{rel})$ such that $E_{P^{-}} [Y_{1} - Y_{0}] = \underline{μ}_{1} - \overline{μ}_{0}, E_{P^{+}} [Y_{1} - Y_{0}] = \overline{μ}_{1} - \underline{μ}_{0} .$

⊢ Lean

Proof of Lemma 2.

1. Construct compatible endpoint laws. Compatibility implies that $H$ and $P_{rel}$ are probability laws and, for every arm $a$ and label $r$ , $P_{rel} (A = a, R = r) = q_{a r} .$ By Assumption 1, $ε \leq p_{a} (e) \leq 1 - ε$ on $E$ . Thus $ε H (C_{r}) \leq q_{a r} \leq (1 - ε) H (C_{r}),$ so a zero-mass arm cell is also $H$ -null. Define, on $E$ , $w_{a} (e) = \frac{1}{p _{a} ( e )} .$ For each $q_{a r} > 0$ , let $U$ be uniform on $(0, 1)$ and define two laws on outcome–weight pairs: $π_{a r}^{-} = L (Q_{F_{a r}} (U), Q_{W_{a r}} (1 - U)), π_{a r}^{+} = L (Q_{F_{a r}} (U), Q_{W_{a r}} (U)) .$ Both have marginals $F_{a r}$ and $L (W_{a r})$ . They can be lifted to laws $γ_{a r}^{s}$ on score–outcome pairs, for $s \in {-, +}$ , satisfying $L_{γ_{a r}^{s}} (E) = G_{a r}, L_{γ_{a r}^{s}} (Y, w_{a} (E)) = π_{a r}^{s} .$ Indeed, $L (W_{a r})$ is the common weight marginal of $π_{a r}^{s}$ and $L (E_{a r}, w_{a} (E_{a r}))$ . Conditional on that weight, couple their outcome and score coordinates. Conditional laws exist on these standard Borel spaces.

For either sign, form the assigned and potential-outcome laws $N_{a}^{s} = r : q_{a r} > 0 \sum q_{a r} γ_{a r}^{s}, M_{a}^{s} (d e, d y) = w_{a} (e) N_{a}^{s} (d e, d y) .$ The score marginal of $N_{a}^{s}$ is $p_{a} (e) H (d e)$ : on $C_{r}$ , its score marginal is $q_{a r} G_{a r} (d e) = 1_{C_{r}} (e) p_{a} (e) H (d e)$ , and zero-mass cells are $H$ -null. Consequently, $M_{a}^{s} (d e, [0, 1]) = H (d e), p_{a} (e) M_{a}^{s} (d e, d y) = N_{a}^{s} (d e, d y) .$ For signs $s_{0}, s_{1} \in {-, +}$ , glue $M_{0}^{s_{0}}$ and $M_{1}^{s_{1}}$ along their common score marginal $H$ , obtaining a law of $(E, Y_{0}, Y_{1})$ with those two score–outcome marginals. Conditional on the resulting variables, draw $A = 1$ with probability $E$ , and set $R = g (E)$ and $Y = Y_{A}$ . Denote the resulting full law by $P^{s_{0} s_{1}}$ .

This construction has score law $H$ , score-based assignment, consistency, and deterministic release. For $q_{a r} > 0$ and measurable $B \subseteq [0, 1]$ , it also gives $P^{s_{0} s_{1}} (R = r, A = a, Y \in B) = \int_{C_{r} \times B} p_{a} (e) M_{a}^{s_{a}} (d e, d y) = q_{a r} F_{a r} (B) = P_{rel} (R = r, A = a, Y \in B) .$ Both sides vanish when $q_{a r} = 0$ . Hence every $P^{s_{0} s_{1}}$ belongs to the class in Definition 2.

2. Compute their means and treatment effects. The two quantile couplings give, for every positive-mass cell, $\int y w π_{a r}^{-} (d y, d w) = \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (1 - u) d u, \int y w π_{a r}^{+} (d y, d w) = \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (u) d u .$ Since $M_{a}^{s} = w_{a} N_{a}^{s}$ , summing these identities over cells yields $E_{P^{s_{0} s_{1}}} [Y_{a}] = r : q_{a r} > 0 \sum q_{a r} \int y w π_{a r}^{s_{a}} (d y, d w) = {\underline{μ}_{a}, \overline{μ}_{a}, s_{a} = -, s_{a} = + .$ Set $P_{lo} = P^{--}, P_{hi} = P^{++}, P^{-} = P^{+-}, P^{+} = P^{-+},$ where the first sign selects the control-arm coupling. Bounded outcomes permit subtraction of their expectations, so $E_{P^{-}} [Y_{1} - Y_{0}] = \underline{μ}_{1} - \overline{μ}_{0}, E_{P^{+}} [Y_{1} - Y_{0}] = \overline{μ}_{1} - \underline{μ}_{0} .$

3. Bound every compatible arm mean. Fix $P \in M (H, g, P_{rel})$ . For $q_{a r} > 0$ , define its conditional outcome–weight coupling by $π_{a r, P} = L_{P} (Y_{a}, w_{a} (E) ∣ A = a, R = r) .$ Consistency and the released-law condition give its outcome marginal $F_{a r}$ ; score-based assignment and score marginality give its weight marginal $L (W_{a r})$ . The same assignment identity, now weighted by $w_{a} (E)$ , gives $E_{P} [Y_{a}] = r : q_{a r} > 0 \sum q_{a r} \int y w π_{a r, P} (d y, d w) .$ Cells with $q_{a r} = 0$ contribute zero.

For any coupling $π$ of $F_{a r}$ and $L (W_{a r})$ , the layer-cake identity writes $\int y w d π$ as the integral of joint upper-tail probabilities. For thresholds $τ_{Y}, τ_{W} \geq 0$ , those probabilities lie between the intersection bounds $max {P (Y > τ_{Y}) + P (W > τ_{W}) - 1, 0} \leq P (Y > τ_{Y}, W > τ_{W}) \leq min {P (Y > τ_{Y}), P (W > τ_{W})} .$ The couplings $π_{a r}^{-}$ and $π_{a r}^{+}$ attain the respective bounds: their quantile upper-tail events are oppositely ordered and nested, respectively. Integrating the tail bounds therefore gives $\int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (1 - u) d u \leq \int y w π_{a r, P} (d y, d w) \leq \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (u) d u .$ All integrals are finite because $0 \leq Y_{a} \leq 1$ and $w_{a} (E) \leq ε^{- 1}$ . Multiplication by $q_{a r}$ and summation show that $\underline{μ}_{a} \leq E_{P} [Y_{a}] \leq \overline{μ}_{a} .$

4. Fill each arm interval. For any $x \in [\underline{μ}_{a}, \overline{μ}_{a}]$ , choose $ρ_{a} \in [0, 1]$ with $x = (1 - ρ_{a}) \underline{μ}_{a} + ρ_{a} \overline{μ}_{a},$ including $ρ_{a} = 0$ when the endpoints coincide, and define $P_{a, x} = (1 - ρ_{a}) P_{lo} + ρ_{a} P_{hi} .$ Probability normalization, the score and released marginals, and the assignment identity are preserved by this mixture; consistency and deterministic release hold under both component laws and hence under the mixture. Thus $P_{a, x}$ is compatible. Linearity of integration gives $E_{P_{a, x}} [Y_{a}] = (1 - ρ_{a}) E_{P_{lo}} [Y_{a}] + ρ_{a} E_{P_{hi}} [Y_{a}] = x .$ Together with Equation 2, this proves the claimed attainable interval for each arm.

5. Fill the treatment-effect interval. For every compatible $P$ , the two arm bounds and $E_{P} [Y_{1} - Y_{0}] = E_{P} [Y_{1}] - E_{P} [Y_{0}]$ give $\underline{μ}_{1} - \overline{μ}_{0} \leq E_{P} [Y_{1} - Y_{0}] \leq \overline{μ}_{1} - \underline{μ}_{0} .$ Conversely, for any $x$ in this interval, choose $ρ_{ATE} \in [0, 1]$ such that $x = (1 - ρ_{ATE}) (\underline{μ}_{1} - \overline{μ}_{0}) + ρ_{ATE} (\overline{μ}_{1} - \underline{μ}_{0}),$ and set $P_{x} = (1 - ρ_{ATE}) P^{-} + ρ_{ATE} P^{+} .$ The same mixture argument makes $P_{x}$ compatible, and linearity gives $E_{P_{x}} [Y_{1} - Y_{0}] = x$ . The interval is $I (P_{rel}; H, g)$ by Definition 7; the compatible laws $P^{-}$ and $P^{+}$ attain its two endpoints as computed in Equation 1.

∎

The attainable endpoints make the interval sharp for each compatible released law. With the compatibility characterization in Theorem 1, this fixed-law result supplies the interval whose width is optimized in Definition 9.

Ambiguity and finite-label design

The all-label result in Theorem 2 applies that outer optimization to the fixed-law interval, while Theorem 3 characterizes universal point identification. For finite-label design, the proof first expresses the paired distortion as an optimization over arbitrary measurable partitions. The next lemma establishes the high-resolution limit over arbitrary measurable partitions and constructs an asymptotically attaining sequence of ordered interval cells.

Lemma 3 [lem:paired-high-resolution-quantization] (Paired high-resolution quantization).

Let $I = [a, b]$ , let $S$ be an integer, and let $β_{s} : I \times I \to R$ , $s = 1, \dots, S$ , satisfy:

(Interval.) $a < b$ .

(Number of components.) $S \geq 1$ .

(Continuity.) Each $β_{s}$ is continuous on $I \times I$ .

(Positivity.) $β_{s} (x, z) > 0$ for every $s$ and every $x, z \in I$ .

For each positive integer $k$ , define $V_{k} = (B_{1}, \dots, B_{k}) measurable, pairwise disjoint ⋃_{j = 1}^{k} B_{j} = I, z_{j s} \in I in f j = 1 \sum k s = 1 \sum S \int_{B_{j}} β_{s} (x, z_{j s}) ∣ x - z_{j s} ∣ d x, w (x) = s = 1 \sum S β_{s} (x, x) .$ Then $k \to \infty lim k V_{k} = \frac{1}{4} (\int_{a}^{b} w (x) d x)^{2} .$ For each positive integer $k$ , let $a = t_{0} < \dots < t_{k} = b$ be boundaries satisfying $\int_{a}^{t_{j}} w (x) d x = \frac{j}{k} \int_{a}^{b} w (x) d x (j = 0, \dots, k) .$ Set $B_{j} = [t_{j - 1}, t_{j})$ for $j < k$ , $B_{k} = [t_{k - 1}, t_{k}]$ , and $z_{j s} = (t_{j - 1} + t_{j}) /2$ for every $s$ . These cells form a measurable, pairwise-disjoint partition of $I$ , every $z_{j s}$ belongs to $I$ , and $k \to \infty lim k j = 1 \sum k s = 1 \sum S \int_{B_{j}} β_{s} (x, z_{j s}) ∣ x - z_{j s} ∣ d x = \frac{1}{4} (\int_{a}^{b} w (x) d x)^{2} .$

⊢ Lean

Proof of Lemma 3.

Write $f (x) = w (x), Λ = \int_{a}^{b} f (x) d x .$ Continuity, positivity, and compactness give $\underline{β} = 1 \leq s \leq S x, z \in [a, b] min β_{s} (x, z) > 0, \underline{f} = x \in [a, b] min f (x) > 0, \overline{f} = x \in [a, b] max f (x) < \infty.$

For the stated construction, the continuous function $x \mapsto \int_{a}^{x} f (u) d u$ is strictly increasing from $0$ to $Λ$ . Equivalently, its boundaries can be written $t_{j} = in f {x \in [a, b] : \frac{j Λ}{k} \leq \int_{a}^{x} f (u) d u}, j = 0, \dots, k .$ Thus $t_{0} = a$ , $t_{k} = b$ , the boundaries are ordered, and each cell has $f$ -mass $Λ/ k$ . Put $h_{j} = t_{j} - t_{j - 1}$ and $u_{j} = (t_{j - 1} + t_{j}) /2$ . Then $0 < h_{j} \leq \frac{Λ}{k f}, k j = 1 \sum k h_{j}^{2} \leq \frac{Λ}{f} j = 1 \sum k h_{j} = \frac{Λ ( b - a )}{f} .$ Uniform continuity of $f$ and the $β_{s}$ , together with $\int_{B_{j}} ∣ x - u_{j} ∣ d x = h_{j}^{2} /4$ , shows that, for every $ε > 0$ and all sufficiently large $k$ , uniformly over the cells, $w (u_{j}) h_{j}^{2} - (\frac{Λ}{k})^{2} \leq ε h_{j}^{2}, s = 1 \sum S \int_{B_{j}} β_{s} (x, u_{j}) ∣ x - u_{j} ∣ d x - \frac{w ( u _{j} ) h _{j}^{2}}{4} \leq ε h_{j}^{2} .$ The bounded scaled sum of squared cell lengths therefore gives $k j = 1 \sum k s = 1 \sum S \int_{B_{j}} β_{s} (x, u_{j}) ∣ x - u_{j} ∣ d x ⟶ \frac{Λ ^{2}}{4} .$

For the lower bound, take any admissible measurable partition and reproduction points, and define its cost by $D_{k} (B, z) = j = 1 \sum k s = 1 \sum S \int_{B_{j}} β_{s} (x, z_{j s}) ∣ x - z_{j s} ∣ d x .$ Fix $0 < η < 1$ . Choose $e > 0$ sufficiently small that $e \leq min {1, \underline{β} /2}, e (2 \overline{f} + 1 + S) \leq η S \underline{β} .$ Uniform continuity supplies $δ > 0$ such that, for each cell $j$ , whenever $x, y \in [a, b]$ satisfy $∣ x - z_{j s} ∣ < δ$ and $∣ y - z_{j s} ∣ < δ$ for every $s = 1, \dots, S$ , one has $β_{s} (x, z_{j s}) - β_{s} (y, y) < e (1 \leq s \leq S), ∣ f (x) - f (y) ∣ < e .$ Set $G_{j} = {x \in B_{j} : ∣ x - z_{j s} ∣ < δ for every s}, D_{j} = B_{j} ∖ G_{j} .$ For a nonempty $G_{j}$ , choose $y_{j} \in G_{j}$ and set $γ_{j s} = β_{s} (y_{j}, y_{j}) - e, Q_{j} = f (y_{j}) + e, Γ_{j} = s = 1 \sum S γ_{j s} .$ These coefficients are positive. On $G_{j}$ , $β_{s} (x, z_{j s}) \geq γ_{j s}$ and $f (x) \leq Q_{j}$ . Moreover, the choice of $e$ , $w (y_{j}) \geq S \underline{β}$ , and $f (y_{j}) \leq \overline{f}$ give $(1 - η) Q_{j}^{2} \leq w (y_{j}) - S e = Γ_{j} .$

For any measurable $G \subset R$ of finite measure and any $v \in R$ , filling the points nearest $v$ first yields $\int_{G} ∣ x - v ∣ d x \geq \int_{0}^{∣ G ∣/2} (∣ G ∣ - 2 r) d r = \frac{∣ G ∣ ^{2}}{4} .$ With $v = Γ_{j}^{- 1} \sum_{s} γ_{j s} z_{j s}$ , the triangle inequality gives $\sum_{s} γ_{j s} ∣ x - z_{j s} ∣ \geq Γ_{j} ∣ x - v ∣$ . Consequently, including the trivial case $G_{j} = \emptyset$ , $s = 1 \sum S \int_{B_{j}} β_{s} (x, z_{j s}) ∣ x - z_{j s} ∣ d x \geq \frac{Γ _{j} ∣ G _{j} ∣ ^{2}}{4} \geq \frac{1 - η}{4} (\int_{G_{j}} f (x) d x)^{2} .$ Summing and applying Cauchy–Schwarz, with disjointness and coverage of the cells, gives $k D_{k} (B, z) \geq \frac{1 - η}{4} (Λ - j = 1 \sum k \int_{D_{j}} f (x) d x)^{2} .$

At every $x \in D_{j}$ , some reproduction point is at distance at least $δ$ . Hence $\underline{β} δ j = 1 \sum k ∣ D_{j} ∣ \leq D_{k} (B, z), j = 1 \sum k \int_{D_{j}} f (x) d x \leq \frac{f}{β δ} D_{k} (B, z) .$ If $k D_{k} (B, z) \leq Λ^{2} /4$ , the omitted $f$ -mass is therefore at most $\overline{f} Λ^{2} / (4 \underline{β} δ k)$ ; for larger costs the desired asymptotic lower bound is immediate. It follows uniformly over admissible partitions that $k \to \infty lim inf k V_{k} \geq \frac{1 - η}{4} Λ^{2} .$ Letting $η ↓ 0$ proves the lower bound. The constructed cost bounds $V_{k}$ from above and has limit $Λ^{2} /4$ , so $k V_{k}$ has that limit as well.

Finally, the ordered boundaries with $t_{0} = a$ and $t_{k} = b$ make the stated half-open cells, with the last cell closed on the right, a measurable pairwise-disjoint partition of $[a, b]$ . Each $u_{j}$ lies between its two boundaries, hence in $[a, b]$ , and serves as $z_{j s}$ for every component.

∎

The auxiliary result identifies the leading constant for the paired loss and gives an attaining sequence of ordered cells. It supplies the quantization component of the high-resolution conclusion in Theorem 5.

External-log excess risk

The external-log analysis has two sampling contributions: released trial rows and independent score draws. The following certificate supplies lower bounds for both contributions to the excess-risk criterion in Definition 19.

Lemma 4 [lem:external-two-source-lower-certificate] (Two-source excess-risk lower bounds).

Let $E = [ε, 1 - ε]$ be the score interval, let $R_{J}$ be the finite label set, and fix a measurable release $g : E \to R_{J}$ . Let $Q_{P, H}^{n, m}$ be a family of joint sampling laws on $n$ released trial rows and $m$ score-log draws. Suppose:

(Overlap and level.) Assumption 1 holds and $0 < α < 1/2$ .

(Trial sampling.) For every $n, m$ and every admissible causal-law and score-law pair $(P, H)$ under $g$ , the trial marginal of $Q_{P, H}^{n, m}$ is the $n$ -fold product of the released-row law under $P$ .

(Score-log sampling.) The joint sampling laws satisfy Assumptions 9 and 10 for every $n, m$ .

Set $L_{α} = 1 + (1 - 2 α)^{2}, S_{g} = r \in R_{J}, e_{1}, e_{2}, e_{3} \in E e_{1} < e_{2} < e_{3}, g (e_{1}) = g (e_{2}) = g (e_{3}) = r sup \frac{( e _{3} - e _{2} ) ( 1 - e _{1} / e _{2} )}{( e _{3} - e _{2} ) ^{2} + ( e _{3} - e _{1} ) ^{2} + ( e _{2} - e _{1} ) ^{2}},$ and $c_{tr} (α) = \frac{( 1 - 2 α ) lo g L _{α}}{4}, c_{log} (g, α) = \frac{( 1 - 2 α ) lo g L _{α}}{2 3} S_{g} .$ Then $0 < S_{g} \leq 1$ . The external-score minimax excess risk of Definition 19 satisfies, for every $n, m \geq 1$ , $R_{n, m, α}^{⋆} (g) \geq \frac{c _{tr} ( α )}{n} .$ It also satisfies $m \to \infty lim inf n \geq 1 in f {m R_{n, m, α}^{⋆} (g)} \geq c_{log} (g, α) > 0.$ For every $ρ > 0$ , the normalized risk of Definition 20 satisfies $n, m \to \infty n / m \to ρ lim inf T_{n, m, α} (g) \geq max {\frac{c _{tr} ( α )}{1 + ρ}, \frac{c _{log} ( g , α ) ρ}{1 + ρ}} > 0.$

⊢ Lean

Proof of Lemma 4.

Write $β = 1 - 2 α$ , so $0 < β < 1$ , $L_{α} = 1 + β^{2} > 1$ , and both displayed certificate coefficients are positive once $S_{g} > 0$ .

The interval $E$ is infinite, whereas the label set is finite. Thus some fiber of $g$ contains three points $e_{1} < e_{2} < e_{3}$ . For any such triple, put $D (e_{1}, e_{2}, e_{3}) = (e_{3} - e_{2})^{2} + (e_{3} - e_{1})^{2} + (e_{2} - e_{1})^{2} .$ Overlap gives $0 < e_{1} / e_{2} < 1$ , and $D (e_{1}, e_{2}, e_{3}) \geq e_{3} - e_{2} > 0$ . Consequently every ratio in the definition of $S_{g}$ is positive and at most one. The set of ratios is nonempty, so $0 < S_{g} \leq 1, c_{tr} (α) > 0, c_{log} (g, α) > 0.$

We first establish a uniform upper bound used to pass the score-log certificate through an infimum and a liminf. For finite measures on $V = [v_{-}, v_{+}]$ , define $d_{V} (μ, ν) = ∣ μ (V) - ν (V) ∣ + \int_{v_{-}}^{v_{+}} ∣ μ (V \cap (- \infty, t]) - ν (V \cap (- \infty, t]) ∣ d t .$ Let $λ_{a r} (B) = P_{rel} (A = a, R = r, Y \in B)$ and $σ_{a r} (B) = \int_{B \cap C_{r}} p_{a} (e) H (d e)$ . Using the empirical cell measures in Definition 22, set $D_{Y} = a, r \sum d_{[0, 1]} (λ_{a r}, λ_{a r}), D_{E} = a, r \sum d_{E} (σ_{a r}, σ_{a r}), Λ_{ε} = ε^{- 1} + ε^{- 2} .$ For a retained sieve array, the triangle inequality places its outcome and score arrays within $r_{n} + D_{Y}$ and $r_{m} + D_{E}$ , respectively, of the population arrays. The quantile-transport arm endpoints are Lipschitz in these distances with coefficient $Λ_{ε}$ : the reciprocal arm probabilities are bounded by $ε^{- 1}$ , their variation across scores is bounded by $ε^{- 2}$ , and integration of the corresponding distribution-function differences gives the two distances above. Hence each of the four arm endpoints differs from its population endpoint by at most $δ = Λ_{ε} (r_{n} + D_{Y} + r_{m} + D_{E}) .$ The lower and upper ATE endpoints each combine two arm endpoints. Taking their convex hull and clipping to $[- 1, 1]$ therefore gives, on the projection branch of Definition 22, for its interval $C_{n, m}$ , $(len C_{n, m} - len I (P_{rel}; H, g))_{+} \leq 4 Λ_{ε} (r_{n} + D_{Y} + r_{m} + D_{E}) .$ The same inequality holds when the totalized interval in Definition 22 is ${0}$ , since its length is zero. The empirical-CDF variance bound, integrated over each support interval and summed over the $2 J$ cells, yields $E D_{Y} \leq \frac{2 J}{n}, E D_{E} \leq \frac{J ( 2 - 2 ε )}{m} .$ The radii $r_{n} = 4 J / (α n)$ and $r_{m} = 2 J (2 - 2 ε) / (α m)$ make the projection interval honest: Markov’s inequality assigns probability at most $α /2$ to each failed empirical ball, and approximation by compatible rational arrays places the population sharp interval in the resulting closed projection hull on the complementary event. Thus Definition 19 and the preceding bounds give $R_{n, m, α}^{⋆} (g) \leq 4 Λ_{ε} [(\frac{4 J}{α} + 2 J) n^{- 1/2} + (\frac{2 J ( 2 - 2 ε )}{α} + J (2 - 2 ε)) m^{- 1/2}] .$ In particular, with $M = 4 Λ_{ε} (\frac{4 J}{α} + 2 J + \frac{2 J ( 2 - 2 ε )}{α} + J (2 - 2 ε)) + 1,$ we have $T_{n, m, α} (g) \leq M$ for all $n, m \geq 1$ , by the definition of $b_{n, m}$ in Definition 20.

Fix an ordered triple $e_{1} < e_{2} < e_{3}$ in one fiber, and define $h = (e_{3} - e_{2}, - (e_{3} - e_{1}), e_{2} - e_{1}), u_{m} = \frac{lo g L _{α}}{3 ∥ h ∥ _{2} m}, q = \frac{e _{1} + e _{2} + e _{3}}{3}, t = \frac{1}{2} {\frac{e _{1}}{3} + min (\frac{e _{1} + e _{2}}{3}, \frac{e _{3}}{3})}, s = \frac{t}{q} .$ The identities $\sum_{i} h_{i} = \sum_{i} e_{i} h_{i} = 0$ show that $H_{0} = \frac{1}{3} i = 1 \sum 3 δ_{e_{i}}, H_{m} = i = 1 \sum 3 (\frac{1}{3} + u_{m} h_{i}) δ_{e_{i}}$ are probability laws with the same score mean $q$ for all sufficiently large $m$ . The strict inequalities $\frac{e _{1}}{3} < t < min (\frac{e _{1} + e _{2}}{3}, \frac{e _{3}}{3}), 0 < s < 1,$ hold by the choice of $t$ . Writing $w_{i, m} = 1/3 + u_{m} h_{i}$ for $i = 1, 2, 3$ , continuity and $u_{m} \to 0$ give, for all sufficiently large $m$ , $w_{i, m} > 0 (i = 1, 2, 3), e_{1} w_{1, m} < t < min {e_{1} w_{1, m} + e_{2} w_{2, m}, e_{3} w_{3, m}} .$ Under either score law, take $Y_{0} = 0$ , an independent Bernoulli $(s)$ potential outcome $Y_{1}$ , score-based treatment assignment, and the fixed label of the triple. These constructions satisfy Definition 16; their released trial laws coincide, with treatment probability $q$ and treated-success probability $t$ .

For score masses $w_{i}$ in this neighborhood, the upper rearrangement of the treated successes fills score $e_{1}$ and then score $e_{2}$ , while the lower rearrangement fits them at score $e_{3}$ . The endpoint formulas in Definition 6 therefore reduce to $U (w) = w_{1} + \frac{t - e _{1} w _{1}}{e _{2}}, L (w) = \frac{t}{e _{3}} .$ The control endpoints are zero. The two sharp intervals have common lower endpoint $L (w)$ , and their upper endpoints differ by $Δ_{m} = U (\frac{1}{3} + u_{m} h_{1}, \frac{1}{3} + u_{m} h_{2}, \frac{1}{3} + u_{m} h_{3}) - U (\frac{1}{3}, \frac{1}{3}, \frac{1}{3}) = u_{m} (e_{3} - e_{2}) (1 - \frac{e _{1}}{e _{2}}) > 0.$ By the endpoint-attainment assertion of Lemma 2, choose causal populations attaining the lower endpoint under $H_{0}$ and the upper endpoint under $H_{m}$ , while preserving their respective released laws. If $W_{0}$ denotes the sharp interval length under $H_{0}$ , their ATEs differ by $W_{0} + Δ_{m}$ .

Only the score logs distinguish these endpoint-attaining experiments. Direct calculation gives $χ^{2} (H_{m}, H_{0}) = 3 u_{m}^{2} ∥ h ∥_{2}^{2} = \frac{lo g L _{α}}{m} .$ For product laws, $1 + χ^{2}$ raises to the sample-size power; Cauchy–Schwarz then bounds total variation by half the square root of $χ^{2}$ . Using $(1 + x / m)^{m} \leq e^{x}$ , the joint experiments consequently satisfy, uniformly in $n$ , $TV (Q_{0}^{n, m}, Q_{m}^{n, m}) \leq \frac{1}{2} (1 + \frac{lo g L _{α}}{m})^{m} - 1 \leq \frac{1}{2} L_{α} - 1 = \frac{β}{2} .$ For any honest interval, transfer coverage of the second ATE to the first experiment and intersect it with coverage of the first ATE. The intersection has first-experiment probability at least $1 - 2 α - TV \geq β /2$ . On it the interval length is at least $W_{0} + Δ_{m}$ . Taking the supremum over laws and the infimum over honest procedures gives, for every $n \geq 1$ and all sufficiently large $m$ , $R_{n, m, α}^{⋆} (g) \geq \frac{β Δ _{m}}{2} = \frac{β lo g L _{α}}{2 3 m} \frac{( e _{3} - e _{2} ) ( 1 - e _{1} / e _{2} )}{D ( e _{1} , e _{2} , e _{3} )} .$

To pass from a fixed triple to $S_{g}$ , take any number below $β lo g L_{α} S_{g} / (23)$ . The definition of the supremum supplies a triple whose displayed coefficient exceeds that number. Its eventual lower bound holds uniformly over $n \geq 1$ . The infimum over $n$ is finite: it is bounded below by this eventual certificate and above by the choice $n = m$ , for which $b_{m, m} = m /2$ and the bound $T_{m, m, α} (g) \leq M$ gives $m R_{m, m, α}^{⋆} (g) \leq 2 M$ . Taking the liminf and then letting the chosen number increase to the supremum proves $m \to \infty lim inf n \geq 1 in f m R_{n, m, α}^{⋆} (g) \geq c_{log} (g, α) .$

For the trial certificate, take $H = δ_{1/2}$ , which is supported on $E$ by Assumption 1. Let $P_{0}$ have $Y_{0} = 0$ and an independent Bernoulli $(1/2)$ outcome $Y_{1}$ , and let $P_{1}$ replace its success probability by $1/2 + v_{n}$ , where $v_{n} = \frac{1}{2} \frac{lo g L _{α}}{n} .$ Both laws use treatment probability $E = 1/2$ , consistency, and the fixed release $g (1/2)$ . Since $0 < β < 1$ and $n \geq 1$ , $0 < v_{n} < 1/2$ ; both pairs belong to Definition 16. The fixed score makes the reciprocal treatment weights constant, so Definitions 6 and 7 give singleton sharp intervals at $1/2$ and $1/2 + v_{n}$ .

For a latent Bernoulli outcome, the chi-squared divergence between these two success probabilities is $4 v_{n}^{2}$ . Adding the common randomized arm, releasing the trial row, and adding the common score log cannot increase total variation. Hence $TV (Q_{0}^{n, m}, Q_{1}^{n, m}) \leq \frac{1}{2} (1 + 4 v_{n}^{2})^{n} - 1 \leq \frac{1}{2} e^{l o g L_{α}} - 1 = \frac{β}{2},$ where the middle inequality uses $(1 + lo g L_{α} / n)^{n} \leq L_{α}$ . Under the first experiment, honesty and transfer of the second coverage event put both ATEs in any honest interval with probability at least $β /2$ . Its length on that event is at least $v_{n}$ , while the first sharp interval has length zero. Thus every honest procedure has worst-case expected excess length at least $\frac{β v _{n}}{2} = \frac{β lo g L _{α}}{4 n} = \frac{c _{tr} ( α )}{n} .$ The full interval $[- 1, 1]$ is honest, so the infimum defining the minimax risk is over a nonempty set; every candidate satisfies the displayed bound. This proves the finite-sample assertion.

Finally, for positive $n, m$ , multiplying the trial bound by $b_{n, m}$ gives $T_{n, m, α} (g) \geq c_{tr} (α) \frac{m}{n + m} .$ If $n, m \to \infty$ with $n / m \to ρ > 0$ , the fraction tends to $1/ (1 + ρ)$ . For the log bound, let any $γ < c_{log} (g, α)$ be fixed. The preceding liminf inequality implies, eventually in $m$ , uniformly over $n \geq 1$ , $R_{n, m, α}^{⋆} (g) \geq γ / m$ . Hence eventually $T_{n, m, α} (g) \geq γ \frac{n}{n + m} ⟶ γ \frac{ρ}{1 + ρ} .$ The uniform bound $T_{n, m, α} (g) \leq M$ makes the normalized liminf finite. Letting $γ$ increase to $c_{log} (g, α)$ and combining the two lower bounds yields $n, m \to \infty n / m \to ρ lim inf T_{n, m, α} (g) \geq max {\frac{c _{tr} ( α )}{1 + ρ}, \frac{c _{log} ( g , α ) ρ}{1 + ρ}} > 0,$ as required.

∎

The trial bound applies at every pair of positive sample sizes. The score-log bound persists when trial size is unrestricted, and the final bound records both contributions at a fixed positive sample-size ratio. These bounds provide the lower-risk component of Theorem 7.

Verification scope

The displayed theorem and lemma declarations and their rendered proofs are machine-checked with Lean 4.33.0 at source commit 9135ac11b7d3e6ebd997f8c56bc48396dde396e4. The machine-readable manifest verification_contract.json maps each paper object identifier to its Lean declaration, source file, statement and proof audits, external dependencies, and sorry-free status. It records 44 displayed objects and 82 referenced Lean declarations. Objects marked matched have a checked formal counterpart; synthesized presentation definitions organize notation and are identified separately in that manifest. The fixed-law result is credited to Fan et al. (2014) as prior mathematics, while Lemma 2 has no external formal dependency and its present proof is checked under the displayed assumptions.

Proofs of the main results

Proof of Theorem 1.

Suppose $P \in M (H, g, P_{rel})$ . For each label $r$ , score-based assignment, deterministic release, and the score marginal give the treated-arm identity $P_{rel} (A = 1, R = r) = P (A = 1, g (E) = r) = E_{P} [1 {g (E) = r} p_{1} (E)] = \int_{C_{r}} e H (d e) = q_{1 r} .$ This is the treated-arm instance of Lemma 1; the arm-cell quantities are defined in Definition 5. The score marginal and deterministic release also give $P_{rel} (R = r) = P (g (E) = r) = H (C_{r}) .$ Partitioning the label event by arm therefore yields the control-arm identity $P_{rel} (A = 0, R = r) = P_{rel} (R = r) - P_{rel} (A = 1, R = r) = H (C_{r}) - \int_{C_{r}} e H (d e) = \int_{C_{r}} (1 - e) H (d e) = q_{0 r} .$ Thus $P_{rel} (A = a, R = r) = q_{a r}$ for both arms.

Since $p_{0} (e) + p_{1} (e) = 1$ , summing the arm masses gives $P_{rel} (R = r) = a \in A \sum P_{rel} (A = a, R = r) = a \in A \sum q_{a r} = \int_{C_{r}} 1 H (d e) = H (C_{r}) .$ The treated-arm identity above is the second required equality.

Conversely, suppose the two stated equalities hold for every $r$ . Partitioning each label event by arm and using $p_{0} = 1 - p_{1}$ yields $P_{rel} (A = 0, R = r) = P_{rel} (R = r) - P_{rel} (A = 1, R = r) = H (C_{r}) - \int_{C_{r}} e H (d e) = \int_{C_{r}} (1 - e) H (d e) = q_{0 r} .$ The assumed treated equality is $P_{rel} (A = 1, R = r) = q_{1 r}$ . Thus $P_{rel} (A = a, R = r) = q_{a r}$ for both arms and every label.

For every $(a, r) \in A \times R_{J}$ , define a probability law on the outcome interval by $F_{a r}^{⋆} (U) := {P_{rel} (Y \in U ∣ A = a, R = r), 1 {0 \in U}, P_{rel} (A = a, R = r) > 0, P_{rel} (A = a, R = r) = 0, U \subseteq [0, 1] Borel .$ On positive-mass pairs this is $F_{a r}$ from Definition 5; on zero-mass pairs it is point mass at zero. In particular, for every Borel outcome set $U$ , $P_{rel} (Y \in U, A = a, R = r) = P_{rel} (A = a, R = r) F_{a r}^{⋆} (U) = q_{a r} F_{a r}^{⋆} (U) .$ Define a law for the latent variables by $Λ (d e, d y_{0}, d y_{1}) = H (d e) F_{0, g (e)}^{⋆} (d y_{0}) F_{1, g (e)}^{⋆} (d y_{1}) .$ Its score marginal is $H$ , and its two potential outcomes are conditionally independent given the score. The finite label alphabet and measurability of $g$ make these kernels measurable.

From $Λ$ , construct $P$ by drawing $A$ conditionally on $(E, Y_{0}, Y_{1})$ with probabilities $p_{a} (E)$ , then setting $R = g (E)$ and $Y = A Y_{1} + (1 - A) Y_{0}$ . Equivalently, in the full-row coordinate order $(E, Y_{0}, Y_{1}, A, Y, R)$ , its law is $P = a \in A \sum ((e, y_{0}, y_{1}) \mapsto (e, y_{0}, y_{1}, a, a y_{1} + (1 - a) y_{0}, g (e)))_{#} (p_{a} (e) Λ (d e, d y_{0}, d y_{1})) .$ Overlap gives $0 \leq p_{a} (e) \leq 1$ , and $p_{0} (e) + p_{1} (e) = 1, P (E \in S) = \int_{S} a \in A \sum p_{a} (e) H (d e) = H (S)$ for every Borel score set $S$ . Hence $P$ is a probability law with score marginal $H$ . Its conditional assignment probabilities are $p_{a} (E)$ , while consistency and deterministic release hold by construction.

Finally, for every $a, r, U$ as above, $P (R = r, A = a, Y \in U) = \int_{C_{r}} p_{a} (e) F_{a r}^{⋆} (U) H (d e) = q_{a r} F_{a r}^{⋆} (U) = P_{rel} (R = r, A = a, Y \in U) .$ These events determine the law of $(R, A, Y)$ , including zero-mass cells. Thus its law under $P$ is $P_{rel}$ , and $P \in M (H, g, P_{rel})$ .

∎

Proof of Theorem 2.

Step 1 (general upper bound). For each arm and label, define $Γ_{a r} := c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - c p_{a} (e) ∣ H (d e), Γ_{all} := r \in R_{J} \sum (Γ_{1 r} + Γ_{0 r}) .$ Consider any causal law $P$ in the supremum defining $D_{H} (g)$ , and set $P_{rel} := L_{P} (R, A, Y) .$ For a cell with $q_{a r} > 0$ , let $F_{a r}$ be its observed outcome law under $P_{rel}$ , and define its contribution to the interval width by $Δ_{a r} (P_{rel}) := q_{a r} \int_{0}^{1} Q_{F_{a r}} (u) {Q_{W_{a r}} (u) - Q_{W_{a r}} (1 - u)} d u .$ Set $Δ_{a r} (P_{rel}) = 0$ when $q_{a r} = 0$ . By Lemma 2 and the definitions of the mean endpoints, $len I (P_{rel}; H, g) = r \in R_{J} \sum {Δ_{1 r} (P_{rel}) + Δ_{0 r} (P_{rel})} .$

Fix a positive-mass cell and $c \in [1/ (1 - ε), 1/ ε]$ . Since $0 \leq Q_{F_{a r}} (u) \leq 1$ almost everywhere, the positive and negative parts give $\int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (u) d u \int_{0}^{1} Q_{F_{a r}} (u) Q_{W_{a r}} (1 - u) d u \leq c \int_{0}^{1} Q_{F_{a r}} (u) d u + \int_{0}^{1} (Q_{W_{a r}} (u) - c)_{+} d u, \geq c \int_{0}^{1} Q_{F_{a r}} (u) d u - \int_{0}^{1} (c - Q_{W_{a r}} (1 - u))_{+} d u .$ The quantiles at $u$ and $1 - u$ each have law $W_{a r}$ under uniform $u$ . Subtraction therefore yields $\frac{Δ _{a r} ( P _{rel} )}{q _{a r}} \leq E ∣ W_{a r} - c ∣.$ The defining score law of $E_{a r}$ and $p_{a} (e) > 0$ give the scaling identity $q_{a r} E ∣ W_{a r} - c ∣ = \int_{C_{r}} p_{a} (e) \frac{1}{p _{a} ( e )} - c H (d e) = \int_{C_{r}} ∣1 - c p_{a} (e) ∣ H (d e) .$ Taking the infimum shows $Δ_{a r} (P_{rel}) \leq Γ_{a r}$ . If $q_{a r} = 0$ , then $H (C_{r}) = 0$ , since $p_{a} (e) \geq ε > 0$ on $E$ ; hence both sides are zero. Summing over all cells proves $len I (P_{rel}; H, g) \leq Γ_{all}, D_{H} (g) \leq Γ_{all} .$

Step 2 (width of the half-outcome release). For the $P_{rel}$ in the statement, every positive-mass cell has outcome law Bernoulli $(1/2)$ , whose quantile is zero below $1/2$ and one above $1/2$ , up to a null set. Put $m_{a r} := Q_{W_{a r}} (1/2)$ in such a cell. Monotonicity of the quantile and a change of variable give $\frac{Δ _{a r} ( P _{rel} )}{q _{a r}} = \int_{1/2}^{1} Q_{W_{a r}} (u) d u - \int_{0}^{1/2} Q_{W_{a r}} (u) d u = \int_{0}^{1} ∣ Q_{W_{a r}} (u) - m_{a r} ∣ d u = E ∣ W_{a r} - m_{a r} ∣.$ Overlap places $W_{a r}$ , and thus its median $m_{a r}$ , in $[1/ (1 - ε), 1/ ε]$ . The preceding cellwise bound applies to this fair outcome law for every admissible $c$ , while $m_{a r}$ attains that bound. The scaling identity consequently gives $Δ_{a r} (P_{rel}) = q_{a r} c \in [1/ (1 - ε), 1/ ε] in f E ∣ W_{a r} - c ∣ = Γ_{a r} .$ The equality also holds in zero-mass cells by the zero-mass argument above. Summing the armwise contributions yields $len I (P_{rel}; H, g) = Γ_{all} .$

Step 3 (compatible laws and endpoints). The cell masses satisfy $r \in R_{J} \sum a \in {0, 1} \sum q_{a r} = \int_{E} (p_{1} (e) + p_{0} (e)) H (d e) = 1.$ Thus $P_{rel}$ is a probability law. For every label $r$ , its defining mixture gives $P_{rel} (R = r) = q_{1 r} + q_{0 r} = H (C_{r}), P_{rel} (A = 1, R = r) = q_{1 r} = \int_{C_{r}} e H (d e) .$ By Theorem 1, there is a compatible full law producing $P_{rel}$ . Applying Lemma 2 to this released law gives compatible probability laws $P_{-}, P_{+}$ with $E_{P_{-}} [Y_{1} - Y_{0}] = \underline{μ}_{1} - \overline{μ}_{0}, E_{P_{+}} [Y_{1} - Y_{0}] = \overline{μ}_{1} - \underline{μ}_{0},$ and hence $E_{P_{+}} [Y_{1} - Y_{0}] - E_{P_{-}} [Y_{1} - Y_{0}] = len I (P_{rel}; H, g) = Γ_{all} .$

Step 4 (supremum and conclusion). The set of widths in Definition 9 is bounded above by $Γ_{all}$ , by the general upper bound. The compatible law constructed for $P_{rel}$ puts its width in that set, and the half-outcome calculation shows that this width equals $Γ_{all}$ . Therefore $D_{H} (g) = Γ_{all} = r \in R_{J} \sum [c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - ce ∣ H (d e) + c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - c (1 - e) ∣ H (d e)] .$ Substituting this equality into the attained endpoint gap above proves the asserted gap. The hypotheses also cover the index-set boundary: $E$ contains $ε$ , so the value $g (ε)$ ensures $R_{J}$ is nonempty.

∎

Proof of Theorem 3.

For $a \in {0, 1}$ and $r \in R_{J}$ , set $δ_{a r} := c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - c p_{a} (e) ∣ H (d e), p_{1} (e) = e, p_{0} (e) = 1 - e .$ The coefficient interval is nonempty under overlap. Each defining integral is finite and nonnegative, so $δ_{a r} \geq 0$ . By Theorem 2, $D_{H} (g) = r \in R_{J} \sum (δ_{1 r} + δ_{0 r}) .$ Thus $D_{H} (g) = 0$ implies $δ_{1 r} = 0$ for every $r$ : each term in this finite sum is nonnegative.
Fix $r$ with $H (C_{r}) > 0$ , and define, for every real $t$ , $Φ_{r} (t) := \int_{C_{r}} ∣1 - t e ∣ H (d e) .$ Since $0 \leq e \leq 1$ on $E$ , for all real $t, t^{'}$ , $∣ Φ_{r} (t) - Φ_{r} (t^{'}) ∣ \leq \int_{C_{r}} ∣ t - t^{'} ∣ e H (d e) \leq ∣ t - t^{'} ∣ H (C_{r}) \leq ∣ t - t^{'} ∣.$ Hence $Φ_{r}$ is continuous and attains its minimum on the compact coefficient interval. Let $c_{r}$ attain it. The preceding step gives $0 = δ_{1 r} = Φ_{r} (c_{r}) = \int_{C_{r}} ∣1 - c_{r} e ∣ H (d e),$ so $1 - c_{r} e = 0$ for $H$ -almost every $e \in C_{r}$ . Because $H (C_{r}) > 0$ , there is an $x_{r} \in C_{r}$ with $1 - c_{r} x_{r} = 0$ . Also $c_{r} \geq 1/ (1 - ε) > 0$ . Consequently, $c_{r} (e - x_{r}) = 0 for H -almost every e \in C_{r},$ and therefore $e = x_{r}$ there almost surely. This proves the cellwise condition.
Conversely, suppose the cellwise condition holds. Choose its value $x_{r}$ on each positive-mass cell and define the map on the entire label set by $h (r) := {x_{r}, ε, H (C_{r}) > 0, H (C_{r}) = 0, r \in R_{J} .$ Here $ε \in E$ by overlap. The finite label set makes $h$ measurable. On every positive-mass cell, $e = h (r)$ almost surely; the same assertion is vacuous on a zero-mass cell. Taking the finite union of these cellwise assertions yields $e = h (g (e)) for H -almost every e .$
For every $a \in {0, 1}$ and $r \in R_{J}$ , set $c_{a r} := \frac{1}{p _{a} ( h ( r ))} .$ Overlap gives $ε \leq p_{a} (h (r)) \leq 1 - ε, \frac{1}{1 - ε} \leq c_{a r} \leq \frac{1}{ε} .$ The cellwise equality established above gives $p_{a} (e) = p_{a} (h (r))$ almost surely on $C_{r}$ , including when that cell has zero mass. Thus $0 \leq δ_{a r} \leq \int_{C_{r}} ∣1 - c_{a r} p_{a} (e) ∣ H (d e) = 0.$ Every summand in the all-label formula is zero, and hence $D_{H} (g) = 0$ . Finally, if a measurable $h$ satisfies $e = h (g (e))$ $H$ -almost surely, then on each positive-mass $C_{r}$ its value $h (r)$ witnesses the cellwise condition. The two stated conditions are therefore each equivalent to $D_{H} (g) = 0$ .

∎

Proof of Theorem 4.

The overlap condition gives $ℓ > 0$ . First fix $H \in H_{ε, m_{f}}^{lb}$ and an arbitrary measurable $g \in G_{K}$ . For each label $r$ , set $C_{r} = {e \in E : g (e) = r}, h_{r} = Leb (C_{r}) .$ The measurable cells partition $E$ , including any empty cells, so $h_{r} \geq 0$ and $\sum_{r} h_{r} = ℓ$ .

For every $ζ \in R$ and $t \geq 0$ , the points within distance $t$ of $ζ$ occupy an interval of length $2 t$ . Thus $Leb {e \in C_{r} : ∣ e - ζ ∣ > t} \geq h_{r} - 2 t,$ and the layer-cake identity gives $\int_{C_{r}} ∣ e - ζ ∣ d e \geq \int_{0}^{h_{r} /2} (h_{r} - 2 t) d t = \frac{h _{r}^{2}}{4} .$

Since $H (d e) = f (e) d e$ with $f \geq m_{f}$ almost everywhere, it follows for every $ζ \in R$ that $\int_{C_{r}} ∣ e - ζ ∣ H (d e) \geq m_{f} \int_{C_{r}} ∣ e - ζ ∣ d e \geq \frac{m _{f} h _{r}^{2}}{4} .$

Write $p_{1} (e) = e$ and $p_{0} (e) = 1 - e$ , as in Theorem 2. For any $c \in [1/ (1 - ε), 1/ ε]$ , define the two score centers by $z_{1, c} = c^{- 1}, z_{0, c} = 1 - c^{- 1} .$ Here $c > 0$ , and direct algebra gives $∣1 - c p_{a} (e) ∣ = c ∣ e - z_{a, c} ∣, a \in {0, 1} .$

Because $c \geq 1/ (1 - ε)$ , the preceding cell bound yields, for either arm, $\int_{C_{r}} ∣1 - c p_{a} (e) ∣ H (d e) \geq \frac{m _{f} h _{r}^{2}}{4 ( 1 - ε )} .$

By the exact cell formula in Theorem 2, $D_{H} (g) = r \sum a \in {0, 1} \sum c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - c p_{a} (e) ∣ H (d e) \geq \frac{m _{f}}{2 ( 1 - ε )} r \sum h_{r}^{2} .$

There are $K$ labels, so Cauchy–Schwarz gives $r \sum h_{r}^{2} \geq \frac{( \sum _{r} h _{r} ) ^{2}}{K} = \frac{ℓ ^{2}}{K} .$ Consequently every $g \in G_{K}$ satisfies $D_{H} (g) \geq \frac{m _{f} ℓ ^{2}}{2 ( 1 - ε ) K} .$ The class $G_{K}$ is nonempty because $K \geq 1$ permits a constant measurable release. Taking the infimum as in Definition 11 proves the lower bound for $Δ_{K} (H)$ .

Now let $H$ be any probability law on $E$ , and take the equal-width release $g$ in the statement. It is measurable: the score transformation inside the floor is continuous, the floor is measurable, and clipping its value to the finite label set preserves measurability.

Index its labels by $r = 1, \dots, K$ , write $C_{r} = {e \in E : g (e) = r}$ , and define $z_{r} = ε + (r - \frac{1}{2}) \frac{ℓ}{K} .$ For $e \in C_{r}$ , the floor rule places $e$ between $ε + (r - 1) ℓ / K$ and $ε + r ℓ / K$ . At the right endpoint of $E$ , clipping assigns the last label, for which the same closed bounds hold. Hence $z_{r} \in E$ and $∣ e - z_{r} ∣ \leq \frac{ℓ}{2 K} (e \in C_{r}) .$

The candidates $z_{r}^{- 1}$ and $(1 - z_{r})^{- 1}$ lie in $[1/ (1 - ε), 1/ ε]$ . Moreover, $z_{r} (1 - z_{r}) - ε (1 - ε) = (z_{r} - ε) (1 - ε - z_{r}) \geq 0.$ Thus, for $e \in C_{r}$ , $1 - \frac{e}{z _{r}} + 1 - \frac{1 - e}{1 - z _{r}} = \frac{∣ e - z _{r} ∣}{z _{r} ( 1 - z _{r} )} \leq \frac{∣ e - z _{r} ∣}{ε ( 1 - ε )} .$

Using these candidates in the two cell infima, then applying the midpoint bound, gives $a \in {0, 1} \sum c \in [1/ (1 - ε), 1/ ε] in f \int_{C_{r}} ∣1 - c p_{a} (e) ∣ H (d e) \leq \frac{1}{ε ( 1 - ε )} \int_{C_{r}} ∣ e - z_{r} ∣ H (d e) \leq \frac{ℓ}{2 ε ( 1 - ε ) K} H (C_{r}) .$

The cells partition $E$ and $H (E) = 1$ . Summing the cell bounds therefore yields $D_{H} (g) \leq \frac{ℓ}{2 ε ( 1 - ε ) K} r \sum H (C_{r}) = \frac{ℓ}{2 ε ( 1 - ε ) K} .$

Finally, the exact cell formula shows $D_{H} (g^{'}) \geq 0$ for every measurable release $g^{'}$ , while the measurable $g$ above belongs to $G_{K}$ . Hence the defining infimum satisfies $Δ_{K} (H) \leq D_{H} (g) \leq \frac{ℓ}{2 ε ( 1 - ε ) K} .$

∎

Proof of Theorem 5.

By Assumption 1, $E$ is a nondegenerate compact interval and $e, 1 - e \geq ε > 0$ throughout $E$ . Continuity and strict positivity give $0 < e \in E min f (e) \leq e \in E max f (e) < \infty.$

For $x, z \in E$ , define the two distortion coefficients $β_{1} (x, z) = \frac{f ( x )}{z}, β_{0} (x, z) = \frac{f ( x )}{1 - z} .$ Both are continuous and strictly positive on $E^{2}$ . Their diagonal weight is $w (x) := β_{0} (x, x) + β_{1} (x, x) = \frac{f ( x )}{x ( 1 - x )} .$ Thus Lemma 3 applies with two components. In particular, if $V_{K}$ denotes its optimal paired cost for these coefficients, then $K V_{K} ⟶ \frac{1}{4} (\int_{ε}^{1 - ε} \frac{f ( x )}{x ( 1 - x )} d x)^{2} .$

We identify this paired cost with the release objective. Fix $K > 0$ and a measurable release $g : E \to {0, \dots, K - 1}$ , and put $C_{r} = {x \in E : g (x) = r}$ . For centers $z = (z_{r, a})_{r, a} \in E^{{0, \dots, K - 1} \times {0, 1}}$ , define $Φ_{K} (g, z) := r = 0 \sum K - 1 a = 0 \sum 1 \int_{C_{r}} β_{a} (x, z_{r, a}) ∣ x - z_{r, a} ∣ d x .$ The changes of variables $z_{r, 1} = c^{- 1}$ and $z_{r, 0} = 1 - c^{- 1}$ each map the coefficient range in Theorem 2 bijectively onto $E$ , and give $f (x) ∣1 - c x ∣ = β_{1} (x, z_{r, 1}) ∣ x - z_{r, 1} ∣, f (x) ∣1 - c (1 - x) ∣ = β_{0} (x, z_{r, 0}) ∣ x - z_{r, 0} ∣.$ The cellwise infima are independent. Each has a nonempty set of feasible values bounded below by zero, including when its cell is empty. Hence Theorem 2 yields $D_{H} (g) = z in f Φ_{K} (g, z) .$ Taking the infimum over releases flattens these independent choices. Their cells are measurable, pairwise disjoint, and cover $E$ ; conversely, every such $K$ -cell partition defines a measurable release by assigning its cell indices as labels. Empty cells are allowed in both descriptions. Therefore Definition 11 gives the exact identity $Δ_{K} (H) = g \in G_{K} in f z in f Φ_{K} (g, z) = V_{K} .$ It follows that $K Δ_{K} (H) ⟶ \frac{1}{4} (\int_{ε}^{1 - ε} \frac{f ( x )}{x ( 1 - x )} d x)^{2} .$

To construct the releases, set $A_{H} := \int_{ε}^{1 - ε} w (x) d x .$ For each $K > 0$ , choose boundaries $t_{0, K}, \dots, t_{K, K}$ by $t_{0, K} = ε, t_{K, K} = 1 - ε, \int_{ε}^{t_{j, K}} w (x) d x = \frac{j}{K} A_{H} (0 \leq j \leq K) .$ Positivity of $w$ makes these boundaries strictly increasing. Let $g_{K}$ assign label $j$ to $[t_{j, K}, t_{j + 1, K})$ for $j < K - 1$ , and label $K - 1$ to $[t_{K - 1, K}, t_{K, K}]$ . Put $ζ_{j, K} := \frac{t _{j, K} + t _{j + 1, K}}{2}, U_{K} := Φ_{K} (g_{K}, z) with z_{j, 0} = z_{j, 1} = ζ_{j, K} .$ The construction clause of Lemma 3 ensures that these cells form a measurable partition, that every midpoint lies in $E$ , and that $K U_{K} ⟶ \frac{1}{4} A_{H}^{2} .$

For every $K > 0$ , optimality over releases gives the lower bound, while the chosen centers give a feasible value for each cellwise infimum: $Δ_{K} (H) \leq D_{H} (g_{K}) = z in f Φ_{K} (g_{K}, z) \leq U_{K} .$ Multiplication by $K \geq 0$ preserves both inequalities. At $K = 0$ , assign zero to the two auxiliary scaled quantities; both bounds then read $0 \leq 0 \leq 0$ . The two established limits squeeze $K D_{H} (g_{K})$ to $\frac{1}{4} A_{H}^{2}$ .

Finally, each displayed cell of $g_{K}$ is an interval and is measurable. If $x, z$ carry the same label and $x \leq y \leq z$ , that interval also contains $y$ ; thus the label cells have the asserted interval property.

∎

Proof of Theorem 6.

Put $ℓ = 1 - 2 ε, β = 1 - 2 α, B_{α} = \frac{β lo g ( 1 + β ^{2} )}{4}, U_{ε, α} = \frac{ℓ}{ε ( 1 - ε )} + \frac{8}{ε} lo g (4/ α), C_{ε, α} = max {B_{α}, U_{ε, α}} .$ The overlap and miscoverage conditions give $ℓ > 0$ , $β > 0$ , and $B_{α} > 0$ ; hence $C_{ε, α} > 0$ .

First fix any probability score law $H$ , any $n, K \geq 1$ , and any honest pair $(g, C_{n})$ . Set $u_{n} = \frac{1}{2} \frac{lo g ( 1 + β ^{2} )}{n} .$ Construct two causal laws $P^{(0)}, P^{(1)}$ as follows. Under both, $E \sim H$ , $Y_{0} = 0$ , $R = g (E)$ , and, conditional on the latent variables, $A$ is Bernoulli with parameter $E$ . Independently of $E$ , take $Y_{1}$ to be Bernoulli with parameter $1/2$ under $P^{(0)}$ and $1/2 + u_{n}$ under $P^{(1)}$ ; set $Y = A Y_{1} + (1 - A) Y_{0}$ . Since $0 < u_{n} < 1/2$ , both laws belong to $P (H, g)$ of Definition 1, and their average treatment effects are $1/2$ and $1/2 + u_{n}$ .

Let $Q_{j}$ be the released $n$ -row law under $P^{(j)}$ , for $j = 0, 1$ . The released rows are measurable functions of Bernoulli potential outcomes and a common, independent score-and-assignment design. Total variation contracts under this readout. The chi-squared divergence of Bernoulli $(1/2 + u_{n})$ from Bernoulli $(1/2)$ is $4 u_{n}^{2}$ ; its product-law identity and Cauchy–Schwarz therefore give $TV (Q_{0}, Q_{1}) \leq \frac{1}{2} (1 + 4 u_{n}^{2})^{n} - 1 .$ Writing $x = lo g (1 + β^{2})$ , we have $4 u_{n}^{2} = x / n$ , so $(1 + x / n)^{n} \leq e^{x} = 1 + β^{2}$ . Consequently, $TV (Q_{0}, Q_{1}) \leq \frac{β}{2} .$ The two coverage events have probabilities at least $1 - α$ under their respective laws. Transferring the second event to $Q_{0}$ and intersecting the events shows that, with $Q_{0}$ -probability at least $1 - 2 α - TV (Q_{0}, Q_{1}) \geq β /2$ , the interval contains both treatment effects. Its length is then at least $u_{n}$ . Thus $P \in P (H, g) sup E_{P_{rel}^{\otimes n}} ∣ C_{n} ∣ \geq E_{Q_{0}} ∣ C_{n} ∣ \geq \frac{β u _{n}}{2} = B_{α} n^{- 1/2} .$

This bound holds for every honest pair. The collection of such pairs is nonempty: a constant release paired with the interval $[- 1, 1]$ is honest. Their expected lengths lie in $[0, 2]$ . Taking the infimum as in Definition 15 yields $B_{α} n^{- 1/2} \leq L_{n, K, α}^{⋆} (H) .$

Now suppose $H \in H_{ε, m_{f}}^{lb}$ , where $m_{f} > 0$ . By Definition 12, $H (d e) = f (e) d e$ with $f \geq m_{f}$ almost everywhere. Fix an arbitrary $g \in G_{K}$ , and write $C_{r} = {e \in E : g (e) = r}, h_{r} = Leb (C_{r}), r \in R_{K} .$ These measurable cells partition $E$ , including when some are empty or disconnected, so $\sum_{r} h_{r} = ℓ$ . For $c \in [1/ (1 - ε), 1/ ε]$ , put $z_{1, c} = c^{- 1}, z_{0, c} = 1 - c^{- 1} .$ Both centers lie in $E$ . With $p_{1} (e) = e$ and $p_{0} (e) = 1 - e$ , as in Theorem 2, for either arm $a$ we have $\int_{C_{r}} ∣1 - c p_{a} (e) ∣ H (d e) = c \int_{C_{r}} ∣ e - z_{a, c} ∣ H (d e) \geq \frac{m _{f}}{1 - ε} \int_{C_{r}} ∣ e - z_{a, c} ∣ d e .$

Here is the geometric bound used for each cell. For any measurable set $V$ of finite Lebesgue measure $h$ and any real $z$ , the interval ${∣ e - z ∣ \leq t}$ has measure at most $2 t$ . The layer-cake identity gives, also when $h = 0$ , $\int_{V} ∣ e - z ∣ d e = \int_{0}^{\infty} Leb {e \in V : ∣ e - z ∣ > t} d t \geq \int_{0}^{h /2} (h - 2 t) d t = \frac{h ^{2}}{4} .$ Applying this with $V = C_{r}$ bounds each arm’s infimum in the exact ambiguity formula of Theorem 2. Since $\sum_{r} h_{r}^{2} \geq (\sum_{r} h_{r})^{2} / K = ℓ^{2} / K$ , that formula yields $D_{H} (g) \geq \frac{m _{f}}{2 ( 1 - ε )} r \sum h_{r}^{2} \geq \frac{m _{f} ℓ ^{2}}{2 ( 1 - ε ) K} .$

For this same release, Theorem 2 supplies two causal laws with a common released law and treatment effects separated by $D_{H} (g)$ . Under their common $n$ -row law, honesty makes the two coverage events intersect with probability at least $1 - 2 α$ . On that intersection, the interval has length at least $D_{H} (g)$ . Hence every honest $(g, C_{n})$ satisfies $P \in P (H, g) sup E_{P_{rel}^{\otimes n}} ∣ C_{n} ∣ \geq (1 - 2 α) D_{H} (g) \geq A_{ε, m_{f}, α} K^{- 1}, A_{ε, m_{f}, α} := \frac{( 1 - 2 α ) m _{f} ℓ ^{2}}{2 ( 1 - ε )} > 0.$ Taking the infimum over honest pairs preserves this bound.

Define $c_{ε, m_{f}, α} = \frac{1}{2} min {A_{ε, m_{f}, α}, B_{α}} > 0.$ The label and sampling bounds give $c_{ε, m_{f}, α} (K^{- 1} + n^{- 1/2}) \leq max {A_{ε, m_{f}, α} K^{- 1}, B_{α} n^{- 1/2}} \leq L_{n, K, α}^{⋆} (H) .$

For the upper bound, use the equal-width release and midpoints in the statement. Its endpoint convention assigns every $e \in E$ a label and gives $z_{g_{K} (e)} \in [ε, 1 - ε], ∣ e - z_{g_{K} (e)} ∣ \leq \frac{ℓ}{2 K} .$ Fix $P \in P (H, g_{K})$ , and choose conditional means $η_{a} (e) = E_{P} [Y_{a} ∣ E = e] \in [0, 1], a \in {0, 1} .$ The score-based assignment and consistency conditions in Definition 1 give $E_{P_{rel}^{\otimes n}} T_{n} θ (P) = \int_{E} {\frac{e η _{1} ( e )}{z _{g_{K} (e)}} - \frac{( 1 - e ) η _{0} ( e )}{1 - z _{g_{K} (e)}}} H (d e), = \int_{E} {η_{1} (e) - η_{0} (e)} H (d e) .$ Subtracting and using $z (1 - z) \geq ε (1 - ε)$ on the score interval gives $E_{P_{rel}^{\otimes n}} T_{n} - θ (P) E_{P_{rel}^{\otimes n}} T_{n} - θ (P) = \int_{E} (e - z_{g_{K} (e)}) {\frac{η _{1} ( e )}{z _{g_{K} (e)}} + \frac{η _{0} ( e )}{1 - z _{g_{K} (e)}}} H (d e), \leq \frac{ℓ}{2 K ε ( 1 - ε )} .$

Each summand of $T_{n}$ lies in $[- ε^{- 1}, ε^{- 1}]$ . Hoeffding’s inequality for the independent released rows, with $t_{n} = \frac{4}{ε} \frac{lo g ( 4/ α )}{n},$ therefore gives $P_{rel}^{\otimes n} (T_{n} - E_{P_{rel}^{\otimes n}} T_{n} \geq t_{n}) \leq 2 exp (- \frac{n ε ^{2} t _{n}^{2}}{2}) = 2 (α /4)^{8} \leq α .$

The radius in the statement is $R_{n, K} = t_{n} + ℓ / [2 K ε (1 - ε)]$ . Outside the displayed deviation event, the bias bound implies $∣ T_{n} - θ (P)∣ \leq R_{n, K}$ . Also $θ (P) \in [- 1, 1]$ , since $Y_{0}, Y_{1} \in [0, 1]$ . Clamping the two endpoints to $[- 1, 1]$ therefore preserves containment of $θ (P)$ . The radius is nonnegative, and the clamp is measurable and nondecreasing, so the stated endpoints form an interval for every sample. The release is measurable. As the argument holds for every $P \in P (H, g_{K})$ , $(g_{K}, C_{n}) \in J_{n, K, α} (H)$ by Definition 14.

Finally, the clamp is one-Lipschitz. Pointwise in the sample, $∣ C_{n} ∣ \leq 2 R_{n, K} = \frac{ℓ}{ε ( 1 - ε )} K^{- 1} + \frac{8}{ε} lo g (4/ α) n^{- 1/2} \leq U_{ε, α} (K^{- 1} + n^{- 1/2}) .$ Integrating under every released $n$ -row law gives the asserted expected-length bound with $C_{ε, α} \geq U_{ε, α}$ . Taking the supremum over causal laws and the infimum over honest pairs also gives $L_{n, K, α}^{⋆} (H) \leq C_{ε, α} (K^{- 1} + n^{- 1/2}) .$ Together with the two lower bounds, this proves the claims.

∎

Proof of Theorem 7.

Step 1: Lower certificates. Lemma 4 gives $0 < S_{g} \leq 1$ , the trial and score-log lower bounds, and the stated lower bound on the normalized risk. It also gives $c_{log} (g, α) > 0$ . We construct an interval attaining the upper bound.

Step 2: Empirical distances and endpoint stability. Fix positive $n, m$ and an admissible pair $(P, H)$ . For each arm $a$ and label $r$ , define the population finite measures $λ_{a r} (B) = P (R = r, A = a, Y \in B), B \subseteq [0, 1], σ_{a r} (B) = \int_{B \cap C_{r}} p_{a} (e) H (d e), B \subseteq E .$ Their total masses agree by the score-marginal, assignment, and release conditions. For finite measures $ξ, ξ^{'}$ on a compact interval $I$ , write $d_{I} (ξ, ξ^{'}) = ∣ ξ (I) - ξ^{'} (I) ∣ + \int_{I} ∣ F_{ξ} (t) - F_{ξ^{'}} (t) ∣ d t, F_{ξ} (t) = ξ ((- \infty, t]) .$ For a joint sample $ω$ , set $D_{Y} (ω) = a, r \sum d_{[0, 1]} (λ_{a r} (ω), λ_{a r}), D_{E} (ω) = a, r \sum d_{E} (σ_{a r} (ω), σ_{a r}) .$ The empirical measures are those of Definition 22. Each empirical cumulative mass, including its total mass, is an average of independent variables in $[0, 1]$ . Its expected absolute deviation is at most $1/ (2 n)$ for a trial cell and $1/ (2 m)$ for a score-log cell. Integrating over intervals of lengths $1$ and $1 - 2 ε$ , respectively, and summing the $2 J$ cells gives $E_{Q_{P, H}^{n, m}} D_{Y} \leq \frac{2 J}{n}, E_{Q_{P, H}^{n, m}} D_{E} \leq \frac{J ( 2 - 2 ε )}{m} .$

Here is the stability estimate used below. For compatible finite measures $ξ$ on $[0, 1]$ and $ζ$ on $E$ , let their common mass be $κ$ . When $κ > 0$ , define $Ψ_{a}^{-} (ξ, ζ) = κ \int_{0}^{1} Q_{ξ / κ} (u) Q_{(p_{a}^{- 1})_{#} (ζ / κ)} (1 - u) d u, Ψ_{a}^{+} (ξ, ζ) = κ \int_{0}^{1} Q_{ξ / κ} (u) Q_{(p_{a}^{- 1})_{#} (ζ / κ)} (u) d u;$ when $κ = 0$ , set both values to zero. For another compatible pair $(ξ^{'}, ζ^{'})$ of mass $κ^{'}$ , put $κ_{\land} = min {κ, κ^{'}}$ . Suppose first that both masses are positive. The quantile transport identity on a compact interval $I$ identifies the integral of the absolute difference of normalized quantiles with the integral of the absolute difference of normalized CDFs. If $κ \leq κ^{'}$ , then $0 \leq F_{ξ^{'}} (t) \leq κ^{'}$ gives, pointwise, $κ \frac{F _{ξ} ( t )}{κ} - \frac{F _{ξ^{'}} ( t )}{κ ^{'}} \leq ∣ F_{ξ} (t) - F_{ξ^{'}} (t) ∣ + ∣ κ - κ^{'} ∣.$ The same inequality with the pairs exchanged covers $κ^{'} \leq κ$ . Applying it to the outcome and score CDFs and integrating over supports of lengths $1$ and $1 - 2 ε$ , respectively, yields $κ_{\land} \int_{0}^{1} ∣ Q_{ξ / κ} (u) - Q_{ξ^{'} / κ^{'}} (u) ∣ d u κ_{\land} \int_{0}^{1} ∣ Q_{ζ / κ} (u) - Q_{ζ^{'} / κ^{'}} (u) ∣ d u \leq \int_{0}^{1} ∣ F_{ξ} (t) - F_{ξ^{'}} (t) ∣ d t + ∣ κ - κ^{'} ∣, \leq \int_{E} ∣ F_{ζ} (t) - F_{ζ^{'}} (t) ∣ d t + (1 - 2 ε) ∣ κ - κ^{'} ∣.$ Since $0 \leq y \leq 1$ , $p_{a} (e) \geq ε$ , and $e \mapsto p_{a} (e)^{- 1}$ is $ε^{- 2}$ -Lipschitz, the product difference in either definition of $Ψ_{a}^{\pm}$ , multiplied by $κ_{\land}$ , is bounded using [eq:external-root-order-transport] by $ε^{- 1} (\int_{0}^{1} ∣ F_{ξ} - F_{ξ^{'}} ∣ + ∣ κ - κ^{'} ∣) + ε^{- 2} (\int_{E} ∣ F_{ζ} - F_{ζ^{'}} ∣ + ∣ κ - κ^{'} ∣) .$ The remaining mass contributes at most $ε^{- 1} ∣ κ - κ^{'} ∣$ . Because both distances contain that mass difference, [eq:external-root-order-product] implies, with $Λ_{ε} = ε^{- 1} + ε^{- 2}$ , $∣ Ψ_{a}^{\pm} (ξ, ζ) - Ψ_{a}^{\pm} (ξ^{'}, ζ^{'}) ∣ \leq Λ_{ε} (d_{[0, 1]} (ξ, ξ^{'}) + d_{E} (ζ, ζ^{'})) .$ If either mass is zero, the bound $0 \leq Ψ_{a}^{\pm} (ξ, ζ) \leq ε^{- 1} κ$ and the mass term in the distance give [eq:external-root-order-stability] directly. Summing [eq:external-root-order-stability] over labels gives the same bound, with summed distances, for each arm endpoint. By Lemma 2, those endpoints at $(λ_{a r}, σ_{a r})_{a, r}$ are $\underline{μ}_{a}, \overline{μ}_{a}$ .

Step 3: Honesty and excess length. Use the interval $C_{n, m}$ of Definition 22. Its countable rational sieve and selected endpoints give measurable endpoints and a closed interval in $[- 1, 1]$ . The release $g : E \to R_{J}$ , with nonempty $E$ , also ensures $J \geq 1$ . The radii in that construction are $r_{n} = \frac{4 J}{α n}, r_{m} = \frac{2 J ( 2 - 2 ε )}{α m} .$ By [eq:external-root-order-mean], Markov’s inequality applied to the nonnegative distances gives $Q_{P, H}^{n, m} {D_{Y} < r_{n}, D_{E} < r_{m}} \geq 1 - α .$ On the strict-ball event in [eq:external-root-order-coverage], define the available slack $η_{*} = min {r_{n} - D_{Y} (ω), r_{m} - D_{E} (ω)} > 0, η_{k} = \frac{η _{*}}{k + 1} (k \geq 1) .$ For each arm-label cell, its population outcome and score measures have the same finite mass. Given $η > 0$ , choose a common nonnegative rational mass and a common positive atom count for two equal-weight atomic approximations, with outcome and score atoms on their respective dense rational grids. To see the quantitative bound, first approximate each normalized measure by equally weighted quantile atoms; increasing the common atom count makes the sum of their integrated CDF errors arbitrarily small. Moving those atoms to the rational grids preserves that convergence. If the common population mass is $κ$ and the chosen rational mass is $κ^{'}$ , changing the weight of each atom from $κ / N$ to $κ^{'} / N$ adds at most $(1 + ∣ I ∣) ∣ κ - κ^{'} ∣$ to the distance on support $I$ . Thus the combined weight error for the two supports is at most $(4 - 2 ε) ∣ κ - κ^{'} ∣$ . Choosing $κ^{'}$ sufficiently close to $κ$ gives combined cell error below any prescribed tolerance; this also covers zero mass by taking rational mass zero.

Apply this construction in every cell with tolerance $η_{k} / [2 (J + 1)]$ . Since there are $2 J$ cells, it gives a compatible rational array $b_{k}$ satisfying $a, r \sum (d_{[0, 1]} (λ_{a r}, λ_{a r} (b_{k})) + d_{E} (σ_{a r}, σ_{a r} (b_{k}))) < \frac{2 J}{2 ( J + 1 )} η_{k} < η_{k} .$ Here $λ_{a r} (b_{k})$ and $σ_{a r} (b_{k})$ denote the two measures encoded by $b_{k}$ . Each of the two separate distance sums is therefore below $η_{k}$ . The triangle inequality gives empirical distances below $D_{Y} (ω) + η_{k} < r_{n}$ and $D_{E} (ω) + η_{k} < r_{m}$ , so $b_{k}$ belongs to both closed empirical balls. As $k \to \infty$ , [eq:external-root-order-stability] makes all four arm endpoints converge to their population values. Write $I (b_{k}) = [\underline{θ}_{k}, \overline{θ}_{k}], I (P_{rel}; H, g) = [\underline{θ}_{⋆}, \overline{θ}_{⋆}] .$ Both candidate endpoints converge to their corresponding population endpoints. Fix any $v \in I (P_{rel}; H, g)$ and clamp it to the candidate interval: $v_{k} = min {max {v, \underline{θ}_{k}}, \overline{θ}_{k}} \in I (b_{k}) .$ If $v < \underline{θ}_{k}$ , the distance $∣ v_{k} - v ∣$ is at most $∣ \underline{θ}_{k} - \underline{θ}_{⋆} ∣$ ; if $\overline{θ}_{k} < v$ , it is at most $∣ \overline{θ}_{k} - \overline{θ}_{⋆} ∣$ ; otherwise it is zero. Thus $v_{k} \to v$ . Every point of the population interval therefore lies in the closure of the union of candidate intervals, and hence in their closed convex hull. Write $θ (P) = E_{P} [Y_{1} - Y_{0}]$ . By Lemma 2, $θ (P)$ belongs to that sharp interval; its potential-outcome support also places it in $[- 1, 1]$ . Thus the clipped hull contains $θ (P)$ on the event in [eq:external-root-order-coverage], proving $C_{n, m} \in J_{n, m, α}^{ext} (g), C_{n, m} (ω) = the closed interval of Definition 22 at ω for every ω .$

For any retained candidate, the two empirical-ball inequalities and the triangle inequality bound its summed distance from the population array by $r_{n} + D_{Y} (ω) + r_{m} + D_{E} (ω)$ . therefore bounds each candidate arm endpoint’s error by $Λ_{ε} (r_{n} + D_{Y} (ω) + r_{m} + D_{E} (ω))$ . Each average-treatment-effect endpoint combines two arm endpoints; taking the hull and clipping it to $[- 1, 1]$ yields $(length (C_{n, m} (ω)) - length I (P_{rel}; H, g))_{+} \leq 4 Λ_{ε} (r_{n} + D_{Y} (ω) + r_{m} + D_{E} (ω)) .$ In either fallback branch of the construction the interval is ${0}$ , so its positive excess is zero and [eq:external-root-order-excess] holds there as well. Taking expectations and using [eq:external-root-order-mean] gives, uniformly over admissible $(P, H)$ , $E_{Q_{P, H}^{n, m}} [(length (C_{n, m}) - length I (P_{rel}; H, g))_{+}] \leq 4 Λ_{ε} (\frac{4 J / α + 2 J}{n} + \frac{2 J ( 2 - 2 ε ) / α + J ( 2 - 2 ε )}{m}) .$ The joint marginal and independence assumptions identify $Q_{P, H}^{n, m}$ with the product experiment in Definition 17. Hence honesty and [eq:external-root-order-mean-excess], followed by the infimum and supremum in Definition 19, give the same upper bound for $R_{n, m, α}^{⋆} (g)$ . Set $C_{ε, J, α, g} = 4 Λ_{ε} (\frac{4 J}{α} + 2 J + \frac{2 J ( 2 - 2 ε )}{α} + J (2 - 2 ε)) + 1 > 0.$ Both [eq:external-root-order-mean-excess] and the minimax bound are then at most $C_{ε, J, α, g} (n^{- 1/2} + m^{- 1/2})$ , as required.

Step 4: Normalized bounds. For positive $n, m$ , the upper bound just proved and Definition 20 imply $0 \leq T_{n, m, α} (g) = b_{n, m} R_{n, m, α}^{⋆} (g) \leq C_{ε, J, α, g}, b_{n, m} = (n^{- 1/2} + m^{- 1/2})^{- 1} .$ The lower inequality follows from the positive trial certificate in Lemma 4. Along the nonempty joint regime $n, m \to \infty$ , $n / m \to ρ > 0$ , [eq:external-root-order-normalized] bounds the limsup by $C_{ε, J, α, g}$ and ensures that the liminf is at most the limsup. The same cited lower certificate supplies $lim inf T_{n, m, α} (g) \geq max {\frac{c _{tr} ( α )}{1 + ρ}, \frac{c _{log} ( g , α ) ρ}{1 + ρ}} > 0.$ Together with the score-log liminf bound in Lemma 4, these are all the asserted inequalities.

∎

References

Rubin, Donald B. (1974). Estimating Causal Effects of Treatments in Randomized and Nonrandomized Studies. Journal of Educational Psychology. doi
Manski, Charles F. (1990). Nonparametric Bounds on Treatment Effects. American Economic Review. doi
Tamer, Elie (2010). Partial Identification in Econometrics. Annual Review of Economics. doi
Horowitz, Joel L. and Manski, Charles F. (1995). Identification and Robustness with Contaminated and Corrupted Data. Econometrica. doi
D'Orazio, Marcello and Di Zio, Marco and Scanu, Mauro (2006). Statistical Matching: Theory and Practice. Wiley. doi
Fan, Yanqin and Sherman, Robert and Shum, Matthew (2014). Identifying Treatment Effects Under Data Combination. Econometrica. doi
Torgovitsky, Alexander (2019). Partial Identification by Extending Subdistributions. Quantitative Economics. doi
Fan, Yanqin and Park, Hyeonseok and Pass, Brendan and Shi, Xuetao (2025). Partial Identification in Moment Models with Incomplete Data---A Conditional Optimal Transport Approach. . arXiv
Cochran, William G. (1968). The Effectiveness of Adjustment by Subclassification in Removing Bias in Observational Studies. Biometrics. doi
Rosenbaum, Paul R. and Rubin, Donald B. (1984). Reducing Bias in Observational Studies Using Subclassification on the Propensity Score. Journal of the American Statistical Association. doi
Kalavasis, Alkis and Mehrotra, Anay and Zampetakis, Manolis (2024). Smaller Confidence Intervals From {IPW} Estimators via Data-Dependent Coarsening. Proceedings of the 37th Conference on Learning Theory. arXiv
Lee, Sokbae and Weidner, Martin (2026). Bounding Treatment Effects by Pooling Limited Information across Observations. Journal of Econometrics. doi
Komarova, Tatiana and Nekipelov, Denis and Yakovlev, Evgeny (2018). Identification, Data Combination, and the Risk of Disclosure. Quantitative Economics. doi
Conti, Pier Luigi and Marella, Daniela and Scanu, Mauro (2017). How Far from Identifiability? A Systematic Overview of the Statistical Matching Problem in a Nonparametric Framework. Communications in Statistics---Theory and Methods. doi
Marella, Daniela and Pfeffermann, Danny (2019). Matching Information from Two Independent Informative Samples. Journal of Statistical Planning and Inference. doi
Lemaire, Vincent and Montes, Thibaut and Pag{\`e}s, Gilles (2020). New Weak Error Bounds and Expansions for Optimal Quantization. Journal of Computational and Applied Mathematics. doi
Imbens, Guido W. and Manski, Charles F. (2004). Confidence Intervals for Partially Identified Parameters. Econometrica. doi
Stoye, J{\"o}rg (2009). More on Confidence Intervals for Partially Identified Parameters. Econometrica. doi
Chernozhukov, Victor and Hong, Han and Tamer, Elie (2007). Estimation and Confidence Regions for Parameter Sets in Econometric Models. Econometrica. doi
Kaido, Hiroaki and Molinari, Francesca and Stoye, J{\"o}rg (2019). Confidence Intervals for Projections of Partially Identified Parameters. Econometrica. doi

Formal layer — Lean correspondence

Every object below is formalized in Lean 4. Click a verified row to view its statement; the rest link to the Lean source.

Setups (3)

Setup S-1 — A randomized causal population with overlap margin $\varepsilon$ , score space $\mathcal E=[\varepsilon,1-\varepsilon]$ , outcome space $\mathcal Y=[0,1]$ , arms $\mathcal A=\{0,1\}$ , and label alphabet $\mathcal R_J=\{1,\ldots,J\}$ . A causal law $P$ is a probability measure on $\mathcal E\times\mathcal Y^2\times\mathcal A\times\mathcal Y\times\mathcal R_J$ describing $(E,Y_0,Y_1,A,Y,R)$ . The known score law is $H\in\mathcal P(\mathcal E)$ (with density $f$ when absolutely continuous), a deterministic release rule $g:\mathcal E\to\mathcal R_J$ has cells $C_r=g^{-1}(r)$ , and the released law is $P_{\mathrm{rel}}=\mathcal L_P(R,A,Y)$ . Derived objects: $p_a,q_{ar},F_{ar},G_{ar},W_{ar}$ , the generalized quantile $Q$ , the endpoints $\underline\mu_a,\overline\mu_a$ , the interval $I(P_{\mathrm{rel}};H,g)$ , the classes $\mathfrak P(H,g)$ and $\mathfrak M(H,g,P_{\mathrm{rel}})$ , the ambiguity $D_H(g)$ , the release families $\mathcal G_K$ , the positive lower-density class $\mathcal H^{\mathrm{lb}}_{\varepsilon,m_f}$ , and $\Delta_K(H)$ .
Setup S-2 — The trial sampling experiment with a known score law: for a release $g\in\mathcal G_K$ , the analyst observes $n$ independent draws $(R_i,A_i,Y_i)$ of the released law of a causal population $P\in\mathfrak P(H,g)$ , and reports an interval $C_n\subseteq[-1,1]$ with miscoverage level $\alpha\in(0,1/2)$ . $\mathcal J_{n,K,\alpha}(H)$ is the class of uniformly honest release–procedure pairs, and $\mathcal L^\star_{n,K,\alpha}(H)$ is their minimax expected length.
Setup S-3 — The external score-log experiment: for a release $g$ , law pairs $(P,H)\in\mathfrak X(g)$ generate $n$ independent trial rows $(R_i,A_i,Y_i)$ and, independently, $m$ i.i.d. score draws $E^{\mathrm{log}}_j\sim H$ with empirical law $\widehat H_m$ . The joint law is $\mathbb Q^{n,m}_{P,H}$ , confidence procedures are $C_{n,m}$ valued in closed subintervals of $[-1,1]$ , $\mathcal J^{\mathrm{ext}}_{n,m,\alpha}(g)$ is the uniformly honest class, $\mathcal R^\star_{n,m,\alpha}(g)$ is the minimax expected excess length, $b_{n,m}=(n^{-1/2}+m^{-1/2})^{-1}$ , $T_{n,m,\alpha}(g)=b_{n,m}\mathcal R^\star_{n,m,\alpha}(g)$ , and $\rho\in(0,\infty)$ is the limiting ratio $n/m$ .

Definitions (18)

Definition P-1 verified CausalSmith.PartialID.UnlinkedPropensityAte.RandomizedCausalLaw $\mathfrak P(H,g)=\{P:\mathcal L_P(E)=H,\ P(A=1\mid E,Y_0,Y_1)=E,\ Y=AY_1+(1-A)Y_0,\ R=g(E)\ \text{almost surely}\}$ .
Definition P-2 verified CausalSmith.PartialID.UnlinkedPropensityAte.CompatibleCausalLaw $\mathfrak M(H,g,P_{\mathrm{rel}})=\{P\in\mathfrak P(H,g):\mathcal L_P(R,A,Y)=P_{\mathrm{rel}}\}$ .
Definition P-3 verified CausalSmith.PartialID.UnlinkedPropensityAte.armCell For $a\in\mathcal A$ and $r\in\mathcal R_J$ , set $p_1(e)=e$ , $p_0(e)=1-e$ , $C_r=\{e:g(e)=r\}$ , and $q_{ar}=\int_{C_r}p_a(e)H(de)$ . Define $F_{ar}=\mathcal L_{P_{\mathrm{rel}}}(Y\mid A=a,R=r)$ only when $P_{\mathrm{rel}}(A=a,R=r)>0$ . For $q_{ar}>0$ , define $G_{ar}(de)=\mathbf 1\{e\in C_r\}p_a(e)H(de)/q_{ar}$ and $W_{ar}=1/p_a(E_{ar})$ for $E_{ar}\sim G_{ar}$ . The endpoint formulas below apply to triples satisfying $P_{\mathrm{rel}}(A=a,R=r)=q_{ar}$ for every arm and label; then every term with $q_{ar}>0$ has a defined conditional law $F_{ar}$ , while zero-mass cells are omitted.
Definition P-4 verified CausalSmith.PartialID.UnlinkedPropensityAte.armMeanEndpoints For triples $H,g,P_{\mathrm{rel}}$ satisfying $P_{\mathrm{rel}}(A=a,R=r)=q_{ar}$ for every arm and label, set $\underline\mu_a=\sum_{r:q_{ar}>0}q_{ar}\int_0^1Q_{F_{ar}}(u)Q_{W_{ar}}(1-u)\,du$ and $\overline\mu_a=\sum_{r:q_{ar}>0}q_{ar}\int_0^1Q_{F_{ar}}(u)Q_{W_{ar}}(u)\,du$ .
Definition P-5 verified CausalSmith.PartialID.UnlinkedPropensityAte.sharpATESet $I(P_{\mathrm{rel}};H,g)=[\underline\mu_1-\overline\mu_0,\overline\mu_1-\underline\mu_0]$ .
Definition P-6 verified CausalSmith.PartialID.UnlinkedPropensityAte.worstCaseAmbiguity $D_H(g)=\sup_{P\in\mathfrak P(H,g)}\operatorname{len}\{I(\mathcal L_P(R,A,Y);H,g)\}$ .
Definition P-7 verified CausalSmith.PartialID.UnlinkedPropensityAte.kLabelReleases $\mathcal G_K=\{g:\mathcal E\to\{1,\ldots,K\}:g\text{ is measurable}\}$ .
Definition P-8 verified CausalSmith.PartialID.UnlinkedPropensityAte.optimalKAmbiguity $\Delta_K(H)=\inf_{g\in\mathcal G_K}D_H(g)$ .
Definition P-9 verified CausalSmith.PartialID.UnlinkedPropensityAte.honestProcedures $\mathcal J_{n,K,\alpha}(H)=\{(g,C_n):g\in\mathcal G_K,\ \inf_{P\in\mathfrak P(H,g)}P^{\otimes n}[\theta(P)\in C_n((R_i,A_i,Y_i)_{i=1}^n)]\ge1-\alpha\}$ .
Definition P-10 verified CausalSmith.PartialID.UnlinkedPropensityAte.minimaxHonestLength $\mathcal L^\star_{n,K,\alpha}(H)=\inf_{(g,C_n)\in\mathcal J_{n,K,\alpha}(H)}\sup_{P\in\mathfrak P(H,g)}\mathbb E_{P^{\otimes n}}[\operatorname{len}(C_n)]$ .
Definition P-12 verified CausalSmith.PartialID.UnlinkedPropensityAte.ExternalScoreLaw $\mathfrak X(g)=\{(P,H):H\in\mathcal P(\mathcal E),\ P\in\mathfrak P(H,g)\}$ .
Definition P-13 verified CausalSmith.PartialID.UnlinkedPropensityAte.externalExperiment For $(P,H)\in\mathfrak X(g)$ , $\mathbb Q_{P,H}^{n,m}=\mathcal L_P(R,A,Y)^{\otimes n}\otimes H^{\otimes m}$ is the law of $((R_i,A_i,Y_i)_{i=1}^n,(E_j^{\mathrm{log}})_{j=1}^m)$ .
Definition P-14 verified CausalSmith.PartialID.UnlinkedPropensityAte.externalHonestProcedures $\mathcal J^{\mathrm{ext}}_{n,m,\alpha}(g)=\{C_{n,m}:\inf_{(P,H)\in\mathfrak X(g)}\mathbb Q_{P,H}^{n,m}[\theta(P)\in C_{n,m}]\ge1-\alpha\}$ .
Definition P-15 verified CausalSmith.PartialID.UnlinkedPropensityAte.externalExcessRisk $\mathcal R^{\star}_{n,m,\alpha}(g)=\inf_{C_{n,m}\in\mathcal J^{\mathrm{ext}}_{n,m,\alpha}(g)}\sup_{(P,H)\in\mathfrak X(g)}\mathbb E_{\mathbb Q_{P,H}^{n,m}}[(\operatorname{len}(C_{n,m})-\operatorname{len}I(\mathcal L_P(R,A,Y);H,g))_+]$ .
Definition P-16 verified CausalSmith.PartialID.UnlinkedPropensityAte.externalNormalizedRisk $b_{n,m}=(n^{-1/2}+m^{-1/2})^{-1},\qquad T_{n,m,\alpha}(g)=b_{n,m}\mathcal R^{\star}_{n,m,\alpha}(g).$
Definition P-17 verified CausalSmith.PartialID.UnlinkedPropensityAte.externalProjectionCI For trial rows, form the empirical finite measures $\widehat\lambda_{ar}(B)=n^{-1}\sum_i\mathbf 1\{R_i=r,A_i=a,Y_i\in B\}$ . For the independent score log, form $\widehat\sigma_{ar}(B)=m^{-1}\sum_j p_a(E_j^{\mathrm{log}})\mathbf 1\{g(E_j^{\mathrm{log}})=r,E_j^{\mathrm{log}}\in B\}$ . Equip finite measures on each compact support with total-mass plus integrated-CDF distance, and use the explicit radii $r_n=4J/(\alpha\sqrt n)$ and $r_m=2J(2-2\varepsilon)/(\alpha\sqrt m)$ . For $q\in\mathbb Q$ , put $x(q)=\max\{0,\min\{1,q\}\}\in[0,1]$ and $e_\varepsilon(q)=\varepsilon+(1-2\varepsilon)x(q)\in\mathcal E$ . For a finite list $L=((q_s,w_s))_{s=1}^N\in\operatorname{List}(\mathbb Q\times\mathbb Q)$ , define $\nu_Y(L)=\sum_{s=1}^N\operatorname{ofReal}(w_s)\,\delta_{x(q_s)},\qquad \nu_E(L)=\sum_{s=1}^N\operatorname{ofReal}(w_s)\,\delta_{e_\varepsilon(q_s)},$ where $\operatorname{ofReal}(w)=\max\{w,0\}$ , viewed as a nonnegative extended-real weight. Under the standing overlap condition, define the canonical sieve $\mathcal D_{\varepsilon,J}= \left\{ \left( ((\nu_Y(L^Y_{ar}))_{a,r}, (\nu_E(L^E_{ar}))_{a,r}) \right): L^Y,L^E:\mathcal A\to\mathcal R_J\to \operatorname{List}(\mathbb Q\times\mathbb Q) \right\} \cap\{(\lambda',\sigma'):\operatorname{ProjectionCompatible}(\lambda',\sigma')\}.$ If overlap fails, set $\mathcal D_{\varepsilon,J}=\varnothing$ . Thus the outcome and score lists are arbitrary and separate, while the intersection imposes exact equality of their total masses in every arm-label cell. Duplicate support codes, clamped codes outside $[0,1]$ , and nonpositive weights do not change the represented nonnegative measure and need not be excluded. Let $\mathcal B_{n,m}$ be the exact intersection of $\mathcal D_{\varepsilon,J}$ with the finite compatible arrays satisfying the two closed empirical-ball inequalities $\sum_{a,r}d_{[0,1]}(\lambda'_{ar},\widehat\lambda_{ar})\le r_n, \qquad \sum_{a,r}d_{\mathcal E}(\sigma'_{ar},\widehat\sigma_{ar})\le r_m.$ For each $b\in\mathcal B_{n,m}$ , compute its two quantile-transport ATE endpoints and interval $I(b)$ . When $\mathcal B_{n,m}\ne\varnothing$ , define the clipped hull $J_{n,m}=[-1,1]\cap\operatorname{cl}\operatorname{conv}\!\left(\bigcup_{b\in\mathcal B_{n,m}}I(b)\right).$ Return $C_{n,m}=J_{n,m}$ when $\mathcal B_{n,m}\ne\varnothing$ and $J_{n,m}\ne\varnothing$ . Return $C_{n,m}=\{0\}$ in each of the two failure branches: when $\mathcal B_{n,m}=\varnothing$ , or when $\mathcal B_{n,m}\ne\varnothing$ but $J_{n,m}=\varnothing$ . This piecewise totalized canonical rational-sieve rule is measurable and is the atom-valid attaining procedure used by the external-score root-order theorem; directional or resampling refinements are optional rather than required for its stated rate.
Definition P-18 verified CausalSmith.PartialID.UnlinkedPropensityAte.LowerScoreDensity $\mathcal H^{\mathrm{lb}}_{\varepsilon,m_f}=\{H\in\mathcal P(\mathcal E):H(de)=f(e)\,de,\ f(e)\ge m_f\ \text{for Lebesgue-almost every }e\in\mathcal E\}$ .
Definition P-19 verified CausalSmith.PartialID.UnlinkedPropensityAte.ExternalSharpLimitQuestion Fix a measurable release $g$ and $0<\alpha<1/2$ . Over the external-score law class $\mathfrak X(g)$ , with confidence procedures restricted by $\mathcal J^{\mathrm{ext}}_{n,m,\alpha}(g)$ , determine $\liminf_{\substack{n,m\to\infty\\ n/m\to\rho}} T_{n,m,\alpha}(g) \quad\text{and}\quad \limsup_{\substack{n,m\to\infty\\ n/m\to\rho}} T_{n,m,\alpha}(g)$ for each $\rho\in(0,\infty)$ . Decide whether these limits coincide, and determine the common sharp constant if they do. If a common sharp limit does not hold over the full class, identify an explicitly defined regular subclass of $\mathfrak X(g)$ for which a common sharp limit holds for each $\rho\in(0,\infty)$ , state its defining regularity conditions, and determine that limit. For this subclass question, restrict both the uniform honesty requirement and the supremum in expected excess length to that subclass. Use $\mathsf H_{\mathrm{ext}}$ to construct an attaining projection or a counterexample.

Assumptions (10)

Assumption A-1 verified CausalSmith.PartialID.UnlinkedPropensityAte.Overlap $0<\varepsilon<1/2$
Assumption A-2 verified CausalSmith.PartialID.UnlinkedPropensityAte.ScoreMarginal $\mathcal L_P(E)=H$
Assumption A-3 verified CausalSmith.PartialID.UnlinkedPropensityAte.RandomizedAssignment $P(A=1\mid E,Y_0,Y_1)=E\quad\text{almost surely}.$
Assumption A-4 verified CausalSmith.PartialID.UnlinkedPropensityAte.Consistency $Y=AY_1+(1-A)Y_0\quad\text{almost surely}.$
Assumption A-5 verified CausalSmith.PartialID.UnlinkedPropensityAte.DeterministicRelease $R=g(E)\quad\text{almost surely}.$
Assumption A-6 verified CausalSmith.PartialID.UnlinkedPropensityAte.ReleasedLaw $\mathcal L_P(R,A,Y)=P_{\mathrm{rel}}$
Assumption A-7 verified CausalSmith.PartialID.UnlinkedPropensityAte.DensityLower $H(de)=f(e)\,de,\qquad f(e)\ge m_f\quad\text{for Lebesgue-almost every }e\in\mathcal E.$
Assumption A-8 verified CausalSmith.PartialID.UnlinkedPropensityAte.IIDTrialSampling $(R_i,A_i,Y_i)_{i=1}^n\stackrel{\mathrm{iid}}{\sim}\mathcal L_P(R,A,Y).$
Assumption A-9 verified CausalSmith.PartialID.UnlinkedPropensityAte.ExternalLogIID $(E_j^{\mathrm{log}})_{j=1}^m\stackrel{\mathrm{iid}}{\sim}H.$
Assumption A-10 verified CausalSmith.PartialID.UnlinkedPropensityAte.ExternalLogIndependent $(E_j^{\mathrm{log}})_{j=1}^m\mathrel{\perp\!\!\!\perp}(R_i,A_i,Y_i)_{i=1}^n.$

Lemmas (4)

Lemma L-4 verified CausalSmith.PartialID.UnlinkedPropensityAte.compatibleCellMasses_of_randomizedCausalLaw Let $H$ be a score law on $\mathcal E$ , let $g:\mathcal E\to\mathcal R_J$ be a measurable release, let $P\in\mathfrak P(H,g)$ , and let $P_{\mathrm{rel}}=\mathcal L_P(R,A,Y)$ be its released law. Then $H$ and $P_{\mathrm{rel}}$ are probability laws, and for every $r\in\mathcal R_J$ the treated arm-cell mass is $P_{\mathrm{rel}}(A=1,R=r)=\int_{C_r}e\,H(de)=q_{1r}$ , by score-based assignment and the score marginal. The control arm-cell mass is obtained by subtracting this treated mass from the label mass supplied by the score marginal: $P_{\mathrm{rel}}(A=0,R=r)=P(E\in C_r)-P(E\in C_r,A=1)=H(C_r)-\int_{C_r}e\,H(de)=\int_{C_r}(1-e)\,H(de)=q_{0r}$ . Consequently $P_{\mathrm{rel}}(A=a,R=r)=q_{ar}$ for every $a\in\mathcal A$ and $r\in\mathcal R_J$ .
Lemma L-1 verified CausalSmith.PartialID.UnlinkedPropensityAte.fixedReleasedLaw_sharp Fix $P_{\mathrm{rel}}$ with $\mathfrak M(H,g,P_{\mathrm{rel}})\ne\varnothing$ . Applying FanShermanShum2014, Theorem 3.2, to each label-specific fixed observed law gives, for every $a\in\mathcal A$ , the exact attainable interval $[\underline\mu_a,\overline\mu_a]$ for $\mathbb E_P[Y_a]$ over $P\in\mathfrak M(H,g,P_{\mathrm{rel}})$ . Their equation (3.1) and sharpness construction then give exactly $I(P_{\mathrm{rel}};H,g)=[\underline\mu_1-\overline\mu_0,\overline\mu_1-\underline\mu_0]$ , with each endpoint attained by a common causal population and convex mixtures filling the interval.
Lemma L-2 verified CausalSmith.PartialID.UnlinkedPropensityAte.pairedQuantization_tendsto Let $\mathcal I=[a,b]$ be a nondegenerate compact interval, let $S\ge1$ , and let $\beta_s:\mathcal I\times\mathcal I\to(0,\infty)$ , $s=1,\ldots,S$ , be continuous. For $k\ge1$ , define $V_k=\inf_{\substack{(B_1,\ldots,B_k)\ \mathrm{measurable\ partition\ of}\ \mathcal I\\ z_{js}\in\mathcal I}} \sum_{j=1}^k\sum_{s=1}^S \int_{B_j}\beta_s(x,z_{js})|x-z_{js}|\,dx$ and $w(x)=\sum_{s=1}^S\beta_s(x,x)$ . Then $\lim_{k\to\infty}kV_k =\frac14\left(\int_a^b\sqrt{w(x)}\,dx\right)^2.$ Moreover, the upper limit is attained by ordered interval cells whose boundaries equalize the integral of $\sqrt w$ , with all $S$ reproduction points in a cell chosen equal to its midpoint.
Lemma L-3 verified CausalSmith.PartialID.UnlinkedPropensityAte.externalExcessRisk_lower_certificates Fix a measurable finite-label release $g:\mathcal E\to\mathcal R_J$ and let $0<\alpha<1/2$ . Put $L_\alpha=1+(1-2\alpha)^2$ and $S_g= \sup_{\substack{r\in\mathcal R_J,\ e_1<e_2<e_3\\ e_1,e_2,e_3\in C_r}} \frac{(e_3-e_2)(1-e_1/e_2)} {\sqrt{(e_3-e_2)^2+(e_3-e_1)^2+(e_2-e_1)^2}}.$ Then $0<S_g\le 1$ . With $c_{\mathrm{tr}}(\alpha) =\frac{(1-2\alpha)\sqrt{\log L_\alpha}}4, \qquad c_{\mathrm{log}}(g,\alpha) =\frac{(1-2\alpha)\sqrt{\log L_\alpha}}{2\sqrt3}S_g,$ the external-score minimax excess risk satisfies, for all positive integers $n,m$ , $\mathcal R^\star_{n,m,\alpha}(g) \ge c_{\mathrm{tr}}(\alpha)n^{-1/2},$ and $\liminf_{m\to\infty}\inf_{n\ge1} \sqrt m\,\mathcal R^\star_{n,m,\alpha}(g) \ge c_{\mathrm{log}}(g,\alpha)>0.$ Consequently, for every $\rho\in(0,\infty)$ , $\liminf_{\substack{n,m\to\infty\\ n/m\to\rho}} T_{n,m,\alpha}(g) \ge \max\left\{ \frac{c_{\mathrm{tr}}(\alpha)}{1+\sqrt\rho}, \frac{c_{\mathrm{log}}(g,\alpha)\sqrt\rho}{1+\sqrt\rho} \right\}>0.$

Theorems (7)

Theorem T-1 verified CausalSmith.PartialID.UnlinkedPropensityAte.compatible_nonempty_iff The class $\mathfrak M(H,g,P_{\mathrm{rel}})$ is nonempty if and only if, for every $r\in\mathcal R_J$ , $P_{\mathrm{rel}}(R=r)=H(C_r)$ and $P_{\mathrm{rel}}(A=1,R=r)=\int_{C_r}e\,H(de)$ . No further restriction is imposed on the conditional outcome laws $F_{ar}$ beyond support in $[0,1]$ .
Theorem T-2 verified CausalSmith.PartialID.UnlinkedPropensityAte.worstCaseAmbiguity_eq For every $H\in\mathcal P(\mathcal E)$ and measurable $g:\mathcal E\to\mathcal R_J$ , including atomic $H$ and disconnected cells $C_r$ , the exact worst-case attained ATE width is $D_H(g)=\sum_{r=1}^J\left\{\inf_{c\in[1/(1-\varepsilon),1/\varepsilon]}\int_{C_r}|1-ce|\,H(de)+\inf_{d\in[1/(1-\varepsilon),1/\varepsilon]}\int_{C_r}|1-d(1-e)|\,H(de)\right\}.$ The supremum over released laws is attained by $F_{ar}=\operatorname{Bernoulli}(1/2)$ in every positive-mass arm-cell, and two full causal populations with that same released law attain the opposite ATE endpoints.
Theorem T-3 verified CausalSmith.PartialID.UnlinkedPropensityAte.worstCaseAmbiguity_eq_zero_iff For every $H$ and deterministic release $R=g(E)$ , $D_H(g)=0$ if and only if there exists a measurable map $h$ such that $E=h(R)$ almost surely under $H$ . Equivalently, each positive- $H$ -mass cell $C_r$ contains a single score value up to an $H$ -null set.
Theorem T-4 verified CausalSmith.PartialID.UnlinkedPropensityAte.optimalKAmbiguity_bounds Let $\ell=1-2\varepsilon$ . For every $H\in\mathcal H^{\mathrm{lb}}_{\varepsilon,m_f}$ and every integer $K\ge 1$ , $\frac{m_f\ell^2}{2(1-\varepsilon)K} \le \Delta_K(H) \le \frac{\ell}{2\varepsilon(1-\varepsilon)K}.$ The lower bound holds over all measurable releases with at most $K$ labels, including releases with disconnected cells. The upper bound is witnessed by equal-width interval labels; that upper inequality, considered by itself, holds for every probability law $H$ on $\mathcal E$ , without absolute continuity or either density bound.
Theorem T-5 verified CausalSmith.PartialID.UnlinkedPropensityAte.minimaxHonestLength_order Fix $0<\alpha<1/2$ . There exist constants $c_{\varepsilon,m_f,\alpha}>0$ and $C_{\varepsilon,\alpha}<\infty$ such that, for every $H\in\mathcal H^{\mathrm{lb}}_{\varepsilon,m_f}$ , $n\ge1$ , and $K\ge1$ , $c_{\varepsilon,m_f,\alpha}\left(K^{-1}+n^{-1/2}\right) \le \mathcal L^\star_{n,K,\alpha}(H) \le C_{\varepsilon,\alpha}\left(K^{-1}+n^{-1/2}\right).$ For the equal-width release, let $z_r$ be the midpoint of label cell $r$ and define $\widehat T_n=n^{-1}\sum_{i=1}^n\{A_iY_i/z_{R_i}-(1-A_i)Y_i/(1-z_{R_i})\}$ , $B_K=\frac{1-2\varepsilon}{2K\varepsilon(1-\varepsilon)}$ , and $R_{n,K}=(4/\varepsilon)\sqrt{\log(4/\alpha)/n}+B_K$ . With $\operatorname{clampATE}(x)=\max\{-1,\min\{1,x\}\}$ , the upper bound is achieved by the always-nonempty interval $C_n=[\operatorname{clampATE}(\widehat T_n-R_{n,K}),\operatorname{clampATE}(\widehat T_n+R_{n,K})]$ . The label component of the lower bound holds for arbitrary measurable, including disconnected, release cells and uses only the density lower bound; the sampling component uses neither a density lower nor upper bound.
Theorem T-6 verified CausalSmith.PartialID.UnlinkedPropensityAte.tendsto_K_mul_optimalKAmbiguity Let $H\in\mathcal P(\mathcal E)$ , where $\mathcal E=[\varepsilon,1-\varepsilon]$ , and suppose that $H(de)=f(e)\,de$ for a continuous strictly positive density $f$ on $\mathcal E$ . Then the question posed through $\mathsf H_{\mathrm{opt}}$ has the exact answer $\lim_{K\to\infty}K\Delta_K(H) =\frac14\left( \int_\varepsilon^{1-\varepsilon} \sqrt{\frac{f(e)}{e(1-e)}}\,de \right)^2.$ There is a sequence $g_K\in\mathcal G_K$ of ordered interval releases attaining this limit. Hence unrestricted measurable cells cannot improve the leading constant, and an asymptotically optimal unrestricted value can always be replaced, in value up to $o(K^{-1})$ , by ordered interval cells. No claim of finite- $K$ intervalization is made.
Theorem T-7 verified CausalSmith.PartialID.UnlinkedPropensityAte.externalExcessRisk_root_order Fix a measurable finite-label release $g:\mathcal E\to\mathcal R_J$ and $0<\alpha<1/2$ . Define $L_\alpha=1+(1-2\alpha)^2,$ $S_g= \sup_{\substack{r\in\mathcal R_J,\ e_1<e_2<e_3\\ e_1,e_2,e_3\in C_r}} \frac{(e_3-e_2)(1-e_1/e_2)} {\sqrt{(e_3-e_2)^2+(e_3-e_1)^2+(e_2-e_1)^2}},$ and $c_{\mathrm{tr}}(\alpha) =\frac{(1-2\alpha)\sqrt{\log L_\alpha}}4, \qquad c_{\mathrm{log}}(g,\alpha) =\frac{(1-2\alpha)\sqrt{\log L_\alpha}}{2\sqrt3}S_g.$ Then $0<S_g\le1$ , and there is a finite constant $C_{\varepsilon,J,\alpha,g}$ such that, for all positive integers $n,m$ , $c_{\mathrm{tr}}(\alpha)n^{-1/2} \le\mathcal R^\star_{n,m,\alpha}(g) \le C_{\varepsilon,J,\alpha,g}(n^{-1/2}+m^{-1/2}).$ The upper bound is attained by the atom-valid totalized rational-sieve interval $C_{n,m}$ prescribed by $\mathsf H_{\mathrm{ext}}$ , with $C_{n,m}=\{0\}$ when either its sieve candidate set is empty or its nonempty candidate set has an empty clipped hull. In the external-score direction, $\liminf_{m\to\infty}\inf_{n\ge1} \sqrt m\,\mathcal R^\star_{n,m,\alpha}(g) \ge c_{\mathrm{log}}(g,\alpha)>0.$ Consequently, for every $\rho\in(0,\infty)$ , $\max\left\{ \frac{c_{\mathrm{tr}}(\alpha)}{1+\sqrt\rho}, \frac{c_{\mathrm{log}}(g,\alpha)\sqrt\rho}{1+\sqrt\rho} \right\} \le\liminf_{\substack{n,m\to\infty\\ n/m\to\rho}} T_{n,m,\alpha}(g) \le\limsup_{\substack{n,m\to\infty\\ n/m\to\rho}} T_{n,m,\alpha}(g) \le C_{\varepsilon,J,\alpha,g}<\infty,$ and the displayed maximum is strictly positive. Thus the root-two-sample normalization is correct uniformly over the stated class, including atomic score and outcome laws and rank contacts. This order theorem does not determine either exact normalized limit, assert that the limits are equal, or give a common sharp efficiency constant.

Auxiliary Lean lemmas (machine-checked) (186)

Definition CausalLaws —
Definition cell —
Definition cellAbsoluteDeviation —
Definition clampATE —
Definition compandingAmbiguity —
Definition densityExtension —
Definition equalWidthRelease —
Definition ExternalIntervalProcedure —
Definition ExternalLaws —
Definition fiberTripleSeparation —
Definition FullRow —
Definition halfOutcomeReleasedLaw —
Definition IntervalProcedure —
Definition label —
Definition LabelSpace —
Definition logCertificate —
Definition midpointWeightedCenter —
Definition midpointWeightedRadius —
Definition muUpper —
Definition ProjectionCompatible —
Definition ratioFilter —
Definition releasedLaw —
Definition ScoreSpace —
Definition sharpATELength —
Definition trialCertificate —
Definition TrialSample —
Definition muLower —
Definition CompatibleCellMasses —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellMass_nonneg —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellMass_sum_arms —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellMass_total —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.compatibility_armCellMass_sum —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.releasedLabelMass_sum_arms —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.compatibleCellMasses_of_label_treated —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.scoreRecovery_iff_cellwiseAE —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.cellAbsoluteDeviation_nonneg —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.cellAbsoluteDeviation_le_integral —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.cellAbsoluteDeviation_zero_of_ae —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armProb_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.cellAbsoluteDeviation_zero_of_cellwiseAE —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.cellDeviationIntegral_continuousOn —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.cellAbsoluteDeviation_minimizer —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellMass_lower_overlap —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellMass_pos_of_cellMass_pos —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellMass_eq_zero_iff_cellMass_eq_zero —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedWeightedAbsDeviation_lower —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.fiberTriple_exists —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.fiberTriple_ratio_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.fiberTripleSeparation_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.fiberTriple_perturbation_identities —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.fiberTriple_upperEndpoint_shift —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.fiberTriple_chisq_identity —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalCertificate_constants_pos —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedDiagonalWeight_pos —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedDiagonalWeight_continuousOn —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedDiagonalWeight_uniform_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.abs_deviation_integral_midpoint —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedPartitionCost_nonneg —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.optimalPairedCost_nonneg —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedCoefficient_uniform_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedCoefficients_uniform_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.optimalPairedCost_le_feasible —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.equalWidthRelease_measurable —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedBadPoint_cost_lower —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedGoodCell_diameter —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedBadSet_measure_cost —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedBadSet_measure_le —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedBoundary_zero —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedBoundary_mem_Icc —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedCompandingMidpoint_mem_Icc —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.orderedHalfOpenIntervals_cover —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.orderedIntervalCells_partition —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedBoundary_mono —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.pairedBoundary_last —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellOutcomeLaw_isProbabilityMeasure —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.armCellOutcomeLaw_apply —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionArmProb_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionArmProb_diff_abs —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionInverseArmProb_lipschitz —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCost_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.variance_trialCellIndicator_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.variance_trialCellFrequency_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalProjectionCI_excessLength_le_of_envelope —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalProjectionCI_subset_envelope_of_candidates —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.empiricalScoreCells_real_apply —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.variance_scoreCellIndicator —
Definition CausalSmith.PartialID.UnlinkedPropensityAte.scoreCellFrequency —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.variance_scoreCellFrequency_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.measurable_scoreCellFrequency —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.integral_scoreCellFrequency_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.empiricalScoreCells_real_eq_scoreCellFrequency —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.integral_empiricalScoreCells_real_apply_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.variance_empiricalScoreCells_real_apply_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionMeanAbs_le_sqrt_variance —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionMeanAbs_le_inv_two_sqrt —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.meanAbs_trialCellFrequency_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.meanAbs_scoreCellFrequency_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.meanAbs_empiricalScoreCells_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.sum_meanAbs_trialCellFrequency_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.sum_meanAbs_empiricalScoreCells_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionExpectedIntegratedError_le —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.meanIntegratedAbs_empiricalTrialCellCDF_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.meanIntegratedAbs_empiricalScoreCellCDF_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.measurable_projectionFiniteCDF —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.measurable_empiricalTrialCellCDF_joint —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.measurable_trialPopulationCellCDF —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.empiricalTrialCellCDF_mem_Icc —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.trialPopulationCellCDF_mem_Icc —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.integrable_empiricalTrialCellCDF_joint —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.measurable_empiricalScoreCellCDF_joint —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.measurable_scorePopulationCellCDF —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.integrable_empiricalScoreCellCDF_joint —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.sum_meanTrialCellCDFError_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.sum_meanScoreCellCDFError_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalProjectionCI_excessLength_le_of_candidate_envelopes —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.countable_rationalArraySieve —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.countable_sievedProjectionCandidates —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projection_strictBalls_closure_of_dense —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.normalizedCertificate_trial —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.normalizedCertificate_log —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projection_twoSource_strictBall_probability —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectedATEInterval_subset_of_armEndpoint_bounds —
Definition CausalSmith.PartialID.UnlinkedPropensityAte.trialPopulationCells —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.trialPopulationCells_apply —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.trialPopulationCells_real_apply —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.outcomeCDFDistance_trialPopulationCells —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.meanOutcomeCDFDistance_trialPopulationCells_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.sum_meanOutcomeCDFDistance_trialPopulationCells_pi —
Definition CausalSmith.PartialID.UnlinkedPropensityAte.scorePopulationCells —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.scorePopulationCells_real_apply —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.scoreCDFDistance_scorePopulationCells —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.meanScoreCDFDistance_scorePopulationCells_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.sum_meanScoreCDFDistance_scorePopulationCells_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCompatible_populationCells —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalProjectionCI_excessLength_le_of_armEndpoint_bounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projection_strictBall_probability_at_paper_radii —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalJointLaw_eq_experiment —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalJointTrial_integral_eq_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalJointLog_integral_eq_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalNormalizer_mul_rootSum —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalNormalizedRisk_le_of_rootSum_bound —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.ratioFilter_ratio_tendsto —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.normalizedCertificate_ratio_trial —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.normalizedCertificate_ratio_log —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCandidate_populationDistance_le —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionFiniteCDF_intervalIntegrable —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionFiniteCDF_absDiff_intervalIntegrable —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionIntegratedAbs_triangle —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.outcomeCDFDistance_triangle —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.scoreCDFDistance_triangle —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCandidate_populationDistance_le_of_finite —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCandidate_populationDistance_le_of_populationFinite —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.empiricalTrialCells_finite —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.empiricalScoreCells_finite —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalJointTrial_meanDistance_le —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalJointLog_meanDistance_le —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectedArmEndpoint_abs_le_of_cellBounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.outcomeCDFDistance_nonneg —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.scoreCDFDistance_nonneg —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectedArmEndpoint_abs_le_of_armBounds —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.ratioFilter_eventually_pos —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCandidate_armEndpoint_abs_le —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.ratioFilter_neBot —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCandidate_populationArmEndpoint_abs_le —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionCandidate_populationATEInterval_subset —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectionPopulationCells_finite —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalATE_mem_Icc —
Definition CausalSmith.PartialID.UnlinkedPropensityAte.externalFullInterval —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalFullInterval_honest —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalExcessIntegral_le_two —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectedArmEndpoint_lower_le_upper —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projectedATEInterval_mem_closure_of_sieve_approx —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projection_strict_population_approximants —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.projection_strictBall_ate_mem_CI —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalProjectionIntervalProcedure_honest —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalExcessRisk_le_of_honest_uniform_bound —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.integrable_outcomeCDFDistance_population_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.integrable_scoreCDFDistance_population_pi —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.cell_lower_le_upper_of_overlap —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.exists_sievedProjectionCandidate_close_of_slack —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.externalExcessRisk_normalized_upper —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.logCertificate_ratio_liminf_of_upperBound —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.logCertificate_ratio_liminf_of_infimum —
Definition ExternalScoreLaw —
Definition RationalProjectionSieveScope —
Lemma CausalSmith.PartialID.UnlinkedPropensityAte.equalWidthBinMidpoint_val —

Symbol realizations (Lean @realizes) (53)

Espace verified realized by ScoreSpace
Yspace verified realized by OutcomeSpace
Aspace verified realized by ArmSpace
a verified realized by ArmSpace
Rspace verified realized by LabelSpace
J verified realized by LabelSpace
P verified realized by Observation, RandomizedCausalLaw, CompatibleCausalLaw, CompatibleLaws, ExternalScoreLaw, ExternalLaws
Prel verified realized by score, ate, CompatibleCellMasses, compatible_nonempty_iff
E verified realized by score
Y0 verified realized by outcome0
Y1 verified realized by outcome1
A verified realized by arm
Y verified realized by observed
R verified realized by label
theta verified realized by ate
epsilon verified realized by Overlap
H verified realized by ScoreMarginal, DensityLower, LowerScoreDensity, BoundedScoreDensity, CompatibleCellMasses, ExternalScoreLaw, ExternalLaws, compatible_nonempty_iff
p verified realized by RandomizedAssignment, armProb
g verified realized by DeterministicRelease, RandomizedCausalLaw, CompatibleCausalLaw, CompatibleCellMasses, kLabelReleases, ExternalScoreLaw
Pclass verified realized by RandomizedCausalLaw
Mclass verified realized by CausalLaws
f verified realized by DensityLower
mf verified realized by DensityLower, optimalKAmbiguity_bounds, minimaxHonestLength_order
C verified realized by cell
q verified realized by armCellMass, CompatibleCellMasses
F verified realized by armCellScoreLaw
G verified realized by armCellWeightLaw
W verified realized by armCellWeightLaw
Q verified realized by generalizedQuantile
muL verified realized by muUpper
muU verified realized by muUpper
Isharp verified realized by sharpATELength
D verified realized by worstCaseAmbiguity
GK verified realized by kLabelReleases
K verified realized by kLabelReleases, optimalKAmbiguity_bounds, minimaxHonestLength_order
DeltaK verified realized by optimalKAmbiguity
Hopt verified realized by highResolutionHandle
m verified realized by ExternalSample, externalExcessRisk_lower_certificates, externalExcessRisk_root_order
Elog verified realized by ExternalSample
Xext verified realized by ExternalLaws
Qext verified realized by externalExperiment
Cext verified realized by ExternalIntervalProcedure
Jext verified realized by externalHonestProcedures
Rext verified realized by externalNormalizer
bext verified realized by externalNormalizer
Text verified realized by externalNormalizedRisk
rho verified realized by ratioFilter, externalExcessRisk_lower_certificates, externalExcessRisk_root_order
n verified realized by externalExcessRisk_lower_certificates, TrialSample, externalExcessRisk_root_order, minimaxHonestLength_order
Cn verified realized by IntervalProcedure
alpha verified realized by honestProcedures, externalExcessRisk_root_order, minimaxHonestLength_order
Jhonest verified realized by honestProcedures
Lminimax verified realized by minimaxHonestLength
Hext verified realized by externalProjectionCI

Proof map 11 statements · 11 edges

Assignment Probabilities Without Row-level Links: Identification, Label Design, and Inference in Randomized Trials

Abstract

Introduction

Related work

Trial setup and the sharp identified interval

Information retained by a score label

Designing a finite-label release

Honest intervals with a known score law

Inference with an independent score log

Discussion and open questions

Open questions

Appendices

Proofs and verification scope

Fixed-law bounds and compatibility

Ambiguity and finite-label design

External-log excess risk

Verification scope

Proofs of the main results

References