Formalization: Treatment Effect Estimation with Auxiliary Records and Diminishing Overlap
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. Note: this index was generated at a different commit than the paper's audited pin (70df51f) — statements may have moved since the audit.
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Basic 61 declarations Finite two-channel ATE experiment and its rare-overlap frontier.
Finite two-channel ATE experiment and its rare-overlap frontier.
Complete record with binary treatment and outcome.
An auxiliary record retains covariates and treatment without the outcome.
The unknown observable population is a PMF on complete-record atoms.
The simplex carries its coordinate Borel sigma algebra.
Definition (Lean source)
For a finite covariate dimension and an observable population law, the observed-data sampling law is the probability measure represented by that law's PMF.
Definition (Lean source)
The real mass of one complete-record atom is read from the population PMF.
Covariate masses sum the complete-record probabilities over both binary coordinates.
Arm-cell masses sum the two possible outcome marks.
The outcome-marked mass is the probability of a success in the specified arm and cell.
The occupied-cell treatment probability uses the arm-to-cell ratio; null cells use one half.
Outcome regression is the success-to-arm ratio, with zero on null arm cells.
Definition (Lean source)
Marginal PMFs carry the Borel sigma algebra of their real atom-mass coordinates.
Definition (Lean source)
The auxiliary PMF is the actual treatment-covariate projection of the observed law.
Definition (Lean source)
The ordered complete records have the iid product probability law.
Definition (Lean source)
The ordered auxiliary records have the iid law of the actual treatment-covariate marginal.
Definition (Lean source)
For the complete-sample size, the auxiliary-sample size, and the covariate dimension, the experiment's sample space consists of an ordered complete-record array paired with an ordered auxiliary-record array.
The two ordered iid arrays are independent and share the population marginal.
Definition (Lean source)
The randomization seed is uniform on the closed unit interval.
Original-record rules are jointly measurable and take values in the closed interval from minus one to one.
Definition (Lean source)
A data-only statistic becomes a randomized-domain rule by ignoring the independent seed.
Both arm probabilities exceed the public floor on occupied cells.
Definition (Lean source)
The sample law is the canonical independent product of the two channels.
Definition (Lean source)
Under the stated inputs and conditions, The canonical experiment realizes the structural independent-sampling atom.
Formal statement
Proof (Lean source)
For a covariate dimension, an overlap floor, and a population law, the model class is the proposition that the law satisfies the occupied-cell overlap condition.
Definition (Lean source)
A model law pairs its population PMF with occupied-cell overlap membership.
Definition (Lean source)
The signed ATE sums cell mass times the treated-minus-control conditional outcome mean.
Definition (Lean source)
Under the stated inputs and conditions, Every observable atom has nonnegative real mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Arm masses are nonnegative, including on null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Covariate masses are nonnegative. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Binary outcome regressions lie in the unit interval, with zero on null arms. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The covariate masses exhaust the population probability. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The observable signed contrast lies between minus one and one, including null cells.
Formal statement
Proof (Lean source)
Squared-error risk integrates over both sample channels and the independent uniform seed.
Definition (Lean source)
Worst-case squared-error risk takes the supremum over the overlap model class.
The original-experiment minimax risk infimizes worst-case risk over clipped Borel randomized rules.
A full atom augments the observed record with binary control and treated potential outcomes.
A potential-outcome law is a PMF on all five coordinates.
The real probability of a full potential-outcome atom is read from its PMF.
Definition (Lean source)
Marginal potential-outcome atom masses sum out the factual outcome.
A full law induces its observed complete-record marginal by coordinate projection.
Definition (Lean source)
The causal contrast is the finite expectation of treated minus control potential outcome.
Full atoms with factual outcome different from the selected potential outcome have zero mass.
Definition (Lean source)
The joint potential-outcome pair is independent of treatment given covariates, including null cells.
Exact auxiliary tables use the product Borel space of real coordinate masses.
The supplied side-information table is read from the actual auxiliary marginal PMF.
Definition (Lean source)
Exact-table rules are jointly Borel in complete records, the supplied table, and the seed, with clipped output.
An exact-table rule receives the true population marginal in its squared-error risk.
Definition (Lean source)
The exact-marginal minimax benchmark infimizes worst-case risk over all clipped jointly Borel rules.
Rare-label information is the complete-record budget multiplied by the overlap floor.
The logarithmic diagnostic is the natural logarithm of exp one plus rare-label information.
The rare-label benchmark caps the inverse rare-label information at one.
Definition (Lean source)
The fixed-overlap benchmark combines inverse labeled size with the squared annotation approximation term.
The four-index frontier caps the sum of inverse rare-label scale and the squared marginal approximation ratio.
Under the stated inputs and conditions, The evaluated frontier is strictly positive on the public experiment domain.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The evaluated frontier is capped at one.
Formal statement
Proof (Lean source)
Allowed public indices; scalar ranges are not additional model fields.
An experiment sequence is an arbitrary sequence of allowed public indices.
Definition (Lean source)
The risk of a public index evaluates the canonical original-experiment minimax value.
Definition (Lean source)
The consistency phase consists of sequences with minimax risk tending to zero.
Definition (Lean source)
The oracle phase requires diverging rare-label information and an eventually bounded risk-to-benchmark ratio.
Definition (Lean source)
Strict auxiliary improvement means risk divided by the supervised risk tends to zero.
Definition (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.AtomHistogram 20 declarations Singleton factorization and structural zero support for the original raw atom histograms, connecting the embedded count experiment to independent atom counts.
Singleton factorization and structural zero support for the original raw atom histograms, connecting the embedded count experiment to independent atom counts.
Independent atom counts in both original raw channels.
Definition (Lean source)
Under the stated inputs and conditions, Raw complete counts have no positive control outcomes. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Outside the rare cells, all complete positive outcome atoms are structural zeros. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Labels beyond the reservoir have zero complete and auxiliary raw mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Singleton probabilities of the full original histogram factor over all atoms. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A zero-intensity atom contributes one exactly at count zero. This gives the stated result.
Formal statement
Proof (Lean source)
The six atom factors at a single original covariate label.
Definition (Lean source)
Under the stated inputs and conditions, Grouping by label preserves every original complete and auxiliary atom. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every unused label contributes only deterministic zero counts. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A finite label product with unit tail consists of its rare prefix and reservoir. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, At a rare label the original atom factors are exactly its five-coordinate law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, At the reservoir label the original atom factors retain both channels and arms. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Supported histogram singleton probabilities agree in both count constructions. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A nonzero count at a zero complete intensity makes the whole atom mass zero. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A nonzero count at a zero auxiliary intensity makes the whole atom mass zero. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Unsupported histograms have probability zero also in the independent atom law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The embedded conditional law equals the full independent raw atom histogram law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The selected reservoir fits inside the original public alphabet. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The conditional histogram is exactly the normalized random-scale atom count law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Ordering the actual conditional histogram gives precisely the two independent normalized iid channels at their shared random scale. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.AtomLaw 5 declarations Exact raw atom intensities for the rare-cell and reservoir factors, and identification of the normalized random-scale independent atom count laws.
Exact raw atom intensities for the rare-cell and reservoir factors, and identification of the normalized random-scale independent atom count laws.
Under the stated inputs and conditions, The five independent coordinates of a rare cell have exactly the raw complete and auxiliary atom intensities at its original label. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The independent reservoir coordinates have the same raw atom intensities in both hypotheses, including the full auxiliary arm marginal. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Scaling the normalized complete atom law by its random total gives the independent Poisson product at the original raw complete intensities. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Scaling the normalized auxiliary law by the same total retains both arm marginals and gives the independent Poisson product at their raw intensities. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Uniformly ordering the independent raw atom counts recovers the two independent normalized iid Poisson channels at their actual random totals. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.CellPredictive 14 declarations The actual finite core/filler mixture for one rare cell in the raw Poisson experiment, with singleton readback and exact signed outcome cancellation.
The actual finite core/filler mixture for one rare cell in the raw Poisson experiment, with singleton readback and exact signed outcome cancellation.
The four counts retain both treated outcome marks, auxiliary treated counts, and the combined control count. The filler has zero treated outcome mean.
Definition (Lean source)
Each conditional raw cell law is a probability measure.
Definition (Lean source)
Mix the conditional raw count law over the specified finite latent PMF.
Definition (Lean source)
The finite latent mixture has total mass one.
Definition (Lean source)
Under the stated inputs and conditions, Singleton masses of the finite mixture are the finite weighted sums of conditional singleton masses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The filler is identical under the two hypotheses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, On core atoms, a nonzero treated count in one outcome channel has the signed polar discrepancy times the three unmarked Poisson singleton masses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Mixing the core atoms cancels the filler and restores the signed certificate weights. This is the measure-level signed identity behind equation (6). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, With no complete treated observations, both core hypotheses have the same likelihood, including the shared auxiliary and control counts. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, With zero treated complete counts, the predictive singleton masses agree. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Deterministic marks forbid a positive count in both complete treated outcome channels, under every core or filler draw. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Mixed positive complete treated outcome counts have zero predictive mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The three independent unmarked Poisson singleton masses give the exponential times powers likelihood in equation (6). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The actual predictive discrepancy at either nonzero deterministic outcome pattern is exactly the signed count kernel from equation (6). This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.CellTV 6 declarations Absolute singleton discrepancy bounds for the actual core/filler rare-cell predictive measures, connecting their likelihoods to the signed Taylor envelope.
Absolute singleton discrepancy bounds for the actual core/filler rare-cell predictive measures, connecting their likelihoods to the signed Taylor envelope.
Under the stated inputs and conditions, Either deterministic marked pattern has the same absolute signed discrepancy. The core/filler likelihood is read back before taking the absolute value. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The actual one-cell predictive singleton discrepancies are absolutely summable, and their sum over one deterministic mark pattern has equation (7)'s bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, At the paper's tuning the K-cell budget for actual marked-pattern singleton discrepancies is strictly below one sixty-fourth. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The two disjoint deterministic mark patterns exhaust the predictive discrepancy; null treated counts and mixed positive marks contribute zero. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The actual rare-cell predictive total variation is bounded by the signed Taylor tail, retaining both observed channels and the core/filler mixture. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The tuned sum of rare-cell total variation bounds is below the paper's one-sixty-fourth budget. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Certificate 2 declarations The shrinking-cone dual as a normalized atomic signed-moment certificate.
The shrinking-cone dual as a normalized atomic signed-moment certificate.
Retain the nodes, weights, and matching moments of the paper's dual witness.
Definition (Lean source)
Under the stated inputs and conditions, The certificate variation is supported on the original shrinking cone. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Concentration 18 declarations Exact normalized target readback and the deterministic error decomposition used for affine prior concentration.
Exact normalized target readback and the deterministic error decomposition used for affine prior concentration. The filler, reservoir, and null cells contribute zero target.
The raw target is the sum of the treated rare-cell contributions.
Definition (Lean source)
Under the stated inputs and conditions, Every control mean is zero, including the reservoir and null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Rare treated means are exactly their assigned binary marks; other means vanish. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The normalized ATE is precisely the raw target divided by the common total mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The raw target lies between zero and the shared normalizer. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both normalized affine targets lie in the unit interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Normalization separates the raw target error from the total-mass error exactly. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The squared normalized error is controlled by the raw target and normalizer errors. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Finite latent product expectations of additive statistics equal K times their cell mean. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Expected raw targets are K times their one-cell expectations. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Independence lifts the signed one-cell gap to the expected raw targets. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Independence makes the variance of any additive finite latent mark exactly K-fold. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The raw target variance is bounded using its one-cell second moment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The common normalizer has expectation exactly one under the latent product prior. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The normalizer variance is at most four thirds K B alpha. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The normalized target's mean squared error about its raw mean has the roadmap bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Markov's inequality turns the normalized target MSE into a two-sided tail bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The two affine target priors have the roadmap's gap-relative concentration bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.ControlSplit 18 declarations The common binomial reconstruction of combined control counts into the two original channels, with exact independent-Poisson likelihood readback.
The common binomial reconstruction of combined control counts into the two original channels, with exact independent-Poisson likelihood readback.
Under the stated inputs and conditions, Splitting a combined Poisson count by the channel intensity ratio gives exactly the two independent channel likelihoods. This gives the stated result.
Formal statement
Proof (Lean source)
Conditional channel split of a combined control count.
The split law is a probability law for every combined count.
Definition (Lean source)
Under the stated inputs and conditions, A split singleton has nonzero likelihood only at the matching total. This gives the stated result.
Formal statement
Proof (Lean source)
The channel split is a common Markov kernel, independent of latent masses and of the hypothesis's outcome marks.
Definition (Lean source)
Each control reconstruction has total mass one.
Definition (Lean source)
Under the stated inputs and conditions, Applying the common control split to a combined Poisson count recovers both independent Poisson control channels, without dropping either channel. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Keeping independent existing coordinates while splitting a control count preserves their laws and restores the independent channel controls. This gives the stated result.
Formal statement
Proof (Lean source)
Reconstruct the full rare-cell control channels while keeping both complete treated outcome counts and the auxiliary treated count.
Definition (Lean source)
Full rare-cell control reconstruction is a common probability kernel.
Definition (Lean source)
Under the stated inputs and conditions, Independent coordinate reconstruction commutes with the product law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Splitting an actual conditional rare-cell law restores the independent complete and auxiliary control counts, while leaving all treated counts intact. This gives the stated result.
Formal statement
Proof (Lean source)
The conditional rare-cell law with separate controls in the original two channels. All five potentially nonzero atom counts are retained.
Definition (Lean source)
The full conditional cell law has total mass one.
Definition (Lean source)
The actual core/filler predictive law with control channels restored.
Mixing full conditional cell laws gives a probability measure.
Definition (Lean source)
Under the stated inputs and conditions, The common channel reconstruction identifies the actual full core/filler predictive law, rather than merely bounding an abstract postprocessing. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Restoring both control channels preserves the calibrated joint TV budget for the independent product of the actual full rare-cell mixtures. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.CountEnvelope 18 declarations Countwise nonnegative polynomial envelopes for equation (6), the shifted labeled factorial comparison, absolutely convergent coefficientwise count sums, and exact cancellation of the common control baseline.
Countwise nonnegative polynomial envelopes for equation (6), the shifted labeled factorial comparison, absolutely convergent coefficientwise count sums, and exact cancellation of the common control baseline.
Under the stated inputs and conditions, Products of nonnegative affine powers have nonnegative Taylor coefficients. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each count kernel is bounded by positive coefficients with only total degrees above the matching degree retained, including counts exceeding that degree. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The shifted exponential tail is exactly the series filtered by total degree. This form retains the cancellation cutoff when polynomial and count sums are exchanged. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The signed count kernel has a nonnegative envelope filtered by total degree, ready for exchanging the polynomial, exponential, and count sums. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Shifting the labeled count by one decreases every nonnegative factorial term. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The labeled Palm count series is dominated by the ordinary exponential series. This gives the stated result.
Formal statement
Proof (Lean source)
The positive count generating functions cancel the entire common baseline, so their envelope contains only twice the latent intensity.
Formal statement
Proof (Lean source)
The binomial coefficient of an affine arm power, including zero slopes.
Formal statement
Proof (Lean source)
After shifting by the coefficient degree, a count term separates into a fixed slope coefficient and an ordinary exponential term.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each fixed affine Taylor coefficient is absolutely summable over the Poisson count. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing a fixed Taylor coefficient over all counts reads back the affine exponential exactly; the common constant is retained rather than bounded. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The finite convolution of two exponential Taylor coefficients is the coefficient for the sum of their slopes. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The two independent arm-count sums exchange with the finite coefficient convolution and retain their common constant exactly. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The Palm shift in the labeled count decreases each coefficient of the nonnegative two-arm polynomial envelope. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing the combined treated and control counts cancels the common baseline at every coefficient, without any bound on its size. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Convolving the coefficientwise count sum with the positive Taylor series of exp(Mv) leaves exactly the coefficients of exp(2Mv). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Grouping the labeled and auxiliary treated counts by their sum gives the ordinary combined-intensity coefficient; the polynomial power is unchanged. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, At the support endpoint, the full coefficientwise count envelope has exactly the Taylor tail used in equation (7). No common baseline enters the bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.CountSummation 8 declarations Absolutely convergent count sums and the Palm-shifted coefficient envelope for one rare cell.
Absolutely convergent count sums and the Palm-shifted coefficient envelope for one rare cell. These bounds retain the common control baseline exactly.
Under the stated inputs and conditions, Absolute convergence justifies regrouping the two count indices at any fixed Taylor coefficient. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The labeled Palm shift preserves absolute convergence of the joint count sum. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, After summing both counts, the Palm-shifted coefficients are dominated by those of the ordinary two-arm exponential. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, When treated channels have been combined, the Palm envelope cancels the common baseline, coefficient by coefficient. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Absolute convergence of both treated channels remains valid after multiplying by a fixed control-count polynomial. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Regrouping the complete and auxiliary treated counts gives intensity u+w, with every fixed control count retained. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The labeled factorial shift decreases the joint treated-channel coefficient sum, while retaining the entire control-count polynomial. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The three count indices have the coefficient envelope asserted in equation (7): the two treated intensities combine, and the baseline cancels exactly. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.CountTail 4 declarations Exchange of the count-summed coefficient envelope with the positive exponential series.
Exchange of the count-summed coefficient envelope with the positive exponential series. The total-degree cutoff reads back the one-cell Taylor tail without a bound on the common control baseline.
Under the stated hypotheses, The positive two-series envelope is absolutely summable even after the matching-degree cutoff is imposed. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Regrouping the two positive exponential series by total degree gives the Taylor tail of exp(2z), retaining precisely the degrees above L. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Any nonnegative coefficient envelope dominated by the baseline-canceled Poisson coefficients has total-degree tail at most that of exp(2MB). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (7)'s count-summed Taylor envelope is bounded by the one-cell exponential tail. Both treated channels and all control counts are retained. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.FixedExperiment 18 declarations The tagged affine parameter's original fixed experiment, exact ordered prefix retention with its independent seed, and the conditional and predictive failure budgets.
The tagged affine parameter's original fixed experiment, exact ordered prefix retention with its independent seed, and the conditional and predictive failure budgets. These are the experiment leaves for the final minimax transfer.
The complete mark kernel retains the hypothesis and its latent vector.
Definition (Lean source)
The auxiliary mark kernel is the full normalized arm marginal.
Definition (Lean source)
Every complete mark law is a probability measure.
Definition (Lean source)
Every auxiliary mark law is a probability measure.
Definition (Lean source)
The unseeded tagged raw experiment has the actual ordered conditional laws.
Definition (Lean source)
The ordered tagged raw laws are probability measures.
Definition (Lean source)
The fixed experiment keeps both full original ordered arrays.
Definition (Lean source)
The fixed tagged experiment satisfies the exact unequal two-pool interface.
Formal statement
Proof (Lean source)
Retaining the hypothesis tag changes neither scaled intensity nor mark law.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Exact retention on joint success gives the original fixed data law times its success probability, for every parameter rather than merely on average. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The same exact retention identity keeps the independent uniform seed. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Conditional count failure fits the half-gap budget for every raw table. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Integrating the uniform tablewise budget gives the same predictive budget under either tagged prior; no low-scale exception is needed. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The independent seed has unit mass, so it adds no count failure. This gives the stated result.
Formal statement
Proof (Lean source)
A randomized original rule uses the first requested records when both prefixes exist, and returns zero on failure, keeping the same seed.
Definition (Lean source)
Under the stated inputs and conditions, Prefix transfer preserves joint Borel measurability with the seed. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Prefix transfer preserves the clipping constraint, including on failure. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, For each actual normalized table, successful ordered retention pays exactly its fixed-experiment risk; zero fallback costs at most the count-failure mass. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.FixedRisk 9 declarations Real and extended squared-risk readback for clipped original-experiment rules, and the affine prior's fixed-size minimax assembly.
Real and extended squared-risk readback for clipped original-experiment rules, and the affine prior's fixed-size minimax assembly.
Under the stated inputs and conditions, Clipping the action and target bounds squared loss by four. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The bounded measurable squared loss is integrable under the original experiment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The original real risk agrees with the extended nonnegative loss integral. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every clipped original rule has nonnegative risk bounded by four. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A legal table's risk is dominated by the bounded real worst-case supremum. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Averaging the conditional transfer under either tagged prior preserves the worst-case bound and the half-gap failure budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The genuine raw Bayes bound and prefix transfer force each original clipped Borel rule to pay at least one one-hundred-twenty-eighth of the squared gap. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squaring the quantitative target separation gives the displayed affine rate, with the same numerical constant as the paper. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Taking the infimum over all original randomized Borel rules preserves the fixed-size affine lower bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Histogram 21 declarations Embedding the five rare-cell count coordinates and the four common reservoir counts into both original atom histograms, followed by uniform channel ordering.
Embedding the five rare-cell count coordinates and the four common reservoir counts into both original atom histograms, followed by uniform channel ordering.
Place rare-cell counts at their original labels, reservoir counts at label k, and zeros at unused labels. Complete control outcomes are always zero.
Definition (Lean source)
Both histogram channels are measurable functions of the finite count coordinates.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The five rare-cell coordinates occupy exactly their original complete and auxiliary atoms, with no positive complete control outcomes. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, All four reservoir coordinates are retained, and its complete outcomes are zero. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Labels beyond the reservoir contribute no counts in either channel. This gives the stated result.
Formal statement
Proof (Lean source)
The reservoir has independent zero-outcome complete and auxiliary counts in both arms, each with half the common reservoir mass.
Definition (Lean source)
The common reservoir count law has total mass one.
Definition (Lean source)
Embed the independent full rare-cell mixtures and the construction's common reservoir into the two complete atom histograms.
Definition (Lean source)
The embedded histogram mixture is a probability law in both channels.
Definition (Lean source)
Under the stated inputs and conditions, The embedded paired histogram experiment satisfies the full joint TV budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Uniform ordering independently restores both channels without increasing the distance of the embedded full count mixtures. This gives the stated result.
Formal statement
Proof (Lean source)
The conditional product of the five full cell coordinates over the actual latent vector, before adding the common reservoir.
Definition (Lean source)
Each full conditional product is a probability kernel.
Definition (Lean source)
Under the stated inputs and conditions, Mixing the full conditional cell products over independent core/filler latent draws gives exactly the product used by the histogram experiment. This gives the stated result.
Formal statement
Proof (Lean source)
Attach the actual common reservoir to the full conditional cell experiment.
Definition (Lean source)
The conditional full count law is a probability kernel.
Definition (Lean source)
Under the stated inputs and conditions, The independent reservoir factors out of the actual full latent mixture. This gives the stated result.
Formal statement
Proof (Lean source)
The concrete histogram embedding of the actual conditional full count law.
Definition (Lean source)
The conditional histogram embedding is a probability kernel.
Definition (Lean source)
Under the stated inputs and conditions, The histogram predictive law is the mixture of the actual conditional core/filler count embeddings, rather than an assumed identification. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The ordered, mixed conditional histogram experiment obeys the joint TV budget in the orientation used by the two-prior testing inequality. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.HistogramCoordinates 14 declarations The full histogram embedding is injective and its image consists precisely of histograms with zero counts at the structural zero atoms.
The full histogram embedding is injective and its image consists precisely of histograms with zero counts at the structural zero atoms. Singleton probabilities therefore reduce to the unique original rare-cell and reservoir count vector.
Read every rare-cell and reservoir coordinate from the original histograms.
Definition (Lean source)
Under the stated inputs and conditions, The full embedding loses none of the nine types of stochastic coordinates. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A full count vector is uniquely determined by its original atom histograms. This gives the stated result.
Formal statement
Proof (Lean source)
Structural zero coordinates of the two-channel raw affine experiment.
Definition (Lean source)
Under the stated inputs and conditions, Every embedded count vector vanishes at exactly the structural zero coordinates. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Reading and re-embedding any supported histogram returns that histogram. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The structural zero conditions exactly characterize the histogram image. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A supported histogram has precisely one preimage, the explicit coordinate readback. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Unsupported histograms have no preimage under the full embedding. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Singleton masses after embedding are explicit coordinate masses on the image, and zero off the image. This applies to conditional laws and to their mixtures. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The actual conditional histogram law is the pushforward of the full count law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The conditional histogram singleton mass is the unique original count mass; no untracked coordinates or histogram multiplicities remain. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Conditional full count singleton probabilities factor over the independent rare cells and the independent common reservoir. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A supported original histogram has the product probability of its read-back rare-cell counts and reservoir counts in the actual conditional experiment. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Membership 4 declarations Positivity and support of every normalized affine table under the common latent coupling.
Positivity and support of every normalized affine table under the common latent coupling.
Under the stated inputs and conditions, Every normalized affine atom is its raw mass divided by the common normalizer. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Summing the outcome marks leaves arm masses independent of the hypothesis. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The normalized cell mass is the sum of its two normalized arm masses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Reservoir and normalizer positivity, legal support, and pointwise common marginal are derived.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.NumericalConcentration 7 declarations Uniform numerical degree and rare-cell count estimates for concentration of the affine priors.
Uniform numerical degree and rare-cell count estimates for concentration of the affine priors.
Under the stated inputs and conditions, Half-scale exponential growth dominates the numerical linear budget above the threshold. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, Above label scale two, the scheduled logarithm is within one of the ordinary logarithm. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Above the affine threshold the polynomial degree is bounded by ten times log S. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The floor of the reciprocal mass budget retains at least 500 M ε L cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both alphabet and floor budgets exceed the square-root-scale count in the affine regime. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The scheduled cell count dominates the entire degree-dependent concentration budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each normalized affine target has bad-event probability at most 1/128. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.NumericalSeparation 5 declarations Uniform numerical target separation for the affine priors, as in equation (10).
Uniform numerical target separation for the affine priors, as in equation (10).
Under the stated inputs and conditions, The logarithmic scale is at least one for nonnegative overlap. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, The scheduled baseline mass is bounded below in terms of the public indices. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The floor cap retains at least half of its reciprocal mass budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The actual rare-cell mass budget dominates the clipped public affine scale. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The raw target mean gap has the uniform numerical scale claimed in equation (10). This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.NumericalTV 6 declarations Uniform numerical bound on the joint raw-mixture Taylor envelope in equation (8).
Uniform numerical bound on the joint raw-mixture Taylor envelope in equation (8).
Under the stated inputs and conditions, The scheduled Taylor argument is exactly the degree divided by 500. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The summed marked intensity is controlled by the capped rare-cell mass budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Degree calibration makes the label-scale weighted exponential tail uniformly tiny. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The full K-cell Taylor envelope is below the testing distance budget of 1/64. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The full three-count coefficient envelope, weighted by the K-cell marked intensity, meets the raw testing budget directly. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The K-cell sum of the absolute equation (6) signed masses meets the testing budget in equation (8), with no bound on the common control baseline. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.NumericalTransfer 4 declarations Numerical prefix-failure and squared-gap bounds for the fixed-size affine transfer.
Numerical prefix-failure and squared-gap bounds for the fixed-size affine transfer. These are the final numerical estimates following equations (10)--(12).
Under the stated inputs and conditions, Above unit label scale, the weighted failure envelope is bounded at scale one. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, The two prefix failures cost at most 10⁻²⁴ divided by the label scale. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, In the affine regime, the squared raw target gap dominates 10⁻²⁰/S. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Prefix failures consume at most half of the raw testing lower bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.OrderedExperiment 6 declarations The actual ordered random-scale experiment and its two-channel mixture distance, including the independent uniform seed used by randomized rules.
The actual ordered random-scale experiment and its two-channel mixture distance, including the independent uniform seed used by randomized rules.
Conditional on the latent table, both ordered channels have their normalized mark laws and independent Poisson totals at the shared raw scale.
Definition (Lean source)
The actual ordered experiment is a probability kernel.
Definition (Lean source)
Under the stated inputs and conditions, The exact normalized mark laws and raw normalizer instantiate the shared-scale experiment property required by the fixed-size transfer theorem. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The atom-histogram reconstruction equals the actual ordered conditional law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The distance budget holds for the actual normalized ordered random-scale experiment, retaining both original observation channels. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A common independent uniform seed preserves the ordered mixture TV budget. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.ProductExperiment 8 declarations Identification of the independent rare-cell predictive law with the mixture of conditional raw cell products over the construction's independent latent draws.
Identification of the independent rare-cell predictive law with the mixture of conditional raw cell products over the construction's independent latent draws.
Conditional independent raw count laws of the rare cells, before restoring control-channel splits and ordering the records.
Definition (Lean source)
Every conditional rare-cell product is a probability law.
Definition (Lean source)
Under the stated inputs and conditions, Mixing independent conditional raw cells over the actual latent product prior gives exactly the product of the actual core/filler predictive measures. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The raw rare-cell mixture itself inherits the joint one-sixty-fourth TV budget; the product identity eliminates any identification hypothesis. This gives the stated result.
Formal statement
Proof (Lean source)
Attach a common independent reservoir to the conditional rare-cell counts.
A probability reservoir preserves the conditional probability law.
Definition (Lean source)
Under the stated inputs and conditions, The common reservoir factors out of the actual finite latent mixture. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A common reconstruction channel, including control splits, ordering and a common random seed, preserves the TV budget of the mixed raw cells and reservoir. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.ProductTV 2 declarations Tensorization of the actual affine core/filler predictive measures.
Tensorization of the actual affine core/filler predictive measures. Independent rare cells obey the joint Taylor budget, and a common reservoir law adds no distance.
Under the stated inputs and conditions, The independent rare-cell product has total variation below one sixty-fourth. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Adding any common independent reservoir factor preserves the joint distance budget. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.RawBayes 9 declarations Two-prior testing for the actual ordered raw experiment.
Two-prior testing for the actual ordered raw experiment. A hypothesis tag retains its raw scale together with the latent vector, so the same parameter space can also be used by the random-scale fixed-size transfer.
The raw parameter retains the hypothesis and its finite latent draw.
Definition (Lean source)
The tagged prior draws the common latent vector with a fixed hypothesis.
Definition (Lean source)
Both tagged priors are probability measures.
Definition (Lean source)
The tagged experiment keeps both ordered channels and the independent seed.
Definition (Lean source)
Each tagged conditional law is a probability law.
Definition (Lean source)
Under the stated inputs and conditions, Mixing the tagged experiment reads back to the seeded ordered raw mixture. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The tagged normalized target has the paper's concentration budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The tagged Bayes risk is exactly the latent average of the actual seeded conditional squared risk; tagging changes no observation or loss. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Every randomized measurable rule in the actual raw experiment has a Bayes risk at least one sixty-fourth of the squared raw target gap. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.RawMass 10 declarations Nonnegative affine raw tables and their exact total mass before normalization.
Nonnegative affine raw tables and their exact total mass before normalization.
Under the stated inputs and conditions, Reciprocal tilting gives nonnegative core probabilities whose sum is at most one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The latent PMF has exactly the specified core and filler masses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The expected latent node is at most alpha divided by one minus the overlap floor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The latent second moment is bounded by the bandwidth times its first moment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The reservoir has mass greater than one half uniformly in all legal public indices. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Extending a finite cell table by zero preserves its total mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every raw affine atom is nonnegative, including the reservoir and null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing the raw table gives the shared reservoir-plus-cells normalizer. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Positive rare-cell masses preserve the reservoir lower bound on the normalizer. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Normalizing any finite nonnegative table divides each atom by its positive total. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.RawPoissonTV 11 declarations Moment cancellation and exact Taylor-remainder readback for the affine one-cell marked-Poisson kernel, together with its calibrated exponential tail bound.
Moment cancellation and exact Taylor-remainder readback for the affine one-cell marked-Poisson kernel, together with its calibrated exponential tail bound.
Under the stated inputs and conditions, The Taylor remainder at 2MB=L/500 is geometrically small in the degree.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every polynomial through the matching degree cancels against the cone dual. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The low-degree terms of the exponential times the two affine arm powers cancel. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Subtracting any canceled polynomial bounds the signed sum by its uniform remainder, using the dual's variation mass one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every retained Taylor term of the one-cell kernel has zero signed integral. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The signed one-cell exponential kernel equals its surviving Taylor remainder exactly. This removes all terms of total degree at most L before bounding absolute coefficients. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The absolute exponential remainder on the cone is bounded by its positive Taylor tail at the support endpoint; no bound on the common baseline is used. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Matching moments cancel the monomial times every retained exponential term. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A signed exponential monomial retains only terms above the matching total degree. The variation mass one bounds the remainder by its positive endpoint tail. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Without a matching-degree restriction, the full positive Taylor series still bounds the signed exponential monomial. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Polynomial coefficients give a total-degree Taylor envelope for the signed kernel. This preserves each monomial's cancellation degree before the count sums are exchanged. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Separation 7 declarations Signed reciprocal-certificate separation before reservoir normalization.
Signed reciprocal-certificate separation before reservoir normalization.
Under the stated inputs and conditions, The signed one-cell raw target gap is at least one twelfth of b0.
Formal statement
Proof (Lean source)
A single rare cell's raw contribution to the target, including the zero filler.
Definition (Lean source)
Under the stated inputs and conditions, Multiplying the polar sign by the absolute weight restores the signed weight. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The expected target difference is exactly the reciprocal signed functional. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The two hypotheses separate the expected one-cell raw targets by b0/12. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each raw cell target is between zero and the cell's total raw mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The cell target second moment has the bound used in the prior concentration step. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.SignedCountTail 6 declarations Absolute convergence and count-summed Taylor bounds for the signed rare-cell kernel.
Absolute convergence and count-summed Taylor bounds for the signed rare-cell kernel. These justify exchanging the count indices with the polynomial envelope.
Under the stated hypotheses, The coefficient majorant remains summable after attaching the matching-degree tail. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A family of nonnegative polynomial coefficients with summable columns and an exponential column bound has an absolutely summable signed-kernel envelope. Moment cancellation is applied to each polynomial before the count exchange. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The three original count indices are jointly absolutely summable at every fixed Taylor coefficient, including the Palm factorial shift. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The absolute signed equation (6) kernels, summed over all three counts, have precisely the equation (7) tail bound. The common baseline cancels before any bound is taken, and the convergence claim justifies the exchange. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Factoring the original signed count difference in equation (6) gives the Palm intensity times the kernel controlled by the count-summed Taylor bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The equation (6) signed masses are absolutely summable and their absolute sum obeys the equation (7) one-cell bound, with both channels retained. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Testing 4 declarations Normalized affine-prior concentration and the two-prior testing step in equation (11).
Normalized affine-prior concentration and the two-prior testing step in equation (11). The experiment-distance estimate is a separate input, to be proved for the raw experiment.
Under the stated inputs and conditions, The ATE is Borel measurable in the finite table of observable atom probabilities. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each normalized affine prior is a probability measure, including its zero filler. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Pushing forward the latent tail bound gives concentration for the actual law prior. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, With the raw-mixture distance budget, every measurable rule has Bayes risk at least one sixty-fourth of the squared affine target gap. This is equation (11). This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Transfer 8 declarations Raw-to-normalized likelihood and intensity readback for both channels, and the Poisson prefix-failure budgets for the random-scale two-channel transfer.
Raw-to-normalized likelihood and intensity readback for both channels, and the Poisson prefix-failure budgets for the random-scale two-channel transfer.
Under the stated inputs and conditions, Normalized complete-record atom masses read back to raw masses divided by the shared Q.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The auxiliary channel retains the full arm marginal of the raw table, divided by Q. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Multiplying the normalized complete-channel probabilities by the raw total recovers every complete Poisson intensity exactly. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The random-scale auxiliary pool has exactly the raw arm intensities, including all controls. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A Poisson pool with mean at least 64 times the requested size has the exponential prefix-failure bound in equation (12). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The complete raw pool has the uniform exponential prefix budget, since Q exceeds one half. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Retaining m auxiliary records costs at most the exponential budget calibrated to n+m. When m is zero, monotonicity still applies to the empty failure event. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The sum of the two actual Poisson failure probabilities fits the gap budget required by the fixed-size transfer. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Affine.Tuning 5 declarations Affine-prior public schedule and the shared raw total mass.
Affine-prior public schedule and the shared raw total mass.
Under the stated inputs and conditions, The affine schedule has uniform total-intensity, degree, and rare-cell mass bounds.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The baseline mass has the explicit reciprocal form used in the numerical bounds. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The bandwidth contribution to concentration equals the stated dimensionless scale. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, At label scale at least one, the affine schedule includes a rare cell. This gives the stated result.
Formal statement
Proof (Lean source)
For the complete-sample size, the auxiliary-sample size, the covariate dimension, the overlap floor, a cone-dual certificate, and the latent assignments of rare cells, the raw normalizer is the remaining reservoir mass after the affine rare-cell masses are assigned.
Definition (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.AffineTesting 5 declarations Support, common normalized marginal, and original-experiment affine-prior testing bound.
Support, common normalized marginal, and original-experiment affine-prior testing bound.
Under the stated inputs and conditions, The auxiliary marginal is Borel in the complete-record mass coordinates. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Coupling the same finite latent vector gives identical normalized marginal laws. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both affine hypotheses have legal support and the same marginal under the latent coupling. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, In the affine regime the selected prior handle preserves the common marginal law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The normalized affine priors have legal support and a common auxiliary-table distribution, and prove the all-rule lower bound. This gives the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Baseline 4 declarations Deterministic inverse-count baseline with independent two-pool prefix averaging.
Deterministic inverse-count baseline with independent two-pool prefix averaging.
The baseline prefix statistic clips the treated-minus-control inverse-count sum.
Definition (Lean source)
The inverse-count baseline averages valid two-pool prefixes and outputs zero on overflow or small sample sizes.
Definition (Lean source)
The baseline is measurable on the original finite sample arrays.
Formal statement
Proof (Lean source)
The total baseline takes values between minus one and one.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.BaselinePoissonRisk 7 declarations Squared-risk assembly for the inverse-count Poisson baseline and numerical pool bounds.
Squared-risk assembly for the inverse-count Poisson baseline and numerical pool bounds.
Under the stated hypotheses, Independent Poisson cell statistics have a square-integrable arm sum. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squared loss around any constant is variance plus squared bias. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The proved arm bias and variance bounds imply the uncapped squared-risk bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The clipped Poisson contrast has risk at most four times the arm envelope; independence between the two arms is unnecessary. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The baseline's two disjoint pools have the lower sizes required by the roadmap. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Zero on overflow adds at most two inverse label scales. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Substituting the pool intensities and absorbing overflow gives a numerical public-rate bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.BaselinePoolEncoding 19 declarations Exact identifications of the baseline's array block counts with ordered-prefix histograms.
Exact identifications of the baseline's array block counts with ordered-prefix histograms. These identities provide the deterministic count bridge for finite-pool risk transfer.
An ordered block is represented as a finite sample without changing its order.
Definition (Lean source)
Under the stated inputs and conditions, Histogram counts of an ordered block equal the corresponding array filter counts. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The baseline's complete-record block counter is the exact ordered-block histogram. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The baseline's auxiliary block counter is the exact ordered-block histogram. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A histogram can be evaluated as a sum of unit contributions over array positions. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Concatenating two arrays adds their histogram counts. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Projecting away the binary outcome adds the two outcome-marked counts. This gives the stated result.
Formal statement
Proof (Lean source)
The baseline's auxiliary prefix concatenates projected complete records and auxiliary records in precisely the order used by the array implementation.
Definition (Lean source)
Under the stated inputs and conditions, The concatenated auxiliary prefix has the requested length, including either empty part. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The baseline's pooled arm counter is exactly the histogram of its concatenated prefix. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The array baseline prefix statistic is exactly the clipped ordered-prefix statistic. The complete and auxiliary histogram identities retain every arm contribution. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Integrating a zero-overflow two-prefix statistic gives exactly the finite product of Poisson weights. No continuity or nonzero cell mass is needed. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The baseline's finite average is the expectation of its array prefix statistic with exactly zero output when either Poisson request exceeds its pool. This gives the stated result.
Formal statement
Proof (Lean source)
On the original arrays, either requested prefix overflow resets the baseline to zero.
Definition (Lean source)
Under the stated inputs and conditions, Every original-array capped statistic lies in the clipping interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Conditional Poisson averaging contracts the squared loss at every original array. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Conditional averaging also contracts squared risk under the original experiment's finite-data distribution. This step does not require a pool-law identification. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The independent uniform seed has no effect on the risk of the data-only baseline. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The original randomized-rule risk is bounded by the loss of the zero-overflow prefix statistic before averaging over its independent Poisson requests. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.BaselinePoolLaw 8 declarations Exact iid laws for splitting the complete-record array and concatenating its remaining treatment--covariate projections with the auxiliary array.
Exact iid laws for splitting the complete-record array and concatenating its remaining treatment--covariate projections with the auxiliary array.
Under the stated inputs and conditions, Splitting an iid array into its first and last blocks gives independent iid pools. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The split law also holds when the total capacity is expressed by an equal index. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Concatenating independent iid arrays of the same law gives one iid array. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Dropping the outcome from an iid complete-record block gives the iid marginal block. This gives the stated result.
Formal statement
Proof (Lean source)
The baseline pools preserve the original order: the first block is complete, and the second block concatenates the remaining projections and auxiliary records.
Extracting the two disjoint baseline pools is measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Under the original two-channel experiment, the extracted pools are independent with exactly the complete-record and treatment--covariate iid laws. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squared risk of a measurable statistic of the extracted baseline pools is exactly its risk in the independent fixed-pool experiment. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.BaselinePoolStatistic 7 declarations Deterministic identification of the array baseline with the fixed-pool prefix rule.
Deterministic identification of the array baseline with the fixed-pool prefix rule.
Under the stated hypotheses, Prefixing an appended array retains the first block followed by the required part of the second block, also when the prefix stops inside the first block. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The complete prefix of the extracted pool is the first original-array block. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The marginal prefix of the extracted pool is the prescribed projected block concatenated with the prescribed auxiliary block. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every valid original-array prefix computes the fixed-pool statistic exactly. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Overflow is zero in both implementations, and valid prefixes agree exactly. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The deterministic baseline is exactly the prefix average of its extracted pools. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The original rule risk equals the independent fixed-pool prefix-average risk. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.BaselinePrefixCounts 14 declarations Exact thinning laws for the two independent ordered Poisson pools of the baseline.
Exact thinning laws for the two independent ordered Poisson pools of the baseline. The complete-record and auxiliary histograms are joined before selecting arm counts.
The complete-record law is a probability measure.
Definition (Lean source)
The histogram of an ordered finite sample on a finite alphabet is measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
The full histogram of both pools, with disjoint indices for the two channels.
Definition (Lean source)
Both ordered finite alphabets make the joint histogram measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Thinning the independent ordered prefixes gives independent Poisson counts, including zero-mass atoms, jointly across the two channels. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each coordinate has its exact Poisson marginal under the joint prefix law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The full collection of complete and auxiliary atom counts is independent. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Selecting one arm's success counts and both marginal arm counts preserves independence. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A complete-prefix success count has the exact marked-mass Poisson mean. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, An auxiliary-prefix count has the exact arm-mass Poisson mean. This gives the stated result.
Formal statement
Proof (Lean source)
The clipped inverse-count contrast on the two untruncated ordered prefixes.
Definition (Lean source)
The ordered-prefix statistic is measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The ordered-prefix statistic takes values in the prescribed interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The ordered Poisson prefixes satisfy the baseline contrast risk bound by thinning, the independent-cell moment bounds, and clipping. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.CausalRealization 25 declarations Existence and universal ATE identification for compatible finite potential laws.
Existence and universal ATE identification for compatible finite potential laws.
Independent conditional Bernoulli completion followed by the factual outcome.
Definition (Lean source)
Under the stated inputs and conditions, The propensity is a probability even on the stipulated null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each Bernoulli factor is nonnegative, including boundary probabilities. This gives the stated result.
Formal statement
Proof (Lean source)
The factual-outcome indicator leaves a unit mass over all binary coordinates.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The independent completion table is normalized before applying the PMF constructor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Normalization preserves the explicit completion table on every full atom. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The completion assigns zero probability to every inconsistent factual outcome. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing the factual outcome gives the product conditional Bernoulli table. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The potential-outcome pair and treatment factor conditionally on each covariate cell. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The propensity weights reconstruct both arm masses, including null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The binary regression reconstructs the two outcome atom masses, including null arms. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Mapping a full law to its observed coordinates sums out both potential outcomes. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The completion reproduces every original complete-record mass exactly. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The independent potential-outcome completion extends exactly the supplied observed law. This gives the stated result.
Formal statement
Proof (Lean source)
Success mass of one potential outcome in a fixed covariate cell.
Under the stated inputs and conditions, Potential-outcome marginal atom masses are nonnegative. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The full potential-outcome table and observed law have identical covariate masses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The full potential-outcome table and observed law have identical arm masses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Consistency identifies factual success mass with selected potential success mass in each arm. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each potential success mass is bounded by its covariate mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing conditional exchangeability over a potential success event gives its identifying equation. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Overlap identifies each potential success mass without restricting the unseen coupling. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Finite expectation of the contrast equals the difference of the two potential success masses. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every compatible extension identifies the same observable ATE under occupied-cell overlap. This gives the stated result.
Formal statement
Proof (Lean source)
For an observed law with at least two covariate cells, positive overlap, overlap at most one quarter, and membership in the model class, the independent potential-outcome extension realizes the observed law, and every compatible exchangeable extension has the stated causal contrast.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.ChebyshevAlgebra 7 declarations Algebraic degree bounds and removable-value identities for the Chebyshev continuations.
Algebraic degree bounds and removable-value identities for the Chebyshev continuations.
Under the stated inputs and conditions, Division by the variable removes the zero constant coefficient of the first numerator. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The removable value of the first continuation is the normalized endpoint derivative. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, The second numerator also has zero constant coefficient, so division is exact. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, Both polynomial divisions realize the displayed removable rational expressions. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each exact division lowers the degree by one, giving the factorial truncation order. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, The Chebyshev numerator is nonnegative and bounded by both its range and endpoint slope. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The first continuation lies between zero and the smaller of one and the inverse-scale bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.CitedGates 4 declarations Finite Pinsker, Markov, and finite polynomial duality proved from Causalean primitives.
Finite Pinsker, Markov, and finite polynomial duality proved from Causalean primitives.
Natural-log KL on a finite alphabet, with infinite divergence when a positive mass has zero reference mass. On probability vectors its finite branch is the usual KL sum.
Wu and Yang (2016), Remark 4, displayed Pinsker inequality, arXiv:1407.0381v3. Natural-log finite divergence, including infinite KL for singular probability pairs.
Formal statement
Proof (Lean source)
Pierzchała (2016), Theorem 1.1, DOI:10.1007/s00208-015-1294-9. The degree-bounded pointwise form of Markov's inequality.
Formal statement
Proof (Lean source)
Wu and Yang (2016), Appendix E, identity (34) and alternating finite weights, arXiv:1407.0381v3. Weights have variation one and positive orientation.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.CoefficientBounds 4 declarations Coefficient bounds for the two Chebyshev continuation polynomials, using the shifted Chebyshev recurrence and invariance of the coefficient norm under multiplication by X.
Coefficient bounds for the two Chebyshev continuation polynomials, using the shifted Chebyshev recurrence and invariance of the coefficient norm under multiplication by X.
Under the stated inputs and conditions, Scalar multiplication scales the sum of absolute polynomial coefficients. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Multiplication by the variable shifts coefficients and preserves their absolute sum. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The first continuation inherits the shifted Chebyshev coefficient bound after division. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The second removable division gives the coefficient sum required by the certificate. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.ComparisonPluginRisk 12 declarations Bounded-loss transport from a supplied marginal table to its proof-only replacement population, and the auxiliary plug-in rule used for experiment comparison.
Bounded-loss transport from a supplied marginal table to its proof-only replacement population, and the auxiliary plug-in rule used for experiment comparison.
Under the stated inputs and conditions, The replacement complete-record law is at most half the marginal L¹ error away in TV. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squared loss on the action and target intervals is four-Lipschitz in the target. This gives the stated result.
Formal statement
Proof (Lean source)
Risk of a supplied-table rule when the supplied table need not equal the true one.
Definition (Lean source)
Under the stated inputs and conditions, Bounded measurable supplied-table losses are integrable at any population and target. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, For a fixed legal table, product-TV and target transport cost at most (2n + 4) times its marginal L¹ error. This gives the stated result.
Formal statement
Proof (Lean source)
Plug a legal auxiliary empirical table into any supplied-table rule.
Under the stated hypotheses, the plug-in is jointly Borel in both channels and the seed. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The supplied-table rule's range bound also bounds its empirical plug-in. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Product sampling expresses plug-in risk as the auxiliary average of fixed-table risks. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every supplied-table rule has uniformly bounded squared risk, so its supremum is finite. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Conditional transport and the expected empirical L¹ bound give the plug-in risk guarantee. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Taking rule infima after the plug-in construction gives the numerical experiment bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.ComparisonReplacement 14 declarations Proof-only replacement of a population marginal while retaining its binary outcome regressions.
Proof-only replacement of a population marginal while retaining its binary outcome regressions. This realizes the comparison law in the benchmark-recovery roadmap.
Under the stated inputs and conditions, Binary conditional outcome weights are nonnegative, including null original arms. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The two conditional outcome weights sum to one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every original atom factors into its arm mass and its conditional outcome weight. This gives the stated result.
Formal statement
Proof (Lean source)
Attach the original outcome regressions to an arbitrary supplied table, with a population fallback on ambient inputs that cannot be normalized.
Definition (Lean source)
Under the stated inputs and conditions, A nonnegative probability table gives exactly the specified replacement atoms. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The arm masses of the replacement law are the supplied table entries. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The auxiliary table is exactly the requested replacement marginal. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Covariate masses sum the supplied arm entries. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A legal replacement marginal gives a law in the same overlap model. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, In every positive replacement arm the conditional mean is inherited, even if the original arm was null (its inherited mean is then zero). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Retaining the binary conditional weights preserves the complete-table L¹ distance. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, In a legal occupied replacement cell, both inherited arm means are unchanged. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The replacement target is the original regression contrast under the new cell weights. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Moving a legal marginal changes the target by at most the marginal L¹ distance. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.EmpiricalTableAdjustment 24 declarations Legal overlap adjustment of empirical marginal tables, its factor-three L¹ bound, and the expected empirical approximation error.
Legal overlap adjustment of empirical marginal tables, its factor-three L¹ bound, and the expected empirical approximation error.
Clamp the treated mass while keeping the empirical covariate mass fixed.
The legal adjustment is total on the ambient real table space.
The adjustment is Borel, including at empty cells. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Adjustment preserves the covariate mass cell by cell. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A nonnegative cell is adjusted into the overlap interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Relative to a legal population cell, moving the treated entry costs at most its L¹ error. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both entries together incur at most three times their original L¹ error. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing the cell bounds gives the factor-three table adjustment estimate in the roadmap. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Nonnegative input coordinates remain nonnegative after adjustment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A normalized empirical table stays normalized. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The adjusted table satisfies both arm overlap inequalities, including at null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A legal input table is fixed by the adjustment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The population marginal has exactly the legal overlap bounds used in the L¹ estimate. This gives the stated result.
Formal statement
Proof (Lean source)
Auxiliary records determine the adjusted empirical table without using labeled data.
Definition (Lean source)
Under the stated hypotheses, the adjusted empirical table is a total Borel function of the auxiliary array. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Empirical adjustment preserves positivity and the normalization to a probability table. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The adjusted empirical table belongs to the legal marginal set. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The data-only legal adjustment costs at most three times the raw empirical L¹ error. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The library's empirical mass and the empirical-frequency table agree. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each empirical marginal coordinate has the exact binomial mean squared error. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The squared L¹ error is controlled by the sum of squared coordinate errors. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The empirical marginal's expected squared L¹ error is at most alphabet size over budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Nonnegative variance converts the squared L¹ bound into its expected-error bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The legal empirical table has expected L¹ error at most three times the iid square-root rate. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Estimator 13 declarations Ordered three-pool estimator with degree calibrated to rare-label information.
Ordered three-pool estimator with degree calibrated to rare-label information.
The hybrid schedule records the stated pool sizes, Poisson intensities, polynomial degree, and bandwidth.
The public tuning implements the ordered splits and logarithmic degree based on rare-label information.
Definition (Lean source)
The first Chebyshev continuation divides its zero-constant numerator by the polynomial variable.
The second continuation divides one minus the first by the polynomial variable.
Definition (Lean source)
Complete records in an ordered block with a fixed mark.
The count uses an ordered auxiliary block and the specified arm-cell mark.
Concatenation order is complete-record projections followed by auxiliary records.
Definition (Lean source)
A pilot count selects the polynomial or inverse-count arm contribution.
Definition (Lean source)
A valid prefix triple contributes the clipped sum of treated-minus-control hybrid cell values.
Definition (Lean source)
The attaining data-only rule averages all valid prefix triples with their Poisson weights; overflow outputs zero.
Definition (Lean source)
The finite prefix-average rule is measurable on the original finite data.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A finite Poisson average with zero output on omitted counts preserves [-1,1]. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The prefix-average rule takes values between minus one and one.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.ExperimentComparison 13 declarations Conditional averaging of auxiliary samples for the exact-marginal experiment, and the zero-rule cap on the original minimax risk.
Conditional averaging of auxiliary samples for the exact-marginal experiment, and the zero-rule cap on the original minimax risk.
The iid auxiliary-array weight is a polynomial in the supplied table.
Under the stated inputs and conditions, At the true table the polynomial weight is the probability of the auxiliary array. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Auxiliary-array weights at a population table sum to one, including the empty array. This gives the stated result.
Formal statement
Proof (Lean source)
Averaging over auxiliary arrays retains the independent seed; clipping makes the rule legal on every ambient table.
The averaged rule is Borel on the entire ambient table space. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Clipping bounds the average even on tables that are not probability vectors. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, On a true marginal table the convex average already lies in the action interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Jensen's inequality for the finite conditional average of a randomized rule. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Auxiliary conditional averaging cannot increase squared-error risk at any population. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Conditional averaging proves that exact marginal information can only lower minimax risk. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squared loss makes the exact-marginal minimax value nonnegative. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The original zero rule gives the universal minimax cap of one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both elementary endpoints of the experiment comparison hold for every auxiliary budget. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.FactorialCertificate 8 declarations Chebyshev continuation and factorial-lift mean and second-moment certificate.
Chebyshev continuation and factorial-lift mean and second-moment certificate.
Under the stated inputs and conditions, Products of falling factorials have finite Poisson expectation. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Normalize the exact overlap formula by the factorial-pool intensity. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each overlap factor is at most one when the order is below the intensity. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The binomial overlap sum gives the uniform mixed-moment envelope. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Finite assembly of the mixed-moment envelope against absolute coefficients. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The coefficient certificate and the mixed-moment envelope give the stated constant. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The factorial lift of the second continuation is unbiased under its Poisson law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The Chebyshev continuations obey the stated approximation, coefficient, unbiasedness, and factorial second-moment bounds. This gives the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.FiniteLaw 3 declarations Finite normalization with a total fallback outside the public parameter domain.
Finite normalization with a total fallback outside the public parameter domain.
Normalize finite nonnegative masses; a supplied PMF handles illegal total inputs.
For a success probability and a binary outcome, the Bernoulli atom mass is the success probability for a success and its complement for a failure.
Under the stated inputs and conditions, Normalizing an already normalized nonnegative table preserves every atom. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.FinitePrefixTransfer 3 declarations Run-facing aliases for the generic finite-family Poisson-prefix transfer theorems.
Run-facing aliases for the generic finite-family Poisson-prefix transfer theorems.
Under the stated inputs and conditions, zero overflow output costs at most the overflow probability for a target in [-1,1]. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, a Poisson prefix with one eighth of the pool's mean overflows with probability at most exp(-h). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, For finitely many independent iid pools on arbitrary measurable observation spaces (including infinite Borel alphabets), a measurable statistic with values in [-1,1] and a target in [-1,1], finite independent prefix averaging with zero overflow output transfers risk with the stated exponential tail penalty and yields a total deterministic measurable rule. For Borel observation spaces the resulting rule is Borel. No alphabet finiteness is required. This gives the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.AggregateBias 10 declarations Aggregate pilot bias and heavy-cell separation bounds for equations (10)--(13) of the hybrid arm risk proof.
Aggregate pilot bias and heavy-cell separation bounds for equations (10)--(13) of the hybrid arm risk proof.
Under the stated inputs and conditions, The incorrectly selected inverse branch has total bias at most S to the negative twentieth power, using only the total cell mass bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A light cell's actual pilot mixture retains the polynomial approximation bias and an inverse twentieth power remainder weighted by cell mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (12) on the light cells: summing the actual cell biases gives one bandwidth term per cell and a single public-scale pilot remainder. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The coefficient certificate controls the continuation polynomial on the entire nonnegative half-line, including cells outside the approximation interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The polynomial bias outside the bandwidth grows more slowly than the full factorial second-moment envelope used by the pilot-tail absorption. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A falsely light cell's polynomial bias is absorbed by its pilot probability, with no inverse-overlap factor in the remainder. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The actual heavy-cell mixture bias includes both pilot errors and is bounded by three times cell mass times the public inverse twentieth power. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A zero-success Poisson outcome count makes both branch expectations zero, including at a null own-arm cell. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Null outcome counts contribute zero also after the independent pilot selection. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (12): the sum of canonical hybrid cell biases is bounded by one approximation term per cell and a universal pilot remainder. Null cells are included. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.AggregateMSE 2 declarations Mean squared error assembly for independent canonical hybrid cells, retaining every variance and squared-bias term from roadmap equations (12)--(14).
Mean squared error assembly for independent canonical hybrid cells, retaining every variance and squared-bias term from roadmap equations (12)--(14).
Under the stated inputs and conditions, Independence across canonical cells turns the MSE of their sum into the sum of the cell variances plus the squared sum of their biases. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The proved light/heavy variance assembly and squared total bias bound give the canonical arm MSE envelope, without dropping either incorrect pilot branch. The inverse-count sum remains explicit for its separate overlap bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.AggregateVariance 3 declarations Light-cell assembly of the pilot-mixture variance in roadmap equation (13).
Light-cell assembly of the pilot-mixture variance in roadmap equation (13). All three mixture terms are retained, including at null cells.
Under the stated inputs and conditions, Summing equation (13) over light cells retains the inverse-count variance, the polynomial mass envelope, and both parts of the branch separation. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Adding the light and heavy cell bounds retains every term of equation (13). The only global mass requirement is total mass at most one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squaring equation (12) gives the approximation term and a pilot remainder of the same order retained in equation (14), including null cells. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.BetweenBranch 4 declarations The light-cell between-branch contribution in equation (13), including null cells.
The light-cell between-branch contribution in equation (13), including null cells.
Under the stated inputs and conditions, Overlap controls squared missing-cell bias by cell mass over twice the intensity. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing the squared inverse-branch biases costs no factor for the cell count. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The light-cell branch separation bound extends to zero own-arm masses by overlap. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The light-cell part of equation (13) retains its squared approximation term and absorbs all inverse-branch separation terms using total mass at most one. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.BranchMeans 6 declarations Canonical Poisson branch statistics and their exact polynomial and inverse-count means.
Canonical Poisson branch statistics and their exact polynomial and inverse-count means.
Canonical independent outcome-success, own-arm, and opposite-arm counts.
Definition (Lean source)
For the polynomial degree, the scale bound, the marked-count intensity, the arm-count intensity, and a triple of observed counts, the polynomial cell branch is the factorial-polynomial estimator used for the light-cell branch.
For the marked-count intensity and a triple of observed counts, the inverse-count cell branch is the reciprocal-count estimator used for the heavy-cell branch.
Under the stated inputs and conditions, A finite factorial lift has the same mean as its ordinary polynomial. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Independent Poisson counts factor the outcome and opposite-arm multiplier means. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both branch means equal the arm target minus their explicit bias terms.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.Calibration 1 declarations Numerical degree and exponential absorption calibrated in S, uniformly in overlap.
Numerical degree and exponential absorption calibrated in S, uniformly in overlap.
Under the stated inputs and conditions, The rare-label degree yields the numerical absorption needed in the hybrid proof.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.CanonicalRate 3 declarations Overlap bounds for canonical inverse-count variances and the completed canonical hybrid arm rate.
Overlap bounds for canonical inverse-count variances and the completed canonical hybrid arm rate. The transfer to an arbitrary independent count family is separate.
Under the stated inputs and conditions, The canonical product counts satisfy the inverse-count cell variance envelope, including zero success intensity and null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing canonical inverse-count variances uses total mass at most one and therefore has no cell-count factor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The canonical independent three-pool statistic has the full universal arm rate, assembled from its actual MSE envelope and inverse-count variance bound. Null cells and boundary outcome means are included. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.CountTransfer 1 declarations Transfer from independent count families to the canonical four-count product law.
Transfer from independent count families to the canonical four-count product law.
Under the stated inputs and conditions, Grouping four independent counts in each cell gives the product of their four marginal laws, jointly over all cells. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.FalseLight 1 declarations Exponential absorption of false-light polynomial moments outside the bandwidth.
Exponential absorption of false-light polynomial moments outside the bandwidth.
Under the stated inputs and conditions, The heavy-cell pilot tail absorbs the full factorial second-moment growth.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.FalseLightRisk 11 declarations Global polynomial second moments and false-light pilot-weighted risk, implementing roadmap equations (7), (9), and (10) without a minimum cell mass.
Global polynomial second moments and false-light pilot-weighted risk, implementing roadmap equations (7), (9), and (10) without a minimum cell mass.
Under the stated inputs and conditions, The factorial multiplier has a global squared-moment envelope. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Outside the bandwidth, rescaling the light-cell overlap monomials retains only cell mass, squared cell mass, and the quadratic continuation factor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (7): the heavy-cell polynomial second moment has the full factorial continuation factor and no extra inverse-overlap factor on its squared mass. This gives the stated result.
Formal statement
Proof (Lean source)
Equations (7) and (9): the actual false-light selection probability absorbs the polynomial branch's second moment into the inverse twentieth power of S.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (10): summing false-light polynomial second moments uses only the total mass bound, retaining the outcome and factorial intensity terms. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The unweighted false-light pilot probability obeys the same public-scale tail bound, since the absorbed factorial continuation factor is at least one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, On a heavy cell the mixture separation is bounded by the pilot-weighted polynomial second moment and squared mass, using square integrability rather than branch independence. This gives the stated result.
Formal statement
Proof (Lean source)
The heavy-cell contribution to the between-branch mixture variance is absorbed by the same public-scale bound as its falsely selected polynomial second moment.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The falsely selected polynomial variances are bounded by the already summed second moments in equation (10). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The heavy-cell part of equation (13) sums to a universal pilot-tail remainder, without any independence assumption between the polynomial and inverse branches. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (13), summed over heavy cells: the actual pilot-selected variances retain the inverse-count variance sum and absorb both false-light contributions. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.LightCellRisk 7 declarations Light-cell polynomial second moments and the overlap algebra for equation (5).+
Light-cell polynomial second moments and the overlap algebra for equation (5).+
Under the stated inputs and conditions, The independent success count factors the polynomial branch's second moment into its Poisson second moment and the factorial multiplier's second moment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The light-cell multiplier certificate controls the actual polynomial branch variance, retaining both the outcome-count fluctuation and its squared mean. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (4): light-cell bandwidth and overlap control every mixed monomial in the polynomial second-moment envelope, including null own-arm cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Expanding the light-cell envelope gives the mass-over-intensity and squared-bandwidth terms used in equation (5), without a minimum positive cell mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A light polynomial cell has variance controlled by its mass over the outcome and factorial intensities, plus squared bandwidth over squared overlap. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (5): summing the actual light-cell polynomial variances keeps the total light mass in both intensity terms and the cell count in the bandwidth term. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The light-cell mass is at most one and at most the number of light cells times bandwidth over overlap, as used in equation (5). This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.LightVariance 2 declarations Factorial branch light-cell moments, upstream of the aggregate variance bound.
Factorial branch light-cell moments, upstream of the aggregate variance bound.
Under the stated inputs and conditions, Every finite normalized falling-factorial polynomial is square-integrable under a Poisson law, so its second-moment estimates can be integrated. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The factorial multiplier has a universal light-cell squared-moment bound. This gives the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.MixtureVariance 8 declarations Variance algebra for pilot-controlled branch mixtures, without branch independence.
Variance algebra for pilot-controlled branch mixtures, without branch independence.
Under the stated inputs and conditions, The Bernoulli branch-mixture variance expression admits a deterministic upper bound.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both canonical branches are square-integrable, including null cells and zero intensities. This gives the stated result.
Formal statement
Proof (Lean source)
The implemented hybrid cell is exactly the pilot-event mixture of the two branches.
Formal statement
Proof (Lean source)
The actual pilot-selected cell has finite second moment under the independent pool law.
Formal statement
Proof (Lean source)
Equation (13): the independent pilot mixes branch variances and their mean separation; the polynomial and heavy branches may share all their evaluation counts.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The hybrid's bias is the pilot-weighted sum of the two explicit branch biases. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (2): overlap turns the light-cell approximation error into the public bandwidth divided by epsilon and squared degree. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, On a light cell the between-branch term of equation (13) is bounded by twice the squared polynomial bias plus twice the squared inverse-count bias. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.PilotTails 6 declarations Poisson pilot misclassification probabilities at the public bandwidth cutoff.
Poisson pilot misclassification probabilities at the public bandwidth cutoff.
Under the stated inputs and conditions, A heavy cell is selected as light with exponentially small probability.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The heavy-branch probability times its inverse-count bias has a cutoff-only bound, including at zero cell mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The public bandwidth makes the weighted heavy-branch error exponentially small in the degree, uniformly over every nonnegative cell mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Degree calibration turns the opposite pilot error into the required inverse twentieth power of the label scale. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The estimator's actual minimum-pool bandwidth satisfies the pilot scale condition. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, With the prescribed bandwidth and pilot cutoff, the heavy selection probability times the inverse-count bias is at most the inverse twentieth power of S. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.Hybrid.RateAbsorption 8 declarations Bandwidth rescaling and absorption of the intermediate hybrid variance terms in roadmap equations (14)--(15).
Bandwidth rescaling and absorption of the intermediate hybrid variance terms in roadmap equations (14)--(15). All degree calibration uses S = n epsilon.
Under the stated inputs and conditions, The lower bounds on both factorial intensities give the public bandwidth bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Equation (15): a bandwidth bound controls the light mass, the variance bandwidth, and the squared total bias at the common public scale d / (N epsilon L). This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The calibrated factorial growth absorbs both light-mass terms and the bandwidth variance term into z / sqrt S, retaining the factorial-intensity constant. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Young's inequality at the public scale converts the mixed rate to the two terms of the arm risk, with no restriction on the cell-budget scale z. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, The pilot's inverse twentieth power remainder is smaller than the leading rate. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Applying the actual degree calibration and pool-size assumptions absorbs the entire equation (5) light-variance envelope into the target arm rate. This gives the stated result.
Formal statement
Proof (Lean source)
Every retained term of equation (14), including the single-cell squared-bias sum and the false-pilot remainder, is bounded by a universal multiple of the arm rate. This is deterministic absorption; the probabilistic MSE assembly is separate.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The actual canonical MSE envelope, with its branch constants and pool intensities, absorbs into the public arm rate. The inverse-count variance is supplied by its separate proved overlap bound; no retained pilot term is discarded. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridArmRisk 1 declarations Uniform arm MSE bound for the independent three-pool hybrid statistic.
Uniform arm MSE bound for the independent three-pool hybrid statistic.
The three-pool Poisson hybrid arm statistic has the universal rare-overlap mean squared error bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridFiniteEncoding 13 declarations Ordered three-pool count readback and conditional averaging for the finite hybrid rule.
Ordered three-pool count readback and conditional averaging for the finite hybrid rule.
The ideal ordered statistic retains the outcome, pilot, and factorial pools separately.
Definition (Lean source)
Under the stated inputs and conditions, Ordered histograms recover exactly the three original array counters. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The count bridge applies to every retained triple, with no extra array-bound premises. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Integrating a capped triple gives the exact product of the three Poisson weights. This gives the stated result.
Formal statement
Proof (Lean source)
Each Poisson request is independent, with the exact public pool intensity.
Definition (Lean source)
The independent request law has total mass one, also when a pool is empty.
Definition (Lean source)
Overflow in any of the three pools returns zero.
Definition (Lean source)
Under the stated inputs and conditions, Both valid-prefix clipping and zero overflow lie in the required interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The estimator's finite sum is exactly conditional averaging of the capped statistic. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Jensen's inequality contracts the squared loss at each fixed original sample. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Conditional averaging contracts risk under the original product data law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The independent seed leaves the data-only hybrid rule's risk unchanged. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The original rule risk is bounded by its unaveraged, zero-overflow prefix risk. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridFiniteRate 9 declarations Finite-pool size, intensity, overflow, and logarithmic rate calibration for the hybrid upper bound.
Finite-pool size, intensity, overflow, and logarithmic rate calibration for the hybrid upper bound.
Under the stated inputs and conditions, The large-information branch has at least twelve complete records. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The prescribed splits retain positive pools and comparable marginal pool lengths. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Pool intensities satisfy exactly the hypotheses of the uniform hybrid arm theorem. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each positive capacity has an exponential overflow cost bounded by its reciprocal. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, The three overflow costs are absorbed by the rare-label inverse-information rate. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The degree calibrated to log S also controls the frontier logarithm. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Converting from the polynomial degree to the frontier logarithm costs a numerical factor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The exact zero branch has risk at most one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The frontier rate absorbs the zero-branch risk with a universal numerical constant. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridFiniteTransfer 17 declarations The three independent hybrid pools as a finite family, and exact finite-prefix risk transfer.
The three independent hybrid pools as a finite family, and exact finite-prefix risk transfer.
Three singleton coordinates distinguish the complete, pilot, and factorial pools.
Evaluation identifies a three-coordinate dependent family with its ordered triple.
Definition (Lean source)
Under the stated inputs and conditions, The triple equivalence preserves the independent product law. This gives the stated result.
Formal statement
Proof (Lean source)
The alphabet family retains the two marginal pools as different coordinates.
Definition (Lean source)
Each coordinate inherits its finite observation alphabet's measurable structure.
Definition (Lean source)
The observation-law family assigns the complete law and its two marginal copies.
Definition (Lean source)
Each pool's observation law is a probability measure.
Definition (Lean source)
The family capacities are exactly the three public hybrid pool lengths.
Definition (Lean source)
Prefix-family readback computes the same ordered clipped hybrid contrast.
Definition (Lean source)
Prefix-family readback is measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The family statistic retains the clipped interval at every prefix. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The ideal prefix-family risk is exactly the already established triple-prefix risk. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Extracting and packing the original three pools gives the finite-family iid law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Valid requests have identical family and triple readback; overflow resets both to zero. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, The estimator is precisely the finite-family conditional prefix average. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Original-record risk equals the finite-family Rao--Blackwell risk. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Finite-prefix averaging transfers the exact-tuning bound to the original records. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridPoolLaw 17 declarations Exact independent laws of the three disjoint original-record hybrid pools.
Exact independent laws of the three disjoint original-record hybrid pools.
Under the stated hypotheses, Three consecutive blocks of an iid array retain their independent iid laws. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Regroup four independent pools to pair the pilot blocks and the factorial blocks. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Rewriting a pool capacity preserves its iid law and ordered coordinates. This gives the stated result.
Formal statement
Proof (Lean source)
Complete outcomes, pilot marginals, and factorial marginals use disjoint ordered blocks.
Definition (Lean source)
Extracting the three finite pools is measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Under the original data law, the extracted hybrid pools are mutually independent. The two marginal pools concatenate projected complete records with auxiliary records. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Any measurable statistic of the three extracted pools has the independent-pool risk. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The outcome prefix keeps exactly the first requested complete records. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The pilot prefix uses the pilot complete block before its auxiliary block. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Casting an array capacity does not change any retained ordered prefix. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The factorial prefix uses the final complete block before the final auxiliary block. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every retained triple computes the same clipped statistic in the array and pool forms. This gives the stated result.
Formal statement
Proof (Lean source)
The independent fixed-pool statistic returns zero whenever any request overflows.
Definition (Lean source)
Under the stated inputs and conditions, Valid requests agree by count readback, and both forms reset overflow to zero. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Extraction of disjoint pools preserves the independent request law as well. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The capped array risk is exactly its independent three-pool risk. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Conditional averaging bounds original-record risk by the independent capped-pool risk. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridPrefixContrast 6 declarations Square integrability and clipped contrast risk for the independent three-pool hybrid prefixes.
Square integrability and clipped contrast risk for the independent three-pool hybrid prefixes.
Under the stated hypotheses, Independent Poisson counts give a square-integrable hybrid arm sum at every tuning. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each ordered-prefix hybrid arm has finite second moment, including zero intensities. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The ordered clipped statistic is exactly the difference of the two hybrid arm sums. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squared-difference and clipping bounds aggregate the two arm risks without arm independence. This gives the stated result.
Formal statement
Proof (Lean source)
The clipped ordered hybrid statistic is measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Clipping keeps every ordered hybrid output in the target interval. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridPrefixCounts 11 declarations Joint independent Poisson histogram laws for the outcome, pilot, and factorial prefixes.
Joint independent Poisson histogram laws for the outcome, pilot, and factorial prefixes.
The three ideal ordered pools have independent Poisson sample laws.
Definition (Lean source)
The ideal three-pool experiment is a probability law even at zero intensities.
Definition (Lean source)
Disjoint sum indices distinguish all atoms of the three histograms.
Definition (Lean source)
Histograms of all three ordered finite samples are measurable. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Thinning and the product law give independent Poisson counts for every atom. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Every atom has its prescribed Poisson marginal in the three-pool law. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, All atom counts are mutually independent across cells and across pools. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The outcome success counts and both marginal pools form the independent arm experiment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Outcome success counts have mean intensity times the marked mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Pilot arm counts have mean pilot intensity times the arm mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Factorial arm counts have mean factorial intensity times the arm mass. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridPrefixRisk 2 declarations Arm risk readback from independent ordered Poisson prefixes.
Arm risk readback from independent ordered Poisson prefixes.
The unclipped arm sum computed from the three ordered histograms.
Definition (Lean source)
Under the stated inputs and conditions, Applying the count-experiment theorem bounds each ordered-prefix arm's risk. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridTunedRisk 3 declarations Risk bounds for the exact public hybrid tuning, including the logarithmic conversion and the three finite-pool overflow costs.
Risk bounds for the exact public hybrid tuning, including the logarithmic conversion and the three finite-pool overflow costs.
Under the stated inputs and conditions, The prescribed intensities and bandwidth realize the ordered-prefix contrast bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The ideal contrast risk and all three overflow costs have the uncapped frontier order. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The clipped finite hybrid estimator has squared risk at most four for every law. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.HybridUpper 1 declarations Gate-free original-record upper bound and range for the finite hybrid rule.
Gate-free original-record upper bound and range for the finite hybrid rule.
The finite hybrid rule is measurable, clipped, and uniformly attains the frontier upper order.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.InverseCountArmRisk 11 declarations Overlap-uniform inverse-count arm bias and variance under independent Poisson counts.
Overlap-uniform inverse-count arm bias and variance under independent Poisson counts.
Under the stated inputs and conditions, Both arms inherit the occupied-cell overlap floor, including zero-mass cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The exponential missing-cell envelope has the sharp reciprocal-intensity bound. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The sum of exponential missing-cell masses is capped by one and by the cell budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The explicit inverse-count bias obeys the overlap-uniform bound without excluding null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The Poisson reciprocal first-moment formula gives target minus missing-cell bias. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summed cell means satisfy the claimed capped bias bound once the Poisson means are read back. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Pull back Poisson integrability and the exact count mean along a measurable count. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Independent Poisson factors give the exact inverse-count cell mean and integrability. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Reading back all independent Poisson cell means gives the arm expectation, including null cells. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing the numerical Poisson cell envelopes gives a universal arm envelope. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Independent Poisson count families yield the overlap-explicit arm bias and variance guarantee. This gives the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.InverseCountProductMoments 7 declarations Independent product moments for the inverse-count arm statistic.
Independent product moments for the inverse-count arm statistic.
Under the stated inputs and conditions, Independent square-integrable factors have a square-integrable product. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The exact independent-product variance identity separates count and weight fluctuations. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, A measurable Poisson count inherits its first two moments and variance. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, A measurable Poisson count inherits reciprocal square-integrability and moment bounds. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Independence yields both moment bounds for the marginal inverse-count weight. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, All three independent Poisson factors give the cell variance envelope. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Statistics computed in distinct three-count cells are independent. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.InverseCountVarianceAlgebra 3 declarations Numerical cell envelopes for the inverse-count Poisson variance calculation.
Numerical cell envelopes for the inverse-count Poisson variance calculation.
Under the stated inputs and conditions, Overlap controls the squared opposite-arm mass divided by the current-arm mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The four rational factors in the Poisson second-moment and variance bounds. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The cell second-moment and variance envelopes are uniform even when the arm mass is zero. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.KnownMarginalUpper 12 declarations A total supplied-marginal inverse-propensity rule and its finite-sample risk bound.
A total supplied-marginal inverse-propensity rule and its finite-sample risk bound.
The binary inverse-propensity score reads both cell masses from the supplied table. Division is total even for illegal tables and null cells.
The score is Borel jointly in its real table and finite record. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Clipping makes the supplied-table mean a total bounded rule on every table.
The supplied-table rule is jointly Borel. This gives the stated conclusion.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The total supplied-table rule is clipped to the prescribed action interval. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, At the actual marginal table the score has exactly the observable ATE mean. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Overlap bounds each arm's marked contribution to the score's second moment. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The score's second moment is at most twice the inverse overlap floor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Independence of complete records divides the score variance by the labeled budget. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Projection onto the action interval cannot increase squared distance to a legal target. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The zero branch and the clipped iid mean attain the capped oracle label rate. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Taking the infimum over Borel supplied-table rules preserves the oracle upper bound. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.LabelFloorPair 18 declarations Explicit diagnostic pair sharing its treatment-covariate marginal.
Explicit diagnostic pair sharing its treatment-covariate marginal.
The arbitrary real diagnostic amplitude is positive and at most one eighth. @realizes \delta(arbitrary Real amplitude in (0,1/8])
Definition (Lean source)
The displayed two-cell law, with total fallback outside legal scalar ranges.
Definition (Lean source)
The fixed endpoint one eighth is a legal diagnostic amplitude.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The displayed scale choice is a legal diagnostic amplitude for every scale.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing a constant over the two occupied covariates gives twice that constant. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The diagnostic table has nonnegative entries throughout the legal parameter range. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The displayed diagnostic table already has total mass one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Reading back a diagnostic atom gives exactly its specified table entry. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing out the outcome leaves a diagnostic arm mass independent of the sign. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Each occupied diagnostic covariate has mass one half, and all other cells are null. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The occupied diagnostic propensities equal the public overlap floor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Both signs of the diagnostic pair belong to the public model class. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Diagnostic conditional means match the specified control and treated Bernoulli means. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Summing the two occupied-cell contrasts yields the signed diagnostic amplitude. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The real mass of a projected treatment-covariate atom is its arm-cell mass. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The positive and negative diagnostic laws have exactly the same auxiliary PMF. This gives the stated result.
Formal statement
Proof (Lean source)
Finite natural-log divergence sums population mass times the log probability ratio.
Under the stated inputs and conditions, At amplitude one eighth the diagnostic one-record KL has its exact stated value. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.LabelFloorTesting 10 declarations Scaled diagnostic KL and testing bounds for the rare-label pair, including common randomness.
Scaled diagnostic KL and testing bounds for the rare-label pair, including common randomness.
Under the stated inputs and conditions, The diagnostic pair has the stated KL formula at every legal amplitude. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The diagnostic one-record KL is bounded by sixteen times overlap times amplitude squared. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The diagnostic laws have common support even when the remaining cells are null. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The ordered labeled arrays have divergence at most sixteen times their rare-label scale. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Squaring the chosen amplitude gives the inverse maximum-scale expression. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The scaled labeled pair is uniformly close in total variation. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The amplitude squared divided by four is exactly the asserted label benchmark constant. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A close pair with opposite targets forces squared loss for every clipped Borel rule. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Adjoining an independent common probability law preserves total variation. This gives the stated result.
Proof (Lean source)
Under the stated inputs and conditions, Clipping the rule and target bounds squared risk by four under any probability law. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.OraclePhaseAlgebra 5 declarations The capped frontier has oracle order exactly when the dimension is bounded by the marginal information divided by the square root of the label information.
The capped frontier has oracle order exactly when the dimension is bounded by the marginal information divided by the square root of the label information.
Under the stated inputs and conditions, A positive dimension bound can be expressed as a bound on its normalized ratio. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Uniform frontier comparisons turn bounded oracle risk ratios into the dimension condition. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, On the supervised slice, the oracle dimension scale is exactly square-root label information. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Positive factors convert the dimension condition into the marginal-budget condition. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The dimension and marginal-budget big-O conditions use exactly the same eventual constants. This gives the stated result.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.PhaseAlgebra 5 declarations Abstract sequence algebra for risks uniformly comparable to the frontier.
Abstract sequence algebra for risks uniformly comparable to the frontier.
Under the stated inputs and conditions, The logarithmic diagnostic is positive for every positive label scale. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The frontier always dominates the capped rare-label benchmark. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, At the dimension saturation threshold the capped frontier equals one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The marginal-budget plateau bounds the frontier by twice the capped label benchmark. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Any sequence risk uniformly comparable to the displayed frontier has the consistency phase.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.PoissonInverseMoments 1 declarations First moment, squared moment, and variance of a shifted reciprocal Poisson count.
First moment, squared moment, and variance of a shifted reciprocal Poisson count.
The shifted reciprocal Poisson count has its exact first moment and the displayed universal squared-moment and variance bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.PriorHandle 13 declarations Finite core/filler affine priors with a reservoir and shared normalizer.
Finite core/filler affine priors with a reservoir and shared normalizer.
The affine-prior schedule records its intensities, degree, bandwidth, cone scale, and number of rare cells.
The affine schedule uses all marginal records and a degree calibrated to rare-label information.
Definition (Lean source)
A finite signed reciprocal-gap certificate, with all its defining properties.
Definition (Lean source)
The latent type retains a separate filler branch even when a core atom is at zero.
For the cone degree, the measurable-space structure on latent states is the discrete measurable space.
Definition (Lean source)
The core branch reads its certificate node and the filler branch uses zero.
The core sign is the polar sign of its signed weight; the filler carries no signed contribution.
Core latent probabilities tilt the absolute certificate weights by the reciprocal treated mass.
The finite latent PMF uses reciprocal-tilted core weights and places the remaining probability on the filler.
Definition (Lean source)
The common expected raw cell mass averages b0 plus the latent node.
Raw complete-record masses implement the affine cone, signed outcome marking, reservoir, and null remaining cells.
Definition (Lean source)
The raw complete-record table is divided by its total mass, with a total fallback outside legal inputs.
Definition (Lean source)
The finite product of common latent draws pushes forward to normalized complete-record tables under each hypothesis.
Definition (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.Helpers.ShrinkingConeDual 5 declarations Reciprocal approximation gap on the shrinking overlap cone, using proved polynomial interfaces.
Reciprocal approximation gap on the shrinking overlap cone, using proved polynomial interfaces.
Under the stated inputs and conditions, The shrinking-cone reciprocal is continuous even at the zero endpoint. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Markov's derivative bound rules out error below one eighth on the shrinking cone. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The polynomial inequalities imply a variation-one finite signed moment certificate with reciprocal gap at least one eighth.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The public affine schedule admits the named shrinking-cone dual witness.
Formal statement
Proof (Lean source)
The testing priors use the displayed Dirac pair in the rare-label regime and choose the named dual witness only in the affine branch.
Definition (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.T_AnnotationResourcePhases 11 declarations Exact resource phases for arbitrary sequences and universal saturation and oracle plateaus.
Exact resource phases for arbitrary sequences and universal saturation and oracle plateaus.
Under the stated inputs and conditions, The zero Borel rule gives a risk at most one on the full observable model class. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Uniform positive comparisons transfer vanishing ratios in both directions. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The supervised cap differs from the dimension-only cap by at most the inverse label scale. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Normalizing the auxiliary dimension term by its cap gives the exact budget ratio square. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Strict improvement is exactly vanishing frontier ratio under the uniform comparison. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A vanishing frontier ratio forces diverging label information, even on oscillating sequences. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The capped frontier ratio is bounded by the three inverse information scales. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Diverging label, relative-dimension, and marginal-budget scales imply strict improvement. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Once the label cap is inactive, a small frontier ratio controls both inverse scales. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Vanishing capped frontier ratios force both dimension and marginal-budget divergence. This gives the stated result.
Formal statement
Proof (Lean source)
Exact consistency, oracle, and strict-improvement phases and the two finite-budget elbows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.T_BenchmarkRecovery 8 declarations Same-class benchmark recovery and exact-marginal quantitative experiment comparison.
Same-class benchmark recovery and exact-marginal quantitative experiment comparison.
Under the stated inputs and conditions, The capped label benchmark has a positive uniform floor on bounded label scales. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The fixed-parameter comparison error vanishes as the auxiliary sample grows. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, A quantitative comparison with the exact-marginal experiment implies its limit. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The baseline guarantee bounds the infimum over all original-data Borel rules. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, With two covariate cells the baseline comparison is at most five label benchmarks. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Uniform logarithmic comparisons at a fixed positive overlap floor. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated hypotheses, Fixed-floor logarithmic comparisons give the uncapped and capped rate comparisons. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Fixed-floor recovery, binary-alphabet and oracle orders, quantitative comparison, and limit. This gives the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.T_RareLabelFloor 1 declarations Rare-label lower bound uniform in auxiliary budget and exact-marginal side information.
Rare-label lower bound uniform in auxiliary budget and exact-marginal side information.
Uniform rare-label floors, explicit legal common-marginal pair, and its exact KL.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.T_UniformAnnotationFrontier 1 declarations Uniform rare-overlap annotation frontier and existence and identification of causal extensions.
Uniform rare-overlap annotation frontier and existence and identification of causal extensions.
Universal four-index minimax comparison, attaining rule, and compatible causal interpretation.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_AnnotationRarearmFrontier_Research.T_UniformBaseline 4 declarations Uniform original-record inverse-count baseline theorem.
Uniform original-record inverse-count baseline theorem.
Under the stated inputs and conditions, The prescribed zero branch has squared risk at most one. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, Clipping both the baseline and the target bounds squared loss by four. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, For fewer than six labeled records, the capped baseline rate is at least four fifths. This gives the stated result.
Formal statement
Proof (Lean source)
Under the stated inputs and conditions, The total inverse-count baseline has a universal overlap-explicit risk guarantee. This gives the stated conclusion.