Formalization: Minimax Excess Variance with Smooth Pairwise Interactions in Randomized Experiments
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 (1efc342) — statements may have moved since the audit.
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Basic 63 declarations The continuous covariate world uses Mathlib kernels; the finite-design substrate does not carry covariate-dependent assignment.
Bivariate Sobolev design capacity: carriers and constructions
The continuous covariate world uses Mathlib kernels; the finite-design substrate does not carry covariate-dependent assignment. The minimax functional reuses Causalean's extended nonnegative API. All paper-owned proof obligations are left to the proof-filling stage.
[ Ambient coordinates; the sampling measure is supported on the unit cube.
Definition (Lean source)
Unit indices.
Definition (Lean source)
Coordinate indices.
Definition (Lean source)
Product uniform measure, including the zero-dimensional convention.
Definition (Lean source)
Finite-valued Borel centered square-integrable representatives.
Definition (Lean source)
Canonical main effect, integrating the unused coordinates.
Canonical pair effect, subtracting the two main effects.
The closed unit cube in Euclidean coordinates.
Definition (Lean source)
The unitary angular-frequency Fourier integral, initially on integrable extensions.
Definition (Lean source)
Squared restriction norm, as an extension infimum of weighted Fourier energy. The integrable extensions give the same infimum by cutoff approximation; the squared functional is used directly, avoiding an accidental fourth power in the pooled budget.
Definition (Lean source)
Exact canonical order-two ANOVA with zero intercept.
Definition (Lean source)
The pooled squared component restriction norms have total budget one.
Definition (Lean source)
Centered bivariate outcomes with the exact ANOVA decomposition and pooled budget.
Definition (Lean source)
A Bool represents a sign; true is +1 and false is −1.
The finite sign space is standard Borel.
Definition (Lean source)
The real sign associated with a coin.
Definition (Lean source)
Covariate arrays.
Definition (Lean source)
The covariate array is standard Borel.
Definition (Lean source)
Independent uniform original covariates.
Definition (Lean source)
Pre-assignment schedules, with control first and treatment second.
Definition (Lean source)
The schedule space is standard Borel.
Definition (Lean source)
Joint law drawing a schedule before drawing covariate-only assignment.
Definition (Lean source)
Independent uniform covariates on an arbitrary sampling space.
Definition (Lean source)
Unitwise conditional zero sign means under the original cube-supported sampling law. Null-set representatives and values outside the sampled cube are unrestricted.
Definition (Lean source)
Pointwise fairness, used internally for concrete constructions and the cited carrier.
Definition (Lean source)
Assignment is conditionally independent of every pre-assignment outcome mechanism.
Definition (Lean source)
Borel probability assignment kernels, with no outcomes in the input.
Definition (Lean source)
Fair outcome-independent original-sample designs.
Definition (Lean source)
Independent fair signs.
Definition (Lean source)
The independent-sign law is a probability measure.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
[ The independent-sign branch, constant in the covariates.
Definition (Lean source)
Uniform signs have zero marginal means by the sign-reversal involution.](goal) This uses the stated conclusion.
Proof (Lean source)
Every almost-everywhere fair design has a pointwise fair null-equivalent representative. This changes a representative for proof purposes, not membership in the public design class. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Extended expected squared prognostic imbalance.
Full-design capacity, keeping the fixed-function supremum outside sampling.
Definition (Lean source)
Worst risk of a specified design.
Definition (Lean source)
Number of coordinate pairs.
Definition (Lean source)
Pair-cosine indices and positive integer frequencies.
Number of cosine coordinates.
Definition (Lean source)
Explicit positive cutoff-extension normalization.
Tensor-pair cosine features.
The normalized random-sign cosine polynomial.
Definition (Lean source)
The prior cutoff.
Uniform independent coefficient signs; its function image is the legal-prior candidate.
Definition (Lean source)
The prior average risk, without a measurable-space choice on the function space.
Definition (Lean source)
Lower comparison scale.
Definition (Lean source)
Sharper lower constant, independent of n and d.
Definition (Lean source)
Uniform upper constant.
Definition (Lean source)
The fixed average treatment effect.
Definition (Lean source)
The fixed treatment-effect amplitude.
Definition (Lean source)
The sinusoidal covariate treatment effect.
Independent unit-variance Gaussian noise, drawn before assignment.
Definition (Lean source)
Potential outcomes with prognosis m and the fixed heterogeneous treatment effect.
Definition (Lean source)
Measurability of the Gaussian completion's measure-valued map. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The pre-assignment Gaussian potential-outcome kernel.
Definition (Lean source)
Treatment indicator corresponding to the original unit sign.
Actual unit-weight Horvitz--Thompson ATE estimator.
Realized full-schedule finite-population ATE.
Definition (Lean source)
Potential-outcome midpoint vector.
The assignment covariance matrix, including its mean subtraction.
Gaussian benchmark.
Definition (Lean source)
Superpopulation target under the Gaussian completion.
Definition (Lean source)
The frozen causal completion uses independent standard Gaussian pre-assignment noise and the sinusoidal treatment effect specified by S3. It draws X, then the full schedule Y, then assignment from the covariate-only kernel. The remaining components explicitly anchor A=(Z+1)/2, the actual HT estimator, the full-schedule target, and its sampling expectation.
Definition (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CapacityHandle 22 declarations One smoothness-free kernel uses the ordered cosine/sine features of the reflected and commonly shifted original sample.
Spectral design and capacity handle
One smoothness-free kernel uses the ordered cosine/sine features of the reflected and commonly shifted original sample. Its seed measure and exact arithmetic map are explicit. Feature prefixes are obtained by finite box sorting, with no well-founded enumeration.
[ One representative of each {k,-k}, taking the first nonzero coordinate positive.
Definition (Lean source)
Lexicographic tie-breaking in the original coordinate order.
Definition (Lean source)
Finite frequency enumeration for a requested prefix.
Definition (Lean source)
The index-th frequency in the prescribed ordering; a box of radius index+1 suffices.
Definition (Lean source)
Consecutive real cosine/sine pairs, with row numbering starting at one.
Independent fair reflection coins for every original unit and coordinate.
Uniform law of the reflection coins.
Definition (Lean source)
The reflected covariates, encoded by half of the period-two coordinate.
Definition (Lean source)
Shift the lifted sample by one independent common Haar torus element.
Definition (Lean source)
Reflection coins, common shift, and independent uniform rounding seeds.
Definition (Lean source)
Independent spectral seed law.
Definition (Lean source)
Evaluate the first floor(n/4) prescribed real rows at the randomized sample.
The prescribed exact-real signing map.
Definition (Lean source)
Joint Borel measurability of the exact spectral signing map. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Measurability of the seed-image kernel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Seed image of the prescribed procedure.
Definition (Lean source)
The spectral seed-image kernel has total mass one.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Every prescribed real Fourier row has the common envelope √2.
Proof (Lean source)
[ One attaining design for every smoothness: independent signs when B≥n.
Definition (Lean source)
The concrete attaining construction has pointwise zero sign means, a stronger internal property than the public class's almost-everywhere fairness requirement.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Explicit comparison scale.
Definition (Lean source)
The comparison scale, single original-sample design, and independent finite prior.
Definition (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CitedGates 29 declarations Cited facts are recorded as Sort-0 propositions.
Disclosed cited logical gates
Cited facts are recorded as Sort-0 propositions. Torus Parseval and the two exact interpolation facts have proved witnesses; remaining cited facts are explicit consumer inputs. Definitions fix the normalized K norm and the actual published HT benchmark.
[ Unit-torus coordinates represent period-two coordinates by y=2u.
Definition (Lean source)
Normalized Haar probability on the period-two torus.
Definition (Lean source)
The explicit torus measure has total mass one.
Definition (Lean source)
Increasing finite integer frequency boxes.
Fourier characters in L² for the explicitly chosen normalized torus measure.
Definition (Lean source)
Complete orthonormal Fourier characters, Parseval, and L² box convergence. Citation: Nikhil Bansal and Haotian Jiang (2024), §2.2, the Parseval display after the Fourier-series formula; arXiv:2408.06475v1. Classical Fourier theory as recalled there. Source checked separately; no pointwise convergence assertion is imported.
Definition (Lean source)
The cited torus Parseval gate follows from Mathlib's Fourier basis and cofinal finite boxes. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Normalized quadratic real-interpolation norm squared.
An endpoint norm on the ambient space, infinite outside the embedded Banach space.
Definition (Lean source)
Exact exponent θ for common linear operators between compatible Banach pairs, with the normalized quadratic K norm. Completeness is required at every endpoint. Citation: S. N. Chandler-Wilde, D. P. Hewett, A. Moiola (2015), Theorem 2.2(i), normalization (8)–(9), arXiv:1404.3599v4; that item credits McLean (2000), Theorem B.2. Compatible pairs may be embedded in their Banach sum spaces, as in the source §2.
Definition (Lean source)
The exact operator interpolation proposition follows from the generic normalized theorem.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
[ Weighted L² norm on measurable functions modulo null sets.
Definition (Lean source)
Weighted L² real interpolation with exactly equal normalized norms. Infinite values encode membership equivalently as well as the equality of finite norms. Citation: S. N. Chandler-Wilde, D. P. Hewett, A. Moiola (2015), Theorem 3.1, arXiv:1404.3599v4, measurable positive finite weights on an arbitrary measure space. The source includes both Lebesgue and counting measures and credits McLean B.4 for an intermediate pointwise minimization; the theorem itself is proved by these authors.
Definition (Lean source)
The weighted L² proposition follows from the generic exact norm identity.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Separability in the product topology of pointwise convergence on S → ℝ: a countable subclass is dense, so every finite set of evaluations can be approximated simultaneously to arbitrary positive accuracy. No norm or sequential density is required.
Expected absolute supremum, with extended nonnegative semantics.
The expected absolute-supremum contraction bound with factor two. Citation: Peter L. Bartlett and Shahar Mendelson (2002), Theorem 12(4), Definition 2, JMLR 3, pp. 464, 469–470, https://www.jmlr.org/papers/volume3/bartlett02a/bartlett02a.pdf. Their proof credits Ledoux–Talagrand (1991), Corollary 3.17. The integrable envelope and separability in the product topology of pointwise convergence (countable density, equivalently simultaneous approximation on each finite evaluation set) specify the function-class scope.
Definition (Lean source)
Probability laws of a single unit's covariate and two potential outcomes.
Definition (Lean source)
Covariate marginal of a single-unit law.
Definition (Lean source)
Conditional midpoint mean, a finite real-valued version modulo covariate null sets.
Definition (Lean source)
Conditional mean treatment effect.
Definition (Lean source)
The law-specific conditional-variance benchmark.
Definition (Lean source)
Actual iid-outcome experiment with covariate-only assignment.
Definition (Lean source)
Actual published HT statistic on iid units and original signs.
Definition (Lean source)
Finite second moments of both potential outcomes.
Definition (Lean source)
Covariate density with fixed strictly positive finite bounds.
Definition (Lean source)
Bounded positive covariate density.
Definition (Lean source)
Actual (real-valued) HT excess above the law's own benchmark.
Definition (Lean source)
Cytrynbaum's actual HT excess-variance identity for fair outcome-independent kernels. Citation: Max Cytrynbaum (2026), Proposition 2.3, equation (2.4), with Assumption 2.1 and Definition 2.2, arXiv:2608.18057v1. The source credits Kallus (2018) for an earlier slightly different imbalance-variance equivalence. Conditional means are modulo null sets. The existing cited carrier retains pointwise fairness; public a.e. fairness is bridged by published_excess_of_ae_fair using a null-equivalent representative.
Definition (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosineDerivative 11 declarations Sine orthogonality supplies the exact derivative energy identity used by the cosine-prior cutoff-extension roadmap.
Spatial derivative energy of finite pair-cosine polynomials
Sine orthogonality supplies the exact derivative energy identity used by the cosine-prior cutoff-extension roadmap. The estimates concern the explicit polynomial, before weak derivatives and Fourier unitarity are applied.
Positive sine modes have the same diagonal unit-interval inner products as cosine modes. Under the stated conditions.
Formal statement
Proof (Lean source)
The pair mode with one sine factor, normalized on the unit square.
Each coordinate's differentiated modes are orthonormal under cube probability. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Finite linear combinations of integrable orthonormal real modes have coefficient energy. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A finite pair-cosine polynomial with arbitrary real coefficients.
The polynomial's squared cube norm is exactly its coefficient energy. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
[ The explicit partial derivative polynomial in either coordinate.
Definition (Lean source)
The coordinate partial energy is exactly the corresponding squared frequency sum.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
The explicit partial polynomial is the ordinary derivative along its coordinate slice.
Formal statement
Proof (Lean source)
Each coordinate derivative costs at most the squared largest frequency times coefficient energy.
Formal statement
Proof (Lean source)
The two partial energies together obey the roadmap's dimension-two gradient bound.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosineEnergy 7 declarations The cosine-prior roadmap interpolates its zero- and first-order whole-space energy estimates by Hölder's inequality.
Fractional Fourier energy of cutoff extensions
The cosine-prior roadmap interpolates its zero- and first-order whole-space energy estimates by Hölder's inequality. This file proves that step for the paper's angular-frequency transform, including zero-energy and endpoint cases. The weak-derivative identities and endpoint estimates remain separate obligations.
The angular-frequency transform equals Mathlib's transform at the rescaled frequency, with the unitary normalization.
Formal statement
Proof (Lean source)
[ An integrable extension has a continuous angular-frequency Fourier transform. This uses the hG hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The squared whole-space Fourier energy at a local Sobolev exponent.
Definition (Lean source)
The weighted real energy density factors into nonnegative extended-real factors.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Hölder interpolates the zero- and first-order extension energies, including both endpoints and zero energy. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Zero-order energy at most A and first-order energy at most A times the squared cutoff give fractional energy at most A times the cutoff to power twice the smoothness. Under the stated conditions.
Formal statement
Proof (Lean source)
The roadmap's two endpoint estimates for the explicit cutoff extension imply the required pair restriction bound; the endpoint estimates are explicit remaining proof obligations. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosineExtension 35 declarations The roadmap's piecewise affine cutoff is one on the cube and zero outside [-1,2].
Explicit whole-space extensions of the cosine prior
The roadmap's piecewise affine cutoff is one on the cube and zero outside [-1,2]. Its product gives continuous compactly supported extensions of the canonical pair polynomials, admissible in the restriction-norm infimum. The weak-derivative and weighted Fourier-energy bounds remain separate obligations.
[ The piecewise affine cutoff with plateau [0,1] and support [-1,2].
The cutoff is continuous, including at every joining point. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The cutoff takes values between zero and one everywhere.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
The plateau agrees exactly with one on the closed unit interval. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
On the left ramp the cutoff has slope one. Under the stated conditions.
Formal statement
Proof (Lean source)
On the right ramp the cutoff has slope minus one. Under the stated conditions.
Formal statement
Proof (Lean source)
Outside the larger closed interval the cutoff vanishes. Under the stated conditions.
Formal statement
Proof (Lean source)
The cutoff is a contraction on the whole real line. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
On the open left ramp the cutoff has derivative one. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
On the open plateau the cutoff has derivative zero. Under the stated conditions.
Formal statement
Proof (Lean source)
On the open right ramp the cutoff has derivative minus one. Under the stated conditions.
Formal statement
Proof (Lean source)
Outside the support interval the cutoff has derivative zero. Under the stated conditions.
Formal statement
Proof (Lean source)
The cutoff is differentiable away from its four joining points. Under the stated conditions.
Formal statement
Proof (Lean source)
The four joining points form a null set, so the cutoff is differentiable almost everywhere. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The derivative is bounded by one, including Lean's zero value at nondifferentiable points.
Formal statement
Proof (Lean source)
[ The product cutoff in the two component coordinates.
Definition (Lean source)
The product cutoff is continuous. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The product cutoff is between zero and one.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Differentiating the first coordinate slice gives the first product-rule term. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Differentiating the second coordinate slice gives the second product-rule term. Under the stated conditions.
Formal statement
Proof (Lean source)
The squared Euclidean length of the two cutoff partial derivatives is at most two. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The product cutoff equals one on the closed Euclidean unit cube. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A nonzero product cutoff forces both coordinates into [-1,2]. Under the stated conditions.
Formal statement
Proof (Lean source)
The product cutoff has compact support in the whole Euclidean plane. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
[ Multiply a cube formula by the roadmap's product cutoff to extend it globally.
Definition (Lean source)
Continuous component formulas give continuous cutoff extensions. This uses the hg hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The extension vanishes outside the support of the fixed product cutoff.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
On the closed cube the extension is the original formula, including its boundary. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A continuous pair formula has a valid integrable, square-integrable extension in the defining infimum of the restriction norm. Under the stated conditions.
Formal statement
Proof (Lean source)
[ The canonical pair effects of every cosine-prior realization are continuous formulas. This uses the hjl hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Every canonical pair polynomial has an explicit admissible whole-space extension.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Any admissible whole-space extension bounds the restriction-norm infimum by its own weighted Fourier energy. Under the stated conditions.
Formal statement
Proof (Lean source)
The explicit cutoff extension can be used directly to bound every canonical pair restriction norm of the prior. Under the stated conditions.
Formal statement
Proof (Lean source)
The zero formula has zero restriction energy, using the zero extension. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The main effects contribute no restriction energy to any cosine-prior realization.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosineFourierEndpoints 4 declarations The proved slice integration-by-parts identity and nine-cell spatial bounds instantiate angular Plancherel with the exact one-half gradient normalization.
Fourier endpoints for the explicit cosine cutoff extension
The proved slice integration-by-parts identity and nine-cell spatial bounds instantiate angular Plancherel with the exact one-half gradient normalization.
[ The paper and library angular Fourier definitions have identical normalization and kernel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Product-coordinate and Euclidean nonnegative integrals agree with Jacobian one.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The cutoff extension obeys both angular Fourier endpoint bounds with the paper's constants. Under the stated conditions.
Formal statement
Proof (Lean source)
The explicit cutoff certifies the pair restriction bound for arbitrary coefficients, without any endpoint assumptions. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosineLegality 7 declarations The canonical pair coefficients instantiate the proved cutoff restriction bound.
Pooled legality of the normalized cosine prior
The canonical pair coefficients instantiate the proved cutoff restriction bound.
Summing prior coordinates is equivalent to summing ordered pairs and local frequencies.
Formal statement
Proof (Lean source)
Each canonical pair effect is the local polynomial with its normalized sign coefficients. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A local array of normalized signs has squared coefficient energy equal to its cardinality. Under the stated conditions.
Formal statement
Proof (Lean source)
The ordered-coordinate sum of a common pair budget counts each pair exactly once. Under the stated conditions.
Formal statement
Proof (Lean source)
The pooled real coefficient normalization is exactly one. Under the stated conditions.
Formal statement
Proof (Lean source)
Every prior realization satisfies the pooled restriction budget. Under the stated conditions.
Formal statement
Proof (Lean source)
Every coefficient realization is legal, and all pair features are jointly isotropic, including pairs sharing a coordinate. This uses the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosinePrior 29 declarations Legality is a conclusion over the constructed polynomial, never a free assumption.
Legal cosine priors and pair-feature isotropy
Legality is a conclusion over the constructed polynomial, never a free assumption. The fixed normalization is independent of every sample and dimension parameter.
Positive integer cosine frequencies have zero mean on the unit interval. Under the stated conditions.
Formal statement
Proof (Lean source)
Integer cosine frequencies integrate to the constant-frequency indicator. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The one-dimensional positive-frequency cosine inner products are exactly diagonal. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every pair-cosine feature is Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Pair-cosine features are bounded by two on the entire ambient space. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every pair feature is square-integrable under cube sampling.
Formal statement
Proof (Lean source)
Distinct cube coordinates factor the mean of two scalar functions. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Pair features are centered, including when the ambient dimension is larger than two. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Features on one original coordinate pair have diagonal frequency inner products. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A coordinate appearing in only one pair makes the two features orthogonal. Under the stated conditions.
Formal statement
Proof (Lean source)
All pair-cosine coordinates are jointly isotropic under the cube law. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The feature index really has the prescribed dimension, including pairs that share an original coordinate.
Formal statement
Proof (Lean source)
The feature inner product extracts a coefficient from any finite cosine expansion.
Formal statement
Proof (Lean source)
The squared energy of a finite pair-cosine polynomial is its coefficient energy.
Formal statement
Proof (Lean source)
Fixing one coordinate of a pair feature leaves a centered factor to integrate out.
Formal statement
Proof (Lean source)
Fixing coordinates in a finite feature sum preserves integrability.
Formal statement
Proof (Lean source)
A canonical pair marginal retains exactly the feature on that ordered coordinate pair. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The finite pair marginals of a cosine expansion are well-defined integrals. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Uniform-draw transport preserves the pair-feature inner products of any original unit. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Finite coefficient realizations of the prior are Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Finite coefficient realizations of the prior are square-integrable. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The coefficient prior is centered for each fixed sign realization.
Formal statement
Proof (Lean source)
The canonical main effects of every prior realization vanish.
Formal statement
Proof (Lean source)
Canonical pair effects of the prior are its polynomials on the corresponding pair. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every cosine-prior realization has exactly its canonical order-two decomposition. Under the stated conditions.
Formal statement
Proof (Lean source)
Each prior realization has exactly the squared energy fixed by its normalization. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The prior has a positive number of coordinates at every admitted dimension and cutoff. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The normalized prior has reciprocal cutoff energy, independently of its signs or dimension. Under the stated conditions.
Formal statement
Proof (Lean source)
The coefficient normalization supplies exactly one unit of the pooled extension budget. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosineSpatialEnergy 15 declarations Exact trigonometric orthogonality on the three-unit interval gives the nine-cell polynomial and gradient estimates used by the cosine-prior extension.
Spatial energy on the cutoff support square
Exact trigonometric orthogonality on the three-unit interval gives the nine-cell polynomial and gradient estimates used by the cosine-prior extension.
[ Lebesgue measure on the nine unit cells containing the cutoff support.
Definition (Lean source)
Integer cosine modes integrate to zero over three complete unit cells.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Cosine orthogonality on the three-cell support interval has diagonal energy three halves. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Sine orthogonality on the three-cell support interval has diagonal energy three halves. Under the stated conditions.
Formal statement
Proof (Lean source)
Fubini factors a product on the cutoff support square into its two interval integrals. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Continuous functions are integrable on the compact cutoff support square. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Pair-cosine modes have diagonal energy nine on the cutoff support square. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Differentiated modes have diagonal energy nine on the cutoff support square.
Formal statement
Proof (Lean source)
The exact polynomial energy over all nine support cells is nine times coefficient energy. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The exact partial energy on the nine support cells keeps the squared coordinate frequency.
Formal statement
Proof (Lean source)
Each partial costs at most nine times squared cutoff frequency times coefficient energy.
Formal statement
Proof (Lean source)
The support-square gradient energy is bounded without an ambient-dimension factor.
Formal statement
Proof (Lean source)
A nonnegative energy density supported on the cutoff square has the same integral under ambient Lebesgue measure and the support-square measure. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The cutoff polynomial has whole-space squared energy at most nine times coefficient energy. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The weak product derivatives have whole-space gradient energy bounded by the exact nine-cell polynomial energies.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.CosineWeakDerivative 22 declarations The piecewise affine cutoff has an integrable derivative.
Integration by parts for the cosine-prior cutoff
The piecewise affine cutoff has an integrable derivative. Splitting at its joining points proves integration by parts for a cutoff times a smooth formula: the shared boundary terms cancel and the exterior boundary terms vanish. This supplies the one-dimensional face-cancellation step of the weak-derivative roadmap, without imposing a periodic boundary condition.
The cutoff derivative is integrable on every finite interval.
Formal statement
Proof (Lean source)
The cutoff vanishes at the two exterior faces of its support interval.
Formal statement
Proof (Lean source)
On a single smooth piece, the derivative of the cutoff product has the usual product rule. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The cutoff product rule holds almost everywhere, including across its joins. Under the stated conditions.
Formal statement
Proof (Lean source)
The candidate product derivative is integrable on any finite interval when the formula has a continuous derivative. Under the stated conditions.
Formal statement
Proof (Lean source)
Integration by parts for a cutoff product on a piece where the cutoff is differentiable. Under the stated conditions.
Formal statement
Proof (Lean source)
Integration by parts across all three pieces cancels the interior faces; the exterior faces contribute zero. This is the weak product rule tested on a smooth function. Under the stated conditions.
Formal statement
Proof (Lean source)
The derivative vanishes outside the cutoff's support interval. Under the stated conditions.
Formal statement
Proof (Lean source)
On the whole real line the cutoff product satisfies integration by parts, with no boundary restriction on either smooth factor. Under the stated conditions.
Formal statement
Proof (Lean source)
[ The finite cosine polynomial is continuous on the whole coordinate plane. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Each explicit partial polynomial is continuous on the whole coordinate plane. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The cutoff's coordinate partial, using the almost-everywhere scalar derivative.
Definition (Lean source)
The roadmap's explicit weak partial derivative of the cutoff cosine polynomial.
Definition (Lean source)
On every coordinate slice the explicit pair partial is a weak derivative of the cutoff extension. The smooth test function need not vanish at the cutoff's joins.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Each cutoff partial has absolute value at most one. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The explicit extension partial is dominated by continuous polynomial magnitudes.
Formal statement
Proof (Lean source)
The extension partial vanishes when either coordinate is outside the support square. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The candidate partial has compact support in the Euclidean plane. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The explicit weak partial is in every Lp space, in particular L1 and L2: it is measurable, compactly supported, and bounded by a continuous envelope on that support. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Both analytic integrability obligations for the weak partial follow from its Lp regularity. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The two explicit cutoff partials have total squared length at most two.
Formal statement
Proof (Lean source)
The product rule and the squared triangle inequality give the roadmap's pointwise gradient estimate before integration.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.GaussianMoments 11 declarations The sinusoidal treatment effect has variance delta squared.
Treatment-effect and selected-noise moments
The sinusoidal treatment effect has variance delta squared. Independent original units give the sample-mean variance, and selected Gaussian errors have zero mean and variance four over n for every fixed assignment. These are the moment steps of HT transfer.
The squared sine integrates to one half over a full uniform period.
Proof (Lean source)
The treatment effect is square integrable by its uniform bound. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The frozen treatment-effect variance is delta squared. Under the stated conditions.
Formal statement
Proof (Lean source)
Independence of the original covariates gives the sample-average effect variance. Under the stated conditions.
Formal statement
Proof (Lean source)
A fixed selected unit error has a finite second moment. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Each selected standard Gaussian error is centered for either treatment sign.
Formal statement
Proof (Lean source)
Selection and the treatment sign preserve the unit noise variance.
Formal statement
Proof (Lean source)
The selected-noise contribution is centered for every fixed original assignment.
Formal statement
Proof (Lean source)
Independent unit errors yield exactly four over n selected-noise variance.
Formal statement
Proof (Lean source)
The entire selected-noise contribution has a finite second moment.
Formal statement
Proof (Lean source)
Centering turns the selected-noise variance into its exact second moment.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.GaussianTarget 10 declarations Uniform sinusoidal effects have mean tau0, and the independent Gaussian contrasts have mean zero.
Mean of the frozen Gaussian causal completion
Uniform sinusoidal effects have mean tau0, and the independent Gaussian contrasts have mean zero. The calculation uses the actual pre-assignment schedule.
A full sine period has zero mean under the uniform unit interval.
Proof (Lean source)
The bounded sinusoidal treatment effect is integrable under cube sampling. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Uniform covariates give the stipulated average treatment effect. Under the stated conditions.
Proof (Lean source)
Both coordinates of each original-unit Gaussian noise have finite first moments. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Independent centered Gaussian noise gives a zero mean unit contrast.
Formal statement
Proof (Lean source)
The Gaussian schedule kernel is a probability kernel. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A noise envelope uniform in covariates gives integrability after Gaussian completion. Under the stated conditions.
Formal statement
Proof (Lean source)
The finite-population contrast cancels the prognostic function pointwise. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual pre-assignment finite-population target is integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
Averaging the frozen Gaussian schedule gives the specified target tau0. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.HTConditionalMoments 22 declarations The actual HT statistic decomposes into treatment effects, prognostic imbalance, and selected Gaussian noise.
Conditional Gaussian HT moments
The actual HT statistic decomposes into treatment effects, prognostic imbalance, and selected Gaussian noise. Fair full-schedule and Gaussian conditional moments supply the pointwise identities used in the joint-experiment variance calculation.
[ Actual Gaussian HT excess for a fixed prognostic function.
Definition (Lean source)
Fixed-function Gaussian actual HT worst excess.
Definition (Lean source)
Minimax Gaussian actual HT excess, with the fixed-function supremum outside sampling.
Definition (Lean source)
The actual HT estimator splits into the realized target and signed midpoints.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Substituting the causal completion gives the sample-average treatment effect, prognostic imbalance, and selected Gaussian-noise contribution in the roadmap. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Under a fair finite sign law the signed midpoint sum has expectation zero. Under the stated conditions.
Formal statement
Proof (Lean source)
Fairness gives fixed-schedule HT unbiasedness for an arbitrary dependent sign law. Under the stated conditions.
Formal statement
Proof (Lean source)
Expanding the signed midpoint square yields the full double covariance sum. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The exact fixed-schedule HT covariance identity uses fairness but no independence between the assignment coordinates. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Conditional on any realized schedule, a fair original-sample design is unbiased and has the exact midpoint covariance quadratic form. Under the stated conditions.
Formal statement
Proof (Lean source)
Cauchy–Schwarz bounds every signed sum by the sum of the unitwise squares. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Square-integrable prognosis has finite imbalance loss for every Markov design. The bound is uniform over all sign laws and does not require fairness.
Formal statement
Proof (Lean source)
For a fixed covariate array and assignment, the completed HT statistic has finite second moment over the pre-assignment Gaussian noise. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Averaging the actual completed HT statistic over noise leaves precisely the sample treatment effect and the signed prognostic imbalance. Under the stated conditions.
Formal statement
Proof (Lean source)
Conditional on the original covariates and signs, the only remaining variance of the completed HT statistic is the selected-noise variance, four over n. Under the stated conditions.
Formal statement
Proof (Lean source)
Centering by any deterministic target, the conditional Gaussian second moment is the squared conditional bias plus four over n. This directly removes both noise cross terms in the HT roadmap. Under the stated conditions.
Formal statement
Proof (Lean source)
Fair assignment removes the covariance between any fixed covariate statistic and its signed prognostic imbalance. No independence between signs is needed. Under the stated conditions.
Formal statement
Proof (Lean source)
Integrating the conditional noise second moment against a fair assignment law leaves the treatment-effect square, the imbalance square, and four over n. Under the stated conditions.
Formal statement
Proof (Lean source)
[ The actual HT statistic is Borel in the full schedule for each fixed assignment. This uses the stated conclusion.
Formal statement
Proof (Lean source)
A finite assignment space permits exchanging assignment and noise integrals once each fixed-assignment noise statistic is integrable.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
For a realized original sample, integrating the actual pre-assignment schedule kernel and then any fair assignment kernel gives the sample treatment-effect mean. Under the stated conditions.
Formal statement
Proof (Lean source)
The conditional full-schedule Gaussian kernel has the exact centered second moment used by the HT transfer, with no hidden conditional moment assumption. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.HTTransfer 12 declarations The conditional moments integrate over the original covariates to give the actual HT mean, finite second moment, and exact excess-variance identity.
Gaussian HT joint-experiment variance transfer
The conditional moments integrate over the original covariates to give the actual HT mean, finite second moment, and exact excess-variance identity.
The sample-average treatment effect has a finite second moment. Under the stated conditions.
Formal statement
Proof (Lean source)
Averaging the independent uniform units preserves the population treatment mean. Under the stated conditions.
Formal statement
Proof (Lean source)
The centered sample treatment-effect square contributes delta squared over n. Under the stated conditions.
Formal statement
Proof (Lean source)
The conditional imbalance second moment is integrable over original samples. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Taking the real value of the loss gives its iterated real second moment.
Formal statement
Proof (Lean source)
Integrating the fair conditional Gaussian square over covariates yields exactly its treatment variation, prognostic loss, and selected-noise contribution. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
[ The finite assignment space makes the actual statistic jointly Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Each fixed assignment has an integrable centered square under its Gaussian schedule.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The actual joint experiment has a finite centered HT second moment. Under the stated conditions.
Formal statement
Proof (Lean source)
The fair Gaussian joint experiment is centered at the population treatment effect. Under the stated conditions.
Formal statement
Proof (Lean source)
Fair outcome-independent assignment is conditionally unbiased and, for any centered square-integrable prognosis, its Gaussian actual HT excess above 4.01 equals the expected prognostic imbalance loss. This uses the hContraction_of_gate hypothesis, the hn hypothesis, the hd hypothesis, the hfair hypothesis, the hindep hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Fair outcome-independent assignment is conditionally unbiased and, for every prognosis in the bivariate Sobolev class, its Gaussian actual HT excess above 4.01 equals the expected prognostic imbalance loss. This uses the hContraction_of_gate hypothesis, the hn hypothesis, the hd hypothesis, the hs hypothesis, the hs1 hypothesis, the hm hypothesis, the hfair hypothesis, the hindep hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.IsotropicSigning 21 declarations Coordinate second moments control isotropic norms and projections.
Isotropic row signing lower bound
Coordinate second moments control isotropic norms and projections. Direct pairwise
moment bounds handle at most 256 rows. These results support the full signing theorem
assembled in SigningPartition, without coordinate independence.
Coordinate second moments make the squared Euclidean norm integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
The diagonal energy of one isotropic row is exactly its dimension. Under the stated conditions.
Formal statement
Proof (Lean source)
Independent rows have expected diagonal energy equal to sample size times dimension. Under the stated conditions.
Formal statement
Proof (Lean source)
Expected minimum signing energy is diagonal energy minus at most the expected maximum off-diagonal fluctuation, the final subtraction in the proof roadmap. Under the stated conditions.
Formal statement
Proof (Lean source)
Expand a squared real Euclidean inner product into coordinate moment products. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Coordinate L² moments suffice to integrate every squared fixed-direction projection. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Isotropy controls all fixed-direction projections without coordinate independence. Under the stated conditions.
Formal statement
Proof (Lean source)
The squared inner product of independent isotropic rows is integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
Independent isotropic rows have squared inner-product expectation equal to dimension. Under the stated conditions.
Formal statement
Proof (Lean source)
The mean absolute projection is at most the length of its fixed direction. Under the stated conditions.
Formal statement
Proof (Lean source)
The mean absolute inner product of independent isotropic rows is at most √r. Under the stated conditions.
Formal statement
Proof (Lean source)
Two distinct evaluation rows have the original product law. Under the stated conditions.
Formal statement
Proof (Lean source)
The pairwise absolute moment bound applies to any two distinct sample rows. Under the stated conditions.
Formal statement
Proof (Lean source)
The triangle inequality bounds every off-diagonal signing by the sum of pair magnitudes. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Summing distinct-pair moments controls the maximum fluctuation directly, without contraction; the loose n² count also includes the zero diagonal terms. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Direct pairwise second moments give a contraction-free signing bound for all sample sizes, useful before the sharper large-sample argument is available. Under the stated conditions.
Formal statement
Proof (Lean source)
For at most 256 rows, the direct pair count fits within the paper's 16n√(nr) error allowance. Under the stated conditions.
Formal statement
Proof (Lean source)
The small-sample portion of the headline follows directly from isotropic pair moments and diagonal subtraction, with no contraction premise. Under the stated conditions.
Formal statement
Proof (Lean source)
For two rows, the four signings reduce exactly to the diagonal energy minus twice the absolute inner product, as in the roadmap's smallest-sample check. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The complete two-row signing lower bound follows from the independent inner-product moment, with the sharper error 2√r from the roadmap's check. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
At the prescribed dimension threshold, the two error terms consume at most half of the diagonal energy. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.LowerConverse 2 declarations A positive comparison-scale lower bound forces the square-root dimension condition, even when the risks are extended real and the dimension sequence oscillates.
Lower constants and the dimension converse
A positive comparison-scale lower bound forces the square-root dimension condition, even when the risks are extended real and the dimension sequence oscillates.
The sharper lower constant dominates its positive endpoint value. Under the stated conditions.
Formal statement
Proof (Lean source)
Vanishing extended-real risks bounded below by the comparison scale require sub-square-root dimension growth. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.OrderedRounding 1 declarations The Borel component is assembled from the finite arithmetic and changing-basis proofs.
Ordered boundary rounding guarantee
The Borel component is assembled from the finite arithmetic and changing-basis proofs. Finite termination follows from the active trace and phase invariant; fairness follows by successive fresh-seed integration. Exact direction-lottery covariance, test-row variance, norm-energy increments, and localized projection contraction, exact active-rank counts, and retained-row invariance are proved; finite move-moment accumulation and the geometric phase allowance are proved; predictably selected actual moves have additive moments and exact interval energy budgets; measurable predictable halving intervals partition the actual trace. The row budget follows from the uniform move comparison and the energy telescope after the first loss of protection.
Ordered boundary rounding is Borel, terminates within n moves, is fair, and controls every prefix row without a full-rank or general-position assumption. This uses the hrows hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.OrderedRoundingCore 41 declarations Exact finite arithmetic, ordered Gram--Schmidt, half-open inverse-CDF choices, and a structural n-step iteration implement the prescribed procedure.
Ordered boundary rounding
Exact finite arithmetic, ordered Gram--Schmidt, half-open inverse-CDF choices, and a structural n-step iteration implement the prescribed procedure. The fractional terminal state is retained separately so termination is a substantive proof obligation.
[ Euclidean dot product on the original coordinates.
Definition (Lean source)
Subtract rank-one projections onto an ordered orthonormal list.
One ordered Gram--Schmidt insertion, discarding zero residuals.
Structural ordered Gram--Schmidt; no well-founded recursion enters the algorithm.
Definition (Lean source)
Active coordinates in increasing original-unit order.
Restrict a vector to active coordinates.
First q restricted constraints, including zero rows outside the supplied prefix.
Definition (Lean source)
The projection onto the active-coordinate nullspace of the retained prefix.
Definition (Lean source)
Process projected standard basis vectors in index order.
Definition (Lean source)
Finite minimum, in original index order.
The positive boundary-hit distance along a nonzero active direction.
Definition (Lean source)
The negative boundary-hit distance.
Definition (Lean source)
Select with half-open cumulative intervals; seed one selects the last interval.
Definition (Lean source)
One asymmetric boundary move with direction weights proportional to 1/(δ⁺δ⁻).
Definition (Lean source)
State is (fractional vector, phase stopping count, retained constraint count).
Definition (Lean source)
A move preserves the phase prefix until the phase stopping count is reached. Only at a new phase start is an active count at most three independently rounded, one coordinate per move with its own seed.
Definition (Lean source)
Uniform independent seeds, represented as 3n coordinates.
Definition (Lean source)
Read a seed; out-of-range padding is never used during the n actual moves.
Definition (Lean source)
Structural k-step fractional-state iteration.
Definition (Lean source)
The prescribed finite exact-real randomized signing map.
Definition (Lean source)
Independent uniform seed law.
Definition (Lean source)
Prefix supplied to the algorithm; rows are numbered starting at one.
Active membership is exactly strict interior membership of the coordinate.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Taking a finite nonempty minimum preserves strict positivity. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A nonempty finite minimum is one of the entries and is no larger than any entry. Under the stated conditions.
Formal statement
Proof (Lean source)
A nonzero direction supported inside the active coordinates has positive positive boundary distance; sign guards keep every candidate denominator positive. Under the stated conditions.
Formal statement
Proof (Lean source)
Moving by the positive boundary distance stays inside the cube and hits a boundary. This uses the actual finite minimum, without a symmetry or generic-position assumption. Under the stated conditions.
Formal statement
Proof (Lean source)
Reversing a nonzero active direction gives a positive negative boundary distance. Under the stated conditions.
Formal statement
Proof (Lean source)
The asymmetric boundary coin is a probability strictly between zero and one. Under the stated conditions.
Formal statement
Proof (Lean source)
The prescribed asymmetric coin makes each direction increment mean zero. Under the stated conditions.
Formal statement
Proof (Lean source)
The scalar increment variance is exactly the product of the two boundary distances. Under the stated conditions.
Formal statement
Proof (Lean source)
The active-coordinate list has no repetitions. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
A cube move that fixes inactive coordinates and hits a new boundary strictly reduces the active count, regardless of the number of other simultaneous hits. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A positive boundary move fixes inactive coordinates and strictly decreases their count. Under the stated conditions.
Formal statement
Proof (Lean source)
Negative boundary moves have the same cube and progress guarantees by direction reversal. Under the stated conditions.
Formal statement
Proof (Lean source)
Once the selected nullspace direction is nonzero and active-supported, the actual asymmetric rounding step preserves the cube and makes strict progress. Under the stated conditions.
Formal statement
Proof (Lean source)
Setting a coordinate to a boundary value removes exactly that active index. Under the stated conditions.
Formal statement
Proof (Lean source)
A terminal boundary update removes one active coordinate and preserves the cube. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual terminal branch preserves the cube and strictly decreases the active count. Under the stated conditions.
Formal statement
Proof (Lean source)
Terminal single-coordinate rounding preserves its current conditional mean. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The terminal centered increment has variance one minus the current squared coordinate.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.OutcomeLaws 33 declarations Concrete Gaussian completions and the finite-support witness used by the published class bridge, with their probability and conditional-prognosis properties.
Single-unit outcome laws
Concrete Gaussian completions and the finite-support witness used by the published class bridge, with their probability and conditional-prognosis properties.
[ The single-unit Gaussian completion map.
Definition (Lean source)
The single-unit Gaussian completion measure.
Definition (Lean source)
The uniform cube sampling measure has total mass one.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
The concrete Gaussian completion has total mass one. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The Gaussian single-unit completion as a probability law.
Definition (Lean source)
Image of the stated Gaussian completion over legal prognostic functions.
Definition (Lean source)
Two equal ±1 potential outcomes, independent of the uniform covariate.
Definition (Lean source)
The explicit two-point witness has total mass one. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The explicit non-Gaussian completion witness.
Definition (Lean source)
The Gaussian outcome map is Borel for every legal representative. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The completion preserves the uniform covariate marginal. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Both completed potential outcomes have finite second moments. Under the stated conditions.
Formal statement
Proof (Lean source)
[ The conditional Gaussian outcome distribution draws two independent unit noises.
Definition (Lean source)
The explicit conditional outcome distribution is a Markov kernel.
Definition (Lean source)
Disintegrating the completion recovers the explicit conditional Gaussian kernel.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Mean-zero independent Gaussian errors leave the conditional midpoint equal to m. Under the stated conditions.
Formal statement
Proof (Lean source)
The law's pinned conditional prognosis agrees almost everywhere with its input. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Uniform zero-intercept correctly specified published laws.
Definition (Lean source)
The complete prognostic image, saturated under Lebesgue null representatives.
Definition (Lean source)
The outcome class image, saturated under Lebesgue null representatives.
Definition (Lean source)
Gaussian completions belong to the published uniform class with their chosen prognosis.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The Gaussian family is contained in the arbitrary finite-second-moment uniform class. Under the stated conditions.
Formal statement
Proof (Lean source)
The prognostic image is exactly the Sobolev class modulo cube-null changes; every reverse inclusion is witnessed by the prescribed Gaussian completion. Under the stated conditions.
Formal statement
Proof (Lean source)
Zero prognosis has the exact order-two representation and zero pooled budget.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The two-point law is a product of uniform covariates and one fair diagonal sign. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The two-point witness retains uniform covariates.
Formal statement
Proof (Lean source)
Bounded two-point outcomes have finite second moments.
Formal statement
Proof (Lean source)
The fair diagonal sign has zero conditional midpoint expectation.
Formal statement
Proof (Lean source)
The finite-support witness is legal in every uniform Sobolev law class.
Formal statement
Proof (Lean source)
Equal two-point potential outcomes lie on the diagonal with probability one.
Formal statement
Proof (Lean source)
Independent continuous Gaussian errors give the outcome diagonal probability zero. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A law supported on equal two-point outcomes cannot be a Gaussian completion. Under the stated conditions.
Formal statement
Proof (Lean source)
The Gaussian inclusion is strict, witnessed by the legal diagonal two-point law. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.PublishedClass 24 declarations The prognostic function is pinned to each law's conditional kernel.
Published prognostic law classes and exact capacity transfer
The prognostic function is pinned to each law's conditional kernel. The uniform class retains arbitrary square-integrable outcomes; Gaussian completions are a strict subclass. The larger class permits intercepts and fixed covariate-density bounds and receives a converse only. Its original prognostic L² bound is retained.
[ The larger published correctly specified class, with intercepts and a prognostic L² bound.
Definition (Lean source)
Covariate projection of the iid single-unit sample.
Definition (Lean source)
Borel measurability of the covariate projection on the full experiment. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The iid-outcome experiment is a probability law.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Published admissibility: iid pre-assignment schedules, conditional fairness and conditional independence given the observed original covariate array.
Definition (Lean source)
Replacing a design on a cube-null set preserves every iid experiment whose covariate marginal is absolutely continuous with respect to the cube law. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A covariate-only assignment kernel is independent of every outcome mechanism conditional on the covariates, by uniqueness of its conditional distribution. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Pushing the base sample through a Borel observation map commutes with drawing an assignment from a kernel that depends only on that observation. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Assignment conditioned on all sampled outcomes has the same conditional law as assignment conditioned on the observed covariates alone. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Published and research admissibility are the same fairness condition on the same covariate-only Borel kernel; conditional outcome independence follows from its input.
Formal statement
Proof (Lean source)
The cited pointwise carrier transfers to every publicly admissible a.e. fair kernel. Bounded positive densities share the cube's null sets, so representative replacement preserves the iid experiment and both sides of the excess identity. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
[ Nonnegative carrier of the actual law-specific excess, not a surrogate imbalance risk.
Definition (Lean source)
Fixed-law worst excess, outside the experiment expectation.
Definition (Lean source)
Minimax actual excess over a specified class of iid laws.
Definition (Lean source)
A fixed cube-null change of prognosis leaves every finite-sample design loss unchanged.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Uniform outcome laws induce exactly the original covariate/sign experiment. Under the stated conditions.
Formal statement
Proof (Lean source)
Every Markov sign law preserves integrability of the squared finite imbalance. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The finite imbalance loss is the nonnegative real joint second moment.
Formal statement
Proof (Lean source)
The cited excess identity transfers to the original-sample loss for every uniform law with square-integrable Sobolev prognosis; null representatives cause no change. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Equality of prognostic images modulo null sets and the pointwise excess identity identify the fixed-design suprema, without moving a supremum inside an expectation. Under the stated conditions.
Formal statement
Proof (Lean source)
Equal worst risks for every admissible original-sample design give equal capacities by taking the infimum over the common design class. Under the stated conditions.
Formal statement
Proof (Lean source)
Enlarging the law class increases its fixed-design supremum and minimax capacity. Under the stated conditions.
Formal statement
Proof (Lean source)
A uniform law meets all permitted fixed density bounds. Under the stated conditions.
Formal statement
Proof (Lean source)
The frozen published class has exactly the legal prognostic image and full-design capacity; the bounded-density class inherits the all-design converse and vanishing necessity. This uses the hExcess_of_gate hypothesis, the hContraction_of_gate hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionANOVA 16 declarations Independent coordinate resampling preserves cube probability.
Canonical ANOVA regularity and Fourier supports
Independent coordinate resampling preserves cube probability. Fubini then proves centering of canonical main effects and L² regularity of all canonical effects. Translation invariance localizes their Fourier supports, and their integrability gives exact coefficient additivity for the order-two decomposition.
[ Unit-cube Lebesgue measure has total mass one in every dimension.
Definition (Lean source)
Selecting each coordinate from either of two independent cube draws preserves cube probability.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
A Borel representative has a Borel canonical main effect, including at exceptional slices where the Bochner integral is defined to be zero. This uses the hm hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The lifted main marginal of an integrable cube function is integrable. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Integrating a lifted canonical main effect recovers the original cube mean. Under the stated conditions.
Formal statement
Proof (Lean source)
Centering of the original cube outcome centers each lifted canonical main effect. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Averaging independent unused coordinates contracts square integrability. This applies to both one-coordinate and two-coordinate raw marginals. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The lifted canonical main effect is square integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
The raw two-coordinate marginal equals averaging a two-coordinate resampling. Under the stated conditions.
Formal statement
Proof (Lean source)
The lifted canonical pair effect is square integrable, without any regularity premise beyond the original measurable square-integrable outcome. Under the stated conditions.
Formal statement
Proof (Lean source)
A nonzero character coordinate has zero coefficient against a function invariant under shifts in that coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
Reflected main effects have no frequency outside their own coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
Each reflected main effect has zero intercept. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Reflected pair effects have no frequency outside their two coordinates. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The order-two decomposition is additive at each Fourier coefficient; all of its canonical summands have derived L² regularity. Under the stated conditions.
Formal statement
Proof (Lean source)
Additivity and the individual coordinate supports give the ambient order-two support statement directly from the canonical components. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionANOVACentering 15 declarations Fubini and independent coordinate resampling center canonical pair effects in each coordinate.
Canonical pair centering and exact Fourier component separation
Fubini and independent coordinate resampling center canonical pair effects in each coordinate. Folding preserves these identities, so main and pair effects have disjoint exact Fourier supports. The order-two Fourier sum therefore identifies each coefficient with its unique canonical component.
Averaging the second coordinate of a raw pair marginal recovers the main marginal, with integrable slices almost everywhere. Under the stated conditions.
Formal statement
Proof (Lean source)
Swapping the two distinct coordinates and their arguments preserves a canonical pair effect. Under the stated conditions.
Formal statement
Proof (Lean source)
Each canonical pair effect is integrable and centered in its second coordinate for almost every fixed first coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
Each canonical pair effect is integrable and centered in its first coordinate for almost every fixed second coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
The lifted canonical pair effect has zero cube mean. Under the stated conditions.
Formal statement
Proof (Lean source)
[ A Borel outcome has a jointly Borel canonical pair effect, including exceptional slices. This uses the hm hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Each reflected canonical pair effect has zero intercept.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Replacing one torus coordinate by the corresponding coordinate of an independent Haar draw preserves Haar probability. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
A character with zero frequency in a coordinate is unchanged by resampling that coordinate. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A reflected pair coefficient vanishes when its second coordinate frequency is zero, by Fubini and canonical centering. Under the stated conditions.
Formal statement
Proof (Lean source)
A reflected pair coefficient vanishes when its first coordinate frequency is zero. Under the stated conditions.
Formal statement
Proof (Lean source)
Every nonzero reflected canonical pair coefficient has support exactly equal to its two coordinates. Under the stated conditions.
Formal statement
Proof (Lean source)
Every nonzero reflected canonical main coefficient has support exactly equal to its coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
At a singleton-support frequency the full order-two outcome coefficient equals its unique main component coefficient. Under the stated conditions.
Formal statement
Proof (Lean source)
At an ordered pair-support frequency the full order-two outcome coefficient equals its unique pair component coefficient. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionBudget 2 declarations The component contraction and pooled ANOVA bound for the even reflected extension.
Exact pooled reflection budget
The component contraction and pooled ANOVA bound for the even reflected extension.
[ Exact component reflection contraction and its pooled ANOVA consequences. Parseval and interpolation have proved witnesses; no periodic cube boundary condition is assumed. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The pooled reflection estimate controls the original-cube second moment.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionBudgetTransport 10 declarations Folding sends normalized Haar measure exactly to cube probability.
Cube transport and the zero Fourier coefficient
Folding sends normalized Haar measure exactly to cube probability. This gives representative-independent reflection and the centered zero-frequency identity.
Folding the independently reflected cube sample recovers its original point almost surely.
Formal statement
Proof (Lean source)
Normalized Haar measure folds to unit-cube Lebesgue probability in every dimension.
Formal statement
Proof (Lean source)
Reflection preserves almost-everywhere equality of cube representatives. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The zero Fourier coefficient of a reflected centered outcome vanishes. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every cube L² representative reflects to a torus L² representative, with no centering requirement. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Parseval and folding identify the full Fourier mass with the cube second moment. Under the stated conditions.
Formal statement
Proof (Lean source)
Centered outcomes inherit the full cube Parseval identity. Under the stated conditions.
Formal statement
Proof (Lean source)
The zero-smoothness endpoint is exactly cube L² energy under normalized Haar measure. Under the stated conditions.
Formal statement
Proof (Lean source)
Nonnegative smoothness weights are at least one, so the pooled spectral budget controls the full Fourier mass when the excluded coefficients vanish. Under the stated conditions.
Formal statement
Proof (Lean source)
Once the pooled spectral estimate and its support statement are proved, Parseval supplies the original-cube second-moment bound without a dimension factor. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionCoefficientTransport 16 declarations Selecting distinct coordinates preserves cube and Haar probability.
Local-to-ambient canonical Fourier coefficients
Selecting distinct coordinates preserves cube and Haar probability. Characters supported on those coordinates transport exactly, with normalized coefficients and no factor depending on the ambient dimension.
A selection of distinct coordinates preserves finite product probability. Under the stated conditions.
Formal statement
Proof (Lean source)
Selecting distinct coordinates sends ambient Haar probability to local Haar probability. Under the stated conditions.
Formal statement
Proof (Lean source)
Selecting distinct coordinates sends ambient cube probability to local cube probability. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Folding commutes pointwise with selection of coordinates. This uses the stated conclusion.
Formal statement
Proof (Lean source)
A character supported on selected coordinates is exactly the corresponding local character.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Normalized reflected Fourier coefficients transport from local to ambient coordinates. Under the stated conditions.
Formal statement
Proof (Lean source)
Selecting the supporting coordinates preserves the squared Euclidean frequency length. Under the stated conditions.
Formal statement
Proof (Lean source)
When all selected coordinates are active, ambient support has exactly local size. Under the stated conditions.
Formal statement
Proof (Lean source)
The ambient complexity equals local squared length divided by local dimension. Under the stated conditions.
Formal statement
Proof (Lean source)
The one-coordinate canonical representative is square integrable under local cube measure. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The two-coordinate canonical representative is square integrable under local cube measure. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A canonical main coefficient on its supporting coordinate equals its local coefficient. Under the stated conditions.
Formal statement
Proof (Lean source)
A canonical pair coefficient on its two supporting coordinates equals its local coefficient. Under the stated conditions.
Formal statement
Proof (Lean source)
Disjoint-support localization transports a lifted component's entire weighted budget into its local Fourier budget, with constant one. Under the stated conditions.
Formal statement
Proof (Lean source)
The ambient weighted budget of a canonical main effect is bounded by its local budget. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The ambient weighted budget of a canonical pair effect is bounded by its local budget. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionDefinitions 9 declarations Definitions fix the period-two folding map, reflected extension, frequency complexity, and component and pooled Fourier budgets, independently of the budget proofs.
Even reflection and the exact pooled Fourier budget
Definitions fix the period-two folding map, reflected extension, frequency complexity, and component and pooled Fourier budgets, independently of the budget proofs.
Fold y=2u to the closed unit cube, using the half-open representative of u.
Even period-two extension.
Definition (Lean source)
Characters of the period-two torus.
Normalized Fourier coefficients of the reflected function.
Integer frequencies with their actual nonzero coordinate support.
Squared Euclidean length of an integer frequency.
Definition (Lean source)
Complexity of a nonzero frequency, with the harmless value zero at frequency zero.
Definition (Lean source)
Squared weighted torus norm in a fixed component dimension.
Definition (Lean source)
The Fourier budget restricted to support sizes one and two.
Definition (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionEndpointLimit 7 declarations Reflection is continuous on spatial L² classes.
Passage to the reflected spectral endpoint limit
Reflection is continuous on spatial L² classes. Character pairing is continuous on torus L² classes, and finite Fourier sums pass to the limit without losing any part of the weight. These are the completion steps in roadmap (5).
Character pairing expresses each normalized coefficient as an L² inner product.
Formal statement
Proof (Lean source)
Spatial L² convergence implies convergence of each normalized Fourier coefficient.
Formal statement
Proof (Lean source)
A uniform exact weighted Fourier bound survives an L² limit. The proof passes each finite sum to the limit and then takes their supremum. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The genuine smooth inverse truncations converge after even reflection to reflection of the original extension. No periodic trace condition is needed. Under the stated conditions.
Formal statement
Proof (Lean source)
Every admissible whole-space extension has exactly the cube function's reflected equivalence class under the common operator. Under the stated conditions.
Formal statement
Proof (Lean source)
Fourier coefficients of the reflected extension are independent of which admissible whole-space extension was chosen. Under the stated conditions.
Formal statement
Proof (Lean source)
Smooth truncations of any admissible extension recover the specified cube function's Fourier coefficients after reflection, with the exact normalization. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionEndpointZero 12 declarations Angular Plancherel and restriction to the unit cube prove the zero-order reflection contraction for every admissible whole-space extension.
Zero-order reflection endpoint
Angular Plancherel and restriction to the unit cube prove the zero-order reflection contraction for every admissible whole-space extension. Taking the extension infimum also bounds cube L² energy by each nonnegative Sobolev norm.
Euclidean coordinates preserve the restricted unit-cube measure.
Formal statement
Proof (Lean source)
Restricted Euclidean and product-cube nonnegative integrals agree, including infinite values. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every admissible extension has at least the cube's squared L² energy. Under the stated conditions.
Formal statement
Proof (Lean source)
Angular Plancherel gives the exact norm-one zero-order reflection endpoint. Under the stated conditions.
Formal statement
Proof (Lean source)
Nonnegative Sobolev weights dominate the cube energy for every extension; therefore the same bound survives taking the extension infimum. Under the stated conditions.
Formal statement
Proof (Lean source)
The zero-order reflected Fourier mass is bounded by the restriction norm at every nonnegative exponent, with constant one and no attainment assumption. Under the stated conditions.
Formal statement
Proof (Lean source)
Folding into Euclidean coordinates preserves normalized cube measure. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
[ Restriction of whole-space L² equivalence classes to the cube as a linear map.
Definition (Lean source)
The restriction map has norm at most one.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
[ The common even-reflection operator on whole-space L² equivalence classes. Restriction is a contraction and the subsequent folded pullback is an isometry.
Definition (Lean source)
The actual even-reflection L² operator has endpoint norm at most one.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
The L² operator is the genuine folded pullback, independently of representatives.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionFourier 10 declarations The reflected outcome is rewritten on the torus and the original seed integral is transported to independent Haar sample and shift coordinates.
Reflection transport for the Fourier identity
The reflected outcome is rewritten on the torus and the original seed integral is transported to independent Haar sample and shift coordinates. This isolates the remaining Parseval argument.
Folding a lifted coordinate recovers its original value on the closed unit interval. Under the stated conditions.
Formal statement
Proof (Lean source)
Cube probability is supported on the closed unit cube. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The period-two folding map is Borel measurable, including at its endpoints. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The joint law of the shifted sample, common shift, and original outcome values can be written entirely in independent Haar coordinates. The original value at unit i becomes the even reflected extension evaluated at W i - T. This uses the hX hypothesis, the hm hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Every nonnegative measurable functional of the shifted sample, common shift, and original outcome vector can be averaged instead over independent Haar coordinates, with outcomes recovered by folding W i - T. This uses the hX hypothesis, the hm hypothesis, the Φ hypothesis, the hΦ hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Folding normalized Haar measure has the same squared-integral normalization as the unit cube. This is obtained from the reflected sampling law, including its endpoint convention. This uses the hm hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The even reflected extension of a cube L² representative is L² for normalized Haar measure on the torus. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The paper's reflected coefficient is Mathlib's normalized torus Fourier coefficient. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Parseval for a finite complex linear combination of translates by a common Haar shift. The coefficient phase is indexed in the same direction as the Fourier character after reindexing the intermediate formula by k ↦ -k. This uses the hd hypothesis, the hf hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The common-shift Parseval identity in the nonnegative extended-real form used by kernel averages. This uses the hd hypothesis, the hf hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionGradientLimit 8 declarations Finite first-order Fourier energy supplies square-integrable coordinate multipliers.
First-order convergence of the genuine inverse truncations
Finite first-order Fourier energy supplies square-integrable coordinate multipliers. Their inverse L² representatives are the limits of the actual smooth derivatives in roadmap (3), without imposing L¹ regularity on these full multipliers.
Finite first-order energy implies L² membership of each full coordinate multiplier; this regularity is derived rather than assumed. Under the stated conditions.
Formal statement
Proof (Lean source)
Truncation commutes with the coordinate multiplier, so the actual smooth spatial derivative is precisely its inverse Fourier approximation. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every actual smooth coordinate derivative converges to the inverse L² class of its full frequency multiplier. The multiplier's L² regularity follows from the original finite first-order energy. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The limiting coordinate derivative has exactly its full coordinate-weighted frequency energy, even when that multiplier is not L¹. Under the stated conditions.
Formal statement
Proof (Lean source)
The limiting inverse function and all limiting coordinate derivatives have the exact first-order energy from roadmap (3), with local gradient factor 1/p. Under the stated conditions.
Formal statement
Proof (Lean source)
Spatial inverse truncations and their actual coordinate derivatives converge together to the explicit inverse Fourier classes. All derivative regularity is derived from the one finite first-order energy assumption. Under the stated conditions.
Formal statement
Proof (Lean source)
The derivative error relative to its full inverse class has the exact coordinate-weighted truncation error, with no spatial normalization loss. Under the stated conditions.
Formal statement
Proof (Lean source)
Roadmap (3)'s entire first-order squared error tends to zero. This is convergence in the genuine spatial endpoint norm, not only coefficientwise convergence, and keeps the exact local gradient factor 1/p. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionInterpolation 8 declarations The weighted measurable-function minimizer belongs to the ambient L² space when the first-order weight dominates one.
Weighted interpolation on the ambient frequency L² space
The weighted measurable-function minimizer belongs to the ambient L² space when the first-order weight dominates one. Thus restricting the decomposition infimum to L² classes preserves the exact normalized interpolation energy.
The unweighted measurable-function gauge is the ambient L² norm.
Formal statement
Proof (Lean source)
A finite weighted gauge with weight at least one gives ambient L² membership. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The weighted gauge of the zero equivalence class vanishes for any weight. Under the stated conditions.
Formal statement
Proof (Lean source)
Restricting weighted quadratic decompositions to ambient L² classes does not change the K-functional. Finite minimizing costs force both summands into L². Under the stated conditions.
Formal statement
Proof (Lean source)
The normalized K norm on L² classes is exactly the fractional weighted energy, with no enlargement of the ambient space and no loss of constant. Under the stated conditions.
Formal statement
Proof (Lean source)
The frequency first-order gauge agrees with its weighted L² realization. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Source interpolation is precisely the paper's fractional angular Fourier energy, including its local dimension normalization. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The genuine reflection operator's target K energy is bounded by the exact fractional whole-space energy. Both endpoint contractions and the source norm identification enter this estimate with constant one. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionInverseL2 11 declarations Angular Plancherel and the measure-preserving spatial reflection identify the exact spatial energies and differences of the inverse integrals in roadmap step (3).
Spatial L² control of the smooth inverse truncations
Angular Plancherel and the measure-preserving spatial reflection identify the exact spatial energies and differences of the inverse integrals in roadmap step (3).
Angular Fourier transformation commutes with subtraction of L¹ profiles. Under the stated conditions.
Formal statement
Proof (Lean source)
The inverse angular integral of an L¹∩L² profile is square integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
Spatial negation and angular Plancherel preserve the exact inverse-integral energy. Under the stated conditions.
Formal statement
Proof (Lean source)
The inverse-integral squared distance equals the frequency squared distance, including profiles whose inverse integrals need not be L¹. Under the stated conditions.
Formal statement
Proof (Lean source)
Every smooth ball-truncated inverse integral is genuinely in spatial L². Under the stated conditions.
Formal statement
Proof (Lean source)
The smooth inverse approximations have exactly the truncated frequency energy. Under the stated conditions.
Formal statement
Proof (Lean source)
Differences of smooth inverse truncations preserve squared L² distance with constant one. Under the stated conditions.
Formal statement
Proof (Lean source)
The frequency truncations are Cauchy in squared L² energy, jointly in both radii. The domination has constant one because two nested indicators differ only by a sign. Under the stated conditions.
Formal statement
Proof (Lean source)
The smooth inverse integrals are Cauchy in spatial squared L² energy. This uses the exact Plancherel distance identity rather than assuming inverse L¹ regularity. Under the stated conditions.
Formal statement
Proof (Lean source)
The inverse truncations define a Cauchy sequence of actual spatial L² classes. Under the stated conditions.
Formal statement
Proof (Lean source)
Completeness produces the spatial L² limit of the smooth inverse truncations. Identifying this limit with the inverse Fourier class is a separate obligation. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionInverseLimit 18 declarations The normalized reflected Mathlib Fourier representative gives the inverse angular transform on all frequency L² classes.
Identification of the inverse-truncation L² limit
The normalized reflected Mathlib Fourier representative gives the inverse angular transform on all frequency L² classes. Its exact energy and distance identities identify the limit in reflection-budget roadmap (3), without L¹ regularity of the full frequency profile.
[ The inverse angular L² representative is the normalized, dilated, reflected Mathlib Fourier L² transform. The input is a frequency equivalence class.
Definition (Lean source)
The dilation and reflection used by the inverse preserve null sets.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
The inverse angular representative is strongly measurable almost everywhere.
Formal statement
Proof (Lean source)
The squared energy of any L² representative is its squared extended norm.
Formal statement
Proof (Lean source)
Spatial reflection, the exact Jacobian, and Fourier unitarity give the inverse energy with constant one for every L² frequency class.
Formal statement
Proof (Lean source)
The inverse representative has finite L² norm, without an L¹ premise.
Formal statement
Proof (Lean source)
Subtraction of inverse representatives agrees almost everywhere with the inverse of the difference class; the a.e. Fourier identity is pulled through a map that preserves null sets.
Formal statement
Proof (Lean source)
The inverse map preserves the exact squared distance between frequency classes, including profiles with no integrable representative.
Formal statement
Proof (Lean source)
Smooth inverse truncations agree with the inverse L² representative of their frequency truncation class. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The spatial error relative to the full inverse L² class is exactly the frequency truncation error, even when the full frequency profile is not L¹. Under the stated conditions.
Formal statement
Proof (Lean source)
The genuine smooth inverse truncations converge to the explicit inverse Fourier L² class of every measurable square-integrable frequency profile. No integrability assumption on the full frequency profile is used. Under the stated conditions.
Formal statement
Proof (Lean source)
Every completeness limit of the inverse truncations is the explicit normalized reflected Fourier representative for an arbitrary measurable L² profile. This identifies the limit used in roadmap (3). Under the stated conditions.
Formal statement
Proof (Lean source)
L² class norms recover the squared energy of the supplied representative. Under the stated conditions.
Formal statement
Proof (Lean source)
The L² inner product is the genuine sesquilinear integral of representatives. Under the stated conditions.
Formal statement
Proof (Lean source)
Adjoint pairing and Plancherel give the exact spatial error of a smooth inverse truncation of the Fourier profile of an L¹∩L² extension. The full Fourier profile need not be integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual frequency truncation classes converge to the original frequency class in L², using the proved dominated-convergence error estimate. Under the stated conditions.
Formal statement
Proof (Lean source)
The inverse truncations of an extension's angular Fourier profile converge to that very extension in spatial L². Adjoint pairing supplies the cross term and Plancherel supplies both norms, so no Fourier inversion integrability gate is imposed on the untruncated profile. Under the stated conditions.
Formal statement
Proof (Lean source)
The explicit inverse L² representative recovers every admissible extension from its genuine angular Fourier profile. This completes the original-extension identification in reflection-budget roadmap (3). Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionInversePairing 13 declarations Fubini transfers the normalized inverse angular integral to an integrable test function.
Test-function pairing for the inverse truncations
Fubini transfers the normalized inverse angular integral to an integrable test function. This is the adjoint-identification step in reflection-budget roadmap (3).
Absolute integrability of the two-variable inverse pairing kernel. Under the stated conditions.
Formal statement
Proof (Lean source)
Bilinear pairing with an inverse integral transfers the inverse transform to an arbitrary L¹ test. No L¹ assumption on the inverse integral is needed. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual ball-truncated smooth inverse integrals satisfy the test pairing used to identify their spatial L² limit in the endpoint proof. Under the stated conditions.
Formal statement
Proof (Lean source)
Conjugation exchanges the forward angular kernel and the inverse kernel. The real unitary prefactor is unchanged. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Sesquilinear pairing identifies the inverse integral with the adjoint of the angular transform on integrable tests. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The smooth truncations obey the exact adjoint pairing, with the genuine Fourier ball cutoff and the paper's unitary angular normalization. Under the stated conditions.
Formal statement
Proof (Lean source)
The inverse integral of an L¹∩L² frequency profile agrees with the reflected, normalized dilation of Mathlib's actual Fourier L² representative. Pulling the a.e. identity through negation is justified by measure preservation. Under the stated conditions.
Formal statement
Proof (Lean source)
Each constructed truncation has the L² representative required for adjoint identification; no integrability of its spatial inverse is assumed. Under the stated conditions.
Formal statement
Proof (Lean source)
Unweighted frequency truncation error vanishes for every measurable L² profile. Under the stated conditions.
Formal statement
Proof (Lean source)
For an L¹∩L² profile the spatial error relative to its actual inverse integral has exactly the frequency truncation error, with unit constant. Under the stated conditions.
Formal statement
Proof (Lean source)
The smooth inverses converge in squared spatial L² error to the actual inverse integral whenever the profile is L¹∩L². Under the stated conditions.
Formal statement
Proof (Lean source)
The limit in spatial L² is the class of the genuine inverse integral, rather than an unidentified completeness witness, for L¹∩L² profiles. Under the stated conditions.
Formal statement
Proof (Lean source)
Any spatial L² limit produced by completeness has the normalized reflected Mathlib Fourier representative for an L¹∩L² frequency profile. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionKernel 3 declarations Tonelli transports an arbitrary Borel sign kernel through the reflected sampling law, then averages the pointwise common-shift Parseval identity.
Kernel averages of the common-shift identity
Tonelli transports an arbitrary Borel sign kernel through the reflected sampling law, then averages the pointwise common-shift Parseval identity. No fairness assumption is needed.
[ The reflected representative is Borel, including at the fold endpoints. This uses the hm hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Averaging common-shift Parseval against any Borel sign kernel.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The original outcome imbalance has the Fourier kernel-average representation. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionLaw 3 declarations This file proves that independent cube coordinates, independently reflected into the two halves of the circle and then translated by a common Haar element, give an iid Haar sample that is independent of the translating e
Law of the reflected and shifted sample
This file proves that independent cube coordinates, independently reflected into the two halves of the circle and then translated by a common Haar element, give an iid Haar sample that is independent of the translating element.
[ One fair reflection coin lifts a cube coordinate into the period-two circle.
Definition (Lean source)
Independent fair coordinate reflections send cube probability to normalized Haar measure.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Independent cube coordinates with independent fair reflections, followed by a common Haar shift, have the iid Haar product law and remain independent of that common shift. This uses the hX hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionPlane 26 declarations The four reflected cells have matching function traces.
Two-dimensional reflected smooth endpoint
The four reflected cells have matching function traces. Slice integration by parts cancels all faces in each coordinate, and the signed gradient preserves the normalized spatial energy. These are the two-dimensional constructions in (4) and (5) of the exact-reflection-budget roadmap.
[ Even reflection in both coordinate directions.
Definition (Lean source)
The first coordinate derivative has the reflected orientation sign.
Definition (Lean source)
The second coordinate derivative has its own reflected orientation sign.
Definition (Lean source)
Coordinate transposition commutes with even reflection.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Transposition exchanges the two reflected gradient coordinates.
Formal statement
Proof (Lean source)
Reflection in the other coordinate preserves the smooth slice derivative. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The first coordinate face cancellation is valid for every periodic smooth test slice. Under the stated conditions.
Formal statement
Proof (Lean source)
The second coordinate cancels faces by the same construction, with no cube trace condition. Under the stated conditions.
Formal statement
Proof (Lean source)
In the first coordinate the character test gives the exact multiplier. Under the stated conditions.
Formal statement
Proof (Lean source)
In the second coordinate the multiplier has the second frequency. Under the stated conditions.
Formal statement
Proof (Lean source)
Normalized reflection transports a continuous scalar slice integral exactly. Under the stated conditions.
Formal statement
Proof (Lean source)
Four-cell normalized L² energy is exactly the original square energy. Under the stated conditions.
Formal statement
Proof (Lean source)
The first gradient coordinate has exactly the same energy as even reflection. Under the stated conditions.
Formal statement
Proof (Lean source)
The second gradient coordinate also preserves energy, including the face jumps. Under the stated conditions.
Formal statement
Proof (Lean source)
Continuous formulas on the four cells are integrable on the representative square, even when their derivative traces disagree on the joining faces. Under the stated conditions.
Formal statement
Proof (Lean source)
The joint period-two coefficient is an iterated normalized square integral.
Definition (Lean source)
Both one-dimensional normalizations multiply to the square's Haar factor. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Fubini exchanges the two coefficient orders when the character-weighted cells are integrable. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Character-weighted even reflection is integrable on the square by its four continuous cells. Under the stated conditions.
Formal statement
Proof (Lean source)
The signed first derivative also has four integrable character-weighted cells. Under the stated conditions.
Formal statement
Proof (Lean source)
The second-coordinate slice multiplier assembles to the joint Fourier multiplier. Under the stated conditions.
Formal statement
Proof (Lean source)
Fubini and transposition assemble the first-coordinate joint multiplier as well. Under the stated conditions.
Formal statement
Proof (Lean source)
The two-dimensional spatial endpoint has exactly the local 1/2 gradient coefficient. Every energy on the right is an original-cube energy; the faces impose no trace condition. Under the stated conditions.
Formal statement
Proof (Lean source)
Both genuine derivative multipliers give the local two-coordinate spectral weight. Under the stated conditions.
Formal statement
Proof (Lean source)
Restricting spatial square energy to the original square is a contraction. Under the stated conditions.
Formal statement
Proof (Lean source)
The four-cell smooth spatial endpoint contracts whole-space H¹ energy with exactly the same local 1/2 gradient normalization. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionPlaneParseval 9 declarations Iterated interval Parseval and dominated convergence sum the joint Fourier coefficients of the four reflected cells.
Joint Parseval for reflected cells
Iterated interval Parseval and dominated convergence sum the joint Fourier coefficients of the four reflected cells. Applying this to the function and both signed derivatives proves the smooth two-dimensional spectral endpoint.
Four continuous cell formulas have every finite Lp regularity on the square. Under the stated conditions.
Formal statement
Proof (Lean source)
Integrating two continuous inner cell formulas against a character is continuous in the outer parameter, despite a possible jump at the inner face. Under the stated conditions.
Formal statement
Proof (Lean source)
Two interval Parseval identities assemble to joint Parseval. The square integrability and partial-coefficient regularity justify exchanging the series and integral. Under the stated conditions.
Formal statement
Proof (Lean source)
Joint Parseval applies to four continuous cells, including discontinuous signed reflected derivatives; no agreement of derivative traces is required. Under the stated conditions.
Formal statement
Proof (Lean source)
Joint Parseval recovers the even reflected square's exact normalized spatial energy. Under the stated conditions.
Formal statement
Proof (Lean source)
Joint Parseval also applies to the signed first derivative across its jumping face. Under the stated conditions.
Formal statement
Proof (Lean source)
The second signed derivative has the same joint Parseval identity. Under the stated conditions.
Formal statement
Proof (Lean source)
Joint Parseval and the two genuine weak derivative multipliers prove the smooth spectral H¹ endpoint, with precisely the local gradient factor one half. Under the stated conditions.
Formal statement
Proof (Lean source)
The smooth two-dimensional Fourier endpoint contracts the whole-space spatial H¹ norm with constant one, independently of the two cube-face traces. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionPooledBudget 4 declarations Exact Fourier component separation and local coordinate transport sum the constant-one component contractions into the pooled ambient spectral bound.
Pooled canonical reflection budget
Exact Fourier component separation and local coordinate transport sum the constant-one component contractions into the pooled ambient spectral bound.
Nonnegative Fourier masses commute with a finite sum of components. Under the stated conditions.
Formal statement
Proof (Lean source)
At each active frequency only its unique canonical component contributes to the weighted outcome mass; summing gives a bound by the ambient component budgets. Under the stated conditions.
Formal statement
Proof (Lean source)
Local coordinate transport pools the ambient spectral mass into local component budgets. Under the stated conditions.
Formal statement
Proof (Lean source)
Exact component contraction and the defining pooled restriction budget bound the reflected outcome's weighted Fourier budget by one. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionProfileEndpoint 12 declarations The inverse angular transform is a real linear isometry on all frequency L² classes.
Reflection endpoints on full frequency L² classes
The inverse angular transform is a real linear isometry on all frequency L² classes. Composing it with even reflection supplies the common operator for interpolation. Smooth inverse truncations prove its first-order endpoints in both component dimensions without any L¹ premise on the spatial representative.
[ The inverse angular transform on equivalence classes is real linear.
Definition (Lean source)
Angular inversion preserves the L² norm with constant exactly one.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
[ The complete frequency L² space maps isometrically into spatial L².
Definition (Lean source)
The common operator for both interpolation endpoints: angular inversion followed by genuine restriction and even reflection.
Definition (Lean source)
The common frequency-to-torus operator contracts the zero-order norm.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Smooth profile truncations converge under the actual common reflection operator on every frequency L² class.
Formal statement
Proof (Lean source)
The full one-dimensional first-order endpoint holds for all frequency L² classes, including those whose spatial inverse has no L¹ representative.
Formal statement
Proof (Lean source)
The full two-dimensional endpoint retains the exact gradient factor 1/2 on all frequency L² classes, without additional integrability assumptions.
Formal statement
Proof (Lean source)
The whole-space first-order frequency gauge, infinite off the endpoint.
The periodic first-order Fourier gauge with the exact local dimension factor.
Definition (Lean source)
The common operator contracts the full first-order endpoint gauge in both component dimensions; the bound was derived from smooth truncations. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The normalized quadratic K norm contracts under the genuine common reflection operator. Both endpoint bounds are proved here, rather than assumed; the remaining fractional step is identification with the weighted Fourier norms. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionSmoothDerivative 14 declarations Differentiation under the inverse integral in roadmap (3) produces the genuine coordinate multiplier.
Coordinate derivatives of the smooth inverse truncations
Differentiation under the inverse integral in roadmap (3) produces the genuine coordinate multiplier. Plancherel then identifies its spatial energy exactly.
[ The spatial coordinate derivative constructed by the inverse angular integral.
Definition (Lean source)
The derivative's frequency profile is both L¹ and L².](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Polynomial multiplication on a compact frequency ball preserves L². Under the stated conditions.
Formal statement
Proof (Lean source)
The actual inverse derivative is spatially square integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
Plancherel gives the exact coordinate-weighted energy, without an extra constant. Under the stated conditions.
Formal statement
Proof (Lean source)
The positive angular phase has the expected derivative on each coordinate slice. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Positive angular kernels preserve integrability of any L¹ profile. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Differentiation under the inverse integral identifies the constructed derivative on every coordinate line. Compact spectral support supplies its integrable dominator. Under the stated conditions.
Formal statement
Proof (Lean source)
The constructed slice derivative is the genuine Fréchet coordinate derivative. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Each constructed coordinate derivative is continuous, even though the spectral cutoff itself has a discontinuity at the ball boundary. This uses the hψ hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
All spatial coordinate derivative energies together equal the exact radial frequency moment; no dimension factor enters Plancherel.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Roadmap (3)'s exact first-order energy identity for the smooth inverse truncations, expressed using their actual coordinate derivatives. Under the stated conditions.
Formal statement
Proof (Lean source)
Restricting the spectral profile to a ball cannot increase the exact H¹ energy. Combined with the identity above this is the spatial approximation bound. Under the stated conditions.
Formal statement
Proof (Lean source)
The exact coordinate-energy identity also holds for differences of two smooth truncations, as required in endpoint completion. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionSmoothEndpoint 17 declarations Coordinate changes preserve Lebesgue measure.
Spectral endpoints for the actual smooth inverse truncations
Coordinate changes preserve Lebesgue measure. The slice and plane reflected Parseval identities therefore apply to the genuine inverse angular truncations, with their actual derivatives and exact whole-space Fourier energy.
The single-coordinate parametrization of Euclidean one-space preserves volume.
Formal statement
Proof (Lean source)
On the real-line parametrization, the constructed coordinate derivative is the actual derivative of the smooth inverse truncation. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The one-dimensional smooth reflected spectrum contracts the exact angular first-order frequency energy. No derivative or endpoint bound is assumed. Under the stated conditions.
Formal statement
Proof (Lean source)
The two-coordinate parametrization of Euclidean two-space preserves volume. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Both real coordinate slices of the genuine two-dimensional truncation have the constructed inverse derivatives. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The actual two-dimensional smooth reflected spectrum contracts the angular first-order energy with exactly the local gradient factor one half. Under the stated conditions.
Formal statement
Proof (Lean source)
The unit-circle coordinate convention gives precisely the normalized period-two slice coefficient after folding, for any complex cube slice. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The actual whole-space reflection operator's coefficients agree with the period-two slice coefficients, independently of the chosen L² representative. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Smooth inverse truncations satisfy the first-order bound in the actual torus L² operator, rather than merely in interval coordinates. Under the stated conditions.
Formal statement
Proof (Lean source)
Spatial L² convergence passes the proved smooth spectral bound to every admissible one-dimensional extension, with no trace condition or assumed endpoint. Under the stated conditions.
Formal statement
Proof (Lean source)
Taking the infimum over genuine extensions proves the complete one-dimensional component contraction at the first-order endpoint. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The folded one-coordinate coefficient can be integrated directly on the circle.
Formal statement
Proof (Lean source)
The two-dimensional torus coefficient is the iterated period-two coefficient of the actual folded whole-space representative. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The actual reflection operator has the joint period-two coefficients of any whole-space L² representative. Under the stated conditions.
Formal statement
Proof (Lean source)
The smooth plane estimate holds in the actual torus reflection operator, with precisely the local factor one half. Under the stated conditions.
Formal statement
Proof (Lean source)
The proved smooth two-dimensional endpoint passes to every whole-space extension by spatial L² convergence, without a cube trace assumption. Under the stated conditions.
Formal statement
Proof (Lean source)
The extension infimum gives the complete two-dimensional component contraction at smoothness one, with constant one. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionSupport 17 declarations Mixed translation differences annihilate effects using at most two coordinates.
Fourier support of reflected ANOVA effects
Mixed translation differences annihilate effects using at most two coordinates. This proves the order-two Fourier support without requiring pointwise versions of conditional marginal regularity.
[ The translation difference on the normalized torus.
Translation differences commute.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
A translation-invariant summand is annihilated by its difference. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Translation differences distribute over addition. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Translation differences distribute over finite sums.
Formal statement
Proof (Lean source)
Any invariant direction kills the third mixed difference. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Translation preserves normalized product Haar measure. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Translation differences preserve integrability. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Translation differences preserve almost-everywhere equality. Under the stated conditions.
Formal statement
Proof (Lean source)
A character times an integrable torus function is integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
Shifting one coordinate by half an inverse nonzero frequency negates its character. Under the stated conditions.
Formal statement
Proof (Lean source)
A half-character translation difference doubles that Fourier coefficient. Under the stated conditions.
Formal statement
Proof (Lean source)
A shift in another coordinate leaves a folded coordinate unchanged. Under the stated conditions.
Formal statement
Proof (Lean source)
Three distinct coordinate differences annihilate every two-coordinate effect. Under the stated conditions.
Formal statement
Proof (Lean source)
The exact order-two decomposition has zero third mixed translation difference, modulo Haar null sets. No marginal representative regularity is needed. Under the stated conditions.
Formal statement
Proof (Lean source)
A zero third difference in three half-character directions forces a zero coefficient. Under the stated conditions.
Formal statement
Proof (Lean source)
An exactly order-two centered cube outcome has no reflected Fourier coefficient supported on more than two coordinates. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionTargetInterpolation 13 declarations Fourier coefficients transport the periodic endpoint gauges to weighted counting measure spaces.
Target Fourier interpolation
Fourier coefficients transport the periodic endpoint gauges to weighted counting measure spaces. Exact weighted interpolation gives the fractional spectral budget from the genuine reflection operator's K norm without any loss of constant.
[ The normalized Fourier characters form the periodic L² basis.
Definition (Lean source)
The basis coordinates are the paper's normalized Fourier coefficients.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
[ Fourier coordinates define an additive map into measurable counting classes.
Definition (Lean source)
Every weighted coefficient gauge is its explicit spectral sum.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Parseval identifies the zero-order coefficient gauge with the torus norm. Under the stated conditions.
Formal statement
Proof (Lean source)
The first-order target gauge is exactly the weighted coefficient gauge. Under the stated conditions.
Formal statement
Proof (Lean source)
Exact weighted interpolation evaluates the coefficient K norm. Under the stated conditions.
Formal statement
Proof (Lean source)
The fractional spectral energy is controlled by the actual torus K norm. Under the stated conditions.
Formal statement
Proof (Lean source)
Both genuine endpoint contractions give the exact fractional reflection budget. Under the stated conditions.
Formal statement
Proof (Lean source)
Angular inversion identifies the common profile operator with reflection of an original admissible spatial extension. Under the stated conditions.
Formal statement
Proof (Lean source)
Each whole-space extension contracts to its exact fractional periodic budget. Under the stated conditions.
Formal statement
Proof (Lean source)
Infimizing over extensions completes the fractional component contraction. Under the stated conditions.
Formal statement
Proof (Lean source)
The complete component reflection contraction, including the first-order endpoint, has constant one in each local dimension. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionTransfer 1 declarations The product-law assertion simultaneously states iid Haar sampling and independence from the common shift.
Reflection, common shift, and Fourier transfer
The product-law assertion simultaneously states iid Haar sampling and independence from the common shift. The arbitrary assignment kernel reads only W and its own fresh randomness.
Even reflection transfers restriction norms, random shifts produce independent Haar samples, and squared imbalance decomposes over the Fourier coefficients in L². This uses the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionTruncation 14 declarations The frequency truncations in step (3) of the reflection-budget proof have compact support and converge in the exact weighted Fourier energy.
Fourier ball truncations for endpoint completion
The frequency truncations in step (3) of the reflection-budget proof have compact support and converge in the exact weighted Fourier energy. No endpoint estimate or periodic boundary condition is assumed here.
[ Cut a frequency profile off at the closed ball of radius R.
Definition (Lean source)
The cutoff of a measurable frequency profile is measurable. This uses the hψ hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Cutting off a square-integrable profile preserves square integrability.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Every frequency cutoff has compact support, including negative-radius cutoffs. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
A frequency cutoff of an L² profile is L¹ by finite volume of the ball. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every continuous multiplier of an L² frequency cutoff is again L². In particular this covers all polynomial moments used to differentiate the inverse integral. Under the stated conditions.
Formal statement
Proof (Lean source)
Continuous multipliers of frequency cutoffs are L¹ as well as L², since their supports lie in the same finite-volume ball. Under the stated conditions.
Formal statement
Proof (Lean source)
Every norm moment of a truncated L² profile is integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
The smooth inverse angular Fourier integral of a ball-truncated profile. Evaluating the forward angular transform at minus the spatial argument gives exactly the positive exponential and the unitary prefactor in step (3).
Definition (Lean source)
The constructed smooth approximation is the normalized inverse angular integral from step (3), with the positive exponential and no extra dilation constant. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The inverse integral from the roadmap is smooth to every order, because all norm moments of its compactly supported L² frequency profile are L¹. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
At each frequency the integer-radius truncations eventually equal the profile. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The exact weighted squared error of the frequency truncations tends to zero. This is the dominated-convergence assertion in step (3), with the paper's local normalization by p and with no loss in the weight. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The genuine Fourier ball truncations of an admissible whole-space extension satisfy the smoothness, integrable-moment and weighted frequency-convergence parts of step (3). Identifying the inverse integrals in L² remains a separate step. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.ReflectionWeakDerivative 15 declarations On the period-two representative interval, a smooth cube slice is reflected at one.
Face cancellation for the first-order reflection endpoint
On the period-two representative interval, a smooth cube slice is reflected at one. Its signed derivative satisfies integration by parts against periodic smooth tests: the internal face cancels, and the two external faces cancel using periodicity of the test alone. The cube slice has no boundary condition. Parseval then proves the one-dimensional smooth first-order spectral endpoint with constant one. These establish equations (4) and (5) of the reflection-budget roadmap on slices, before Fourier truncation and completion.
[ The even reflected slice on the period-two representative interval.
Definition (Lean source)
The derivative on reflected open cells has opposite signs on the two halves.
Definition (Lean source)
Splitting a two-cell integral is valid even if its two formulas disagree on the join.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Reflecting a differentiable slice reverses its derivative on the second cell. Under the stated conditions.
Formal statement
Proof (Lean source)
Integration by parts cancels both reflected faces. Only the test values at zero and two must agree; no equality between the cube function's values at zero and one is used. Under the stated conditions.
Formal statement
Proof (Lean source)
The normalized reflected L² energy is exactly the cube-slice energy. Under the stated conditions.
Formal statement
Proof (Lean source)
The sign reversal preserves the normalized derivative energy, with constant one. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Fourier coefficients on the period-two representative interval use normalized Haar mass.
Definition (Lean source)
Testing the cancelled slice identity with a character gives the exact derivative multiplier, including zero frequency.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The zeroth and derivative energies add without loss under normalized even reflection. Under the stated conditions.
Formal statement
Proof (Lean source)
Continuous cell formulas give Lp regularity on the finite representative interval, even when the signed derivative jumps at the reflection face. Under the stated conditions.
Formal statement
Proof (Lean source)
The local slice normalization agrees with Mathlib's interval Fourier coefficients. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Squaring the exact derivative multiplier supplies the first-order Fourier weight. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Parseval on the function and its signed weak derivative proves the smooth, one-dimensional first-order endpoint with the exact constant one. Under the stated conditions.
Formal statement
Proof (Lean source)
Restricting the smooth one-dimensional endpoint energy to the cube is a contraction from whole-space spatial H¹ energy, independently of the two original face values. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingBorel 15 declarations The active-coordinate masks, sign-guarded finite boundary minima, and finite inverse-CDF selections are measurable without rank or nondegeneracy assumptions.
Borel arithmetic for ordered boundary rounding
The active-coordinate masks, sign-guarded finite boundary minima, and finite inverse-CDF selections are measurable without rank or nondegeneracy assumptions. These are the arithmetic ingredients of the roadmap's Borel-stratum argument.
Adding an entry to a nonempty finite minimum takes the minimum of the two values. Under the stated conditions.
Formal statement
Proof (Lean source)
A sign-guarded list is empty on a measurable set and its finite minimum is measurable. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Finite row inner products are Borel in both vectors. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Restriction to the active coordinates is Borel even at boundary states. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The boundary minimum is Borel in state and direction, including empty-candidate strata. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The opposite boundary distance is Borel by negating the direction. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Every padded seed read is measurable. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Removing a fixed finite family of measurable rank-one projections is Borel. This uses the hb hypothesis, the hv hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The Gram--Schmidt residual norm is Borel for each fixed family of preceding vectors. This uses the hb hypothesis, the hv hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The zero-residual branch of Gram--Schmidt is a Borel stratum.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
[ Finite inverse-CDF selection is Borel for measurable candidates, weights, and seed. Neither positivity nor distinct interval boundaries are needed for this arithmetic fact. This uses the hv hypothesis, the hw hypothesis, the ht hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The asymmetric boundary coin probability is Borel in the state and direction. This uses the stated conclusion.
Formal statement
Proof (Lean source)
A boundary move with a supplied measurable direction and fresh seed is Borel. This uses the hu hypothesis, the hv hypothesis, the ht hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
A terminal single-coordinate round is Borel, including the threshold tie. This uses the hu hypothesis, the ht hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
On a stratum with a fixed measurable basis family, the complete nonterminal move is Borel. The list representation is a local description of a rank stratum, not a rank assumption.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingCrossingTimes 32 declarations The first active-count crossing after a measurable starting time is bounded by n.
Bounded crossing times of the actual rounding trace
The first active-count crossing after a measurable starting time is bounded by n. Its interval mask depends only on the current history. In particular, the first loss of row protection is a measurable, predictable crossing, with an actual starting active count below 4h. Successive halving crossings give measurable intervals ending at the terminal state and the pathwise 8 min(h,n) active-count allowance. These intervals refine the move trace and need not coincide with metadata refreshes.
The terminal state supplies a crossing for every nonnegative active threshold.
Formal statement
Proof (Lean source)
[ First active-count crossing after the clipped starting time, on the actual trace.
Definition (Lean source)
The crossing respects its starting time and attains the prescribed active bound. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Every crossing lies within the deterministic move horizon.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
By monotonicity, a crossing has not occurred exactly when the start is still in the future or the current active count is above the threshold.
Formal statement
Proof (Lean source)
A crossing has occurred precisely when its start has occurred and the current active count is at or below the threshold.
Formal statement
Proof (Lean source)
Measurable random starts and active thresholds give a measurable first crossing. This uses the hK hypothesis, the hR hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Inside the horizon, the crossing interval is decided by the current active count and the event that the random start has occurred. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Crossing intervals are predictable when their start event and threshold are unchanged by the fresh coin. The end time itself need not be unchanged. Under the stated conditions.
Formal statement
Proof (Lean source)
The first unprotected move is the crossing of the integer threshold 4h-1.
Definition (Lean source)
The row's first unprotected time is Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
An unprotected-time crossing always occurs before or at the terminal state. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Loss of protection occurs exactly on the terminal interval starting at the crossing. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The crossing starts with fewer than 4h active coordinates and at most n. Under the stated conditions.
Formal statement
Proof (Lean source)
Membership in the unprotected terminal interval is predictable before the next coin. Under the stated conditions.
Formal statement
Proof (Lean source)
The active count at a measurable random time is measurable. This uses the hK hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Starting at a clipped time, repeatedly stop at the first halving of the actual active count. Empty intervals pad the trace once every coordinate is fixed.
Definition (Lean source)
Every realized halving endpoint lies within the finite move horizon. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Successive realized halving intervals occur in chronological order.
Formal statement
Proof (Lean source)
The starting active counts of consecutive actual intervals at least halve.
Formal statement
Proof (Lean source)
[ Each halving time is a measurable function of the original finite seed list. This uses the hK hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
After j halving intervals, at most n-j coordinates remain active.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Padding to n intervals includes every nonzero actual increment: the last endpoint already has no active coordinates.
Formal statement
Proof (Lean source)
The padded endpoint is the same actual state as the final output signing.
Formal statement
Proof (Lean source)
Starting the realized intervals when a row loses protection gives the paper's deterministic geometric active-count allowance on every seed realization. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Equal sublevel events up to k determine the same time clipped at k+1. Under the stated conditions.
Formal statement
Proof (Lean source)
The first unprotected time, clipped just after the current move, ignores all seed coordinates that have not yet been read. Under the stated conditions.
Formal statement
Proof (Lean source)
Realized halving endpoints are stopping times for the finite seed history: only their part up to the current move can be observed before the fresh seeds. Under the stated conditions.
Formal statement
Proof (Lean source)
Each realized halving interval has a predictable move mask, including empty intervals after the terminal state. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual halving interval has the integrated coordinate-variance budget of its realized starting active count, with no extra stopping-time premises. Under the stated conditions.
Formal statement
Proof (Lean source)
The realized interval row increment has exactly the sum of its move second moments. This combines the crossing-time mask with the actual martingale telescope. Under the stated conditions.
Formal statement
Proof (Lean source)
Integrating the realized geometric count allowance preserves the paper's 8 min(h,n) budget; each random count is bounded and measurable. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingFairness 6 declarations Integrating one fresh coordinate of the product seed law preserves the fractional-state mean.
Seed-history integration and fairness
Integrating one fresh coordinate of the product seed law preserves the fractional-state mean. Finite iteration from zero gives fair terminal signs.
A fresh-coordinate conditional mean integrates to the preceding mean under product uniform seeds, provided that the preceding state ignores that seed. Under the stated conditions.
Formal statement
Proof (Lean source)
Each fractional coordinate is Borel as a function of all seeds. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Cube preservation makes every fractional coordinate integrable under the full product seed law, without any row bound. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Successive fresh-coin integration preserves the full-seed coordinate mean. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Starting at zero and integrating the fresh seed at each move gives zero mean for every fractional coordinate up to the deterministic move limit. Under the stated conditions.
Formal statement
Proof (Lean source)
Terminal signs equal the final fractional state, so the constructed signing is fair under its actual product seed law. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingGeometry 15 declarations Ordered Gram--Schmidt preserves active-coordinate support and discards zero vectors.
Support and nonzero directions in ordered boundary rounding
Ordered Gram--Schmidt preserves active-coordinate support and discards zero vectors. Finite inverse-CDF sampling therefore selects a valid direction from any nonempty constructed nullspace basis, yielding strict active-count progress.
Removing projections onto active-supported vectors preserves active support. Under the stated conditions.
Formal statement
Proof (Lean source)
Gram--Schmidt insertion cannot introduce a coordinate outside the input support. Under the stated conditions.
Formal statement
Proof (Lean source)
Every vector returned by ordered Gram--Schmidt has the common input support. Under the stated conditions.
Formal statement
Proof (Lean source)
The constructed constraint projection vanishes on inactive coordinates. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every constructed nullspace basis vector is supported on active coordinates.
Formal statement
Proof (Lean source)
A positive residual norm makes its normalized direction nonzero. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The insertion rule preserves nonzero old directions and adds only a nonzero residual. Under the stated conditions.
Formal statement
Proof (Lean source)
Zero residuals are discarded throughout the structural Gram--Schmidt fold. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Normalization gives the unit squared length used in the covariance trace. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every inserted Gram--Schmidt residual has unit squared length. Under the stated conditions.
Formal statement
Proof (Lean source)
All output directions of the ordered Gram--Schmidt construction are unit vectors. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Each inverse boundary-product weight in the actual nullspace basis is positive.
Formal statement
Proof (Lean source)
The finite basis-sampling normalizer is strictly positive whenever a direction exists. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Sampling a nonempty finite distribution always returns one of its directions, including seeds at interval ties and at the final endpoint. Under the stated conditions.
Formal statement
Proof (Lean source)
Any nonempty nullspace basis makes the actual move preserve the cube and strictly decrease the active count; no seed restrictions or generic rank are needed. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingLottery 11 declarations The half-open inverse-CDF sampler integrates finite rewards with their prescribed weights.
Exact direction-lottery moments
The half-open inverse-CDF sampler integrates finite rewards with their prescribed weights. Applied to reciprocal boundary-distance weights, this supplies the isotropic covariance of a boundary move before the phase energy argument.
A nonnegative finite direction lottery integrates every reward on its full weight interval, including zero weights and tied cumulative boundaries. Under the stated conditions.
Formal statement
Proof (Lean source)
A unit-mass finite direction lottery has precisely the expected weighted reward under the uniform seed used by the rounding construction. Under the stated conditions.
Formal statement
Proof (Lean source)
Zipping each direction with its own weight keeps the ordered finite lottery. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Dividing positive finite weights by their total gives the exact normalized uniform-seed expectation, without independence of vector coordinates. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The actual direction lottery averages the direction-conditioned boundary covariance to the reciprocal total weight times the basis outer-product sum. Under the stated conditions.
Formal statement
Proof (Lean source)
Reciprocal boundary-product sampling cancels that product for any finite basis reward. This is the common averaging step for row and norm energies. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual move's test-row increment has the exact conditional second moment, with the asymmetric boundary coin rather than a symmetric surrogate. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Averaging both fresh seeds gives the exact test-row quadratic form in the constructed nullspace basis, the phase variance identity in the roadmap. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A single asymmetric boundary coin increases squared norm in expectation by its distance product times the direction's squared norm. Under the stated conditions.
Formal statement
Proof (Lean source)
The squared-norm potential's conditional increase for the actual move is its boundary-distance product, since every selected basis direction is a unit vector. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The two-seed squared-norm increase is reciprocal total weight times the actual basis size, giving the trace term needed for the phase energy budget. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingMoments 15 declarations Half-open uniform threshold sampling realizes the asymmetric boundary coin.
Fresh-seed boundary moments
Half-open uniform threshold sampling realizes the asymmetric boundary coin. Its coordinate mean and covariance are computed before integrating over the selected nullspace direction or the preceding seed history.
A half-open uniform threshold has the prescribed two-point expectation, including thresholds at either endpoint of the unit interval. Under the stated conditions.
Formal statement
Proof (Lean source)
A finite threshold coin is integrable under its fresh uniform seed. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The actual half-open asymmetric boundary coin preserves a coordinate mean. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The centered boundary increment has the roadmap's exact coordinate covariance. Under the stated conditions.
Formal statement
Proof (Lean source)
A fresh terminal coin preserves the current fractional coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
A fresh terminal increment has variance one minus the current square. Under the stated conditions.
Formal statement
Proof (Lean source)
The constructed finite sampler selects a genuine nullspace basis vector. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual boundary step preserves each coordinate mean conditional on the entire current state and the selected direction seed. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Each coordinate of the actual boundary step is integrable over its coin seed.
Formal statement
Proof (Lean source)
The actual direction-conditioned increment covariance is the boundary-distance product times the selected direction's outer product.
Formal statement
Proof (Lean source)
Every padded phase move preserves each fractional coordinate's mean under its fresh coin seed, including terminal and already-finished branches. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every phase-move coordinate is integrable over its fresh coin seed. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The first k moves depend only on their first 2k seeds. This is the finite-history property needed when integrating the next independent coin. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Changing a future seed cannot change the current fractional state. Under the stated conditions.
Formal statement
Proof (Lean source)
Integrating the next actual coin, while holding all other seeds fixed, returns the preceding fractional coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingPhaseSums 21 declarations The deterministic halving estimate gives the total active-count allowance after any row loses protection.
Finite phase sums for ordered rounding
The deterministic halving estimate gives the total active-count allowance after any row loses protection. Orthogonal finite increments have additive second moments. Terminal single-coordinate rounding has the exact test-row variance and norm-energy increment required by the phase argument. The actual row seed iteration has centered increments and exact finite second-moment accumulation.
Halving phase counts telescope, including the unused terminal endpoint. Under the stated conditions.
Formal statement
Proof (Lean source)
A finite halving chain spends at most twice its initial active count. Under the stated conditions.
Formal statement
Proof (Lean source)
Once a row is unprotected, the halving phase chain spends at most eight times its row index, and also at most twice the original sample size. Under the stated conditions.
Formal statement
Proof (Lean source)
The paper's constant 32 is the product of the phase variance allowance 4 and the deterministic unprotected-count allowance 8. Under the stated conditions.
Formal statement
Proof (Lean source)
Orthogonality to the preceding partial sum removes exactly the cross term in a finite second-moment expansion. Under the stated conditions.
Formal statement
Proof (Lean source)
Finite orthogonal phase increments inherit the sum of their separate variance allowances. The increments and counts can be zero-padded. Under the stated conditions.
Formal statement
Proof (Lean source)
A preceding seed-history statistic is orthogonal to a fresh centered increment. This is the conditional-mean argument used for padded moves and phases. Under the stated conditions.
Formal statement
Proof (Lean source)
Random realized phase counts obey the same pathwise halving budget before integration. This keeps the active-count bound inside the seed expectation. Under the stated conditions.
Formal statement
Proof (Lean source)
Updating one coordinate changes a test row by its coefficient times the single-coordinate increment. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The actual terminal coordinate update contributes exactly its coefficient square times one minus the current coordinate square to the row variance. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Each terminal row increment spends at most one coefficient-square allowance. Under the stated conditions.
Formal statement
Proof (Lean source)
A single-coordinate terminal update changes norm energy only at that coordinate. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every fresh terminal coin spends exactly one minus the current coordinate square in norm energy, independently of the threshold's asymmetry.
Formal statement
Proof (Lean source)
Terminal moves satisfy the row variance-to-energy comparison with constant one. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every actual fractional coordinate has all finite moments, by cube preservation. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
A finite deterministic test row preserves square-integrability of the state.
Formal statement
Proof (Lean source)
Integrating the next fresh actual coin centers each coordinate increment. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The actual row increment has zero conditional mean under its fresh coin. Under the stated conditions.
Formal statement
Proof (Lean source)
Finite increment sums telescope without any convergence or stopping-time theorem. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Orthogonality holds for the actual row increments and the preceding fractional row. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The constructed signing's second moment is exactly the finite sum of its move variances. The initial state is zero and the terminal state is the actual signing. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingPhaseTrace 15 declarations The retained prefix dominates one quarter of the active count on live moves.
Protected rows along the actual rounding trace
The retained prefix dominates one quarter of the active count on live moves. Consequently, row h cannot change until fewer than 4h coordinates remain active. These pathwise facts connect the actual iteration to the unprotected phase budget.
Active counts decrease monotonically along the actual seed realization.
Formal statement
Proof (Lean source)
A move preserves the lower bound on the retained prefix when its phase is live. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
On a live actual phase, the retained prefix contains at least a quarter of its current active coordinates. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
A supplied row stays fixed on a move with at least four times its row number active coordinates, whether that move starts a new phase or continues one. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
While a phase is live, its stopping threshold and retained row count do not change on the next actual move. Under the stated conditions.
Formal statement
Proof (Lean source)
A supplied row is still zero at every actual state above its protection threshold, because all earlier states have at least as many active coordinates. Under the stated conditions.
Formal statement
Proof (Lean source)
The paper's one-based row numbering has the same protection threshold, even for rows beyond the supplied prefix (whose protection premise is impossible). Under the stated conditions.
Formal statement
Proof (Lean source)
Protection can be represented by a zero-padded increment supported precisely on the unprotected active-count event. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual active count is a Borel statistic of the seeds. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The event that a numbered row is unprotected before a move is Borel. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Protection is decided before either fresh seed used by the next move is read. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Once a row is unprotected it remains so; the selected moves form a terminal interval of the actual trace. Under the stated conditions.
Formal statement
Proof (Lean source)
The final row second moment is exactly the sum over its unprotected moves. This specializes the proved martingale identity to the paper's actual trace. Under the stated conditions.
Formal statement
Proof (Lean source)
A nonterminal refresh records exactly the paper's halving threshold and quarter-prefix length for its realized starting active count. Under the stated conditions.
Formal statement
Proof (Lean source)
Keeping a refreshed phase's metadata until its threshold is reached gives an actual active count at most half that phase's starting count. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingProjection 15 declarations Ordered Gram--Schmidt produces orthogonal unit directions.
Projection contraction for the constructed rounding basis
Ordered Gram--Schmidt produces orthogonal unit directions. Its residual energy identity bounds the basis quadratic form by the active-coordinate row energy.
Dotting a finite projection residual distributes over its basis list.
Formal statement
Proof (Lean source)
An orthogonal unit list extracts the coefficient of each member exactly. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The residual is orthogonal to every direction already in the basis. Under the stated conditions.
Formal statement
Proof (Lean source)
Gram--Schmidt insertion preserves orthogonality, including discarded residuals. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual ordered construction yields pairwise orthogonal directions. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Pythagoras for the explicit residual accounts for every basis coefficient. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Nonnegative residual energy gives Bessel contraction for the explicit list. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual nullspace basis contracts every test-row quadratic form. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Inactive coordinates contribute no coefficient against any nullspace direction. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Projection contraction can be localized to the current active coordinates. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
A bounded test row has at most one squared-entry budget per active coordinate. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The roadmap's localized projection quadratic bound holds for the actual basis. Under the stated conditions.
Formal statement
Proof (Lean source)
Each actual two-seed row variance is bounded by gamma times active row energy. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual row variance and norm increment obey the same gamma-weighted budget, with the constructed basis length retained explicitly. Under the stated conditions.
Formal statement
Proof (Lean source)
Only initially active coordinates can spend endpoint norm energy; their combined increase is bounded by the phase's initial count. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingRank 14 declarations The actual ordered orthonormalization preserves its input orthogonal complement.
Quantitative rank and protected rows in ordered rounding
The actual ordered orthonormalization preserves its input orthogonal complement. A trace argument gives the exact constraint-plus-nullspace rank identity on active coordinates, even for dependent rows. The live-phase rank estimate bounds each fresh-seed row variance by four times its squared-norm energy increment. Retained rows are fixed by every boundary move. Finite phase accumulation is separate.
A test vector orthogonal to the basis sees the same coefficient before and after projection. Under the stated conditions.
Formal statement
Proof (Lean source)
One insertion preserves exactly the orthogonal complement of the old basis and new input. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Discarding zero residuals preserves the orthogonal complement of all input vectors.
Formal statement
Proof (Lean source)
An active-supported vector pairs with a masked coordinate vector to give that coordinate. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every constructed nullspace direction is orthogonal to every constraint-basis vector. Under the stated conditions.
Formal statement
Proof (Lean source)
An active-supported vector orthogonal to both constructed bases must vanish. Under the stated conditions.
Formal statement
Proof (Lean source)
A unit active-supported basis resolving every active coordinate has size equal to the active count. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual constraint and nullspace basis sizes sum exactly to the active-coordinate count. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Dependent constraints only increase the constructed nullspace rank above active count minus row count.
Formal statement
Proof (Lean source)
Before the phase stopping threshold, the actual nullspace rank is at least one quarter of the initial count. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A live phase has at most four active coordinates per constructed nullspace direction. Under the stated conditions.
Formal statement
Proof (Lean source)
The fresh two-seed row variance in a live phase is bounded by four times its norm-energy increment and squared entry bound. Under the stated conditions.
Formal statement
Proof (Lean source)
Each constructed nullspace direction annihilates every retained original row. Under the stated conditions.
Formal statement
Proof (Lean source)
The asymmetric boundary move fixes each retained row for every seed, including empty-basis padding. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingRankBorel 14 declarations Finite branching at zero residuals preserves measurability for every consumer of a basis.
Borel elimination of changing Gram--Schmidt bases
Finite branching at zero residuals preserves measurability for every consumer of a basis. This proves the rank-stratum step without imposing a fixed rank.
A measurable consumer of every fixed measurable basis family remains measurable through the finite Gram--Schmidt branching, including discarded residuals. Under the stated conditions.
Formal statement
Proof (Lean source)
Ordered orthonormalization admits measurable consumers with no rank premise. Under the stated conditions.
Formal statement
Proof (Lean source)
Finite projection subtraction is Borel for a list of measurable vectors. Under the stated conditions.
Formal statement
Proof (Lean source)
[ At any fixed retained prefix length, the actual constraint projection is Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Consumers of the actual nullspace basis are measurable for each retained prefix.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Inverse-CDF selection is measurable for lists indexed by their measurable members. Under the stated conditions.
Formal statement
Proof (Lean source)
The specified basis sampling and asymmetric boundary move form a Borel consumer. Under the stated conditions.
Formal statement
Proof (Lean source)
[ The actual nonterminal move is Borel for a fixed number of retained constraints. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Discrete retained-count choices can be combined with the Borel step family.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Filtering a finite index list by active tests preserves measurable consumers. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual active list has measurable consumers, including changing lengths and heads. Under the stated conditions.
Formal statement
Proof (Lean source)
Phase transitions, including terminal head selection, are Borel. Under the stated conditions.
Formal statement
Proof (Lean source)
Every fractional iteration is jointly Borel in input rows and all seeds. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The full signing map is Borel, without any rank or row-bound premise. This uses the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingRowBudget 14 declarations The phase metadata keeps twice the retained count below the stopping count.
Row variance budgets for the actual rounding moves
The phase metadata keeps twice the retained count below the stopping count. Thus each live move has a uniform row-to-energy comparison, including refreshes and terminal single-coordinate moves.
Phase refreshes preserve the stronger rank invariant needed for energy comparison. Under the stated conditions.
Formal statement
Proof (Lean source)
Every actual state carries the stronger retained-count invariant. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Any move retaining at most half the active count has a uniform row-to-energy bound. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Actual metadata gives the row-to-energy comparison on every move, including phase refreshes, terminal coins, and identity padding. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Averaging a fresh cube coordinate preserves measurability. This uses the hf hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
A uniform bound survives averaging one independent cube coordinate.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Independent coordinate averaging preserves the full cube integral. Under the stated conditions.
Formal statement
Proof (Lean source)
A bounded two-fresh-coordinate comparison integrates over all preceding history. Under the stated conditions.
Formal statement
Proof (Lean source)
A cube-valued state has a uniformly bounded deterministic row evaluation. Under the stated conditions.
Formal statement
Proof (Lean source)
Cube-valued states have norm energy between zero and the ambient count. Under the stated conditions.
Formal statement
Proof (Lean source)
Averaging a predictably selected actual move compares its row variance with its norm-energy expenditure, after integrating both fresh seeds. Under the stated conditions.
Formal statement
Proof (Lean source)
The variance-to-energy comparison sums over any predictable family of move masks. Under the stated conditions.
Formal statement
Proof (Lean source)
Energy spent after the first loss of row protection is bounded by the active count at that crossing, hence by four times the smaller of the row number and n. Under the stated conditions.
Formal statement
Proof (Lean source)
Actual rounding signs satisfy the paper's row bound by predictable move orthogonality, the rank comparison, and the crossing-time energy telescope. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingStoppedPhases 20 declarations Seed-history events select zero-padded phase increments without changing their conditional means.
Predictable selection of actual rounding moves
Seed-history events select zero-padded phase increments without changing their conditional means. Their finite second moments add exactly, and their coordinate variance is the corresponding selected norm-energy expenditure. Random interval masks telescope pathwise, so a phase's endpoint bound can be applied before integrating. The construction of the actual phase intervals is separate.
A seed-history event can select a centered fresh increment without bias. Under the stated conditions.
Formal statement
Proof (Lean source)
A predictable selected increment is orthogonal to any preceding square-integrable statistic, including a preceding selected partial sum. Under the stated conditions.
Formal statement
Proof (Lean source)
Earlier actual row increments ignore every seed at or after the current move. Under the stated conditions.
Formal statement
Proof (Lean source)
Measurable phase membership preserves the actual increment's second moment domain. Under the stated conditions.
Formal statement
Proof (Lean source)
The actual next coin centers every predictably selected row increment. Under the stated conditions.
Formal statement
Proof (Lean source)
The zero-padded moves in any predictable phase have additive second moments. Membership may depend on all preceding seeds; no deterministic phase lengths are assumed. Under the stated conditions.
Formal statement
Proof (Lean source)
A selected actual move remains orthogonal to the current fractional coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
The selected coordinate variance is exactly its selected square-energy increment. Under the stated conditions.
Formal statement
Proof (Lean source)
No boundary move changes an already inactive coordinate, even with an empty basis. Under the stated conditions.
Formal statement
Proof (Lean source)
Phase changes and terminal moves also preserve all inactive coordinates. Under the stated conditions.
Formal statement
Proof (Lean source)
Once a coordinate is inactive, every later actual state retains it. Under the stated conditions.
Formal statement
Proof (Lean source)
Every actual interval can spend at most its initially active count in endpoint energy. Under the stated conditions.
Formal statement
Proof (Lean source)
A finite interval mask telescopes even when the interval is empty. Under the stated conditions.
Formal statement
Proof (Lean source)
Summing the selected coordinate variances gives the selected norm-energy expenditure. Under the stated conditions.
Formal statement
Proof (Lean source)
Predictable random intervals inherit the exact norm-energy telescope of actual states. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Evaluating an actual coordinate at any measurable integer time is Borel. This uses the hK hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
A measurable random endpoint still has square-integrable coordinates, by cube preservation.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Random-endpoint norm energy is integrable; no stopping-time theorem is needed. Under the stated conditions.
Formal statement
Proof (Lean source)
The initial active-count allowance at a measurable random phase start is integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
The predictable random phase's total coordinate variance is bounded by its expected initial active count. This is the conditional energy budget integrated over the phase-start history, for the actual finite rounding iteration. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.RoundingTermination 23 declarations A trace count forces a nonempty constructed nullspace basis whenever the active count exceeds the retained constraint count.
Finite termination of ordered boundary rounding
A trace count forces a nonempty constructed nullspace basis whenever the active count exceeds the retained constraint count. The phase invariant and strict boundary progress then exhaust all active coordinates in at most n moves.
A vector with zero squared Euclidean length is zero.
Proof (Lean source)
With no constraints the residual is the input vector itself.
Formal statement
Proof (Lean source)
Gram--Schmidt never removes old vectors.
Formal statement
Proof (Lean source)
An empty insertion has both an empty input basis and a zero input vector.
Formal statement
Proof (Lean source)
The structural orthonormalization is empty only when every input vector is zero.
Formal statement
Proof (Lean source)
At most one vector is added by each insertion.
Formal statement
Proof (Lean source)
Discarding residuals cannot increase the number of input constraints.
Formal statement
Proof (Lean source)
The constraint basis has no more vectors than retained rows.
Formal statement
Proof (Lean source)
An empty constructed nullspace basis annihilates every projected coordinate vector. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The active-coordinate count is the trace of the active mask. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Summing the diagonal contributions of a finite basis gives its total squared length.
Formal statement
Proof (Lean source)
Unit squared lengths make the basis trace exactly its number of vectors. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
If all projected coordinate vectors vanish, the active trace equals the constraint trace. Under the stated conditions.
Formal statement
Proof (Lean source)
More active coordinates than retained rows forces an actual constructed direction. Under the stated conditions.
Formal statement
Proof (Lean source)
The retained row count never exceeds the phase stopping count. Under the stated conditions.
Formal statement
Proof (Lean source)
At zero active count the padded iteration is exactly the identity. Under the stated conditions.
Formal statement
Proof (Lean source)
The phase invariant ensures a nonempty constructed basis on every live nonterminal move. Under the stated conditions.
Formal statement
Proof (Lean source)
Every live move preserves the cube and removes at least one active coordinate. Under the stated conditions.
Formal statement
Proof (Lean source)
One padded move preserves the cube and lowers the active count by one until exhaustion. Under the stated conditions.
Formal statement
Proof (Lean source)
The finite iteration preserves the phase invariant at every step. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every seed realization remains in the cube and has at most n-k active coordinates.
Formal statement
Proof (Lean source)
After n moves no coordinate is fractional.
Formal statement
Proof (Lean source)
The actual terminal state equals the output signing, for every seed realization.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SigningCrossExpectation 16 declarations Finite projection classes retain their exact Rademacher average after centering and contraction.
Conditional cross-group expectations
Finite projection classes retain their exact Rademacher average after centering and contraction. For a fixed complementary sample this gives the conditional cross-group bound used in the isotropic signing roadmap.
Isotropic projections have integrable absolute values. Under the stated conditions.
Formal statement
Proof (Lean source)
Centering a finite bounded direction class costs at most its radius times the sample size. The remaining term is the actual centered supremum. Under the stated conditions.
Formal statement
Proof (Lean source)
Symmetrization and contraction bound the uncentered finite projection supremum while preserving the exact linear Rademacher average for the independent-group step. Under the stated conditions.
Formal statement
Proof (Lean source)
Cross-group sign optimization as a finite class of absolute projections.
Definition (Lean source)
The cross-group maximum is nonnegative, also for empty groups. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Two independent groups give a product-integrable cross maximum under the common envelope consisting of the product of their summed row norms. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
For a fixed complementary sample, the finite class of its signed sums gives the conditional cross-group bound with no loss of the independent-group structure. Under the stated conditions.
Formal statement
Proof (Lean source)
An independent group of isotropic rows costs at most its size times the norm of a fixed direction, including the empty-group convention. Under the stated conditions.
Formal statement
Proof (Lean source)
The signed first-group norm is jointly integrable under rows and fresh signs. Under the stated conditions.
Formal statement
Proof (Lean source)
The linear Rademacher cross term has a product-integrable norm envelope; this justifies exchanging the two independent groups without higher moments. Under the stated conditions.
Formal statement
Proof (Lean source)
After exchanging the independent samples, isotropy bounds the exact cross Rademacher average by the second-group size times the first-group square-root scale. Under the stated conditions.
Formal statement
Proof (Lean source)
Integrating the conditional finite-class bound gives the cross-group estimate in terms of the complementary group's expected maximum norm. Its Rademacher term already has the sharp independent-group square-root scale. Under the stated conditions.
Formal statement
Proof (Lean source)
Finite classes of unit directions obey the uncentered isotropic projection bound. Under the stated conditions.
Formal statement
Proof (Lean source)
A finite net of unit directions approximates the signed norm maximum uniformly on every sample, with an error controlled by the sum of row norms. Under the stated conditions.
Formal statement
Proof (Lean source)
Compact unit-ball approximation passes finite-class symmetrization and contraction to the expected maximum signed norm, with no extra moment assumption. Under the stated conditions.
Formal statement
Proof (Lean source)
The two independent groups satisfy the roadmap's explicit cross bound. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SigningDecoupling 23 declarations Signed squared norms split into a sign-independent diagonal and an off-diagonal quadratic form.
Deterministic diagonal separation for isotropic row signing
Signed squared norms split into a sign-independent diagonal and an off-diagonal quadratic form. Random partitioning recovers one quarter of each form, and optimizing after averaging is bounded by averaging the cross-group maxima. Finite extrema and selector averages are measurable and integrable under coordinate second moments.
[ The off-diagonal quadratic form for a fixed signing of deterministic rows.
The maximum absolute off-diagonal quadratic form over the finite sign space.
Definition (Lean source)
Every signed squared norm has the same diagonal part.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
The finite minimum is bounded below by diagonal energy minus maximum fluctuation.
Formal statement
Proof (Lean source)
Coordinate second moments integrate the squared norm of every fixed signing. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
[ The genuine finite signing minimum is Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The finite minimum is integrable, since it lies between zero and one fixed signing.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
[ The maximum off-diagonal fluctuation is Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Each off-diagonal form is integrable, as the difference of two quadratic energies.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The maximum absolute fluctuation is integrable, bounded by the finite sum of fluctuations. Under the stated conditions.
Formal statement
Proof (Lean source)
Distinct coordinates of a uniformly sampled sign vector have zero product mean. Under the stated conditions.
Formal statement
Proof (Lean source)
An ordered pair of distinct rows belongs to the selected and complementary groups with probability exactly one quarter. Under the stated conditions.
Formal statement
Proof (Lean source)
The cross-group signed quadratic form for a selected set and its complement.
Random partitioning recovers exactly one quarter of every fixed off-diagonal form. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The cross-group form is the actual inner product of the two disjoint signed sums.
Formal statement
Proof (Lean source)
[ Maximum absolute signed cross-group fluctuation for a realized partition.
Definition (Lean source)
Optimizing after averaging can only decrease the absolute supremum. This is the load-bearing direction of the random-partition inequality in the roadmap.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
Coordinate second moments integrate inner products of any two rows, even when equal. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Each signed cross-group quadratic form is integrable under coordinate second moments. Under the stated conditions.
Formal statement
Proof (Lean source)
[ The finite cross-group maximum is Borel for every realized selector. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The finite cross-group maximum is integrable under coordinate second moments.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Averaging a finite cross-group maximum over selectors preserves integrability. Under the stated conditions.
Formal statement
Proof (Lean source)
The expected absolute off-diagonal maximum is at most four times the expected cross-group maximum. The finite selector average is inside the row expectation. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SigningDuality 7 declarations Norm duality and a countable dense direction class supply the unit-ball specialization of the cited contraction interface in the row-signing roadmap.
Unit-ball projections for isotropic signing
Norm duality and a countable dense direction class supply the unit-ball specialization of the cited contraction interface in the row-signing roadmap.
Every real Euclidean vector has a unit-ball direction attaining its norm.
Formal statement
Proof (Lean source)
The signed norm maximum equals the supremum of absolute projections summed over the rows; this is the deterministic duality step in the roadmap.
Formal statement
Proof (Lean source)
A separable Euclidean direction set gives a countable class that simultaneously approximates every finite evaluation set of its linear projections.
Formal statement
Proof (Lean source)
The unit-ball projection class satisfies factor-two contraction, with no extra separability assumption on its callers. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Unit-ball projections recover the length of each Rademacher sum exactly. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The unit-ball linear Rademacher average is exactly the expected signed norm, so no slack is introduced by the projection representation. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Removing the population mean from each unit projection bounds the signed norm maximum by the row count plus the largest centered empirical fluctuation. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SigningPartition 8 declarations The selected rows and their complement are independent product samples after reindexing.
Reindexing the random signing partition
The selected rows and their complement are independent product samples after reindexing. Their cross maximum is controlled by the independent-group bound, and partition averaging completes the expected minimum-signing lower bound.
An indicator sum is exactly the sum on its selected subtype.
Formal statement
Proof (Lean source)
[ Selected and complementary arrays, each indexed by its own finite cardinality.
Definition (Lean source)
Partition reindexing preserves the product law, proving independence of the groups.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
A realized partition's cross maximum is bounded by the independent-group projection maximum after reindexing, including either empty group.
Formal statement
Proof (Lean source)
The explicit cross-group error is bounded uniformly over all partitions of n rows. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Each fixed selector satisfies the independent-group cross bound under the original row law. Reindexing supplies the independence required by the roadmap. Under the stated conditions.
Formal statement
Proof (Lean source)
Averaging the uniform cross bound over fair selectors closes the random-partition step, with the exact factor four from the ordered-pair selection probability. Under the stated conditions.
Formal statement
Proof (Lean source)
Independent isotropic rows have the stated expected minimum-signing lower bound. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SigningRademacher 19 declarations Independent fair signs cancel every off-diagonal term without centering the row law.
Rademacher moments for isotropic signing
Independent fair signs cancel every off-diagonal term without centering the row law. The resulting exact second moment gives the square-root first-moment estimate used by the symmetrization and contraction roadmap. Finite projection classes satisfy the cited contraction bound, and cross-group maxima are expressed as absolute projections.
Fair signs annihilate the entire off-diagonal form for deterministic rows.
Formal statement
Proof (Lean source)
The fair-sign second moment is precisely the deterministic diagonal energy.
Formal statement
Proof (Lean source)
The fair-sign first moment is bounded by the square root of diagonal energy.
Formal statement
Proof (Lean source)
Averaging the exact fair-sign moment over isotropic rows gives sample size times dimension. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Joint row/sign squared energy is integrable using only coordinate second moments. Under the stated conditions.
Formal statement
Proof (Lean source)
Joint Rademacher averaging has first moment at most the isotropic square-root scale. Under the stated conditions.
Formal statement
Proof (Lean source)
A finite function class is its own countable pointwise-dense subclass. Under the stated conditions.
Formal statement
Proof (Lean source)
Linear projections in a bounded direction class are controlled by the random signed norm. Under the stated conditions.
Formal statement
Proof (Lean source)
The cited factor-two contraction applies to every finite bounded projection family. This is the deterministic class used after conditioning on the other row group. Under the stated conditions.
Formal statement
Proof (Lean source)
Signs chosen according to a fixed projection attain the sum of absolute projections. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
[ Maximum norm over all signings of deterministic rows.
Definition (Lean source)
Every signed norm is at most the finite maximum.](goal) This uses the stated conclusion.
Formal statement
Proof (Lean source)
The maximum signed norm is nonnegative, including the empty sample.
Formal statement
Proof (Lean source)
The sum of row lengths is a common envelope for all signed norms.
Formal statement
Proof (Lean source)
The finite signed-norm maximum is Borel. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Coordinate second moments integrate the signed-norm maximum's common envelope. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The conditional finite class of all signed sums satisfies the contraction bound. Under the stated conditions.
Formal statement
Proof (Lean source)
Disjoint groups allow their signs to be optimized independently, even though the original cross form uses a single signing of all rows. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Conditional on the complementary group, the cross-group maximum is exactly a finite supremum of sums of absolute projections, as in the proof roadmap.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SigningSymmetrization 20 declarations The row-signing roadmap introduces an independent ghost sample, exchanges paired observations with fair signs, and uses the triangle inequality before contraction.
First-moment symmetrization for finite projection classes
The row-signing roadmap introduces an independent ghost sample, exchanges paired observations with fair signs, and uses the triangle inequality before contraction. These comparisons need only integrability of the finite class; no boundedness or higher moments are imposed.
A finite absolute supremum is integrable if each measurable member is integrable. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Largest population-centered sum over a deterministic finite class.
Definition (Lean source)
Largest two-copy empirical difference over a deterministic finite class.
Definition (Lean source)
Largest signed empirical sum over a deterministic finite class.
Centered empirical sums have an integrable finite supremum under the iid law.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Ghost differences have an integrable finite supremum under the two-copy law. Under the stated conditions.
Formal statement
Proof (Lean source)
Each fixed-sign empirical supremum is integrable under the iid law. Under the stated conditions.
Formal statement
Proof (Lean source)
A centered empirical sum is exactly the expectation of its ghost difference. Under the stated conditions.
Formal statement
Proof (Lean source)
Conditional Jensen compares the centered supremum to an independent ghost sample. Under the stated conditions.
Formal statement
Proof (Lean source)
Paired-coordinate exchange turns each ghost difference into its fixed-sign version. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The signed ghost supremum is bounded by the two separate signed suprema.
Formal statement
Proof (Lean source)
The product-law symmetry and triangle inequality give the factor-two ghost bound for every fixed signing, before taking the fair-sign average. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The fair-sign empirical supremum is jointly integrable under sample and sign laws. Under the stated conditions.
Formal statement
Proof (Lean source)
Averaging conditional Jensen bounds the centered expectation by the ghost expectation. Under the stated conditions.
Formal statement
Proof (Lean source)
A finite integrable class satisfies first-moment Rademacher symmetrization with factor two, including an empty sample. Under the stated conditions.
Formal statement
Proof (Lean source)
Passing a finite real supremum through ofReal agrees with the nonnegative supremum. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The finite-class real signed supremum represents the extended-valued contraction interface exactly, with no moment lost in the change of codomain. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Absolute transformation of a finite class agrees exactly with the signed supremum used in the contraction interface. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Symmetrization followed by the cited contraction controls a finite class of absolute functions by four times the original linear Rademacher average. Keeping the exact average permits the subsequent independent-group isotropy argument. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Absolute projections in any finite bounded direction class have expected centered supremum at most four times its radius times the isotropic square-root scale. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SpectralCounting 27 declarations A square-root box contains every supported frequency below a given complexity.
Finite counts through a spectral complexity cutoff
A square-root box contains every supported frequency below a given complexity. The resulting finite count bounds the global indices of both real rows, including ties.
Each coordinate of a supported frequency is bounded by its averaged energy. Under the stated conditions.
Formal statement
Proof (Lean source)
The square-root box contains every frequency of support one or two below the cutoff. Under the stated conditions.
Formal statement
Proof (Lean source)
Integer magnitudes respect the floor of the real square-root bound. Under the stated conditions.
Proof (Lean source)
A support-one frequency has exactly its single coordinate's squared complexity. Under the stated conditions.
Formal statement
Proof (Lean source)
The representatives through a complexity cutoff, including every tie.
Definition (Lean source)
The finite cutoff set captures precisely all representatives below its cutoff. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The entire global prefix up to an indexed frequency lies below its complexity. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Counting the global prefix bounds both real-row indices, even at complexity ties. Under the stated conditions.
Formal statement
Proof (Lean source)
The first nonzero coordinate of a singleton representative is positive. Under the stated conditions.
Formal statement
Proof (Lean source)
The smaller support coordinate of a pair representative is positive. Under the stated conditions.
Formal statement
Proof (Lean source)
Every representative has either a singleton or an increasing two-coordinate support. Under the stated conditions.
Formal statement
Proof (Lean source)
[ Single-coordinate integer frequencies with positive amplitude.
Two-coordinate representatives, with a positive first amplitude and a signed second one.
Definition (Lean source)
Every positive integer of bounded magnitude has a positive-amplitude index.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
Every nonzero bounded integer is a signed positive-amplitude index. Under the stated conditions.
Formal statement
Proof (Lean source)
A singleton representative below the cutoff is in the finite main-effect encoding. Under the stated conditions.
Formal statement
Proof (Lean source)
A pair representative below the cutoff is in the finite signed pair encoding. Under the stated conditions.
Formal statement
Proof (Lean source)
There are exactly binomially many increasing coordinate pairs. The asserted mathematical result follows.
Proof (Lean source)
Main effects and signed pairs give the finite cutoff-count bound before scalar simplification.
Formal statement
Proof (Lean source)
A nonzero integer frequency has averaged squared complexity at least one. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
In dimension at least two, the coordinate count is at most twice the pair count. Under the stated conditions.
Formal statement
Proof (Lean source)
The two real rows for every conjugate pair have total cutoff count at most twelve times the pair count and the complexity cutoff. Under the stated conditions.
Formal statement
Proof (Lean source)
Both real row indices of an indexed frequency obey the explicit twelve-pair cutoff. Under the stated conditions.
Formal statement
Proof (Lean source)
Negating a frequency preserves its support. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Opposite frequencies have the same averaged squared complexity.
Formal statement
Proof (Lean source)
Every supported nonzero frequency has exactly a prescribed orientation up to sign. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every support-one or support-two frequency occurs in the global real-row enumeration up to the unique choice of conjugate orientation. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SpectralFrequency 19 declarations The positive frequencies on the first coordinate supply an explicit finite family inside every sufficiently large frequency box.
Elementary properties of the ordered spectral frequencies
The positive frequencies on the first coordinate supply an explicit finite family inside every sufficiently large frequency box. This proves that the ordered prefix lookup is in range and hence that every selected frequency is a nonzero representative supported on at most two coordinates.
The positive frequency of size m + 1 on the first coordinate.
Definition (Lean source)
In positive dimension, the first-coordinate frequency has singleton support. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
In positive dimension, every first-coordinate frequency is a prescribed representative. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Frequencies of distinct positive sizes on the first coordinate are distinct. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The first J positive first-coordinate frequencies lie in the radius-J box. This uses the hm hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The strict spectral comparator is false on equal frequencies. This uses the stated conclusion.
Formal statement
Proof (Lean source)
A transitive strict comparator that compares every pair of distinct entries makes merge sort strictly pairwise sorted on every noduplicated input. This uses the htrans hypothesis, the hcompare hypothesis, the hnodup hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The strict spectral comparator is transitive. This uses the hab hypothesis, the hbc hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
A frequency is determined by its coordinate list. This uses the stated conclusion.
Proof (Lean source)
Distinct frequencies are comparable by the strict spectral comparator. This uses the hab hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Every ordered frequency box is strictly pairwise sorted by the prescribed comparator. This uses the stated conclusion.
Formal statement
Proof (Lean source)
A frequency placed before another by the spectral comparator has no larger complexity. This uses the h hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
In positive dimension, the representative part of the radius-J box has at least J elements. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
In positive dimension, the ordered radius-J box contains at least J entries. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
The lookup defining the index-th feature frequency is in range in positive dimension. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
In positive dimension, the feature-frequency lookup never uses its zero fallback. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
In positive dimension, every selected feature frequency belongs to its defining box and is a prescribed representative. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
In positive dimension, every selected feature frequency is a prescribed representative. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
Every selected feature frequency has nonempty support. This uses the hd hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SpectralPrefix 20 declarations Two-coordinate witnesses bound the complexity of each selected frequency.
Stability of finite spectral prefixes
Two-coordinate witnesses bound the complexity of each selected frequency. Frequencies outside its defining box have strictly greater complexity, so enlarging the box preserves all earlier entries, including the lexicographic order at ties.
[ A family of two-coordinate representatives with controlled complexity.
Definition (Lean source)
The witness family has exactly the first two coordinates in its support.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The witness family consists of distinct representatives. Under the stated conditions.
Formal statement
Proof (Lean source)
Distinct witness sizes give distinct frequencies. Under the stated conditions.
Formal statement
Proof (Lean source)
The first J witnesses belong to the radius-J frequency box. Under the stated conditions.
Formal statement
Proof (Lean source)
The exact witness complexity uses the averaged two-coordinate normalization. Under the stated conditions.
Formal statement
Proof (Lean source)
The witness family supplies J representatives below a strict outside-box cutoff. Under the stated conditions.
Formal statement
Proof (Lean source)
Membership in the sorted box is exactly boundedness and representative status. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Sorted frequency boxes have no duplicate entries.
Formal statement
Proof (Lean source)
Enough low-complexity witnesses bound the complexity of an indexed sorted entry. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Any supported representative outside a box exceeds the witness cutoff strictly. Under the stated conditions.
Formal statement
Proof (Lean source)
Enlarging a box leaves its low-complexity sorted portion unchanged. Under the stated conditions.
Formal statement
Proof (Lean source)
Filtering a list preserves an index if all entries up to that index pass the test. Under the stated conditions.
Formal statement
Proof (Lean source)
Every selected frequency has exactly the same index in every larger box. Under the stated conditions.
Formal statement
Proof (Lean source)
The indexed frequency sequence is strictly sorted globally, including ties. Under the stated conditions.
Formal statement
Proof (Lean source)
Global prefix stability prevents any frequency from being enumerated twice. Under the stated conditions.
Formal statement
Proof (Lean source)
Every finite integer frequency lies in a positive-radius box. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
In a sorted box, enough entries below a cutoff bound the indexed entry by that cutoff. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The indexed sequence enumerates every prescribed representative. Under the stated conditions.
Formal statement
Proof (Lean source)
A single finite box computes exactly the entire global prefix requested by rounding. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.SpectralRisk 6 declarations The torus kernel averages only the fresh rounding seeds.
Fourier representation of the spectral seed-image design
The torus kernel averages only the fresh rounding seeds. Reflection and the common shift are then transported by the proved reflection identity.
[ Joint measurability of rounding on the torus feature rows. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The fresh-seed kernel on torus samples.
Definition (Lean source)
Rounding seed images are probability measures.
Definition (Lean source)
Integrating the torus kernel is exactly integrating the fresh rounding seeds.](goal) Under the stated conditions. This uses the stated conclusion.
Formal statement
Proof (Lean source)
The original-sample kernel averages the torus kernel over reflection and shift. Under the stated conditions.
Formal statement
Proof (Lean source)
Exact Fourier loss representation for the spectral branch of the design. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.UpperBound 26 declarations The single design is fair and outcome independent.
Spectral upper-bound proof subsystem
The single design is fair and outcome independent. The scalar spectral estimate converts its frequencywise minimum bound into the simultaneous fractional rate; the Fourier-row assembly and both design branches have proved risk bounds.
The spectral construction is an admissible design for every sample size and dimension.
Formal statement
Proof (Lean source)
A truncated linear weight is bounded by every fractional power through exponent one. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The frequencywise minimum is dominated by the pooled Sobolev weight times the minimum rate, including the endpoint exponent one. Under the stated conditions.
Formal statement
Proof (Lean source)
Odd feature rows are the normalized real parts of the indexed characters. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Even feature rows are the normalized imaginary parts of the same indexed characters.
Formal statement
Proof (Lean source)
The squared character imbalance is exactly half the sum of its two real-row squares, for every deterministic sample and every real coefficient vector.
Formal statement
Proof (Lean source)
The scalar rate bound applies to the precise angular Sobolev normalization. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The exact pooled budget controls the entire truncated spectral sum at the minimum rate, without a frequency-scale sum or logarithmic loss. Under the stated conditions.
Formal statement
Proof (Lean source)
Every terminal spectral sign has a finite second moment under the rounding seeds. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The square of any deterministic test row is integrable under the actual spectral rounding.
Formal statement
Proof (Lean source)
The proved ordered-rounding theorem controls each actual spectral test row, including rows beyond the supplied prefix. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
A character inherits the average of its two real-row moment bounds. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
Real signs make the imbalances at opposite frequencies complex conjugates, so their squared moduli coincide pointwise.
Formal statement
Proof (Lean source)
The same ordered-row moment estimate holds for the other member of each conjugate frequency pair.
Formal statement
Proof (Lean source)
Character squared imbalance is integrable, by its exact real-row decomposition.
Formal statement
Proof (Lean source)
The conditional character bound in the nonnegative integral form needed for Tonelli and the reflected Fourier loss identity.
Formal statement
Proof (Lean source)
The explicit frequency count converts the indexed rounding bound to its spectral minimum. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
Every nonzero frequency of support one or two obeys the same conditional minimum bound, regardless of its conjugate orientation. Under the stated conditions.
Formal statement
Proof (Lean source)
The supported conditional character estimate in the nonnegative integral form for Tonelli. Under the stated conditions.
Formal statement
Proof (Lean source)
Scaling the conditional minimum gives the normalized loss weight exactly. Under the stated conditions.
Formal statement
Proof (Lean source)
Fourier coefficients outside the nonzero order-two support vanish. Under the stated conditions.
Formal statement
Proof (Lean source)
The original spectral branch obeys the truncated Fourier risk estimate. Under the stated conditions.
Formal statement
Proof (Lean source)
Independent fair signs cancel the real-valued off-diagonal terms. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The independent-sign branch's loss is exactly four times the cube second moment. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The cube Sobolev budget bounds independent-sign loss by four. Under the stated conditions.
Formal statement
Proof (Lean source)
The concrete spectral design is fair, outcome independent, and has the stated upper risk. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.Helpers.Vanishing 2 declarations The binomial-ratio and square-root dimension criteria include arbitrary oscillating sequences.
Vanishing comparison-scale subsystem
The binomial-ratio and square-root dimension criteria include arbitrary oscillating sequences.
The pair count is uniformly comparable to the squared dimension. Under the stated conditions.
Formal statement
Proof (Lean source)
The explicit scale vanishes exactly below the square-root dimension frontier. Under the stated conditions.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.TCapacityAnswer 1 declarations This capstone retains the concrete attaining kernel, legal prior, actual Gaussian HT transfer, exact frozen-class capacity, and the entire dimension-sequence equivalence.
Complete answer to the bivariate design-capacity question
This capstone retains the concrete attaining kernel, legal prior, actual Gaussian HT transfer, exact frozen-class capacity, and the entire dimension-sequence equivalence.
The single smoothness-free kernel and independent legal prior give the complete capacity answer, including actual HT excess and exact published-law minimax transfer. This uses the hContraction_of_gate hypothesis, the hExcess_of_gate hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.TFullDesignLower 14 declarations The explicit lower constant is chosen outside the sample and dimension quantifiers.
The full-design prior lower bound
The explicit lower constant is chosen outside the sample and dimension quantifiers. Every admissible covariate-dependent randomized original-sign law is covered. Finite coefficient averaging gives the exact feature-energy identity, which is compared with the pointwise minimum and the isotropic signing lemma. The explicit ceiling cutoff then gives the published lower constant. Prior legality and isotropic signing retain their separate proof obligations in the imported modules.
Uniform coefficient signs have diagonal second moments for any finite index type.
Formal statement
Proof (Lean source)
A finite independent coefficient prior averages a square to its diagonal energy.
Formal statement
Proof (Lean source)
The nonnegative finite prior has the same diagonal-energy identity.
Formal statement
Proof (Lean source)
Before averaging over the sample, coefficient averaging produces precisely the squared feature-signing norm with the stated normalization.
Formal statement
Proof (Lean source)
Coefficient averaging commutes with the fixed design and covariate integrals, giving the exact prior-risk identity from the lower-bound roadmap.
Formal statement
Proof (Lean source)
Any covariate-dependent randomized design dominates the pointwise minimum over all original sign vectors. Fairness is not needed for this comparison.
Formal statement
Proof (Lean source)
The prescribed cutoff has enough features for the isotropic signing threshold. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The ceiling cutoff loses only the explicit factor 16384 in squared frequency. The asserted mathematical result follows.
Formal statement
Proof (Lean source)
The cosine feature map transports independent uniform rows to the isotropic row law, so the signing lemma lower-bounds the original-sample minimum. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
The ceiling comparison yields the paper's explicit lower constant and scale. Under the stated conditions.
Formal statement
Proof (Lean source)
After isotropic signing, normalization cancels the original sample size and feature dimension, leaving the inverse-frequency lower bound. Under the stated conditions.
Formal statement
Proof (Lean source)
A finite coefficient prior supported on the legal class cannot exceed the fixed-function supremum, even when risks are infinite. Under the stated conditions.
Formal statement
Proof (Lean source)
A lower bound for every design's legal finite prior transfers to full capacity. Under the stated conditions.
Formal statement
Proof (Lean source)
The independent legal cosine prior lower-bounds every design and hence capacity. This uses the hContraction_of_gate hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.TLogFreeBivariateCapacity 5 declarations All asserted bounds refer to the concrete smoothness-free original-sample design.
Log-free bivariate full-design capacity
All asserted bounds refer to the concrete smoothness-free original-sample design. Both law-level capacity transfer and the converse-only bounded-density comparison are retained, as are the oscillating-sequence frontier and Gaussian sample-size corollaries.
The Gaussian identity identifies each admissible design's worst excess with loss. Under the stated conditions.
Formal statement
Proof (Lean source)
The Gaussian identity also identifies the full admissible-design infimum. Under the stated conditions.
Formal statement
Proof (Lean source)
Inverting the upper power bound gives the sufficient sample-size condition. Under the stated conditions.
Formal statement
Proof (Lean source)
Below saturation, inverting the lower power bound gives the necessary sample size. Under the stated conditions.
Formal statement
Proof (Lean source)
One original-sample kernel attains the log-free scale for all smoothnesses, with a legal independent finite prior, the exact published capacity, and the square-root frontier. This uses the hContraction_of_gate hypothesis, the hExcess_of_gate hypothesis, the stated conclusion.
Formal statement
Proof (Lean source)
CausalSmith.Experimentation.EXP_BivariateSobolevDesignCapacity_Research.TPublishedClassInclusion 5 declarations The d=2 converse and the independent-sign L² identity retain the full frozen outcome class.
Strict published-class inclusion and independent-sign comparison
The d=2 converse and the independent-sign L² identity retain the full frozen outcome class.
Independent fair signs have identity second-moment matrix.
Formal statement
Proof (Lean source)
Averaging a deterministic signed sum over all independent fair signs leaves only its diagonal squares.
Formal statement
Proof (Lean source)
Independent fair assignment has exactly four times the prognostic second moment as its original-unit imbalance loss. Under the stated conditions, the asserted mathematical result follows.
Formal statement
Proof (Lean source)
In dimension two the comparison scale is the single-pair power of sample size. Under the stated conditions.
Formal statement
Proof (Lean source)
Gaussian completions form a proper published subclass, with the same admissible kernels, a single-pair lower exponent, and independent-sign loss at most four. This uses the hExcess_of_gate hypothesis, the hContraction_of_gate hypothesis, the stated conclusion.