Formalization: Random Group Formation and the Equal-group CR2 Variance in Finite Populations
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Basic 11 declarations This file defines the deterministic composition-indexed potential-outcome schedule, the uniform fixed-cardinality slice, and its group-level moments.
Dense random-group experiments: finite-population slice
This file defines the deterministic composition-indexed potential-outcome schedule, the uniform fixed-cardinality slice, and its group-level moments.
The labeled finite population.
Definition (Lean source)
The fixed-cardinality slice of candidate groups.
The two treatment arms.
Definition (Lean source)
A deterministic potential-outcome schedule, defined only for units belonging to the group.
The uniform design on the M-slice.
Definition (Lean source)
Uniform-slice inner product.
Definition (Lean source)
Squared uniform-slice norm.
Definition (Lean source)
Uniform-slice norm.
Definition (Lean source)
The arm-specific mean outcome of a candidate group.
Definition (Lean source)
The centered arm table.
Definition (Lean source)
The uniform-slice arm variance.
Definition (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.Asymptotics 20 declarations This file bundles each deterministic row of the experiment and defines exactly the five asymptotic/support conditions used by the paper.
Triangular arrays and the dense schedule class
This file bundles each deterministic row of the experiment and defines exactly the five asymptotic/support conditions used by the paper.
A triangular array of feasible dense random-group experiment rows.
Definition (Lean source)
Row control-group count.
Definition (Lean source)
Row grouped-unit count.
Definition (Lean source)
Row treatment fraction.
Definition (Lean source)
The row's joint finite design.
Definition (Lean source)
The row's exact PAME variance.
Definition (Lean source)
Each feasible row contains at least one whole group.
Formal statement
Proof (Lean source)
Row arm variance.
Definition (Lean source)
Row ordered-disjoint covariance.
Definition (Lean source)
Row ordered-disjoint arm-contrast covariance.
Definition (Lean source)
Row independent-group leading variance.
Definition (Lean source)
Row degree-one arm-difference energy.
Definition (Lean source)
Row scalar CR2 statistic.
Definition (Lean source)
The number of randomized groups tends to infinity.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Treatment fractions converge to an interior limit.
Definition (Lean source)
Grouped-unit fractions converge in the closed unit interval.
Definition (Lean source)
The schedule is uniformly bounded over rows, groups, members, and arms.
Definition (Lean source)
The liminf of the group-scaled exact variance has a positive uniform floor.
Definition (Lean source)
The paper's dense bounded schedule-array class.
Definition (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.Cr2Concentration 37 declarations
For the stated inputs, table schedule is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the arm table table schedule same result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the arm table table schedule ne result holds.
Formal statement
Proof (Lean source)
For the stated inputs, selected mean is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the pame hat table schedule true result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the pame hat table schedule false result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the pame table schedule true result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the pame table schedule false result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the cross cov table schedule same result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the cross cov table schedule left ne result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the cross cov table schedule right ne result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
For the stated inputs, with table is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the with table bounded result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated cardinality formula holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the bounded in prob of pointwise bound result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the square of bounded result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.Cr2Ratio 5 declarations CR2 ratio and convergence helpers
CR2 ratio and convergence helpers
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the retarget result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.DiagonalSupport 1 declarations This file turns finite-design convergence in probability into finite supports whose probability tends to one and on which the error vanishes uniformly.
High-probability diagonal supports
This file turns finite-design convergence in probability into finite supports whose probability tends to one and on which the error vanishes uniformly.
Given the stated population sizes, design objects, functions, and conditions, the exists uniform support result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.Estimator 15 declarations This file defines the estimand and estimator on the two-stage assignment space, the exact design variance, the independent-group leading term, the degree-one correction, and the equal-group scalar CR2 statistic.
PAME, exact variance, and scalar CR2 statistics
This file defines the estimand and estimator on the two-stage assignment space, the exact design variance, the independent-group leading term, the degree-one correction, and the equal-group scalar CR2 statistic.
Treated-group fraction.
Definition (Lean source)
The observed group mean under its assigned arm.
Definition (Lean source)
Finite-population PAME.
Difference in realized treated and control group means.
Definition (Lean source)
The estimand and its design-based estimator, exposed jointly as required by the paper's definition.
Definition (Lean source)
Exact design variance of the PAME estimator.
Definition (Lean source)
Independent-group leading variance.
Degree-one energy of the arm-table contrast.
Definition (Lean source)
Both deterministic quantities entering the dense variance correction.
Definition (Lean source)
The paper's degree-one energy and independent-group leading variance, constructed together from a genuine Johnson projection family.
Definition (Lean source)
The realized groups in arm z.
Definition (Lean source)
The fixed number of groups in arm z.
Definition (Lean source)
Realized mean within one treatment arm.
Definition (Lean source)
Within-arm sample variance with the paper's G_z - 1 denominator.
Definition (Lean source)
Equal-group scalar CR2 statistic.
Definition (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.ExactVariance 19 declarations Exchangeable moments for the exact two-stage variance calculation
Exchangeable moments for the exact two-stage variance calculation
Given the stated population sizes, design objects, functions, and conditions, the finite design ext p result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the disjoint cov sub self result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.Kneser 24 declarations This file gives the paper's data-only projection family, normalized disjointness operator, spectral multipliers, covariance functionals, and two cited logical gates.
Johnson components and Kneser covariance
This file gives the paper's data-only projection family, normalized disjointness operator, spectral multipliers, covariance functionals, and two cited logical gates.
The canonical degree-k Johnson harmonic space: the degree-at-most-k space orthogonal to all lower-degree inclusion monomials.
Definition (Lean source)
Genuine orthogonal Johnson projections onto the canonical harmonic degree spaces, including the centered orthogonal decomposition asserted in the paper.
Definition (Lean source)
The canonical Johnson projection family supplied by the reusable Johnson--Kneser substrate.
Definition (Lean source)
The degree-indexed component family of a slice function.
Definition (Lean source)
The unnormalized Kneser adjacency sum.
Definition (Lean source)
When two groups fit in the population, every Kneser neighborhood has the stated cardinality.
Formal statement
Proof (Lean source)
The normalized Kneser disjointness operator.
Definition (Lean source)
The normalized degree-k Kneser eigenvalue.
Definition (Lean source)
Ordered-disjoint covariance of two arm tables.
Definition (Lean source)
Ordered-disjoint covariance of the arm contrast.
Ordered pairs of disjoint slice elements.
Definition (Lean source)
A uniform design on any inhabited finite type.
Definition (Lean source)
If twice the group size does not exceed the population, then the ordered-disjoint-pair type is nonempty.
Formal statement
Proof (Lean source)
The uniform ordered-disjoint-pair design.
Definition (Lean source)
Ordered disjoint pairs are a dependent pair of a slice element and a disjoint second slice element.
Definition (Lean source)
When two groups fit in the population, the fiber of groups disjoint from a fixed group has the Kneser degree.
Formal statement
Proof (Lean source)
When two groups fit in the population, the ordered-disjoint-pair space has slice cardinality times Kneser degree.
Formal statement
Proof (Lean source)
For two slice functions, a sum over ordered disjoint pairs is the corresponding iterated slice-and-neighborhood sum.
Formal statement
Proof (Lean source)
When two groups fit in the population, ordered-pair expectation agrees with the Kneser inner-product formula.
Formal statement
Proof (Lean source)
When two groups fit in the population, the quotient of unnormalized Kneser eigenvalue magnitudes is the ratio of the corresponding falling factorials.
Formal statement
Proof (Lean source)
Yuval Filmus (2016), An Orthogonal Basis for Functions over a Slice of the Boolean Hypercube, Theorem 4.1 and Lemma 4.3, arXiv:1406.0142v2, pp. 10 and 12. The cited result supplies the orthogonal direct-sum decomposition of functions on the uniform slice and the Bose--Mesner eigenspace identification.
Definition (Lean source)
Andries E. Brouwer, Sebastian M. Cioaba, Ferdinand Ihringer, and Matt McGinnis (2018), The Smallest Eigenvalues of Hamming Graphs, Johnson Graphs and Other Distance-Regular Graphs with Classical Parameters, Proposition 3.1, arXiv:1709.09011, p. 10. It gives the unnormalized Kneser adjacency eigenvalue (-1)^k * choose (n-M-k) (M-k).
Definition (Lean source)
For a feasible slice size, the canonical projection family has the Johnson orthogonal decomposition required here.
Formal statement
Proof (Lean source)
The canonical Kneser adjacency operator has the stated harmonic spectrum.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.PartitionDesign 15 declarations Only the uniform law on ordered disjoint group tuples is new.
Uniform ordered partitions and the independent two-stage design
Only the uniform law on ordered disjoint group tuples is new. The independent combination with complete treatment randomization uses the existing dependent product design and its pushforward operation.
Ordered tuples of pairwise-disjoint groups.
Complete treatment assignments to the realized groups.
If the requested groups fit in the population, the ordered partition space is nonempty.
Formal statement
Proof (Lean source)
The uniform first-stage law.
Definition (Lean source)
The two dependent coordinate spaces: partition tuple, then treatment set.
Definition (Lean source)
For the population and group-count parameters and a stage indicator, the two-stage sample space has a finite enumeration.
Definition (Lean source)
Coordinate designs for the dependent product.
Definition (Lean source)
The two Boolean-indexed stage coordinates, repackaged as an ordinary pair.
Definition (Lean source)
Independent uniform partition and complete group-treatment randomization.
Definition (Lean source)
Relabeling population units by a permutation relabels ordered partition tuples.
Definition (Lean source)
Relabeling population units by a permutation relabels ordered disjoint pairs.
Definition (Lean source)
For two ordered disjoint pairs, one population relabeling maps the first pair to the second.
Formal statement
Proof (Lean source)
The realized group in coordinate g.
Definition (Lean source)
When the groups fit in the population, there is at least one group, and the treatment count is feasible, each group coordinate is marginally uniform on the slice.
Formal statement
Proof (Lean source)
When the groups and treatment count are feasible, two groups fit in the population, and the selected coordinates differ, the two coordinates are uniform over ordered disjoint pairs.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.QVDiagonalAssembly 4 declarations Finite-design conditioning and deterministic-array membership facts used by the one-realization impossibility argument.
Diagonal lower-bound assembly helpers
Finite-design conditioning and deterministic-array membership facts used by the one-realization impossibility argument.
Replace only the deterministic schedule in a fixed design skeleton.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.RademacherDegreeOne 18 declarations This file connects centered inclusion-linear functions in the reusable Johnson space to the paper-local uniform-slice expectation.
Degree-one slice bridges for additive schedules
This file connects centered inclusion-linear functions in the reusable Johnson space to the paper-local uniform-slice expectation.
Given the stated population sizes, design objects, functions, and conditions, the stated membership property holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated membership property holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated membership property holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
For the stated inputs, rad cross mean is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the rad pair e result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the rad pair cov ne result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the rad cross mean e result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the deterministic mul result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.RademacherMoments 20 declarations Exact slice-variance formulas and the basic product-design law of large numbers used by the Rademacher mixture separation argument.
Finite-product Rademacher moments
Exact slice-variance formulas and the basic product-design law of large numbers used by the Rademacher mixture separation argument.
For the stated inputs, rad mean is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the rad mean e result holds.
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
For the stated inputs, rad arm mean is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the rad arm mean e result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the degree one energy same prior result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.RademacherPriors 15 declarations This file realizes the common-sign and independent-arm product priors as finite product designs, embeds their signs into additive schedules, and records the one-realization observation channel.
Product Rademacher schedule priors and observation channel
This file realizes the common-sign and independent-arm product priors as finite product designs, embeds their signs into additive schedules, and records the one-realization observation channel.
Convert a fair coin to a Rademacher sign.
Definition (Lean source)
Common-arm product Rademacher prior.
Definition (Lean source)
Independent-arm product Rademacher prior.
Definition (Lean source)
Additive schedule induced by common signs.
Definition (Lean source)
Additive schedule induced by independent arm-specific signs.
Definition (Lean source)
One observed realization: partition, treatment allocation, and observed outcomes for every member of every realized group.
Definition (Lean source)
The one-realization observation channel.
Definition (Lean source)
A generic statistic of one realization.
Definition (Lean source)
For the stated inputs, select swap equiv is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the fair coin weight result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
For the stated inputs, observed arm selector is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the observed arm selector of mem result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.RademacherScaledVariance 6 declarations This file supplies the rowwise spectral identities used to assemble the two Rademacher-prior variance limits.
Exact scaled variance for additive Rademacher schedules
This file supplies the rowwise spectral identities used to assemble the two Rademacher-prior variance limits.
Given the stated population sizes, design objects, functions, and conditions, the congr eventually result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the kneser eigenvalue one result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.Software 8 declarations The declarations in this file are cited logical gates.
Versioned software contracts
The declarations in this file are cited logical gates. They expose only the
mathematical claims attributed to the pinned clubSandwich and sandwich
sources; no Lean proof of package semantics is asserted.
Algebraic semantics of an unweighted full-column-rank OLS fit with possibly unequal cluster sizes, including fitted-observation residuals and the normal equations.
Definition (Lean source)
The observable configuration and return value of a clubSandwich::vcovCR call.
The pinned version-0.7.0 default CR2 call used in the paper.
Definition (Lean source)
The observable configuration and return value of a sandwich::bread call.
The pinned version-3.1-3 unweighted bread call used in the paper.
Definition (Lean source)
The CR2 cluster meat corresponding to arbitrarily sized block matrices and residual vectors.
James E. Pustejovsky (2026), clubSandwich version 0.7.0 source package, CRAN, R/lm.R lines 47--52 and 70--72; R/S3-methods.R lines 21--33 and 63--65; R/clubSandwich.R lines 167--175, 216--225, 237--287; and R/CR-adjustments.R lines 5--7 and 22--42. The source tarball SHA-256 is f3cd9cd5840022b8d1354dce3e7e4a820edcd47411b9f95bdd200c4e040032ed. For an unweighted full-rank fit with an arbitrary fitted-observation count and arbitrarily sized cluster-row blocks, identity working target, and positive-definite cluster leverage complements, the returned CR2 matrix is the stated sandwich.
Definition (Lean source)
Achim Zeileis and Thomas Lumley (2026), sandwich version 3.1-3 source package, CRAN, R/bread.R lines 10--15. The source tarball SHA-256 is 960006cf4fcbada936b43acd04ddd8c0d1255570f41dda046ce778873f546134. For a full-column-rank unweighted lm fit with arbitrarily sized cluster-row blocks, bread is the fitted-observation count times the inverse Gram matrix.
Definition (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.Helpers.Witness 4 declarations This file defines the balanced four-plus/four-minus vector and its composition schedule for the paper's finite exact-moment witness.
Balanced eight-unit witness
This file defines the balanced four-plus/four-minus vector and its composition schedule for the paper's finite exact-moment witness.
The balanced eight-unit sign vector.
Definition (Lean source)
A bundled witness whose type fixes the paper's population, group size, group count, treated count, and grouped-unit count.
Definition (Lean source)
The bundled balanced n = N = 8, M = 2, G = 4, G1 = 2 witness.
The schedule component of the bundled eight-unit witness.
Definition (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TClubsandwichConsumer 4 declarations The deterministic equal-group identity is conditional on the two versioned software contracts and on the explicit intercept-plus-binary-treatment fit data.
clubSandwich CR2 consumer identity
The deterministic equal-group identity is conditional on the two versioned software contracts and on the explicit intercept-plus-binary-treatment fit data.
The algebraic data fixed by an unweighted equal-group intercept-plus-binary- treatment OLS fit.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the matrix sandwich rank one result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the pos def rank one inverse sqrt result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TCr2PhaseFrontier 1 declarations CR2 dense-regime phase frontier
CR2 dense-regime phase frontier
Given the stated population sizes, design objects, functions, and conditions, the cr2 phase frontier result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TDenseProjectionLimit 12 declarations The deterministic group-scaled variance expansion is stated for bounded schedule arrays without a scaled-variance nondegeneracy premise.
Dense projection expansion
The deterministic group-scaled variance expansion is stated for bounded schedule arrays without a scaled-variance nondegeneracy premise.
The pooled Johnson degrees at least two, at the group-count scale.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the higher degree contribution uniform bound result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the scaled contrast cross cov decomposition result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the dense projection limit result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TEightUnitWitness 14 declarations Exact moments of the eight-unit witness
Exact moments of the eight-unit witness
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
the witness8 arm table mean result holds.
Proof (Lean source)
the stated variance result holds.
Proof (Lean source)
the witness8 arm table control result holds.
the stated variance result holds.
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the witness8 cross cov control right result holds.
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the witness8 cross cov control left result holds.
Proof (Lean source)
the witness8 ordered disjoint sign sum result holds.
Formal statement
Proof (Lean source)
the witness8 ordered disjoint sign sum real result holds.
Formal statement
Proof (Lean source)
the witness8 cross cov treated result holds.
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated nonnegativity result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the witness8 degree one from spectrum result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the eight unit witness moments result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TExactKneserIdentity 13 declarations The paper's exact identity is stated conditionally on the two cited Johnson/Kneser logical gates.
Exact Kneser spectral identity
The paper's exact identity is stated conditionally on the two cited Johnson/Kneser logical gates. Stage 3 supplies the Lean proof of the conditional result.
Given the stated population sizes, design objects, functions, and conditions, the slice inner sum left result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the slice inner sum right result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the slice inner const mul right result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated nonnegativity result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the slice inner sub self result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the kneser op sum result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
For the stated inputs, ordered disjoint pair swap is defined by the formula below.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TExactPameVariance 1 declarations Exact PAME variance and CR2 expectation
Exact PAME variance and CR2 expectation
Given the stated population sizes, design objects, functions, and conditions, the stated variance result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TQvDiagonalImpossibility 13 declarations The lower bound is encoded in witness form: explicit high-prior-probability finite supports, conditioned-mixture separation, uniform support-wise variance limits, and a worst-case risk bound for every one-realization sta
One-realization diagonal impossibility
The lower bound is encoded in witness form: explicit high-prior-probability finite supports, conditioned-mixture separation, uniform support-wise variance limits, and a worst-case risk bound for every one-realization statistic.
Conditioned common-sign expectation, written as a finite weighted ratio.
Definition (Lean source)
Conditioned independent-arm expectation, written as a finite weighted ratio.
Definition (Lean source)
Total variation of the two conditioned finite mixtures, in its bounded-test form.
Definition (Lean source)
The support-wise diagonal certificate used by the fuzzy-hypothesis argument.
Definition (Lean source)
Worst-case rowwise relative-error probability over the dense class with the fixed design skeleton A.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the indicated sequence converges to its stated limit.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the ratio good implies same decision result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the ratio good implies independent decision result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated bound holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the qv diagonal impossibility result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TRademacherMixtureSeparation 6 declarations The two product priors induce the same one-realization observation law while their group-scaled exact variances separate at positive sampling density.
Rademacher mixture separation
The two product priors induce the same one-realization observation law while their group-scaled exact variances separate at positive sampling density.
Expected value of a statistic of observed data under the common-sign mixture.
Definition (Lean source)
Expected value of a statistic of observed data under the independent-arm mixture.
Definition (Lean source)
Group-scaled exact variance under a common-sign schedule draw.
Definition (Lean source)
Group-scaled exact variance under an independent-arm schedule draw.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated expectation identity holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the rademacher mixture separation result holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_DenseGroupPartitionProjectionPhase_Research.TSparseBeyondBirthday 11 declarations Sparse consistency beyond the birthday scale
Sparse consistency beyond the birthday scale
The benchmark group count floor (n^(3/4) / M).
Definition (Lean source)
The corresponding grouped-unit count.
Definition (Lean source)
The three unconditional arithmetic facts of the birthday-scale benchmark.
Definition (Lean source)
An array's grouped-unit counts agree row-by-row with the birthday benchmark.
Definition (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the birthday grouped units feasible result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the birthday grouped units lower bound result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the stated equality holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the birthday benchmark proof result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the sparse dense ratio consistency result holds.
Formal statement
Proof (Lean source)
Given the stated population sizes, design objects, functions, and conditions, the sparse beyond birthday result holds.