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).