Formalization: Exact Randomized Designs for Two-Block Interference Experiments

Range lemma for ρ_⋆. The rounding-loss certificate lands in its core-declared space [0,∞): 0 ≤ ρ_⋆(m,a,b,r,κ). This holds because the implementable reduced value (the constrained sInf over T_m ∩ {y+z ≥ d_m}) dominates the relaxed reduced value (the unconstrained sInf over the larger set T_m), the implementable feasible set being a subset of the relaxed one. Together with the roundingLossCertificate carrier def above, this lemma IS the realization of the symbol's standing range condition (the bare sInf − sInf real difference does not by itself guarantee nonnegativity). @realizes rho_star(m,a,b,r,kappa)(range [0,∞) pinned via {y+z ≥ d_m}-constrained inf ≥ unconstrained inf ⇒ implementable reduced value ≥ relaxed reduced value)

Sum a two-valued function over a finite set when one distinguished point takes the diagonal value.

Pair count over the two equal blocks: diagonal pairs contribute d, same-community off-diagonal pairs contribute s, and cross-community pairs contribute c.

The same pair count with a community-sign multiplier. Same-community pairs have sign product +1, and cross-community pairs have sign product -1.

Along the tangent (x,y,z) = (1+t, 1-q t, 1), the Frobenius term has zero first derivative at the center, so the objective derivative is c_x - q c_y.

Along the tangent (x,y,z) = (1, 1+t, 1-t), the Frobenius term has zero first derivative at the center, so the objective derivative is c_y - c_z.

Frobenius-center certificate: (1,1,1) uniquely minimizes the weighted Frobenius term on T_m; it minimizes the full objective for finite κ only if c_x/q = c_y = c_z, and under that equality with κ > 0 it is the unique minimizer.

The implementability gap equals the reduced-coordinate implementable-minus-relaxed value: Δ_m^±(r,κ) = implementableReducedValue − relaxedReducedValue.

Range lemma for Δ_m^±. The implementability gap lands in its core-declared space [0,∞): 0 ≤ Δ_m^±(r,κ). The reduction lemma identifies it with the reduced constrained-minus-unconstrained value, whose nonnegativity is proved by roundingLossCertificate_nonneg. @realizes Delta_m^pm(r,kappa)(range [0,∞) pinned via the reduced constrained-minus-unconstrained identity)

If the relaxed reduced objective has a unique minimizer outside the implementable parity slice, and the implementable reduced problem is attained, then the implementability gap is strictly positive.

If a reduced triangle point globally minimizes the relaxed reduced objective, then the sInf defining relaxedReducedValue is its objective value.

If a reduced triangle point globally minimizes the parity-truncated reduced objective, then the sInf defining implementableReducedValue is its objective value.

The relaxed reduced problem attains its minimum: some point of the reduced triangle minimizes the reduced objective over the whole triangle. This is the existence statement behind the relaxed value being a genuine minimum rather than only an infimum; it is proved by transporting the triangle to the weighted simplex, where the linear-plus-weighted-norm objective has an explicit minimizer (an active-set point when the robustness weight is positive, an exposed-face vertex when it is zero).

The implementable reduced problem attains its minimum: some point of the reduced triangle satisfies the parity constraint and minimizes the reduced objective over all triangle points that satisfy it. This is the parity-truncated counterpart of exists_relaxed_reduced_minimizer, and it is what makes the implementability gap a difference of two attained minima.

The implementability gap is never negative: restricting a design to be realizable by an actual ±1 assignment law can only raise the achievable objective value. Formally, both reduced problems attain their minima and the implementable problem optimizes over a subset of the relaxed feasible set, so its minimum dominates. This is the range condition for Δ_m^± promised in the definition of implementabilityGap.

Zero implementability gap is equivalent to the relaxed argmin set meeting the implementable parity slice.

In the unique-relaxed-minimizer case (in particular the κ > 0 active-set case), zero gap is equivalent to that unique minimizer lying in the parity slice.

Unique-minimizer form matching the sharp_rho_star clause: with a unique relaxed minimizer, zero gap is equivalent to every relaxed minimizer lying in the parity slice.

At κ = 0, if the exposed relaxed min-face is disjoint from the implementable slice, then the implementability gap is strictly positive.

The ±1 covariance image of the block-exchangeable class in spectral coordinates is exactly the reduced triangle truncated by the parity threshold d_m (0 for even m, 2/m for odd m). In particular, for odd m the spread vertex (m/(m−1), 0, 0) is not implementable, while for even m the whole slice is.

For even m, the whole block elliptope slice is implementable.

For odd m ≥ 2, the spread covariance is not ±1 implementable.

Backward direction, even m: the barycentric 3-vertex mixture.

Backward (sufficiency) direction. Any parity-truncated reduced-triangle point is realized by a block-exchangeable ±1 design.

Each ±1 sign squares to 1.

|A_m| = m.

|B_m| = m.

The design second-moment entries read off from X(u,v): the (i,j) entry is 1 on the diagonal, u within a block, v across blocks.

E[S_A²] = m + m(m−1) u (and identically E[S_B²]).

E[S_B²] = m + m(m−1) u: whenever a design's assignment second moment is the block-symmetric matrix X(u,v), the mean square of the community-B sign sum depends only on the common within-block correlation u (not on the across-block entry v), and equals the corresponding community-A quantity. The two blocks have the same size m, so this is the mirror image of E_sumAr_sq.

E[S_A S_B] = m² v.

The within-block second moment u ≤ 1 (from E[(Z_i − Z_j)²] ≥ 0 for a within-block pair, available since m ≥ 2).

For odd m, the integer block sum S_A is odd for every assignment.

For odd m, E[S_A²] ≥ 1.

For odd m, E[S_B²] ≥ 1 under every design. Community B has an odd number m of units, so its sign sum is an odd integer for every assignment and therefore has square at least one; averaging preserves the bound. This is the parity obstruction that keeps the odd-m reduced slice away from the spread vertex.

Forward (necessity) direction. A design realizing X(u,v) has reduced spectral coordinates in the parity-truncated triangle.

Change of variables: for a design invariant under the block-automorphism σ (D.p (reindexBy σ z) = D.p z), expectation is invariant under precomposition by reindexBy σ.

The pointwise sign transports under reindexing: signOf (R σ z) i = signOf z (σ i).

Pair-expectation transport: if D is invariant under the block-automorphism σ then E[Z_{σ i} Z_{σ j}] = E[Z_i Z_j].

A within-block transposition (swap two indices of block A, fixing everything else) is a two-block automorphism.

The block-symmetry general lemma. For a block-exchangeable design D, its second moment is block-symmetric: it equals X(u,v) with u = E[Z_{i₀} Z_{j₀}] the within-block reference-pair value and v = E[Z_{i₀} Z_{k₀}] the cross-block reference-pair value.

If the support S is invariant under global negation and under reindexing by every two-block automorphism, the uniform design lies in the block-exchangeable class.

Expectation of a mixture is the convex combination of expectations.

A mixture of block-exchangeable designs is block-exchangeable.

Averaging block-symmetric matrices with weights summing to 1.

The second moment of a mixture whose components have block-symmetric second moments X(uᵢ,vᵢ) is X(∑ wᵢ uᵢ, ∑ wᵢ vᵢ).

For odd m some assignment has community sign sums (1, −1), so the pcut parity support is nonempty and the uniform law on it is well defined. When m is odd each community sum is an odd integer, so (±1, ∓1) is the closest an oppositely-signed pair of communities can come to being balanced.

For odd m some assignment has community sign sums (1, 1), so the pall parity support is nonempty and the uniform law on it is well defined. This is the companion of pcutSupport_nonempty for the equally-signed parity vertex.

For odd m, the pcut parity design — uniform over the assignments whose community sign sums are (1, −1) or (−1, 1) — belongs to the block-exchangeable design class. Negating an assignment swaps the two cases, and a two-block automorphism either fixes the pair of community sums or transposes it, so the support is invariant either way.

For odd m, the pall parity design — uniform over the assignments whose community sign sums are (1, 1) or (−1, −1) — belongs to the block-exchangeable design class, by the same negation and two-block-automorphism invariance of its support.

On pcutSupport, S_A² = 1, so E[S_A²] = 1.

On pcutSupport, S_A S_B = -1.

Under the pall parity design the community-A sign sum has mean square 1, because every assignment in its support has that sum equal to +1 or −1.

Under the pall parity design the two community sign sums have cross moment +1: they always carry the same sign, both +1 or both −1. This is the sign flip of the corresponding pcut value and is what separates the two parity vertices.

For odd m ≥ 2 the pcut parity design has assignment second moment X(−1/m, −1/m²): units in the same community carry correlation −1/m, units in opposite communities −1/m². Its reduced spectral coordinates are y = 2/m, z = 0, so it sits exactly on the parity threshold y + z = 2/m — one of the two extra vertices that odd community size creates.

For odd m ≥ 2 the pall parity design has assignment second moment X(−1/m, 1/m²): units in the same community carry correlation −1/m, units in opposite communities +1/m². Its reduced spectral coordinates are y = 0, z = 2/m, the second parity vertex, again sitting exactly on the threshold y + z = 2/m.

Backward direction, odd m: the 4-vertex quadrilateral mixture.

Negating an assignment negates each community sum.

Negating an assignment negates the community-B sign sum, the mirror of blockSumA_neg. Together the two make every sign-symmetric support closed under global negation, which is what the balanced-design membership proofs need.

Under a block-automorphism σ, the pair of community sums of reindexBy σ z is either (S_A, S_B) (block-preserving) or (S_B, S_A) (block-swapping).

Expectation under the uniform law on a two-element support {z₁, z₂}.

The cut vertex design — a fair coin between "treat community A, control community B" and its reverse — belongs to the block-exchangeable design class: its two-point support is closed under global sign flip and under every two-block automorphism (relabelling units inside a community fixes each of the two assignments, swapping the communities exchanges them).

The all-ones vertex design — a fair coin between "treat everyone" and "control everyone" — belongs to the block-exchangeable design class: its two-point support is closed under global sign flip, and both constant assignments are fixed by every permutation of the units, hence by every two-block automorphism.

The cut vertex design has assignment second moment X(1,−1): two units in the same community always receive the same sign, and two units in opposite communities always receive opposite signs. In the reduced spectral coordinates this is the triangle vertex (0, 2m, 0).

The all-ones vertex design has assignment second moment X(1,1): every pair of units always receives the same sign, whether or not they share a community. In the reduced spectral coordinates this is the triangle vertex (0, 0, 2m).

For even m, the explicit half-and-half assignment (treat the first half of each community, control the second half) really is balanced in each block: both community sign sums are zero.

For even m at least one assignment has both community sign sums equal to zero, so the balanced-in-each-block support is nonempty and the uniform law on it is well defined. Evenness is essential: for odd m each community sum is an odd integer and this support is empty.

For even m, the spread vertex design — uniform over the assignments that are exactly balanced inside each community — belongs to the block-exchangeable design class. Negating an assignment and relabelling units by a two-block automorphism both leave the pair of community sign sums at (0,0), so the support is invariant.

On the spread support the real community sums vanish, so E[S_A²]=E[S_A S_B]=0.

Under the spread vertex design the two community sign sums have zero cross moment, since every assignment in its support has both sums equal to zero pointwise. With the companion spreadVDesign_sumAr_zero this pins the design's reduced coordinates.

For even m ≥ 2 the spread vertex design has assignment second moment X(−1/(m−1), 0): units in different communities are uncorrelated, and units in the same community carry the small negative correlation −1/(m−1) forced by the community sign sum being identically zero. These are the reduced coordinates (2m/q, 0, 0) — the spread vertex of the triangle — so for even m the spread covariance is implementable.

The change of variables t = (q x, y, z) sends the reduced triangle to Δ_{2m}.

The inverse change of variables x = t_x/q, y = t_y, z = t_z.

Under t = (q x, y, z), the reduced objective is the weighted-simplex objective with α = (c_x/q, c_y, c_z) and β = (1/q, 1, 1).

The inverse form of reducedObjective_eq_wsObj, for a simplex point t.

The reduced Frobenius square at X(u,v) is the identity square plus the two off-diagonal block contributions.

Any choice of relaxed minimizers converges entrywise to the identity as κ → ∞.

Under the uniform iid sign law, the raw sum of two distinct coordinate signs is zero.

The iid Rademacher design has identity second-moment matrix.

The identity covariance is the block-symmetric center (u,v)=(0,0), hence lies in E_m^blk under two-block homophily.

The center first-order equality c_x/q = c_y forces r = 2b(a+b).

The two center coefficient equalities are equivalent to the affine-balanced locus.

On the affine-balanced locus, the reduced linear coefficients are all equal.

Inverse map from reduced coordinates to block-symmetric (u,v) coordinates.

The matrix objective at I_n is the reduced objective at (1,1,1).

If I_n minimizes the matrix objective on the block elliptope, the reduced center first-order coefficient equalities hold.

On the affine-balanced locus and for κ>0, I_n is the strict relaxed minimizer over the block elliptope.