Formalization: Contour Instruments for Partially Linear Models with Cumulant-separated Treatment Noise
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.
Basic 61 declarations This file gives the observed-data law, residuals, exact assumptions, model classes, and decision-theoretic losses shared by the paper's statements.
Spectral annihilation for partially linear models: common setup
This file gives the observed-data law, residuals, exact assumptions, model classes, and decision-theoretic losses shared by the paper's statements. The PO substrate is deliberately bypassed: this paper ranges over triangular classes of observed-data laws rather than one fixed potential-outcome system.
The observation space: a single observed unit is a triple made of a covariate value drawn from the covariate space, a real-valued treatment, and a real-valued outcome. Every law considered in the paper is a probability distribution on this space.
Definition (Lean source)
Primitive constants and deterministic code-radius sequences.
Definition (Lean source)
A law and its deterministic supplied regression codes.
Definition (Lean source)
The observed-data law carried by a model is a probability measure, i.e. it assigns total mass one to the observation space. This is exactly the normalization recorded among the model's defining conditions, made available automatically wherever a probability law is required.
Definition (Lean source)
Covariate coordinate.
Definition (Lean source)
Treatment coordinate.
Outcome coordinate.
An observed unit is the coordinate triple (X,T,Y).
Definition (Lean source)
Covariate marginal of the observed law.
Definition (Lean source)
Current-index clipping of an externally supplied treatment-code sequence.
Definition (Lean source)
Clipped treatment code.
Definition (Lean source)
Current-index clipping of an externally supplied outcome-code sequence.
Definition (Lean source)
Clipped outcome code.
Definition (Lean source)
Treatment noise T-g0(X).
Outcome noise Y-q0(X)-theta0*eta.
Treatment-code residual contamination.
Definition (Lean source)
Observable learned treatment residual.
Definition (Lean source)
Outcome-side contamination.
Definition (Lean source)
The cumulant is the real part of the kth derivative at zero of the analytic logarithm of the treatment-noise complex MGF.
Definition (Lean source)
The fourth cumulant, independent of the parameter field k.
Definition (Lean source)
Exact order-dependent constant in the localization radius.
Definition (Lean source)
Explicit transform-zero localization radius.
Definition (Lean source)
The radius of the window over which the procedure searches for a zero of the treatment-noise transform: one unit larger than the explicit localization radius. The extra unit guarantees that the window strictly contains the zero whose existence the localization radius certifies, so the search cannot fail by landing on the boundary.
Definition (Lean source)
The deterministic lower and upper inference folds.
The upper inference fold at sample size n: the collection of unit indices lying at or beyond the halfway point of the sample, the halfway point being the integer part of half the sample size. Together with the lower fold it splits the sample deterministically into two halves for cross-fitting.
Independent and identically distributed sampling: the joint law of the n observed units is the n-fold product of the single-unit observed-data law, so the units are drawn independently, each from that same law.
Definition (Lean source)
The treatment noise, that is the treatment minus its conditional mean given the covariates, is statistically independent of the covariates under the observed-data law.
Definition (Lean source)
The sigma-algebra generated by (X,T).
Definition (Lean source)
The outcome noise — the outcome minus its conditional mean given the covariates minus the target coefficient times the treatment noise — is integrable and has conditional mean zero given the covariates and the treatment jointly.
Definition (Lean source)
The target coefficient of the partially linear model is bounded in absolute value by the target range constant Ctheta, i.e. it lies in the symmetric interval of that half-width.
Definition (Lean source)
The treatment regression function — the conditional mean of the treatment given the covariates — is bounded in absolute value by the treatment-regression range constant Cg at almost every covariate value under the covariate marginal.
Definition (Lean source)
The outcome regression function — the conditional mean of the outcome given the covariates — is bounded in absolute value by the outcome range constant Cq at almost every covariate value under the covariate marginal.
Definition (Lean source)
The outcome variable itself is bounded in absolute value by the outcome range constant Cq almost surely under the observed-data law.
Definition (Lean source)
The treatment noise is sub-Gaussian at the treatment-noise scale psieta: the exponential of its squared value divided by the squared scale is integrable and has expectation at most two.
Definition (Lean source)
The outcome noise is conditionally sub-Gaussian given the covariates at the outcome-noise scale psixi: the exponential of its squared value divided by the squared scale is integrable, and its conditional expectation given the covariates is at most two at almost every covariate value.
Definition (Lean source)
The cumulant of the treatment noise at the order used throughout the paper is bounded away from zero: its absolute value is at least the separation constant delta.
Definition (Lean source)
At every sample size of one or more, the clipped treatment code approximates the true treatment regression function to within the first accuracy sequence, the error being measured in the norm of exponent s under the covariate marginal.
Definition (Lean source)
The treatment-side accuracy budget imposed at a single sample size: the clipped treatment code approximates the true treatment regression function to within the first accuracy sequence evaluated at that sample size, measured in the norm of exponent s under the covariate marginal.
Definition (Lean source)
At every sample size of one or more, the clipped outcome code approximates the true outcome regression function to within the second accuracy sequence, the error being measured in the norm of exponent s under the covariate marginal.
Definition (Lean source)
The outcome-side accuracy budget imposed at a single sample size: the clipped outcome code approximates the true outcome regression function to within the second accuracy sequence evaluated at that sample size, measured in the norm of exponent s under the covariate marginal.
Definition (Lean source)
At every sample size of one or more, the clipped treatment code approximates the true treatment regression function to within the first accuracy sequence, with the error measured in the norm of exponent r — the fixed order of the cumulant analysis — under the covariate marginal.
Definition (Lean source)
The comparator's treatment-side accuracy budget imposed at a single sample size: the clipped treatment code approximates the true treatment regression function to within the first accuracy sequence evaluated at that sample size, measured in the norm of exponent r under the covariate marginal.
Definition (Lean source)
At every sample size of one or more, the clipped outcome code approximates the true outcome regression function to within the second accuracy sequence, with the error measured in the norm of exponent r under the covariate marginal.
Definition (Lean source)
The comparator's outcome-side accuracy budget imposed at a single sample size: the clipped outcome code approximates the true outcome regression function to within the second accuracy sequence evaluated at that sample size, measured in the norm of exponent r under the covariate marginal.
Definition (Lean source)
The treatment noise is exactly centered Gaussian with standard deviation sigma, i.e. its distribution under the observed-data law is the normal law with mean zero and variance the square of sigma.
Definition (Lean source)
At every sample size of one or more, the absolute deviation between the clipped treatment code and the true treatment regression function is integrable under the covariate marginal, and its mean is at most the first accuracy sequence evaluated at that sample size.
Definition (Lean source)
The mean-absolute-error accuracy budget imposed at a single sample size: the deviation between the clipped treatment code and the true treatment regression function is integrable under the covariate marginal, with mean at most the first accuracy sequence evaluated at that sample size.
Definition (Lean source)
The broad non-Gaussian model class at a given sample size: partially linear laws whose treatment noise is independent of the covariates, whose outcome noise is mean-independent of the covariate-treatment pair, whose target coefficient and whose two regression functions all obey their range bounds, whose treatment noise is sub-Gaussian and whose outcome noise is conditionally sub-Gaussian at the stated scales, whose treatment-noise cumulant is separated from zero, and whose treatment code attains the first accuracy sequence in mean absolute error at that sample size.
Definition (Lean source)
The Gaussian model class at a given sample size: partially linear laws whose treatment noise is independent of the covariates and exactly centered Gaussian with standard deviation sigma, whose outcome noise is mean-independent of the covariate-treatment pair, whose target coefficient and treatment regression function obey their range bounds, whose outcome is bounded almost surely, and whose treatment and outcome codes both attain their accuracy sequences in the norm of exponent s at that sample size.
Definition (Lean source)
The published comparator's model class at a given sample size: partially linear laws with treatment noise independent of the covariates, outcome noise mean-independent of the covariate-treatment pair, target coefficient and both regression functions inside their range bounds, sub-Gaussian treatment noise and conditionally sub-Gaussian outcome noise, a treatment-noise cumulant separated from zero, and both the treatment and the outcome code attaining their accuracy sequences in the norm of exponent r at that sample size.
Definition (Lean source)
The comparison subclass at a given sample size: every law in the broad non-Gaussian class that additionally has both its treatment code and its outcome code attaining their accuracy sequences in the norm of exponent s.
Definition (Lean source)
An estimator at sample size n is a real-valued function of the entire sample, that is of the n observed covariate-treatment-outcome triples. No measurability is imposed here; the risk definitions restrict to measurable estimators where that is needed.
I.i.d. product law used by all risks.
Extended nonnegative mean squared error of an estimator at one law.
Minimax mean squared error on a supplied set of laws.
Definition (Lean source)
The lower quantile at level one minus the confidence parameter gamma of a real-valued statistic of the sample, the quantile being taken of the distribution the statistic induces when the n units are drawn independently from the given law.
Definition (Lean source)
Gaussian generalized-quantile minimax loss with fixed supplied codes.
Definition (Lean source)
The three losses defined together in the paper: non-Gaussian MSE, Gaussian-intersection MSE, and Gaussian generalized-quantile risk.
Definition (Lean source)
First projection of the jointly anchored minimax-loss triple.
Definition (Lean source)
Second projection of the jointly anchored minimax-loss triple.
Definition (Lean source)
Third projection of the jointly anchored minimax-loss triple.
Definition (Lean source)
Helpers.AdaptiveSelectorPacket 19 declarations This module packages the deterministic split-fold facts, measurable empirical transform errors, and selected-contour certificate used by the root-risk proof.
Good-event assembly for the adaptive contour selector
This module packages the deterministic split-fold facts, measurable empirical transform errors, and selected-contour certificate used by the root-risk proof.
The split-fold empirical residual-transform supremum error is Borel measurable as a function of the finite sample.
Formal statement
Proof (Lean source)
The split-fold empirical outcome-transform supremum error is Borel measurable as a function of the finite sample.
Formal statement
Proof (Lean source)
Absolute centered-factorial coefficient majorant for the residual transform on one inference fold.
Definition (Lean source)
Absolute centered-factorial coefficient majorant for the outcome-weighted transform on one inference fold.
Definition (Lean source)
The residual-transform disk error is pointwise dominated by its centered factorial-series majorant.
Formal statement
Proof (Lean source)
The outcome-transform disk error is pointwise dominated by its centered factorial-series majorant.
Formal statement
Proof (Lean source)
Residual-transform disk error on one inference fold.
Definition (Lean source)
Outcome-transform disk error on one inference fold.
Definition (Lean source)
For a model in the non-Gaussian spectral class, the residual-transform error on either inference fold — the largest discrepancy, over all points of the search disk, between the fold's empirical residual transform and its population counterpart — is a measurable function of the sample.
Formal statement
Proof (Lean source)
For a model in the non-Gaussian spectral class, the outcome-transform error on either inference fold — the largest discrepancy, over all points of the search disk, between the fold's empirical outcome transform and its population counterpart — is a measurable function of the sample.
Formal statement
Proof (Lean source)
Deterministic perturbation scale of the selected population contour.
Definition (Lean source)
The explicit constant in the adaptive selector's inverse-sample-size MSE bound.
Definition (Lean source)
Whenever the transform-accuracy input is strictly positive, the explicit constant appearing in the adaptive selector's inverse-sample-size mean squared error bound is strictly positive, so that bound is never vacuous.
Formal statement
Proof (Lean source)
On the two-fold small-error event, the selected estimator has the deterministic squared perturbation bound used by the risk proof.
Formal statement
Proof (Lean source)
Projection onto the certified parameter range globally bounds squared loss.
Formal statement
Proof (Lean source)
Risk bridge from the foldwise transform L² estimate to the adaptive selector's explicit MSE constant.
Formal statement
Proof (Lean source)
Uniform adaptive-selector MSE bound obtained from the empirical-transform L² theorem. The witness K depends only on the six displayed fixed class constants.
Formal statement
Proof (Lean source)
The preceding risk theorem with its proof's explicit transform constant, quantified before the covariate space.
Formal statement
Proof (Lean source)
The generalized-quantile consequence of any positive adaptive-selector MSE constant, at the paper's probability level 1 - gamma.
Formal statement
Proof (Lean source)
Helpers.AffineGaussianKL 15 declarations Kernel and bind representations of the affine outcome channel, used to reduce its KL divergence to the equal-variance Gaussian location formula.
KL control for affine Gaussian outcome paths
Kernel and bind representations of the affine outcome channel, used to reduce its KL divergence to the equal-variance Gaussian location formula.
The scalar innovation channel obtained after expressing an affine outcome law in the coordinates of a fixed reference parameter.
Definition (Lean source)
The scalar innovation channel — which, given the covariates and the treatment, draws a normal variable centred at the parameter displacement times the treatment innovation, with variance the square of the innovation scale — is a probability kernel: every one of its conditional slices is a probability measure.
Definition (Lean source)
Each scalar slice is the equal-variance Gaussian whose mean is the parameter displacement times the retained treatment innovation.
Formal statement
Proof (Lean source)
In reference affine coordinates, the observed affine Gaussian law is the pushforward of the retained (X,T) law and the scalar shifted innovation.
Formal statement
Proof (Lean source)
The affine outcome mechanism applied to (X,T) and a scalar innovation.
Definition (Lean source)
The affine outcome mechanism — which maps covariates, treatment, and a scalar innovation to the observed triple whose outcome coordinate is the baseline outcome regression plus the treatment coefficient times the treatment innovation plus that scalar innovation — is jointly measurable.
Formal statement
Proof (Lean source)
Conditional affine Gaussian outcome channel given (X,T).
Definition (Lean source)
The conditional affine Gaussian outcome channel — which, given the covariates and the treatment, returns the observed triple whose outcome is the baseline outcome regression plus the treatment coefficient times the treatment innovation plus centred Gaussian noise of the stated scale — is a probability kernel.
Definition (Lean source)
The affine Gaussian law is the base (X,T) law bound to its affine Gaussian outcome channel.
Formal statement
Proof (Lean source)
A channel slice is a pushforward of its centered Gaussian innovation.
Formal statement
Proof (Lean source)
A second parameter value can be represented through the first affine map by shifting only the Gaussian innovation mean.
Formal statement
Proof (Lean source)
Pointwise channel KL is bounded by the corresponding Gaussian-location KL, with shift proportional to the treatment residual.
Formal statement
Proof (Lean source)
The treatment innovation has an integrable square under the exact Luxemburg assumption.
Formal statement
Proof (Lean source)
One observation on the affine Gaussian path has KL bounded by the parameter displacement squared times the treatment-innovation second moment.
Formal statement
Proof (Lean source)
Tensorization turns the one-observation affine-path bound into the corresponding finite i.i.d. KL budget.
Formal statement
Proof (Lean source)
Helpers.AffineGaussianOutcomePath 40 declarations Measure-theoretic infrastructure for replacing the outcome coordinate by an affine partially-linear signal plus independent Gaussian noise while retaining the joint covariate-treatment law.
Affine Gaussian outcome paths
Measure-theoretic infrastructure for replacing the outcome coordinate by an affine partially-linear signal plus independent Gaussian noise while retaining the joint covariate-treatment law.
A conditional-mean identity is determined by the joint law of the conditioning variable and the integrand.
Formal statement
Proof (Lean source)
The measurable coordinate change from (X,T,Z) to (X,T,Y) for an affine Gaussian outcome path.
Definition (Lean source)
The fixed covariate-treatment marginal used by an affine outcome path.
The covariate–treatment marginal of a base model is again a probability distribution: discarding the outcome coordinate from an observed-data law leaves a law of total mass one on covariate–treatment pairs.
Definition (Lean source)
The Gaussian law with mean mu and variance tau ^ 2 is a probability measure.
Definition (Lean source)
The observed-data law obtained by adjoining centered Gaussian noise and applying the affine outcome coordinate change.
Definition (Lean source)
The observed-data law of an affine Gaussian outcome path is a probability distribution: it couples the base covariate–treatment marginal with an independent centered Gaussian noise draw of standard deviation tau and then relabels coordinates by a measurable bijection, and neither step changes total mass.
Definition (Lean source)
An affine Gaussian outcome law retains the base joint (X,T) marginal.
Formal statement
Proof (Lean source)
Treatment remains integrable along the affine Gaussian outcome path.
Formal statement
Proof (Lean source)
The supplied treatment regression remains integrable along the affine Gaussian outcome path.
Formal statement
Proof (Lean source)
The supplied outcome regression remains integrable along the affine Gaussian outcome path.
Formal statement
Proof (Lean source)
The treatment conditional mean is unchanged by replacing only the outcome channel with the affine Gaussian channel.
Formal statement
Proof (Lean source)
Under the affine law, algebraically extracting the residual returns the fresh Gaussian coordinate.
Formal statement
Proof (Lean source)
The extracted Gaussian residual is integrable.
Formal statement
Proof (Lean source)
Outcomes are integrable under the affine Gaussian outcome path.
Formal statement
Proof (Lean source)
The extracted Gaussian residual is independent of (X,T).
Formal statement
Proof (Lean source)
The extracted residual has conditional mean zero given the covariate.
Formal statement
Proof (Lean source)
Treatment residuals have conditional mean zero given the covariate along the affine Gaussian path.
Formal statement
Proof (Lean source)
The affine Gaussian outcome has conditional mean q0(X).
Formal statement
Proof (Lean source)
The model obtained by keeping every supplied nuisance component fixed and replacing the outcome channel by affine Gaussian noise.
Definition (Lean source)
Rebuilding a model along the affine Gaussian outcome path at slope theta and noise scale tau makes theta the treatment-effect parameter of the new model.
Formal statement
Proof (Lean source)
Rebuilding a model along the affine Gaussian outcome path leaves the treatment regression — the conditional mean of treatment given the covariate — exactly the one carried by the base model.
Formal statement
Proof (Lean source)
Rebuilding a model along the affine Gaussian outcome path leaves the outcome regression — the conditional mean of the outcome given the covariate — exactly the one carried by the base model.
Formal statement
Proof (Lean source)
Rebuilding a model along the affine Gaussian outcome path carries over the supplied sequence of treatment-regression estimates unchanged.
Formal statement
Proof (Lean source)
Rebuilding a model along the affine Gaussian outcome path carries over the supplied sequence of outcome-regression estimates unchanged.
Formal statement
Proof (Lean source)
The model-level outcome residual is exactly the extracted fresh Gaussian coordinate.
Formal statement
Proof (Lean source)
The model-level treatment residual is unchanged.
Formal statement
Proof (Lean source)
The affine model residual has the prescribed centered Gaussian law.
Formal statement
Proof (Lean source)
The affine model residual is independent of the retained (X,T) pair.
Formal statement
Proof (Lean source)
The affine model satisfies the paper's conditional mean-independence condition for its outcome residual.
Formal statement
Proof (Lean source)
The covariate-treatment marginal of the packaged affine model is the base model's covariate-treatment marginal.
Formal statement
Proof (Lean source)
The covariate marginal is retained by the affine Gaussian model.
Formal statement
Proof (Lean source)
Any property depending only on the treatment residual's pushforward law is unchanged along the affine Gaussian outcome path.
Formal statement
Proof (Lean source)
The treatment-residual complex MGF is retained by the affine model.
Formal statement
Proof (Lean source)
The cumulant separation functional is retained by the affine model.
Formal statement
Proof (Lean source)
Integrability of any measurable function of the treatment residual is retained along the affine path.
Formal statement
Proof (Lean source)
Integrals of measurable functions of the treatment residual are retained along the affine path.
Formal statement
Proof (Lean source)
Independence of the treatment residual and covariate is preserved along the affine Gaussian outcome path.
Formal statement
Proof (Lean source)
All non-Gaussian-class fields except the explicitly supplied Gaussian residual Luxemburg bound transport automatically along the affine path.
Formal statement
Proof (Lean source)
The published ACE comparator class is likewise retained, apart from the explicitly supplied Gaussian residual Luxemburg bound.
Formal statement
Proof (Lean source)
Helpers.AffineGaussianSubGaussian 4 declarations This file supplies the explicit exponential-square calculation needed to put the fresh Gaussian outcome residual in the paper's conditional sub-Gaussian class.
Luxemburg control for the affine Gaussian outcome path
This file supplies the explicit exponential-square calculation needed to put the fresh Gaussian outcome residual in the paper's conditional sub-Gaussian class.
At standard deviation psi / 4, a centered Gaussian's exponential-square moment at Luxemburg scale psi is finite and at most two.
Formal statement
Proof (Lean source)
The affine Gaussian model at scale psi / 4 satisfies the exact conditional Luxemburg requirement at scale psi.
Formal statement
Proof (Lean source)
The quarter-scale affine family remains in the broad non-Gaussian class throughout the original target range.
Formal statement
Proof (Lean source)
The quarter-scale affine family remains in the published ACE comparator class throughout the original target range.
Formal statement
Proof (Lean source)
Helpers.BoundedCertifiedComplex 92 declarations The generic contour API deliberately does not package multiplication of two certified values, because its global map interface is too strong for empirical exponential sums.
Paper-local bounded certified-complex combinators
The generic contour API deliberately does not package multiplication of two certified values, because its global map interface is too strong for empirical exponential sums. This file supplies the bounded name-level operations needed by the finite spectral evaluator. Every executable approximation remains a rational rectangle; semantic values occur only in the external certificate.
The certified name built for the complex exponential of a certified complex number denotes exactly the complex exponential of that number's exact value.
Formal statement
Proof (Lean source)
The certified name for the circle constant denotes exactly the real number pi.
Formal statement
The exact value of the certified sum of two certified complex numbers is the sum of their exact values.
Formal statement
Proof (Lean source)
A certified real regarded as a certified complex number with zero imaginary part.
Definition (Lean source)
Viewing a certified real number as a certified complex number with zero imaginary part leaves its exact value unchanged.
Formal statement
Proof (Lean source)
Recursive intersections of raw rectangle products.
Definition (Lean source)
Every stage of the recursively intersected rectangle products encloses the product of the two exact values, the stages are nested one inside the previous one, and each stage refines the raw rectangle product of the two inputs at that same stage.
Formal statement
Proof (Lean source)
The stage index at which the certified product of two complex numbers is guaranteed to be accurate to a requested rational tolerance: the larger of the two stage indices at which each factor's own modulus of convergence delivers an internally derived, magnitude-adjusted tolerance.
Definition (Lean source)
At the stage index selected by the product precision schedule, the rectangle enclosing the product of two certified complex numbers has width at most the requested tolerance.
Formal statement
Proof (Lean source)
Multiplication of bounded certified complex names.
Definition (Lean source)
The exact value of the certified product of two certified complex numbers is the product of their exact values.
Formal statement
Proof (Lean source)
Scaling a certified complex number by a rational number, realized as the certified product with the exact constant name for that rational.
Definition (Lean source)
Scaling a certified complex number by a rational number multiplies its exact value by that rational.
Formal statement
Proof (Lean source)
Repeated certified multiplication: the zero-th power is the certified constant one, and each further power multiplies the previous one by the base. Every intermediate product is itself a certified value, so the recursion carries its enclosure along.
Definition (Lean source)
The exact value of the n-fold certified power of a certified complex number is the n-th power of its exact value.
Formal statement
Proof (Lean source)
The certified sum of a finite list of certified complex numbers, obtained by folding certified addition along the list with the exact constant zero as the empty case.
Definition (Lean source)
The exact value of the certified sum of a list of certified complex numbers is the ordinary sum of their exact values.
Formal statement
Proof (Lean source)
Rational midpoint of a complex rectangle, coordinate by coordinate.
Definition (Lean source)
The midpoint represented as a constant certified complex name.
Definition (Lean source)
A rational envelope for the real exponential on the argument rectangle. The base three dominates Euler's number, and negative real parts are covered by the exponent zero branch.
Definition (Lean source)
The rational exponential envelope attached to a complex rectangle is nonnegative.
Formal statement
Proof (Lean source)
Deterministic Taylor fuel used by the certified exponential stage at the rational midpoint. This name is included in traces and schedule accounting.
Definition (Lean source)
Nested certified exponential enclosure at the rational midpoint.
Definition (Lean source)
The Taylor fuel recorded for the midpoint-centered exponential stage on a rectangle is, by definition, the certified-exponential stage fuel of the constant name for that rectangle's rational midpoint.
Formal statement
Proof (Lean source)
Midpoint-centered exponential interval. Its only dependence on the argument rectangle width is the displayed coordinatewise expansion.
Definition (Lean source)
The rational envelope bounds the real exponential at every real coordinate represented by the argument rectangle.
Formal statement
Proof (Lean source)
Midpoint Lipschitz control makes the widened midpoint enclosure sound for every complex point in the argument rectangle.
Formal statement
Proof (Lean source)
At the promoted complex-exponential precision, centered evaluation costs the algorithmic remainder plus exactly twice the explicit input-width allowance.
Formal statement
Proof (Lean source)
Promote a real rational interval to the real axis.
Definition (Lean source)
Whenever a rational interval encloses a real number, the rectangle obtained by placing that interval on the real axis encloses the same number viewed as a complex number.
Formal statement
Proof (Lean source)
Placing a rational interval on the real axis yields a rectangle of exactly the same width as the interval.
Formal statement
Proof (Lean source)
The certified-real bank radius is refined before it is multiplied by a unit-circle node. This is the only place where the bank radius enters a circle node.
Definition (Lean source)
Refining a certified real radius to a requested rational precision and placing the resulting interval on the real axis yields a rectangle that encloses the exact value of the radius.
Formal statement
Proof (Lean source)
The refined radius rectangle has width at most the requested rational precision.
Formal statement
Proof (Lean source)
A certified-real radius times the reused rational-radius-one circle node.
Definition (Lean source)
A Machin-π rectangle for 2 π i.
Definition (Lean source)
The Machin-series rectangle built at any precision encloses the complex number two pi times the imaginary unit.
Formal statement
Proof (Lean source)
The tangent rectangle is 2 π i times the certified-radius node.
Definition (Lean source)
The map-level target is quadratically smaller than the requested branch tolerance. The second factor of the requested tolerance pays for the box-local derivative term in BoundedComplexMap.Valid; the rational factor sixteen leaves room for quotient, tangent, quadrature, and normalization amplification.
Definition (Lean source)
Closed-form finite empirical-map fuel.
Definition (Lean source)
Closed-form modulus fuel used at a scheduled node.
Definition (Lean source)
Closed-form rational-bisection fuel used by the modulus square root.
Definition (Lean source)
Magnitude-aware Newton fuel for applying normInterval directly to a raw map rectangle.
Definition (Lean source)
Closed fuel for the finite rational endpoint operations at one node.
Definition (Lean source)
One bound dominating every non-circle finite-map fuel used by a node.
Definition (Lean source)
One third of the requested tolerance, packaged for the exact mesh constructor.
Definition (Lean source)
Exact endpoint-complete mesh from the local certified-transcendental schedule.
Definition (Lean source)
For a nonnegative Lipschitz magnitude, dividing that magnitude by the mesh count chosen by the spectral schedule leaves a discretization error of at most one third of the requested tolerance.
Formal statement
Proof (Lean source)
Paper-local explicit schedule with exact circle precision and dominating circle, empirical-map, norm, and square-root fuel.
Definition (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the input precision recorded by the paper's spectral schedule is exactly the circle input precision at radius one for the quadratically reduced node target.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the magnitude recorded by the paper's spectral schedule is exactly the supplied Lipschitz constant.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the circle exponential fuel at radius one, taken at the schedule's own mesh and at the reduced node target, does not exceed the fuel the schedule budgets.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the dominating non-circle fuel bound at the reduced node target does not exceed the fuel the spectral schedule budgets.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the magnitude-aware Newton fuel for taking the modulus of a raw map rectangle does not exceed the fuel the spectral schedule budgets.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the empirical-map fuel at the reduced node target does not exceed the fuel the spectral schedule budgets.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the modulus fuel at the reduced node target does not exceed the fuel the spectral schedule budgets.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the rational-bisection fuel used by the modulus square root at the reduced node target does not exceed the fuel the spectral schedule budgets.
Formal statement
Proof (Lean source)
For a nonnegative Lipschitz magnitude and a nonnegative amplification factor, the fuel for the finite rational endpoint operations at one node does not exceed the fuel the spectral schedule budgets.
Formal statement
Proof (Lean source)
A complex map whose interval program is certified only on one fixed box. The proof obligations are kept in BoundedComplexMap.Valid, allowing the finite program itself to remain executable data.
Definition (Lean source)
The correctness conditions carried by a box-local certified complex map: its magnitude and derivative envelopes are nonnegative, and for every rectangle contained in the fixed box and every complex point that rectangle encloses, all of the map's interval evaluations enclose the true value, the evaluations shrink as fuel increases, and at the stage chosen by the map's own precision schedule the output width is at most the derivative envelope times the input width plus the requested tolerance.
Definition (Lean source)
The box-local map that sends every point to one fixed rational complex number. Its interval evaluation is the degenerate rectangle at that number, its magnitude envelope is the sum of the absolute values of the two coordinates, and its derivative envelope is zero.
Definition (Lean source)
The box-local identity map. Its interval evaluation returns the input rectangle unchanged, its magnitude envelope is the largest modulus attained on the fixed box, and its derivative envelope is one.
Definition (Lean source)
Box-local addition. The two maps are added pointwise and their interval evaluators are added at matching fuel; the operation count, magnitude envelope and derivative envelope of the sum are the sums of those of the summands, and each summand is asked for half the requested tolerance so the combined error meets it.
Definition (Lean source)
Box-local subtraction. The two maps are subtracted pointwise and their interval evaluators are subtracted at matching fuel; the operation count, magnitude envelope and derivative envelope add rather than cancel, since they bound magnitudes, and each operand is asked for half the requested tolerance.
Definition (Lean source)
Box-local multiplication. The displayed envelopes are rational input data used by the local width schedule.
Definition (Lean source)
Box-local interval extension of z ↦ exp(c*z).
Definition (Lean source)
A tangent-corrected guarded quotient evaluator on a fixed disk.
Definition (Lean source)
The correctness conditions carried by a tangent-corrected guarded quotient evaluator on a fixed disk: the numerator and denominator maps are both valid on the box; at every mesh index up to the schedule's mesh the certified radius node lies inside the box and the denominator's evaluated rectangle there has squared modulus bounded away from zero; and the circle integrand of the quotient is Lipschitz in the circle parameter with the recorded constant.
Definition (Lean source)
One full contour-integrand node. Its value is the guarded quotient times the tangent; the radius is not multiplied anywhere else.
Definition (Lean source)
The endpoint-complete finite quadrature uses every index k ≤ mesh, including the terminal trapezoid endpoint.
Definition (Lean source)
Post-quadrature normalization by N * 2 π i; no normalization is hidden in the node family.
Definition (Lean source)
Divides a rectangle by the post-quadrature normalizing constant, the node count times two pi times the imaginary unit, using guarded rectangle division when that divisor is certified away from zero and returning the zero rectangle otherwise.
Definition (Lean source)
The exact rational width expression supplied by guarded rectangle division. Keeping it named makes the post-quadrature amplification visible to the branch schedule instead of hiding it in a fuel-only argument.
Definition (Lean source)
Whenever a rectangle encloses a complex number, the normalized rectangle encloses that number divided by the node count times two pi times the imaginary unit.
Formal statement
Proof (Lean source)
For a positive separation constant that bounds from below the squared modulus of the normalizing divisor, the normalized rectangle has width at most the explicit rational amplification bound recorded for guarded division.
Formal statement
Proof (Lean source)
For a positive separation constant that bounds from below the squared modulus of the normalizing divisor, and a target that the explicit amplification bound does not exceed, the normalized rectangle has width at most that target.
Formal statement
Proof (Lean source)
For any mesh index no larger than the schedule's mesh, the certified radius node encloses the point of the circle of that radius, centered at the origin, at the corresponding mesh parameter.
Formal statement
Proof (Lean source)
For a mesh index no larger than the schedule's mesh, given a bound on the largest modulus attained by the refined radius rectangle, a bound on the width of the unit-radius circle node, and the matching bound of one plus that width on the node's largest modulus, the certified radius node has width at most twice the sum of the modulus bound times the width bound and the shifted modulus bound times the radius precision.
Formal statement
Proof (Lean source)
For any mesh index no larger than the schedule's mesh, the tangent rectangle encloses the tangent vector of the circle of that radius at the corresponding mesh parameter.
Formal statement
Proof (Lean source)
For an evaluator satisfying its validity conditions, the finite endpoint-complete quadrature rectangle encloses the true contour integral of the numerator over denominator quotient around the circle of the evaluator's radius.
Formal statement
Proof (Lean source)
For an evaluator satisfying its validity conditions and a common width bound met by every node rectangle up to the mesh, the quadrature rectangle has width at most that node width plus the Lipschitz constant divided by the mesh count.
Formal statement
Proof (Lean source)
Executable rational endpoint operations. No semantic real or complex value is stored in this table: represented inputs are the value-opaque local approximant structures and their meanings are supplied externally.
Definition (Lean source)
The square-free endpoint rule used by the concrete bounded build for the absolute value of a real interval.
Definition (Lean source)
The complete, lossless resource trace is the schedule itself.
Definition (Lean source)
The list of mesh indices a node evaluation schedule visits: every index from zero up to and including the schedule's mesh fuel, so the terminal trapezoid endpoint is enumerated.
Definition (Lean source)
Exact executable algorithms required by the paper's bounded-build specification. This prevents an arbitrary sound operation table from being mistaken for the specified Machin/Taylor/bisection implementation.
Definition (Lean source)
When an operation table is the canonical one specified by the paper's bounded build, its real interval addition is the ordinary endpointwise addition of rational intervals.
Formal statement
Proof (Lean source)
When an operation table is the canonical one specified by the paper's bounded build, its complex interval addition is the ordinary coordinatewise addition of rational rectangles.
Formal statement
Proof (Lean source)
When an operation table is the canonical one specified by the paper's bounded build, its finite-infimum routine applied to a family of node intervals with a nonnegative Lipschitz constant and a positive mesh count returns the standard circle-mesh infimum enclosure.
Formal statement
Proof (Lean source)
When an operation table is the canonical one specified by the paper's bounded build, its quadrature routine applied to a family of node rectangles with a nonnegative Lipschitz constant and a positive mesh count returns the standard circle-mesh integral enclosure.
Formal statement
Proof (Lean source)
Full conditional build carrier for represented execution. It bundles the executable rational/complex arithmetic, guarded division, constructed transcendentals, circle nodes, finite extrema and quadrature, together with semantic soundness, effective fuel/modulus, endpoint, trace, and compilation certificates. Paper-specific spectral maps and schedules remain local derived facts and are not fields of this generic carrier.
Definition (Lean source)
Conditional carrier for represented execution.
Definition (Lean source)
Helpers.CertifiedComplex 35 declarations This file supplies the complex-algebra half missing from the promoted real certified interval API.
Certified complex rectangle arithmetic
This file supplies the complex-algebra half missing from the promoted real certified interval API. Every executable operation uses rational endpoints; exact complex values occur only in the semantic soundness contracts.
Coordinatewise complex rectangle subtraction.
Definition (Lean source)
Complex conjugation negates the imaginary interval.
Definition (Lean source)
Outward complex multiplication assembled from the promoted real API.
Definition (Lean source)
Rational lower bound for the square of every point of an interval.
Definition (Lean source)
Rational upper bound for the square of every point of an interval.
Definition (Lean source)
Squared modulus enclosure obtained by adding coordinate-square bounds.
Definition (Lean source)
One rational bisection state.
Definition (Lean source)
Initial nonnegative bracket used by the square-root routines.
Definition (Lean source)
Bisection from below, using only a rational square comparison.
Definition (Lean source)
Bisection from above, using only a rational square comparison.
Definition (Lean source)
Fixed-fuel lower square-root bisection.
Definition (Lean source)
Fixed-fuel upper square-root bisection.
Definition (Lean source)
Rational bisection enclosure for square roots on a nonnegative interval. The two endpoint bisections are deliberately exposed, so the executable algorithm is fixed independently of the promoted interval API.
Definition (Lean source)
Fixed-fuel rational enclosure of the modulus of a complex rectangle.
Definition (Lean source)
Guarded complex division via multiplication by the conjugate and an outward reciprocal of the squared modulus interval.
Definition (Lean source)
Public exact guarded-division primitive used by the bounded carrier.
Definition (Lean source)
Endpoint rule for the absolute value of a real interval.
Definition (Lean source)
Rectangle subtraction is sound: if a complex number lies in the first rectangle and a second complex number lies in the second rectangle, then their difference lies in the rectangle obtained by subtracting the two rectangles coordinate by coordinate.
Formal statement
Proof (Lean source)
Conjugation of rectangles is sound: if a complex number lies in a rectangle, then its complex conjugate lies in the rectangle whose imaginary side has been negated and whose real side is unchanged.
Formal statement
Proof (Lean source)
Rectangle multiplication is sound: if a complex number lies in the first rectangle and a second complex number lies in the second rectangle, then their product lies in the outward product rectangle, whose real side encloses the real part built from the cross-products of the coordinate intervals and whose imaginary side encloses the corresponding imaginary part.
Formal statement
Proof (Lean source)
The rational square bounds are sound: if a real number lies in a rational interval, then its square is at least the interval's rational lower square bound and at most its rational upper square bound.
Formal statement
Proof (Lean source)
The starting bracket of the square-root bisection is valid: for a nonnegative rational number, the initial bracket has a nonnegative lower endpoint, its lower endpoint does not exceed its upper endpoint, the square of its lower endpoint is at most the number, and the number is at most the square of its upper endpoint.
Formal statement
Proof (Lean source)
One bisection step preserves the bracketing invariant: if a bracket has a nonnegative lower endpoint, is correctly ordered, and its endpoint squares straddle the target number, then the bracket produced by one lower bisection step again has a nonnegative lower endpoint, is correctly ordered, and has endpoint squares straddling the same number.
Formal statement
Proof (Lean source)
The bracketing invariant survives any number of bisection steps: for a nonnegative rational number, after iterating the lower bisection step any fixed number of times starting from the initial bracket, the resulting bracket still has a nonnegative lower endpoint, is correctly ordered, and its endpoint squares straddle the number.
Formal statement
Proof (Lean source)
The lower bisection output never overshoots: for a nonnegative rational number, the rational value returned by the fixed-fuel lower bisection is at most the true real square root of that number.
Formal statement
Proof (Lean source)
The upper bisection output never undershoots: for a nonnegative rational number, the true real square root of that number is at most the rational value returned by the fixed-fuel upper bisection.
Formal statement
Proof (Lean source)
The rational lower square bound of any interval is nonnegative, since it is either zero, when the interval straddles the origin, or the smaller of two squares.
Formal statement
Proof (Lean source)
The modulus enclosure is sound: if a complex number lies in a rectangle, then its modulus lies in the rational interval produced by the fixed-fuel modulus routine for that rectangle, for any amount of bisection fuel.
Formal statement
Proof (Lean source)
The square-root enclosure is sound: for an interval whose lower endpoint is nonnegative, if a real number lies in that interval, then its square root lies in the rational interval produced by the fixed-fuel bisection enclosure, for any amount of bisection fuel.
Formal statement
Proof (Lean source)
One step of the lower bisection halves the width of the bracket: the distance between the new endpoints is exactly half the distance between the old ones, whichever branch the midpoint test takes.
Formal statement
Proof (Lean source)
One step of the upper bisection halves the width of the bracket: the distance between the new endpoints is exactly half the distance between the old ones, whichever branch the midpoint test takes.
Formal statement
Proof (Lean source)
Halving compounds geometrically: for a bracket update rule that always halves the width of the bracket it is applied to, iterating that rule a fixed number of times shrinks the width of any starting bracket by a factor of one half raised to the number of iterations.
Formal statement
Proof (Lean source)
The gap between the upper and lower square-root bisection outputs is at most the width of the initial bracket times one half raised to the amount of fuel, so the enclosure tightens geometrically in the number of bisection steps.
Formal statement
Proof (Lean source)
Guarded rectangle division is sound: if a complex number lies in the numerator rectangle, a second complex number lies in the denominator rectangle, and a strictly positive rational guard bounds the squared modulus of the denominator rectangle away from zero from below, then the quotient of the two complex numbers lies in the rectangle returned by the guarded division.
Formal statement
Proof (Lean source)
The absolute-value endpoint rule is sound: if a real number lies in a rational interval, then its absolute value lies in the interval produced by the absolute-value rule.
Formal statement
Proof (Lean source)
Helpers.CertifiedTranscendental 82 declarations This file defines the genuine rational, finite-fuel algorithms required by the paper.
Conditional certified transcendental substrate
This file defines the genuine rational, finite-fuel algorithms required by the paper. It deliberately does not manufacture a certified implementation. The record at the end is the contract that a future compiled implementation must discharge.
The convergence clauses consume shrinking input approximants. In particular,
there is no claim that the image of one fixed nondegenerate interval under
exp, sin, cos, or complex exp can have arbitrarily small width.
Rational alternating arctangent polynomial through index N.
Definition (Lean source)
Alternating-series remainder radius.
Definition (Lean source)
Raw rational enclosure of the arctangent at the rational point x: the alternating Taylor partial sum truncated at index N, widened symmetrically by the alternating-series remainder radius attached to that truncation.
Definition (Lean source)
Nested arctangent enclosure obtained by finite intersections.
Definition (Lean source)
Raw Machin enclosure 16 atan(1/5) - 4 atan(1/239).
Definition (Lean source)
Nested Machin enclosure.
Definition (Lean source)
Displayed finite Machin cutoff for a positive rational tolerance.
Definition (Lean source)
The Machin enclosures of π never widen as the cutoff index grows: the enclosure computed at cutoff N + 1 is contained in the one computed at cutoff N.
Formal statement
Proof (Lean source)
Interval evaluation of a rational-coefficient polynomial by primitive recursion.
Definition (Lean source)
The Taylor coefficient of the exponential function at index j, namely the reciprocal of j factorial.
Definition (Lean source)
The Taylor coefficient of the sine function at index j: zero at every even index, and at an odd index the alternating sign attached to that term divided by j factorial.
Definition (Lean source)
The Taylor coefficient of the cosine function at index j: zero at every odd index, and at an even index the alternating sign attached to that term divided by j factorial.
Definition (Lean source)
The displayed Taylor cutoff.
Definition (Lean source)
A rational bound for the exponential's Taylor remainder past degree N over an interval: the largest endpoint magnitude of the interval raised to the power N + 1, divided by N + 1 factorial, and scaled by three raised to the ceiling of that magnitude.
Definition (Lean source)
A rational bound for the sine or cosine Taylor remainder past degree N over an interval: the largest endpoint magnitude of the interval raised to the power N + 1, divided by N + 1 factorial.
Definition (Lean source)
Raw enclosure of the exponential over a rational interval at a requested precision: evaluate the exponential's Taylor polynomial in interval arithmetic up to the displayed cutoff degree for that interval and precision, then widen the result on both sides by the matching exponential remainder bound.
Definition (Lean source)
Raw enclosure of the sine over a rational interval at a requested precision: evaluate the sine's Taylor polynomial in interval arithmetic up to the displayed cutoff degree, then widen the result on both sides by the trigonometric remainder bound.
Definition (Lean source)
Raw enclosure of the cosine over a rational interval at a requested precision: evaluate the cosine's Taylor polynomial in interval arithmetic up to the displayed cutoff degree, then widen the result on both sides by the trigonometric remainder bound.
Definition (Lean source)
Fuel-indexed exponential enclosure over a rational interval: at fuel zero it is the raw Taylor enclosure at precision zero, and each further unit of fuel intersects the enclosure obtained so far with the raw enclosure computed at the next precision, so the family can only shrink.
Definition (Lean source)
Fuel-indexed sine enclosure over a rational interval: at fuel zero it is the raw Taylor enclosure at precision zero, and each further unit of fuel intersects the enclosure obtained so far with the raw enclosure computed at the next precision.
Definition (Lean source)
Fuel-indexed cosine enclosure over a rational interval: at fuel zero it is the raw Taylor enclosure at precision zero, and each further unit of fuel intersects the enclosure obtained so far with the raw enclosure computed at the next precision.
Definition (Lean source)
The finite Taylor cutoff spent on one real transcendental evaluation over a rational interval at a requested positive tolerance: the displayed cutoff formula applied to that interval, with the precision taken to be the denominator of the tolerance.
Definition (Lean source)
Certified rectangle extension of exp(x+iy)=exp(x)(cos y+i sin y).
Definition (Lean source)
The finite fuel spent on one complex exponential evaluation over a rational rectangle at a requested positive tolerance: the larger of the real transcendental cutoffs computed for the rectangle's real side and for its imaginary side.
Definition (Lean source)
The fuel-indexed exponential enclosures over a fixed rational interval never widen: the enclosure at fuel N + 1 is contained in the enclosure at fuel N.
Formal statement
Proof (Lean source)
The fuel-indexed sine enclosures over a fixed rational interval never widen: the enclosure at fuel N + 1 is contained in the enclosure at fuel N.
Formal statement
Proof (Lean source)
The fuel-indexed cosine enclosures over a fixed rational interval never widen: the enclosure at fuel N + 1 is contained in the enclosure at fuel N.
Formal statement
Proof (Lean source)
Pure represented-real input. Executable code sees no semantic exact real.
Definition (Lean source)
A family of rational approximants represents a given real number when every enclosure it produces, at every fuel level, contains that number.
Definition (Lean source)
Pure represented-complex input with a common effective modulus.
Definition (Lean source)
A family of rational rectangle approximants represents a given complex number when every rectangle it produces, at every fuel level, contains that number.
Definition (Lean source)
A value-opaque positive real name. Positivity is carried by a rational lower certificate; the represented real remains external to executable data.
Definition (Lean source)
External semantics of a value-opaque positive name.
Definition (Lean source)
Finite compositional fuel for one real transcendental call. The input tolerance is selected from the bounded input enclosure and requested output tolerance; it is not a hard-coded fraction of the latter.
Finite compositional fuel for one complex exponential call.
Coordinatewise finite intersection of complex rectangles.
Definition (Lean source)
Intersecting a complex rectangle with another one can only shrink it: the coordinatewise intersection of two rectangles is contained in the first rectangle.
Formal statement
Proof (Lean source)
Coordinatewise intersection of complex rectangles is sound: whenever a complex number lies in the first rectangle and lies in the second rectangle, it also lies in their intersection.
Formal statement
Proof (Lean source)
For one fixed represented input, evaluate the rational program at fuel m and intersect it with every previous output. Nesting is therefore indexed by fuel, not inferred from an ordering of requested tolerances.
Definition (Lean source)
Fuel-indexed complex-exponential outputs, recursively intersected with the previous rectangle.
Definition (Lean source)
The accumulated outputs of a real evaluation program on a fixed represented input never widen as fuel grows: the output enclosure at one more unit of fuel is contained in the output enclosure at the current fuel.
Formal statement
Proof (Lean source)
The accumulated complex-exponential output rectangles on a fixed represented input never widen as fuel grows: the rectangle at one more unit of fuel is contained in the rectangle at the current fuel.
Formal statement
Proof (Lean source)
Accumulating intersections preserves soundness for real programs: if every raw evaluation of the program, at every fuel level, encloses the target real number, then every accumulated output enclosure encloses it as well.
Formal statement
Proof (Lean source)
Accumulating intersections preserves soundness for the complex exponential: if every raw exponential rectangle, at every fuel level, encloses the target complex number, then every accumulated output rectangle encloses it as well.
Formal statement
Proof (Lean source)
The fuel at which a real transcendental call is finally read off: the larger of the schedule's input-refinement fuel and its Taylor fuel.
Definition (Lean source)
The fuel at which a complex exponential call is finally read off: the larger of the schedule's input-refinement fuel and its Taylor fuel.
Definition (Lean source)
The rational enclosure a real transcendental program returns under a given schedule: the accumulated output enclosure on the represented input, read at the schedule's output fuel.
Definition (Lean source)
The rational rectangle the complex exponential program returns under a given schedule: the accumulated output rectangle on the represented input, read at the schedule's output fuel.
Definition (Lean source)
Split a requested tolerance into a displayed finite number of positive pieces using rational arithmetic only.
Definition (Lean source)
Fixed compositional schedule for real exponential evaluation. Its input budget includes a rational Lipschitz envelope computed from the first supplied input interval; its Taylor budget is a separate quarter of the requested error.
Definition (Lean source)
Fixed compositional schedule for sine and cosine evaluation.
Definition (Lean source)
Fixed compositional schedule for complex exponential evaluation on a shrinking rectangle name.
Definition (Lean source)
Sound effective convergence of a rational finite-fuel real transcendental program on shrinking certified inputs.
Definition (Lean source)
Sound effective convergence of the rational finite-fuel complex exponential program on shrinking certified rectangles.
Definition (Lean source)
Circle fuel composes the radius-name modulus, Machin cutoff, and Taylor cutoff.
Definition (Lean source)
The fuel at which a circle-node or circle-tangent call is finally read off: the largest of the schedule's radius fuel, its Machin fuel for π, and its Taylor fuel.
Definition (Lean source)
Certified rectangle for the q-th of N equally spaced points on the circle of radius given by a positive real name: multiply the radius enclosure, read at the schedule's radius fuel, by the complex exponential enclosure of the purely imaginary angle obtained from twice q over N times the Machin enclosure of π.
Definition (Lean source)
Certified rectangle for the tangent (parametric velocity) of the same circle at its q-th of N equally spaced points: form the purely imaginary quantity two times π times the radius, using the Machin enclosure of π and the radius enclosure at the schedule's radius fuel, and multiply it by the complex exponential enclosure of the same angle.
Definition (Lean source)
Raw circle node at one common finite fuel.
Definition (Lean source)
Raw circle tangent at one common finite fuel.
Definition (Lean source)
Circle nodes for fixed radius data and mesh indices, recursively intersected by fuel.
Definition (Lean source)
Circle tangents for fixed radius data and mesh indices, recursively intersected by fuel.
Definition (Lean source)
The accumulated circle-node rectangles for fixed radius data and mesh indices never widen as fuel grows: the rectangle at one more unit of fuel is contained in the rectangle at the current fuel.
Formal statement
Proof (Lean source)
The accumulated circle-tangent rectangles for fixed radius data and mesh indices never widen as fuel grows: the rectangle at one more unit of fuel is contained in the rectangle at the current fuel.
Formal statement
Proof (Lean source)
Accumulating intersections preserves soundness for circle nodes: if every raw node rectangle, at every fuel level, contains the target complex value, then every accumulated node rectangle contains it as well.
Formal statement
Proof (Lean source)
Accumulating intersections preserves soundness for circle tangents: if every raw tangent rectangle, at every fuel level, contains the target complex value, then every accumulated tangent rectangle contains it as well.
Formal statement
Proof (Lean source)
The circle-node rectangle returned under a given schedule: the accumulated node sequence for that radius name and mesh index, read at the schedule's output fuel.
Definition (Lean source)
The circle-tangent rectangle returned under a given schedule: the accumulated tangent sequence for that radius name and mesh index, read at the schedule's output fuel.
Definition (Lean source)
Fixed finite schedule for a circle node. Every component is computed from the requested tolerance, the supplied radius modulus, and the displayed Machin/Taylor programs.
Definition (Lean source)
Fixed finite schedule for the corresponding circle tangent.
Definition (Lean source)
Complete soundness and effective-modulus contract for positive-radius circle nodes and tangents.
Definition (Lean source)
The explicit number of mesh subdivisions used for a Lipschitz constant L and a requested positive tolerance: the ceiling of the constant divided by the tolerance, plus one.
Definition (Lean source)
Legacy contract for the retired callable-table finite-extrema interface. The canonical bounded-domain adapter exposes its paper-specific contract in SelectorSoundness.
Definition (Lean source)
The promoted primitive-recursive trapezoidal enclosure, with its exact Lipschitz soundness and the irreducible uniform node-width contribution.
Definition (Lean source)
Uniform finite-fuel names for the complex values at every node of every finite mesh. The semantic function is supplied only to the external RepresentsNodeFunction relation and is not executable data.
Definition (Lean source)
A family of node approximants represents a complex-valued function on the unit parameter interval when, for every mesh size, every node index not exceeding that mesh size, and every fuel level, the rectangle it produces contains the value of the function at the corresponding mesh point.
Definition (Lean source)
The displayed finite resources for node evaluation and mesh aggregation.
Definition (Lean source)
The actual callable node evaluator: select the requested rational rectangle from a value-opaque node name using only mesh indices and fuel.
Definition (Lean source)
A closed-form finite bisection budget. It depends only on rational endpoint data and the requested positive tolerance; no least witness or unbounded search is used.
Definition (Lean source)
Fixed node/mesh schedule from the displayed operation count and rational error budget.
Definition (Lean source)
The exact mesh, node-call, Taylor, square-root, and endpoint-operation fuel obligations from the bounded-build specification.
Definition (Lean source)
Sound, nested node evaluation at the displayed finite fuel.
Definition (Lean source)
Helpers.ClassRelations 1 declarations Relations among the non-Gaussian and published ACE classes
Relations among the non-Gaussian and published ACE classes
The published ACE comparator class sits inside the broad non-Gaussian class, the comparison subclass sits inside the comparator class, and when the two code-accuracy exponents coincide the comparator class and the comparison subclass are one and the same set of laws.
Formal statement
Proof (Lean source)
Helpers.ComplexAnalysisLocal 9 declarations These are the two bounded local complex-analysis builds used by the contour bank.
Local finite-product and disk estimates
These are the two bounded local complex-analysis builds used by the contour bank. They are not external interfaces.
One radius-R Blaschke factor.
Definition (Lean source)
A finite radius-R Blaschke product.
Definition (Lean source)
Inside the defining disk, a Blaschke factor vanishes exactly at its listed zero.
Formal statement
Proof (Lean source)
On a disk of positive radius whose prescribed zero lies strictly inside it, at any point of the closed disk the modulus of the Blaschke factor is at least the distance from the point to the zero, divided by the radius plus the modulus of the point.
Formal statement
Proof (Lean source)
For a disk of positive radius and a finite list of prescribed zeros all lying strictly inside it, the corresponding finite Blaschke product is analytic on a neighbourhood of every point of the open disk: its only possible singularities sit outside the closed disk.
Formal statement
Proof (Lean source)
For a disk of positive radius whose prescribed zeros all lie strictly inside it, at any point on the boundary circle the finite Blaschke product has modulus exactly one.
Formal statement
Proof (Lean source)
For a disk of positive radius whose prescribed zeros all lie strictly inside it, the finite Blaschke product has modulus at most one at the centre of the disk, since each factor there has modulus at most one.
Formal statement
Proof (Lean source)
Harnack bound for the real part of a holomorphic function on a disk.
Formal statement
Proof (Lean source)
Log-modulus lower bound for a bounded zero-free holomorphic function.
Formal statement
Proof (Lean source)
Helpers.ContourBank 16 declarations The bank reads one experiment-wide record for the primitive constants.
Fixed-fuel translated-dyadic contour bank
The bank reads one experiment-wide record for the primitive constants. Its integers are the displayed closed forms; there is no unbounded or proof-selected search, exact-real inspection, or law query.
A supplied positive certified-real record. Executable consumers inspect only name.approx, name.modulus, and the rational lower witness.
Definition (Lean source)
The one fixed primitive record shared by the bank and estimator.
Definition (Lean source)
Reuse the identical primitive names for another parameter record carrying the same primitive constants. Only the propositional value contracts are transported; no new name is selected or reconstructed.
Definition (Lean source)
Error-one rational refinement used exactly twice by the bank.
Definition (Lean source)
Natural ceiling of a rational upper endpoint, clamped below by one.
Definition (Lean source)
The clamped rational ceiling dominates its input.
Formal statement
Proof (Lean source)
The clamped rational ceiling is at least one.
Formal statement
Proof (Lean source)
All data computed by the displayed fixed-fuel bank program.
Definition (Lean source)
Cardinality of the explicit bank.
Definition (Lean source)
The circle belonging to one bank radius.
Definition (Lean source)
A dyadic grid with mesh 2⁻(k+1) and indices through 2^k stays strictly below the unit-length endpoint after translation by one quarter.
Formal statement
Proof (Lean source)
More grid points than listed complex numbers leave one translated grid radius uniformly separated from every listed modulus.
Formal statement
Proof (Lean source)
The closed-form dyadic exponent dominates a product of at most K factors, each bounded below by a dyadic mesh divided by a positive integer.
Formal statement
Proof (Lean source)
Two binary digits per natural exponent are enough to lie below the corresponding negative exponential.
Formal statement
Proof (Lean source)
The closed-form law-blind translated-dyadic bank.
Definition (Lean source)
The fixed-fuel bank contains a uniformly conditioned positive-count circle for every treatment-noise transform in the broad class.
Formal statement
Proof (Lean source)
Helpers.Cumulant 2 declarations Cumulants and transform-zero localization
Cumulants and transform-zero localization
The treatment-noise transform is entire, normalized at the origin, and obeys the quadratic exponential envelope supplied by the Luxemburg bound.
Formal statement
Proof (Lean source)
A separated cumulant forces a transform zero in the explicit disk.
Formal statement
Proof (Lean source)
Helpers.EmpiricalTransform 14 declarations Uniform L2 control of empirical transforms
Uniform L2 control of empirical transforms
The uniform error of a random transform against a fixed target on a disk: the supremum, over all complex points of modulus at most the given radius, of the distance between the value of the random transform at that point and the value of the target there.
Definition (Lean source)
The transform error is exactly the disk supremum of the centered random analytic function.
Formal statement
Proof (Lean source)
The two deterministic folds, indexed by Fin 2.
A Luxemburg-square envelope controls every even moment with the factorial constant used in the empirical-transform coefficient series.
Formal statement
Proof (Lean source)
The treatment-noise Luxemburg assumption gives the factorial even-moment majorant used for residual-transform coefficients.
Formal statement
Proof (Lean source)
The conditional Luxemburg bound for the outcome innovation implies its unconditional square-exponential bound.
Formal statement
Proof (Lean source)
A uniform square-integral envelope for the absolute exponential of the learned residual.
Formal statement
Proof (Lean source)
The primitive bounds imply a uniform fourth moment for the observed outcome.
Formal statement
Proof (Lean source)
Multiplying the outcome by an absolute learned-residual exponential still has a uniform L² envelope.
Formal statement
Proof (Lean source)
A real-weighted exponential transform is its factorial-weighted moment series whenever the doubled absolute exponential is integrable.
Formal statement
Proof (Lean source)
A doubled absolute-exponential L² envelope gives geometric L² bounds for factorial-weighted moment coefficients.
Formal statement
Proof (Lean source)
A split-fold residual-transform error is the average of its centered single-observation transform values.
Formal statement
Proof (Lean source)
A split-fold outcome-transform error is the average of its centered single-observation weighted transform values.
Formal statement
Proof (Lean source)
A summable sequence of real centered coefficients with coefficientwise L² bounds controls the uniform squared norm of its analytic series.
Formal statement
Proof (Lean source)
Helpers.EmpiricalTransformSeries 6 declarations This module converts real exponential-envelope bounds into uniform disk L² bounds for centered empirical analytic transforms and proves the exact coefficient-series identity used to connect those bounds to the paper's em
Factorial-series assembly for empirical transforms
This module converts real exponential-envelope bounds into uniform disk L² bounds for centered empirical analytic transforms and proves the exact coefficient-series identity used to connect those bounds to the paper's empirical transforms.
Take a nonempty block of sample indices, a measurable weight and a measurable exponent variable, and fix a disk of positive radius. If the envelope given by the absolute weight times the exponential of twice the radius times the absolute exponent variable has second moment no larger than the square of a nonnegative constant, then, for the power series whose k-th coefficient is the block average of the centered factorial statistic — weight times exponent variable to the power k over k factorial, minus its population mean — the expected squared supremum of that series over the disk is at most four times the squared constant divided by the block size.
Formal statement
Proof (Lean source)
Take a nonempty block of sample indices, a measurable weight and a measurable exponent variable, a disk of positive radius, and assume the envelope given by the absolute weight times the exponential of twice the radius times the absolute exponent variable has second moment no larger than the square of a nonnegative constant. Then at every argument of modulus at most the radius the block average of the weight times the exponential of the argument times the exponent variable, minus the population weighted transform, equals the power series whose k-th coefficient is the block average of the centered factorial statistic — weight times exponent variable to the power k over k factorial, minus its population mean.
Formal statement
Proof (Lean source)
The explicit constant in the uniform disk bound for the empirical transforms: four times the sum of two envelope factors. The first is twice the exponential of eight times the search radius times the treatment-regression bound, plus four times the squared radius times the squared treatment sub-Gaussian scale. The second adds to a fourth-moment term — sixty-four times the sum of the fourth power of the outcome-regression bound, four times the fourth power of the treatment-effect bound times the fourth power of the treatment scale, and four times the fourth power of the outcome sub-Gaussian scale — twice the exponential of sixteen times the radius times the treatment-regression bound plus sixteen times the squared radius times the squared treatment scale.
Definition (Lean source)
The explicit constant in the uniform disk bound for the empirical transforms is strictly positive for any values of the model constants and the search radius.
Formal statement
Proof (Lean source)
Explicit-constant form of the uniform split-fold transform bound.
Formal statement
Proof (Lean source)
Both split-fold analytic transforms have uniform mean-square error of order inverse fold size.
Formal statement
Proof (Lean source)
Helpers.FixedCodeConverse 2 declarations This module packages the affine-Gaussian two-point construction while retaining both supplied nuisance-code functions.
Fixed-code non-Gaussian minimax converse
This module packages the affine-Gaussian two-point construction while retaining both supplied nuisance-code functions.
A positive inverse-sample-size minimax lower bound on every nonempty broad non-Gaussian class with both supplied codes fixed.
Formal statement
Proof (Lean source)
A positive inverse-sample-size lower bound for every nonempty fixed-code published ACE class, uniform over the covariate space.
Formal statement
Proof (Lean source)
Helpers.GaussianRademacherBenchmark 6 declarations This module assembles the explicit transform identities and the generic clipped-ratio risk bound for the local-to-Gaussian path.
Gaussian--Rademacher sine-score benchmark
This module assembles the explicit transform identities and the generic clipped-ratio risk bound for the local-to-Gaussian path.
The Gaussian--Rademacher path has a uniform second-moment envelope.
Formal statement
Proof (Lean source)
At a characteristic zero, the sine-score regression remainder is centered.
Formal statement
Proof (Lean source)
Suppose the treatment noise has second moment at most four, the treatment coefficient lies within its range bound, the treatment regression is uniformly bounded, the outcome regression is uniformly bounded, and the outcome noise is sub-Gaussian with the stated scale. Then the two sine scores — the learned treatment residual times the sine of the frequency times that residual, and the residualized outcome times the same sine — are measurable and square integrable, with squared second moments at most eight plus sixteen times the squared treatment-regression bound, and at most four times the squared combined outcome bound plus four times the squared outcome-noise scale, respectively.
Formal statement
Proof (Lean source)
The sine-score estimator at a given frequency and denominator threshold is exactly the generic clipped ratio rule applied to two sample averages: the average of the learned treatment residual times the sine of the frequency times that residual as denominator, and the average of the residualized outcome times the same sine as numerator correction, which is what lets the generic risk bound for clipped ratios be applied to it.
Formal statement
Proof (Lean source)
The complete path conclusion shared by the benchmark lemma and the local-to-Gaussian partial theorem.
Definition (Lean source)
Path-specific MGF, cumulant, annihilation, denominator, and risk benchmark.
Formal statement
Proof (Lean source)
Helpers.HardSubmodel 4 declarations Non-Gaussian hard submodel
Non-Gaussian hard submodel
Symmetric clipping used only to reduce arbitrary estimators to bounded ones in the two-point lower bound.
Definition (Lean source)
For a nonnegative clipping level and a target whose absolute value does not exceed it, clipping any real number symmetrically to that level never increases its squared distance to the target. Restricting attention to estimators bounded by the clipping level therefore costs nothing in the two-point lower bound.
Formal statement
Proof (Lean source)
A pair of class members with finite KL budget gives an ENNReal lower bound for the local class-indexed minimax risk.
Formal statement
Proof (Lean source)
Both the broad spectral class and the full published ACE class contain ACE-preserving fixed-innovation paths with quadratic local KL divergence; the second path yields the full-class c / n minimax converse.
Formal statement
Proof (Lean source)
Helpers.JensenBlaschke 16 declarations This file connects the open-disk multiplicity count used by the contour library to Mathlib's logarithmic divisor count.
Quantitative Jensen bridges
This file connects the open-disk multiplicity count used by the contour library to Mathlib's logarithmic divisor count. The resulting Jensen bound does not require the outer circle to be zero-free.
Keep precisely the strict-interior part of a closed-disk divisor.
Definition (Lean source)
The strict-interior part of a divisor on a closed disk agrees with the divisor at every point lying strictly inside the disk and is zero everywhere else, so it records exactly the multiplicities that the argument principle counts and discards those sitting on the boundary circle.
Formal statement
Proof (Lean source)
The analytic nonvanishing correction which converts the radius-R Blaschke product back to the corresponding monic zero polynomial.
Definition (Lean source)
A Blaschke product times its correction is the monic polynomial with the listed zeros.
Formal statement
Proof (Lean source)
The Blaschke correction is analytic and nonzero throughout the closed disk when all listed zeros lie strictly inside it.
Formal statement
Proof (Lean source)
On a closed disk, Mathlib's divisor extraction constructs the analytic zero-free quotient. The equality is in Mathlib's canonical codiscrete form; this is the raw cancellation bridge from which a concrete finite Blaschke factorization can be obtained after identifying the finite divisor.
Formal statement
Proof (Lean source)
A multiplicity-expanded enumeration of the disk divisor yields an actual pointwise finite Blaschke factorization. The zero-free remainder is constructed from Mathlib's extracted quotient and the explicit nonvanishing Blaschke correction; it is not an assumption.
Formal statement
Proof (Lean source)
Every finite nonnegative divisor admits a multiplicity-expanded finite enumeration whose monic product is its factorized rational function.
Formal statement
Proof (Lean source)
The open-disk zero count can be evaluated on any finite set containing all nonzero analytic orders in the disk.
Formal statement
Proof (Lean source)
Factorized rational functions multiply when two finite exponent functions are nonnegative. Nonnegativity is essential at common zeros: it lets us reduce integer powers to ordinary natural powers before using pow_add.
Formal statement
Proof (Lean source)
A normalized analytic function admits a complete finite pointwise Blaschke factorization on the disk even when it has zeros on the boundary. Only strict-interior zeros enter the Blaschke product; boundary factors are absorbed into a remainder which is zero-free on the open disk.
Formal statement
Proof (Lean source)
Jensen's formula bounds the logarithmic divisor count by any uniform log-modulus bound on the outer circle, when the function is normalized at the origin. Zeros on that circle are allowed.
Formal statement
Proof (Lean source)
The open-disk multiplicity count, after casting to the integers, is the sum of the analytic orders over any finite set containing every zero in the disk.
Formal statement
Proof (Lean source)
Quantitative Jensen zero-counting inequality in the project's zeroMultiplicityCount representation. It has no boundary-zero hypothesis.
Formal statement
Proof (Lean source)
A normalized entire function whose modulus is at most exp A on the outer circle has at most Jensen growth worth of inner zeros.
Formal statement
Proof (Lean source)
A supplied finite Blaschke factorization turns an outer boundary bound into a quantitative interior lower bound. This is the reusable consumer of a complete multiplicity list: the remaining local burden is only to construct the analytic zero-free quotient and the factorization equality.
Formal statement
Proof (Lean source)
Helpers.JmsComparator 12 declarations Jin--Mackey--Syrgkanis ACE comparator
Jin--Mackey--Syrgkanis ACE comparator
The published estimator is indexed by its order, sample size, and the one fixed supplied treatment/outcome code pair for that experiment.
Definition (Lean source)
Citation interface for the single published order-r ACE procedure. The handle is supplied once at the cited boundary and then shared unchanged by both cited statements and all of their consumers.
Definition (Lean source)
The first exponential-tilt scale of the published eligibility condition: twice the logarithm of six times the sum of the treatment-regression bound and the treatment sub-Gaussian scale, divided by the treatment-code accuracy budget at sample size n.
Definition (Lean source)
The first budget quantity of the published eligibility condition: the logarithm of the effective sample size — the overlap exponent times n — divided by nine.
Definition (Lean source)
The second exponential-tilt scale of the published eligibility condition: four times the sum of the treatment-regression bound and the treatment sub-Gaussian scale.
Definition (Lean source)
The second budget quantity of the published eligibility condition: two hundred times the smaller of one and the treatment-effect bound, times the cumulant separation, divided by the largest of the treatment-code budget, the outcome-code budget, and the parametric-rate noise level — the effective sample size to the power −1/2 times the sum of the outcome sub-Gaussian scale and the treatment-effect bound times the treatment sub-Gaussian scale.
Definition (Lean source)
Condition (21) evaluated at an explicitly supplied separation. This is the generalization used only by the shrinking-separation benchmark.
Definition (Lean source)
Exact paper condition (21), evaluated at the model separation p.delta, with precisely the nonzero denominators and positive logarithm arguments needed for the displayed expression to be defined.
Definition (Lean source)
The published finite-order ACE error bound of Jin, Mackey and Syrgkanis: an overlap-dependent constant times the factorial of the expansion order, times sixteen to that order, divided by the cumulant separation, multiplied by the sum of three terms — the treatment-code budget raised to the expansion order times the outcome-code budget, the treatment-effect bound times the treatment-code budget raised to one plus the expansion order, and a nuisance-scale factor times the effective sample size to the power −1/2.
Definition (Lean source)
The published ACE class with its cumulant separation evaluated at an explicit value rather than at p.delta.
Definition (Lean source)
Jikai Jin, Lester Mackey, and Vasilis Syrgkanis (2025), It is hard to be normal, Theorem 5.4, equations (21)--(22), arXiv:2507.02275v3: fixed-separation generalized-quantile upper bound for the estimator carried by the sealed published-procedure handle.
Definition (Lean source)
Jikai Jin, Lester Mackey, and Vasilis Syrgkanis (2025), It is hard to be normal, Theorem 5.4, equations (21)--(22), arXiv:2507.02275v3: the same bound for the estimator carried by the same sealed published-procedure handle, universally specialized to a positive separation constant.
Definition (Lean source)
Helpers.KnownZeroConditional 3 declarations Conditional annihilation for known-zero instruments
Conditional annihilation for known-zero instruments
All transform derivatives below a positive analytic zero order vanish.
Formal statement
Proof (Lean source)
A transform zero of order ell annihilates its polynomial-exponential instrument after every deterministic real shift.
Formal statement
Proof (Lean source)
For a model in the broad non-Gaussian class and a complex point where the treatment-noise moment generating function vanishes to a known order that is at least one, the transform-zero instrument evaluated at the observable learned residual has conditional mean zero given the covariates, almost surely.
Formal statement
Proof (Lean source)
Helpers.KnownZeroOrthogonality 4 declarations Moment and outcome assembly for known-zero instruments
Moment and outcome assembly for known-zero instruments
For a law in the paper's non-Gaussian class, at a point where the moment generating function of the treatment noise vanishes with multiplicity exactly the given order, that order being at least one, the expected product of the observable learned residual with the zero instrument evaluated at that residual equals the derivative of that order of the treatment-noise transform at the point, times the transform of the treatment-code error at the same point.
Formal statement
Proof (Lean source)
For a law in the paper's non-Gaussian class, at a point where the moment generating function of the treatment noise vanishes with multiplicity exactly the given order, that order being at least one, the product of the outcome noise with the zero instrument evaluated at the observable learned residual is integrable and has expectation zero.
Formal statement
Proof (Lean source)
For a law in the paper's non-Gaussian class, at a point where the moment generating function of the treatment noise vanishes with multiplicity exactly the given order, that order being at least one, the product of the outcome-side contamination, a function of the covariate alone, with the zero instrument evaluated at the observable learned residual is integrable and has expectation zero.
Formal statement
Proof (Lean source)
For a law in the paper's non-Gaussian class, at a point where the moment generating function of the treatment noise vanishes with multiplicity exactly the given order, that order being at least one, the expected product of the outcome with the zero instrument evaluated at the observable learned residual equals the treatment-effect parameter times the expected product of that residual with the same instrument.
Formal statement
Proof (Lean source)
Helpers.LuxemburgMGF 2 declarations This file supplies the real-variable estimate used by transform-zero localization.
A Luxemburg square-exponential bound implies a global MGF bound
This file supplies the real-variable estimate used by transform-zero localization. A centered random variable whose square-exponential moment is at most two has all real exponential moments, with an explicit quadratic MGF envelope.
A square-exponential envelope gives integrability of every real exponential tilt.
Formal statement
Proof (Lean source)
A centered Luxemburg square-exponential bound implies the global MGF estimate E exp(tX) ≤ exp(4 ψ²t²).
Formal statement
Proof (Lean source)
Helpers.PopulationNumeratorBound 2 declarations This file isolates the population G bound used by the adaptive contour risk proof.
Uniform population numerator envelope
This file isolates the population G bound used by the adaptive contour risk proof.
The explicit uniform envelope for the population outcome-residual transform.
Definition (Lean source)
On the search disk, the population numerator is bounded only in terms of the displayed class constants.
Formal statement
Proof (Lean source)
Helpers.ProjectedOutputCertification 1 declarations Certification of the clipped represented output
Certification of the clipped represented output
The interval name obtained from the absolute-value clipping formula is nested, has the inherited effective width modulus, and contains its exact real value.
Formal statement
Proof (Lean source)
Helpers.SelectorSoundness 33 declarations Soundness of the one bounded-domain option-A selector
Soundness of the one bounded-domain option-A selector
Every mesh endpoint consumed by trapezoidal quadrature is evaluated by the bounded adapter.
Definition (Lean source)
Every quadrature schedule enumerates exactly the mesh endpoints it needs: an index appears in the enumerated list of nodes precisely when it does not exceed the schedule's mesh count, so the bounded adapter evaluates the integrand at all of them and at nothing else.
Formal statement
Proof (Lean source)
Exact precision and fuel facts required by every schedule actually used by the bounded program. amplification is the interval-map envelope; it is separate from schedule.magnitude, which remains the contour Lipschitz constant used only by the mesh bound.
Definition (Lean source)
A represented spectral input is canonical when it is the record actually produced by the estimator's data-encoding step: there exist certified bank inputs, a certified range input, a treatment-regression code sequence, and a sample of observations on the covariate space such that the input is the canonical encoding built from them.
Definition (Lean source)
Full-box validity of the empirical denominator map on canonical floor-dyadic represented inputs. The exponential and derivative envelopes use spectralFullBoxRadius B, not the smaller selected-circle radius.
Formal statement
Proof (Lean source)
Full-box validity of the empirical numerator map on canonical floor-dyadic represented inputs.
Formal statement
Proof (Lean source)
Explicit post-quadrature width contract. It exposes the guarded-division amplification and requires the actual normalized rectangle, not merely its fuel, to meet the branch target.
Definition (Lean source)
All paper-specific schedule facts are local consequences of the canonical floor-dyadic input and the explicit schedule, never hypotheses or fields of the generic build carrier.
Definition (Lean source)
The paper schedule is certified only for the floor-dyadic observation records used by the ordinary option-A statistic. In particular, this does not assert a raw-fuel width contract for arbitrary supplied real names.
Formal statement
Proof (Lean source)
The pilot's finite-extremum error is the sum of a node half and a mesh half, each bounded by aStar/128.
Definition (Lean source)
Semantic certificate for one pilot boundary-infimum call.
Definition (Lean source)
The exact complex number a bounded circle evaluator is meant to approximate: integrate the ratio of the evaluator's numerator map to its denominator map once around the circle of the evaluator's radius centred at the origin, then divide by two pi times the imaginary unit times the evaluator's normalization count, where a normalization count of zero is treated as one.
Definition (Lean source)
The contour integral of a complex function around a circle as defined by the quadrature-mesh library agrees with the standard circle integral, for any centre and any radius.
Formal statement
Proof (Lean source)
The winding rectangle encloses the normalized, tangent-corrected contour integral and is narrow enough for unique integer decoding.
Definition (Lean source)
The evaluation rectangle is normalized after quadrature and has the paper's effective 1/max(n,1) midpoint tolerance.
Definition (Lean source)
Selector-side use of the decoder contract: a normalized winding rectangle with the certified strict coordinate widths decodes the exact nonnegative integer it contains.
Formal statement
Proof (Lean source)
The full package of node-level certificates the bounded selector relies on, stated for a given parameter set: for every measurable covariate space and every choice of certified bank inputs, certified range input, treatment-regression code sequence, and sample, the canonically encoded input satisfies, at each candidate contour radius, the two pilot boundary-modulus certificates, the winding-number enclosure certificate, and the evaluation enclosure certificate for every candidate integer; and the projected-output name certifies, at every rational argument, the clipping of that argument to the range constant Ctheta.
Definition (Lean source)
Every parameter set satisfies the full package of node-level certificates: on canonically encoded data the pilot boundary-modulus enclosures, the winding enclosures, the evaluation enclosures, and the certified clipping of the output to the range constant Ctheta all hold, with no further assumptions on the sample or on the treatment-regression code.
Formal statement
Proof (Lean source)
The generic complex operations used by the bounded adapter have their actual executable semantics. This is deliberately a predicate on a supplied build, rather than extra fields on the weak callable carrier.
Definition (Lean source)
The supplied compiled entry points are exactly the pilot, winding, and evaluation programs of the single bounded option-A adapter.
Definition (Lean source)
Complete antecedent for represented delivery on one fixed experiment. It combines the genuine generic complex build, the compiled callable adapter, the locally derived schedule/map/guard/containment/width/normalization facts, and endpoint completeness. Output certification is a conclusion derived from the projected-output certificate, not a premise of this predicate. None of these paper-specific facts is a field of CompiledBoundedSpectralAdapter.
Definition (Lean source)
If a compiled bounded adapter has canonical generic complex arithmetic, canonically compiled entry points, and node certificates valid on every sample, then running that compiled adapter on canonically encoded data reproduces the estimator's represented-execution contract: it returns exactly the same record as the ordinary finite-rational program, the same execution trace, and an output name certifying the clipped point estimate.
Formal statement
Proof (Lean source)
The estimator's reported point estimate is exactly the raw output of the ordinary finite-rational program clipped to the interval between minus the range constant Ctheta and plus Ctheta, for any parameter set, certified records, treatment-regression code, and sample.
Formal statement
Proof (Lean source)
Finite branch endpoints, floor-dyadic maps, and the least-index search are Borel measurable.
Formal statement
Proof (Lean source)
If the treatment-regression code at the current sample size is a measurable function of the covariate, then the estimator is a measurable function of the sample.
Formal statement
Proof (Lean source)
The estimator always takes values between minus the range constant Ctheta and plus Ctheta, whatever the sample, because its last step clips the raw value to that range and the range constant is positive.
Formal statement
Proof (Lean source)
If a compiled bounded adapter satisfies the represented-execution contract, then on every sample the record it produces on canonically encoded data equals the record produced by the ordinary finite-rational program, its execution trace equals the estimator's full trace, and its output name certifies the estimator's reported value.
Formal statement
Proof (Lean source)
The source good event supplies both population controls and the two positive denominator margins. The empirical margin is derived from d ≤ mu-nu; it is not a separate assumption.
Definition (Lean source)
Exact source perturbation scale.
Definition (Lean source)
A population lower bound on a denominator transfers to its empirical counterpart: if the population denominator has modulus at least mu, the empirical denominator differs from it by at most d in modulus, and the estimation error d does not exceed the gap between mu and nu, then the empirical denominator has modulus at least nu.
Formal statement
Proof (Lean source)
A perturbation bound for a ratio of complex numbers. Suppose the population denominator has modulus at least mu and the empirical denominator has modulus at least nu, with both margins strictly positive; the population numerator has modulus at most C, with C nonnegative; the denominators differ by at most d, with d nonnegative; and the numerators differ by at most e, with e nonnegative. Then the two ratios differ by at most e divided by nu plus C times d divided by the product of mu and nu.
Formal statement
Proof (Lean source)
The ratio perturbation bound, integrated around a circle. Consider a circle of nonnegative radius rho centred at the origin, along with nonnegative error scales d and e and a nonnegative numerator bound C and strictly positive denominator margins mu and nu satisfying the requirement that the denominator error does not exceed the gap between the two margins. Suppose the empirical ratio is integrable around the circle, the population ratio is integrable around the circle, and at every point of the circle the population denominator has modulus at least mu, the population numerator has modulus at most C, the denominators differ by at most d, and the numerators differ by at most e. Then the two contour integrals differ by at most the circumference of the circle times the sum of e divided by nu and C times d divided by the product of mu and nu.
Formal statement
Proof (Lean source)
The selected-circle ratio bound plus the separate finite rational midpoint error.
Formal statement
Proof (Lean source)
Helpers.SineRisk 4 declarations Generic clipped sine-ratio risk reductions
Generic clipped sine-ratio risk reductions
The clipped ratio estimator built from two per-observation scores: average the denominator score and the remainder score over the sample; if the average denominator reaches the threshold, return the ratio of the target value times the average denominator plus the average remainder to the average denominator, truncated to the symmetric interval given by the clipping bound; otherwise return zero.
Definition (Lean source)
With at least one observation, a target value inside the clipping bound, a strictly positive denominator level and a population denominator mean of at least half that level, the squared error of the clipped ratio estimator run at a threshold of one quarter of the level is at most sixteen over the squared level, times the sum of the squared sample average of the remainder scores and the squared clipping bound times the squared sample average of the centered denominator scores.
Formal statement
Proof (Lean source)
Whenever the target value lies inside the clipping bound, the squared error of the clipped ratio estimator never exceeds four times the squared clipping bound, on every sample and whatever the denominator level. This is the crude fallback used where the sharp bound is unavailable.
Formal statement
Proof (Lean source)
For an independent sample of size at least one from a probability law, with a target value inside the clipping bound, a strictly positive denominator level and a population denominator mean of at least half that level, and with measurable and square-integrable denominator and remainder scores whose population means are that denominator mean and zero respectively, the expected squared error of the clipped ratio estimator run at a threshold of one quarter of the level is at most sixteen over the squared level, divided by the sample size, times the sum of the second moment of the remainder score and the squared clipping bound times the second moment of the denominator score.
Formal statement
Proof (Lean source)
Helpers.SineScore 22 declarations Bounded sine-score estimators
Bounded sine-score estimators
The sample average of a real-valued function of one observation: the sum of its values over the units in the sample, divided by the sample size.
Definition (Lean source)
Shared clipped ratio engine for a sine score.
Definition (Lean source)
Fixed-mixture sine estimator at frequency pi/2.
Definition (Lean source)
Symmetric Rademacher probability law.
The symmetric Rademacher law — equal mass one half on minus one and on plus one — is a probability measure, its total mass being one.
Definition (Lean source)
The symmetric Rademacher law has complex MGF cosh.
Formal statement
Proof (Lean source)
The standard Gaussian, written with the explicit variance literal ⟨1, zero_le_one⟩, is a probability measure.
Definition (Lean source)
Gaussian--Rademacher treatment-noise path.
Definition (Lean source)
The Gaussian--Rademacher path has the advertised product MGF.
Formal statement
Proof (Lean source)
Every real exponential moment exists along the explicit path.
Formal statement
Proof (Lean source)
The third derivative at zero of a tanh(a z) is -2a^4.
Formal statement
Proof (Lean source)
The fourth logarithmic derivative of the Gaussian--Rademacher MGF is the Rademacher fourth cumulant -2a^4.
Formal statement
Proof (Lean source)
Transport the explicit path transform across the model's noise law.
Formal statement
Proof (Lean source)
The model cumulants inherit the explicit fourth logarithmic derivative.
Formal statement
Proof (Lean source)
Suppose the cumulant order recorded in the parameter block is four and the treatment noise of the model is distributed as the Gaussian--Rademacher path with mixing weight strictly positive and at most one, namely an independent standard normal scaled by the square root of one minus the squared weight plus a symmetric sign variable scaled by the weight. Then the model's treatment-noise cumulant of that order is minus twice the fourth power of the mixing weight, so it is strictly negative and quantifies how far the noise sits from Gaussian.
Formal statement
Proof (Lean source)
The explicit transform has its first positive imaginary-axis zero at pi/(2a).
Formal statement
Proof (Lean source)
The derivative at the first zero is the purely imaginary signal I*A.
Formal statement
Proof (Lean source)
A zero of the characteristic function annihilates every deterministic translate of the sine score.
Formal statement
Proof (Lean source)
Exact-law transport supplies all exponential moments needed to differentiate the characteristic function.
Formal statement
Proof (Lean source)
The first weighted characteristic moment at the first zero is I*A.
Formal statement
Proof (Lean source)
Independence transports the derivative signal through the bounded treatment-code error.
Formal statement
Proof (Lean source)
The direct L¹ radius keeps the population denominator above half of its uncontaminated signal.
Formal statement
Proof (Lean source)
Helpers.SpectralEstimator 154 declarations The ordinary and represented layers below are distinct wrappers around the same finite bounded-domain adapter.
# One bounded-domain certified spectral evaluator The ordinary and represented layers below are distinct wrappers around the same finite bounded-domain adapter. The adapter refines the certified-real bank radius, multiplies it by a reused radius-one circle node, evaluates the finite empirical transforms, forms the guarded quotient times the full circle tangent, applies endpoint-complete quadrature, and normalizes only afterwards.
A certified record for the experiment-wide range constant Ctheta: a strictly positive real number supplied as a certified name (a nested family of rational enclosures with an explicit accuracy modulus), together with the requirement that the number it names is exactly the parameter block's range constant Ctheta.
Definition (Lean source)
The sole experiment-wide primitive-record pair.
Definition (Lean source)
Two parameter blocks carry the same experiment-wide constants: the fixed order r, the cumulant-separation constant delta, the target range constant Ctheta, the treatment- and outcome-regression bounds Cg and Cq, and the two noise scales psieta and psixi all agree. Sample size and the remaining parameters are unconstrained.
Definition (Lean source)
Reuse one certified range record for a second parameter block whose range constant Ctheta is the same number. The certified name itself is reused verbatim; only the propositional contract identifying its value with the range constant is transported.
Definition (Lean source)
Reuse one certified primitive-record bundle (cumulant order, separation constant, noise scale, and the two search radii) for a second parameter block that carries the same experiment-wide constants.
Definition (Lean source)
Reuse one certified range record for a second parameter block that carries the same experiment-wide constants.
Definition (Lean source)
Canonical floor-dyadic observation interval.
Definition (Lean source)
Increasing the precision of the canonical dyadic enclosure of a real number by one binary digit shrinks the interval: the finer enclosure is contained in the coarser one.
Formal statement
Proof (Lean source)
At every precision, the canonical dyadic interval built from a real number actually contains that number.
Formal statement
Proof (Lean source)
For a positive rational accuracy target, taking the canonical dyadic enclosure at precision one more than the denominator of that target makes its width at most the target. This supplies the explicit accuracy modulus of the canonical name.
Formal statement
Proof (Lean source)
The canonical certified name of a real number: the number together with its family of floor-dyadic rational enclosures, the proofs that these are nested and always contain the number, and the explicit rule converting a requested accuracy into a precision level.
Definition (Lean source)
One observation as seen by the certified evaluator: certified names for the treatment value, the outcome value, and the clipped treatment-regression code value at that unit.
Definition (Lean source)
The complete certified input of the spectral estimator: one certified observation record for each of the n sample units, plus the experiment-wide certified primitive records (cumulant order, separation, noise scale, search radii) and the certified range constant.
Definition (Lean source)
The certified input built directly from a data set: each unit contributes the canonical certified names of its treatment, its outcome, and its treatment-regression code value clipped to the interval from minus Cg to Cg; the supplied primitive and range records are carried over unchanged.
Definition (Lean source)
Take a treatment-regression code sequence and a second one. If they agree at every covariate value after clipping to the range from minus Cg to Cg, then they produce the very same certified input record. Only the clipped code matters to the estimator.
Formal statement
Proof (Lean source)
The certified name of unit i's treatment residual: the certified difference between the treatment value and the clipped treatment-regression code value at that unit.
Definition (Lean source)
Selects one of the two deterministic sample-splitting folds: fold index zero gives the units below the halfway point, fold index one gives the remaining units.
The fixed disk box used by every empirical-transform map.
Definition (Lean source)
A rational Euclidean-magnitude envelope for every point in spectralDiskBox. The factor two safely converts the coordinate maximum used by ComplexRatInterval.maxAbs into a complex-norm bound.
Definition (Lean source)
The rational magnitude envelope of the fixed evaluation disk is never negative.
Formal statement
Proof (Lean source)
Adds up a finite list of complex rational rectangles left to right, starting from the degenerate rectangle at the origin.
Definition (Lean source)
Powers propagate input width with an explicit rational magnitude bound.
Formal statement
Proof (Lean source)
Existing rectangle multiplication exposes both operand widths and magnitudes; this alias records the propagation step used by the spectral finite-sum proof.
Formal statement
Proof (Lean source)
A recursive rectangle sum contains the sum of pairwise enclosed values.
Formal statement
Proof (Lean source)
Recursive rectangle addition accumulates no more than the sum of the individual coordinate widths.
Formal statement
Proof (Lean source)
Rational post-scaling propagates width linearly in the scalar magnitude.
Formal statement
Proof (Lean source)
Explicit rational exponential envelope on the fixed disk.
Definition (Lean source)
A rational upper bound for the size of unit i's treatment residual: the largest endpoint magnitude of the residual's certified enclosure, refined until its width is at most one.
Definition (Lean source)
A rational upper bound for the size of unit i's outcome: the largest endpoint magnitude of the outcome's certified enclosure, refined until its width is at most one.
Definition (Lean source)
The rational residual magnitude bound of any unit is never negative.
Formal statement
Proof (Lean source)
The rational outcome magnitude bound of any unit is never negative.
Formal statement
Proof (Lean source)
A rational magnitude envelope for the empirical residual transform and its derivatives of a given order over the disk of radius rho: the sum across sample units of the unit's residual magnitude bound raised to the derivative order, multiplied by a rational exponential envelope for that residual on the disk.
Definition (Lean source)
The same magnitude envelope for the outcome-weighted empirical transform: each unit contributes its outcome magnitude bound times its residual magnitude bound raised to the derivative order, times the rational exponential envelope on the disk of radius rho.
Definition (Lean source)
A conservative propagation envelope for canonical F intervals. The max 1 power is deliberately the same one exposed by the public interval power-width theorem; the extra radius and derivative factors pay for all finite-operation amplification without pretending that it is a semantic derivative bound.
Definition (Lean source)
The analogous canonical G propagation envelope, including the outcome magnitude needed by coefficient multiplication.
Definition (Lean source)
The magnitude envelope for the empirical residual transform is never negative.
Formal statement
Proof (Lean source)
The magnitude envelope for the outcome-weighted empirical transform is never negative.
Formal statement
Proof (Lean source)
For a nonnegative disk radius, the interval-propagation envelope of the empirical residual transform is never negative.
Formal statement
Proof (Lean source)
For a nonnegative disk radius, the interval-propagation envelope of the outcome-weighted empirical transform is never negative.
Formal statement
Proof (Lean source)
The canonical certified enclosure of a real number, taken at a given refinement level, has width at most two raised to the negative of one more than that level.
Formal statement
Proof (Lean source)
For canonically named data, the certified enclosure of any unit's treatment residual at a given refinement level has width at most twice two raised to the negative of one more than that level — twice the single-name bound, because the residual is a difference of two canonical names.
Formal statement
Proof (Lean source)
For canonically named data, the certified enclosure of any unit's outcome at a given refinement level has width at most two raised to the negative of one more than that level.
Formal statement
Proof (Lean source)
Once the refinement level is at least the one at which the residual's enclosure has width one, the largest endpoint magnitude of that enclosure is at most the unit's rational residual magnitude bound. Refining further can only shrink the enclosure.
Formal statement
Proof (Lean source)
Once the refinement level is at least the one at which the outcome's enclosure has width one, the largest endpoint magnitude of that enclosure is at most the unit's rational outcome magnitude bound.
Formal statement
Proof (Lean source)
Recursive whole-rectangle tightening of a fuel-indexed raw evaluator.
Definition (Lean source)
Sound raw enclosures remain sound after recursive tightening; consecutive fuel outputs are nested, and every tightened output lies inside the raw output at the same fuel.
Formal statement
Proof (Lean source)
The raw finite-sum interval program for the empirical F derivative.
Definition (Lean source)
The raw finite-sum interval program for the empirical G derivative.
Definition (Lean source)
Cross-fuel-nested empirical F evaluation obtained by tightening the whole raw finite-sum rectangle at every successive fuel.
Definition (Lean source)
Cross-fuel-nested empirical G evaluation obtained by tightening the whole raw finite-sum rectangle at every successive fuel.
Definition (Lean source)
The finite-sum certified empirical F map on the fixed disk.
Definition (Lean source)
The finite-sum certified empirical G map on the same fixed disk.
Definition (Lean source)
If one complex rectangle is contained in another, then its coordinate diameter is no larger.
Formal statement
Proof (Lean source)
Canonical centered raw F evaluation is semantically sound on every subrectangle of the full spectral box.
Formal statement
Proof (Lean source)
Canonical centered raw G evaluation is semantically sound on every subrectangle of the full spectral box.
Formal statement
Proof (Lean source)
The scheduled raw F rectangle pays for the derivative envelope times the certified input width in addition to the centered algorithmic remainder.
Formal statement
Proof (Lean source)
The scheduled raw G rectangle has the analogous full-box effective-width bound, including the canonical outcome-name refinement.
Formal statement
Proof (Lean source)
The three kinds of certified contour node the estimator evaluates: the pilot boundary scan, the winding-number quadrature, and the final moment evaluation.
Definition (Lean source)
The number of certified interval operations charged to one contour node, as an affine function of the fold's sample size: twelve per unit plus eighteen for a pilot node, twenty-four per unit plus thirty-eight for a winding node, and twenty-eight per unit plus forty-two for an evaluation node.
Definition (Lean source)
The quadratic requested factor pays for applying the raw Newton norm enclosure after certified-radius multiplication. The factor sixty-four leaves the corresponding quotient/tangent propagation margin.
Definition (Lean source)
How accurately the certified contour radius must be refined before it is multiplied by a unit-circle node: the requested accuracy divided by four times one plus the node's own width, capped at one so the precision request never exceeds a unit.
Definition (Lean source)
The node and mesh halves of the pilot's aStar/64 error budget.
Definition (Lean source)
The mesh half of the pilot error budget: one hundred twenty-eighth of the bank's boundary-modulus certificate.
Definition (Lean source)
The total pilot error budget: one sixty-fourth of the bank's boundary-modulus certificate, split evenly between the node and mesh halves.
Definition (Lean source)
The total error budget of the final moment evaluation: the reciprocal of the sample size (with one as a floor), so that the evaluation error vanishes as the sample grows.
Definition (Lean source)
The node half of the evaluation error budget: one over twice the sample size (with one as a floor).
Definition (Lean source)
The mesh half of the evaluation error budget: one over twice the sample size (with one as a floor).
Definition (Lean source)
The node half of the winding-number error budget, fixed at one sixteenth: together with the mesh half this keeps the decoded winding enclosure inside a quarter-width window.
Definition (Lean source)
The mesh half of the winding-number error budget, fixed at one sixteenth.
Definition (Lean source)
A positive denominator certificate controls both guarded division and the propagation of input-rectangle error through the quotient.
Definition (Lean source)
A rational upper bound for the j-th bank radius: the largest endpoint magnitude of that radius's certified enclosure, refined until its width is at most one.
Definition (Lean source)
The error-one radius enclosure needs one explicit unit of slack before it is used as a rectangle-magnitude factor.
Definition (Lean source)
A closed rational upper bound for the amplification introduced after quadrature by division through the certified N * 2πi rectangle.
Definition (Lean source)
Branch-wide scale for interval propagation. It includes the certified radius multiplication, full-box empirical-map magnitude/derivative envelope, guarded quotient inverse-margin loss, tangent multiplication, finite quadrature accumulation, and post-quadrature normalization.
Definition (Lean source)
The rational upper bound for a bank radius is never negative.
Formal statement
Proof (Lean source)
A Lipschitz constant, along a circle of radius rho, for the modulus of the empirical residual transform: eight times the radius times the first-derivative magnitude envelope of that transform. It controls the mesh error of the pilot boundary scan.
Definition (Lean source)
A Lipschitz constant along the circle of radius rho for the logarithmic-derivative quotient integrated by the winding-number quadrature, given a positive lower bound m on the denominator: it combines the first- and second-derivative magnitude envelopes of the empirical residual transform, divided by m and by m squared respectively, with an overall factor sixty-four.
Definition (Lean source)
A Lipschitz constant along the circle of radius rho for the outcome-weighted quotient integrated by the moment evaluation, given a positive lower bound m on the denominator: it combines the magnitude envelopes of the outcome-weighted transform and of the residual transform, divided by m and by m squared, with an overall factor sixty-four.
Definition (Lean source)
For a nonnegative circle radius, the pilot Lipschitz constant is never negative.
Formal statement
Proof (Lean source)
For a nonnegative circle radius and a strictly positive denominator lower bound, the winding-quadrature Lipschitz constant is never negative.
Formal statement
Proof (Lean source)
For a nonnegative circle radius and a strictly positive denominator lower bound, the moment-evaluation Lipschitz constant is never negative.
Formal statement
Proof (Lean source)
Full-box interval amplification for the pilot empirical denominator map. The contour Lipschitz bound is intentionally absent: it is stored separately in Schedule.magnitude and controls only the mesh error.
Definition (Lean source)
The pilot amplification factor is exactly the whole-number part of the square of one hundred twenty-eight times the (floored-at-one) interval-propagation envelope of the empirical residual transform at derivative order zero; in particular it does not depend on which bank circle is used.
Formal statement
Proof (Lean source)
The pilot amplification factor is never negative.
Formal statement
Proof (Lean source)
Full-box magnitude and derivative amplification for the two empirical F maps used by guarded winding division.
Definition (Lean source)
The winding-quadrature amplification factor is never negative.
Formal statement
Proof (Lean source)
Full-box magnitude and derivative amplification for empirical G/F in the evaluation quotient.
Definition (Lean source)
The moment-evaluation amplification factor is never negative.
Formal statement
Proof (Lean source)
The complete accuracy schedule for the pilot boundary scan on fold a and bank circle j: it fixes the mesh of the circle, the refinement level of every certified node, and the input precision, from the pilot error budget rescaled by the branch-wide propagation scale and by the circle Lipschitz constant.
Definition (Lean source)
Common certified-real-radius node used by pilot, winding, and evaluation.
Definition (Lean source)
Pilot boundary infimum from the same bounded denominator map.
Definition (Lean source)
The certified circle evaluator used to compute the winding number on bank circle j: its numerator is the first derivative of the empirical residual transform on the lower fold, its denominator the transform itself, and its accuracy schedule is derived from the winding error budget guarded by the supplied positive lower bound on the denominator.
Definition (Lean source)
A certified rectangular enclosure of the winding number of the empirical residual transform around bank circle j: if the pilot scan certifies a strictly positive lower bound on the transform's modulus along that circle, the argument-principle contour integral is evaluated and normalized; otherwise the degenerate rectangle at the origin is returned.
Definition (Lean source)
Decodes a complex rectangle to a nonnegative whole number when it can only contain one: the candidate is the ceiling of the real lower endpoint, and it is returned exactly when that candidate lies inside the real range, the real upper endpoint is less than one above it, and the imaginary range straddles zero. Otherwise nothing is returned.
Definition (Lean source)
Soundness, completeness at the paper's strict quarter-width threshold, and uniqueness of the finite winding decoder.
Definition (Lean source)
The finite winding decoder is sound, complete, and unique: whatever it returns is genuinely contained in the rectangle; any nonnegative whole number contained in a rectangle narrower than a quarter in both coordinates is returned; and if it returns a number while the rectangle is narrower than one in the real direction, no other nonnegative whole number lies in the rectangle.
Formal statement
Proof (Lean source)
If a rectangle contains a nonnegative whole number and is narrower than a quarter in the real direction and in the imaginary direction, then the finite decoder returns exactly that number.
Formal statement
Proof (Lean source)
What the pilot pass records for one bank circle: the certified enclosure of the minimum modulus of the empirical residual transform along the circle, the certified enclosure of the winding number, and the decoded winding number when the enclosure pins one down.
Definition (Lean source)
Runs the pilot pass on bank circle j: computes the certified boundary-modulus interval from the lower fold, the certified winding enclosure, and the decoded winding number.
Definition (Lean source)
A pilot outcome is admissible when its certified boundary modulus is at least half the bank's modulus certificate and its winding number decoded to at least one, so the circle provably encloses a zero and stays away from the boundary.
Definition (Lean source)
Tests whether bank circle j is a best admissible circle: it is admissible and its certified boundary modulus is at least as large as that of every other admissible circle.
Definition (Lean source)
Picks the contour from a family of pilot outcomes: the smallest-indexed circle among those maximizing the certified boundary modulus over admissible circles, or nothing at all if no circle is admissible.
Definition (Lean source)
The contour actually selected for a given certified input: run the pilot pass on every bank circle, then take the least-indexed circle maximizing the certified boundary modulus among admissible ones.
Definition (Lean source)
The certified circle evaluator used for the final moment integral on bank circle j: its numerator is the outcome-weighted empirical transform on the upper fold, its denominator the residual transform on that fold, its normalization count the decoded winding number (floored at one), and its accuracy schedule comes from the evaluation error budget guarded by the supplied positive lower bound on the denominator.
Definition (Lean source)
A certified rectangular enclosure of the final contour moment on bank circle j: if the upper fold's pilot scan certifies a strictly positive lower bound on the denominator's modulus, the contour integral is evaluated and divided by the decoded winding count; otherwise the degenerate rectangle at the origin is returned.
Definition (Lean source)
Build-aware pilot execution. The finite extremum is performed by the certified build over the actual denominator-node modulus intervals.
Definition (Lean source)
Build-aware winding execution. The build performs the trapezoidal quadrature on the evaluator's certified nodes before normalization.
Definition (Lean source)
Build-aware moment execution, using the build's pilot extremum and its quadrature primitive on the evaluation nodes.
Definition (Lean source)
If the compiled interval-arithmetic build computes finite extrema by the canonical rule, then running the pilot boundary scan through the build gives exactly the reference boundary-modulus interval.
Formal statement
Proof (Lean source)
If the compiled interval-arithmetic build computes extrema and quadrature by the canonical rules, then running the winding computation through the build gives exactly the reference winding enclosure.
Formal statement
Proof (Lean source)
If the compiled interval-arithmetic build computes extrema and quadrature by the canonical rules, then running the moment evaluation through the build gives exactly the reference evaluation enclosure.
Formal statement
Proof (Lean source)
A compiled implementation supplies only the three callable entry points of the one bounded adapter, together with their correspondence to the local finite programs. Paper-specific map validity, margins, and schedule bounds are derived locally and are deliberately not fields of this carrier.
Definition (Lean source)
The midpoint of a rational interval, the average of its two endpoints.
Definition (Lean source)
The bare computational content of a certified real number as returned by the program: a family of rational enclosures indexed by a refinement level, together with a rule turning a requested accuracy into a refinement level. No soundness property is bundled in; those are stated separately.
Definition (Lean source)
An executable name represents a real number when every one of its rational enclosures, at every refinement level, contains that number.
Definition (Lean source)
An executable name certifies a real number when its enclosures shrink as the refinement level increases, the enclosure returned at the level demanded by any accuracy request is at least that accurate, and every enclosure contains the number.
Definition (Lean source)
The image of a rational interval under absolute value: the interval itself when it lies in the nonnegative half-line, its reflection when it lies in the nonpositive half-line, and otherwise the interval from zero to the larger of the two endpoint magnitudes.
Definition (Lean source)
The rational enclosure, at a given refinement level, of the raw output y clipped to the symmetric range determined by the certified constant: it evaluates the identity that half the difference between the absolute values of y plus the constant and y minus the constant equals y truncated to that range.
Definition (Lean source)
The executable certified name of the estimator's reported value: the rational raw output clipped to the symmetric range given by the certified range constant, with the accuracy modulus inherited from that constant's own certified name.
Definition (Lean source)
The three reasons the estimator can fall back to its default output: no bank circle was admissible, the winding enclosure did not pin down a whole number, or the evaluation fold's certified boundary modulus was too small.
Definition (Lean source)
The five certified quantities the evaluator can request approximations of: a treatment value, an outcome value, a clipped treatment-regression code value, a treatment residual, and a bank radius.
Definition (Lean source)
The certified rectangle operations the evaluator performs: subtraction, exponentiation, multiplication, addition, scalar rescaling, modulus and squared modulus, guarded division, finite infimum, trapezoidal quadrature, and post-quadrature normalization.
Definition (Lean source)
One recorded step of the estimator's execution. Events cover which sample fold was used, each accuracy request and each approximation read from a certified name, residual subtractions, radius refinements, unit-circle nodes, complex exponentials with their Taylor and square-root truncation levels, empirical transform node values, individual rectangle operations, guarded divisions and tangent multiplications, the finite extremum and quadrature calls, post-quadrature normalization, returned enclosures, endpoint acceptance tests, fallback decisions, and the tie-break choice of contour.
Definition (Lean source)
A full execution trace: the list of recorded steps, in the order the estimator performs them.
Definition (Lean source)
The half-error/max-fuel behavior of CertifiedReal.sub is visible in the trace rather than summarized as one residual event.
Definition (Lean source)
The execution trace produced by evaluating the empirical residual transform at one contour node: for each unit in the fold it records the residual-subtraction steps, the approximation read of the residual, the complex exponential with its Taylor truncation level, the multiplication by the residual power, and the resulting node value.
Definition (Lean source)
The execution trace produced by evaluating the outcome-weighted empirical transform at one contour node: as for the residual transform, with an extra approximation read of the unit's outcome before the exponential and the multiplication.
Definition (Lean source)
Endpoint-complete node trace: range (mesh+1) is exactly k ≤ mesh. Every repeated empirical rectangle operation is emitted at its execution site.
Definition (Lean source)
The execution trace of the pilot boundary scan on one fold and one bank circle: the fold selection, then for every mesh node the radius refinement, the unit-circle node, the residual-transform evaluation and the modulus with its square-root truncation, and finally the finite-infimum step over all nodes.
Definition (Lean source)
The execution trace of the winding-number computation on one bank circle: the pilot scan on the lower fold, then — only if the certified boundary modulus is strictly positive — the evaluator's node trace, the quadrature and normalization steps, and the returned enclosure; if the modulus test fails the trace stops at the rejected endpoint comparison.
Definition (Lean source)
The execution trace of the whole pilot pass: for every circle in the bank, in index order, the lower-fold boundary scan followed by the winding computation on that circle.
Definition (Lean source)
Everything one run of the estimator returns: the certified name of the reported value, the raw rational value before clipping, the full execution trace, which bank circle was selected, which winding number was decoded, and the final moment enclosure when one was computed.
The one instrumented option-A finite-rational adapter, parameterized only by the three bounded-domain entry points used at runtime.
Definition (Lean source)
The one instrumented option-A finite-rational adapter used by the ordinary wrapper.
Definition (Lean source)
Unconditional ordinary wrapper.
Definition (Lean source)
The represented wrapper calls the supplied compiled entry points of the same bounded adapter.
Definition (Lean source)
Running the estimator through any compiled implementation of the bounded adapter gives exactly the same result — value, trace, selected contour, decoded winding number and enclosure — as the reference instrumented program.
Formal statement
Proof (Lean source)
Semantic empirical residual used only in soundness statements for the finite rational adapter. It is not an executable evaluator path.
Definition (Lean source)
Exact value enclosed by spectralDenominatorMap; proof target only.
Definition (Lean source)
Exact value enclosed by spectralNumeratorMap; proof target only.
Definition (Lean source)
For canonically named data, the real number named by the certified residual of a unit is exactly that unit's treatment minus its clipped treatment-regression code value.
Formal statement
Proof (Lean source)
For canonically named data, the exact value enclosed by the certified residual-transform map coincides with the semantic empirical transform: the fold average of the residual raised to the derivative order times the exponential of the argument against that residual.
Formal statement
Proof (Lean source)
For canonically named data, the exact value enclosed by the certified outcome-weighted map coincides with the semantic outcome-weighted empirical transform.
Formal statement
Proof (Lean source)
The estimator's full result on a data set: build the canonical certified input from the data and the fixed primitive and range records, then run the ordinary finite-rational program on it.
Definition (Lean source)
The real-valued point estimate reported by the estimator: the raw rational output of the program, truncated to the symmetric range determined by the certified range constant.
Definition (Lean source)
Take a treatment-regression code sequence and a second one. If they agree at every covariate value after clipping to the range from minus Cg to Cg, then they yield the same point estimate on every data set.
Formal statement
Proof (Lean source)
Supplied certified observation records for the represented transducer. The type indices fix the experiment-wide primitive records; callers supply only the observation records.
Definition (Lean source)
Completes a caller-supplied family of certified observation records into a full certified input by attaching the experiment-wide primitive and range records.
Definition (Lean source)
The estimator packaged as one object: the domain condition it requires of the supplied regression code, the program it runs on a data set, the real point estimate it reports, the execution trace it emits, the version of the program driven by a compiled implementation, and the correspondence property tying that version to the reference one.
Definition (Lean source)
Lets a packaged estimator be applied directly to a data set, returning its real point estimate.
Definition (Lean source)
The correctness contract demanded of a compiled implementation: on every data set it returns the same result and the same execution trace as the reference program, and the certified name it outputs genuinely certifies the estimator's real point estimate.
Definition (Lean source)
The estimator itself, assembled for a given parameter block, fixed certified records, and supplied treatment-regression code sequence: it requires the code at the current sample size to be measurable, runs the canonical finite-rational program, reports the clipped point estimate, exposes the full execution trace, and demands of any compiled implementation the represented-execution contract.
Definition (Lean source)
Take a treatment-regression code sequence and a second one. If they agree at every covariate value after clipping to the range from minus Cg to Cg, then the two assembled estimators are the same function of the data.
Formal statement
Proof (Lean source)
A compiled implementation is a faithful execution of the estimator when it satisfies the estimator's own represented-output correspondence requirement.
Definition (Lean source)
Helpers.SpectralMeasurability 13 declarations Measurability of the finite rational spectral program
Measurability of the finite rational spectral program
A fixed-precision canonical dyadic interval is a Borel function of its real input.
Formal statement
Proof (Lean source)
Canonical dyadic approximation is jointly measurable in the real input and precision.
Formal statement
Proof (Lean source)
Canonical dyadic approximation remains measurable at a measurable data-dependent precision.
Formal statement
Proof (Lean source)
The treatment-name interval queried at measurable fuel is measurable in the sample.
Formal statement
Proof (Lean source)
The outcome-name interval queried at measurable fuel is measurable in the sample.
Formal statement
Proof (Lean source)
The clipped code-name interval queried at measurable fuel is measurable in the sample.
Formal statement
Proof (Lean source)
Provided the treatment-regression code used at the current sample size is a measurable function of the covariates, the pilot enclosure of the smallest modulus the empirical denominator transform attains along a given bank circle, computed on either fold from the certified input built canonically from the data, is a measurable function of the sample.
Formal statement
Proof (Lean source)
Provided the treatment-regression code used at the current sample size is a measurable function of the covariates, the certified rectangular enclosure of the winding number of the empirical residual transform around a given bank circle, computed from the certified input built canonically from the data, is a measurable function of the sample.
Formal statement
Proof (Lean source)
Provided the treatment-regression code used at the current sample size is a measurable function of the covariates, the certified rectangular enclosure of the contour moment on a given bank circle at a given quadrature order, computed from the certified input built canonically from the data, is a measurable function of the sample.
Formal statement
Proof (Lean source)
The raw rational projection of the option-A program, separated from its certified output name and diagnostic trace.
Definition (Lean source)
Erasing the certified name and trace from the option-A program preserves its raw rational result.
Formal statement
Proof (Lean source)
A measurable countable-valued control state may select among measurable branches.
Formal statement
Proof (Lean source)
The rational output of the canonical option-A program is Borel measurable.
Formal statement
Proof (Lean source)
Helpers.Transforms 23 declarations The unweighted transforms use Mathlib's complex MGF.
Population and empirical analytic transforms
The unweighted transforms use Mathlib's complex MGF. The two genuinely weighted transforms are Bochner integrals with a separate weight.
Weighted bilateral exponential transform.
Definition (Lean source)
The moment generating function of the treatment noise — the deviation of the treatment from its conditional mean given the covariate — evaluated at a complex argument: the expectation of the exponential of that argument times the treatment noise.
Definition (Lean source)
The moment generating function of the treatment-code error at sample size n — the gap between the true treatment regression and the supplied clipped code — evaluated at a complex argument.
Definition (Lean source)
The exponential transform of the treatment-code error weighted by the outcome-side contamination: the expectation of the contamination evaluated at the covariate times the exponential of the complex argument multiplied by the treatment-code error.
Definition (Lean source)
The moment generating function of the observable learned residual at sample size n — the treatment minus the supplied clipped treatment code evaluated at the covariate — at a complex argument.
Definition (Lean source)
The exponential transform of the observable learned residual weighted by the outcome: the expectation of the outcome times the exponential of the complex argument multiplied by the learned residual.
Definition (Lean source)
The exact Luxemburg envelope gives every real exponential moment of the treatment noise.
Formal statement
Proof (Lean source)
The treatment-noise MGF is entire; this is derived from the class's Luxemburg envelope rather than assumed as model data.
Formal statement
Proof (Lean source)
The learned residual has every real exponential moment.
Formal statement
Proof (Lean source)
The outcome innovation has every real exponential moment.
Formal statement
Proof (Lean source)
The outcome innovation times a learned-residual exponential is integrable.
Formal statement
Proof (Lean source)
Conditional mean independence annihilates the outcome innovation against the learned-residual exponential weight.
Formal statement
Proof (Lean source)
The residual complex MGF is entire under the paper's exponential-moment envelope; this is derived from its construction rather than assumed.
Formal statement
Proof (Lean source)
Split empirical unweighted transform.
Definition (Lean source)
Split empirical outcome-weighted transform.
Definition (Lean source)
Multiplicity-adjusted transform-zero instrument.
Definition (Lean source)
Independence of the treatment noise and covariates factors the learned-residual MGF.
Formal statement
Proof (Lean source)
The bounded covariate contamination times a learned-residual exponential is integrable.
Formal statement
Proof (Lean source)
The covariate contamination term factors from the treatment-noise exponential.
Formal statement
Proof (Lean source)
The normalized logarithmic-derivative integral used as the contour count.
Definition (Lean source)
Observable normalized contour ratio.
Definition (Lean source)
Observable factorization of the learned-residual transforms.
Formal statement
Proof (Lean source)
Direct L1 control keeps the nuisance transform uniformly away from zero and preserves analytic zero multiplicities.
Formal statement
Proof (Lean source)
Helpers.UniformDiskSeries 10 declarations This file isolates the two generic steps used by empirical analytic-transform arguments: a power-series coefficient majorant controls the supremum norm on a closed disk, and a countable dense skeleton makes that supremum
Measurable uniform bounds for analytic series on a disk
This file isolates the two generic steps used by empirical analytic-transform
arguments: a power-series coefficient majorant controls the supremum norm on a
closed disk, and a countable dense skeleton makes that supremum measurable and
transfers an L² envelope bound to it.
The uniform norm of a complex-valued random function on the closed disk of radius R.
Definition (Lean source)
The set-builder presentation of the disk supremum agrees with its image presentation.
Formal statement
Proof (Lean source)
An absolutely summable coefficient majorant bounds an analytic series uniformly on the closed disk of radius R.
Formal statement
Proof (Lean source)
The coefficient majorant of an analytic series bounds its uniform norm on the closed disk.
Formal statement
Proof (Lean source)
A countable dense skeleton makes a pointwise disk supremum measurable once the supremum over the skeleton is known to equal the full supremum.
Formal statement
Proof (Lean source)
A measurable pointwise envelope transfers its squared lintegral bound to the uniform norm on a nonempty closed disk.
Formal statement
Proof (Lean source)
Under a finite product probability law, the centered empirical average of a real square-integrable coefficient has second moment at most its population L² energy divided by the sample size.
Formal statement
Proof (Lean source)
Restricting a product sample to a nonempty deterministic finset preserves the inverse-cardinality second-moment bound for a centered average.
Formal statement
Proof (Lean source)
A measurable real function whose squared nonnegative integral is bounded by C² belongs to L² and has L² norm at most C.
Formal statement
Proof (Lean source)
Countably many measurable nonnegative coefficient envelopes obey the L² Minkowski bound when their individual L² norms have a summable real majorant. This packages the finite-truncation and L² limit step needed after applying pi_centered_average_sq_lintegral_le coefficient by coefficient.
Formal statement
Proof (Lean source)
OpenQuestions 11 declarations Nothing in this file asserts a solution of the open problem.
Recorded local-to-Gaussian open problem
Nothing in this file asserts a solution of the open problem.
A rational candidate circle is represented only by its positive radius.
Definition (Lean source)
The finite deterministic rational-circle library at depth m.
Definition (Lean source)
The point of a candidate circle at a given angle: the circle's rational radius times the complex exponential of that angle, so that letting the angle run from zero to two pi traverses the circle once counterclockwise.
Definition (Lean source)
The boundary modulus of a transform on a candidate circle: the smallest absolute value the transform attains anywhere on the circle of that radius centred at the origin. It is the quantity that must be certified strictly positive before the transform may be used as the denominator of a contour integrand.
Definition (Lean source)
The denominator in every candidate record is definitionally the actual empirical transform on its stated inference fold.
Definition (Lean source)
The numerator in every candidate record is definitionally the actual outcome-weighted empirical transform on its stated inference fold.
Definition (Lean source)
The two empirical contour integrands are formed only after a positive boundary-modulus certificate has been supplied.
Definition (Lean source)
The contour-moment integrand on a candidate circle: at each angle, the circle point times the value of the numerator transform there, divided by the value of the denominator transform there. It is formed only after the denominator's boundary modulus on that circle has been certified strictly positive, so the ratio is well defined all along the contour.
Definition (Lean source)
Certified candidate data for one actual sample, inference fold, and rational circle. Its values are enclosures, and every soundness field is tied definitionally to empiricalF and empiricalG on inferenceFold; arbitrary transform arguments cannot be supplied. It contains no selector, estimator, risk, coverage, critical-scale, or lower-bound field.
Definition (Lean source)
The dependent candidate-data schema computed from the actual empirical contour integrands on a prespecified fold and rational circle.
Definition (Lean source)
The unresolved local-to-Gaussian frontier, recorded as complete descriptive payload rather than an asserted proposition. The paper leaves the sharp-rate functional, uniform-inference criterion, selector, confidence procedure, and matching lower-bound witness undefined.
Definition (Lean source)
T1_KnownZeroInstrument 1 declarations Known transform-zero instrument
Known transform-zero instrument
Take at least one observation, a model in the broad non-Gaussian class, and a complex point at which the treatment-noise moment generating function vanishes to a known finite order that is at least one. Build the instrument that raises its argument to the power one below that order and multiplies by the exponential of the zero times the argument. Then the instrument is exactly orthogonal to the treatment noise — its mean is zero however the noise is shifted, and its conditional mean given the covariates vanishes almost surely; its covariance with the observable learned residual equals the derivative of that order of the treatment transform at the zero times the treatment-code-error transform there; and whenever that covariance is nonzero the treatment coefficient equals the ratio of the outcome-weighted instrument mean to it.
Formal statement
Proof (Lean source)
T2_ExactContourIdentification 3 declarations Exact contour identification
Exact contour identification
Every radius in the fixed translated-dyadic bank is positive.
Formal statement
Proof (Lean source)
A weighted exponential transform with bounded measurable weight and argument is complex differentiable everywhere.
Formal statement
Proof (Lean source)
Take at least one observation and a model in the non-Gaussian spectral class. Fix one circle of the certified radius bank and suppose the transform of the observable learned residual has no zero on that circle, the transform of the treatment-code error has no zero anywhere in the closed disk it bounds, and the residual transform does have at least one zero, counted with multiplicity, strictly inside. Then the treatment coefficient is exactly identified by the contour functional built from the residual transform and the outcome-weighted residual transform on that circle, and that functional is the contour integral of the ratio of the two transforms around the circle, divided by the number of enclosed residual zeros times two pi i.
Formal statement
Proof (Lean source)
T3_AdaptiveRootNMinimax 1 declarations The ordinary statistic and all statistical bounds below are unconditional.
Certified adaptive contour estimator and matched fixed-separation rate
The ordinary statistic and all statistical bounds below are unconditional. Only the final represented-data execution clause is parameterized by a compiled implementation of the bounded certified complex arithmetic record.
Fixed-separation matched minimax MSE and generalized-quantile bounds. The same supplied primitive records are used by the bank, the ordinary Borel statistic, and (conditionally) the represented-data transducer.
Formal statement
Proof (Lean source)
T4_JmsAceAlignment 5 declarations Alignment with the published finite-order ACE class
Alignment with the published finite-order ACE class
The same parameter block with the second nuisance-accuracy sequence raised to a floor: each of its terms is replaced by the larger of the original term and the fixed level t, leaving every other constant untouched.
Definition (Lean source)
The same data-generating law, the same treatment and outcome regressions and the same supplied code sequences, read as a model indexed by a different parameter block. Nothing about the distribution changes; only the block of constants attached to it is relabelled.
Definition (Lean source)
For a nonnegative constant, a strictly positive scale and a sample size of at least one, the square root of the constant divided by the scale times the sample size equals the square root of the constant over the scale, multiplied by the sample size raised to the power −1/2 — the parametric-rate factor is split off from the constant.
Formal statement
Proof (Lean source)
With a nonnegative constant, a strictly positive scale and a strictly positive multiplier, if one sequence grows strictly faster than the parametric rate, in the sense that its ratio to the sample size raised to the power −1/2 diverges, and a second sequence eventually dominates the multiplier times the first, then the ratio of the parametric-rate quantity, the square root of the constant over the scale times the sample size, to the second sequence tends to zero.
Formal statement
Proof (Lean source)
The paper's spectral estimator and the published finite-order ACE procedure are put on a common footing, and the spectral guarantee eventually dominates. Fix an expansion order of at least two, a positive cumulant separation and positive bounds on the treatment effect, the two regressions and the two sub-Gaussian scales; then there is a positive constant, depending only on those inputs, such that for any published order-r ACE procedure enjoying its cited generalized-quantile guarantee at an overlap exponent strictly between one half and one: the published ACE class is contained in the paper's non-Gaussian class and contains the comparison subclass, and coincides with that subclass when the smoothness index equals the expansion order; the published estimator's generalized-quantile error over the published class is at most the cited finite-order ACE bound; the spectral estimator's worst-case generalized-quantile error over the same class is at most the square root of that constant divided by the overlap exponent times the sample size; and along any sequence of parameter blocks that keeps the fixed constants and whose ACE leading term outgrows the parametric rate, the ratio of the spectral guarantee to the published bound tends to zero.
Formal statement
Proof (Lean source)
T5_CommonExperimentDichotomy 4 declarations Separate common-experiment conclusions
Separate common-experiment conclusions
Compatibility name for the represented wrapper now defined beside the single option-A adapter.
Definition (Lean source)
A compiled implementation of the bounded spectral adapter is a faithful execution of the estimator built from the given parameter block, certified primitive records, certified range record, and treatment-regression code: everything the compiled build reports agrees with what the estimator's own specification demands.
Definition (Lean source)
Running the contour-selection program through a compiled implementation of the bounded adapter returns exactly the same outcome — reported value, execution trace, selected contour, decoded winding number, and enclosure — as the reference instrumented program, so the choice of compiled build never changes what the estimator reports.
Formal statement
Proof (Lean source)
Fix the experiment-wide constants of the partially linear design: a cumulant order of at least two, a strictly positive cumulant-separation constant, a strictly positive range bound for the treatment coefficient, strictly positive uniform bounds for the treatment and outcome regressions, and strictly positive sub-Gaussian scales for the treatment noise and the outcome noise. Then the same experiment splits into two sharply different halves: on the non-Gaussian class a single pair of positive constants c and C bounds the minimax mean squared error between c/n and C/n along every sequence of sample sizes that carries these constants, the assembled estimator is Borel measurable, attains the C/n upper bound over that class, is executed faithfully by every compiled build, and is read off a contour bank that never changes with the sample size; whereas on the simultaneous bounded-outcome Gaussian class the treatment coefficient is forced to be zero, so both the Gaussian minimax mean squared error and the Gaussian minimax generalized-quantile error vanish identically.
Formal statement
Proof (Lean source)
T6_SymmetricMixtureReduction 4 declarations Symmetric Gaussian-mixture reduction
Symmetric Gaussian-mixture reduction
Equal mixture of N(-1,1) and N(1,1).
Definition (Lean source)
The symmetric Gaussian mixture — equal weight on a unit-variance normal centred at minus one and on a unit-variance normal centred at plus one — is a probability measure, its total mass being one.
Definition (Lean source)
The stipulated symmetric mixture has a uniform second-moment envelope.
Formal statement
Proof (Lean source)
Once the range bound for the treatment coefficient, the two regression bounds, and the outcome-noise scale are fixed, one constant works for every sample size: for any model in which the treatment noise follows the symmetric two-component Gaussian mixture, the data are drawn independently, the usual regularity conditions of the non-Gaussian class hold, and the treatment code is accurate in mean to within one over pi, the fourth cumulant of the treatment noise is exactly minus two, the treatment moment generating function vanishes at the imaginary point i times pi over two, the population sine score equals exp(-π²/8) times the average cosine of the treatment-code error, that score is bounded below by half of exp(-π²/8), and the resulting clipped sine estimator has mean squared error at most the constant divided by the sample size.
Formal statement
Proof (Lean source)
T7_LocalToGaussianPartialBenchmarks 1 declarations Closed local-to-Gaussian upper benchmarks
Closed local-to-Gaussian upper benchmarks
Along a cumulant-separation schedule that is strictly positive at every sample size, nonincreasing, and shrinking to zero, so that the treatment noise drifts toward Gaussian as the sample grows, two closed upper benchmarks are available and can be combined: first, one constant, depending only on the range and regression bounds and the outcome-noise scale, delivers the parametric mean squared error bound for every Gaussian--Rademacher mixture whose mixing weight is strictly positive and at most one, under the usual regularity conditions of the class; second, any published adaptive-cumulant-estimator procedure carrying its stated generalized-quantile guarantee keeps that guarantee at each sample size along this schedule, and a risk that respects both the double-machine-learning benchmark and the adaptive-cumulant benchmark also respects the smaller of the two.
Formal statement
Proof (Lean source)
T8_BoundedOutcomeGaussianDegeneracy 3 declarations Degeneracy of the simultaneous bounded-outcome Gaussian intersection
Degeneracy of the simultaneous bounded-outcome Gaussian intersection
A bounded conditional-mean PLM with nondegenerate Gaussian treatment noise cannot have a nonzero treatment coefficient.
Formal statement
Proof (Lean source)
The generalized lower quantile of the identically zero loss is zero at the paper's interior probability level.
Formal statement
Proof (Lean source)
The simultaneous bounded-outcome Gaussian class is degenerate: every model in it has treatment coefficient exactly zero, so for any supplied pair of treatment- and outcome-code sequences that the class can match, both the minimax mean squared error and the minimax generalized-quantile error over that class are exactly zero — the estimator that always reports zero is perfect there.