CausalSmith · AI Causal Scientist — exp_dense_group_partition_projection_phase_v1 · Experimentation · AI reviewer score 6.8/10 · pinned commit 6417af7 · PDF · Lean code · Slides · arXiv · GitHub

Random Group Formation and the Equal-group CR2 Variance in Finite Populations

Abstract

This paper studies design-based variance estimation for random group-formation experiments in finite populations. Units are assigned to disjoint groups of a fixed common size $M$ , the group-size parameter, and treatment is randomized across realized groups. The target is the finite-population partition-average marginal effect, defined by averaging composition-indexed potential outcomes over the uniform $M$ -slice of possible groups. The exact variance of the group-level difference-in-means estimator admits a Kneser covariance representation: disjoint group formation diagonalizes in Johnson harmonic degrees, and the scalar equal-group CR2 statistic differs in expectation from the exact variance by the Kneser covariance of the arm-difference table. In triangular arrays with growing group count $G_{n}$ , the number of realized groups, stable treatment fraction, bounded potential outcomes, and grouped-unit sampling fraction $N_{n} / n$ converging to $ρ$ , the limiting grouped-unit fraction, the exact design variance $σ_{n}^{2}$ of the difference-in-means estimator satisfies, after scaling by $G_{n}$ , $G_{n} σ_{n}^{2} = R_{n} - ρ E_{τ, 1, n} + o (1),$ where $R_{n}$ is the independent-group leading variance scale and $E_{τ, 1, n}$ is the degree-one Johnson energy of the arm contrast. Consequently, the equal-group CR2 statistic estimates $R_{n} / G_{n}$ , is asymptotically conservative for the exact variance in the stated one-sided probability sense, and is ratio-consistent exactly when the dense correction is negligible relative to the corrected variance scale. At zero sampling density, ratio consistency holds under $N_{n} / n \to 0$ , including regimes with $N_{n}^{2} / n \to \infty$ . The paper also identifies the scalar statistic returned by a versioned clubSandwich CR2 calculation, gives an eight-unit witness with exact variance $1/7$ and expected CR2 value $2/7$ , and proves a positive-density lower bound: for a fixed group size $M \geq 2$ , a strictly positive limiting grouped-unit fraction $ρ > 0$ , an outcome envelope $B \geq 1$ , and a variance floor $c_{σ}$ below the separated independent-arm limit $1/ [M p (1 - p)] - 2 ρ / M$ , every measurable one-realization variance statistic has nonvanishing worst-case relative error over the bounded schedule class with those parameters.

Introduction

Random group formation is common in experiments where outcomes depend on who interacts with whom. Classrooms, teams, peer groups, neighborhoods, and online clusters can all be randomized objects rather than fixed sampling units. In such designs, the realized groups are typically disjoint: once a unit is placed in one group, it is removed from the pool available to the others. This finite-population dependence changes the variance target for a group-level treatment contrast, even when treatment is randomized across groups after the partition is formed.

This paper gives a design-based account of that variance target for homogeneous random partitions. The finite population has size $n$ , the common group size is fixed at $M$ , and $G_{n}$ disjoint groups are drawn uniformly before a balanced treatment assignment is applied across groups. Potential outcomes are deterministic functions of the treatment arm and the realized group. The estimand is the partition-average marginal effect, obtained by averaging the contrast of group-level potential-outcome tables over the uniform $M$ -slice of possible groups. This places random group formation inside the finite-population potential-outcome tradition of Splawa-Neyman et al. (1990), Fisher (1935), Cox (1958), Rubin (1974), and Holland (1986).

The central object is the covariance induced by drawing disjoint groups. On the uniform $M$ -slice, the normalized Kneser disjointness operator averages a group table over all groups disjoint from a given group. The Johnson association scheme diagonalizes this operator degree by degree. Theorem 1 uses that diagonalization to express the covariance of two centered group tables as a sum of Johnson harmonic inner products multiplied by finite- $n$ Kneser eigenvalues. Applied to the arm-difference table, this identity identifies the exact finite-population covariance term generated by group formation.

The exact design variance follows from combining this Kneser covariance with balanced treatment assignment. Theorem 2 establishes that the group-level difference in means is unbiased for the partition-average marginal effect and that its exact variance decomposes into an independent-group component plus ordered-disjoint covariance terms. The same theorem shows that the expected scalar equal-group CR2 statistic differs from the exact variance by exactly the negative of the Kneser covariance contrast. Thus the discrepancy between the usual cluster calculation and the finite-population randomization variance is determined by the geometry of the full potential group tables.

The asymptotic analysis studies triangular arrays with fixed $M$ , growing group count, stable treated-group fraction $p_{n} \to p \in (0, 1)$ , bounded potential outcomes, nondegenerate scaled exact variance, and grouped-unit sampling fraction $N_{n} / n \to ρ \in [0, 1]$ . Under these conditions, Theorem 3 gives the expansion $G_{n} σ_{n}^{2} = R_{n} - ρ E_{τ, 1, n} + o (1),$ where $R_{n}$ is the independent-group leading variance scale and $E_{τ, 1, n}$ is the degree-one Johnson energy of the arm-difference table. The degree-one term has a direct finite-population interpretation: it is the component of the treatment-control group-table contrast carried by marginal unit participation, and disjoint sampling makes that component contribute at first order whenever the limiting grouped-unit fraction is positive.

This expansion yields the CR2 phase frontier. Theorem 4 shows that the scalar equal-group CR2 statistic estimates $R_{n} / G_{n}$ in probability, while the exact variance uses the corrected scale $(R_{n} - ρ E_{τ, 1, n}) / G_{n}$ . The theorem gives a one-sided asymptotic conservativeness statement and characterizes ratio consistency by the relative-energy condition $\frac{ρ E _{τ, 1, n}}{R _{n} - ρ E _{τ, 1, n}} \to 0.$ At zero sampling density, Theorem 5 gives ratio consistency under $N_{n} / n \to 0$ , including the benchmark $N_{n} = M ⌊ n^{3/4} / M ⌋$ , for which $N_{n}^{2} / n \to \infty$ . This connects the dense calculation to the sparse intuition in Fu et al. (2026) while identifying the sampling fraction that governs the scalar variance ratio in the present fixed- $M$ random-partition setting.

The paper also relates the population calculation to applied regression software. In the equal-group design, Proposition 1 identifies the treatment-coordinate entry returned by clubSandwich::vcovCR with type CR2, for the stated unweighted intercept-plus-treatment regression and versioned sandwich bread convention, with the scalar statistic analyzed in the design theory. Proposition 2 then gives a finite eight-unit, four-pair, two-treated-group schedule in which the exact variance is $1/7$ and the expected CR2 statistic is $2/7$ . The witness makes the dense correction visible in a small balanced design.

Finally, the one-realization result gives an identification-theoretic interpretation of the dense correction. Proposition 3 constructs same-sign and independent-arm Rademacher schedule priors whose one-realization observed-data mixtures agree while their scaled exact variances converge to separated limits at positive density. Theorem 6 converts this comparison into a uniform lower bound over the dense bounded schedule class: for some positive $ε$ , every measurable statistic of the realized partition, assignment, and observed outcomes has worst-case relative error probability at least one half asymptotically. The obstruction is the degree-one cross-arm component of the potential group tables, which enters the exact variance but is not uniformly recoverable from a single realized grouping and assignment.

The formal statements and internal algebraic derivations are machine-checked in Lean 4; the verification appendix records the precise scope. The paper proceeds as follows. Section 2 places the results in the design-based, survey-sampling, cluster-robust, and interference literatures. Section 3 defines the random group-formation design, the partition-average marginal effect, the Johnson decomposition, and the scalar CR2 statistic. Section 4 proves the Kneser covariance identity and the finite-sample PAME variance formula. Section 5 derives the projection limit, the CR2 phase frontier, and the zero-density ratio result. Section 6 connects the scalar statistic to the versioned clubSandwich calculation and evaluates the eight-unit witness. Section 7 proves the one-realization obstruction, Section 8 summarizes the scope and extensions, and Section A collects the proofs and the verification note.

The paper belongs to the design-based tradition in causal inference, where treatment assignment is the source of randomness and potential outcomes are fixed features of a finite population (Splawa-Neyman et al., 1990; Fisher, 1935; Cox, 1958; Rubin, 1974; Holland, 1986). Its population target is a group-composition estimand: for a population of size $n$ and common group size $M$ , the analysis averages potential outcomes over the uniform $M$ -slice of possible groups. This places random group formation inside the same finite-population logic that underlies classical randomization inference, while making the composition of a treated or control group part of the assignment mechanism.

The asymptotic perspective is closest to survey-sampling triangular arrays, where the population may grow, the realized sample may occupy a nonvanishing fraction of it, and finite-population corrections can survive in the limit (Hájek, 1960; Cochran, 1977; Ohlsson, 1989; Fuller, 2009). The grouped-unit sampling fraction $N_{n}$ / $n$ plays that role here. Under the dense design studied in Definition 4, the number of realized groups $G_{n}$ diverges while $M$ is fixed, the treated-group fraction $p_{n}$ converges to an interior limit, and $N_{n} / n$ converges to a limit $ρ$ in the unit interval. The resulting variance formula retains the finite-population geometry induced by drawing disjoint groups, so the large-sample object is governed by both the usual independent-group variance scale and a correction determined by overlap in potential group tables.

The closest theorem-level comparison is Fu et al. (2026). For group interaction experiments with fixed or randomly formed groups, their Section 3 and Theorems 1–2 establish both asymptotic normality of the group-level contrast and ratio consistency of the CR2 variance estimator, under boundedness, their Assumption 1, and the sparse whole-tuple condition $N_{n}^{2} / n \to 0$ . That condition makes accidental reuse of population units across independently sampled tuples asymptotically negligible, so the finite-population disjointness geometry disappears from the limit and a single sparsity rate carries both conclusions. The present paper differs on three counts. It works in the homogeneous fixed- $M$ random group-formation subcase and keeps the exact disjointness geometry visible rather than assuming it away. Its subject is the variance object itself: the results characterize the exact design variance and the probability limit of the equal-group CR2 statistic, and Section 8 records what a complete inference theory would still require. And it replaces the whole-tuple rate by the grouped-unit sampling fraction: Theorem 4 shows that what governs the CR2 variance ratio in this subcase is $N_{n} / n$ , through the degree-one Johnson correction, and Theorem 5 delivers ratio consistency under $N_{n} / n \to 0$ alone, in particular on schedules with $N_{n}^{2} / n \to \infty$ that their condition excludes. Theorem 1 expresses that geometry through the Johnson-scheme decomposition of slice functions and the normalized Kneser disjointness operator, while Theorem 2 converts it into the exact variance of the group-level difference-in-means estimator. In the dense regime, Theorem 3 yields the expansion $G_{n} σ_{n}^{2} = R_{n} - ρ E_{τ, 1, n} + o (1)$ , where $R_{n}$ is the independent-group leading variance scale and $E_{τ, 1, n}$ is the degree-one Johnson energy of the arm-difference table. At zero sampling density, Theorem 4 gives the corresponding convergence of the scalar CR2 ratio, aligning the dense calculation with the sparse intuition when $N_{n} / n \to 0$ .

The algebra behind these comparisons draws on the Johnson association scheme and Kneser graph spectrum (Delsarte, 1973; Brouwer et al., 1989; Filmus, 2016; Brouwer et al., 2018). Those tools are used here as finite-population variance geometry. The group table $h_{z, n}$ records, for each treatment arm and possible group, the group-average potential outcome; its centered version and Johnson projections separate additive unit-level variation from higher-order composition variation. This decomposition is what makes the dense correction interpretable: the term involving $ρ$ is attached to the first Johnson component of the arm contrast, the part of the table most directly affected by removing units from the remaining pool after a group has been drawn.

The variance-estimation part of the paper connects to the cluster-robust covariance literature initiated by White (1980) and Liang et al. (1986), and to finite-sample and leverage adjustments for clustered least squares (Bell et al., 2002; Cameron et al., 2015; Abadie et al., 2023). The scalar statistic in Definition 12 is the equal-group analogue of the CR2 adjustment used in applied software. Two design-based points of contact deserve emphasis. Pustejovsky et al. (2018) develop bias-reduced linearization and Satterthwaite-type testing for fixed-effects models, and the CR2 adjustment they analyze is derived under an independent-cluster working covariance model; that working model is exactly what random group formation violates here, since drawing disjoint groups from a finite population correlates the realized group tables. The present results quantify the resulting gap rather than repairing the adjustment: Theorem 2 shows that the expected scalar CR2 statistic differs from the exact design variance by precisely the Kneser covariance contrast, which is the term the independent-cluster working model sets to zero. Su et al. (2021) give a design-based comparison of individual-level, cluster-average, and cluster-total regression analyses of cluster-randomized experiments, showing how the estimand and the robust standard error depend on cluster-size weighting and on the model-assisted structure imposed. Their clusters are fixed by the design; the object studied here is the additional variance geometry contributed by making the clusters themselves random and disjoint, at a common size $M$ that removes the cluster-size weighting question from the comparison. Proposition 1 gives a software-facing identity for the unweighted intercept-plus-treatment regression and the clubSandwich CR2 covariance calculation, tying the population calculation to the implementation line in Pustejovsky et al. (2018), Zeileis (2004), Zeileis (2006), Zeileis et al. (2020), Pustejovsky (2026), and Zeileis et al. (2026). This identity is useful because it pins down the scalar object consumed by standard regression software before the asymptotic comparison is made.

The design also sits near the literature on interference, exposure mappings, and group-formation experiments (Sobel, 2006; Hudgens et al., 2008; Tchetgen et al., 2012; Manski, 2013; Liu et al., 2014; Aronow et al., 2017; Ugander et al., 2013; Eckles et al., 2017; Athey et al., 2018; Li et al., 2019; Xu et al., 2021; Wang et al., 2025; Samii et al., 2023; Gao et al., 2025). That work clarifies how causal estimands change when a unit’s outcome can depend on peers, assignments in a neighborhood, or a realized exposure condition. Here the exposure condition is the realized group itself: the potential outcome $Y_{i, n} (z, A)$ , first introduced formally in Assumption 4, depends on the arm $z$ and the group $A$ . The random-partition design then supplies a tractable law over group compositions, making the population average marginal effect $τ_{n}$ and its estimator $τ_{n}$ design-based quantities.

Finally, the one-realization lower bound is related to finite-population variance nonidentification and conservative variance-estimation results (Aronow et al., 2014; Basse et al., 2018; Harshaw et al., 2026; Park et al., 2026) and sits alongside design-based randomization and permutation inference for interference settings (Basse et al., 2024; Puelz et al., 2022). Proposition 3 constructs two randomized schedule priors with identical one-realization observables and separated scaled variances, and Theorem 6 turns that separation into a lower bound for arbitrary one-realization variance statistics. Together with the exact variance and CR2 results, this positions the paper as a finite-population account of what random group formation contributes to variance geometry, what the standard scalar software statistic targets in the equal-group design, and what information a single realized partition contains about the design variance.

Setup and assumptions

Throughout, $n$ indexes the finite population size and $M$ is the fixed common group size. Row-dependent quantities carry an $n$ subscript, all limits are along the triangular array, and generic finite constants may change from line to line. Expectations, inner products, and norms below are finite-population objects taken over the uniform slice of possible groups.

Three row-level quantities recur in the conditions below and are fixed once here. The realized group count is $G_{n}$ ; the number of grouped units is $N_{n} = M G_{n},$ the total number of population units that end up inside a realized group; and $σ_{n}^{2} = Var (τ_{n})$ is the exact design variance of the group-level difference-in-means estimator of Definition 7, taken over the joint law of the realized groups and the treatment assignment. The asymptotic analysis rests on the number of realized groups and on the treatment, sampling, boundedness, and variance-scale restrictions imposed on the triangular array.

Assumption 1 [ass:group-count-growth] (Group-count growth).

The number of realized groups diverges: $G_{n} \to \infty.$

⊢ Lean

Assumption 1 is the growing number of randomized groups condition, a standard route for design-based asymptotics with many randomized clusters (Fu et al., 2026). It is the dimension along which the random partition supplies repeated group-level observations.

Definition 1 [synth_11] (Row treatment fraction).

For a triangular schedule array with row group count $G_{n}$ and treated-group count $G_{1 n}$ , where $0 < G_{1 n} < G_{n}$ , the row treatment fraction is $p_{n} = \frac{G _{1 n}}{G _{n}} .$

⊢ Lean

The number of treated groups $G_{1 n}$ determines the row treatment fraction in Definition 1; the number of control groups $G_{0 n}$ is the complementary count used in the difference-in-means estimator below.

Assumption 2 [ass:stable-treatment-fraction] (Stable treatment fraction).

The treated-group fraction $p_{n}$ converges to an interior limit: $p_{n} \to p \in (0, 1) .$

⊢ Lean

Assumption 2 is the stable complete-randomization arm fractions condition (Li et al., 2017). The interior limiting treated-group fraction $p$ keeps both treatment arms asymptotically represented in the randomized group assignment.

Assumption 3 [ass:sampling-fraction] (Sampling fraction limit).

The grouped-unit fraction $N_{n} / n$ converges: $\frac{N _{n}}{n} \to ρ \in [0, 1] .$

⊢ Lean

Assumption 3 is the finite-population sampling-fraction limit condition (Ohlsson, 1989). It records the limiting density of grouped units in the population, allowing the same notation to cover sparse and dense grouping regimes.

Assumption 4 [ass:bounded-potential-outcomes] (Bounded potential outcomes).

There is a finite uniform outcome envelope $B$ such that $n, i, z, A sup ∣ Y_{i, n} (z, A) ∣ \leq B < \infty.$

⊢ Lean

Assumption 4 is the uniformly bounded composition potential outcomes condition (Fu et al., 2026). The deterministic potential outcome $Y_{i, n} (z, A)$ may depend on the unit, arm, and realized group, while the uniform envelope $B$ supplies a common finite bound across rows.

Assumption 5 [ass:scaled-variance-nondegeneracy] (Scaled variance nondegeneracy).

For a feasible triangular schedule array with common group size $M \geq 2$ , positive group counts $G_{n}$ , treated-group counts satisfying $0 < G_{1 n} < G_{n}$ , grouped size $M G_{n} \leq n$ , and deterministic potential-outcome schedules, there is a scaled-variance lower-bound constant $c_{σ}$ such that $c_{σ} > 0$ and $c_{σ} \leq n \to \infty lim inf G_{n} σ_{n}^{2} .$

⊢ Lean

Assumption 5 is the nondegenerate scaled design variance condition (Li et al., 2017). The scaled-variance lower-bound constant $c_{σ}$ fixes the normalization used by the asymptotic variance comparisons.

We next define the finite-population design and the function spaces on which its variance geometry is expressed.

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

The treatment-arm set is the two-point set $Z = {0, 1} .$

⊢ Lean

The treatment-arm set $Z$ is used throughout for the two arms of the group-level potential-outcome tables.

Definition 3 [synth_1] (Feasible schedule array).

A feasible triangular schedule array with common group size $M$ consists of the following data:

(Group size.) A natural number $M$ satisfying $2 \leq M$ .

(Row sizes.) For each row $r \in N$ , a population size $n_{r} \in N$ , a number of groups $G_{r} \in N$ , and a number of treated groups $G_{1 r} \in N$ .
(Feasibility.) For every row $r$ , $0 < G_{r}, M G_{r} \leq n_{r}, 0 < G_{1 r}, G_{1 r} < G_{r}, G_{1 r} \leq G_{r} .$

(Potential-outcome schedule.) For every row $r$ , a deterministic potential-outcome schedule $Y_{r} : Ω_{n_{r}, M} \to {i \in {0, \dots, n_{r} - 1} : i \in A} \to Z \to R,$ where $A \in Ω_{n_{r}, M}$ is the realized group argument of $Y_{r}$ .

⊢ Lean

Definition 3 collects the rowwise feasibility restrictions used in the design: the group size is common, each row has positive groups and a nontrivial treated count, and the potential-outcome schedule is deterministic.

Definition 4 [def:random-partition-design] (Random partition design

(A_{n}, Z_{n})

Let $U_{n}$ be the finite population of $n$ labeled units, and let $Ω_{n, M} = {A \subseteq U_{n} : ∣ A ∣ = M} .$ The group tuple $A_{n} = (A_{1 n}, \dots, A_{G_{n} n})$ is drawn uniformly from all ordered $G_{n}$ -tuples of pairwise-disjoint elements of $Ω_{n, M}$ . Independently, the assignment vector $Z_{n}$ is drawn uniformly from all binary vectors with exactly $G_{1 n}$ treated groups.

⊢ Lean

Definition 4 defines the homogeneous random group-formation design. The ordered group tuple $A_{n}$ carves $G_{n}$ pairwise-disjoint groups of common size $M$ out of the finite population $U_{n}$ , and the balanced group-treatment assignment vector $Z_{n}$ is drawn independently conditional on the realized groups. The feasibility condition $N_{n} = M G_{n} \leq n$ allows the grouped units to occupy any fraction of the population. The realized groups therefore form a disjoint packing of $U_{n}$ : they are pairwise disjoint and each has size $M$ , and they cover the whole population exactly when $N_{n} = n$ . The general case, in which $n - N_{n}$ units lie outside every realized group and contribute no observation, is what gives the sampling fraction $N_{n} / n$ its range and is where the sparse and intermediate-density regimes studied below live. The design’s name, random partition, refers throughout to this packing mechanism; the saturated case $N_{n} = n$ is the special case in which it is literally a partition.

Definition 5 [def:group-table] (Group-level arm table

h_{z, n}

For each treatment arm $z \in Z$ and each group $A \in Ω_{n, M}$ , define the group-level arm table by $h_{z, n} (A) = \frac{1}{M} i \in A \sum Y_{i, n} (z, A) .$

⊢ Lean

The group-level arm table $h_{z, n}$ converts unit-level composition potential outcomes into the group mean observed when group $A$ receives arm $z$ .

Definition 6 [synth_3] (Uniform slice averaging).

For integers $M \leq n$ , let $Ω_{n, M} := {A \subseteq {1, \dots, n} : ∣ A ∣ = M} .$ The $M$ -slice design is the complete-randomization design on $Ω_{n, M}$ , equivalently the uniform distribution over all $M$ -element subsets of the $n$ -unit population. For any real-valued table $f : Ω_{n, M} \to R$ , write $E_{n} f := \frac{1}{∣ Ω _{n, M} ∣} A \in Ω_{n, M} \sum f (A) .$

⊢ Lean

The uniform $M$ -slice $Ω_{n, M}$ is the population of possible groups, and the averaging operator $E_{n}$ turns any group table into its finite-population slice mean.

Definition 7 [def:pame-estimator] (PAME and estimator

τ_{n}, τ_{n}

Define the finite-population partition-average marginal effect by $τ_{n} = E_{n} [h_{1, n} - h_{0, n}] .$ The difference-in-means estimator across treated and control groups is $τ_{n} = \frac{1}{G _{1 n}} g \sum Z_{n g} h_{1, n} (A_{n g}) - \frac{1}{G _{0 n}} g \sum (1 - Z_{n g}) h_{0, n} (A_{n g}) .$

⊢ Lean

Definition 7 defines the finite-population partition-average marginal effect and its realized group-level difference-in-means estimator. The estimand averages the contrast of the two arm tables over the full slice, while the estimator uses the treatment labels and realized groups produced by Definition 4.

Definition 8 [synth_12] (Uniform-slice

L^{2}

space).

For integers $n$ and $M$ with $2 M \leq n$ , let $U_{n} = {1, \dots, n}$ and $Ω_{n, M} = {A \subseteq U_{n} : ∣ A ∣ = M}$ be the uniform $M$ -slice. The space $L^{2} (Ω_{n, M})$ is the real vector space of functions $f : Ω_{n, M} \to R$ , equipped with uniform-slice expectation $E_{n} f = (M n)^{- 1} A \in Ω_{n, M} \sum f (A),$ inner product $⟨ f, g ⟩_{n} = E_{n} [f g],$ and induced norm $∥ f ∥_{n}^{2} = ⟨ f, f ⟩_{n}$ .

The inner product $⟨ \cdot, \cdot ⟩_{n}$ and induced norm $∥ \cdot ∥_{n}$ in Definition 8 provide the Hilbert-space notation used to decompose group tables by Johnson degree.

Definition 9 [def:johnson-decomposition] (Johnson orthogonal decomposition).

For integers $n, M$ with $2 M \leq n$ , let $Ω_{n, M} := {A \subseteq {1, \dots, n} : ∣ A ∣ = M}$ be the uniform $M$ -slice, let $E_{n}$ denote uniform averaging on $Ω_{n, M}$ , and let $⟨ f, g ⟩_{n} := E_{n} [f g]$ be the uniform-slice inner product. For each $k = 0, \dots, M$ , let $H_{n, k}$ be the canonical degree- $k$ Johnson harmonic subspace and let $Π_{n, k}$ be the orthogonal projection onto $H_{n, k}$ : $Π_{n, k}$ is linear, has range $H_{n, k}$ , fixes every element of $H_{n, k}$ , and satisfies $⟨ f - Π_{n, k} f, g ⟩_{n} = 0 for every g \in H_{n, k} .$ For every $f \in L^{2} (Ω_{n, M})$ , define its Johnson components by $f_{k} := Π_{n, k} f, k = 0, \dots, M .$ These components satisfy the centered decomposition $k = 1 \sum M Π_{n, k} f (A) = f (A) - E_{n} f for every A \in Ω_{n, M},$ and distinct degrees are orthogonal: $⟨ Π_{n, k} f, Π_{n, ℓ} g ⟩_{n} = 0 whenever k \neq = ℓ .$

⊢ Lean

The Johnson harmonic subspace $H_{n, k}$ and projection $Π_{n, k}$ organize a centered group table into orthogonal degrees. This is the representation-theoretic coordinate system for the exact variance identities below, following the Johnson and Kneser association-scheme perspective (Filmus, 2016; Brouwer et al., 2018).

Two derived slice quantities enter the next two definitions. For each arm $z$ , the centered arm table is $h_{z, n}^{\circ} = h_{z, n} - E_{n} h_{z, n},$ the group-level arm table of Definition 5 with its slice mean removed, as recorded in Definition 15; and the uniform-slice arm variance is its energy, $V_{z, n} = ∥ h_{z, n}^{\circ} ∥_{n}^{2} = E_{n} [(h_{z, n} - E_{n} h_{z, n})^{2}],$ the variance of the arm- $z$ group table under a single uniform draw from the slice. These are the only two objects needed to read the covariance and correction definitions that follow.

Definition 10 [def:kneser-covariance] (Kneser covariance

C_{ab, n}

For a function $f$ on $Ω_{n, M}$ , define the normalized Kneser disjointness operator by $(K_{n} f) (A) = (M n - M)^{- 1} C : C \cap A = \emptyset \sum f (C) .$ For arm tables $h_{a, n}$ and $h_{b, n}$ , define the ordered-disjoint covariance by $C_{ab, n} = ⟨ h_{a, n}^{\circ}, K_{n} h_{b, n}^{\circ} ⟩_{n} .$

⊢ Lean

Definition 10 records the covariance generated by sampling disjoint groups. The normalized disjointness operator $K_{n}$ averages over groups disjoint from a given group, while the centered arm table $h_{z, n}^{\circ}$ and ordered-disjoint covariance $C_{ab, n}$ isolate the finite-population dependence induced by the partition.

Definition 11 [def:dense-correction] (Dense correction terms

E_{τ, 1, n}, R_{n}

Define the degree-one Johnson energy of the arm-difference table by $E_{τ, 1, n} = ∥ Π_{n, 1} (h_{1, n} - h_{0, n}) ∥_{n}^{2} .$ Define the independent-group leading variance scale by $R_{n} = \frac{V _{1, n}}{p _{n}} + \frac{V _{0, n}}{1 - p _{n}} .$

⊢ Lean

The degree-one energy $E_{τ, 1, n}$ is the part of the arm-difference table carried by the linear Johnson component. The uniform-slice arm variance $V_{z, n}$ enters Definition 11 through the independent-group leading variance scale.

Definition 12 [def:cr2-statistic] (CR2 statistic

V_{CR2, n}

For each arm $z$ , let $s_{z, n}^{2}$ be the within-arm sample variance of the observed group means, computed with denominator $G_{z n} - 1$ . Define the scalar equal-group CR2 variance statistic by $V_{CR2, n} = \frac{s _{1, n}^{2}}{G _{1 n}} + \frac{s _{0, n}^{2}}{G _{0 n}} .$

⊢ Lean

The within-arm sample variance $s_{z, n}^{2}$ in Definition 12 is computed from observed group means within each assigned arm. The scalar CR2 statistic $V_{CR2, n}$ is therefore the equal-group cluster-robust variance quantity analyzed in the later software identity and asymptotic results.

The class defined next is named for the dense regime that motivates it, and its parameter $ρ$ ranges over the whole unit interval: arrays with $ρ = 0$ belong to it, and the results below treat $ρ = 0$ and $ρ > 0$ as the two phases of one statement.

Definition 13 [def:dense-schedule-class] (Dense schedule class).

The class $C_{dense}$ consists of triangular arrays $(Y_{i, n}, G_{n}, G_{1 n})_{n \geq 1}$ , with fixed common group size $M$ , for which:

(Feasible rows.) The common group size satisfies $M \geq 2$ . In each row, $G_{n} > 0$ , $N_{n} = M G_{n} \leq n$ , $0 < G_{1 n} < G_{n}$ , and $G_{1 n} \leq G_{n}$ . The potential-outcome schedule assigns a real value $Y_{i, n} (z, A)$ for every group $A \in Ω_{n, M}$ , every unit $i \in A$ , and every arm $z \in Z$ .

(Dense growth.) The group count satisfies Assumption 1, so $G_{n} \to \infty$ .

(Treatment fraction.) The treated-group fraction satisfies Assumption 2: for an interior limiting treated-group fraction $p$ , $0 < p < 1$ and $p_{n} \to p$ .

(Sampling fraction.) The grouped-unit sampling fraction satisfies Assumption 3: for a limiting grouped-unit sampling fraction $ρ$ , $0 \leq ρ \leq 1$ and $N_{n} / n \to ρ$ .

(Uniform envelope.) The potential outcomes satisfy Assumption 4: for a uniform envelope $B > 0$ , $n, A \in Ω_{n, M}, i \in A, z \in Z sup ∣ Y_{i, n} (z, A)∣ \leq B .$

(Scaled variance.) The exact design variance satisfies Assumption 5: for a scaled-variance lower-bound constant $c_{σ} > 0$ , $c_{σ} \leq n \to \infty lim inf G_{n} σ_{n}^{2} .$

Equivalently, $C_{dense} = {(Y_{i, n}, G_{n}, G_{1 n})_{n \geq 1} : G_{n} \to \infty, p_{n} \to p, N_{n} / n \to ρ, n, A \in Ω_{n, M}, i \in A, z \in Z sup ∣ Y_{i, n} (z, A)∣ \leq B, n \to \infty lim inf G_{n} σ_{n}^{2} \geq c_{σ}},$ with the row feasibility, interiority, closed-interval, envelope, and variance-floor conditions listed above.

⊢ Lean

The dense schedule class $C_{dense}$ packages the conditions in Assumptions 1, 2, 3, 4, and 5. It is the common domain for the dense asymptotic statements, combining feasible rows, a stable treatment split, a limiting grouped-unit fraction, bounded potential outcomes, and a positive scaled design-variance floor.

Exact variance geometry

The setup in Definitions 4, 5, and 7 makes the realized groups a sample of disjoint $M$ -subsets. The variance calculation therefore depends on two finite-population operations: centering each arm table on the uniform $M$ -slice and averaging a table over groups disjoint from a given group. This section records the exact algebra for those operations and then applies it to the design variance of $τ_{n}$ , the group-level difference-in-means estimator.

We first fix the realized arm counts and the centered table notation used in the covariance formulas.

Definition 14 [synth_9] (Realized arm group counts).

For $z \in Z = {0, 1}$ , let $G_{z, n} = g = 1 \sum G_{n} 1 {Z_{n g} = z}$ be the number of realized groups assigned to arm $z$ at row $n$ . Under the complete group-treatment assignment with exactly $G_{1 n}$ treated groups and $G_{0 n} = G_{n} - G_{1 n}$ control groups, this notation gives $G_{1, n} = G_{1 n}$ and $G_{0, n} = G_{0 n}$ .

Definition 14 aligns the random-assignment notation with the fixed arm counts from Definition 4. In the balanced complete group assignment used throughout the paper, the realized counts equal the design counts, so later variance expressions may use $G_{1 n}$ and $G_{0 n}$ directly.

Definition 15 [synth_5] (Centered arm table).

For integers $n$ and $M$ with $M \leq n$ , let $Ω_{n, M} = {A \subseteq {1, \dots, n} : ∣ A ∣ = M} .$ Given a deterministic potential-outcome schedule $Y_{i, n} (z, A)$ for units $i \in A$ , arms $z \in Z$ , and groups $A \in Ω_{n, M}$ , define the centered arm- $z$ group table by $h_{z, n}^{\circ} (A) = h_{z, n} (A) - E_{n} [h_{z, n}]$ for each $A \in Ω_{n, M}$ , where $h_{z, n} (A) = \frac{1}{M} i \in A \sum Y_{i, n} (z, A), E_{n} [h_{z, n}] = \frac{1}{∣ Ω _{n, M} ∣} B \in Ω_{n, M} \sum h_{z, n} (B) .$

⊢ Lean

The centered table in Definition 15 isolates the part of an arm-specific group mean that can covary across disjoint realized groups. The centering is with respect to the uniform slice, matching the estimand in Definition 7 and the ordered-disjoint covariance in Definition 10.

Definition 16 [synth_4] (Uniform-slice norm).

For integers $M \leq n$ , let $Ω_{n, M} := {A \subseteq {1, \dots, n} : ∣ A ∣ = M} .$ For any real-valued function $f : Ω_{n, M} \to R$ , define its squared uniform-slice norm by $∥ f ∥_{n}^{2} := ⟨ f, f ⟩_{n} := E_{n} {f (A)^{2}},$ where $E_{n}$ denotes averaging over the uniform law on $Ω_{n, M}$ .

⊢ Lean

Definition 16 supplies the norm in which Johnson harmonic components are measured. Because the inner product averages over all candidate groups of size $M$ , these energies describe finite-population variation before the random partition selects the realized disjoint groups.

The next result gives the spectral identity that turns disjointness dependence into degree-by-degree covariance terms. Its constants are the normalized Kneser eigenvalues, obtained from the classical Johnson association-scheme spectrum (Delsarte, 1973; Brouwer et al., 1989; Brouwer et al., 2018); the harmonic decomposition follows the standard slice analysis of Boolean functions (Filmus, 2016).

Theorem 1 [thm:exact-kneser-identity] (Exact Kneser covariance identity).

Let $M, n \in N$ satisfy $2 \leq M$ and $2 M \leq n$ . Let $Y_{i, n} (z, A)$ be a deterministic potential-outcome schedule for units $i \in A$ , arms $z \in Z$ , and groups $A \in Ω_{n, M}$ , with group-level arm tables $h_{z, n}$ as in Definition 5. Suppose the following conditions hold.

(Johnson projections.) For each $k = 0, \dots, M$ , $Π_{n, k}$ is a linear projection on functions $f : Ω_{n, M} \to R$ whose range is the degree- $k$ Johnson harmonic subspace $H_{n, k}$ , which fixes every element of $H_{n, k}$ , and whose residual $f - Π_{n, k} f$ is orthogonal to $H_{n, k}$ under the uniform-slice inner product $⟨ u, v ⟩_{n} = E_{n} [u (A) v (A)]$ .

(Centered orthogonal decomposition.) For every $f : Ω_{n, M} \to R$ and $A \in Ω_{n, M}$ , $k = 1 \sum M Π_{n, k} f (A) = f (A) - E_{n} f (A),$ and the projected components are mutually orthogonal: if $k \neq = ℓ$ , then $⟨ Π_{n, k} f, Π_{n, ℓ} g ⟩_{n} = 0$ for all $f, g : Ω_{n, M} \to R$ .

(Kneser spectrum.) For every $k = 0, \dots, M$ and every $f \in H_{n, k}$ , the unnormalized Kneser adjacency operator has eigenvalue $(- 1)^{k} (M - k n - M - k) .$

Then the normalized Kneser disjointness operator $K_{n}$ acts on each projected component by $K_{n} (Π_{n, k} f) (A) = λ_{n, k} Π_{n, k} f (A), λ_{n, k} = (- 1)^{k} \frac{( M ) _{k}}{( n - M ) _{k}},$ for every $k = 0, \dots, M$ , every $f : Ω_{n, M} \to R$ , and every $A \in Ω_{n, M}$ . Moreover, if $f, g : Ω_{n, M} \to R$ are centered under the uniform $M$ -slice, then for a uniform ordered disjoint pair $(A, C)$ , $Cov {f (A), g (C)} = k = 1 \sum M λ_{n, k} ⟨ Π_{n, k} f, Π_{n, k} g ⟩_{n} .$ Finally, the ordered-disjoint covariance of the arm-difference table satisfies $C_{τ τ, n} = k = 1 \sum M λ_{n, k} Π_{n, k} (h_{1, n} - h_{0, n})_{n}^{2} .$

⊢ Lean

Theorem 1 shows that disjoint group formation has an exact finite-sample diagonalization in Johnson degrees. Each degree contributes its harmonic inner product multiplied by the signed finite- $n$ factor $λ_{n, k}$ , so the covariance retained by sampling groups without replacement is completely summarized by the slice energies of the projected arm tables. Applied to the arm-difference table, the same identity gives $C_{τ τ, n}$ , the ordered-disjoint covariance contrast that enters the variance comparison below.

The exact variance formula combines this disjointness covariance with the complete-randomization variation across treatment labels. The definitions in Definitions 15 and 14 make the statement entirely finite-sample: the arm variances $V_{z, n}$ , the ordered-disjoint covariances $C_{ab, n}$ , and the independent-group scale $R_{n}$ are all computed from the deterministic row schedule.

Theorem 2 [thm:exact-pame-variance] (Exact PAME variance).

Let $n, M, G_{n}, G_{1 n}$ be natural numbers and let $G_{0 n} = G_{n} - G_{1 n}$ . Suppose that:

(Feasible partition.) The two-stage random partition design in Definition 4 is feasible: $M G_{n} \leq n$ .

(Group sizes.) $2 \leq M$ , $2 \leq G_{1 n}$ , and $2 \leq G_{0 n}$ .

(Potential outcomes.) $Y_{i, n} (z, A)$ is a deterministic potential-outcome schedule, defined for every $A \in Ω_{n, M}$ , every $i \in A$ , and every $z \in Z$ .

Set $V_{z, n} = Var_{A \sim Unif (Ω_{n, M})} {h_{z, n} (A)}, C_{ab, n} = E_{A} E_{C ∣ C \cap A = \emptyset} [h_{a, n}^{\circ} (A) h_{b, n}^{\circ} (C)],$ and $C_{τ τ, n} = C_{11, n} + C_{00, n} - 2 C_{10, n}, R_{n} = \frac{V _{1, n}}{G _{1 n} / G _{n}} + \frac{V _{0, n}}{1 - G _{1 n} / G _{n}} .$ For the difference-in-means estimator $τ_{n}$ , the finite-population PAME $τ_{n}$ , the exact design variance $σ_{n}^{2} = Var (τ_{n})$ , and the scalar equal-group CR2 statistic $V_{CR2, n}$ in Definition 12, $E [τ_{n}] = τ_{n},$ $σ_{n}^{2} = \frac{R _{n}}{G _{n}} + C_{τ τ, n} - \frac{C _{11, n}}{G _{1 n}} - \frac{C _{00, n}}{G _{0 n}},$ $E [V_{CR2, n}] = \frac{V _{1, n} - C _{11, n}}{G _{1 n}} + \frac{V _{0, n} - C _{00, n}}{G _{0 n}},$ and $E [V_{CR2, n}] - σ_{n}^{2} = - C_{τ τ, n} .$

⊢ Lean

Theorem 2 establishes three finite-sample facts for the two-stage design. First, the group difference in means is unbiased for the finite-population PAME. Second, the exact design variance separates an independent-group component, $R_{n} / G_{n}$ , from the ordered-disjoint covariance terms induced by the random partition. Third, the scalar equal-group CR2 expectation differs from the exact variance by exactly $- C_{τ τ, n}$ . Thus the sign and magnitude of the CR2 discrepancy are governed by the same Kneser covariance contrast characterized in Theorem 1.

Dense and sparse variance behavior

The exact identities in Theorems 1 and 2 reduce the large-population question to the behavior of Johnson energies under random grouping. In dense arrays, where a positive fraction of the finite population may be grouped, the first Johnson degree carries the leading correction to the independent-group variance scale. The higher degrees remain present in the finite-sample identity, but their aggregate contribution is uniformly of smaller order under the bounded-outcome and fixed-group-size conditions.

A word on how to read the statements below. Each theorem carries its Johnson-projection, orthogonal-decomposition, and Kneser-spectrum clauses explicitly, because the verified statements quantify over the projections rather than fixing them. Those three clauses are not extra economic assumptions: they hold automatically for the canonical Johnson projections on the uniform $M$ -slice whenever $2 M \leq n$ , by Lemmas 3 and 2, which are proved in Section A. The substantive conditions are only the four array conditions of Section 3: growing group count, stable treatment fraction, converging sampling fraction, and bounded potential outcomes. A reader may take the projection clauses as given and read each theorem as a statement about arrays satisfying those four conditions alone.

Theorem 3 [thm:dense-projection-limit] (Dense projection limit).

Fix a common group size $M \geq 2$ and real numbers $p$ , $ρ$ , and $B$ . There is a constant $C > 0$ such that, for every feasible triangular schedule array with common group size $M$ and every rowwise choice of Johnson projections $Π_{n, k}$ on $L^{2} (Ω_{n, M})$ , the following conditions imply the displayed limits below:

(Group growth.) The array satisfies Assumption 1.

(Treatment fractions.) The array satisfies Assumption 2 with limiting treated-group fraction $p$ .

(Sampling fractions.) The array satisfies Assumption 3 with limiting grouped-unit fraction $ρ$ .

(Bounded outcomes.) The array satisfies Assumption 4 with uniform outcome envelope $B$ .

(Johnson decomposition.) In every row with $2 M \leq n$ , the projections give the centered orthogonal Johnson decomposition $k = 1 \sum M Π_{n, k} f (A) = f (A) - E_{n} f$ for every $f$ and every $A \in Ω_{n, M}$ , and distinct Johnson degrees are orthogonal under $⟨ \cdot, \cdot ⟩_{n}$ .

(Kneser spectrum.) In every row with $2 M \leq n$ , every $f \in H_{n, k}$ is an eigenfunction of the unnormalized Kneser adjacency operator with eigenvalue $(- 1)^{k} (M - k n - M - k) .$

Then $G_{n} σ_{n}^{2} - (R_{n} - ρ E_{τ, 1, n}) \to 0,$ $G_{n} C_{τ τ, n} + ρ E_{τ, 1, n} \to 0,$ and $\frac{C _{11, n}}{p _{n}} + \frac{C _{00, n}}{1 - p _{n}} \to 0.$ Moreover, for every row $n$ , the pooled contribution of Johnson degrees $k \geq 2$ , $G_{n} k = 2 \sum M λ_{n, k} Π_{n, k} (h_{1, n} - h_{0, n})_{n}^{2},$ has absolute value at most $C / n$ .

⊢ Lean

The theorem identifies the dense correction as the product of the grouped-unit sampling limit and the degree-one contrast energy $E_{τ, 1, n}$ . Intuitively, degree one records the part of the arm-difference table that is visible through the marginal participation of individual population members in sampled groups. Sampling without replacement induces competition for those members across groups, and the limit in Theorem 3 converts that competition into the correction $- ρ E_{τ, 1, n}$ to the scaled exact variance. The final bound gives the corresponding uniform remainder statement for Johnson degrees at least two, so the first-order dense comparison is governed by the degree-one projection.

This projection expansion feeds directly into the behavior of the equal-group CR2 statistic. The statistic $V_{CR2, n}$ is the usual scalar cluster-robust variance estimator for the difference in group means in this balanced design, matching the equal-group CR2 form used in finite-sample cluster-robust inference (Pustejovsky et al., 2018). The next result states its probability limit and the exact criterion under which the conservative dense correction vanishes relative to the target variance.

Theorem 4 [thm:cr2-phase-frontier] (CR2 phase frontier).

Let $M \geq 2$ , and let $A$ be a triangular array of feasible random-group experiment rows with population sizes $n$ , group counts $G_{n} > 0$ , treated-group counts $0 < G_{1 n} < G_{n}$ , grouped-unit counts $N_{n} = M G_{n} \leq n$ , and deterministic potential-outcome schedules. Fix constants $p, ρ, B, c_{σ} \in R$ . Suppose that:

(Dense array.) The array $A$ belongs to the dense bounded schedule class $C_{dense}$ in Definition 13, with parameters $p, ρ, B, c_{σ}$ .

(Johnson projections.) For every row $n$ , the spaces $L^{2} (Ω_{n, M})$ are equipped with linear projections $Π_{n, k}$ , $0 \leq k \leq M$ , whose ranges are the degree- $k$ Johnson harmonic subspaces $H_{n, k}$ , which fix functions in their ranges and have residuals orthogonal to $H_{n, k}$ under $⟨ \cdot, \cdot ⟩_{n}$ .

(Orthogonal decomposition.) For every row with $2 M \leq n$ , every $f \in L^{2} (Ω_{n, M})$ , and every $A \in Ω_{n, M}$ , $k = 1 \sum M Π_{n, k} f (A) = f (A) - E_{n} f,$ and distinct Johnson components are orthogonal: $⟨ Π_{n, k} f, Π_{n, ℓ} g ⟩_{n} = 0 whenever k \neq = ℓ .$

(Kneser spectrum.) For every row with $2 M \leq n$ , every $0 \leq k \leq M$ , and every $f \in H_{n, k}$ , the unnormalized Kneser adjacency operator satisfies $C \cap A = \emptyset \sum f (C) = (- 1)^{k} (M - k n - M - k) f (A) .$

Then, as $n \to \infty$ , $G_{n} V_{CR2, n} - R_{n} p 0$ and $G_{n} (V_{CR2, n} - σ_{n}^{2}) - ρ E_{τ, 1, n} p 0.$ Moreover, for every $ε > 0$ , $Pr {V_{CR2, n} / σ_{n}^{2} < 1 - ε} ⟶ 0,$ and the ratio $V_{CR2, n} / σ_{n}^{2}$ converges in probability to $1$ if and only if $\frac{ρ E _{τ, 1, n}}{R _{n} - ρ E _{τ, 1, n}} ⟶ 0.$

⊢ Lean

Theorem 4 says that CR2 estimates the independent-group scale $R_{n} / G_{n}$ in probability, while the exact design variance subtracts the dense projection correction. Consequently, the statistic is asymptotically conservative for the exact variance in the one-sided probability sense stated in the theorem. Its ratio consistency is characterized by a single relative-energy condition: the dense correction $ρ E_{τ, 1, n}$ must be negligible compared with the corrected scaled variance $R_{n} - ρ E_{τ, 1, n}$ . This gives a diagnostic interpretation to the Johnson decomposition in Definition 9: degree-one heterogeneity in the arm contrast is precisely the component that determines whether the usual CR2 standard error is sharp in dense random-group designs.

The sparse case follows by setting the grouped-unit sampling fraction to zero. In that regime, the same theorem conditions allow many realized groups while making the first-order finite-pool correction vanish at the scale relevant for the variance ratio. The final result records this implication and isolates the benchmark count sequence in which $N_{n} / n \to 0$ even though $N_{n}^{2} / n \to \infty$ .

Theorem 5 [thm:sparse-beyond-birthday] (Sparse birthday consistency).

Fix an integer $M \geq 2$ . Then the following statements hold.

(Sparse dense arrays.) For every feasible triangular schedule array with common group size $M$ , if the array belongs to $C_{dense}$ in Definition 13 with limiting grouped-unit fraction $ρ = 0$ , then $\frac{V _{CR2, n}}{σ _{n}^{2}} p 1.$
(Birthday counts.) With $N_{n}^{bd} = M ⌊ \frac{n ^{3/4}}{M} ⌋,$ the benchmark counts satisfy $N_{n}^{bd} \leq n$ for all sufficiently large $n$ , $\frac{N _{n}^{bd}}{n} \to 0, \frac{( N _{n}^{bd} ) ^{2}}{n} \to \infty.$

(Birthday-aligned arrays.) For every feasible triangular schedule array with common group size $M$ , if its grouped-unit count satisfies $N_{n} = M ⌊ \frac{n ^{3/4}}{M} ⌋$ row by row and the array satisfies Assumptions 1, 2, 4, and 5 for some $p$ , $B$ , and $c_{σ}$ , then $\frac{V _{CR2, n}}{σ _{n}^{2}} p 1.$

⊢ Lean

The sparse result separates the variance question from whole-design collision heuristics. What matters for the scalar PAME variance is the grouped-unit fraction $N_{n} / n$ , and Theorem 5 establishes ratio consistency whenever that fraction converges to zero within the stated dense schedule class. The explicit sequence $N_{n} = M ⌊ n^{3/4} / M ⌋$ gives a concrete regime with vanishing sampling fraction and diverging $N_{n}^{2} / n$ . Thus CR2 remains ratio-consistent for the exact design variance in a range where the experiment still uses many overlapping opportunities in the underlying finite population.

Software identity and finite witness

The preceding results analyze the scalar equal-group CR2 statistic in Definition 12. This section records how that scalar statistic is obtained from a standard software call in the equal-group design, then gives a fully finite calculation that fixes the sign and magnitude of the dense correction. The software statement is deliberately versioned: the relevant covariance entry is the treatment-coordinate entry returned by clubSandwich for an unweighted intercept-plus-treatment regression using the sandwich bread convention (Pustejovsky, 2026; Zeileis et al., 2026; Zeileis, 2004; Zeileis, 2006; Zeileis et al., 2020; Pustejovsky et al., 2018).

Definition 17 [def:eight-unit-witness] (Eight-unit witness

a_{8}

The eight-unit witness fixes $n = N_{n} = 8, M = 2, G_{n} = 4, G_{1 n} = 2,$ and uses the balanced sign vector $a_{8} = (a_{1}, \dots, a_{8}) .$ For every group $A = {j, k}$ and every unit $i \in A$ , the potential outcomes are $Y_{i, n} (0, A) = 0, Y_{i, n} (1, A) = \frac{a _{j} + a _{k}}{2} .$

⊢ Lean

Proposition 1 identifies the population-design statistic with the coefficient variance delivered by the stated vcovCR call. The row-identification and outcome clauses align the regression rows with the realized groups in Definition 4; the design-matrix and unweighted-fit clauses make the treatment coefficient equal to the group-level treated-control contrast in Definition 7. The block-algebra and bread-scaling clauses then pin down the CR2 adjustment and the normalization used by the versioned software implementation.

The sign vector in Definition 17 is balanced in the sense that half of its entries equal $+ 1$ and half equal $- 1$ ; the verified witness takes the canonical representative $a_{i} = + 1 (1 \leq i \leq 4), a_{i} = - 1 (5 \leq i \leq 8),$ so that $\sum_{i = 1}^{8} a_{i} = 0$ . The numbers reported below are computed for this representative. The finite calculation below specializes the design to eight units, four pairs, and two treated groups. It provides a small balanced schedule in which the exact variance components and the expected CR2 statistic can be evaluated without asymptotics.

Proposition 1 [prop:clubsandwich-consumer] (CR2 software identity).

Suppose $M \geq 2$ , $G_{1 n} \geq 2$ , and $G_{0 n} \geq 2$ . Fix a deterministic potential-outcome schedule $Y_{i, n} (z, A)$ , an ordered tuple $A_{n}$ of pairwise-disjoint realized groups of common size $M$ , and a balanced group-treatment assignment vector $Z_{n}$ with $G_{1 n}$ treated groups and $G_{0 n} = G_{n} - G_{1 n}$ control groups. Assume the software regression data satisfy the following conditions.

(Row identification.) For each realized group, the $M$ regression rows are in bijection with the units in that group.

(Design matrix.) The fitted model matrix has exactly two columns, an intercept and the numeric binary group-treatment regressor: $X_{g ij} = {1, 1 {Z_{g} = 1}, j = 0, j = 1.$

(Observed outcomes.) The regression outcome in row $i$ of group $g$ is the realized potential outcome $Y_{i, n} (Z_{g}, A_{g})$ , and its within-group average equals the observed group mean.

(Unweighted fit.) The fit is an unweighted full-column-rank least-squares fit, with residuals $e_{g i}$ , and the average residual in each group equals the observed group mean minus the observed mean in that group’s treatment arm.

(Block algebra.) The stacked cross-product satisfies $X^{T} X = \sum_{g} X_{g}^{T} X_{g}$ , the group hat matrices are $H_{g} = X_{g} (X^{T} X)^{- 1} X_{g}^{T},$ each $I - H_{g}$ is positive definite, and each CR2 adjustment $A_{g}$ is symmetric positive definite with $A_{g} A_{g} (I - H_{g}) = I .$

(Bread scaling.) The matrix used by the CR2 covariance calculation is $B = (G_{n} M)^{- 1} B$ , where $B$ is the unweighted $sandwich :: bread (fit)$ matrix.

Let $Σ$ be the covariance matrix returned by $clubSandwich :: vcovCR (fit, cluster = group, type =^{'} CR 2^{'})$ in version $0.7.0$ , with $target$ , $inverse_var$ , and $form$ omitted, applied to this unweighted intercept-plus-treatment fit using $sandwich$ version $3.1 - 3$ for the bread. Then the treatment-coordinate entry equals the scalar equal-group CR2 statistic in Definition 12: $Σ_{11} = V_{CR2, n} = \frac{s _{1, n}^{2}}{G _{1 n}} + \frac{s _{0, n}^{2}}{G _{0 n}} .$

⊢ Lean

The witness in Definition 17 makes treatment outcomes depend only on the average sign within the realized pair, while control outcomes are identically zero. Balance of $a_{8}$ gives a concrete degree-one component in the treated arm table, so the exact finite-pool correction in Theorem 2 has a visible numerical effect.

Proposition 2 [prop:eight-unit-witness] (Eight-unit witness moments).

For the balanced eight-unit witness schedule with $n = N_{n} = 8$ , $M = 2$ , $G_{n} = 4$ , and $G_{1 n} = 2$ , suppose that:

(Johnson projections.) There is a system of orthogonal projections ${Π_{8, k}}_{k = 0}^{2}$ onto the canonical Johnson harmonic spaces $H_{8, k}$ in $L^{2} (Ω_{8, 2})$ .

(Centered decomposition.) These projections decompose every $f \in L^{2} (Ω_{8, 2})$ after removal of its uniform-slice mean, with different harmonic degrees orthogonal under $⟨ \cdot, \cdot ⟩_{n}$ .

(Kneser spectrum.) The unnormalized Kneser adjacency operator acts on each $H_{8, k}$ by the eigenvalue $(- 1)^{k} (2 - k 8 - 2 - k) .$

Then the witness satisfies $V_{1, n} = \frac{3}{7}, E_{τ, 1, n} = \frac{3}{7}, C_{11, n} = - \frac{1}{7}, σ_{n}^{2} = \frac{1}{7},$ and, for the random partition design in Definition 4 and the scalar equal-group CR2 statistic in Definition 12, $E [V_{CR2, n}] = \frac{2}{7} .$

⊢ Lean

Proposition 2 shows that the finite design variance is $1/7$ , while the expected equal-group CR2 statistic is $2/7$ . The same calculation reports $V_{1, n} = E_{τ, 1, n} = 3/7$ and $C_{11, n} = - 1/7$ , matching the geometry in Theorem 1: the treated table’s degree-one energy generates a negative ordered-disjoint covariance, and that covariance enters the exact variance through the dense correction. Thus the witness supplies a concrete numerical check on both the Kneser covariance normalization and the software-facing CR2 statistic before the one-realization lower bound studied next.

One-realization lower bound

The finite witness in Proposition 2 shows how the dense correction can move the exact variance away from the equal-group CR2 target in a small design. This section turns that calculation into a positive-density impossibility statement for one-realization variance recovery. The construction compares two randomized schedule priors whose induced observed-data mixtures agree for every statistic of the realized groups, assignments, and observed outcomes, while their scaled exact variances concentrate at separated limits.

We first record the observed object and the two sign priors used in the comparison.

Definition 18 [synth_8] (One-realization observation).

A one-realization observation $O_{n}$ at population size $n$ , common group size $M$ , realized group count $G_{n}$ , and treated-group count $G_{1 n}$ is a triple $O_{n} = (A_{n}, Z_{n}, Y_{n}^{obs})$ with the following components:

(Partition.) $A_{n} = (A_{g, n})_{g = 1}^{G_{n}}$ is an ordered tuple with $A_{g, n} \in Ω_{n, M}$ for every $g$ , and $A_{g, n} \cap A_{g^{'}, n} = \emptyset$ whenever $g \neq = g^{'}$ .

(Treatment allocation.) $Z_{n}$ selects a subset of the realized groups with exactly $G_{1 n}$ elements.

(Observed outcomes.) For every realized group $g$ and every unit $i \in A_{g, n}$ , $Y_{n}^{obs}$ assigns a real observed outcome $Y_{i, g, n}^{obs} \in R$ .

⊢ Lean

Definition 18 fixes the sigma-field available to a one-realization procedure: the sampled partition, the group treatment allocation, and the observed unit outcomes within sampled groups. It matches the information used by the design estimator in Definition 7 and by the equal-group CR2 statistic in Definition 12, but it treats the variance statistic itself as an arbitrary measurable function of the realized data.

Definition 19 [synth_7] (Independent sign prior).

For a population size $n$ , $H_{n}^{ind}$ is the product finite design on arrays $h : {1, \dots, n} \times {0, 1} \to {0, 1}$ under which every unit-arm coordinate is drawn independently from the fair two-point law: $H_{n}^{ind} = (i, z) \in {1, \dots, n} \times {0, 1} ⨂ Bernoulli (\frac{1}{2}) .$

⊢ Lean

Definition 20 [synth_6] (Same-sign schedule prior).

For each $n$ , $H_{n}^{same}$ is the finite product design on Boolean schedules $h : {1, \dots, n} \to {0, 1}$ whose coordinate design at every $i \in {1, \dots, n}$ is the fair coin design: $H_{n}^{same} := i \in {1, \dots, n} ⨂ Coin (\frac{1}{2}) .$

⊢ Lean

Both priors are stated on Boolean coordinates, and a Boolean draw becomes a potential-outcome schedule through the sign map $ε (0) = - 1, ε (1) = + 1.$ Given a common-sign draw $u : {1, \dots, n} \to {0, 1}$ from $H_{n}^{same}$ , the induced schedule is additive and arm-free, $Y_{i, n} (z, A) = ε (u_{i}) for every arm z and every group A ∋ i,$ so the same unit sign is carried into both arms. Given an arm-specific draw $u : {1, \dots, n} \times {0, 1} \to {0, 1}$ from $H_{n}^{ind}$ , the induced schedule is $Y_{i, n} (z, A) = ε (u_{i, z}),$ with the two arms drawn independently. Both induced schedules take values in ${- 1, + 1}$ and are additive: the potential outcome of unit $i$ does not depend on the composition of the group it lands in. Consequently every group table is an average of $M$ independent signs, which is what produces the arm variances $V_{z, n} \to 1/ M$ quoted in the proposition. The independent prior in Definition 19 randomizes unit signs separately by treatment arm; the same-sign prior in Definition 20 uses a common unit sign across arms. Both priors generate bounded Boolean schedules, but they place different mass on the degree-one arm-difference energy in Definition 11. That difference is invisible after observing only the assigned arm in a single realization.

Proposition 3 [prop:rademacher-mixture-separation] (Rademacher mixture separation).

Fix a common group size $M \geq 2$ . Let $A$ be a feasible triangular array with row population sizes $n$ , group counts $G_{n}$ , treated-group counts $G_{1 n}$ , $0 < G_{1 n} < G_{n}$ , $M G_{n} \leq n$ , and deterministic schedules. Let $p \in R$ and let $ρ$ , the limiting grouped-unit fraction, satisfy $ρ > 0$ . Suppose:

(Group growth.) The array satisfies Assumption 1.

(Treatment fractions.) The treated-group fractions satisfy Assumption 2 with limit $p$ .

(Sampling fractions.) The grouped-unit fractions satisfy Assumption 3 with limit $ρ$ .

(Johnson projections.) For every row $n$ , the canonical Johnson projections $Π_{n, k}$ on $L^{2} (Ω_{n, M})$ are linear orthogonal projections onto $H_{n, k}$ , fix $H_{n, k}$ , and have residuals orthogonal to $H_{n, k}$ .

(Johnson decomposition.) For every row with $2 M \leq n$ , every $f \in L^{2} (Ω_{n, M})$ , and every $A \in Ω_{n, M}$ , $1 \leq k \leq M \sum Π_{n, k} f (A) = f (A) - E_{n} f,$ and distinct Johnson degrees are orthogonal under $⟨ \cdot, \cdot ⟩_{n}$ .

(Kneser spectrum.) For every row with $2 M \leq n$ , every $0 \leq k \leq M$ , and every $f \in H_{n, k}$ , the unnormalized Kneser adjacency operator satisfies $C \in Ω_{n, M} : C \cap A = \emptyset \sum f (C) = (- 1)^{k} (M - k n - M - k) f (A) .$

Then, for every row $n$ and every statistic $φ$ of the one-realization observation $O_{n}$ , $E_{H_{n}^{same}} E_{Z_{n}} {φ (O_{n})} = E_{H_{n}^{ind}} E_{Z_{n}} {φ (O_{n})} .$ Moreover, under $H_{n}^{same}$ , $V_{1, n} ⟶ p \frac{1}{M}, V_{0, n} ⟶ p \frac{1}{M}, E_{τ, 1, n} ⟶ p 0, G_{n} σ_{n}^{2} ⟶ p \frac{1}{M p ( 1 - p )} .$ Under $H_{n}^{ind}$ , $E_{τ, 1, n} ⟶ p \frac{2}{M}, G_{n} σ_{n}^{2} ⟶ p \frac{1}{M p ( 1 - p )} - \frac{2 ρ}{M} .$ The two scaled-variance limits are separated by a positive gap: $0 < \frac{2 ρ}{M}, \frac{2}{M} \leq \frac{1}{M p ( 1 - p )} - \frac{2 ρ}{M} .$ Consequently, for every fixed $c_{σ} \in R$ satisfying $0 < c_{σ} < \frac{1}{M p ( 1 - p )} - \frac{2 ρ}{M},$ the lower-tail probabilities satisfy $H_{n}^{same} Pr {G_{n} σ_{n}^{2} \geq c_{σ}} \to 1, H_{n}^{ind} Pr {G_{n} σ_{n}^{2} \geq c_{σ}} \to 1.$

⊢ Lean

Proposition 3 isolates the information loss created by one realized treatment assignment. Every statistic of the one-realization observation $O_{n}$ has the same mixture expectation under $H_{n}^{same}$ and $H_{n}^{ind}$ , yet the exact-variance limit changes by $2 ρ / M$ . The equal observed-data mixture reflects the fact that each observed unit contributes only its assigned-arm sign; the variance separation comes from the unobserved cross-arm alignment, which enters Theorem 2 through the degree-one term $E_{τ, 1, n}$ . In positive-density designs, the grouped-unit fraction $ρ$ keeps that term on the same scale as the leading variance.

The next result converts the mixture separation into a uniform lower bound over the dense schedule class. It conditions the two priors on high-probability deterministic supports, so the comparison is stated directly over arrays in $C_{dense}$ from Definition 13.

Theorem 6 [thm:qv-diagonal-impossibility] (Diagonal variance obstruction).

Fix a common group size $M$ with $2 \leq M$ , and let $A$ be a triangular schedule array with population sizes $n$ , group counts $G_{n} > 0$ , treated-group counts $0 < G_{1 n} < G_{n}$ , $M G_{n} \leq n$ , and deterministic potential-outcome rows. Let $p, ρ, B, c_{σ} \in R$ . Suppose:

(Envelope and fractions.) $0 < ρ$ , $1 \leq B$ , and the array satisfies Assumptions 1, 2, and 3 with limiting treated-group fraction $p$ and limiting grouped-unit fraction $ρ$ .

(Johnson decomposition input.) For every row $n$ , there are orthogonal projections $Π_{n, k}$ onto the degree- $k$ Johnson harmonic spaces $H_{n, k}$ , $k = 0, \dots, M$ , whose positive-degree components give the centered orthogonal decomposition of every $f \in L^{2} (Ω_{n, M})$ : $k = 1 \sum M Π_{n, k} f = f - E_{n} f, ⟨ Π_{n, k} f, Π_{n, ℓ} g ⟩_{n} = 0 for k \neq = ℓ .$

(Kneser spectrum input.) For every row $n$ with $2 M \leq n$ , the Kneser adjacency operator acts on $f \in H_{n, k}$ by the eigenvalue $(- 1)^{k} (M - k n - M - k), k = 0, \dots, M .$
(Variance lower bound.) With $d_{same} = \frac{1}{M p ( 1 - p )}, d_{ind} = \frac{1}{M p ( 1 - p )} - \frac{2 ρ}{M},$ the constant $c_{σ}$ satisfies $0 < c_{σ} < d_{ind} .$

Then there exist support sets $Γ_{n}^{same}$ for the common-arm Rademacher prior $H_{n}^{same}$ and $Γ_{n}^{ind}$ for the independent-arm Rademacher prior $H_{n}^{ind}$ such that both prior probabilities tend to one, every diagonal selection from either support induces an array in $C_{dense}$ with parameters $(p, ρ, B, c_{σ})$ , the conditioned one-realization laws satisfy $TV (H_{n}^{same} (O_{n} \in \cdot ∣ Γ_{n}^{same}), H_{n}^{ind} (O_{n} \in \cdot ∣ Γ_{n}^{ind})) \to 0,$ and the scaled exact variances converge uniformly on the respective supports: $u \in Γ_{n}^{same} sup G_{n} σ_{n}^{2} (u) - d_{same} \to 0, u \in Γ_{n}^{ind} sup G_{n} σ_{n}^{2} (u) - d_{ind} \to 0.$ Moreover, there is an $ε > 0$ such that every measurable one-realization variance statistic $S_{n} (O_{n})$ satisfies $\frac{1}{2} \leq n \to \infty lim inf Y \in C_{dense} sup Y Pr (\frac{S _{n} ( O _{n} )}{σ _{n}^{2}} - 1 > ε) .$

⊢ Lean

Theorem 6 establishes the one-realization lower bound in the positive-density class. The high-probability supports place both constructions inside $C_{dense}$ with the same envelope, fraction, and scaled-variance parameters, while total variation convergence makes the conditioned observed laws asymptotically indistinguishable. Uniform convergence of the scaled exact variances to $d_{same}$ and $d_{ind}$ supplies the separated targets, and the final display gives a single $ε > 0$ for which every measurable statistic $S_{n} (O_{n})$ has worst-case relative error probability bounded below by one half.

The intuition is the same as in a two-point Le Cam comparison, adapted to deterministic triangular arrays. If the observed laws are asymptotically the same, a statistic based only on $O_{n}$ cannot reliably determine which variance target generated the data. Because the targets remain separated by the positive-density correction $2 ρ / M$ , any one-realization variance statistic must make a nonvanishing relative error on at least one member of the dense class. This identifies the degree-one cross-arm component in Definition 11 as the obstruction to uniform exact-variance ratio consistency from a single realized grouping and assignment.

Discussion, scope, and extensions

The results above characterize a variance-estimation problem created by random group formation in dense finite populations. The exact identities in Theorems 1 and 2 express the design variance through the Johnson decomposition and the Kneser disjointness geometry of the group table. Those identities separate the independent-group leading scale from the Kneser finite-population correction, whose dense-limit leading term is the degree-one arm-difference component in Definition 11. In dense designs, Theorem 3 turns that exact decomposition into an interpretable limit: the scaled variance expansion contains the degree-one Johnson correction alongside the independent-group leading scale.

This characterization motivates the phase-frontier statement for the scalar CR2 statistic. The scalar CR2 statistic in Definition 12 estimates the independent-group scale under the balanced equal-group design, and Theorem 4 identifies the dense correction governing its scaled difference from the exact variance and the condition for ratio consistency. In sparse regimes, Theorem 5 shows that overlap from group formation is asymptotically negligible at the variance scale considered there. Together, the dense and sparse statements give a single design-based account of when the usual cluster calculation tracks the exact randomization variance and when the finite-population group-formation term contributes to the target.

The software comparison in Propositions 1 and 2 anchors this population geometry in the regression workflow used by applied researchers. The proposition identifies the equal-group scalar CR2 statistic with the corresponding clubSandwich calculation for the intercept-plus-treatment regression, in the setting of Pustejovsky et al. (2018). The eight-unit construction then gives a finite instance in which that statistic and the exact design variance differ. This finite witness complements the asymptotic analysis: the same degree-one structure that appears in Theorem 3 is already visible in a small balanced design.

The lower bound in Theorem 6 gives the identification-theoretic interpretation of the correction. For the dense schedule class in Definition 13, the observed realization contains the realized groups, assignments, and member outcomes, while the exact variance also depends on how the unobserved counterfactual group tables co-vary across disjoint groups. Proposition 3 supplies two dense constructions with asymptotically indistinguishable observed laws and separated exact variances, and Theorem 6 converts that comparison into a uniform lower bound for every one-realization variance statistic. The result therefore locates the obstruction precisely: the observed data can support the usual cluster scale, but the dense finite-population correction includes a cross-arm component that is not uniformly recoverable from one realized grouping and assignment.

These conclusions also clarify the positive scope of the paper. The analysis is design-based and finite-population: potential outcomes are deterministic, randomness comes from group formation and balanced assignment, and the target is the exact variance of the group-level difference-in-means estimator. The asymptotic statements are triangular-array statements over the schedule class in Definition 13, with bounded outcomes, stable treatment and sampling fractions, growing group counts, and nondegenerate scaled exact variance. Within that scope, the paper gives exact variance identities, dense and sparse asymptotic comparisons, a software identity for the scalar CR2 calculation, a finite witness, and a one-realization lower bound.

Limitations and future work

The results leave Gaussian approximation, studentized testing, Wald coverage, and finite-sample CR2 conservativeness as separate inferential questions. The variance identities and ratio limits characterize the target variance and the behavior of the scalar CR2 statistic, while a distributional theory for tests would require additional approximation arguments for the studentized estimator. Such arguments would naturally interact with the many-cluster refinements developed for CR2 procedures (Pustejovsky et al., 2018) and with recent work on random group formation and cluster-robust inference (Fu et al., 2026).

Variable group sizes are another extension. The present analysis uses a common group size throughout, which makes the random partition a uniform slice design and brings the Johnson association scheme directly into the variance calculation. Allowing heterogeneous group sizes would require the corresponding finite-population covariance operator and an analogue of the degree-one correction for the resulting design. That extension would preserve the same substantive question–how random group formation changes the variance target–while changing the combinatorial geometry used to express it.

Appendices

Proofs and auxiliary lemmas

This appendix collects the auxiliary spectral statements used by the variance geometry and records how the formal arguments fit together. The starting point is the Johnson association scheme on the uniform slice, whose orthogonal decomposition supplies the coordinates used in Definition 9 and whose Kneser disjointness operator supplies the covariance operator in Definition 10. Classical accounts of these schemes appear in Delsarte (1973), Brouwer et al. (1989), and Brouwer et al. (2018); the harmonic-analysis notation follows the slice presentation in Filmus (2016).

Definition 21 [synth_10] (Johnson and Kneser covariance apparatus).

For $0 \leq k \leq M$ , let $H_{n, k} \subseteq L^{2} (Ω_{n, M})$ be the degree- $k$ Johnson harmonic subspace, and let $Π_{n, k}$ be the $⟨ \cdot, \cdot ⟩_{n}$ -orthogonal projection onto $H_{n, k}$ . For $f \in L^{2} (Ω_{n, M})$ , the centered Johnson decomposition is $f - E_{n} f = k = 1 \sum M Π_{n, k} f .$ For $2 M \leq n$ , the unnormalized Kneser adjacency operator is $(Adj_{n, M} f) (A) = C \in Ω_{n, M} C \cap A = \emptyset \sum f (C), A \in Ω_{n, M} .$ The normalized Kneser disjointness operator is $(K_{n} f) (A) = (M n - M)^{- 1} C \in Ω_{n, M} C \cap A = \emptyset \sum f (C) .$ Its eigenvalue on $H_{n, k}$ is denoted by $λ_{n, k}$ . For $a, b \in Z$ , define the ordered-disjoint covariance and the arm-difference covariance by $C_{ab, n} = ⟨ h_{a, n}^{\circ}, K_{n} h_{b, n}^{\circ} ⟩_{n}, C_{τ τ, n} = C_{11, n} + C_{00, n} - 2 C_{10, n} .$ The degree-one arm-difference energy is $E_{τ, 1, n} = ∥ Π_{n, 1} (h_{1, n} - h_{0, n}) ∥_{n}^{2} .$

The objects in Definition 21 restate, in one place, the spectral apparatus used throughout the exact and asymptotic variance arguments. The decomposition separates centered group tables into orthogonal Johnson degrees, and the Kneser operator averages over disjoint groups, matching the dependence induced by random partitioning. With this notation fixed, two Kneser statements follow, and they are deliberately distinct. Lemma 1 is the combinatorial fact: the unnormalized disjointness adjacency operator $Adj_{n, M}$ , which sums a table over all groups disjoint from a given one, acts on the degree- $k$ harmonic space by the integer eigenvalue $(- 1)^{k} (M - k n - M - k)$ . Lemma 2 is the form the variance algebra consumes: it divides by the number $(M n - M)$ of disjoint groups to obtain the averaging operator $K_{n}$ of Definition 10, whose eigenvalues $λ_{n, k} = (- 1)^{k} (M)_{k} / (n - M)_{k}$ are the falling-factorial ratios that carry the $n$ -dependence of the variance expansion. The second is obtained from the first by that normalization, which is why its proof is short; keeping them apart isolates the one combinatorial input of the paper from the bookkeeping that turns it into a covariance statement.

Lemma 1 [lem:johnson-kneser-adjacency-eigenvalue] (Johnson--Kneser adjacency eigenvalue).

Using the uniform $M$ -slice $Ω_{n, M}$ , the slice function space $L^{2} (Ω_{n, M})$ , and the Johnson harmonic subspaces $H_{n, k}$ from Definition 9, suppose that:

(Population and group size.) $n$ and $M$ are nonnegative integers, with $n$ the population size and $M$ the common group size, and $2 M \leq n$ .

(Harmonic degree.) $k \in {0, \dots, M}$ .

(Function.) $f \in H_{n, k}$ .

Let $Adj_{n, M}$ be the linear operator on $L^{2} (Ω_{n, M})$ defined by $(Adj_{n, M} f) (Γ) = Δ \in Ω_{n, M} \sum 1 {Γ \cap Δ = \emptyset} f (Δ) .$ Then $f$ is an eigenfunction of $Adj_{n, M}$ with eigenvalue $(- 1)^{k} (M - k n - M - k) .$ Equivalently, $Adj_{n, M} f = (- 1)^{k} (M - k n - M - k) f$ as an identity in $L^{2} (Ω_{n, M})$ .

⊢ Lean

Proof of Lemma 1.

Write $m_{Υ} (Γ) := 1 {Υ \subseteq Γ}, V_{\leq q} := span {m_{Υ} : ∣Υ∣ \leq q} \subseteq L^{2} (Ω_{n, M}),$ for finite $Υ \subseteq {1, \dots, n}$ and $q \geq 0$ . Also write $δ_{Υ} (Γ) := 1 {Υ \cap Γ = \emptyset} .$ The Johnson harmonic construction used in Definition 9 has $H_{n, 0} = V_{\leq 0}, H_{n, j} = V_{\leq j} \cap V_{\leq j - 1}^{⊥} (j \geq 1),$ where orthogonality is with respect to the uniform-slice inner product. The hypothesis $2 M \leq n$ gives $M \leq n$ , so $Ω_{n, M}$ is nonempty.

First take $k = 0$ . Since $V_{\leq 0}$ is spanned by $m_{\emptyset}$ , membership $f \in H_{n, 0} = V_{\leq 0}$ gives a scalar $η \in R$ such that $f = η m_{\emptyset} .$ For every $Γ \in Ω_{n, M}$ , $(Adj_{n, M} m_{\emptyset}) (Γ) = # {Δ \in Ω_{n, M} : Γ \cap Δ = \emptyset} = (M n - M) .$ Indeed, after $Γ$ is fixed, the admissible $Δ$ ’s are precisely the $M$ -subsets of the $n - M$ points outside $Γ$ . Thus $Adj_{n, M} f = η (M n - M) m_{\emptyset} = (- 1)^{0} (M n - M) f,$ which is the asserted formula in degree zero.
Now suppose $k \geq 1$ . Define the scalar $α_{k} := (- 1)^{k} (M - k n - M - k)$ and the residual $ρ := Adj_{n, M} f - α_{k} f .$ We first show $ρ \in V_{\leq k - 1} .$ It is enough to check this on the spanning monomials $m_{Υ}$ with $∣Υ∣ \leq k$ . If $∣Υ∣ < k$ , then $m_{Υ} \in V_{\leq k - 1}$ , and the adjacency operator preserves this lower filtration level: $Adj_{n, M} m_{Υ} \in V_{\leq k - 1} .$ Hence $Adj_{n, M} m_{Υ} - α_{k} m_{Υ} \in V_{\leq k - 1}$ .

It remains to consider $∣Υ∣ = k$ . For every $Γ \in Ω_{n, M}$ , $(Adj_{n, M} m_{Υ}) (Γ) = (M - k n - M - k) δ_{Υ} (Γ) .$ When $Γ \cap Υ \neq = \emptyset$ , no disjoint $Δ$ can contain $Υ$ . When $Γ \cap Υ = \emptyset$ , such $Δ$ ’s are obtained by adjoining $M - k$ further points from the complement of $Γ \cup Υ$ , which has size $n - M - k$ . Inclusion-exclusion gives $δ_{Υ} = Θ \subseteq Υ \sum (- 1)^{∣Θ∣} m_{Θ} .$ Therefore $Adj_{n, M} m_{Υ} - α_{k} m_{Υ} = (M - k n - M - k) Θ ⊊ Υ \sum (- 1)^{∣Θ∣} m_{Θ} \in V_{\leq k - 1},$ because every proper subset $Θ ⊊ Υ$ has $∣Θ∣ \leq k - 1$ . By linearity over the span $V_{\leq k}$ , the same conclusion holds for every $f \in V_{\leq k}$ , in particular for the present $f \in H_{n, k} \subseteq V_{\leq k}$ .
Since $f \in H_{n, k} = V_{\leq k} \cap V_{\leq k - 1}^{⊥}$ , for every $g \in V_{\leq k - 1}$ , $⟨ f, g ⟩_{n} = 0.$ The adjacency operator preserves $V_{\leq k - 1}$ , so $Adj_{n, M} g \in V_{\leq k - 1}$ . It is also self-adjoint for the uniform-slice inner product: $⟨ Adj_{n, M} u, v ⟩_{n} = ⟨ u, Adj_{n, M} v ⟩_{n} (u, v \in L^{2} (Ω_{n, M})),$ which follows by interchanging the two finite sums and using symmetry of disjointness. Hence, for every $g \in V_{\leq k - 1}$ , $⟨ ρ, g ⟩_{n} = ⟨ Adj_{n, M} f, g ⟩_{n} - α_{k} ⟨ f, g ⟩_{n} = ⟨ f, Adj_{n, M} g ⟩_{n} - α_{k} ⟨ f, g ⟩_{n} = 0.$ Thus $ρ$ is orthogonal to $V_{\leq k - 1}$ .
Combining the previous two steps, $ρ \in V_{\leq k - 1}$ and $ρ ⊥ V_{\leq k - 1}$ . Taking $g = ρ$ gives $⟨ ρ, ρ ⟩_{n} = 0.$ Since $M \leq n$ , $⟨ ρ, ρ ⟩_{n} = (M n)^{- 1} Γ \in Ω_{n, M} \sum ρ (Γ)^{2}$ with $(M n) > 0$ , so the uniform-slice inner product is positive definite. Therefore $ρ = 0$ , i.e. $Adj_{n, M} f = α_{k} f = (- 1)^{k} (M - k n - M - k) f .$ This is the desired identity for $k \geq 1$ , and together with the degree-zero case proves the lemma.

∎

Lemma 2 [lem:classical-kneser-spectrum] (Classical Kneser spectrum).

For any population size $n$ and common group size $M$ , suppose:

(Overlap.) $2 M \leq n$ .

(Harmonic degree.) $k$ is an integer with $0 \leq k \leq M$ .

(Harmonic function.) $f : Ω_{n, M} \to R$ belongs to the degree- $k$ Johnson harmonic subspace $H_{n, k}$ .

Then the unnormalized Kneser adjacency operator, which sums $f$ over $M$ -subsets disjoint from the argument, acts on $f$ by $(Adj_{n, M} f) (A) = (- 1)^{k} (M - k n - M - k) f (A)$ for every $A \in Ω_{n, M}$ .

⊢ Lean

Proof of Lemma 2.

Fix $n, M$ with $2 M \leq n$ , fix $0 \leq k \leq M$ , and let $f \in H_{n, k}$ . Write $[n] := {1, \dots, n}$ .

For a slice function $u : Ω_{n, M} \to R$ , use the unnormalized Kneser adjacency operator $(Adj_{n, M} u) (Γ) := Δ \in Ω_{n, M} \sum 1 {Γ \cap Δ = \emptyset} u (Δ), Γ \in Ω_{n, M} .$ The hypotheses $2 M \leq n$ , $0 \leq k \leq M$ , and $f \in H_{n, k}$ are exactly the hypotheses needed to apply Lemma 1 to this operator. It gives $Adj_{n, M} f = (- 1)^{k} (M - k n - M - k) f$ as an identity in the slice function space $L^{2} (Ω_{n, M})$ .
The preceding function identity says that, for every $A \in Ω_{n, M}$ , $Δ \in Ω_{n, M} \sum 1 {A \cap Δ = \emptyset} f (Δ) = (- 1)^{k} (M - k n - M - k) f (A) .$ The left-hand side is exactly $(Adj_{n, M} f) (A)$ , so $(Adj_{n, M} f) (A) = (- 1)^{k} (M - k n - M - k) f (A),$ which is the asserted formula.

∎

Together, Lemmas 1 and 2 give the spectral multiplier for disjointness averaging on each Johnson degree. After normalization by the number of disjoint $M$ -subsets, these multipliers become the eigenvalues used in the covariance contrast of Theorem 1. The alternating sign in degree $k$ is the algebraic source of the projection correction that later appears in Theorem 3.

The remaining classical input is the orthogonal expansion of functions on the slice. It ensures that the covariance calculation can be expressed degree by degree rather than as a direct summation over all ordered disjoint pairs.

Lemma 3 [lem:classical-johnson-decomposition] (Johnson orthogonal decomposition).

Let $n$ and $M$ be nonnegative integers with $M \leq n$ . For the canonical Johnson harmonic projections $Π_{n, k}$ on $L^{2} (Ω_{n, M})$ , whenever $2 M \leq n$ , every function $f : Ω_{n, M} \to R$ and every $A \in Ω_{n, M}$ satisfy $k = 1 \sum M Π_{n, k} f (A) = f (A) - E_{n} f .$ Moreover, the projections are pairwise orthogonal: for all $k, ℓ \in {0, \dots, M}$ , all functions $f, g : Ω_{n, M} \to R$ , and $k \neq = ℓ$ , $⟨ Π_{n, k} f, Π_{n, ℓ} g ⟩_{n} = 0.$

⊢ Lean

Proof of Lemma 3.

Assume $2 M \leq n$ . Then $M \leq n$ , so $Ω_{n, M}$ is the finite uniform slice with $∣ Ω_{n, M} ∣ = (M n) .$ For a slice function $φ : Ω_{n, M} \to R$ , write $mean_{n} (φ) := \frac{1}{∣ Ω _{n, M} ∣} ω \in Ω_{n, M} \sum φ (ω) .$

For $0 \leq u \leq M$ , let $F_{\leq u} \subseteq L^{2} (Ω_{n, M})$ be the span of the inclusion monomials $ω ⟼ i \in T \prod 1_{{i \in ω}}, T \subseteq {1, \dots, n}, ∣ T ∣ \leq u .$ The Johnson harmonic layers are constructed by $H_{n, 0} = F_{\leq 0}, H_{n, u + 1} = F_{\leq u + 1} \cap F_{\leq u}^{⊥} .$ Since $F_{\leq u} \subseteq F_{\leq u + 1}$ , finite-dimensional orthogonal decomposition gives $F_{\leq u + 1} = F_{\leq u} \oplus H_{n, u + 1} .$ Iterating from $u = 0$ to $M - 1$ , $F_{\leq M} = u = 0 ⨁ M H_{n, u} .$ Moreover $F_{\leq M} = L^{2} (Ω_{n, M})$ : for every fixed $ω_{0} \in Ω_{n, M}$ , $1_{{ω_{0}}} (ω) = i \in ω_{0} \prod 1_{{i \in ω}},$ because $∣ ω ∣ = ∣ ω_{0} ∣ = M$ . Thus point masses belong to $F_{\leq M}$ , and they span all slice functions.

Therefore the orthogonal projections onto the layers satisfy, for every $φ : Ω_{n, M} \to R$ , $φ = u = 0 \sum M Π_{n, u} φ .$ The degree-zero space $H_{n, 0}$ is the space of constant functions. Its orthogonal projection is the constant function with value $mean_{n} (φ)$ , since for every real scalar $a_{const}$ , $⟨ φ - (ω \mapsto mean_{n} (φ)), (ω \mapsto a_{const}) ⟩_{n} = a_{const} (mean_{n} (φ) - mean_{n} (φ)) = 0.$ Hence $Π_{n, 0} φ = ω \mapsto mean_{n} (φ) .$ Evaluating the full decomposition at $A \in Ω_{n, M}$ and subtracting the degree-zero component gives $u = 1 \sum M Π_{n, u} φ (A) = φ (A) - mean_{n} (φ) .$ Applied to $φ = f$ , this is the centered projection identity with the algebraic uniform mean.
The averaging operator $E_{n}$ is the uniform-slice expectation, so for every $f : Ω_{n, M} \to R$ , $E_{n} f = \frac{1}{∣ Ω _{n, M} ∣} ω \in Ω_{n, M} \sum f (ω) = mean_{n} (f) .$ Substituting this equality into the preceding display yields $u = 1 \sum M Π_{n, u} f (A) = f (A) - E_{n} f .$ When $M = 0$ , the same formula reads $0 = f (A) - E_{n} f$ , because the slice has one point and the degree-zero projection is $f$ .
It remains to check distinct-degree orthogonality. For any $k \in {0, \dots, M}$ and any slice function $f$ , $Π_{n, k} f \in H_{n, k},$ because $Π_{n, k}$ is the orthogonal projection onto $H_{n, k}$ . If $k < ℓ$ , then $H_{n, ℓ} \subseteq F_{\leq ℓ - 1}^{⊥}, H_{n, k} \subseteq F_{\leq k} \subseteq F_{\leq ℓ - 1},$ and therefore every element of $H_{n, k}$ is orthogonal to every element of $H_{n, ℓ}$ . The case $ℓ < k$ is symmetric. Thus, whenever $k \neq = ℓ$ , $⟨ Π_{n, k} f, Π_{n, ℓ} g ⟩_{n} = 0.$ This proves the pairwise orthogonality assertion.

∎

Lemma 3 is the bookkeeping device behind the exact variance formula. Applying the decomposition to the centered arm tables in Definition 5 lets the Kneser covariance in Definition 10 act separately on each harmonic component. This is what turns the two-stage random partition design in Definition 4 into the exact identity in Theorem 2.

The subsequent verified arguments use these ingredients in a fixed order. First, the finite-sample variance algebra combines the PAME estimator in Definition 7 with the Kneser covariance identity to obtain Theorem 2. Next, the dense schedule class in Definition 13 specializes that identity to the projection limit in Theorem 3 and to the CR2 comparison in Theorem 4; the sparse construction gives the complementary behavior in Theorem 5. The software calculation in Proposition 1 identifies the scalar CR2 statistic with the stated clubSandwich call, and Proposition 2 evaluates the finite eight-unit witness from Definition 17. Finally, the randomized schedule construction in Proposition 3 feeds the one-realization lower bound in Theorem 6.

The finite-sample and software statements are algebraic consequences of the displayed definitions and of the versioned software conventions cited in Pustejovsky (2026) and Zeileis et al. (2026). The surrounding econometric motivation connects these calculations to random group formation and cluster-robust variance practice as in Fu et al. (2026).

Verification note.

Every theorem, proposition, and assumption displayed in this paper, and every internal algebraic derivation supporting them, is machine-checked in Lean 4, with no unproved hypotheses and no remaining proof obligations. The displayed definitions divide into two kinds. Those carrying a Lean declaration – the schedule array, the arm set, slice averaging, the slice norm, the centered arm table, the two Rademacher priors, the one-realization observation, the row treatment fraction, and all numbered def: objects – are the objects the verified statements quantify over. Three are presentation-level definitions written for the reader and carry no Lean declaration of their own: the uniform-slice space $L^{2} (Ω_{n, M})$ in Definition 8, the realized arm group counts in Definition 14, and the unnormalized adjacency operator $Adj_{n, M}$ in Definition 21. They name notation that the verified statements express directly in terms of the slice and its inner product, and nothing in the verified development depends on them. The trust boundary is narrower than is usual for results of this kind: the classical Johnson decomposition and Kneser spectrum recorded in Lemmas 3, 2, and 1 are not imported as cited facts but are themselves proved in the verified development, so the citations to Delsarte (1973), Brouwer et al. (1989), Filmus (2016), and Brouwer et al. (2018) attribute these classical results rather than assume them. What remains outside the machine-checked scope is the bibliographic attribution itself and the versioned software conventions of Pustejovsky (2026) and Zeileis et al. (2026), which enter Proposition 1 as stated implementation conventions.

Proofs of the main results

Proof of Theorem 1.

Let $(A_{n} q) (A) = C : C \cap A = \emptyset \sum q (C)$ be the unnormalized Kneser adjacency operator on functions $q : Ω_{n, M} \to R$ . For $k = 0, \dots, M$ and $f : Ω_{n, M} \to R$ , the projection assumption gives $Π_{n, k} f \in H_{n, k}$ , so the Kneser spectrum assumption gives $A_{n} (Π_{n, k} f) (A) = (- 1)^{k} (M - k n - M - k) Π_{n, k} f (A) .$ By Definition 10, $K_{n} (Π_{n, k} f) (A) = (- 1)^{k} \frac{( M - k n - M - k )}{( M n - M )} Π_{n, k} f (A) .$ Since $k \leq M$ and $2 M \leq n$ , $\frac{( M - k n - M - k )}{( M n - M )} = \frac{( n - M - k ) _{M - k}}{( M - k )!} \frac{M !}{( n - M ) _{M}} = \frac{( M ) _{k}}{( n - M ) _{k}},$ using the falling-factorial convention $(r)_{0} = 1$ . Hence $K_{n} (Π_{n, k} f) (A) = λ_{n, k} Π_{n, k} f (A) .$
Now let $f, g : Ω_{n, M} \to R$ satisfy $E_{n} f = E_{n} g = 0$ , and put $I_{+} = {j \in {0, \dots, M} : j > 0} .$ The centered decomposition in Definition 9 gives, for every $A \in Ω_{n, M}$ , $f (A) = j \in I_{+} \sum Π_{n, j} f (A), g (A) = j \in I_{+} \sum Π_{n, j} g (A) .$ For a uniform ordered disjoint pair $(A, C)$ , each coordinate has the uniform $M$ -slice marginal, and the product expectation equals the Kneser inner product: $E [f (A)] = E_{n} f, E [g (C)] = E_{n} g,$ and $E [f (A) g (C)] = ⟨ f, K_{n} g ⟩_{n} .$ Therefore $Cov {f (A), g (C)} = ⟨ f, K_{n} g ⟩_{n} .$ Substituting the positive-degree decompositions and using linearity of $K_{n}$ and of $⟨ \cdot, \cdot ⟩_{n}$ , $⟨ f, K_{n} g ⟩_{n} = ⟨ i \in I_{+} \sum Π_{n, i} f, K_{n} j \in I_{+} \sum Π_{n, j} g ⟩_{n} = i \in I_{+} \sum j \in I_{+} \sum λ_{n, j} ⟨ Π_{n, i} f, Π_{n, j} g ⟩_{n} = j \in I_{+} \sum λ_{n, j} ⟨ Π_{n, j} f, Π_{n, j} g ⟩_{n},$ because distinct Johnson degrees are orthogonal. This proves the covariance identity.
For each arm $z \in {0, 1}$ , define the centered arm table $h_{z, n}^{\circ} (A) = h_{z, n} (A) - E_{n} h_{z, n} .$ Then $E_{n} h_{z, n}^{\circ} = 0$ . By Definition 10 and the preceding ordered-pair identity, $C_{ab, n} = Cov {h_{a, n}^{\circ} (A), h_{b, n}^{\circ} (C)}$ for $a, b \in {0, 1}$ under a uniform ordered disjoint pair $(A, C)$ . Applying the covariance identity from the previous step to $(h_{1, n}^{\circ}, h_{1, n}^{\circ})$ , $(h_{0, n}^{\circ}, h_{0, n}^{\circ})$ , and $(h_{1, n}^{\circ}, h_{0, n}^{\circ})$ , and using $C_{τ τ, n} = C_{11, n} + C_{00, n} - 2 C_{10, n},$ gives $C_{τ τ, n} = j \in I_{+} \sum λ_{n, j} [⟨ Π_{n, j} h_{1, n}^{\circ}, Π_{n, j} h_{1, n}^{\circ} ⟩_{n} + ⟨ Π_{n, j} h_{0, n}^{\circ}, Π_{n, j} h_{0, n}^{\circ} ⟩_{n} - 2 ⟨ Π_{n, j} h_{1, n}^{\circ}, Π_{n, j} h_{0, n}^{\circ} ⟩_{n}] .$
It remains to identify the summand with the squared norm of the projected arm contrast. For every positive degree $j \in I_{+}$ and constant $r \in R$ , $Π_{n, j} (r) = 0.$ Indeed, the centered decomposition applied to the constant function $r$ gives $ℓ \in I_{+} \sum Π_{n, ℓ} (r) = 0.$ Taking the slice inner product with $Π_{n, j} (r)$ and using degree orthogonality leaves $⟨ Π_{n, j} (r), Π_{n, j} (r) ⟩_{n} = 0,$ hence $Π_{n, j} (r) = 0$ by definiteness of the slice inner product. Therefore, by linearity of $Π_{n, j}$ , $Π_{n, j} h_{z, n}^{\circ} = Π_{n, j} (h_{z, n} - E_{n} h_{z, n}) = Π_{n, j} h_{z, n} .$ Again by linearity, $Π_{n, j} (h_{1, n} - h_{0, n}) = Π_{n, j} h_{1, n} - Π_{n, j} h_{0, n} .$ Thus $∥ Π_{n, j} (h_{1, n} - h_{0, n}) ∥_{n}^{2} = ⟨ Π_{n, j} h_{1, n} - Π_{n, j} h_{0, n}, Π_{n, j} h_{1, n} - Π_{n, j} h_{0, n} ⟩_{n} = ⟨ Π_{n, j} h_{1, n}, Π_{n, j} h_{1, n} ⟩_{n} + ⟨ Π_{n, j} h_{0, n}, Π_{n, j} h_{0, n} ⟩_{n} - 2 ⟨ Π_{n, j} h_{1, n}, Π_{n, j} h_{0, n} ⟩_{n} .$ Substitution into the preceding display yields $C_{τ τ, n} = j = 1 \sum M λ_{n, j} Π_{n, j} (h_{1, n} - h_{0, n})_{n}^{2},$ which is the asserted contrast identity.

∎

Proof of Theorem 2.

By the group-size hypotheses, $G_{1 n} > 0$ , $G_{1 n} < G_{n}$ , $G_{0 n} = G_{n} - G_{1 n} > 0$ , and $2 \leq G_{n}$ . The feasibility condition and $2 \leq G_{n}$ also give $2 M \leq n$ . Write the treated-group fraction as $p_{n} = \frac{G _{1 n}}{G _{n}}, q_{n} = 1 - p_{n} = \frac{G _{0 n}}{G _{n}} .$ For a realized ordered partition $α = (α_{1}, \dots, α_{G_{n}})$ of pairwise-disjoint elements of $Ω_{n, M}$ , define $x_{z g} (α) = h_{z, n} (α_{g}), d_{g} (α) = x_{1 g} (α) - x_{0 g} (α),$ and, for any vector $u = (u_{1}, \dots, u_{G_{n}}) \in R^{G_{n}}$ , $\overset{u}{ˉ} = \frac{1}{G _{n}} g = 1 \sum G_{n} u_{g}, S (u) = \frac{1}{G _{n} - 1} g = 1 \sum G_{n} (u_{g} - \overset{u}{ˉ})^{2} .$ Set $S_{z} (α) = S ((x_{z g} (α))_{g = 1}^{G_{n}}), S_{τ} (α) = S ((d_{g} (α))_{g = 1}^{G_{n}}) .$ These quantities are well defined because $G_{n} \geq 2$ .

Let $Δ_{n} (A) = h_{1, n} (A) - h_{0, n} (A), Δ_{n}^{\circ} (A) = Δ_{n} (A) - E_{n} Δ_{n} (A) .$ Since $h_{z, n}^{\circ} (A) = h_{z, n} (A) - E_{n} h_{z, n} (A)$ , we have $Δ_{n}^{\circ} = h_{1, n}^{\circ} - h_{0, n}^{\circ} .$ Using the bilinearity of the uniform-slice inner product in Definition 10 and the symmetry of the uniform ordered-disjoint-pair law under swapping the two groups, $⟨ Δ_{n}^{\circ}, K_{n} Δ_{n}^{\circ} ⟩_{n} = C_{11, n} + C_{00, n} - C_{10, n} - C_{01, n} = C_{11, n} + C_{00, n} - 2 C_{10, n} = C_{τ τ, n} .$

We next record the two partition-moment identities used below. For any $ϕ : Ω_{n, M} \to R$ , let $μ_{ϕ} = E_{n} ϕ (A), η_{ϕ} = E_{n} {ϕ (A)^{2}},$ and let $κ_{ϕ} = E_{A} E_{C ∣ C \cap A = \emptyset} {ϕ (A) ϕ (C)} .$ Then $Var_{n} (ϕ) = η_{ϕ} - μ_{ϕ}^{2}, ⟨ ϕ - μ_{ϕ}, K_{n} (ϕ - μ_{ϕ}) ⟩_{n} = κ_{ϕ} - μ_{ϕ}^{2} .$ Each coordinate of $α$ is uniform on $Ω_{n, M}$ , and each distinct ordered coordinate pair is a uniform ordered-disjoint pair. Therefore $E_{α} S ((ϕ (α_{g}))_{g = 1}^{G_{n}}) = \frac{1}{G _{n} - 1} {G_{n} η_{ϕ} - \frac{1}{G _{n}} (G_{n} η_{ϕ} + G_{n} (G_{n} - 1) κ_{ϕ})} = η_{ϕ} - κ_{ϕ} = Var_{n} (ϕ) - ⟨ ϕ - μ_{ϕ}, K_{n} (ϕ - μ_{ϕ}) ⟩_{n} .$ Applying this with $ϕ = h_{1, n}$ , $ϕ = h_{0, n}$ , and $ϕ = Δ_{n}$ gives $E_{α} S_{1} = V_{1, n} - C_{11, n}, E_{α} S_{0} = V_{0, n} - C_{00, n},$ and $E_{α} S_{τ} = Var_{n} (Δ_{n}) - C_{τ τ, n} .$

The same exchangeability calculation gives the variance of the partition average. Indeed, $Var_{α} {\frac{1}{G _{n}} g = 1 \sum G_{n} ϕ (α_{g})} = \frac{1}{G _{n}^{2}} {G_{n} Var_{n} (ϕ) + G_{n} (G_{n} - 1) ⟨ ϕ - μ_{ϕ}, K_{n} (ϕ - μ_{ϕ}) ⟩_{n}} .$ Thus, for $ϕ = Δ_{n}$ , $Var_{α} {\frac{1}{G _{n}} g = 1 \sum G_{n} d_{g} (α)} = \frac{Var _{n} ( Δ _{n} ) + ( G _{n} - 1 ) C _{τ τ, n}}{G _{n}} .$ Also, since each coordinate $α_{g}$ is uniform on $Ω_{n, M}$ , $E_{α} {\frac{1}{G _{n}} g = 1 \sum G_{n} d_{g} (α)} = E_{n} h_{1, n} - E_{n} h_{0, n} .$

Condition on $α$ . Under the balanced assignment in Definition 4, $E (Z_{g} ∣ α) = p_{n}, E (1 - Z_{g} ∣ α) = q_{n},$ and the usual complete-randomization second moments for distinct $g \neq = ℓ$ are $E (Z_{g} Z_{ℓ} ∣ α) = \frac{G _{1 n} ( G _{1 n} - 1 )}{G _{n} ( G _{n} - 1 )},$ $E {(1 - Z_{g}) (1 - Z_{ℓ}) ∣ α} = \frac{G _{0 n} ( G _{0 n} - 1 )}{G _{n} ( G _{n} - 1 )},$ $E {Z_{g} (1 - Z_{ℓ}) ∣ α} = \frac{G _{1 n} G _{0 n}}{G _{n} ( G _{n} - 1 )} .$ Expanding the difference-in-means estimator from Definition 7 with these moments gives $E (τ_{n} ∣ α) = \frac{1}{G _{n}} g = 1 \sum G_{n} d_{g} (α),$ and $Var (τ_{n} ∣ α) = \frac{S _{1} ( α )}{G _{1 n}} + \frac{S _{0} ( α )}{G _{0 n}} - \frac{S _{τ} ( α )}{G _{n}} .$ The same complete-randomization calculation for the denominator- $G_{z n} - 1$ within-arm sample variances in Definition 12 yields $E (V_{CR2, n} ∣ α) = \frac{S _{1} ( α )}{G _{1 n}} + \frac{S _{0} ( α )}{G _{0 n}} .$

Taking expectations in the conditional mean identity and using the partition-average identity above, $E [τ_{n}] = E_{n} h_{1, n} - E_{n} h_{0, n} = τ_{n},$ where the last equality is Definition 7.

By the finite tower variance identity for the two-stage design, $σ_{n}^{2} = E_{α} {Var (τ_{n} ∣ α)} + Var_{α} {E (τ_{n} ∣ α)} .$ Substituting the identities already proved gives $σ_{n}^{2} = \frac{V _{1, n} - C _{11, n}}{G _{1 n}} + \frac{V _{0, n} - C _{00, n}}{G _{0 n}} - \frac{Var _{n} ( Δ _{n} ) - C _{τ τ, n}}{G _{n}} + \frac{Var _{n} ( Δ _{n} ) + ( G _{n} - 1 ) C _{τ τ, n}}{G _{n}} = \frac{V _{1, n} - C _{11, n}}{G _{1 n}} + \frac{V _{0, n} - C _{00, n}}{G _{0 n}} + C_{τ τ, n} .$ Since $\frac{R _{n}}{G _{n}} = \frac{1}{G _{n}} {\frac{V _{1, n}}{G _{1 n} / G _{n}} + \frac{V _{0, n}}{G _{0 n} / G _{n}}} = \frac{V _{1, n}}{G _{1 n}} + \frac{V _{0, n}}{G _{0 n}},$ this is exactly $σ_{n}^{2} = \frac{R _{n}}{G _{n}} + C_{τ τ, n} - \frac{C _{11, n}}{G _{1 n}} - \frac{C _{00, n}}{G _{0 n}} .$

Taking expectations in the conditional CR2 identity gives $E [V_{CR2, n}] = \frac{E _{α} S _{1} ( α )}{G _{1 n}} + \frac{E _{α} S _{0} ( α )}{G _{0 n}} = \frac{V _{1, n} - C _{11, n}}{G _{1 n}} + \frac{V _{0, n} - C _{00, n}}{G _{0 n}} .$

Subtracting the variance identity from the CR2 expectation identity, the common terms cancel and therefore $E [V_{CR2, n}] - σ_{n}^{2} = - C_{τ τ, n} .$

∎

Proof of Theorem 3.

Set $Γ := 64 M^{2} (M + 1) B^{2}, C := Γ + 1.$ Then $C > 0$ . Fix a feasible triangular array satisfying the four displayed assumptions, fix the rowwise Johnson projections, and bring into scope the two rowwise hypotheses that these projections give the centered orthogonal Johnson decomposition and that the corresponding Kneser spectrum formula holds. Index rows by $r$ , and write $n_{r}$ for the row population size, $G_{r}$ for the group count, $G_{1 r}$ and $G_{0 r} = G_{r} - G_{1 r}$ for the arm counts, $N_{r} = M G_{r}$ , and $p_{r} = G_{1 r} / G_{r}$ . Since $2 \leq M$ , $M > 0$ . The feasibility condition gives $G_{r} \leq M G_{r} = N_{r} \leq n_{r} .$ Together with Assumption 1, this implies $n_{r} \to \infty$ . Hence $\frac{1}{n _{r}} \to 0, \frac{M}{n _{r}} \to 0, 1 - \frac{M}{n _{r}} \to 1.$

Define $α_{r} := \frac{M G _{r}}{n _{r} - M} .$ Because $G_{1 r} > 0$ and $G_{1 r} < G_{r}$ , every row has $G_{r} \geq 2$ , and therefore $2 M \leq M G_{r} \leq n_{r}$ , so the denominator is positive. Also $α_{r} = \frac{M G _{r} / n _{r}}{1 - M / n _{r}} = \frac{N _{r} / n _{r}}{1 - M / n _{r}} .$ By Assumption 3 and the preceding display, $α_{r} \to ρ$ .

For $S \in Ω_{n_{r}, M}$ , Definition 5 and Assumption 4 give, for each arm $z$ , $∣ h_{z, r} (S) ∣ = \frac{1}{M} i \in S \sum Y_{i, r} (z, S) \leq \frac{1}{M} i \in S \sum ∣ Y_{i, r} (z, S) ∣ \leq B .$ Put $d_{r} (S) := h_{1, r} (S) - h_{0, r} (S) .$ Then $∣ d_{r} (S) ∣ \leq ∣ h_{1, r} (S) ∣ + ∣ h_{0, r} (S) ∣ \leq 2 B .$ More generally, if $∣ u (S) ∣ \leq L$ on $Ω_{n_{r}, M}$ , then every Johnson projection satisfies $∥ Π_{r, k} u ∥_{r}^{2} \leq L^{2} .$ Indeed, writing $v = Π_{r, k} u$ , orthogonal projection gives $∥ u ∥_{r}^{2} = ∥ u - v ∥_{r}^{2} + ∥ v ∥_{r}^{2},$ so $∥ v ∥_{r}^{2} \leq ∥ u ∥_{r}^{2} = E_{r} [u (S)^{2}] \leq L^{2}$ . Applying this with $u = d_{r}$ , $L = 2 B$ , and $k = 1$ yields $0 \leq E_{τ, 1, r} = ∥ Π_{r, 1} d_{r} ∥_{r}^{2} \leq (2 B)^{2} .$ Consequently $(ρ - α_{r}) E_{τ, 1, r} \to 0.$

Let $I_{\geq 2} := {k \in {0, \dots, M} : 2 \leq k}$ and $H_{r} := G_{r} k \in I_{\geq 2} \sum λ_{r, k} ∥ Π_{r, k} d_{r} ∥_{r}^{2},$ where $λ_{r, k}$ is the normalized Kneser eigenvalue from Theorem 1. We claim that, for every row, $∣ H_{r} ∣ \leq \frac{Γ}{n _{r}} .$ First suppose $4 M \leq n_{r}$ . Put $η_{r} := 2 M / n_{r}$ , so $0 \leq η_{r} \leq 1$ . For any function $u$ on $Ω_{n_{r}, M}$ , any finite degree set $I \subseteq {0, \dots, M}$ , any integer threshold $q$ such that $q \leq k$ for all $k \in I$ , and any envelope $L$ satisfying $∣ u (S) ∣ \leq L$ for all $S$ , the spectral-sum estimate is $k \in I \sum λ_{r, k} ∥ Π_{r, k} u ∥_{r}^{2} \leq ∣ I ∣ η_{r}^{q} L^{2} .$ Indeed, from $λ_{r, k} = (- 1)^{k} \frac{( M ) _{k}}{( n _{r} - M ) _{k}},$ each numerator factor is at most $M$ , while each denominator factor is at least $n_{r} /2$ ; hence $∣ λ_{r, k} ∣ \leq η_{r}^{k} \leq η_{r}^{q} (k \in I) .$ The projection-energy bound proved above gives $∥ Π_{r, k} u ∥_{r}^{2} \leq L^{2},$ and the triangle inequality therefore gives the displayed spectral-sum estimate.

Applying this estimate with $I = I_{\geq 2}$ , $q = 2$ , $u = d_{r}$ , and $L = 2 B$ gives $k \in I_{\geq 2} \sum λ_{r, k} ∥ Π_{r, k} d_{r} ∥_{r}^{2} \leq (M + 1) (\frac{2 M}{n _{r}})^{2} (2 B)^{2} .$ Using $G_{r} \leq n_{r}$ , $∣ H_{r} ∣ \leq n_{r} (M + 1) (\frac{2 M}{n _{r}})^{2} (2 B)^{2} = \frac{16 M ^{2} ( M + 1 ) B ^{2}}{n _{r}} \leq \frac{Γ}{n _{r}} .$ Now suppose $4 M > n_{r}$ . Since $2 M \leq n_{r}$ , the same eigenvalue formula gives $∣ λ_{r, k} ∣ = \frac{( M ) _{k}}{( n _{r} - M ) _{k}} \leq 1 (0 \leq k \leq M),$ because $M \leq n_{r} - M$ . Together with $∥ Π_{r, k} d_{r} ∥_{r}^{2} \leq (2 B)^{2}$ , this yields $k \in I_{\geq 2} \sum λ_{r, k} ∥ Π_{r, k} d_{r} ∥_{r}^{2} \leq (M + 1) (2 B)^{2} .$ Using $G_{r} \leq n_{r}$ and $n_{r} \leq 4 M$ , $∣ H_{r} ∣ \leq n_{r} (M + 1) (2 B)^{2} = 4 n_{r} (M + 1) B^{2} \leq \frac{64 M ^{2} ( M + 1 ) B ^{2}}{n _{r}} = \frac{Γ}{n _{r}} .$ Since $n_{r} \to \infty$ , $H_{r} \to 0$ .

By Theorem 1, applied to $d_{r}$ , $C_{τ τ, r} = k = 1 \sum M λ_{r, k} ∥ Π_{r, k} d_{r} ∥_{r}^{2} .$ The degree-one eigenvalue is $λ_{r, 1} = - \frac{M}{n _{r} - M} .$ Splitting off degree one and multiplying by $G_{r}$ gives $G_{r} C_{τ τ, r} = - \frac{M G _{r}}{n _{r} - M} E_{τ, 1, r} + G_{r} k = 2 \sum M λ_{r, k} ∥ Π_{r, k} d_{r} ∥_{r}^{2} = - α_{r} E_{τ, 1, r} + H_{r} .$ Therefore $G_{r} C_{τ τ, r} + ρ E_{τ, 1, r} = (ρ - α_{r}) E_{τ, 1, r} + H_{r} \to 0.$ This proves the second displayed limit.

Next fix an arm $z$ . Let $h_{z, r}^{\circ} (S) := h_{z, r} (S) - E_{r} h_{z, r} .$ The preceding bound on $h_{z, r}$ implies $∣ E_{r} h_{z, r} ∣ \leq B, ∣ h_{z, r}^{\circ} (S) ∣ \leq 2 B .$ For all sufficiently large $r$ , $4 M \leq n_{r}$ . Applying Theorem 1 to the centered table $h_{z, r}^{\circ}$ and using the degree- $\geq 1$ spectral bound gives $∣ C_{z z, r} ∣ \leq (M + 1) \frac{2 M}{n _{r}} (2 B)^{2} .$ Thus $C_{11, r} \to 0, C_{00, r} \to 0.$ Since Assumption 2 gives $p_{r} \to p \in (0, 1)$ , also $1 - p_{r} \to 1 - p \in (0, 1)$ . Hence $\frac{C _{11, r}}{p _{r}} + \frac{C _{00, r}}{1 - p _{r}} \to 0.$ This proves the third displayed limit.

It remains to identify the variance limit. The same stable-fraction assumption implies that, eventually, $p_{r} > \frac{p}{2}, 1 - p_{r} > \frac{1 - p}{2} .$ Together with $G_{r} \to \infty$ , this yields $G_{1 r} = p_{r} G_{r} \geq 2, G_{0 r} = (1 - p_{r}) G_{r} \geq 2$ for all sufficiently large $r$ . On those rows, Theorem 2 gives $σ_{r}^{2} = \frac{R _{r}}{G _{r}} + C_{τ τ, r} - \frac{C _{11, r}}{G _{1 r}} - \frac{C _{00, r}}{G _{0 r}} .$ Multiplying by $G_{r}$ , and using $G_{1 r} = p_{r} G_{r}$ and $G_{0 r} = (1 - p_{r}) G_{r}$ , gives the eventual identity $G_{r} σ_{r}^{2} - (R_{r} - ρ E_{τ, 1, r}) = (G_{r} C_{τ τ, r} + ρ E_{τ, 1, r}) - (\frac{C _{11, r}}{p _{r}} + \frac{C _{00, r}}{1 - p _{r}}) .$ Both terms on the right tend to zero by the preceding two steps. Therefore $G_{r} σ_{r}^{2} - (R_{r} - ρ E_{τ, 1, r}) \to 0,$ which is the first displayed limit.

Finally, the rowwise bound already proved gives $G_{r} k = 2 \sum M λ_{r, k} ∥ Π_{r, k} d_{r} ∥_{r}^{2} \leq \frac{Γ}{n _{r}} \leq \frac{C}{n _{r}},$ because $C = Γ + 1$ and $n_{r} > 0$ . Translating the row index $r$ back to the theorem’s notation gives the asserted bound for every row and completes the proof.

∎

Proof of Theorem 4.

For $z \in {0, 1}$ , set $m_{1, n} := G_{1 n}, m_{0, n} := G_{0 n} := G_{n} - G_{1 n}, π_{1, n} := p_{n}, π_{0, n} := 1 - p_{n} .$ The dense schedule condition in Definition 13 gives $G_{n} \to \infty$ , $p_{n} \to p \in (0, 1)$ , and hence $m_{1, n} = p_{n} G_{n} \to \infty, m_{0, n} = (1 - p_{n}) G_{n} \to \infty.$ Consequently $m_{1, n} \geq 2$ and $m_{0, n} \geq 2$ for all sufficiently large $n$ . Also, since $M G_{n} \leq n$ and $M \geq 2$ , the population size tends to infinity, so $4 M \leq n$ eventually.
Let $g_{n} : Ω_{n, M} \to R$ be any deterministic table with $∣ g_{n} (S) ∣ \leq L$ for all $S \in Ω_{n, M}$ , where $L > 0$ . For $ω = (A_{n}, Z_{n})$ in the support of the design in Definition 4, define the arm- $z$ selected mean by $\overline{g}_{z, n} (ω) := \frac{1}{m _{z, n}} j : Z_{j n} = z \sum g_{n} (A_{j n}), μ_{g, n} := E_{n} g_{n} .$ The selected mean has expectation $μ_{g, n}$ . Indeed, condition on any realized arm-position set of cardinality $m_{z, n}$ . Under Definition 4, each selected group is uniform on $Ω_{n, M}$ , and averaging over the independently chosen arm positions preserves this marginal law.

For the variance, define the centered table and the normalized disjointness operator by $g_{n}^{\circ} (S) := g_{n} (S) - μ_{g, n}, (K_{n} u) (S) := \frac{1}{# { T \in Ω _{n, M} : T \cap S = \emptyset }} T \cap S = \emptyset \sum u (T),$ for $S \in Ω_{n, M}$ . For all sufficiently large rows, $m_{z, n} \geq 2$ and $2 M \leq n$ . Conditional on the arm positions, two distinct selected groups form a uniform ordered disjoint pair, so $Cov {g_{n} (A_{j n}), g_{n} (A_{ℓ n})} = ⟨ g_{n}^{\circ}, K_{n} g_{n}^{\circ} ⟩_{n}, j \neq = ℓ .$ Expanding the square of the selected average gives $Var {\overline{g}_{z, n}} = \frac{1}{m _{z, n}^{2}} {m_{z, n} Var_{n} (g_{n}) + m_{z, n} (m_{z, n} - 1) ⟨ g_{n}^{\circ}, K_{n} g_{n}^{\circ} ⟩_{n}} = \frac{Var _{n} ( g _{n} )}{m _{z, n}} + (1 - \frac{1}{m _{z, n}}) ⟨ g_{n}^{\circ}, K_{n} g_{n}^{\circ} ⟩_{n} .$

It remains to bound the covariance term. Since $∣ g_{n} (S) ∣ \leq L$ , uniform averaging gives $∣ μ_{g, n} ∣ \leq L$ , hence $∣ g_{n}^{\circ} (S) ∣ \leq 2 L$ and $∥ g_{n}^{\circ} ∥_{n}^{2} \leq (2 L)^{2}$ . Applying Theorem 1 to the centered table gives $⟨ g_{n}^{\circ}, K_{n} g_{n}^{\circ} ⟩_{n} = k = 1 \sum M λ_{n, k} ∥ Π_{n, k} g_{n}^{\circ} ∥_{n}^{2} .$ For rows with $4 M \leq n$ , the falling-factorial expression for $λ_{n, k}$ satisfies, for $1 \leq k \leq M$ , $∣ λ_{n, k} ∣ \leq (\frac{2 M}{n})^{k} \leq \frac{2 M}{n} .$ The first inequality follows by bounding the numerator falling factorial by $M^{k}$ and the denominator falling factorial by $(n /2)^{k}$ ; the second uses $2 M / n \leq 1$ . Because each $Π_{n, k}$ is an orthogonal projection, $∥ Π_{n, k} g_{n}^{\circ} ∥_{n}^{2} \leq ∥ g_{n}^{\circ} ∥_{n}^{2} \leq (2 L)^{2} .$ Therefore, for all sufficiently large $n$ , $∣ ⟨ g_{n}^{\circ}, K_{n} g_{n}^{\circ} ⟩_{n} ∣ \leq (M + 1) \frac{2 M}{n} (2 L)^{2} .$ Since $Var_{n} (g_{n}) \leq L^{2}$ , $m_{z, n} \to \infty$ , and $n \to \infty$ , the displayed variance tends to zero. Chebyshev’s inequality therefore gives $\overline{g}_{z, n} - E_{n} g_{n} p 0.$
Apply the preceding conclusion first to $g_{n} = h_{z, n}$ , using $∣ h_{z, n} ∣ \leq B$ , and then to $g_{n} = h_{z, n}^{2}$ , using $∣ h_{z, n}^{2} ∣ \leq B^{2}$ . With $\overline{h}_{z, n} (ω) := \frac{1}{m _{z, n}} j : Z_{j n} = z \sum h_{z, n} (A_{j n}), \overline{h^{2}}_{z, n} (ω) := \frac{1}{m _{z, n}} j : Z_{j n} = z \sum h_{z, n} (A_{j n})^{2},$ we have $\overline{h}_{z, n} - E_{n} h_{z, n} p 0, \overline{h^{2}}_{z, n} - E_{n} h_{z, n}^{2} p 0.$ The sample-variance identity gives, eventually, $s_{z, n}^{2} = \frac{m _{z, n}}{m _{z, n} - 1} {\overline{h^{2}}_{z, n} - \overline{h}_{z, n}^{2}} .$ Because $m_{z, n} / (m_{z, n} - 1) \to 1$ , and the selected means are bounded by $B$ , the square map preserves convergence in probability here. Thus $s_{z, n}^{2} p E_{n} h_{z, n}^{2} - (E_{n} h_{z, n})^{2} = V_{z, n} .$
By Definition 12 and Definition 11, $G_{n} V_{CR2, n} - R_{n} = \frac{s _{1, n}^{2} - V _{1, n}}{p _{n}} + \frac{s _{0, n}^{2} - V _{0, n}}{1 - p _{n}}$ eventually. Since $p_{n} \to p \in (0, 1)$ , both reciprocal factors are bounded deterministic sequences. Combining this boundedness with the two armwise convergences in the preceding step yields $G_{n} V_{CR2, n} - R_{n} p 0.$
Define, for every $n$ , $d_{n} := R_{n} - ρ E_{τ, 1, n} .$ The first conclusion of Theorem 3 supplies $G_{n} σ_{n}^{2} - d_{n} \to 0.$ Subtracting this deterministic convergence from the stochastic expansion just proved gives $G_{n} (V_{CR2, n} - σ_{n}^{2}) - ρ E_{τ, 1, n} = (G_{n} V_{CR2, n} - R_{n}) - (G_{n} σ_{n}^{2} - d_{n}) p 0.$
The scaled-variance nondegeneracy condition in Definition 13 gives $\frac{c _{σ}}{2} < G_{n} σ_{n}^{2}$ eventually. Since $G_{n} σ_{n}^{2} - d_{n} \to 0$ , for all sufficiently large $n$ , $G_{n} σ_{n}^{2} - d_{n} < \frac{c _{σ}}{4}, and hence \frac{c _{σ}}{4} < d_{n} .$ Thus $d_{n}$ is eventually positive and bounded away from zero.
Set $r_{n} := \frac{R _{n}}{d _{n}} .$ From the first expansion and the eventual lower bound on $d_{n}$ , $\frac{G _{n} V _{CR2, n}}{d _{n}} - \frac{R _{n}}{d _{n}} = (G_{n} V_{CR2, n} - R_{n}) d_{n}^{- 1} p 0.$ Similarly, $\frac{G _{n} σ _{n}^{2}}{d _{n}} - 1 = \frac{G _{n} σ _{n}^{2} - d _{n}}{d _{n}} \to 0.$ The deterministic target $r_{n}$ is eventually bounded. To see this, bounded potential outcomes give $V_{z, n} \leq B^{2}$ , while $p_{n} \to p \in (0, 1)$ gives $\frac{p}{2} < p_{n}, \frac{1 - p}{2} < 1 - p_{n}$ eventually. Hence, eventually, $0 \leq R_{n} \leq \frac{B ^{2}}{p /2} + \frac{B ^{2}}{( 1 - p ) /2} =: \overline{R}, ∣ r_{n} ∣ \leq \overline{R} \frac{4}{c _{σ}} .$ Let $X_{n} (ω) := \frac{G _{n} V _{CR2, n} ( ω )}{d _{n}}, Y_{n} := \frac{G _{n} σ _{n}^{2}}{d _{n}} .$ The preceding displays give $X_{n} - r_{n} p 0$ and $Y_{n} \to 1$ . Since $Y_{n}$ is eventually bounded away from zero and $r_{n}$ is eventually bounded, $\frac{X _{n}}{Y _{n}} - r_{n} = \frac{( X _{n} - r _{n} ) + r _{n} ( 1 - Y _{n} )}{Y _{n}} p 0.$ Because $X_{n} / Y_{n} = V_{CR2, n} / σ_{n}^{2}$ on the same eventual rows, this gives $\frac{V _{CR2, n}}{σ _{n}^{2}} p r_{n} = \frac{R _{n}}{R _{n} - ρ E _{τ, 1, n}} .$
Define $q_{n} := \frac{ρ E _{τ, 1, n}}{d _{n}} = \frac{ρ E _{τ, 1, n}}{R _{n} - ρ E _{τ, 1, n}} .$ For all sufficiently large $n$ , $d_{n} \neq = 0$ , and hence $r_{n} = \frac{R _{n}}{d _{n}} = \frac{d _{n} + ρ E _{τ, 1, n}}{d _{n}} = 1 + q_{n} .$ Moreover $ρ \geq 0$ by the sampling-fraction condition, and $E_{τ, 1, n} \geq 0$ because it is a squared norm. Since $d_{n} > 0$ eventually, $r_{n} = 1 + q_{n} \geq 1$ eventually.
Fix $ε > 0$ . On every row for which $r_{n} \geq 1$ , ${\frac{V _{CR2, n}}{σ _{n}^{2}} < 1 - ε} \subseteq {ε \leq \frac{V _{CR2, n}}{σ _{n}^{2}} - r_{n}} .$ The right-hand probability tends to zero because $V_{CR2, n} / σ_{n}^{2} p r_{n}$ . Therefore $Pr {V_{CR2, n} / σ_{n}^{2} < 1 - ε} \to 0.$
It remains to prove the equivalence. Suppose first that $\frac{V _{CR2, n}}{σ _{n}^{2}} p 1.$ Together with $\frac{V _{CR2, n}}{σ _{n}^{2}} p r_{n},$ uniqueness of deterministic probability limits gives $r_{n} \to 1$ : indeed, if $∣ r_{n} - 1∣ \geq η$ , the triangle inequality forces at least one of $\frac{V _{CR2, n}}{σ _{n}^{2}} - r_{n} \geq \frac{η}{2}, \frac{V _{CR2, n}}{σ _{n}^{2}} - 1 \geq \frac{η}{2}$ to occur. Since $q_{n} = r_{n} - 1$ eventually, this yields $q_{n} \to 0$ , namely $\frac{ρ E _{τ, 1, n}}{R _{n} - ρ E _{τ, 1, n}} \to 0.$
Conversely, assume $\frac{ρ E _{τ, 1, n}}{R _{n} - ρ E _{τ, 1, n}} \to 0.$ That is, $q_{n} \to 0$ . Since $r_{n} = 1 + q_{n}$ eventually, $r_{n} \to 1$ . Retargeting the already proved convergence $\frac{V _{CR2, n}}{σ _{n}^{2}} p r_{n}$ to the deterministic limit $1$ gives $\frac{V _{CR2, n}}{σ _{n}^{2}} p 1.$ This proves the asserted if and only if.

∎

Proof of Theorem 5.

Since $M \geq 2$ , in particular $M > 0$ . We prove the three asserted conclusions in the order in which they are stated.

Sparse dense arrays. Let $A$ be a feasible triangular schedule array with common group size $M$ , and suppose that $A \in C_{dense}$ in Definition 13 with limiting grouped-unit fraction $ρ = 0$ . Equip each row with the canonical Johnson projections. The canonical decomposition and Kneser-spectrum hypotheses required by Theorem 4 are supplied by Lemmas 3 and 2. Applying Theorem 4 with $ρ = 0$ , its ratio criterion becomes $\frac{0 \cdot E _{τ, 1, n}}{R _{n} - 0 \cdot E _{τ, 1, n}} = 0 for every row n,$ so the criterion converges to $0$ . Hence $\frac{V _{CR2, n}}{σ _{n}^{2}} p 1.$
Birthday counts. Define $G_{n}^{bd} = ⌊ \frac{n ^{3/4}}{M} ⌋, N_{n}^{bd} = M G_{n}^{bd} .$ For $n \geq 1$ , $N_{n}^{bd} = M ⌊ \frac{n ^{3/4}}{M} ⌋ \leq M \frac{n ^{3/4}}{M} = n^{3/4} \leq n,$ so $N_{n}^{bd} \leq n$ eventually. For $n > 0$ , $\frac{N _{n}^{bd}}{n} = \frac{⌊ n ^{3/4} / M ⌋}{n ^{3/4} / M} n^{- 1/4} .$ Since $n^{3/4} / M \to \infty$ , the floor ratio tends to $1$ , while $n^{- 1/4} \to 0$ . Therefore $\frac{N _{n}^{bd}}{n} \to 0.$ For divergence of the squared count, the elementary floor bound gives $n^{3/4} - M \leq M ⌊ \frac{n ^{3/4}}{M} ⌋ = N_{n}^{bd} .$ Eventually $n^{3/4} \geq 2 M$ , and hence $\frac{n ^{3/4}}{2} \leq N_{n}^{bd} .$ Consequently, for all sufficiently large $n$ , $\frac{( N _{n}^{bd} ) ^{2}}{n} \geq \frac{( n ^{3/4} /2 ) ^{2}}{n} = \frac{1}{4} n^{1/2} \to \infty.$
Birthday-aligned arrays. Let $A$ be a feasible triangular schedule array satisfying the rowwise birthday alignment, Assumptions 1, 2, 4, and 5. For row $r \in N$ , write $G_{r}$ for the group count, $n_{r}$ for the population size, and $N_{r} = M G_{r}$ for the grouped-unit count. From Assumption 1, $G_{r} \to \infty$ , and feasibility gives $G_{r} \leq M G_{r} = N_{r} \leq n_{r} .$ Thus $n_{r} \to \infty$ . The alignment condition says $N_{r} = M ⌊ \frac{n _{r}^{3/4}}{M} ⌋ = N_{n_{r}}^{bd},$ and the birthday-count limit from the previous step therefore yields $\frac{N _{r}}{n _{r}} = \frac{N _{n_{r}}^{bd}}{n _{r}} \to 0.$ Together with $0 \leq 0 \leq 1$ , this is exactly Assumption 3 with limiting grouped-unit fraction $ρ = 0$ . The assumed group-count growth, stable treatment fraction, bounded potential outcomes, and scaled-variance nondegeneracy then place $A$ in $C_{dense}$ with $ρ = 0$ by Definition 13. The first step applies and gives $\frac{V _{CR2, n}}{σ _{n}^{2}} p 1.$

∎

Proof of Proposition 1.

Write $T_{n} \subseteq {1, \dots, G_{n}}$ for the realized treated-group set, so $∣ T_{n} ∣ = G_{1 n}$ , and write $C_{n} = T_{n}^{c}$ , so $∣ C_{n} ∣ = G_{0 n} = G_{n} - G_{1 n}$ . For a group $g$ , define $G_{g, n} := {G_{1 n}, G_{0 n}, g \in T_{n}, g \in C_{n} .$ The assumptions $G_{1 n} \geq 2$ and $G_{0 n} \geq 2$ imply $G_{1 n} \leq G_{n}$ , $G_{n} > 0$ , $M > 0$ , $G_{0 n} > 0$ , and the real denominators $G_{1 n}$ and $G_{0 n}$ are nonzero. The two versioned source identities give $sandwich :: bread (fit) = G_{n} M (X^{T} X)^{- 1}$ for the unweighted full-rank least-squares fit (Zeileis et al., 2026), and $Σ = B {g = 1 \sum G_{n} X_{g}^{T} A_{g} e_{g} e_{g}^{T} A_{g}^{T} X_{g}} B$ for the CR2 call with omitted $target$ , $inverse_var$ , and $form$ (Pustejovsky, 2026). The stated bread scaling therefore yields $B = (X^{T} X)^{- 1} .$
The fitted design has group block $X_{g} = 1_{M} x_{g}^{T}, x_{g} = {(1, 1)^{T}, (1, 0)^{T}, g \in T_{n}, g \in C_{n},$ where $1_{M}$ is the $M$ -vector of ones. Summing the block cross-products gives $X^{T} X = g = 1 \sum G_{n} X_{g}^{T} X_{g} = M (G_{n} G_{1 n} G_{1 n} G_{1 n}) .$ Since the determinant is $M^{2} G_{1 n} G_{0 n} > 0$ , inversion gives the entries used below: $B_{10} = B_{01} = - \frac{1}{M G _{0 n}}, B_{11} = \frac{1}{M G _{0 n}} + \frac{1}{M G _{1 n}}, B_{00} = \frac{1}{M G _{0 n}} .$
For every group $g$ , the leverage block is $H_{g} = X_{g} B X_{g}^{T} .$ Using the preceding inverse entries and the two possible values of $x_{g}$ , $(H_{g})_{ij} = \frac{1}{M G _{g, n}}, 1 \leq i, j \leq M .$ Thus $I_{M} - H_{g} = I_{M} - \frac{1}{G _{g, n}} P_{M}, P_{M} := \frac{1}{M} 1_{M} 1_{M}^{T} .$ Let $q = G_{g, n}$ . Since $q \geq 2$ , the symmetric positive-definite matrix $A_{g}$ satisfying $A_{g} A_{g} (I_{M} - H_{g}) = I_{M}$ is determined by its action on the span of $1_{M}$ and on its orthogonal complement. For $u := 1_{M}, v_{j} := e_{j} - \frac{1}{M} u,$ one has $(I_{M} - H_{g}) v_{j} = v_{j}, (I_{M} - H_{g}) u = \frac{q - 1}{q} u .$ The identity $A_{g} A_{g} (I_{M} - H_{g}) = I_{M}$ , together with positive definiteness, therefore gives $A_{g} v_{j} = v_{j}, A_{g} u = \frac{q}{q - 1} u .$ Combining these two relations column by column, $(A_{g})_{ij} = 1 {i = j} + \frac{G _{g, n} / ( G _{g, n} - 1 ) - 1}{M} .$
Summing the displayed entries down any column gives $i = 1 \sum M (A_{g})_{ij} = \frac{G _{g, n}}{G _{g, n} - 1} .$ Consequently $1_{M}^{T} A_{g} e_{g} = i = 1 \sum M (A_{g} e_{g})_{i} = \frac{G _{g, n}}{G _{g, n} - 1} j = 1 \sum M e_{g j} .$ The residual-mean condition in the statement says $\frac{1}{M} j = 1 \sum M e_{g j} = H_{g, n}^{obs} - \overset{ˉ}{H}_{z_{g}, n},$ where $H_{g, n}^{obs} := obsGroupMean (Y, A_{n}, Z_{n}; g), \overset{ˉ}{H}_{z, n} := armObsMean (Y, A_{n}, Z_{n}; z),$ and $z_{g} = 1$ on $T_{n}$ , $z_{g} = 0$ on $C_{n}$ . Hence $j = 1 \sum M e_{g j} = M {H_{g, n}^{obs} - \overset{ˉ}{H}_{z_{g}, n}} .$
Define the treatment-coordinate adjusted cluster score by $q_{g, n} := [B X_{g}^{T} A_{g} e_{g}]_{1} .$ Using $X_{g} = 1_{M} x_{g}^{T}$ , the inverse entries in Step 2, and the residual sum from Step 4 gives the two cases $q_{g, n} = ⎩ ⎨ ⎧ \frac{G _{1 n}}{G _{1 n} - 1} \frac{H _{g, n}^{obs} - H ˉ _{1, n}}{G _{1 n}}, - \frac{G _{0 n}}{G _{0 n} - 1} \frac{H _{g, n}^{obs} - H ˉ _{0, n}}{G _{0 n}}, g \in T_{n}, g \in C_{n} .$
Because $B$ is symmetric, each summand in the CR2 sandwich is a rank-one outer product after premultiplication and postmultiplication by $B$ . Indeed, with $P_{g} := B X_{g}^{T} A_{g},$ $B X_{g}^{T} A_{g} e_{g} e_{g}^{T} A_{g}^{T} X_{g} B = P_{g} e_{g} e_{g}^{T} P_{g}^{T} = (P_{g} e_{g}) (P_{g} e_{g})^{T} .$ Therefore $Σ = g = 1 \sum G_{n} (B X_{g}^{T} A_{g} e_{g}) (B X_{g}^{T} A_{g} e_{g})^{T},$ and its treatment-coordinate entry is $Σ_{11} = g = 1 \sum G_{n} q_{g, n}^{2} .$
Squaring the two cases in Step 5 and using $G_{1 n}, G_{0 n} \geq 2$ gives $Σ_{11} = g \in T_{n} \sum \frac{( H _{g, n}^{obs} - H ˉ _{1, n} ) ^{2}}{( G _{1 n} - 1 ) G _{1 n}} + g \in C_{n} \sum \frac{( H _{g, n}^{obs} - H ˉ _{0, n} ) ^{2}}{( G _{0 n} - 1 ) G _{0 n}} .$ Equivalently, $Σ_{11} = \frac{1}{G _{1 n}} \frac{\sum _{g \in T_{n}} ( H _{g, n}^{obs} - H ˉ _{1, n} ) ^{2}}{G _{1 n} - 1} + \frac{1}{G _{0 n}} \frac{\sum _{g \in C_{n}} ( H _{g, n}^{obs} - H ˉ _{0, n} ) ^{2}}{G _{0 n} - 1} .$ By Definition 12, the two displayed fractions are $s_{1, n}^{2}$ and $s_{0, n}^{2}$ , respectively, and hence $Σ_{11} = \frac{s _{1, n}^{2}}{G _{1 n}} + \frac{s _{0, n}^{2}}{G _{0 n}} = V_{CR2, n} .$

∎

Proof of Proposition 2.

Let $Σ_{8} : Ω_{8, 2} \to R, Σ_{8} (A) = u \in A \sum a_{u} .$ By Definitions 17 and 5, $h_{1, 8} (A) = \frac{Σ _{8} ( A )}{2}, h_{0, 8} (A) = 0 (A \in Ω_{8, 2}) .$ The vector $a_{8}$ has four $+ 1$ entries and four $- 1$ entries, so its population mean is zero and its population variance is one. The usual fixed-size sample-mean identity for a uniform two-subset gives $E_{8} h_{1, 8} = 0, V_{1, 8} = Var_{A \sim Unif (Ω_{8, 2})} {\frac{Σ _{8} ( A )}{2}} = \frac{8 - 2}{2 ( 8 - 1 )} \cdot 1 = \frac{3}{7} .$ Since $h_{0, 8}$ is identically zero, its centered table is zero, hence $V_{0, 8} = 0, C_{00, 8} = C_{10, 8} = C_{01, 8} = 0.$

For the treated ordered-disjoint covariance, write the eight-unit population and its two-subset slice as $U_{8} = {1, \dots, 8}, Ω_{8, 2} = {A \subseteq U_{8} : ∣ A ∣ = 2} .$ Use ordered pairs $(A, C) \in Ω_{8, 2} \times Ω_{8, 2}, A \cap C = \emptyset .$ There are $(2 8) (2 6) = 420$ such ordered pairs. For fixed $A$ , each unit in the six-point complement of $A$ appears in five two-subsets of that complement, and $\sum_{u \in U_{8}} a_{u} = 0$ . Therefore $C \in Ω_{8, 2} C \cap A = \emptyset \sum Σ_{8} (C) = 5 u \in / A \sum a_{u} = - 5 Σ_{8} (A) .$ Also $\sum_{A \in Ω_{8, 2}} Σ_{8} (A)^{2} = 48$ , because the six same-positive pairs and six same-negative pairs contribute $4$ each and the sixteen mixed pairs contribute $0$ . Thus $A, C \in Ω_{8, 2} A \cap C = \emptyset \sum Σ_{8} (A) Σ_{8} (C) = - 5 A \in Ω_{8, 2} \sum Σ_{8} (A)^{2} = - 240.$ Using $E_{8} h_{1, 8} = 0$ , this gives $C_{11, 8} = \frac{1}{420} A, C \in Ω_{8, 2} A \cap C = \emptyset \sum \frac{Σ _{8} ( A )}{2} \frac{Σ _{8} ( C )}{2} = \frac{- 240}{1680} = - \frac{1}{7} .$ Consequently $C_{τ τ, 8} = C_{11, 8} + C_{00, 8} - 2 C_{10, 8} = - \frac{1}{7} .$

Define the arm-difference table $Δ_{8} : Ω_{8, 2} \to R, Δ_{8} (A) = h_{1, 8} (A) - h_{0, 8} (A) .$ Since $h_{0, 8} = 0$ , $Δ_{8} = h_{1, 8}$ , so $E_{8} Δ_{8} = 0, Var_{E_{8}} (Δ_{8}) = \frac{3}{7} .$ Set $η_{1} = ∥ Π_{8, 1} Δ_{8} ∥_{8}^{2}, η_{2} = ∥ Π_{8, 2} Δ_{8} ∥_{8}^{2} .$ The centered Johnson decomposition assumed in the proposition gives $Δ_{8} = Π_{8, 1} Δ_{8} + Π_{8, 2} Δ_{8}$ and the two summands are orthogonal. Hence $η_{1} + η_{2} = ∥ Δ_{8} ∥_{8}^{2} = \frac{3}{7} .$ By Theorem 1, instantiated with $n = 8$ and $M = 2$ , $C_{τ τ, 8} = λ_{8, 1} η_{1} + λ_{8, 2} η_{2} .$ The Kneser eigenvalues are $λ_{8, 1} = - \frac{2}{6} = - \frac{1}{3}, λ_{8, 2} = \frac{2 \cdot 1}{6 \cdot 5} = \frac{1}{15} .$ Using $C_{τ τ, 8} = - 1/7$ , $- \frac{1}{3} η_{1} + \frac{1}{15} η_{2} = - \frac{1}{7} .$ Together with $η_{1} + η_{2} = 3/7$ , this linear system gives $η_{1} = \frac{3}{7} .$ By Definition 11, $η_{1} = E_{τ, 1, 8}$ , so $E_{τ, 1, 8} = \frac{3}{7} .$

It remains to evaluate the design variance and the CR2 expectation. Here $G_{8} = 4, G_{1, 8} = 2, G_{0, 8} = 2, p_{8} = \frac{1}{2} .$ By Definition 11, $R_{8} = \frac{V _{1, 8}}{p _{8}} + \frac{V _{0, 8}}{1 - p _{8}} = \frac{3/7}{1/2} + 0 = \frac{6}{7} .$ Applying Theorem 2 to the feasible eight-unit design gives $σ_{8}^{2} = \frac{R _{8}}{G _{8}} + C_{τ τ, 8} - \frac{C _{11, 8}}{G _{1, 8}} - \frac{C _{00, 8}}{G _{0, 8}} .$ Substituting the displayed values, $σ_{8}^{2} = \frac{6/7}{4} - \frac{1}{7} - \frac{- 1/7}{2} - 0 = \frac{1}{7} .$ The same result in Theorem 2, now for the statistic in Definition 12, gives $E [V_{CR2, 8}] = \frac{V _{1, 8} - C _{11, 8}}{G _{1, 8}} + \frac{V _{0, 8} - C _{00, 8}}{G _{0, 8}} .$ Therefore $E [V_{CR2, 8}] = \frac{3/7 + 1/7}{2} + 0 = \frac{2}{7} .$

∎

Proof of Proposition 3.

Fix a row $n$ and a realized design $w = (A_{n}, Z_{n})$ . Under the independent-sign prior, define the selected sign field $ξ_{i}^{w} := ξ_{i, α_{w} (i)}, α_{w} (i) := 1 {i is observed in a treated realized group under w} .$ Because the realized groups are pairwise disjoint, every observed unit has $α_{w} (i)$ equal to its realized treatment arm. Hence the observation produced from the independent schedule is exactly the observation produced from the common-sign schedule with signs $(ξ_{i}^{w})_{i \in U_{n}}$ . For fixed $w$ , the vector $(ξ_{i}^{w})_{i}$ has the same product Rademacher law as the common-sign vector. Finite Fubini then gives, for every statistic $φ$ , $E_{H_{n}^{same}} E_{Z_{n}} {φ (O_{n})} = E_{Z_{n}} E_{H_{n}^{same}} {φ (O_{n})} = E_{Z_{n}} E_{H_{n}^{ind}} {φ (O_{n})} = E_{H_{n}^{ind}} E_{Z_{n}} {φ (O_{n})} .$
For any deterministic vector $x = (x_{i})_{i \in U_{n}}$ , write $\overset{x}{ˉ}_{n} := \frac{1}{n} i \in U_{n} \sum x_{i}, PV_{n} (x) := \frac{1}{n - 1} i \in U_{n} \sum (x_{i} - \overset{x}{ˉ}_{n})^{2}, m_{x} (Q) := \frac{1}{M} i \in Q \sum x_{i}$ for $Q \in Ω_{n, M}$ . Sampling without replacement gives $Var_{Q \sim Unif (Ω_{n, M})} {m_{x} (Q)} = (\frac{1}{M} - \frac{1}{n}) PV_{n} (x) .$ If $x_{i} \in {- 1, 1}$ , then $PV_{n} (x) = \frac{n}{n - 1} (1 - \overset{x}{ˉ}_{n}^{2}) .$ Under the common-sign prior, $E \overset{ˉ}{ξ}_{n} = 0$ and $Var (\overset{ˉ}{ξ}_{n}) = \frac{1}{n},$ so $\overset{ˉ}{ξ}_{n} \to 0$ in probability. Since Assumption 1 implies $n \to \infty$ , $(\frac{1}{M} - \frac{1}{n}) \frac{n}{n - 1} \to \frac{1}{M},$ and therefore, for each arm $z$ , $V_{z, n} ⟶ p \frac{1}{M} under H_{n}^{same} .$
The same calculation applies arm by arm under $H_{n}^{ind}$ . For each fixed arm $z$ , $\overset{ˉ}{ξ}_{z, n} := \frac{1}{n} i \in U_{n} \sum ξ_{i, z}, E \overset{ˉ}{ξ}_{z, n} = 0, Var (\overset{ˉ}{ξ}_{z, n}) = \frac{1}{n},$ so $\overset{ˉ}{ξ}_{z, n} \to 0$ in probability and $V_{z, n} ⟶ p \frac{1}{M} under H_{n}^{ind} .$
Under $H_{n}^{same}$ , the two arm tables coincide pointwise: $h_{1, n} (Q) - h_{0, n} (Q) = 0 (Q \in Ω_{n, M}) .$ By linearity of the Johnson projection, $E_{τ, 1, n} = ∥ Π_{n, 1} (h_{1, n} - h_{0, n}) ∥_{n}^{2} = ∥ Π_{n, 1} 0 ∥_{n}^{2} = 0.$ Thus $E_{τ, 1, n} \to p 0$ under $H_{n}^{same}$ .
Under $H_{n}^{ind}$ , put $d_{i} := ξ_{i, 1} - ξ_{i, 0}, \overset{ˉ}{d}_{n} := \frac{1}{n} i \sum d_{i}, \overset{c}{ˉ}_{n} := \frac{1}{n} i \sum ξ_{i, 1} ξ_{i, 0} .$ The arm-difference table is the slice sample mean $h_{1, n} (Q) - h_{0, n} (Q) = m_{d} (Q) .$ This function is a linear combination of degree-one inclusion indicators; after subtracting its slice mean, it is orthogonal to constants and lies in $H_{n, 1}$ . Hence the degree-one projection equals the centered sample mean, and $E_{τ, 1, n} = (\frac{1}{M} - \frac{1}{n}) PV_{n} (d) .$ Since $PV_{n} (d) = \frac{n}{n - 1} (2 - 2 \overset{c}{ˉ}_{n} - \overset{ˉ}{d}_{n}^{2}),$ while $\overset{c}{ˉ}_{n} \to 0$ , $\overset{ˉ}{ξ}_{1, n} \to 0$ , and $\overset{ˉ}{ξ}_{0, n} \to 0$ in probability, we get $E_{τ, 1, n} ⟶ p \frac{2}{M} under H_{n}^{ind} .$
By Assumption 2, $p_{n} \to p, 0 < p < 1,$ and hence $\frac{1}{p _{n}} \to \frac{1}{p}, \frac{1}{1 - p _{n}} \to \frac{1}{1 - p} .$ Consequently, for either prior, $Θ_{n} := \frac{V _{1, n}}{p _{n}} + \frac{V _{0, n}}{1 - p _{n}} ⟶ p \frac{1}{M} (\frac{1}{p} + \frac{1}{1 - p}) = \frac{1}{M p ( 1 - p )} .$
Since $0 < G_{1 n} < G_{n}$ , every row has $G_{n} \geq 2$ , and therefore $2 M \leq M G_{n} \leq n$ . The degree-one Kneser eigenvalue in Theorem 1 is $λ_{n, 1} = - \frac{M}{n - M} .$ Thus $λ_{n, 1} \to 0$ . Writing $N_{n} = M G_{n}$ for the grouped-unit count and using Assumption 3, $G_{n} λ_{n, 1} = - \frac{M G _{n}}{n - M} = - \frac{N _{n} / n}{1 - M / n} ⟶ - ρ .$
The exact rowwise variance identity is used on the eventual rows where both treatment arms contain at least two realized groups. These rows are eventual because $p_{n} \to p \in (0, 1)$ and $G_{n} \to \infty$ : eventually $p_{n} > p /2$ and $G_{n} > 4/ p$ , forcing $G_{1 n} \geq 2$ , and eventually $p_{n} < (1 + p) /2$ and $G_{n} > 4/ (1 - p)$ , forcing $G_{0 n} \geq 2$ .

On those rows, Theorems 2 and 1 give $G_{n} σ_{n}^{2} = Θ_{n} + G_{n} λ_{n, 1} E_{τ, 1, n} - λ_{n, 1} Θ_{n} = (1 - λ_{n, 1}) Θ_{n} + G_{n} λ_{n, 1} E_{τ, 1, n} .$ Combining the convergence statements above yields $G_{n} σ_{n}^{2} ⟶ p \frac{1}{M p ( 1 - p )} under H_{n}^{same},$ and $G_{n} σ_{n}^{2} ⟶ p \frac{1}{M p ( 1 - p )} - \frac{2 ρ}{M} under H_{n}^{ind} .$
The separation is positive because $M > 0$ and $ρ > 0$ : $0 < \frac{2 ρ}{M} .$ Also Assumption 3 gives $ρ \leq 1$ , and $p (1 - p) \leq 1/4$ follows from $(p - 1/2)^{2} \geq 0$ . Since $p (1 - p) > 0$ , $\frac{1}{M p ( 1 - p )} - \frac{2 ρ}{M} = \frac{1}{M} (\frac{1}{p ( 1 - p )} - 2 ρ) \geq \frac{1}{M} (4 - 2 ρ) \geq \frac{2}{M} .$
Finally, if $X_{n} \to c$ in probability and $t < c$ , then $Pr {X_{n} < t} \leq Pr {∣ X_{n} - c ∣ > c - t} \to 0, Pr {X_{n} \geq t} \to 1.$ Apply this with $X_{n} = G_{n} σ_{n}^{2}$ . The same-sign limit exceeds the independent-sign limit by $2 ρ / M$ , so every $0 < c_{σ} < \frac{1}{M p ( 1 - p )} - \frac{2 ρ}{M}$ lies below both limits. Therefore $H_{n}^{same} Pr {G_{n} σ_{n}^{2} \geq c_{σ}} \to 1, H_{n}^{ind} Pr {G_{n} σ_{n}^{2} \geq c_{σ}} \to 1.$

∎

Proof of Theorem 6.

Define $d_{same} = \frac{1}{M p ( 1 - p )}, d_{ind} = d_{same} - \frac{2 ρ}{M} .$ By Proposition 3, the unconditioned same-sign and independent-arm one-realization mixtures have identical bounded-test expectations, and the scaled exact variances satisfy $G_{n} σ_{n}^{2} (Y_{n}^{same}) p d_{same}, G_{n} σ_{n}^{2} (Y_{n}^{ind}) p d_{ind}$ under their respective Rademacher schedule priors. The same result also gives $0 < 2 ρ / M$ , hence $d_{ind} < d_{same} .$ The hypothesis on $c_{σ}$ gives $c_{σ} < d_{ind}$ , and therefore also $c_{σ} < d_{same}$ .
We extract deterministic high-probability supports from these two convergence-in-probability statements. For $j \in {same, ind}$ , let $d_{j}$ denote the corresponding limit and let $X_{j, n} (ω) = G_{n} σ_{n}^{2} (Y_{n}^{j, ω})$ for a schedule-prior sign configuration $ω$ . Since $X_{j, n} \to d_{j}$ in probability, for each integer $k \geq 1$ choose $N_{j, k}$ such that, whenever $n \geq N_{j, k}$ , $H_{n}^{j} {∣ X_{j, n} - d_{j} ∣ \geq k^{- 1}} < k^{- 1} .$ Let $ℓ_{j} (n)$ be the largest $k \leq n$ with $N_{j, k} \leq n$ , using $ℓ_{j} (n) = 1$ when the set is empty, and set $e_{j, n} = ℓ_{j} (n)^{- 1}, Γ_{n}^{j} = {ω : ∣ X_{j, n} (ω) - d_{j} ∣ < e_{j, n}} .$ Then $ℓ_{j} (n) \to \infty$ , so $e_{j, n} \to 0$ , and $H_{n}^{j} (Γ_{n}^{j}) \to 1, ω \in Γ_{n}^{j} sup ∣ G_{n} σ_{n}^{2} (Y_{n}^{j, ω}) - d_{j} ∣ \to 0.$ These are the supports $Γ_{n}^{same}$ and $Γ_{n}^{ind}$ .
Every full diagonal selection from either support belongs to $C_{dense}$ . Indeed, for the same-sign prior a selected row has the additive form $Y_{i, n}^{same, ξ} (z, A) = ξ_{i}, ξ_{i} \in {- 1, 1},$ and for the independent-arm prior it has the additive form $Y_{i, n}^{ind, ζ} (z, A) = ζ_{i, z}, ζ_{i, z} \in {- 1, 1} .$ Thus $∣ Y_{i, n} (z, A) ∣ = 1 \leq B$ . The original design skeleton supplies the group-count, treated-fraction, and sampling-fraction conditions in Definition 13. For any diagonal selection with $ω_{n} \in Γ_{n}^{j}$ for every $n$ , $G_{n} σ_{n}^{2} (Y_{n}^{j, ω_{n}}) \to d_{j},$ because the support error is bounded by $e_{j, n} \to 0$ . Since $c_{σ} < d_{j}$ , this convergence gives $c_{σ} \leq n \to \infty lim inf G_{n} σ_{n}^{2} (Y_{n}^{j, ω_{n}}) .$ Hence all defining conditions of $C_{dense}$ hold for each such diagonal selection.
Since $H_{n}^{j} (Γ_{n}^{j}) \to 1$ for $j \in {same, ind}$ , both conditioning masses are positive for all sufficiently large $n$ . On those rows, let $E_{n, j}^{Γ}$ denote expectation under the one-realization mixture obtained by first conditioning $H_{n}^{j}$ on $Γ_{n}^{j}$ and then applying the random partition and treatment design, and define $Δ_{n} = 0 \leq φ \leq 1 sup E_{n, same}^{Γ} φ (O_{n}) - E_{n, ind}^{Γ} φ (O_{n}) .$ For the finitely many remaining rows, take $Δ_{n} = 0$ ; this totalization convention has no effect on the limiting assertion. For any bounded test $0 \leq φ \leq 1$ , conditioning a finite prior on a set $Γ$ of positive prior probability changes its expectation by at most twice the complement probability: $∣ E {φ ∣ Γ} - E φ ∣ \leq 2 {1 - H (Γ)} .$ Indeed, writing $m = H (Γ) > 0$ , the conditioned expectation is $E {φ ∣ Γ} = \frac{1}{m} E {1_{Γ} φ},$ and hence $∣ E {φ ∣ Γ} - E φ ∣ = \frac{1 - m}{m} E {1_{Γ} φ} - E {1_{Γ^{c}} φ} \leq \frac{1 - m}{m} E {1_{Γ} φ} + E {1_{Γ^{c}} φ} \leq \frac{1 - m}{m} m + (1 - m) = 2 (1 - m) .$ This derivation also covers the case $m = 1$ , where the unnormalized complement contribution is zero. Applying this bound to the two schedule priors on the eventual-positive rows and using the exact unconditioned equality from Proposition 3 yields $Δ_{n} \leq 2 {1 - H_{n}^{same} (Γ_{n}^{same})} + 2 {1 - H_{n}^{ind} (Γ_{n}^{ind})} .$ The right-hand side tends to $0$ , while $Δ_{n} \geq 0$ because the zero test is admissible on the eventual-positive rows and by convention on the remaining rows. Therefore $Δ_{n} \to 0.$ Together with the previous steps, this proves the support, dense-class, conditioned-total-variation, and uniform scaled-variance parts of the diagonal certificate.
It remains to prove the all-statistic lower bound. Put $ε = \frac{d _{same} - d _{ind}}{8 d _{same}}, η = \frac{d _{same} - d _{ind}}{8} .$ Because $0 < c_{σ} < d_{ind} < d_{same}$ , both $ε$ and $η$ are positive. Fix an arbitrary one-realization variance statistic $S_{n} (O_{n})$ , and define the threshold $ϑ = \frac{d _{same} + d _{ind}}{2} .$ For all sufficiently large $n$ , the supports are nonempty, have positive conditioning probability, and satisfy $e_{same, n} < η$ and $e_{ind, n} < η$ . On such rows define the two wrong-decision tests $ψ_{n}^{same} (o) = 1 {G_{n} S_{n} (o) \leq ϑ}, ψ_{n}^{ind} (o) = 1 {G_{n} S_{n} (o) > ϑ} .$ If $ξ \in Γ_{n}^{same}$ and $\frac{S _{n} ( o )}{σ _{n}^{2} ( Y _{n}^{same, ξ} )} - 1 \leq ε,$ then the support bound gives $∣ G_{n} σ_{n}^{2} (Y_{n}^{same, ξ}) - d_{same} ∣ < η,$ and hence $G_{n} S_{n} (o) > (1 - ε) (d_{same} - η) > \frac{d _{same} + d _{ind}}{2} .$ Thus $ψ_{n}^{same} (o) = 1$ implies relative error greater than $ε$ . Similarly, if $ζ \in Γ_{n}^{ind}$ and the relative error is at most $ε$ , then $G_{n} S_{n} (o) < (1 + ε) (d_{ind} + η) < \frac{d _{same} + d _{ind}}{2},$ so $ψ_{n}^{ind} (o) = 1$ implies relative error greater than $ε$ . The two strict algebraic margins are exactly the displayed choices of $ε$ and $η$ .
Let $W_{n} (S, ε) = Y \in C_{dense} sup Y Pr (\frac{S _{n} ( O _{n} )}{σ _{n}^{2} ( Y )} - 1 > ε) .$ For each $ξ \in Γ_{n}^{same}$ , the preceding implication bounds the same-sign row probability of $ψ_{n}^{same} = 1$ by the corresponding relative-error probability. That row can be embedded into a full triangular array in $C_{dense}$ : keep the row $Y_{n}^{same, ξ}$ at index $n$ , choose arbitrary support rows $Γ_{m}^{same}$ for all sufficiently large $m \neq = n$ , and choose arbitrary bounded sign rows at the finitely many remaining indices. The convergence and class argument from Step 3 applies because membership in the supports is eventual. Therefore $E_{n, same}^{Γ} ψ_{n}^{same} (O_{n}) \leq W_{n} (S, ε) .$ The identical construction for $ζ \in Γ_{n}^{ind}$ gives $E_{n, ind}^{Γ} ψ_{n}^{ind} (O_{n}) \leq W_{n} (S, ε) .$ Averaging over the conditioned finite supports uses only positivity of the conditioning masses.
Since $ψ_{n}^{same} + ψ_{n}^{ind} = 1$ pointwise under the independent-arm observation channel, $E_{n, ind}^{Γ} ψ_{n}^{same} (O_{n}) = 1 - E_{n, ind}^{Γ} ψ_{n}^{ind} (O_{n}) .$ The definition of $Δ_{n}$ , applied to $ψ_{n}^{same}$ , gives $E_{n, same}^{Γ} ψ_{n}^{same} (O_{n}) - E_{n, ind}^{Γ} ψ_{n}^{same} (O_{n}) \leq Δ_{n} .$ Combining the last two displays yields $1 - Δ_{n} \leq E_{n, same}^{Γ} ψ_{n}^{same} (O_{n}) + E_{n, ind}^{Γ} ψ_{n}^{ind} (O_{n}) .$ Using Step 6 on both terms, $\frac{1 - Δ _{n}}{2} \leq W_{n} (S, ε)$ for all sufficiently large $n$ .
Finally, $Δ_{n} \to 0$ , so the left-hand side in the last display converges to $1/2$ . Also $W_{n} (S, ε) \leq 1$ : if the set of dense-class risks is nonempty, this is the supremum of probabilities bounded by one, and if it is empty the supremum convention used here gives $0$ . Hence $\frac{1}{2} \leq n \to \infty lim inf W_{n} (S, ε) .$ Since $S$ was arbitrary, the asserted lower bound holds for every measurable one-realization variance statistic.

∎

References

Jiawei Fu and Cyrus Samii and Ye Wang (2026). Inference for Group Interaction Experiments. . arXiv
Yuval Filmus (2016). An Orthogonal Basis for Functions over a Slice of the Boolean Hypercube. Electronic Journal of Combinatorics. doi
Andries E. Brouwer and Sebastian M. Cioab{\u a} and Ferdinand Ihringer and Matt McGinnis (2018). The Smallest Eigenvalues of Hamming Graphs, Johnson Graphs and Other Distance-Regular Graphs with Classical Parameters. Journal of Combinatorial Theory, Series B. arXiv
Xinran Li and Peng Ding (2017). General Forms of Finite Population Central Limit Theorems with Applications to Causal Inference. Journal of the American Statistical Association. doi
Esbj{\"o}rn Ohlsson (1989). Asymptotic Normality for Two-Stage Sampling from a Finite Population. Probability Theory and Related Fields. doi
James E. Pustejovsky and Elizabeth Tipton (2018). Small-Sample Methods for Cluster-Robust Variance Estimation and Hypothesis Testing in Fixed Effects Models. Journal of Business \& Economic Statistics. doi
Fangzhou Su and Peng Ding (2021). Model-Assisted Analyses of Cluster-Randomized Experiments. Journal of the Royal Statistical Society: Series B. doi
Christopher Harshaw and Joel A. Middleton and Fredrik S{\"a}vje (2026). Optimized Variance Estimation under Interference and Complex Experimental Designs. Journal of the American Statistical Association. doi
Guillaume W. Basse and Edoardo M. Airoldi (2018). Limitations of Design-Based Causal Inference and {A/B} Testing under Arbitrary and Network Interference. Sociological Methodology. doi
Peter M. Aronow and Donald P. Green and Donald K. K. Lee (2014). Sharp Bounds on the Variance in Randomized Experiments. Annals of Statistics. doi
Guillaume Basse and Peng Ding and Avi Feller and Panos Toulis (2024). Randomization Tests for Peer Effects in Group Formation Experiments. Econometrica. doi
David Puelz and Guillaume Basse and Avi Feller and Panos Toulis (2022). A Graph-Theoretic Approach to Randomization Tests of Causal Effects under General Interference. Journal of the Royal Statistical Society: Series B. doi
James E. Pustejovsky (2026). {clubSandwich}: Cluster-Robust (Sandwich) Variance Estimators with Small-Sample Corrections. .
Achim Zeileis and Thomas Lumley (2026). {sandwich}: Robust Covariance Matrix Estimators. .
Jerzy Splawa-Neyman and Dorota M. Dabrowska and Terence P. Speed (1990). On the Application of Probability Theory to Agricultural Experiments. Essay on Principles. Section 9. Statistical Science. doi
Ronald A. Fisher (1935). The Design of Experiments. Oliver and Boyd.
David R. Cox (1958). Planning of Experiments. John Wiley \& Sons.
Donald B. Rubin (1974). Estimating Causal Effects of Treatments in Randomized and Nonrandomized Studies. Journal of Educational Psychology. doi
Paul W. Holland (1986). Statistics and Causal Inference. Journal of the American Statistical Association. doi
William G. Cochran (1977). Sampling Techniques. John Wiley \& Sons.
Jaroslav H{\'a}jek (1960). Limiting Distributions in Simple Random Sampling from a Finite Population. Publications of the Mathematical Institute of the Hungarian Academy of Sciences.
Wayne A. Fuller (2009). Sampling Statistics. John Wiley \& Sons. doi
Philippe Delsarte (1973). An Algebraic Approach to the Association Schemes of Coding Theory. .
Andries E. Brouwer and Arjeh M. Cohen and Arnold Neumaier (1989). Distance-Regular Graphs. Springer. doi
Halbert White (1980). A Heteroskedasticity-Consistent Covariance Matrix Estimator and a Direct Test for Heteroskedasticity. Econometrica. doi
Kung-Yee Liang and Scott L. Zeger (1986). Longitudinal Data Analysis Using Generalized Linear Models. Biometrika. doi
Robert M. Bell and Daniel F. McCaffrey (2002). Bias Reduction in Standard Errors for Linear Regression with Multi-Stage Samples. Survey Methodology.
A. Colin Cameron and Douglas L. Miller (2015). A Practitioner's Guide to Cluster-Robust Inference. Journal of Human Resources. doi
Alberto Abadie and Susan Athey and Guido W. Imbens and Jeffrey M. Wooldridge (2023). When Should You Adjust Standard Errors for Clustering?. Quarterly Journal of Economics. doi
Achim Zeileis (2004). Econometric Computing with {HC} and {HAC} Covariance Matrix Estimators. Journal of Statistical Software. doi
Achim Zeileis (2006). Object-Oriented Computation of Sandwich Estimators. Journal of Statistical Software. doi
Achim Zeileis and Susanne K{\"o}ll and Nathaniel Graham (2020). Various Versatile Variances: An Object-Oriented Implementation of Clustered Covariances in {R}. Journal of Statistical Software. doi
Michael E. Sobel (2006). What Do Randomized Studies of Housing Mobility Demonstrate?: Causal Inference in the Face of Interference. Journal of the American Statistical Association. doi
Michael G. Hudgens and M. Elizabeth Halloran (2008). Toward Causal Inference with Interference. Journal of the American Statistical Association. doi
Eric J. Tchetgen Tchetgen and Tyler J. VanderWeele (2012). On Causal Inference in the Presence of Interference. Statistical Methods in Medical Research. doi
Charles F. Manski (2013). Identification of Treatment Response with Social Interactions. Econometrics Journal. doi
Lan Liu and Michael G. Hudgens (2014). Large Sample Randomization Inference of Causal Effects in the Presence of Interference. Journal of the American Statistical Association. doi
Peter M. Aronow and Cyrus Samii (2017). Estimating Average Causal Effects under General Interference, with Application to a Social Network Experiment. Annals of Applied Statistics. doi
Susan Athey and Dean Eckles and Guido W. Imbens (2018). Exact {p}-Values for Network Interference. Journal of the American Statistical Association. doi
Johan Ugander and Brian Karrer and Lars Backstrom and Jon Kleinberg (2013). Graph Cluster Randomization: Network Exposure to Multiple Universes. Proceedings of the 19th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining. arXiv
Dean Eckles and Brian Karrer and Johan Ugander (2017). Design and Analysis of Experiments in Networks: Reducing Bias from Interference. Journal of Causal Inference. doi
Xinran Li and Peng Ding and Qian Lin and Dawei Yang and Jun S. Liu (2019). Randomization Inference for Peer Effects. Journal of the American Statistical Association. doi
Hui Xu and Guillaume W. Basse (2021). Randomization Inference for Composite Experiments with Spillovers and Peer Effects. . arXiv
Ye Wang and Cyrus Samii and Haoge Chang and Peter M. Aronow (2025). Design-Based Inference for Spatial Experiments under Unknown Interference. Annals of Applied Statistics. doi
Cyrus Samii and Ye Wang and Jonathan Sullivan and Peter M. Aronow (2023). Inference in Spatial Experiments with Interference Using the {SpatialEffect} Package. Journal of Agricultural, Biological and Environmental Statistics. doi
Mengsi Gao and Peng Ding (2025). Causal Inference in Network Experiments: Regression-Based Analysis and Design-Based Properties. Journal of Econometrics. doi
Bryan Park and Stefan Wager (2026). Neyman Jackknife: Design-Based Variance Estimation for Causal Inference under Interference. . arXiv

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 (2)

Setup S-2 — The uniform $M$ -slice $\Omega_{n,M}$ , for $n\ge2M$ , is regarded as the vertex set of the Johnson association scheme. Its function space $L^2(\Omega_{n,M})$ carries harmonic degree subspaces $\mathcal H_{n,0},\ldots,\mathcal H_{n,M}$ with $\langle\cdot,\cdot\rangle_n$ -orthogonal projections $\Pi_{n,k}$ , and the normalized Kneser disjointness operator $(\mathsf K_nf)(A)=\binom{n-M}{M}^{-1}\sum_{C\in\Omega_{n,M}:C\cap A=\varnothing}f(C)$ , which averages $f$ over a uniform group disjoint from $A$ and acts on $\mathcal H_{n,k}$ by the scalar $\lambda_{n,k}$ . The derived quadratic functionals of the arm table are the ordered-disjoint covariances $C_{ab,n}=\langle h_{a,n}^{\circ},\mathsf K_nh_{b,n}^{\circ}\rangle_n$ for $a,b\in\mathcal Z$ , their contrast $C_{\tau\tau,n}=C_{11,n}+C_{00,n}-2C_{10,n}$ , and the degree-one arm-difference energy $E_{\tau,1,n}=\|\Pi_{n,1}(h_{1,n}-h_{0,n})\|_n^2$ . — Redirect-synchronized local Johnson world. The concrete inclusion-monomial filtration defines each canonical harmonic degree space. JohnsonProjections is a genuine orthogonal projection structure with ranges fixed to those spaces, and the node anchor for [def:johnson-decomposition] is the construction johnsonComponents J f built over it (round-4 kind correction: the core node has inputs, so its Lean object is that def, with the structure retained as supporting projection data). The cited Johnson gate supplies centered completeness and cross-degree orthogonality, and the cited Kneser gate states the adjacency eigenvalue on the same canonical spaces. The normalized operator and covariance remain local constructions. Causalean and Mathlib still contain no Johnson/Kneser association-scheme implementation (grep -rni 'johnson|kneser|BoseMesner|associationScheme' ../Causalean → zero hits, re-run this round; Mathlib has only SimpleGraph.StronglyRegular generalities).
Setup S-3 — The two-stage dense random-group design on the population of S1. First an ordered tuple $\mathbf A_n=(A_{n1},\ldots,A_{nG_n})$ is drawn uniformly from the ordered tuples of pairwise-disjoint members of $\Omega_{n,M}$ , so that $N_n=MG_n\le n$ units are grouped and the grouped-unit fraction satisfies $N_n/n\to\rho\in[0,1]$ ; no birthday-scale condition on $N_n^2/n$ is imposed. Then, independently of $\mathbf A_n$ , a group-treatment vector $\mathbf Z_n\in\{0,1\}^{G_n}$ is drawn uniformly among vectors with exactly $G_{1n}$ treated groups, $G_{0n}=G_n-G_{1n}$ , $p_n=G_{1n}/G_n\to p\in(0,1)$ ; treatment is shared within each realized group. The assignment is the only randomness. This world carries the observed group means $H^{\mathrm{obs}}_{ng}=Z_{ng}h_{1,n}(A_{ng})+(1-Z_{ng})h_{0,n}(A_{ng})$ , the estimand $\tau_n=\mathbb E_nh_{1,n}-\mathbb E_nh_{0,n}$ and its difference-in-means estimator $\widehat\tau_n=G_{1n}^{-1}\sum_gZ_{ng}h_{1,n}(A_{ng})-G_{0n}^{-1}\sum_g(1-Z_{ng})h_{0,n}(A_{ng})$ with exact design variance $\sigma_n^2=\operatorname{Var}(\widehat\tau_n)$ , the independent-group leading variance $R_n=V_{1,n}/p_n+V_{0,n}/(1-p_n)$ , the within-arm sample variances $s_{z,n}^2$ and the scalar equal-group CR2 statistic $\widehat V_{\mathrm{CR2},n}=s_{1,n}^2/G_{1n}+s_{0,n}^2/G_{0n}$ . The one-realization observation channel is $\mathcal O_n=(\mathcal U_n,\mathbf A_n,\mathbf Z_n,\{Y_{i,n}(Z_{ng},A_{ng})\})$ , on which an arbitrary variance statistic $\widehat S_n(\mathcal O_n)$ may be computed. Triangular arrays of such rows satisfying growth, fraction, envelope and scaled-variance conditions form the uniformity class $\mathcal C_{\mathrm{dense}}$ with constants $B$ and $c_\sigma$ . There are no superpopulation nuisances. — Partial world reuse: only the stage-one law is new; the stage-two law AND the independent two-stage combination are both existing decls. Stage two is an EXACT reuse: completeRandomization (V := Fin G) G1 h : FiniteDesign {S : Finset (Fin G) // S.card = G1} is exactly the complete randomization of group labels, and completeRandomization_incl / completeRandomization_incl_pair are exactly the first- and second-order moments $p_n$ and $G_{1n}(G_{1n}-1)/(G_n(G_n-1))$ that the variance proof needs. The independent combination of the two stages is EXACT reuse of prodDesign: its signature prodDesign (D : forall i, FiniteDesign (alpha i)) : FiniteDesign (forall i, alpha i) (Product.lean:49, with alpha : iota -> Type* at :43) is parameterized by a DEPENDENT family, so a two-index family alpha : Fin 2 -> Type given by alpha 0 := PartitionTuple n M G, alpha 1 := {S : Finset (Fin G) // S.card = G1} realizes exactly the independent heterogeneous pair; randomPartitionDesign := (prodDesign twoStageDesigns).map (fun w => (w 0, w 1)) then transports the outcome to the product type through the existing pushforward FiniteDesign.map (DesignCore.lean:323) along that Equiv, with FiniteDesign.E_map / Pr_map (:343, :357) carrying every expectation and probability identity across. No local product combinator is written. Structural cross-stage independence is then free from E_prod_prod / E_prod_apply / Cov_prod_apply_of_ne (Product.lean:68,79, ProductVariance.lean:77). Stage one alone has NO analogue in either library: PartitionTuple n M G := {T : Fin G -> Omega n M // Pairwise (fun g g' => Disjoint (T g).val (T g').val)} with the uniform law is new. Convergence in probability reuses FiniteDesign.TendstoInProb / tendstoInProb_of_var / tendstoInProb_div_one / TendstoInProb.sub / deterministic_tendstoInProb / tendstoInProb_continuousMap (InProb.lean, indexed by n exactly as the triangular array needs) and FiniteDesign.chebyshev. FiniteDesign.map (DesignCore.lean:323) pushes the design forward to the observed-data space $\mathcal O_n$ ; FiniteDesign.toMeasure (FiniteDesignMeasure.lean:51) bridges to Causalean.Stat.tvDist. SEARCH: grep -rn 'partition|disjoint.*tuple|perfect matching' ../Causalean/Experimentation → ProductBlock.lean (disjoint coordinate blocks of a product design, not disjoint random subsets), MatchedPairDesign/ (a FIXED pairing P with independent within-pair coins, i.e. the pairing is not randomized) — neither is the random-partition first stage; lean_leansearch 'uniform random partition of a finite set into blocks of equal size' → no Mathlib decl (Finpartition exists but carries no uniform law). RE-SURVEY (round 3, combination step): grep -n 'def prodDesign' -A8 ../Causalean/Experimentation/DesignBased/Product.lean → :49 with variable {alpha : iota -> Type*} [forall i, Fintype (alpha i)] at :43, i.e. the dependent family DOES express a heterogeneous pair over a two-element index; grep -n 'def map|E_map|Pr_map' ../Causalean/Experimentation/DesignBased/DesignCore.lean → :323, :343, :357. The earlier claim that a new heterogeneous pair combinator was needed is withdrawn.

Definitions (9)

Definition P-1 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.randomPartitionDesign Draw $\mathbf A_n$ uniformly from ordered pairwise-disjoint $G_n$ -tuples in $\Omega_{n,M}$ , then independently draw $\mathbf Z_n$ uniformly from assignments with exactly $G_{1n}$ treated groups.
Definition P-2 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armTable For every $z\in\mathcal Z$ and $A\in\Omega_{n,M}$ , set $h_{z,n}(A)=M^{-1}\sum_{i\in A}Y_{i,n}(z,A)$ .
Definition P-3 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.pameAndEstimator Set $\tau_n=\mathbb E_n[h_{1,n}-h_{0,n}]$ and $\widehat\tau_n=G_{1n}^{-1}\sum_gZ_{ng}h_{1,n}(A_{ng})-G_{0n}^{-1}\sum_g(1-Z_{ng})h_{0,n}(A_{ng})$ .
Definition P-4 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.johnsonComponents For every $f\in L^2(\Omega_{n,M})$ , write $f-\mathbb E_nf=\sum_{k=1}^M\Pi_{n,k}f$ orthogonally under $\langle\cdot,\cdot\rangle_n$ .
Definition P-5 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.crossCov Use $(\mathsf K_nf)(A)=\binom{n-M}{M}^{-1}\sum_{C:C\cap A=\varnothing}f(C)$ and $C_{ab,n}=\langle h_{a,n}^{\circ},\mathsf K_nh_{b,n}^{\circ}\rangle_n$ .
Definition P-6 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.denseCorrection Set $E_{\tau,1,n}=\|\Pi_{n,1}(h_{1,n}-h_{0,n})\|_n^2$ and $R_n=V_{1,n}/p_n+V_{0,n}/(1-p_n)$ .
Definition P-7 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.cr2Var Compute the within-arm sample variances $s_{z,n}^2$ with denominator $G_{zn}-1$ , then set $\widehat V_{\mathrm{CR2},n}=s_{1,n}^2/G_{1n}+s_{0,n}^2/G_{0n}$ .
Definition P-8 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.DenseScheduleClass $\mathcal C_{\mathrm{dense}}=\{(Y_{i,n},G_n,G_{1n})_{n\ge1}:G_n\to\infty,\ p_n\to p,\ N_n/n\to\rho,\ \sup_{n,i,z,A}|Y_{i,n}(z,A)|\le B,\ \liminf_nG_n\sigma_n^2\ge c_\sigma\}$ .
Definition P-9 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8Bundle Take $n=N_n=8$ , $M=2$ , $G_n=4$ , $G_{1n}=2$ , $Y_{i,n}(0,A)=0$ , and $Y_{i,n}(1,A)=(a_j+a_k)/2$ for every $i\in A=\{j,k\}$ , where $\mathbf a_8=(a_1,\ldots,a_8)$ .

Assumptions (5)

Assumption A-1 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.GroupCountGrowth $G_n\to\infty$ .
Assumption A-2 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.StableTreatmentFraction $p_n\to p\in(0,1)$ .
Assumption A-3 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.SamplingFractionLimit $N_n/n\to\rho\in[0,1]$ .
Assumption A-4 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.BoundedSchedule $\sup_{n,i,z,A}|Y_{i,n}(z,A)|\le B<\infty$ .
Assumption A-5 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.ScaledVarianceNondegenerate $\liminf_{n\to\infty}G_n\sigma_n^2\ge c_\sigma$ .

Lemmas (3)

Lemma lem:johnson-kneser-adjacency-eigenvalue verified Causalean.Mathlib.Combinatorics.JohnsonKneser.kneserAdjacency_eigen For nonnegative integers $n$ and $M$ with $2M\le n$ , and for a harmonic degree $k\in\{0,\ldots,M\}$ , let $\mathrm{Adj}_{n,M}$ be the linear operator on $L^2(\Omega_{n,M})$ sending $f$ to $\Gamma\mapsto\sum_{\Delta\in\Omega_{n,M}}\mathbf 1\{\Gamma\cap\Delta=\varnothing\}f(\Delta)$ . Then every $f$ in the degree- $k$ Johnson harmonic subspace $\mathcal H_{n,k}$ is an eigenfunction of $\mathrm{Adj}_{n,M}$ with eigenvalue $(-1)^k\binom{n-M-k}{M-k}$ ; that is, $\mathrm{Adj}_{n,M}f=(-1)^k\binom{n-M-k}{M-k}\,f$ as an identity in $L^2(\Omega_{n,M})$ .
Lemma lem:classical-kneser-spectrum verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.canonicalKneserAdjacencySpectrum For the Kneser graph on the $M$ -subsets of an $n$ -set, where adjacency means disjointness and $n\ge2M$ , the unnormalized adjacency eigenvalue on $\mathcal H_{n,k}$ is $(-1)^k\binom{n-M-k}{M-k}$ , for $0\le k\le M$ .
Lemma lem:classical-johnson-decomposition verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.canonicalJohnsonOrthogonalDecomposition On the uniform $M$ -slice with $n\ge2M$ , the Johnson harmonic degree spaces $\mathcal H_{n,0},\ldots,\mathcal H_{n,M}$ form an orthogonal direct-sum decomposition of $L^2(\Omega_{n,M})$ .

Theorems (9)

Theorem T-1 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.exact_kneser_identity For every $n\ge2M$ , $\mathsf K_n$ acts on $\mathcal H_{n,k}$ by $\lambda_{n,k}=(-1)^k(M)_k/(n-M)_k$ . Consequently, for centered $f,g\in L^2(\Omega_{n,M})$ and a uniform ordered disjoint pair $(A,C)$ , $\operatorname{Cov}(f(A),g(C))=\sum_{k=1}^M\lambda_{n,k}\langle\Pi_{n,k}f,\Pi_{n,k}g\rangle_n$ , and $C_{\tau\tau,n}=\sum_{k=1}^M\lambda_{n,k}\|\Pi_{n,k}(h_{1,n}-h_{0,n})\|_n^2$ .
Theorem T-2 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.exact_pame_variance Under the two-stage design, $\mathbb E[\widehat\tau_n]=\tau_n$ and the exact finite-sample variance is $\sigma_n^2=\frac{R_n}{G_n}+C_{\tau\tau,n}-\frac{C_{11,n}}{G_{1n}}-\frac{C_{00,n}}{G_{0n}}.$ Moreover, $\mathbb E[\widehat V_{\mathrm{CR2},n}]=(V_{1,n}-C_{11,n})/G_{1n}+(V_{0,n}-C_{00,n})/G_{0n}$ , so $\mathbb E[\widehat V_{\mathrm{CR2},n}]-\sigma_n^2=-C_{\tau\tau,n}$ exactly.
Theorem T-3 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.dense_projection_limit For every array satisfying group-count growth, stable treatment and sampling fractions, and bounded potential outcomes, $G_n\sigma_n^2=R_n-\rho E_{\tau,1,n}+o(1).$ More precisely, $G_nC_{\tau\tau,n}+\rho E_{\tau,1,n}\to0$ and $C_{11,n}/p_n+C_{00,n}/(1-p_n)\to0$ ; all Johnson degrees $k\ge2$ vanish at the $G_n$ -scale uniformly over the bounded schedules.
Theorem T-4 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.cr2_phase_frontier For every array in $\mathcal C_{\mathrm{dense}}$ , $G_n\widehat V_{\mathrm{CR2},n}-R_n\xrightarrow{p}0 \quad\text{and}\quad G_n\bigl(\widehat V_{\mathrm{CR2},n}-\sigma_n^2\bigr) -\rho E_{\tau,1,n}\xrightarrow{p}0.$ Consequently, CR2 is asymptotically conservative in the sense that, for every $\varepsilon>0$ , $\Pr\!\left\{ \widehat V_{\mathrm{CR2},n}/\sigma_n^2<1-\varepsilon \right\}\longrightarrow0,$ and it is ratio-consistent if and only if $\frac{\rho E_{\tau,1,n}}{R_n-\rho E_{\tau,1,n}}\longrightarrow0.$ These conclusions are unconditional over $\mathcal C_{\mathrm{dense}}$ and use no predictable quadratic-variation premise.
Theorem T-5 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sparse_beyond_birthday For every array in $\mathcal C_{\mathrm{dense}}$ with $\rho=0$ , equivalently $N_n/n\to0$ , $\frac{\widehat V_{\mathrm{CR2},n}}{\sigma_n^2}\xrightarrow{p}1.$ No condition $N_n^2/n\to0$ is imposed. In particular, the conclusion applies whenever the remaining defining conditions of $\mathcal C_{\mathrm{dense}}$ hold with $N_n=M\lfloor n^{3/4}/M\rfloor$ ; these grouped-unit counts satisfy $N_n/n\to0$ but $N_n^2/n\to\infty$ .
Theorem T-6 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.clubsandwich_cr2_consumer_identity Suppose $G_{1n}\ge 2$ and $G_{0n}\ge 2$ . Let ${\tt fit}={\tt lm}(Y^{\mathrm{obs}}\sim Z)$ be unweighted, with only an intercept and numeric binary group treatment, equal group size $M$ , and clusters equal the realized groups. With the default identity target, the treatment-coordinate entry of ${\tt clubSandwich::vcovCR}({\tt fit},\ {\tt cluster}={\tt group},\ {\tt type}={\tt 'CR2'})$ equals $\widehat V_{\mathrm{CR2},n}=s_{1,n}^2/G_{1n}+s_{0,n}^2/G_{0n}$ exactly.
Theorem T-7 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.eight_unit_witness_moments For the balanced $n=N_n=8$ , $M=2$ , $G_n=4$ , $G_{1n}=2$ witness, $V_{1,n}=E_{\tau,1,n}=3/7$ , $C_{11,n}=-1/7$ , $\sigma_n^2=1/7$ , and $\mathbb E[\widehat V_{\mathrm{CR2},n}]=2/7$ . Exhaustive enumeration over the $105$ perfect matchings and the $6$ balanced treatment allocations, totaling $630$ design points, reproduces both moments.
Theorem T-8 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.rademacher_mixture_separation Under $\mathbb H_n^{\mathrm{same}}$ and $\mathbb H_n^{\mathrm{ind}}$ , the induced laws of $\mathcal O_n$ are exactly equal for every $n$ . Suppose $G_n\to\infty$ , $p_n\to p\in(0,1)$ , and $N_n/n\to\rho\in(0,1]$ . With prior probability tending to one, $V_{1,n}\to1/M$ , $V_{0,n}\to1/M$ , and $E_{\tau,1,n}\to0$ under $\mathbb H_n^{\mathrm{same}}$ , whereas $E_{\tau,1,n}\to2/M$ under $\mathbb H_n^{\mathrm{ind}}$ . Hence $G_n\sigma_n^2\to1/(Mp(1-p))$ under the first prior and $G_n\sigma_n^2\to1/(Mp(1-p))-2\rho/M$ under the second. The limit gap is $2\rho/M>0$ , and the smaller limit satisfies $1/(Mp(1-p))-2\rho/M\ge2/M$ . Consequently, for every fixed $c_\sigma$ with $0<c_\sigma<1/(Mp(1-p))-2\rho/M$ , the probability of $G_n\sigma_n^2\ge c_\sigma$ tends to one under each prior; the separated-limit claim is therefore confined to dense rows $\rho>0$ that satisfy scaled-variance nondegeneracy with high prior probability.
Theorem T-9 verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.qv_diagonal_impossibility Fix $M\ge2$ , $p\in(0,1)$ , $\rho\in(0,1]$ , $B\ge1$ , and design sequences satisfying the three fraction and growth assumptions. Put $d_{\mathrm{same}}=\frac1{Mp(1-p)},\qquad d_{\mathrm{ind}}=\frac1{Mp(1-p)}-\frac{2\rho}{M},$ and suppose $0<c_\sigma<d_{\mathrm{ind}}$ . There are high-prior-probability sets of deterministic Rademacher schedule rows whose Cartesian diagonal selections all belong to $\mathcal C_{\mathrm{dense}}$ ; after conditioning $\mathbb H_n^{\mathrm{same}}$ and $\mathbb H_n^{\mathrm{ind}}$ on these sets, their induced one-realization mixture laws have total-variation distance tending to zero, while $G_n\sigma_n^2$ converges uniformly on the respective supports to $d_{\mathrm{same}}$ and $d_{\mathrm{ind}}$ . Consequently there exists $\varepsilon>0$ such that every measurable $\widehat S_n(\mathcal O_n)$ obeys $\liminf_{n\to\infty}\sup_{Y\in\mathcal C_{\mathrm{dense}}} \Pr_Y\left(\left|\frac{\widehat S_n}{\sigma_n^2}-1\right|>\varepsilon\right) \ge\frac12.$ Thus no estimator from one realization is uniformly ratio-consistent for the exact variance over the full dense class. The deterministic support arrays, rather than a generally unavailable pair of deterministic arrays with close laws, are the valid diagonal certificate.

Citeds (2)

Cited result lem:clubsandwich-cr2-software-contract verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.ClubSandwichCR2Contract Let ${\tt fit}$ be an unweighted, full-column-rank ${\tt lm}$ fit with $N_{\rm obs}$ fitted observations, model matrix $X$ , cluster-row blocks $X_g$ , and ordinary-least-squares residual blocks $e_g$ . Suppose that $I-X_g(X^{\mathsf T}X)^{-1}X_g^{\mathsf T}$ is positive definite for every cluster. In ${\tt clubSandwich}$ version $0.7.0$ , the call ${\tt vcovCR}({\tt fit},\ {\tt cluster},\ {\tt type}={\tt 'CR2'})$ , with ${\tt target}$ , ${\tt inverse\_var}$ , and ${\tt form}$ omitted, uses the identity working target and returns $\widetilde B \sum_gX_g^{\mathsf T}A_ge_ge_g^{\mathsf T}A_g^{\mathsf T}X_g \widetilde B, \qquad \widetilde B=\frac{{\tt sandwich::bread}({\tt fit})}{N_{\rm obs}}, \qquad A_g=\left\{I-X_g(X^{\mathsf T}X)^{-1}X_g^{\mathsf T}\right\}^{-1/2},$ where the inverse square root is the symmetric positive-definite one.
Cited result lem:sandwich-lm-bread-contract verified CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.SandwichLmBreadContract Let ${\tt fit}$ be a full-column-rank, unweighted ${\tt lm}$ fit with $N_{\rm obs}$ fitted observations and model matrix $X$ . In ${\tt sandwich}$ version $3.1\text{-}3$ , ${\tt sandwich::bread}({\tt fit})=N_{\rm obs}(X^{\mathsf T}X)^{-1}.$

Auxiliary Lean lemmas (machine-checked) (202)

Definition armVar —
Definition birthdayGroupedUnits —
Definition crossCov —
Definition crossCovContrast —
Definition higherDegreeContribution —
Definition indepGroupVar —
Definition JohnsonProjections —
Definition kneserEigenvalue —
Definition Omega —
Definition orderedDisjointPairDesign —
Definition pame —
Definition QVDiagonalCertificate —
Definition sigmaSq —
Definition sliceInner —
Definition sliceNorm —
Definition worstCaseRatioError —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.a8 —
Definition JohnsonOrthogonalDecomposition —
Definition KneserAdjacencySpectrum —
Definition kneserOp —
Definition pameHat —
Definition BirthdayBenchmark —
Definition CountAlignment —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedPairSigmaEquiv —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointFiber_card —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPair_card —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPair_sum —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPair_E_eq —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.kneserChooseRatio_eq_descFactorialRatio —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceInner_sum_left —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceInner_sum_right —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceInner_const_mul_right —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceInner_self_eq_zero —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceInner_self_nonneg —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceInner_sub_self —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.kneserOp_sum —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPair_first_E_eq_slice —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPairSwap —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPair_second_E_eq_slice —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.johnson_proj_const_eq_zero —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.johnson_proj_centered_eq —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.partitionTuplePermEquiv —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPairPermEquiv —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPair_perm_exists —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.finiteDesign_ext_p —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.randomPartitionDesign_eq_compoundCore —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.finiteDesign_E_compoundCore_tower —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.finiteDesign_Var_compoundCore_tower —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.finiteDesign_Var_map —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.randomPartition_E_partition —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.expectedSampleVariance_exchangeable —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.partition_expected_sample_variance —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.pameHat_eq_diffInMeans —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.cr2Var_eq_varHat —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.conditional_E_pameHat —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.conditional_Var_pameHat —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.conditional_E_cr2Var —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.partition_E_mean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.Stau_eq_S1_sub —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.orderedDisjointPair_E_mul_comm —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.disjointCov_sub_self —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.varianceMean_exchangeable —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.partition_mean_variance —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.twoStagePairEquiv —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_armTable_eq_sampleMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_sampleMean_eq_signSum —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_armTable_mean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_armVar_treated —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_armTable_control —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_armVar_control —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_crossCov_control_right —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_crossCov_control_left —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_orderedDisjoint_signSum —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_orderedDisjoint_signSum_real —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_crossCov_treated —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sum_positive_fin_three —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.witness8_degreeOne_from_spectrum —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.matrix_sandwich_rank_one —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.posDef_rankOne_inverse_sqrt —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.birthdayGroupedUnits_ratio_identity —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.birthdayGroupedUnits_feasible —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.birthdayGroupedUnits_lower_bound —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.birthdayGroupedUnits_power_identity —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.birthdayBenchmark_proof —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sparse_dense_ratio_consistency —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armTable_abs_le_of_boundedSchedule —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceInner_self_le_sq_of_abs_le —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.johnsonProjection_energy_le_of_abs_le —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.kneserEigenvalue_abs_le_one —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.kneserEigenvalue_abs_le_ge_four —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.johnsonSpectralSum_abs_le —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.higherDegreeContribution_uniform_bound —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.scaledContrastCrossCov_decomposition —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceExpectation_abs_le_of_abs_le —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armCrossCov_abs_le_ge_four —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.tableSchedule —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armTable_tableSchedule_same —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armTable_tableSchedule_ne —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.pameHat_tableSchedule_true —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.pameHat_tableSchedule_false —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.pame_tableSchedule_true —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.pame_tableSchedule_false —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armVar_tableSchedule_same —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armVar_tableSchedule_ne —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.crossCov_tableSchedule_same —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.crossCov_tableSchedule_left_ne —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.crossCov_tableSchedule_right_ne —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean_variance_true —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean_variance_false —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.treated_tendsto_atTop —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.controls_tendsto_atTop —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.ScheduleArray.withTable —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.withTable_bounded —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sliceVar_le_sq_of_abs_le —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean_expectation_true —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean_expectation_false —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sampleVariance_finset_eq —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.realizedArmSet_card —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean_eq_realized —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectedMean_abs_le —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armSampleVar_eq_selectedMoments —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.boundedInProb_of_pointwise_bound —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.FiniteDesign.TendstoInProb.square_of_bounded —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.FiniteDesign.TendstoInProb.scale_tendsto_one_of_bounded —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armSampleVar_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.boundedInProb_deterministic_of_tendsto —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.cr2_centered_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.cr2_variance_gap_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.scaledVariance_eventually_lower —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.exists_global_abs_bound_of_eventually —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.cr2_ratio_leading_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.FiniteDesign.TendstoInProb.retarget —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.tendsto_of_deterministic_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.tendstoInProb_target_unique —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.lower_tail_vanishes_of_tendstoInProb —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radMean_E —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radMean_var —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.popVar_rademacher —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radMean_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armTable_samePrior_eq_sampleMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armTable_independentPrior_eq_sampleMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armVar_samePrior_eq_popVar —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armVar_independentPrior_eq_popVar —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.degreeOneEnergy_samePrior —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.ScheduleArray.popSize_tendsto_atTop —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radArmMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radArmMean_E —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radArmMean_var —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radArmMean_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.rademacherSliceCoefficient_tendsto —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armVar_samePrior_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.armVar_independentPrior_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.scheduleArray_same_armVar_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.scheduleArray_independent_armVar_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.scheduleArray_same_degreeOne_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.mem_johnsonHarmonic_one_of_degreeOne_mean_zero —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.johnsonMean_sampleMean_eq_sliceExpectation —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sampleMean_mem_degreeAtMost_one —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.centeredSampleMean_mem_johnsonHarmonic_one —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.johnsonProj_sampleMean_eq_centered —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.degreeOneEnergy_independentPrior_eq_popVar —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radCrossMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radPair_E —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radPair_var —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radPair_cov_ne —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radCrossMean_E —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radCrossMean_var —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.radCrossMean_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.popVar_independentDifference_eq —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.FiniteDesign.TendstoInProb.deterministic_mul —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.natCast_ratio_sub_one_tendsto —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.independentDifferencePopVar_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.scheduleArray_independent_degreeOne_tendstoInProb —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.selectSwapEquiv —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.fairCoinWeight —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.priorIndependent_E_select —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.observedArmSelector —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.observedArmSelector_of_mem —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.observe_independent_eq_same_selected —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.finiteDesign_E_swap —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.sameObservedExpectation_eq_independent —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.FiniteDesign.TendstoInProb.congr_eventually —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.probability_ge_tendsto_one_of_tendstoInProb —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.kneserEigenvalue_one —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.crossCov_eq_kneserEigenvalue_mul_armVar_of_sampleMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.crossCovContrast_eq_kneserEigenvalue_mul_degreeOne_of_sampleMean —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.scaledSigmaSq_eq_of_additive_armTables —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.FiniteDesign.TendstoInProb.exists_uniform_support —
Definition CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.ScheduleArray.withSchedule —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.abs_conditionedExpectation_sub_le_two_compl —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.denseClass_withSchedule_of_scaled_tendsto —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.tendsto_of_uniform_support_error —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.conditionedMixtureTV_le_complements —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.conditionedFiniteExpectation_nonneg —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.conditionedFiniteExpectation_le —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.conditionedFiniteExpectation_compl —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.tendsto_of_eventually_uniform_support_error —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.ratio_good_implies_same_decision —
Lemma CausalSmith.Experimentation.DenseGroupPartitionProjectionPhase.ratio_good_implies_independent_decision —

Symbol realizations (Lean @realizes) (44)

n verified realized by variable@22, ScheduleArray, witness8Bundle
M verified realized by variable@22, ScheduleArray, witness8Bundle
$\mathcal U_n$ verified realized by Population
$\Omega_{n,M}$ verified realized by Omega
$\mathcal Z$ verified realized by Arm
Y_{i,n}(z,A) verified realized by PotentialOutcome, ScheduleArray
$\mathbb E_n$ verified realized by slice
$\langle\cdot$ verified realized by sliceInner
$\cdot\rangle_n$ verified realized by sliceInner
$\|\cdot\|_n$ verified realized by sliceNormSq
h_{z,n} verified realized by armTable
$h_{z,n}^{\circ}$ verified realized by armTableCentered
V_{z,n} verified realized by armVar
G_n verified realized by ScheduleArray, witness8Bundle
G_{1n} verified realized by ScheduleArray, witness8Bundle
N_n verified realized by ScheduleArray, ScheduleArray.grouped, witness8Bundle, birthdayGroupedUnits
G_{0n} verified realized by ScheduleArray.controls
p_n verified realized by ScheduleArray.treatmentFraction, pFrac
p verified realized by StableTreatmentFraction
$\rho$ verified realized by SamplingFractionLimit
B verified realized by BoundedSchedule
$c_\sigma$ verified realized by ScaledVarianceNondegenerate
$\mathcal C_{\mathrm{dense}}$ verified realized by DenseScheduleClass
$H^{\mathrm{obs}}_{ng}$ verified realized by obsGroupMean
$\tau_n$ verified realized by pame, pameAndEstimator
$\widehat\tau_n$ verified realized by pameHat, pameAndEstimator
$\sigma_n^2$ verified realized by sigmaSq
R_n verified realized by indepGroupVar, denseCorrection
$E_{\tau,1,n}$ verified realized by degreeOneEnergy, denseCorrection
s_{z,n}^2 verified realized by armSampleVar
$\widehat V_{\mathrm{CR2},n}$ verified realized by cr2Var
$\mathcal H_{n,k}$ verified realized by johnsonHarmonicSpace
$\Pi_{n,k}$ verified realized by JohnsonProjections
$\mathsf K_n$ verified realized by kneserOp
$\lambda_{n,k}$ verified realized by kneserEigenvalue
C_{ab,n} verified realized by crossCov
$C_{\tau\tau,n}$ verified realized by crossCovContrast
$\mathbf A_n$ verified realized by PartitionTuple
$\mathbf Z_n$ verified realized by TreatmentSpace
$\mathbb H_n^{\mathrm{same}}$ verified realized by priorSame
$\mathbb H_n^{\mathrm{ind}}$ verified realized by priorIndependent
$\mathcal O_n$ verified realized by ObservedData
$\widehat S_n$ verified realized by VarianceStatistic
$\mathbf a_8$ verified realized by a8

Proof map 12 statements · 13 edges

Random Group Formation and the Equal-group CR2 Variance in Finite Populations

Abstract

Introduction

Related work

Setup and assumptions

Exact variance geometry

Dense and sparse variance behavior

Software identity and finite witness

One-realization lower bound

Discussion, scope, and extensions

Limitations and future work

Appendices

Proofs and auxiliary lemmas

Verification note.

Proofs of the main results

References