Formalization: Minimax Precision for Total Treatment Effects with Partially Observed Interference Networks
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_ThinnedgraphAdditiveRiskFrontier_Research.Basic 59 declarations Raw directed coefficients are needed for the schedule class and the hidden-allocation prior.
Fixed additive schedules and the complete thinned record
Raw directed coefficients are needed for the schedule class and the hidden-allocation prior. The exposure-based potential-outcome substrate and superpopulation PO systems are therefore bypassed. The out-degree predicate and extended minimax carrier reuse Causalean directly. The design is Measure-valued to permit continuous baseline mixtures and an independent seed; the finite Bernoulli design is used through the expectation bridge in Helpers/DesignBridge.
The paper population has n units; the paper label of i is i.val + 1.
Definition (Lean source)
A fixed simple directed off-diagonal graph with additive coefficients.
Definition (Lean source)
The off-diagonal treatment sources of a recipient.
Definition (Lean source)
The zero-one numeric value of a treatment coordinate.
Definition (Lean source)
The centered sign, twice treatment minus one.
Definition (Lean source)
The additive potential outcome.
The all-treated minus all-control population average.
Definition (Lean source)
Each recipient has at most d off-diagonal sources.
Definition (Lean source)
The row coefficient mass includes the baseline and own coordinate.
Definition (Lean source)
The additive fixed-schedule model class.
Definition (Lean source)
The imported predicate is the sole realization of the off-diagonal out-degree atom.
Enlarging the degree bound preserves schedule membership. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coefficient-mass envelope bounds every potential outcome by one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coefficient-mass envelope bounds the total treatment effect by one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Ordered off-diagonal source-recipient labels.
Definition (Lean source)
Complete treatment assignment.
Definition (Lean source)
Latent independent audit marks, including marks on nonedges.
The full graph, treatment, and noiseless outcome record.
A two-atom Bernoulli measure, total also outside the probability regime.
Independent half-Bernoulli assignments.
Independent edge audit with retention q; endpoints are point masses.
The canonical independent assignment-audit product design.
Probability-design scope for the extended minimax risk.
Definition (Lean source)
The finite Bernoulli marginal is a probability measure at admissible retention. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Admissible retention makes the canonical experiment a probability design. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The assignment marginal is the product half-Bernoulli law.
Definition (Lean source)
The audit marginal is the independent product law with admissible retention.
Assignment and audit coordinates are independent.
The original record retains precisely the audited true arrows.
Definition (Lean source)
An independent uniform seed on the unit interval.
The fixed-schedule seeded original-record law.
All measurable real-valued randomized estimators of the complete record.
Definition (Lean source)
Extended nonnegative squared loss avoids nonintegrable-real-integral junk values.
Worst-case risk over the fixed schedule class.
Definition (Lean source)
The unrestricted minimax risk, built on the substrate extended minimax value.
Definition (Lean source)
The complete original record together with the true off-diagonal graph.
All measurable randomized estimators when the true graph is supplied.
Definition (Lean source)
The true off-diagonal graph as a labeled Boolean array.
The original record and the supplied true graph under one design realization.
Definition (Lean source)
The fixed-schedule law of the supplied-graph record and an independent seed.
Definition (Lean source)
Extended squared risk of an estimator that observes the true graph.
Definition (Lean source)
Worst-case supplied-graph risk over the unchanged fixed schedule class.
Definition (Lean source)
Minimax squared risk when the complete original record and true graph are supplied.
Definition (Lean source)
The zero estimator bounds minimax risk by one on any probability design. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The paper's supplied-graph minimax risk at admissible population, degree and retention.
Definition (Lean source)
Canonical-design minimax risk.
Definition (Lean source)
The recorded sources of a recipient, read solely from the observed record.
The observable inverse-edge-inclusion additive score.
Definition (Lean source)
The finite observed graph and assignments give measurable score weights, with the outcome coordinates entering by a finite linear combination.
Formal statement
Proof (Lean source)
The additive supplied-graph score.
Definition (Lean source)
The risk envelope is infinite at zero retention.
Definition (Lean source)
The total clipped-or-zero observable rule.
Definition (Lean source)
The clipped-or-zero rule is measurable on the entire record space.
Formal statement
Proof (Lean source)
Ignoring the independent seed preserves measurability of the upper rule.
Formal statement
Proof (Lean source)
The measurable seeded representative of the total upper rule.
Definition (Lean source)
The explicit positive finite precision scale on the admissible regime.
Definition (Lean source)
The attaining observable rule is the clipped-or-zero rule.
The seeded measurable representative of the attaining frontier rule.
Definition (Lean source)
Names the scale-rule pair without inserting any proved risk properties.
Definition (Lean source)
Admissible degree and retention sequences, with only the n ≥ 4 tail constrained.
Definition (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ActiveCapacityBridge 3 declarations An exact reindexing removes the unused slots outside a response support before applying the active-slot contraction bound.
Masking inactive capacities in the actual conditional coefficient
An exact reindexing removes the unused slots outside a response support before applying the active-slot contraction bound.
Only rows belonging to the response support retain hidden slots.
Inactive rows have zero hidden degree in every compatible allocation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Masking inactive capacities preserves the full labeled support coefficient: its allocations, total degrees, binomial weights and response factors agree. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ActiveLabelEnergyBound 6 declarations Sum the masked allocation bound over disjoint hidden-only response supports, then retain the actual revealed-label indexing and remove its constant term.
Active-support bound for the original labeled coefficient energy
Sum the masked allocation bound over disjoint hidden-only response supports, then retain the actual revealed-label indexing and remove its constant term.
The rowwise energy envelope for one exact revealed-label degree vector.
Definition (Lean source)
The full hidden-degree energy for a fixed revealed subset is bounded by its disjoint active-support envelope, using the original total hidden capacity. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The single removed coefficient has unit reference energy. This identifies its contribution before the full labeled sum is bounded. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restoring exactly the constant coefficient gives the complete original-label energy sum, with all hidden-degree denominators unchanged. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Sum the active-support envelope over the actual labeled revealed subsets.
Definition (Lean source)
On the good event the exact nonconstant labeled energy is bounded by the summed disjoint-support envelope after subtracting its one constant coefficient. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ActiveRowAverage 5 declarations The revealed and hidden active row sets are counted with their labels intact.
Averaging and counting disjoint active rows
The revealed and hidden active row sets are counted with their labels intact. Their independent reveal-energy averages feed the finite contraction series.
Counting subsets of the remaining labeled rows gives a binomial sum, extended by zero to the full row range. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Ordered disjoint active row sets of sizes a and b have exactly the two binomial factors used by the contraction series. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A good-event indicator can be dropped from each nonnegative disjoint active row contribution before averaging independent source reveals. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing labeled disjoint row contributions, omitting the constant term, and then averaging gives exactly the finite binomial contraction bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The averaged nonconstant active-row energy, with any good-event indicator, is bounded by the exponential/geometric expression of the contraction roadmap. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ActiveSupportBridge 5 declarations Compatible response supports are reindexed by their hidden-only active rows.
Disjoint active rows of the actual conditional likelihood
Compatible response supports are reindexed by their hidden-only active rows. The masked allocation coefficient then satisfies the existing good-event energy bound with the exact number of hidden-only rows.
A response support containing the revealed-active rows is uniquely their union with a subset of the complementary labeled rows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual coefficient's squared norm splits over disjoint hidden-only active rows, with incompatible supports contributing zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A masked support uses no more than all hidden slots and no more than degree times the number of its active rows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each compatible actual support satisfies the all-hidden-degrees energy bound after masking inactive capacities, with no independence of hidden rows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ActualLabelSupportEnergy 9 declarations The capacity-constrained coefficient is partitioned by its actual positive-degree response rows.
Active response supports of the actual labeled coefficients
The capacity-constrained coefficient is partitioned by its actual positive-degree response rows. Orthogonality gives an exact decomposition of its energy without assuming orthogonality between different positive degrees within a row.
The positive response rows of a revealed and hidden degree vector.
Restrict the exact bounded allocation coefficient to one response support.
Definition (Lean source)
Every bounded allocation belongs to precisely one actual response support. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Distinct actual response supports contribute additive squared norms. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual enumerated-label coefficient has the same support decomposition, with every original row capacity and labeled revealed count retained. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A coefficient fiber's support condition is exactly a rowwise restriction: revealed-active rows allow every hidden degree, hidden-only active rows require a positive degree, and all remaining rows require degree zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each support-group coefficient is the exact rowwise-restricted allocation sum needed by the allocation-energy bound, with no new statistical premise. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A response support omitting any revealed-active row has no compatible allocation; every compatible support gives the exact rowwise coefficient. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact nonconstant energy of the actual posterior splits by response support before any Cauchy–Schwarz bound is applied. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ActualLabelWalshBridge 19 declarations The original assignment coordinates indexed by revealed and hidden source labels have their exact product law.
Transport of the actual labeled likelihood to independent signs
The original assignment coordinates indexed by revealed and hidden source labels have their exact product law. Ancillary coordinates are integrated out by a measure-preserving projection, rather than replacing hidden row assignments.
An injective selection of actual assignment labels retains independent fair signs. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two disjoint injective label selections have the exact independent sign law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Enumerate every actually revealed source label once.
Definition (Lean source)
The signs occurring in the actual posterior likelihood have the product law used in the hidden/revealed energy identity. The full assignment is the source. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Transport the nonconstant energy identity back to the original assignment, including all unused recipient and padding coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The revealed enumeration covers exactly the observed union of row labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact zero-hidden-degree coefficient contains only the zero row vector. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On positive reference support the actual constant posterior coefficient is one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Actual response coefficients indexed by enumerated revealed subsets and total hidden degree. The coefficients themselves keep all row capacities.
Definition (Lean source)
Injective label maps carry the full subset family to the image subset family. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The original-label likelihood is exactly the finite expansion indexed by the independent sign projection, wherever the reference density is positive. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At each positive reference response the actual assignment norm of the centered likelihood is exactly its nonconstant coefficient energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The independent reference responses almost surely lie in positive row support. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact posterior coefficient cross products are integrable under the actual row reference; no new regularity premise is needed. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the actual original-label likelihood norm over the reference responses gives precisely the nonconstant coefficient norms used in contraction. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Original-assignment energy of the posterior density ratio under the response reference.
Definition (Lean source)
Exact nonconstant posterior coefficient energy, retaining every hidden-degree weight.
Definition (Lean source)
The actual density energy is exactly the label coefficient energy on every compatible detailed graph. This is the bridge consumed by contraction. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.AuditVariance 9 declarations Independent audit noise and conditional second moments
Independent audit noise and conditional second moments
A numeric Bernoulli mark has variance q(1-q). For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent centered audit marks have a diagonal weighted variance. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
An off-diagonal label sum can be organized by recipient and source. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The recorded-neighbor sum is the true-edge sum multiplied by numeric marks. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The audit error is a weighted sum of independent centered true-edge marks. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Squared noise weights sum to the in-degree weighted squared outcomes. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional audit variance follows from the diagonal centered-mark calculation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the conditional variance adds the oracle squared conditional mean. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full assignment-audit variance is the oracle variance plus the expected audit variance. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BaselineTranslationAffinity 19 declarations Translation affinity and common-marginal averaging
Translation affinity and common-marginal averaging
The unhalved squared Hellinger energy of two real densities against a common reference measure.
Definition (Lean source)
The joint mixing-coordinate and response law for a common marginal and conditional density.
Definition (Lean source)
The response mixture after integrating out the common mixing coordinate.
Definition (Lean source)
A measurable nonnegative density defining a probability law is integrable and has integral one; these side conditions are consequences of normalization. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cauchy–Schwarz bounds total variation by the square root of the unhalved Hellinger energy of two probability densities. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The baseline density is nonnegative. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The compactly supported cosine density is integrable and normalized. the stated conclusion holds.
Formal statement
Proof (Lean source)
Translation preserves integrability and normalization of the baseline density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Tensorized affinity and the product-defect bound give subadditivity of squared Hellinger energy for normalized nonnegative coordinate densities. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Joint measurability of the conditional densities gives a measurable family of joint fibers.
Formal statement
Proof (Lean source)
The conditional-density joint law is the density-weighted product reference law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Normalized conditional fibers give a probability joint law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sum-reference Hellinger definition agrees with a sigma-finite density reference. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Marginalizing the joint law recovers its response mixture. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging conditional Hellinger energy over the actual common marginal gives joint Hellinger energy and bounds the response-mixture total variation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The pointwise derivative of the square-root baseline away from its two support boundaries, with the arbitrary boundary values fixed to zero.
Away from the two support boundaries, the square-root baseline has the explicit supported sine derivative. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicitly tied square-root derivative has total squared energy four pi squared. the stated conclusion holds.
Formal statement
Proof (Lean source)
Lipschitz and derivative energy, translation and product bounds, and common-marginal Hellinger averaging. the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BaselineTranslationEnergy 10 declarations The compactly supported cosine square root has a supported sine derivative.
Square-root baseline derivative and translation energy
The compactly supported cosine square root has a supported sine derivative. Its integral representation, interval Cauchy–Schwarz, and Fubini yield the sharp quadratic translation bound used by the block-testing construction.
Clamping to the support interval expresses the square-root density as a cosine, including its zero endpoint values. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The square-root baseline is globally four-pi Lipschitz, including across the boundary of its compact support. the stated conclusion holds.
Formal statement
Proof (Lean source)
Direct integration of the squared interior derivative gives four pi squared. the stated conclusion holds.
Formal statement
Proof (Lean source)
Cauchy–Schwarz on a finite measure bounds the squared integral by mass times energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the interval Cauchy–Schwarz bound and applying Fubini controls translation energy by derivative energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The supported interior derivative of the square-root cosine baseline; endpoint values are immaterial to integration.
The supported derivative and its square are integrable by compact support. the stated conclusion holds.
Formal statement
Proof (Lean source)
The supported derivative has total squared energy four pi squared. the stated conclusion holds.
Formal statement
Proof (Lean source)
Integration of the supported derivative recovers square-root baseline increments, including across the support boundaries. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The square-root baseline translation energy is bounded by four pi squared times the squared shift difference. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BaselineTransport 1 declarations Transport of the block baseline under translation
Transport of the block baseline under translation
Translation of a baseline law has exactly the translated cosine density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BlockLaw 1 declarations The fixed-partition density and compatible-completion count recover the full record with every retained edge and assignment coordinate.
Complete original-record block likelihood assembly
The fixed-partition density and compatible-completion count recover the full record with every retained edge and assignment coordinate.
Support, target, independent source reveals, and the complete-record likelihood reconstruction. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BlockLawBasics 9 declarations Complete original-record block likelihood
Complete original-record block likelihood
A normalized baseline remains a probability law after taking independent blocks. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Mapping a measurable channel commutes with mixing its input laws. For the stated data and conditions, the stated conclusion holds.
Proof (Lean source)
A jointly measurable recording function yields a measurable family of output laws.
Formal statement
Proof (Lean source)
The complete block record depends measurably on its prior parameters and design draw.
Formal statement
Proof (Lean source)
Mixing independent baselines preserves the detailed retained graph and the entire assignment marginal, for either sign and every amplitude. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every finite product of weighted translated baseline densities is integrable, and its integral is the product of the weights. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The constrained density integrates to one on every valid retained graph, since its finite allocation weights are normalized; no posterior-law identification is assumed. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a valid retained graph, the displayed conditional density defines a probability law of the distinct responses, including the zero-hidden-capacity endpoint. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BlockPrior 20 declarations Hidden-allocation fixed-schedule prior
Hidden-allocation fixed-schedule prior
The compactly supported cos-squared baseline density.
Ordered partitions represented by a label for each source with exactly d sources per label.
Uniform finite measure; zero when the finite carrier is empty.
Definition (Lean source)
The recipient block in the second half of the bipartite layout.
Independent baseline levels.
Definition (Lean source)
Partition and baselines are drawn independently before assignment.
Definition (Lean source)
The labeled source-to-recipient block graph, with no diagonal arrows.
Definition (Lean source)
The source-to-recipient block graph has no diagonal arrows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The amplitude domain of the auxiliary block family.
Definition (Lean source)
The fixed schedule map. Source and padding rows are zero; each recipient has its block baseline.
Definition (Lean source)
The prior is its parameter law paired with the concrete fixed-schedule map.
Definition (Lean source)
Apply the complete-record channel after drawing a fixed schedule from the parameter prior.
Mixture law of the entire original record, without removing any coordinates.
Definition (Lean source)
The complete-record block mixture under the canonical assignment-audit product design.
Definition (Lean source)
Probability that at least one of a source's d arrows is retained.
Definition (Lean source)
Admissible audit probability for the source-association retention formula.
Definition (Lean source)
Source-association retention lies in the probability interval. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The nonlocal testing scale is clipped at one and equals one when no association is retained.
Definition (Lean source)
One hundred pi inverse times the nonlocal testing scale.
Definition (Lean source)
Names both constructed priors and their complete original-record mixture laws.
Definition (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BlockReveal 8 declarations Independent revealed source associations
Independent revealed source associations
Selecting distinct coordinates of independent Bernoulli marks preserves their product law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Regroup a rectangular collection of independent marks into independent rows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The OR of d independent audit marks has success probability one minus their joint failure. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a fixed source partition, its true audit marks can be enumerated in disjoint rows; the full retained graph reveals a source exactly when one mark in its row is true. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional on any true partition, the vector of labeled source reveals has the same independent Bernoulli law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A rectangular enumeration provides an ordered source partition for every block layout. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The uniform prior on ordered source partitions has total mass one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Source associations are revealed independently with the stated retention probability. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BlockStatistics 24 declarations Observed block statistics and conditional polynomial density
Observed block statistics and conditional polynomial density
A retained graph uses a single size-d source partition for the entire fitted block layout.
The labeled sources with at least one retained arrow into the specified recipient block.
The number of revealed labeled sources in a recipient block.
Definition (Lean source)
The remaining hidden-source capacity of a block.
Definition (Lean source)
The sum of observed treatment signs over the revealed labeled sources.
The total remaining hidden-source capacity over all blocks.
A recipient label belongs to at most one block. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Partition-supported retained graphs reveal at most d sources in each block. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coefficient-constrained hypergeometric mixture density of distinct block responses.
Definition (Lean source)
Expanding the polynomial product retains exactly allocations with the prescribed total degree. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The row allocation counting polynomial is the binomial polynomial. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coefficient of the binomial polynomial counts treated subsets of a fixed total size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing row subset counts with a fixed global treated count gives the global binomial count. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The constrained row allocation weights sum to one, including zero total capacity. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coefficient-defined density is the exact finite mixture over constrained hidden row counts. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The constrained conditional block density is nonnegative for every input. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Copy each distinct response to its recipient block and set source and padding outcomes to zero.
The actual joint law of the detailed retained graph and every assignment coordinate.
Definition (Lean source)
The actual marginal law of the detailed labeled retained graph.
Every retained graph in the actual fitted block experiment has common partition support. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The indicator vector that a labeled source has at least one retained arrow.
Recover the full original-record mixture from the actual graph-assignment marginal and conditional density.
Definition (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.BlockSupport 11 declarations Support and causal target of the block prior
Support and causal target of the block prior
Recipient blocks contain exactly d labels when the bipartite layout fits. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The source and recipient labels in a block edge are disjoint. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A source has exactly d outgoing edges; other labels have none. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
There are B*d source labels in a fitting block layout. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every recipient in a block has exactly d incoming source labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Labels outside all recipient blocks have no incoming edges. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Baselines in the support interval give the required coefficient-mass and degree bounds. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the outgoing degree counts gives the block prior's constant causal target. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The compact baseline density gives zero mass outside its declared support. the stated conclusion holds.
Formal statement
Proof (Lean source)
All coordinates of the independent baseline draw lie in the support interval. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Almost every prior schedule belongs to the model class and has the stated constant signed target. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ChiSqDecomposition 2 declarations Conditional chi-squared decomposition interface
Conditional chi-squared decomposition interface
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.CompatibleCompletions 13 declarations Restriction to the original unrevealed source labels is a bijection between compatible source partitions and words with the observed remaining row capacities.
Compatible partitions as capacity-constrained hidden-label words
Restriction to the original unrevealed source labels is a bijection between compatible source partitions and words with the observed remaining row capacities. The inverse fixes every revealed label at its observed row. Detailed retained edge subsets remain in the compatibility predicate throughout.
Compatible completions of the entire detailed retained graph.
Original source labels whose association was not revealed.
Row words on original hidden labels with exactly the remaining row capacities.
The Boolean reveal statistic is false exactly when the original label has no retained edge. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Any two compatible completions agree on every revealed original source label. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual hidden word of a compatible completion.
Definition (Lean source)
Compatible partitions and capacity-constrained words on the original hidden labels are in bijection; every revealed source remains fixed.
Definition (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.CompleteBlockConstruction 32 declarations Complete-block construction, support, and response moments
Complete-block construction, support, and response moments
The fixed complete directed blocks of augmented degree d plus one.
Definition (Lean source)
Complete block edges exclude all diagonal arrows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Complete directed blocks of size d+1, sharing one fixed graph under both prior signs.
Definition (Lean source)
The labeled members of one complete block, including its own coordinate.
Each full block has exactly d+1 members. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Quotients index a full block precisely for nonpadding labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A nonpadding label's incoming neighborhood is its block with itself removed. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Padding labels have no incoming arrows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Full block rows have off-diagonal degree d; padding rows have degree zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Complete directed block edges are symmetric, so outgoing degrees equal incoming degrees. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A full block row uses exactly its own baseline. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Padding rows have zero baseline as well as zero treatment effects. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Baselines and amplitudes in the declared support produce admissible complete-block schedules. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The number of nonpadding labels is the number of full blocks times their size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A complete-block response is its baseline plus the translated centered block sign sum. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each nonpadding row has total-treatment contrast sigma*h, and padding rows have zero contrast. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete-block construction has its constant signed target on every baseline draw. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The independent compactly supported baselines put the complete-block prior in the model class. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At least one complete block fits for every admissible degree. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full blocks cover at least half the population, as required by the testing separation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The centered sign sum in a full labeled block has second moment equal to its size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual design has the same block sign moment, with all audit coordinates retained. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The baseline translation in a complete block retains every member's observed sign.
Definition (Lean source)
The squared separation of opposite-sign translations has its exact design expectation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Product of the baseline densities translated by the observed complete-block sign sums.
Definition (Lean source)
Tensorized baseline translation bounds the distinct-response energy for every assignment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging over the full assignment-audit design gives the sharp complete-block energy bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete-block response density is jointly measurable in the full design and responses.
Formal statement
Proof (Lean source)
Every conditional complete-block density is nonnegative. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent translated baselines give an integrable, normalized product density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each conditional product response law is a probability law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The averaged complete-block response energy is at most the population-scale envelope. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.CompleteBlockDensity 8 declarations Translation of the independent prior baselines gives the normalized product response density, conditional on every coordinate of the actual design.
Complete-block conditional density identification
Translation of the independent prior baselines gives the normalized product response density, conditional on every coordinate of the actual design.
The product of translated baseline laws is the product density against vector volume. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independently translating all prior baselines gives the exact vector response density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional on the entire assignment, complete-block responses have the stated density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Mixing a jointly measurable recording channel is the pushforward of the independent prior-design product law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Retaining the entire design draw, the conditional product-density joint law is exactly independent baselines translated by the observed signs. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual full-record prior mixture is the copying of the conditional-density joint law with its full assignment-audit marginal. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The common full-design marginal makes the joint response distance at most the square root of the averaged translation energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The genuine complete original-record mixtures satisfy the population translation bound; projection retains the labeled graph and every treatment coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.CompleteBlockRecord 16 declarations The distinct responses determine every labeled outcome, including padding.
Complete-block copying and reconstruction
The distinct responses determine every labeled outcome, including padding. Reading one fixed member of each block recovers the responses without discarding the graph or any treatment coordinate.
Padding labels have identically zero outcome under the complete-block prior. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A fixed labeled representative of each full block.
The chosen member belongs to its intended block. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Copy each distinct block response to all its labeled members; padding stays zero.
Read the distinct responses while preserving all graph and treatment coordinates.
Copying is measurable on the full labeled record space.
Formal statement
Proof (Lean source)
Reading the fixed representatives is measurable.
Formal statement
Proof (Lean source)
At a full block member the copying map returns exactly that block's response. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At padding labels all terms in the copying sum vanish. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reading the copied outcomes is an exact left inverse, including graph labels and assignment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The original record is exactly the copying of its translated block baselines. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete retained graph is independent of the sign, amplitude, and baseline draws. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full recording channel is jointly measurable in baselines and the actual design draw.
Formal statement
Proof (Lean source)
Extracting after copying recovers any law of distinct responses and ancillary coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
No testing information is lost when distinct responses are copied into the original record. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For any joint baseline-design law, the original-record law is exactly the copied reduced law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.CompletionCounting 7 declarations The multinomial word-fiber theorem counts capacity-constrained allocations of original hidden source labels.
Exact multiplicities of labeled hidden completions
The multinomial word-fiber theorem counts capacity-constrained allocations of original hidden source labels. The counts include all compatible partitions, rather than unlabeled or reduced-information observations.
Functions with specified row-fiber sizes on an arbitrary finite label type.
Definition (Lean source)
Reindexing original labels preserves every row-fiber cardinality. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Capacity-constrained words are invariant under bijections of the original labels.
Definition (Lean source)
The exact multinomial count on an arbitrary finite original-label type, with no division or rounding ambiguity: the count times the row factorials is the total factorial. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact count of compatible partitions times the remaining row factorials is M!. This is the common labeled-completion denominator, including M = 0. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ConditionalDensityBridge 9 declarations Normalize the full retained-graph fiber without discarding assignment coordinates.
The actual positive-graph conditional density
Normalize the full retained-graph fiber without discarding assignment coordinates.
Reduction of the reconstructed original record preserves its exact density kernel. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Graph and full assignment atoms factor under the actual independent design. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual finite response density is measurable jointly with the assignment.
Formal statement
Proof (Lean source)
Independent reference responses have the product reference density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The normalized positive-graph fiber has the displayed response density and keeps the entire actual assignment vector. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The displayed posterior density is a density relative to the actual assignment and independent reference responses, including reference-zero sets. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual conditional Radon--Nikodym likelihood is the complete-label posterior density ratio almost everywhere under the reference. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ConditionalGraphMixture 31 declarations The normalized graph fibers have unit mass on every positive-probability graph.
Finite retained-graph conditioning and conditional testing bounds
The normalized graph fibers have unit mass on every positive-probability graph. Common finite mixtures average conditional total-variation bounds, and a common reference converts two conditional chi-squared budgets into a testing bound.
The distinct-response record has exactly the actual complete retained-graph marginal. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The unnormalized graph fiber has mass equal to the actual graph-atom probability. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On every graph atom of positive probability, the actual conditional law is a probability law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A null retained graph has zero conditional law under the chosen null-atom convention. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Multiplying a conditional law by its graph probability recovers the unnormalized fiber. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restoring the fixed graph coordinate after projecting a graph fiber is exact. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual distinct-response record is the mixture of its normalized complete-graph fibers. Null graph atoms contribute zero, so no conditional law on a null event is assumed. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A common finite mixing marginal averages conditional total-variation distances. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full original-record distance is bounded by the mean conditional distance over its actual complete retained-graph marginal, with all assignment coordinates retained. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two conditional laws with the same chi-squared budget against a common reference have distance at most the square root of that budget. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual complete retained-graph marginal is a probability law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a finite probability space, averaging square roots costs at most the square root of the mean. This is Cauchy--Schwarz with the constant function one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A finite probability mixture splits into a bad-event mass and the square root of its good-event second-moment budget. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional square-root bounds give the roadmap's good-event bound for the complete original record, retaining the full graph and assignment marginal. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The cosine baseline density is even. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reflecting a baseline draw preserves its probability law. the stated conclusion holds.
Formal statement
Proof (Lean source)
Reflecting independent block baselines preserves their joint law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The prior is invariant when all baselines are reflected, with the labeled partition fixed. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reversing the sign and the baselines negates every response, while preserving the complete retained graph and all observed treatment coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The entire negative-sign record law is the response reflection of the positive-sign law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging identical recipients commutes with reflection of every outcome. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Response reflection preserves the full detailed retained-graph coordinate and assignments in the reduced experiment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditioning on any complete retained graph commutes with response reflection. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reflecting every response preserves the uniform-sign reference density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reflecting a reference response preserves its law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The independent reference responses are jointly invariant under reflection. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two conditional sign laws have equal chi-squared divergence against the actual assignment-reference product, by measurable response reflection. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The negative-sign conditional law is also dominated by the reference, since reflection preserves that reference and transports the actual positive-sign law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On any positive-probability detailed graph, square-integrable conditional likelihoods convert the common chi-squared divergence into the conditional testing bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ConditionalLikelihoodBounds 9 declarations The finite row-channel mixture bounds actual conditional likelihoods and supplies square integrability without an extra regularity premise.
Finite conditional likelihood bounds
The finite row-channel mixture bounds actual conditional likelihoods and supplies square integrability without an extra regularity premise.
Tensorizing the finite row bound gives a finite bound for every fixed allocation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every actual fixed-partition response law obeys the finite row-channel bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging actual partition and design draws preserves the uniform density bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restricting to a graph atom costs only its inverse probability in the density bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A finite domination constant bounds the Radon--Nikodym derivative almost everywhere. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite measure domination supplies the square-integrability used by the testing step. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional likelihoods have finite second moments on each positive graph atom. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The roadmap's conditional testing bound requires no extra square-integrability assumption. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging over the actual complete graph marginal gives the good-event testing bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ConditionalWalshBridge 13 declarations Enumerate each completed row using its original source labels, expand its actual translated response density, and average over the exact compatible posterior.
Actual labeled-completion Walsh likelihood
Enumerate each completed row using its original source labels, expand its actual translated response density, and average over the exact compatible posterior. The reference-zero set is kept separate from the positive-density expansion.
A row sign vector reads the original assignment at every completed source label.
Definition (Lean source)
Enumerating a completed row preserves its full labeled sign sum. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The positive-prior density is a product of actual completed-row channels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full fixed-partition likelihood expands row by row without losing labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every completed density vanishes when any reference row density is zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On positive reference density, the actual conditional response likelihood is exactly the uniform posterior average of products of labeled Walsh expansions. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The averaged actual density vanishes on the reference-zero set as well. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact completion-averaged Walsh density, extended by zero off its reference support and off compatible graphs. Completion averaging retains the assignment labels.
Definition (Lean source)
On the actual graph support this finite Walsh density equals the actual density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Replacing the posterior density by its finite Walsh expansion gives exactly the full original-record law, with all edge subsets and outcome copies. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Recovering distinct responses from the Walsh density preserves the complete retained graph and every assignment coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual conditional positive-prior law, expressed using its finite completion-averaged Walsh density. Restriction conditions on the entire graph. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ConditionalWalshRegrouping 16 declarations Split each completed row into its fixed revealed labels and original hidden labels, then group hidden selections by degree before posterior averaging.
Revealed and hidden label regrouping of the actual Walsh likelihood
Split each completed row into its fixed revealed labels and original hidden labels, then group hidden selections by degree before posterior averaging.
Reindex selected Walsh coordinates without changing their cardinalities. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Split selected labels uniquely across disjoint revealed and hidden sets. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A completed row Walsh expansion indexed by original population labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual completed-row Walsh sum, with the revealed monomial separated and hidden original-label subsets grouped by their selected degree.
Definition (Lean source)
Exact revealed/hidden splitting and degree regrouping for a compatible row. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The posterior average of the actual likelihood, regrouped into revealed monomials and hidden degree selections while preserving original labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Expanding the completed likelihood across rows separates the fixed revealed monomial and coefficient product from the selected hidden-label monomials. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact uniform-completion moment of hidden selected-label monomials. The row degrees are fixed, while their original labels remain jointly allocated.
Definition (Lean source)
Move the posterior average onto hidden monomials after expanding across rows. All revealed selections and response coefficients are fixed by the full record. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual density ratio with its posterior average confined to the hidden selected-label moment; no graph or treatment coordinate has been discarded. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual posterior density after splitting revealed selections and grouping hidden selections by degree, extended by zero on the reference-zero set.
Definition (Lean source)
Regrouping gives the actual conditional response density on every compatible retained graph, including zero reference-density endpoints. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The reduced actual law uses the regrouped density and retains the complete graph together with every assignment coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditioning on the entire detailed graph uses exactly the regrouped posterior likelihood, with no independence substitution for hidden treatments. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ContractionSeries 8 declarations Geometric and exponential series for contraction
Geometric and exponential series for contraction
The factorial dominates the exponential-normalized power needed for the contraction series. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Counting disjoint active revealed and hidden row sets gives the coefficient bound used before extending the contraction sum to infinite series. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The nonnegative contraction geometric series sums to the reciprocal gap. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite active-row contraction sum is dominated by an exponential series in the revealed energy times a geometric series in the hidden energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Removing the constant Walsh term from the finite active-row sum produces exactly the minus-one bound in the contraction roadmap. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.DesignBridge 6 declarations Assignment and audit bridges
Assignment and audit bridges
The canonical product design has the required assignment marginal. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The canonical product design has the required audit marginal. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two coordinates of the canonical product design are independent. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The three design atoms determine the canonical assignment-audit product law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The three design atoms imply that the joint design is a probability law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Measure-valued assignment expectations equal finite-design Bernoulli expectations. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.DetailedGraphLikelihood 13 declarations Independent audit marks give a product likelihood on every labeled edge.
Likelihood of a complete detailed retained graph
Independent audit marks give a product likelihood on every labeled edge. For compatible graphs this likelihood depends only on the true and retained edge counts, including at audit probabilities zero and one.
A retained coordinate is Bernoulli on a true edge and identically false on a nonedge. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The probability of the full retained indicator vector is the product over all labeled coordinates, with no summation or deletion of retained-edge subsets. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A graph containing an arrow absent from the true graph has zero probability. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a compatible detailed graph the likelihood is q to the retained-edge count times one minus q to the number of unretained true edges. This formula includes both endpoints. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every source partition has exactly B*d*d true arrows, counted with their full labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional on a true partition, the complete retained-graph probability has the common likelihood q^|H| (1-q)^(B*d*d-|H|) for every compatible completion. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Detailed retained subsets have the same likelihood under any two compatible source partitions, even at the audit endpoints. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full fixed-partition graph likelihood vanishes off compatible completions and is constant on them. Compatibility records every observed arrow with both endpoint labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating any function over the uniform partition prior is its finite arithmetic mean. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under the actual audit law, averaging the full detailed graph likelihood over the uniform source partitions gives the compatible-completion count times its common likelihood. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each labeled partition has the same atom mass in the construction prior. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The joint atom for a fixed labeled partition and detailed retained graph is the prior partition mass times its exact full graph likelihood. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At every positive-probability detailed graph, Bayes' rule assigns each compatible labeled partition exactly the reciprocal of the number of compatible completions. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ElbowAlgebra 4 declarations Precision-scale endpoint and elbow algebra
Precision-scale endpoint and elbow algebra
The source reveal probability is bounded above by the union bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exponential convexity gives a uniform chord lower bound for reveal probabilities. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Endpoint formulas and the explicit positive-retention elbow comparison. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observable risk envelope is at most twenty-four times the explicit precision scale after truncation at one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.FrontierConsistency 2 declarations The elbow comparison turns vanishing precision scale into the two ratio limits, including the infinite value of the inverse-retention ratio at zero retention.
Sequence limits for the explicit precision scale
The elbow comparison turns vanishing precision scale into the two ratio limits, including the infinite value of the inverse-retention ratio at zero retention.
The precision scale is nonnegative on the retention domain. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The scale vanishes exactly when both population and audit ratios vanish. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.FrontierLower 4 declarations The supported two-prior reduction and integer block rounding assemble the complete-record testing bound into the explicit minimax scale.
Explicit frontier lower bound
The supported two-prior reduction and integer block rounding assemble the complete-record testing bound into the explicit minimax scale.
At the prescribed testing amplitude, the opposite supported priors give a squared-target minimax lower bound, including estimator randomization. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Squaring the testing scale dominates the frontier scale whenever the block sources fit inside the population. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Floor rounding supplies between a quarter and a half population of sources in the small-degree regime. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The explicit frontier minimax lower constant follows from supplied blocks at large degree and rounded hidden-partition blocks at small degree. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.GeniePartition 2 declarations Genie-partition translation bound
Genie-partition translation bound
Mixing probability laws over a common finite marginal preserves a uniform TV bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Giving the partition to the observer yields the product-translation upper bound on the original-record distance. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.GoodEvent 6 declarations Good-event probability for hidden source counts
Good-event probability for hidden source counts
Unrevealed source labels, counted in the source index type, are bounded by total capacity. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The inverse-third moment of the hidden count factors over independent source reveals. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fourth-power form avoids numerical approximations in the binomial tail constant. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Markov's inequality applied to the inverse-third count moment gives the required tail. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.GroupedConditionalLikelihood 8 declarations Regroup the exact labeled posterior expansion by total hidden degree.
Total-hidden-degree coefficients of the actual conditional likelihood
Regroup the exact labeled posterior expansion by total hidden degree. The coefficient fibers keep all row capacities and binomial slot multiplicities.
The response coefficient for a revealed-subset family and a total hidden degree, with the exact capacity-constrained binomial multiplicities.
Definition (Lean source)
The same actual coefficient indexed by bounded row degrees, exactly matching the allocation-energy lemmas' finite domain. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The grouped likelihood density keeps the actual labels and the reference-zero extension while making the hidden-degree coefficient fibers explicit.
Definition (Lean source)
Regrouping preserves the entire posterior density, including incompatible graphs and zero reference-density endpoints. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.HiddenAllocationContraction 1 declarations Hidden-allocation chi-squared contraction
Hidden-allocation chi-squared contraction
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.HiddenAllocationEnergy 12 declarations Finite weighted Cauchy–Schwarz and the exact allocation weight count bound each active-row coefficient's squared norm.
Weighted energy of constrained hidden allocations
Finite weighted Cauchy–Schwarz and the exact allocation weight count bound each active-row coefficient's squared norm. The good-event binomial ratio then gives one contraction factor per hidden active row. These bounds do not assume the unfinished identification of the conditional likelihood.
The squared Walsh coefficient is integrable under the normalized row reference; boundedness supplies this regularity without an added premise. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The paper's row energy is exactly the coefficient's squared norm under the row reference law, including reference-density zeros. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Products of row coefficients have finite squared norm, and independence factors that norm into the product of the row energies. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.HiddenAllocationOrthogonality 11 declarations Different sets of active response rows are orthogonal under the independent row reference.
Orthogonality of hidden-allocation response supports
Different sets of active response rows are orthogonal under the independent row reference. Positive degrees within an active row are not assumed orthogonal. The finite weighted and Pythagorean identities assemble the support-group step of the hidden-allocation contraction roadmap.
The constant row coefficient is one almost everywhere under the reference law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The nonconstant row coefficients have zero mean under the actual reference law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A nonconstant coefficient is orthogonal to the constant coefficient. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cross products of arbitrary row coefficient products are integrable, since each row coefficient is bounded by one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A row active in exactly one coefficient product forces their reference cross integral to vanish; degrees on shared active rows may differ. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.HiddenAllocationSummation 5 declarations Summing over the observed total hidden degree removes the degree constraint exactly.
Summing constrained allocation energies
Summing over the observed total hidden degree removes the degree constraint exactly. The remaining nonnegative allocation energies factor over rows, including restrictions requiring positive degree on hidden active rows. This supplies the degree-summation step of the hidden-allocation contraction proof without assuming a posterior identity.
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.HiddenSelectionAveraging 13 declarations Reindex the completion likelihood by capacity-constrained words on the original hidden source type.
Original hidden-label selection averages
Reindex the completion likelihood by capacity-constrained words on the original hidden source type. Permutations of those labels preserve the posterior average.
A completed row's hidden labels are exactly its hidden-word fiber. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Selected-subset monomials commute with an injective relabeling. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The hidden moment in the actual likelihood is the original-label word average. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.HiddenSignEnergy 6 declarations The exact hidden-sign normalization survives adjoining the independent revealed signs.
Joint revealed and hidden sign energies
The exact hidden-sign normalization survives adjoining the independent revealed signs. Finite likelihood expansions therefore have squared norms weighted by inverse binomial coefficients, without treating hidden row counts as independent.
The degree-zero symmetric hidden polynomial is exactly the constant one, including the endpoint with no hidden labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.LabelSubsetConditionalLikelihood 9 declarations Disjoint revealed rows identify their subset families bijectively with subsets of the union of revealed labels.
Revealed-label indexing of the conditional Walsh likelihood
Disjoint revealed rows identify their subset families bijectively with subsets of the union of revealed labels. This puts the actual posterior likelihood in the label-monomial indexing used by the joint sign energy decomposition.
Compatibility assigns each revealed source to a unique row. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Intersecting the union of a disjoint row-subset family with one row recovers exactly that row's selected labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every subset of a row union is recovered from its intersections with the rows. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing over disjoint row-subset families equals summing over subsets of all revealed labels, with row intersections as the inverse map. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Products over a row-subset family are precisely monomials in its union of original revealed labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The grouped actual likelihood is a sum of distinct revealed-label monomials and symmetric hidden polynomials with the exact row-intersection coefficients. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual posterior density with each revealed monomial indexed by its source-label subset, retaining the reference-zero extension.
Definition (Lean source)
The label-subset density equals the actual grouped density on every graph and response, including impossible graphs and reference-density zeros. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.LikelihoodExpansion 24 declarations Conditional likelihood for the hidden-allocation record
Conditional likelihood for the hidden-allocation record
Extract distinct block responses by averaging identical recipient outcomes.
Definition (Lean source)
Full retained graph together with all assignments and distinct block responses.
Definition (Lean source)
Copying a block response gives that same value at every recipient in its block. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging the copied recipients recovers the distinct response exactly. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two recipients in the same block have identical potential outcomes for every assignment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Sources and padding labels have zero response under every constructed schedule. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a genuine block record, the distinct-response average is each recipient's response. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Copying the recovered distinct responses reconstructs the entire original record, including every retained edge and treatment coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The response-copying channel is measurable jointly in the full finite marginal and the distinct real responses.
Formal statement
Proof (Lean source)
Recovering distinct responses is a measurable statistic of the complete original record.
Formal statement
Proof (Lean source)
Applying the measurable copying channel to the reduced law recovers the complete original-record mixture, without using the unfinished conditional-density identity. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A measurable map contracts total variation by taking preimages of test events. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Complete block mixtures are probability laws for every sign and amplitude. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Recovering and copying distinct responses preserve total variation exactly. Thus working with distinct outcomes retains all the information in the original record. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A recipient response is its baseline plus the centered source-sign shift. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Enumerating a recipient's actual d source labels gives a row-channel sign vector. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
All distinct responses, conditional on a fixed partition and the entire design draw, are independent baseline translations by actual source signs. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a fixed partition and complete design draw, the positive-sign response law is exactly a product of row-channel components indexed by the actual source labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every fixed-partition, fixed-design response law is dominated by the independent reference responses, before any conditional allocation calculation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditioning on a finite retained-graph atom; values on null atoms are immaterial.
Definition (Lean source)
After mixing the partition and baselines, the assignment-response marginal is still dominated by the actual assignment marginal times the reference responses. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restriction to a retained-graph atom and rescaling preserve reference domination; this also covers null atoms under the total ENNReal convention. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The positive-sign conditional block law is dominated by the reference law on almost every retained graph. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.OracleQuadraticEnergy 9 declarations Finite quadratic coefficient energy
Finite quadratic coefficient energy
The augmented coefficient mass is at most one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A pair square is bounded by its absolute coefficient mass. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Swapping the two coordinates preserves the row-pair incidence set. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The symmetrized collected coefficient is the rowwise pair-coefficient sum. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Out-degree bounds the number of rows sharing a coordinate pair. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the absolute pair masses over a row uses at most twice its augmented degree. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reindexing pairwise row energies preserves all neighborhood coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Ordered pairs count each symmetrized quadratic coefficient twice. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite Cauchy–Schwarz, out-degree multiplicity and row mass control the quadratic energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.OracleVariance 1 declarations Supplied-graph score variance bound
Supplied-graph score variance bound
The supplied-graph additive score has variance at most five times squared augmented degree over population size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.OracleWalsh 29 declarations Oracle variance chain
Oracle variance chain
The compulsory own coordinate adjoined to the off-diagonal sources.
The additive coefficient on an augmented source coordinate.
Definition (Lean source)
The assignment-averaged row outcome in the centered-sign expansion.
Definition (Lean source)
No own coordinate occurs among the off-diagonal sources. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing augmented coefficients separates the own treatment coefficient. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The augmented coefficient mass is precisely the own plus spillover mass. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The augmented row has at most d+1 coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Adjoining the diagonal increases coordinate multiplicity by at most one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The centered row baseline has magnitude at most one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Substituting treatment=(1+sign)/2 gives the actual centered row response. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sum of augmented signs is the recorded supplied-graph weight. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The constant coefficient of the score is the all-treated contrast. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Removing the diagonal sign squares leaves a genuinely quadratic, distinct-coordinate term. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact degree-at-most-two expansion of the centered supplied-graph score. The quadratic sum uses ordered pairs so it requires no arbitrary ordering of the population. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The collected coefficient of a source sign in the oracle score.
Definition (Lean source)
Collecting the linear terms by source preserves all augmented neighborhoods. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two centered signs are orthonormal under the actual assignment measure. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Orthogonality gives the exact second moment of the linear sign polynomial. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cauchy-Schwarz and the out-degree bound control the linear coefficient energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete linear contribution to the oracle variance is at most 4D²/n. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A singleton sign is orthogonal to every distinct-coordinate quadratic monomial. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual linear and quadratic parts of the supplied score have zero cross moment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ordered-pair coefficient retains the true augmented-neighborhood incidences.
Definition (Lean source)
Diagonal coordinates have already contributed to the causal target. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Collecting the quadratic monomials by ordered source pair changes no graph incidence. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equal unordered pairs are precisely the two orientations of an ordered pair. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fourth sign moment matches the two orientations, with no other surviving pairs. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the fourth moments leaves both orientations of each non-diagonal pair. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact quadratic energy: ordered coefficients pair with their reverse orientation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.PartitionResponseDensity 10 declarations Before averaging compatible source partitions, the actual responses are independent translations of the prior baselines.
Fixed-partition density of the original hidden-allocation experiment
Before averaging compatible source partitions, the actual responses are independent translations of the prior baselines. The identities here preserve the complete retained graph and every assignment coordinate for either sign.
The actual distinct response when all block baselines are zero.
Definition (Lean source)
Adding independent baselines adds them coordinatewise to the actual distinct responses. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Product baseline densities translated by the actual fixed-partition response shifts.
Definition (Lean source)
The fixed-partition density is measurable jointly in the full design and responses.
Formal statement
Proof (Lean source)
Conditional on any fixed partition and complete design draw, independent prior baselines have exactly the translated product response density, for both signs. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Copying the shifted baselines reconstructs the original record for any actual design realization; detailed edges and ancillary assignments remain in the record. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the fixed-partition density against the complete design is equivalent to independent baselines followed by their actual response translations. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a fixed source partition, the complete original-record mixture is exactly obtained by drawing the actual design and the translated product response density, then copying. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Drawing partition and baselines independently is equivalent to first mixing the fixed-partition original-record laws. This identity uses the actual complete design. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full original-record block mixture has an exact density representation conditional on the true partition and actual design, prior to the posterior-completion calculation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.PartitionTranslationBound 8 declarations The actual labeled source sums have second moment d under the assignment marginal.
Translation testing bound conditional on the true partition
The actual labeled source sums have second moment d under the assignment marginal. Tensorized baseline translation and common-marginal Hellinger averaging then bound the complete original-record distance for each fixed partition.
The fixed-partition shift uses the actual incoming source labels of any recipient. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Opposite signs have exactly h squared over d expected squared shift separation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Tensorized translation controls fixed-partition response energy at each design draw. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging the translation bound keeps every assignment and audit coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Fixed-partition product densities are nonnegative. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent translated baselines normalize every fixed-partition response density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Common full-design marginals turn the averaged response energy into a joint TV bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full original record conditional on the true partition satisfies the genie bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.PosteriorCompletionLaw 10 declarations Disintegration over the complete retained graph and assignment preserves every coordinate.
Full-record posterior completion mixture
Disintegration over the complete retained graph and assignment preserves every coordinate. The compatible-partition posterior is uniform and its denominator is the exact labeled multinomial count.
The finite full graph-assignment law for a fixed labeled source partition.
A fixed-partition response channel depends on the assignment but not the audit marks.
Definition (Lean source)
The fixed-partition original-record law factors through its full graph-assignment law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A graph-assignment atom factors into its exact detailed graph likelihood and the probability of the entire assignment vector. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The common likelihood includes every assignment coordinate and retained-edge subset. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform finite mixing followed by a common-likelihood observation channel gives the uniform posterior over compatible completions, including null observation atoms. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete original-record mixture is the actual full graph-assignment marginal followed by a uniform mixture of all compatible fixed-partition response kernels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.PosteriorResponseBridge 19 declarations A compatible labeled partition splits each source row into the observed signs and its hidden labels.
Compatible-completion response shifts
A compatible labeled partition splits each source row into the observed signs and its hidden labels. The hidden treated count supplies the exact shift used in the polynomial conditional density; no treatment coordinate is discarded.
The original source labels assigned to a specified block by a completion.
Definition (Lean source)
Hidden labels in a completed row retain their original population labels.
Definition (Lean source)
Count treated hidden labels in a specified compatible completed row.
Definition (Lean source)
Every completed row has exactly d original source labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Compatibility with the complete graph fixes the row of every revealed label. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A compatible completion has exactly the observed remaining capacity in each row. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The completed row's treated hidden count is an admissible polynomial index. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Within a compatible completion, a hidden row label is precisely a source in that row with no retained arrow anywhere in the complete graph. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Completed row treated counts sum to the observed global hidden treated count; this equality uses every assignment coordinate of each original hidden source label. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Incoming neighbors of any block recipient are the completion's original source labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A sum of centered Boolean signs is twice the treated-label count minus the row size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The completed source sum is exactly the revealed signs plus twice the hidden treated count minus the remaining capacity. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual completed hidden counts are admissible polynomial indices, retaining all original labels and the detailed retained edge subsets.
Definition (Lean source)
The actual admissible allocation satisfies the coefficient extraction's global degree constraint, including the endpoint of zero hidden capacity. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The product row density associated with the actual compatible allocation. Its shifts are precisely those appearing in the coefficient-extraction formula.
Definition (Lean source)
The original fixed-partition density is exactly the row product at the completed hidden treated allocation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fixed-partition product density satisfies exactly the total-degree constraint used in the hypergeometric polynomial formula. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Before the compatible-allocation counting step, the actual full mixture is exactly the partition average of the allocation row density followed by copying every outcome. This representation preserves all retained edges and all assignment coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.PosteriorTreatedDensity 8 declarations The treated-label word average is the coefficient-extraction density on the complete retained graph and the entire assignment vector.
Exact posterior response density
The treated-label word average is the coefficient-extraction density on the complete retained graph and the entire assignment vector.
The actual compatible partition's row treated count is the restricted word's row count. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Compatible partitions have the displayed response shift for the observed detailed retained graph, independently of the audit representative used to write the density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The product response at an admissible row treated-count vector.
Definition (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.PublishedModel 47 declarations Published SNIPE convention gate and specialization
Published SNIPE convention gate and specialization
Published raw-polynomial schedules allow diagonal arrows and zero edge coefficients.
Definition (Lean source)
The published in-neighborhood, including diagonal arrows when present.
Definition (Lean source)
The published out-neighborhood, including diagonal arrows when present.
Definition (Lean source)
Order-one neighborhood interference restricts only unsupported and higher-order coefficients; loops and zero singleton coefficients are permitted.
Definition (Lean source)
The published raw-monomial polynomial potential outcome, including the empty monomial.
Definition (Lean source)
The coefficient-mass envelope is the maximum row sum of absolute polynomial coefficients, including the empty monomial. The empty-population extension is zero.
Definition (Lean source)
Cortez-Rodriguez, Eichhorn and Yu (2023), arXiv:2208.05553v4, Sections 3.1–3.2, Assumptions 1–2 and equations (3.2)–(3.3). At interaction order one the polynomial has a constant and neighborhood singleton terms, and its defined envelope is their maximum absolute-coefficient mass. Neighborhoods may contain their own vertices, and singleton coefficients may vanish. No normalization or degree bound is part of this convention gate. Source: https://arxiv.org/html/2208.05553v4#S3 .
Definition (Lean source)
The paper's bounded-envelope and bounded-total-degree specialization of the order-one published model. These restrictions belong to the specialization, not the cited conventions.
Definition (Lean source)
The all-treated minus all-control average in the published polynomial carrier.
Definition (Lean source)
Adjoin all diagonal arrows and encode the baseline, own effect, and off-diagonal coefficients as order-one monomials.
Definition (Lean source)
Removing diagonal arrows gives an irreflexive published graph. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Remove diagonal arrows and read the empty and singleton polynomial coefficients as additive schedule coefficients.
Definition (Lean source)
Equality of graph and all supported polynomial coefficients.
Definition (Lean source)
Equality of schedules modulo unused off-graph values of the coefficient array.
Definition (Lean source)
The measurable augmented graph carrier contains every known diagonal arrow.
The augmented complete record consists of the diagonal-complete graph, assignments, and outcomes.
Add the known diagonal arrows to a recorded off-diagonal labeled graph.
Every diagonal arrow is present after graph augmentation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Augment only the graph coordinate of the complete record.
Definition (Lean source)
Remove known diagonal arrows while preserving all assignments and outcomes.
Removing and re-adjoining diagonals is the identity on augmented records. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Adjoining and then removing diagonals is the identity on original records. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Adjoining known diagonal arrows is measurable.
Formal statement
Proof (Lean source)
Removing known diagonal arrows is measurable.
Formal statement
Proof (Lean source)
The deterministic measurable equivalence adds the known diagonals.
Definition (Lean source)
The published schedule under the same off-diagonal audit and assignment channel, with known diagonals adjoined.
Definition (Lean source)
The complete augmented record and independent uniform seed law at a published schedule.
Definition (Lean source)
All measurable seeded real-valued estimators of the augmented record.
Definition (Lean source)
The extended minimax risk over a specified published class and all measurable seeded augmented-record estimators.
Definition (Lean source)
Augmentation puts the baseline at the empty monomial. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Augmentation puts each treatment effect at its singleton monomial. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The augmented neighborhood is the original one with the own coordinate inserted. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Stripping the augmented schedule recovers every coefficient that is used by an outcome. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Only the empty and supported singleton monomials survive augmentation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under the published polynomial convention, augmentation preserves every outcome. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Preserving all outcomes preserves the all-treated causal contrast. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The augmented original record is exactly the published record under the same channel. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Augmentation adds exactly the own recipient to each out-neighborhood. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The published coefficient mass equals the original row coefficient mass. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A degree-d additive schedule maps to a diagonal-complete degree-(d+1) published schedule. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A diagonal-complete published neighborhood is the stripped neighborhood plus its own vertex. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The same diagonal removal identity holds for out-neighborhoods. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Stripping removes one degree and retains exactly the published row coefficient mass. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Re-augmentation recovers the graph and every supported coefficient of an order-one schedule. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Composing a published estimator with record augmentation preserves squared loss. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Class inclusion and the measurable record map transfer the minimax lower bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional on the cited conventions, diagonal augmentation and stripping are inverse specializations, preserve all outcomes and the target, give an invertible record transformation, and transfer lower bounds by class inclusion under the same assignment-audit channel. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.RetainedRowAverage 9 declarations Enumerate the source fiber of each original partition before reducing the full retained graph to its row counts.
Averaging actual partition-dependent retained rows
Enumerate the source fiber of each original partition before reducing the full retained graph to its row counts.
Under a fixed original partition, membership in a revealed row is exactly source revelation together with membership in that partition's source fiber. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A size-d source fiber can be enumerated without dropping any labels. The revealed row count then equals the count in its enumerated source-reveal row. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The enumerated reveals in any fixed original partition have the independent row law, even though the observed retained graph keeps all edge subsets. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Canonical count patterns preserve both row energies for any actual reveal row. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The nonconstant retained envelope is the independent-row expression under any label-preserving enumeration of the original source partition. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact graph marginal is the uniform mixture of the fixed-partition graph laws, before any row-count reduction. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each actual retained-row contribution is nonnegative, so removing the good indicator is valid before partitionwise averaging. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Fixed-partition averaging of the actual row-count envelope uses independent reveals only after its original labels have been enumerated. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging the full detailed graph mixture gives the finite nonconstant contraction series. No source or edge labels are discarded in forming the law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.RevealedSubsetEnergyBridge 13 declarations Remove masked inactive rows and reindex the original revealed-label subsets by families of subsets of the disjoint revealed rows.
Exact row factors in the revealed-label energy envelope
Remove masked inactive rows and reindex the original revealed-label subsets by families of subsets of the disjoint revealed rows. All original labels remain in the bijection; only their rowwise energy factors are simplified.
The constant Walsh coefficient has unit reference energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On disjoint active rows, the masked product consists of the unrestricted revealed-degree factors and the positive-degree hidden factors; all other rows contribute exactly one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing nonempty revealed subsets and every hidden degree is precisely revealed row energy, rather than an independent hidden-row approximation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The revealed-subset energy factor depends only on the revealed and hidden counts, and therefore agrees with any row reveal pattern of those counts. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A canonical reveal pattern with r revealed slots preserves the two row counts. It is used only to express energies, after the full-label reindexing.
The canonical count pattern has exactly r revealed slots and d-r hidden slots. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At a fixed revealed-active set, the row-subset sum factors into independent nonempty-subset sums; inactive rows have the unique empty selection. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact row-subset envelope before revealed-active rows are grouped.
Definition (Lean source)
Grouping the exact revealed-subset families by their nonempty rows gives products of row-subset energies for every disjoint pair of active sets. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
When row counts match, the exact active-set envelope is the product of the revealed and hidden row energies used by independent-row averaging. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The original label enumeration and the disjoint row-subset family have identical envelopes, including the constant coefficient. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Nonconstant disjoint-row envelope expressed through the actual row counts.
Definition (Lean source)
Summing all actual revealed labels gives the nonconstant disjoint-row energy envelope, with exactly one constant term removed. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ReverseBaselineMoments 7 declarations Evenness removes the baseline mean and independent baseline coordinates remove cross-row covariance.
Integrating the independent baselines in the observable reverse test
Evenness removes the baseline mean and independent baseline coordinates remove cross-row covariance. Compact support bounds the remaining diagonal energy.
A polynomial of a baseline coordinate is integrable on its compact support. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Evenness of the actual joint baseline law centers each coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Distinct independent baseline coordinates have zero mixed moment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The baseline's diagonal second moment is bounded by its support radius. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A weighted baseline sum and its square are integrable without new premises. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent centered baselines contribute only their diagonal energies. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Adding any fixed signal leaves only its squared value and baseline energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ReverseRowMoments 6 declarations Injective restrictions of the full independent assignments and reveals have the size-d product law.
Actual source-row marginals for the reverse test
Injective restrictions of the full independent assignments and reveals have the size-d product law. This connects the finite sign moments to labeled source rows.
Restricting an independent Boolean vector to distinct labels preserves its law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A row selected at distinct assignment and reveal labels has the actual row law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating a row function against its actual labeled inputs uses the row marginal. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual row product law gives the revealed sign energy dp. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual row product law gives the signal mean dp. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual row product law bounds the signal second moment by 3d²p. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ReverseSourceRows 9 declarations Actual source fibers have the row marginals used in the sign calculations.
Labeled source-row variance in the reverse test
Actual source fibers have the row marginals used in the sign calculations. Their disjoint labels give independent row signals and additive variances.
The revealed sign sum at the original labels of a source row.
The total sign sum at the original labels of a source row.
Reindexing a true source fiber connects its two sums to the actual row law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual revealed row energy equals dp. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual row signal mean equals dp. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual row signal second moment is at most 3d²p. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each source's sign and reveal form an independent paired coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Disjoint source fibers give independent row signals in the original-input law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent row variances sum to at most B times the row second-moment bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ReverseTest 32 declarations The test uses the entire recorded graph and assignment to compute revealed sign sums, and reads the distinct responses from the copied outcomes.
Observable reverse-test statistic and its actual partition channel
The test uses the entire recorded graph and assignment to compute revealed sign sums, and reads the distinct responses from the copied outcomes. Its latent representation keeps the original source labels and independent reveal vector.
The sign test's real-valued statistic, computed from the original record.
Definition (Lean source)
The original-record statistic is Borel measurable.
Formal statement
Proof (Lean source)
Retained graphs of the block channel do not depend on baselines or the prior sign. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a compatible detailed graph, a row's revealed set is its source set filtered by whether an arrow from the original label was retained anywhere. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each recorded response has the true row's total sign shift. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The true row's original labels are the image of its finite source fiber. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reindexing a row sum preserves each original source label. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A compatible row's revealed sum is the source-fiber sum with its Bernoulli reveal indicators, keeping assignments at their original population labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The reverse statistic as a function of baselines, assignments and source reveals, conditional on the true source partition.
Definition (Lean source)
The original-record test is exactly the independent-input statistic; the partition is used for the proof but is never supplied to the test. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Actual assignments and source reveals have a product law conditional on every true partition; the complete assignment vector remains available. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For each fixed partition and baseline draw, the actual statistic's law is obtained from independent assignments and independent source reveals. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Mixing the independent-input reverse statistic over the genuine prior parameters.
Definition (Lean source)
The actual full-record statistic has exactly the independent-input mixture law. Every conditional law retains the true source-label fiber and all assignment coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Chebyshev bounds the plus-sign error, including the strict tie convention. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Chebyshev bounds the minus-sign error, with zero assigned to plus. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observable sign test separates scalar laws with opposite centers and controlled squared deviations; no assertion about those moments is assumed in the paper theorem. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar law is the pushforward of the actual probability experiment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A bounded sign sum over the true source fiber is bounded by its row size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every fixed-input scalar statistic is bounded on the genuine baseline support. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The bound on every fixed-input statistic survives the actual parameter mixture. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every squared deviation under the actual scalar law is integrable by bounded support, without a new regularity hypothesis. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The baseline-free squared signal plus the diagonal baseline budget, retaining all original assignment coordinates and source-label fibers.
Definition (Lean source)
Integrating the actual statistic's baselines leaves the finite signal energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under the stated population-size condition, the actual independent-input statistic is jointly Borel measurable.
Formal statement
Proof (Lean source)
The scalar mixture is the pushforward of its actual independent joint inputs. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The remaining scalar moment is bounded by a finite partition, assignment and reveal average; the continuous baseline variables have been integrated out. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing the exact actual-row energies gives the finite baseline contribution. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite signal energy of every genuine partition satisfies the roadmap bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging the uniform fixed-partition bound retains its exact constant. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Substituting the exact center and row-variance bound gives the paper constant. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The revealed-sign outcome test supplies the reverse total-variation bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ReverseTestMoments 13 declarations The independent assignment signs have exact weighted second and fourth moments.
Exact sign moments for the revealed-source reverse test
The independent assignment signs have exact weighted second and fourth moments. These identities supply the finite-row moment calculations in the reverse test.
The actual independent assignment expectation equals the uniform Boolean average. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Weighted independent centered signs have their coefficient energy as second moment. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fourth moment retains the exact diagonal correction, rather than a loose bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing two coefficient levels counts the revealed coordinates exactly. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A revealed sum over r coordinates has second moment r. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Polarizing second moments gives E[AT] = r for revealed and total sign sums. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A revealed sum over r coordinates has fourth moment 3r² − 2r. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Polarizing exact fourth moments yields the mixed revealed/total second moment. The coordinates outside R remain observed assignment coordinates. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mixed row moment is at most 3rd, including the empty revealed set. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The independent reveal count in a size-d row has expectation dp. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging the conditional sign second moment gives E A² = dp. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging the revealed/total sign product gives E[AT] = dp. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent reveals and exact sign moments give E[A²T²] ≤ 3d²p. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.RowEnergyCounts 5 declarations Counting subsets of the actual hidden labels identifies the hidden active-row energy with the binomial degree sum in the contraction roadmap.
Row energies from hidden capacities
Counting subsets of the actual hidden labels identifies the hidden active-row energy with the binomial degree sum in the contraction roadmap. The revealed energy is its complement in the total nonconstant channel energy.
Hidden energy sums exactly the nonconstant subsets of the hidden label set. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Counting hidden subsets by cardinality gives the exact positive-degree binomial sum, including an empty hidden label set. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The revealed energy is the remainder after the exact hidden-degree sum. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The positive-degree factor used by the restricted allocation sum is exactly hidden row energy, with the zero-degree allocation excluded. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.RowReferenceDomination 15 declarations The finite reference mixture controls each row likelihood, including the zero-density set.
Domination of translated rows by their reference law
The finite reference mixture controls each row likelihood, including the zero-density set. These bounds justify the finite integrals in the hidden-allocation roadmap.
Each component of the uniform reference mixture is bounded by its number of components times the mixture density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The row likelihood is nonnegative and bounded on the entire real line, with the conventional zero value at a zero of the reference density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Multiplying the likelihood by the reference recovers the component density even on the zero-density set. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each translated row law is bounded by a finite multiple of the reference law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The reference law dominates every sign-conditioned translated row law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reweighting the reference by the bounded row likelihood gives the exact translated law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A normalized reference density defines a probability law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each translated component is a probability law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact bounded likelihood integrates to one under the reference law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent rows with arbitrary fixed sign vectors are dominated by the independent reference responses. This does not replace the constrained allocation by independent signs. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A product of row likelihoods is bounded by the product of their finite row bounds. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A finite product of the total row likelihoods is measurable, including at reference zeros.
Formal statement
Proof (Lean source)
A fixed-allocation likelihood is integrable under the independent reference responses. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Fixed-allocation likelihoods have finite second moments under the reference law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The product likelihood remains normalized because its reference responses are independent. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.RowRevealEnergy 17 declarations Splits the nonconstant Walsh energy by whether a source subset contains a revealed label.
Revealed and hidden row energies
Splits the nonconstant Walsh energy by whether a source subset contains a revealed label. Under independent source reveals, the expected revealed energy is at most the reveal probability times the order-weighted channel energy.
Nonconstant energy attached to a labeled source subset; the empty subset is excluded.
Energy of source subsets containing at least one actually revealed label.
Energy of nonempty source subsets containing only hidden labels.
Each source subset contributes nonnegative energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Counting subsets by cardinality recovers the total nonconstant channel energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Revealed and hidden subsets partition the full nonconstant row energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both parts are nonnegative, and hidden row energy is bounded by total energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A subset of independently revealed source labels is hit with its exact OR probability. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact mean of a subset's reveal indicator. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The elementary union bound controls a subset's probability of containing a reveal. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent source reveals give exactly the cardinality-weighted revealed row energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Counting source subsets by order gives the exact revealed-energy mean from the roadmap. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Counting order-weighted subset energies recovers the weighted Walsh channel energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The expected revealed row energy is at most reveal probability times weighted energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mean hidden energy is the complement of the mean revealed energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mean hidden row energy lies between zero and total channel energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independent row reveals factor the energies of disjoint active revealed and hidden row sets, giving the product bound in the contraction roadmap. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ScoreAudit 1 declarations Exact audit score moments
Exact audit score moments
Unbiasedness, the exact assignment-audit variance identity, and the explicit oracle bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.ScoreMean 12 declarations Assignment moments and conditional audit means
Assignment moments and conditional audit means
The assignment law is a probability measure. the stated conclusion holds.
Formal statement
Proof (Lean source)
Every real statistic on the finite assignment space is integrable. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A half-Bernoulli centered sign has mean zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Pairing a treatment indicator with a sign isolates its own coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A row outcome paired with a sign has half its corresponding additive coefficient. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Orthogonal sign moments identify the oracle score's constant term with the causal target. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The audit product is a probability law at admissible retention. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every real audit statistic is integrable on the finite audit space. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mean of a single numeric audit mark is its retention probability. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional on assignment, the retained-neighbor sign sum has mean q times the true sum. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Inverse inclusion weighting recovers the oracle score's conditional mean. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete-record inverse-inclusion score is unbiased under the three design atoms. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.SuppliedBlockRisk 10 declarations The translated full-record laws at the bounded testing amplitude give the unrestricted randomized minimax converse through the two-prior testing inequality.
Supplied-block risk assembly
The translated full-record laws at the bounded testing amplitude give the unrestricted randomized minimax converse through the two-prior testing inequality.
The roadmap amplitude, expressed using the square root of the risk scale.
The testing amplitude is positive, admissible, and has exactly the required squared scale. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The genuine original-record distance at the roadmap amplitude is at most one fiftieth. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Support, full-record testing distance, and coverage yield the supplied-block risk scale. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Hard-coding a graph makes a supplied-graph estimator a measurable original-record rule.
Definition (Lean source)
On a schedule with the hard-coded graph, the original and supplied squared risks agree. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A constant-target, fixed-graph prior's hard-coded risks are bounded by supplied worst risk. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The common deterministic complete-block graph allows testing against supplied worst risk. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The unchanged support, distance, and algebra certify supplied-graph minimax risk. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The same lower bound holds for the entire original record and for that record with the true graph additionally supplied. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.SymmetricConditionalLikelihood 4 declarations The uniform original-label allocation average is replaced by its exact binomial-weighted symmetric polynomial.
Conditional likelihood with symmetric hidden polynomials
The uniform original-label allocation average is replaced by its exact binomial-weighted symmetric polynomial. The full graph and assignment marginal and all reference-zero endpoints remain those of the actual experiment.
The posterior response density using exact binomial-weighted symmetric hidden polynomials, extended by zero at incompatible graphs and reference-density zeros.
Definition (Lean source)
The symmetric hidden-subset expansion gives the full actual response density, including every zero-density endpoint. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.SymmetricSignPolys 3 declarations Symmetric hidden-sign polynomials
Symmetric hidden-sign polynomials
Symmetric sign polynomial on a Boolean slice.
Products of independent centered signs form an orthonormal family. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
When both polynomial degrees do not exceed the ambient dimension, their Bernoulli inner product is the reciprocal binomial coefficient when the degrees agree and zero otherwise.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.TreatedCompletionCounting 8 declarations Splitting the original hidden labels into treated and untreated subtypes gives exact multiplicities of completed row treatment counts.
Treated-label fibers of compatible completions
Splitting the original hidden labels into treated and untreated subtypes gives exact multiplicities of completed row treatment counts.
Row counts on the treated original labels of a finite word.
Definition (Lean source)
Splitting a row into treated and untreated labels preserves its full cardinality. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A fixed treated-count fiber splits bijectively into words on treated and untreated original labels. No label permutations are identified or discarded.
Definition (Lean source)
Counts across rows exhaust the treated original labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The fixed treated-count fiber has the product of the two multinomial counts. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The treated-count fiber multiplicity relative to all labeled words is the hypergeometric weight, including zero treated or zero hidden labels. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The completed row counts are bounded by their row capacities.
Definition (Lean source)
Averaging any function of the completed treated counts over labeled words gives exact hypergeometric weights. This is the finite posterior averaging identity. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.TwoPriorRisk 6 declarations Full original-record two-prior risk reduction
Full original-record two-prior risk reduction
Joint measurability of the record channel makes its component laws measurable.
Formal statement
Proof (Lean source)
A measurable mixture of probability record channels is a probability law. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Prior averaging of a constant-target family's seeded squared risk is bounded by the worst fixed-schedule risk. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each sign error costs at least the squared target amplitude, also for infinite risk. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Threshold testing of two opposite targets bounds any common upper bound on their risks. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Opposite constant-target priors give the full-record lower bound for every measurable seeded estimator. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.UniformHiddenSelection 7 declarations Average selected hidden slots over original-label permutations, keeping the capacity-constrained posterior rather than independent row allocations.
Uniform hidden-subset averaging
Average selected hidden slots over original-label permutations, keeping the capacity-constrained posterior rather than independent row allocations.
Averaging a finite transitive group orbit gives the uniform average on its target. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A selected set transported by a uniform label permutation is a uniform subset of its original cardinality, including the empty-set endpoint. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniformly permuting the labels of a fixed row allocation averages every selected slot family to the uniform subset with the same total degree. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.WalshChannelBasics 40 declarations Walsh expansion and channel energy estimates
Walsh expansion and channel energy estimates
A single-row shifted baseline density for a fixed Boolean sign vector.
Definition (Lean source)
The uniform average of all sign-vector row densities.
The permutation-symmetric Walsh likelihood coefficient, zero when the reference density vanishes.
Definition (Lean source)
The squared Walsh coefficient integrated against its reference density.
Definition (Lean source)
The total nonconstant Walsh channel energy.
The order-weighted nonconstant Walsh channel energy.
Each sign-conditioned response density is a normalized translated baseline. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
All sign-conditioned densities and their uniform average are nonnegative. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The reference density integrates to one, since there are exactly two-to-d sign vectors. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At a zero of the reference density every component density also vanishes. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The degree-zero coefficient equals one wherever the reference density is positive. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing a nonempty sign character over the full Boolean cube gives zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Multiplication by the reference density cancels the coefficient's denominator, including at zero-density points where all component densities vanish. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every nonconstant Walsh coefficient has reference-weighted integral zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Squared Walsh coefficients have nonnegative reference-weighted energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Weighting each nonconstant degree by its positive order increases the energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Relabeling coordinates preserves the row likelihood and transports its sign character. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Equal-size subsets have the same Walsh coefficient, by extending a subset bijection into a coordinate permutation. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The canonical first-s coordinates have cardinality s for every s at most d. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On positive reference density, the symmetric coefficient agrees with the coefficient of any subset of the specified size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The likelihood has its finite permutation-symmetric Walsh expansion. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The global square-root Lipschitz bound controls the squared difference of baseline densities, including points crossing the boundary of their support. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reversing one Boolean sign changes the row's sign sum by twice that sign. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The single-sign flip estimate used in the order-weighted Walsh energy proof. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reversing one coordinate permutes the Boolean cube, so it preserves the density sum. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Averaging the single-coordinate differences cancels the reference denominator. At zero reference density every summand is zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The row's centered sign sum is bounded by its number of coordinates. For the stated data and conditions, the stated conclusion holds.
Proof (Lean source)
All shifted row densities vanish outside the common enlarged baseline support. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The reference density has the same common compact support as its shifted components. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The averaged squared density difference under a single coordinate reversal.
Definition (Lean source)
The averaged flip energy is nonnegative, including at zero reference density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A translated baseline row is measurable across the support boundary.
Formal statement
Proof (Lean source)
A finite average of the measurable row densities is measurable.
Formal statement
Proof (Lean source)
The averaged flip energy is measurable despite division at reference-density zeros.
Formal statement
Proof (Lean source)
The pointwise flip estimate is dominated by a constant on the common support interval. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Compact support and the flip estimate supply integrability without an extra premise. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the flip bound costs only the support length, at most three quarters. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The sum of the integrated coordinate flips has the desired weighted-energy bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At zero amplitude the reference density is the unshifted baseline. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At zero amplitude all nonconstant Walsh coefficients vanish pointwise. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.WalshChannelEnergy 7 declarations Assembles finite Parseval, coefficient integrability, and the integrated flip bound.
Weighted Walsh channel energy
Assembles finite Parseval, coefficient integrability, and the integrated flip bound.
The order-weighted Walsh energy density equals one quarter of the total flip energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A Walsh likelihood coefficient has absolute value at most one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coefficient convention at zero reference density preserves measurability.
Formal statement
Proof (Lean source)
Squared coefficient densities are integrable, dominated by the normalized reference density. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating the finite weighted Parseval formula gives the channel's weighted energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At zero amplitude the order-weighted channel energy vanishes. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite permutation-symmetric Walsh expansion, centered coefficients, and weighted channel energy. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.Helpers.WalshParseval 7 declarations The Boolean delta kernel, inversion, and squared coefficient norm used in the channel energy proof.
Finite Walsh Parseval identities
The Boolean delta kernel, inversion, and squared coefficient norm used in the channel energy proof.
The sum of products of two sign characters is the Boolean-cube delta kernel. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite Walsh inversion follows by summing the Boolean delta kernel. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The squared Walsh coefficients sum to the uniformly averaged squared response. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Flipping one Boolean coordinate negates exactly the characters that contain it. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A coordinate flip multiplies each finite Walsh coefficient by its character sign. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Parseval for a coordinate difference retains only Walsh subsets containing that coordinate. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing coordinate differences weights each squared coefficient by its subset size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.TBlockTestingScale 11 declarations Uniform nonlocal original-record testing scale
Uniform nonlocal original-record testing scale
The nonlocal testing scale is positive and at most one. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The chosen testing amplitude is in the baseline channel's declared domain. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The testing scale bounds the source-retention energy without dividing by zero. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Walsh energy at the testing amplitude is small, both per row and after retention weighting. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The numerical exponential and geometric factors leave a chi-squared budget below one sixteenth. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The hidden-allocation contraction theorem, with its numerical premise discharged by Walsh energy, bounds the good-event chi-squared integral at the chosen amplitude. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A genie bound closes the high-retention regime of the testing proof. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The same genie bound closes every retention level with fewer than thirty-two sources. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Above twice the unclipped testing scale, the reverse bound excludes an amplitude from the set whose total variation is at most one half. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Small-distance membership and the reverse bound give both endpoints of the testing radius; no monotonicity of total variation in amplitude is required. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The all-degree complete-record testing bound, reverse bound, and two-sided testing radius. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.TFrontierAnswer 1 declarations Explicit precision frontier answer
Explicit precision frontier answer
Explicit-constant precision answer and the necessary and sufficient consistency criteria. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.TNonlocalTestingAnswer 1 declarations Nonlocal testing answer
Nonlocal testing answer
The original block family attains its nonlocal radius, with the explicit degree-two scale. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.TObservableUpper 4 declarations Observable total upper bound
Observable total upper bound
Ignoring the independent seed reduces squared loss to the original design integral. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Projection onto the target interval cannot increase squared error. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The audit-score moments and bounded outcomes give the unclipped squared-risk envelope. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The total observable upper rule attains the envelope, including zero retention. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.TObservedRecordPrecisionFrontier 3 declarations Complete original-record precision frontier
Complete original-record precision frontier
The total observable frontier estimator attains the explicit upper constant through the audit-score envelope and the reveal-probability comparisons. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The displayed explicit constants establish the risk bounds, consistency criterion, endpoint identities, and interior-retention comparison.
Formal statement
Proof (Lean source)
There exist positive universal constants c and C0 giving the stated risk sandwich; consistent estimators exist exactly when both asymptotic scale conditions hold; the frontier scale equals 1 at zero retention and min 1 (d²/n) at full retention; and positive universal comparison constants c1 and C1, independent of n, d, and q, bound the frontier by the stated interior-retention scale.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_ThinnedgraphAdditiveRiskFrontier_Research.TSupportedBoundaries 4 declarations Supported boundary regimes
Supported boundary regimes
Enlarging the schedule degree class cannot reduce minimax risk. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The degree-one testing frontier dominates the reciprocal audit sample size. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The degree-one observable envelope gives the reciprocal audit upper bound. For the stated data and conditions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Universal lower bound and the zero-retention, known-graph, and degree-one boundary sandwiches. the stated conclusion holds.