Formalization: Uniform Estimation and Honest Inference in Regression Discontinuity with a Mismeasured Score
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs. Note: this index was generated at a different commit than the paper's audited pin (f9001b6) — statements may have moved since the audit.
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Basic 52 declarations Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The latent coordinates are score, two binary potential outcomes, and error.
The observed coordinates are proxy score, true treatment side, and binary outcome.
Binary outcomes take their usual numerical values. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The latent score coordinate. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Both potential outcomes remain in the latent schedule. Given the displayed inputs and assumptions, this definition specifies the stated object.
The latent perturbation coordinate. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Treatment uses the true latent score. Given the displayed inputs and assumptions, this definition specifies the stated object.
The observed outcome is the potential outcome at the assigned side. Given the displayed inputs and assumptions, this definition specifies the stated object.
Known-scale perturbation of the latent score. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The common observation map. Given the displayed inputs and assumptions, this definition specifies the stated object.
Ambient latent law with its density and continuous conditional-mean versions.
Definition (Lean source)
The observed law is the common pushforward. Given the displayed inputs and assumptions, this definition specifies the stated object.
The cutoff causal contrast. Given the displayed inputs and assumptions, this definition specifies the stated object.
The fractional seminorm on the whole latent interval. Given the displayed inputs and assumptions, this definition specifies the stated object.
Arm reflection. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Centered Gaussian density at the public noise scale. Given the displayed inputs and assumptions, this definition specifies the stated object.
Mathlib shifted Legendre uses the reversed interval orientation. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Standard Gaussian error. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Error is independent of the whole potential-outcome schedule jointly with the score. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Global lower and upper density bounds. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Interior bounds for each potential-mean version. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Radius-two Hölder restriction, written pointwise to avoid a real-supremum junk value. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The exact benchmark class contains precisely the five maintained member atoms.
Definition (Lean source)
The noise scale indexes the observed experiment, and does not change latent membership.
Definition (Lean source)
Finite observed sample.
Definition (Lean source)
Randomized procedure input, with an independent unit-interval seed.
Definition (Lean source)
The seed has uniform probability measure on the unit interval. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
IID observation law before procedure randomization. Given the displayed inputs and assumptions, this definition specifies the stated object.
The sample experiment includes the independent uniform seed. Given the displayed inputs and assumptions, this definition specifies the stated object.
Every measurable real-valued procedure is permitted.
Definition (Lean source)
Connected closed intervals with measurable endpoints, lying in the declared target region.
Definition (Lean source)
Uniform ninety-percent coverage on the exact benchmark. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Extended absolute loss risk retains infinite loss of arbitrary procedures. Given the displayed inputs and assumptions, this definition specifies the stated object.
Extended expected length. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Minimax absolute risk, converted to real only after minimizing extended loss. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Minimax honest expected length. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Extended chi-square, with infinity when absolute continuity fails. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Event-supremum total variation.
Definition (Lean source)
Off absolute continuity, the extended divergence is infinite. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The extended divergence agrees with the finite-real substrate when the density square is integrable. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Finiteness discharges both hypotheses needed by the finite-real chi-square API. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Laws on the unrestricted score space with locally continuous potential-mean versions.
Definition (Lean source)
The larger Gaussian observed-treatment identification class. The cutoff versions are means of binary potentials, so their range is explicitly recorded as [0,1]. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Observed law in the larger identification class. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The larger-class causal target. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The larger-class experiment uses the same finite product and independent seed. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Honest intervals on the larger identification class. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Extended minimax risk on the larger class, before its finite value is converted to real. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Minimax honest expected length on the larger class. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Pei and Shen Assumption 1Y, jointly nondifferential measurement error. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Pei and Shen Assumption 2C, positive score density on a cutoff neighborhood. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Pei and Shen Assumption 7, centered Gaussian measurement error. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.CitedGates 12 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The exact cited Legendre interface follows from the neutral Mathlib/Causalean proof. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The exact cited Hermite interface follows from the reusable neutral substrate. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Pei--Shen's score, real observed outcome, and measurement error; no binary or potential-mean-continuity restriction is built into this cited theorem's domain.
Definition (Lean source)
Source convention: treatment is assigned below the cutoff, Section 2, display (1). Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The continuous-score sharp-RD domain: a score density and a genuine local observed regression with finite left and right limits. These are the meanings of the conditional means and limit contrast in Section 2, not continuity assumptions on potential outcomes. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Assumption 1Y on the full real-outcome cited domain. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Assumption 2C requires positivity throughout an open cutoff neighborhood. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Assumption 7 specifies the actual centered Gaussian measurement error. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Pei and Shen (2017), cite:peishen2017, Section 2 and Section 4.1, Assumptions 1Y, 2C, 7 and Proposition 4(b), printed pp.4,18,28--29; https://arxiv.org/pdf/1609.01396. Identification of the real-outcome continuous-score sharp RD contrast, the left observed-regression limit minus the right limit under source display (1). The domain is not restricted to the benchmark's binary potentials or locally continuous potential-mean versions. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
Dong (2018), cite:dong2018-identification, Chapter 2 Section 2.2, Assumptions 8--9, printed p.49; https://etheses.lse.ac.uk/3756/1/Dong__essays-in-microeconometrics.pdf. Frozen bibliographic metadata, with zero logical consumers. Attested literal source: Assumption 8. f_{R*}(0) > 0 and E[Y_d|R* = r] is continuous at r = 0 for d = 0, 1. Assumption 9. R* and ε are continuous, and ε ⊥⊥ (Y, R*). Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
Dong (2018), cite:dong2018-inference, Chapter 2 Section 2.4, Assumptions 11,13 and Theorem 6, printed pp.59,61, PDF pages 69,71; https://researchonline.lse.ac.uk/id/eprint/134713/1/Dong_essays-in-microeconometrics.pdf. Pointwise Gaussian specialization of the actual observed-treatment local-linear estimator (2.3.3), with the source's defining averages and leading Lyapunov summand. This is a logical cited claim, with no consumers in this paper. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
Zhang and Karunamuni (2009), cite:zhangkarunamuni2009, DOI 10.1016/j.jspi.2008.10.021; publisher abstract, Section 1 introduction and estimator (1.3), Section 4 opening and Section 5 excerpt; https://www.sciencedirect.com/science/article/abs/pii/S0378375808004175. Frozen bibliographic metadata, with zero logical consumers. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.ClassicalFactInterfaces 2 declarations The cited Legendre and Hermite propositions are kept verbatim in this neutral interface module so their proofs can be imported without a cycle through the remaining cited-source declarations.
Classical polynomial fact interfaces
The cited Legendre and Hermite propositions are kept verbatim in this neutral interface module so their proofs can be imported without a cycle through the remaining cited-source declarations.
NIST DLMF (2026 access), cite:nistdlmf-legendre, Tables 18.3.1 and 18.6.1, equation 18.14.1 at zero Jacobi parameters; https://dlmf.nist.gov/18.3. Orthogonality, reflection symmetry, unit bound, and the normalized left endpoint. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
NIST DLMF (2026 access), cite:nistdlmf-hermite, equation 18.12.16 and Table 18.3.1, probabilists' Hermite row; https://dlmf.nist.gov/18.12.E16. The generating series and Gaussian-normalized orthogonality. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.Covariance 23 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The removable quotient has degree at most one less than its Chebyshev index. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Proof (Lean source)
Cubing the endpoint quotient gives the declared kernel degree bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Squaring the factorial derivative norm estimate gives the covariance summands. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The finite cubic-factorial variance series follows from endpoint mass and derivative bounds. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
With zero noise the finite inverse-heat operator is the identity polynomial. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Zero noise leaves the kernel mean and square unchanged under the Gaussian expectation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Nonnegative diagonal cubes are bounded by the cube of their finite sum. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The cubic-factorial series is bounded by the cube of the exponential series. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Below the endpoint resolution, the factorial series has an absolute exponential bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The diagonal-series argument controls variance by the two-thirds noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The intermediate cost exactly equals the two-thirds endpoint noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Below the compact-support interface, the public variance has the exact cost envelope. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A finite cubic-factorial series admits a logarithmic bound at a fixed degree scale. The exponential coefficient estimate is the uniform version of the factorial/logarithm estimate: each normalized coefficient at scale L is bounded by exp L. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On the compact-support branch, the endpoint cost is the degree times a logarithm. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Above the compact-support interface the logarithmic noise scale is at least one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The exponential cost factor is nonnegative in every endpoint noise branch. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The finite degree and cubic factorial yield the compact-support variance envelope. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The nonzero diagonal orthogonality integral supplies square integrability. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The constant Hermite mode extracts the Gaussian mean of every mode. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A finite Hermite series has mean equal to its constant coefficient. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Orthogonality removes all cross terms in the square of a finite Hermite series. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Exact inverse-heat mean, exact second moment, and absolute factorial covariance envelope. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
An absolute exponential cost envelope for the exact public variance. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DerivativeBounds 8 declarations Prefix-weight telescoping supplies the factorial gain in powers of the shifted-Legendre differentiation matrix; weighted Cauchy--Schwarz bounds its action.
Weighted increasing-chain bounds for differentiation
Prefix-weight telescoping supplies the factorial gain in powers of the shifted-Legendre differentiation matrix; weighted Cauchy--Schwarz bounds its action.
Summing prefix powers of the endpoint weights gains one power and its divisor. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The entries of the iterated derivative matrix, multiplied on the right. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Matrix entries are nonnegative, so deleting parity restrictions preserves an upper bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
After positive differentiation order only strictly increasing index paths survive. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Prefix-weight telescoping bounds all increasing chains, with one factorial per internal index. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The recursively multiplied entries act on coefficients exactly as repeated differentiation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Weighted Cauchy--Schwarz transfers a separable entry bound to the weighted coefficient norm. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every power of the Legendre differentiation action has the roadmap's factorial norm bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DerivativeChains 9 declarations The increasing-chain argument for factorial_derivatives: fixed-size subset products admit a factorial bound, shifted-Legendre weights sum to the square of the basis dimension, and squared matrix entries bound coefficient
Nonnegative chain weights for the factorial derivative bound
The increasing-chain argument for factorial_derivatives: fixed-size subset
products admit a factorial bound, shifted-Legendre weights sum to the square
of the basis dimension, and squared matrix entries bound coefficient-vector norms.
The identification of iterated polynomial differentiation with these chains
remains in Kernel.lean.
The constant and linear binomial terms are bounded by the full power. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Splitting fixed-size subsets according to a newly inserted element gives an exact recurrence for their weighted products. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Each increasing chain contributes once to a fixed-size subset sum; its factorial multiple is bounded by the full nonnegative power expansion. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Deleting restrictions on nonnegative chain weights bounds any retained collection of distinct-index products by the total weight power divided by its factorial. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The total shifted-Legendre endpoint weight is the square of the basis dimension. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The increasing-chain factor in the jth derivative matrix has the roadmap's factorial bound, even after arbitrary parity and endpoint restrictions. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The loss of one factorial index in the chain bound is absorbed by the extra factor two per derivative, as in the last inequality of the roadmap. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Bounding every squared matrix entry bounds its action by the squared Frobenius norm; this is the coefficient-vector estimate in the roadmap. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The separable endpoint weights in the chain entry bound give the full basis-dimension factor after summing the squared matrix entries. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DerivativeCoefficients 6 declarations The exact finite differentiation matrix acts on every degree-bounded polynomial expansion.
Coefficients of iterated shifted-Legendre differentiation
The exact finite differentiation matrix acts on every degree-bounded polynomial expansion. Iteration identifies all derivative coefficients before the chain bound and Parseval steps in the factorial derivative estimate.
Differentiation in the unnormalized shifted-Legendre basis, retaining parity. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The finite coefficient action of ordinary differentiation. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The derivative of each basis polynomial has exactly the matrix's column. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Differentiating a finite basis expansion applies the coefficient matrix once. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Iterating the matrix action gives every coefficient of the iterated derivative. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The canonical orthogonal coefficients reconstruct the polynomial itself. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DirectGaussianChannel 10 declarations Gaussian channel for the direct lower bound
Gaussian channel for the direct lower bound
Add independent Gaussian score noise while retaining the true-side arm and observed outcome. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The common Gaussian channel from the error-free observation to an observation at noise scale sigma.
Definition (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Gaussian error independence makes every noisy observed law a common Markov garbling of its error-free observed law. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Coordinatewise Gaussian randomization of an error-free sample. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the sample size and noise scale, this definition specifies the coordinatewise Gaussian observation kernel.
Definition (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Adding the same independent Gaussian noise coordinatewise cannot increase sample total variation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DirectTestingAssembly 3 declarations IID testing and two-point direct lower-bound assembly
IID testing and two-point direct lower-bound assembly
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The generic two-point calculation specialized to the legal direct bump alternatives. Its hypothesis is exactly the observed-product testing bound; the independent procedure seed is appended by experiment_tv_le. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The legal direct witnesses give the ordinary boundary-regression lower bound uniformly over every public noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DirectWitness 12 declarations The clipped linear bump has the global modulus required by the direct-reduction roadmap.
Direct bump witness legality
The clipped linear bump has the global modulus required by the direct-reduction roadmap. Its Bernoulli perturbations belong to the same latent model class at every noise scale, and their cutoff targets have the stated separation.
Both clipping operations contract distance, giving the global direct-bump Lipschitz bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full bump has oscillation at most one, including on the negative half-line. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The unit oscillation and Lipschitz bound interpolate to the roadmap's fractional modulus. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The small direct perturbations stay inside the benchmark's mean interval everywhere. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Scaling the bump cancels its Hölder resolution factor, giving a modulus at most kappa. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Each direct latent witness satisfies every model atom at every noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The direct witness's causal target is its signed cutoff perturbation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The direct alternatives have the target separation used by the two-point argument. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On its positive support the direct bump is exactly the declining linear segment. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The direct bump vanishes to the right of its positive support. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The direct bump has squared mass h/3 on its support, as used in DR.1. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating over the whole treated arm gives the same squared mass, with no tail truncation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DirectZeroInformation 23 declarations Noiseless direct-witness information bound
Noiseless direct-witness information bound
At zero noise, a treated observed cell is exactly its latent score cell. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
At zero noise, either control observed cell is the common latent score cell. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Density of the noiseless observed direct alternative with respect to Lebesgue measure on the score and counting measure on the two marks. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Likelihood ratio of the plus direct alternative against the minus direct alternative on the common noiseless support. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The noiseless direct alternatives have one-observation chi-squared divergence of the boundary-bump order h^(2*beta+1). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.DongInference 26 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
Dong's comparison allows real-valued potential outcomes.
Definition (Lean source)
Observed-treatment outcome in Dong's experiment. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Ordinary characteristic function, with the source's positive Fourier sign. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Fourier transform of the source's real kernel. Given the displayed inputs and assumptions, this definition specifies the stated object.
The source's iterated Fourier derivative. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Actual observed-treatment deconvolution weights, Section 2.3.1, printed p.53. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Arm membership uses true treatment status, as in the source. Given the displayed inputs and assumptions, this definition specifies the stated object.
Source's unmarked sample average. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Source's marked sample average. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Source's local-linear arm intercept, with exactly its displayed ratio. Given the displayed inputs and assumptions, this definition specifies the stated object.
Dong's observed-treatment contrast estimator (2.3.3). Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Genuine conditional potential means on a cutoff neighborhood. The reused regression predicate requires integrability of each potential outcome and of its mean representative on that neighborhood before its measurable-slice integral characterization applies. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The score density and well-defined local conditional potential means are pinned to the law. No unrestricted Bochner integral of a nonintegrable counterfactual is used as a version certificate. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Dong's cutoff target. Given the displayed inputs and assumptions, this definition specifies the stated object.
Continuous part of the observed regression after removing the cutoff jump. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Assumption 8: positive cutoff density and continuous potential means at zero. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Assumption 9, specialized to a fixed positive-scale Gaussian error. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Source's Assumption 11 on transforms, local smoothness, and real symmetric kernel moments. IID sampling and a known fixed error law are built into the experiment and weights. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
One-sided kernel moments and the population linearization constants. Given the displayed inputs and assumptions, this definition specifies the stated object.
Source's Section 2.8.1 leading summand P_{1,n,1}, with its displayed residual. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The source's logarithmic bandwidth at Gaussian supersmooth exponent two. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Assumption 13 at fixed Gaussian scale, with the exact leading-summand Lyapunov restriction. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Dong's IID latent sample experiment, with the observed estimator using only observable coordinates. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Actual estimator bias; no freely supplied centering sequence. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Actual estimator variance; no freely supplied normalization sequence. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Pointwise asymptotic normality, using the equivalent CDF convergence for a continuous Gaussian limit. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.EmpiricalMoments 6 declarations The IID second-moment calculation in FC.5 is unchanged by appending the independent procedure seed.
Seeded empirical-average moments
The IID second-moment calculation in FC.5 is unchanged by appending the independent procedure seed. The remaining population calculations concern a single observed summand, rather than the full sample experiment.
An IID empirical average retains its mean and centered second-moment bound when an independent probability seed is appended, as required in FC.5. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The observed law is normalized independently of the noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The expectation of a seeded IID average is its single-observation mean. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The population denominator expectation reduces to one observed weight. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Single-observation marked moments suffice for all centered marked-average moments under the actual seeded experiment; no sample-level bound is assumed. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Single-observation unmarked moments suffice for all centered denominator moments under the actual seeded experiment. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.EmpiricalPopulationBridge 28 declarations This file isolates the product-law reduction used by the single-observation calculations.
Population bridges for the finite certificate
This file isolates the product-law reduction used by the single-observation calculations. In particular, reflecting the Gaussian error for either arm does not change its law or its independence from the latent schedule.
The part of a latent observation independent of the measurement error. Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The first coordinate of the latent schedule is the latent score. Given the latent observation, this records the defining projection identity.
Formal statement
Proof (Lean source)
Pull an observed integral back to the latent law. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On the independent schedule/Gaussian product, the inverse-heat evaluation at the reflected compactly-supported score is square integrable. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Reflecting the proxy splits into the reflected score and the reflected error with the original nonnegative noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On an observation assigned to arm d, the observed binary mark is exactly the corresponding latent potential. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
The conditional-mean density is globally measurable even though the version itself is only controlled on the score support. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The finite measure obtained by weighting the latent law by a binary potential outcome. Given the displayed inputs and assumptions, this definition specifies the stated object.
The score pushforward of the potential-weighted latent law has density mu d * f. This promotes the eventwise mu_version axiom to a measure identity that can be integrated against arbitrary measurable weights. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The eventwise conditional-mean identity integrates against every measurable real score weight. Integrability is handled by the Bochner integral convention and can be strengthened separately when needed. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The ordinary score-density identity also integrates against every measurable real weight. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A score law with a Lebesgue density has no atom at the cutoff. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Apart from the null cutoff atom, true-side assignment is exactly membership of the reflected score in [0,1]. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The inverse-heat evaluation of one observed proxy is square integrable. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Both arm-weighted observed summands inherit square integrability from the unweighted inverse-heat proxy. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Reflection into either treatment arm preserves the standard Gaussian error marginal. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The same factorization with the schedule first, convenient for applying the Gaussian covariance identities as inner integrals. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Schedule-first Fubini reduction, matching the shape of exact_covariance. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Reflection sends either arm's compact score half to the common endpoint interval, with the cutoff discrepancy already absorbed by Lebesgue nullity. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Exact FC.1 population identity for the unmarked arm summand. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Exact FC.1 population identity for the marked arm summand. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.EmpiricalPopulationMoments 7 declarations
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.FrontierComparison 2 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
Matched minimax chains and honesty, retaining extended expectations of the observable procedures. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Constructed upper procedures and all-procedure lower witnesses give the matched minimax chains. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.FrontierRoot 2 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The constructed resolution is a root in the declared interval and is its only root there. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The scalar branch formulas and both interfaces have constants uniform in sample size and noise. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.FrontierSequences 4 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
Explicit eventually-in-size comparisons for shrinking and fixed noise, and exact direct sequences. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The beta-one shrinking-noise specialization holds at every declared sample size. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
The exact scalar formulas imply the shrinking-noise and fixed-noise asymptotic comparisons. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The beta-one example lies on the intermediate branch at every sample size. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.GaussianLikelihood 11 declarations The midpoint denominator comparison and absolute integrability of the signed Gaussian cross-kernel justify the Fubini step preceding the moment series ML.5.
Gaussian reference likelihood on the full proxy line
The midpoint denominator comparison and absolute integrability of the signed Gaussian cross-kernel justify the Fubini step preceding the moment series ML.5.
Dividing the global midpoint lower bound gives the pointwise ML.3 comparison. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The centered cross exponent stays below λ on the entire support square. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The absolute signed cross-kernel has an explicit finite Gaussian integral (ML.4). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Absolute cross-kernel integrability justifies signed Fubini over both latent coordinates and every real proxy value, with no discarded tails (ML.4--ML.5). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Multiplying the two compact latent integrals gives the square of the marked convolution, with the positive Gaussian reference denominator left outside. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The Gaussian-reference square is integrable on all real proxy values; this follows from the signed three-variable absolute-integrability bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Signed Fubini and the exact Gaussian cross-kernel give the compact double integral in ML.5, retaining every real proxy value. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating ML.3 reduces the actual likelihood square to the finite Gaussian-reference square, using the just-proved full-domain integrability. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The absolute cross exponent is uniformly controlled on the support square, so its exponential power series has a summable constant majorant. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Expanding the compact cross-kernel and integrating its summable majorant proves the exact centered-moment series ML.5. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
ML.3--ML.6 bound the full proxy-domain likelihood square by the retained factorial tail; no observed-law identities are assumed in this analytic step. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.Handle 2 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The endpoint handle records objects only; it carries no comparability or legality premises.
Definition (Lean source)
Endpoint precision handle over the constructed objects in Definitions 3--10. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.HeatAlgebra 13 declarations The transform is linear, its truncation is independent of an upper degree bound, and its action on every monomial has explicit descending-factorial coefficients.
Finite coefficient algebra for the inverse heat transform
The transform is linear, its truncation is independent of an upper degree bound, and its action on every monomial has explicit descending-factorial coefficients. These facts reduce the covariance roadmap's finite Hermite identity to monomials.
The inverse heat operator with an arbitrary public degree cutoff. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Iterated polynomial differentiation distributes over finite sums. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Scalar polynomial coefficients commute with iterated differentiation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every monomial derivative has its descending-factorial coefficient, including zero derivatives above the monomial degree. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Derivatives above any upper degree bound vanish. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The finite heat operator distributes over finite polynomial sums. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The finite heat operator commutes with scalar polynomial coefficients. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Enlarging a degree cutoff adds only identically zero heat terms. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The exact scalar action of inverse heat on a monomial is a finite sum with no convergence assumptions. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The public transform is exactly the general finite operator at the declared kernel degree. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Applying inverse heat coefficientwise gives the finite monomial decomposition prescribed in the covariance proof roadmap. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Evaluating the coefficientwise heat decomposition reduces the transform to its explicit finite descending-factorial sums. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The finite Hermite expression is likewise coefficientwise linear in the input polynomial. This is the other half of the monomial reduction. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.HeatHermite 7 declarations Coefficient comparison identifies inverse heat on monomials with Hermite polynomials.
Finite Hermite expansion of inverse heat
Coefficient comparison identifies inverse heat on monomials with Hermite polynomials. Affine substitution and the finite Taylor formula extend this identity to arbitrary polynomials, without any infinite-series interchange.
The even factorial splits into its even and odd double-factorial products. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Each nonzero Hermite coefficient equals the corresponding inverse-heat coefficient. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Unit-noise inverse heat maps a monomial to the corresponding Hermite polynomial. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Affine substitution multiplies the iterated derivative by the appropriate power of its slope. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The coefficients after affine substitution are the scaled finite Taylor coefficients. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Translation and scaling reduce inverse heat evaluation to the unit-noise operator. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A polynomial of bounded degree has the exact finite inverse-heat Hermite expansion. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.Kernel 25 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The removable endpoint value of the Chebyshev quotient is the squared index. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Multiplication by the score recovers the Chebyshev numerator, including zero. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The quotient has the sine-square representation used for endpoint concentration. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The sine addition formula bounds an integer frequency by its index times the base sine. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Proof (Lean source)
The quotient is uniformly bounded by the squared index throughout the latent arm. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Away from zero the quotient is bounded by the reciprocal score. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On the endpoint window, Jordan's sine inequality gives a squared-index lower bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The nonnegative cubed endpoint quotient has strictly positive normalization for every positive index. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating the endpoint window gives the normalization lower bound from the roadmap. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The endpoint kernel has unit mass because its cubed quotient normalization is nonzero. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Normalization converts the quotient bound into a uniform squared-index kernel envelope. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Unit mass and the uniform kernel envelope give its square-mass bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The reciprocal-score quotient bound and normalization give the cubic kernel tail. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Splitting at the squared-index resolution bounds the endpoint bias moment. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Positive normalized endpoint kernels and their bias and square-mass bounds. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The odd-parity Legendre derivative weights have the exact endpoint total. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The cited unit bound and derivative expansion imply the sharp endpoint derivative bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Derivative expansion with the odd parity restriction, and its endpoint bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Finite shifted Legendre expansions have the diagonal square integral prescribed by orthogonality. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Orthogonal expansion gives Parseval's identity for every degree-bounded real polynomial. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Parseval identifies the square mass of every iterated derivative with the weighted squared norm of the iterated differentiation coefficients. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The parity-restricted derivative expansion has exact square mass twice its endpoint weight. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The Legendre coefficient matrix and weighted Cauchy--Schwarz bound the first derivative square mass. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The first-order case of the factorial bound follows from its Legendre square-mass estimate. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Factorial gain in the interval square-integral derivative bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.LegalRegularity 5 declarations Clamping to the polynomial interval preserves the derivative-based Lipschitz bound.
Full-domain regularity of the tapered Legendre extension
Clamping to the polynomial interval preserves the derivative-based Lipschitz bound. The unit bound and that Lipschitz bound give the required fractional seminorm.
The endpoint continuation is evaluation at the clamped, rescaled argument. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Clamping the argument puts it in the polynomial's unit interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Proof (Lean source)
The continuation retains the polynomial's uniform unit bound across both seams. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The polynomial derivative bound extends across both constant pieces by clamping. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The unit and Lipschitz bounds imply the full-domain Hölder bound at every legal exponent. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.LegendreBasis 17 declarations Polynomial spanning, orthogonality, and integration by parts for the endpoint witnesses.
Shifted Legendre basis and derivative coefficients
Polynomial spanning, orthogonality, and integration by parts for the endpoint witnesses.
The usual forward shifted Legendre polynomial. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the Legendre degree, Legendre evaluation is continuous on the real line.
Formal statement
Proof (Lean source)
Affine substitution transfers cited Legendre orthogonality to the unit interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Real coefficient versions of the reversed shifted Legendre polynomials form a polynomial sequence, with the polynomial at index j having degree j. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
Reflection relates the polynomial sequence to the forward shifted Legendre functions. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Cited Legendre orthogonality and the polynomial-sequence spanning theorem make any polynomial of degree below j orthogonal to the jth shifted Legendre function. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the Legendre degree, shifted Legendre evaluation is differentiable on the real line.
Formal statement
Proof (Lean source)
Orthogonal projection reconstructs every polynomial of degree below the cutoff. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A real polynomial realizing the forward shifted Legendre function. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The two orientation signs cancel in the forward polynomial evaluation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Multiplying by the nonzero orientation sign preserves degree. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Differentiation lowers the forward polynomial degree strictly below its index. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The forward polynomial derivative is the ordinary function derivative. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The cited reflection symmetry and left endpoint fix both shifted endpoint values. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The endpoint term selects exactly the odd derivative modes. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integration by parts removes the lower-degree differentiated mode and leaves the parity-selected boundary coefficient of the forward Legendre derivative. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Expansion of the lower-degree derivative in the orthogonal shifted basis. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.LegendreBlock 18 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The initial segment of odd weights has square total mass. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The Legendre block normalizer is its total positive weight. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Proof (Lean source)
Endpoint signs cancel in the normalized Legendre block. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The taper vanishes at the right endpoint. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
The cited Legendre unit bound controls the tapered block on the whole unit interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The legal continuation retains the normalized cutoff value. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The explicitly constructed alternative has the displayed cutoff effect. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Opposite Bernoulli perturbations have twice the positive cutoff amplitude. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The unnormalized Legendre block before the endpoint taper. Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the polynomial degree, the finite Legendre block is continuous on the real line.
Formal statement
Proof (Lean source)
Orthogonality leaves precisely the sum of odd weights in the squared block integral. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The normalized untapered block has squared mass equal to its inverse normalizer. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Tapering the normalized block cannot increase its squared mass on the unit interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the polynomial degree, the untapered finite Legendre block is differentiable on the real line.
Formal statement
Proof (Lean source)
The untapered normalized block has absolute value at most one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The derivative of the untapered block is bounded by its total weight times the largest shifted Legendre derivative in the block. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Differentiating the endpoint taper gives the paper's uniform derivative bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The endpoint taper increases degree by at most one, so all prescribed monomials remain orthogonal to every Legendre mode in the block. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.LegendreFacts 6 declarations This module discharges the run's cited Legendre interface from Mathlib's shifted Legendre polynomials and Causalean's Jacobi and Legendre identities.
Exact classical Legendre facts
This module discharges the run's cited Legendre interface from Mathlib's shifted Legendre polynomials and Causalean's Jacobi and Legendre identities.
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The exact cited Legendre interface follows from Mathlib's shifted Legendre polynomials and Causalean's normalized Jacobi bound and beta calculus. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.LowerWitness 26 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
All cancellation and full-domain legality assertions for the actual alternative laws. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The factorial likelihood tail. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The factorial likelihood tail is absolutely convergent at every support and noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The convergent factorial likelihood tail is nonnegative. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The retained likelihood terms are bounded by the full exponential series. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Above an index whose successor dominates twice the argument, factorial terms are bounded by a geometric sequence with ratio one half. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Summing the geometric majorant bounds the retained likelihood tail by twice its first term; this is the first inequality in roadmap step CE.1. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full observed binary-mark likelihood bound, including absolute continuity and finite density square. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Positive noise yields a legal support width. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The noise-adapted support keeps the factorial-series argument below m/256, including the support saturation interface. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The public support's likelihood tail is at most twice its first retained term. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Inserting CE.1 into the full marked likelihood bound retains both binary marks and the whole real proxy domain. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The elementary logarithmic factorial estimate in CE.1, valid at every positive integer, follows by summing the logarithm's tangent-line inequality. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The last inequality in CE.1: factorial decay is written in exponential form. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CE.2 compares the retained factorial exponent to the uniform degree exponent. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The support choice and CE.1--CE.2 give the exponential likelihood-tail bound CE.3. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The block normalization converts support mass into one resolution factor. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CE.4 is the full marked information bound with its factorial degree exponent. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The saturated support implies the scalar threshold in CE.8. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
At saturated support, the compact cost formula is exact, including the saturation equality; this is the equality in CE.8. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The logarithm is monotone under the factor four in the likelihood argument, yielding the inequality in CE.8. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The unsaturated support fixes the likelihood parameter and the scale identity. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CE.5: the intermediate cost is exactly four times the degree. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CE.6--CE.7 bound the two compact-cost factors throughout unsaturated support. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CE.5--CE.7 compare both unsaturated cost branches to the likelihood degree exponent. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The optimized one-observation extended information envelope. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.MarkedCells 9 declarations The full continuation restricts to the compact block on the treated arm.
Treated-cell convolution formulas for the actual witness probabilities
The full continuation restricts to the compact block on the treated arm. Applying Gaussian convolution to the witness success and failure probabilities gives ML.1, and the existing two-cell integral bound supplies ML.2 for these convolutions.
On the treated arm the full continuation has exactly the compact convolution. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Convolving the actual success probability gives the first treated cell of ML.1. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Convolving the failure probability gives the second treated cell of ML.1. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The two treated-cell convolutions induced by the actual witness probabilities. The factor one half is the uniform latent score density. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Both actual treated-cell convolutions have the displayed ML.1 form. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The actual minus-cell convolutions stay strictly positive everywhere. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Summing the squared differences over both actual treated cells gives precisely the integrand already bounded in ML.2. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The sum of the actual treated-cell likelihood contributions is integrable on the whole real proxy line. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
ML.2 now applies to the convolutions of the actual witness probabilities, with both outcomes summed and no restriction on the real proxy domain. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.MarkedConvolution 36 declarations The first marked-likelihood step bounds the signed perturbation by the positive Gaussian mixture on every real proxy value.
Full-domain integrability of the marked Gaussian likelihood
The first marked-likelihood step bounds the signed perturbation by the positive Gaussian mixture on every real proxy value. Fubini and the normalized Gaussian mass then make the density-square ratio integrable without trimming proxy tails. Centered-moment cancellation and Cauchy--Schwarz bound the convergent moment series by the factorial tail used in the second likelihood inequality.
The paper density is the centered Mathlib Gaussian density at variance σ². Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the Gaussian scale, the density is continuous in its real argument, including at zero scale.
Formal statement
Proof (Lean source)
Every value of the Gaussian density is nonnegative. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Positive noise gives a strictly positive Gaussian density everywhere. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every translated Gaussian density is integrable over the whole proxy line. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A translated positive-scale Gaussian density has total mass one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The treated Gaussian mixture is positive at every real proxy value (ML.1). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Fubini and Gaussian normalization give full-domain mixture integrability. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The legal block bound dominates the signed mixture by the treated mixture (ML.1). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the arm width, noise scale, and polynomial degree, integrating the marked kernel over the fixed latent arm preserves strong measurability.
Formal statement
Proof (Lean source)
Given the noise scale, integrating the Gaussian kernel over the treated arm preserves strong measurability.
Formal statement
Proof (Lean source)
The domination |u| ≤ q gives u²/q ≤ q and full-domain integrability (ML.2). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Both Bernoulli cells retain at least one eighth of the unmarked density (ML.1). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Adding the two outcome cells gives the factor sixteen in ML.2. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full-domain treated-cell square ratio is integrable, without proxy truncation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating both outcome-cell contributions gives the full-domain ML.2 bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The paper's perturbation amplitude satisfies the cell-denominator condition. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
ML.2 for the actual witness amplitude, retaining both binary cells and all proxy values. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every polynomial of the canceled degrees is orthogonal to the legal block. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Changing scale preserves the canceled monomial moments on the full support. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Centering does not change the cancellation order (ML.5). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Scaling the block's squared-mass bound gives its support-width factor (ML.6). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every centered power has the compact-support squared-mass bound used in ML.6. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Cauchy--Schwarz on the complete latent support, with continuous integrands. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The centered moments obey the squared-mass estimate ML.6 at every order. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Normalizing ML.6 by the Gaussian variance and factorial gives each likelihood-series term. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Cancellation and ML.6 make the exact centered-moment series convergent and bound it by the retained factorial tail, before the Gaussian identity ML.5 is inserted. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Averaging the tangent inequality for the exponential gives a lower bound when the exponent has zero interval mean (the elementary Jensen step in ML.3). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The centered quadratic Gaussian log-ratio has zero mean on its support (ML.3). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Factoring at the local midpoint exposes the mean-zero exponent of ML.3. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The local Gaussian mixture is bounded below at every real proxy value (ML.3). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Restricting the unit mixture to the local support proves the global denominator bound, including the full real proxy line (ML.3). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Completing the square factors the product of two Gaussian translates (ML.4). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The positive reference density cancels in the square-completion identity. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The square-completed ratio is integrable on the entire proxy line (ML.4). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating the square completion gives the exact Gaussian cross-kernel (ML.4). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.MarkedDomination 8 declarations Interior Bernoulli probabilities bound the latent likelihood ratio.
Domination of the full marked witness laws
Interior Bernoulli probabilities bound the latent likelihood ratio. Measure products and the observation map preserve this domination, providing absolute continuity and square integrability on the entire observed space (ML.1–ML.2).
Given the noise scale, the true-side assignment and Gaussian proxy form a measurable observation map.
Formal statement
Proof (Lean source)
Interior success and failure weights dominate each other by a factor three. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Fibrewise bounded domination survives a composition product. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full latent witness, including both potentials and the Gaussian, is dominated. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Both alternative observation laws obey bounded domination at every noise scale. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Domination gives absolute continuity for the entire observed triple. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A uniformly dominated finite law has an integrable centered likelihood square. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full observed alternative likelihood square is integrable on all cells. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.MatchedFrontierLower 8 declarations This file rounds the scalar noisy resolution to the explicit cancellation witness grid and transfers its information bound to the product experiment.
Noise-adapted lower tuning for the matched frontier
This file rounds the scalar noisy resolution to the explicit cancellation witness grid and transfers its information bound to the product experiment.
The noise-adapted support is monotone in the integer degree. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Consecutive noise resolutions lose at most a factor four. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every positive target scale is eventually crossed by the explicit noise-resolution grid. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Minimal grid crossing at H/4096; it lies within a factor four of the requested scale once the scalar root is strictly below the noise level. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
At the rounded cancellation scale, the likelihood exponential absorbs the exact scalar root balance with a fixed numerical margin. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A small one-observation extended chi-square bound gives the testing constant required by two_point_transfer after n IID observations. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
In the genuinely noisy regime, cancellation alternatives attain a fixed multiple of the scalar frontier for both minimax criteria. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Combining the ordinary direct witness below the direct resolution with the cancellation witness above it gives a uniform scalar-frontier converse. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.MatchedFrontierUpper 6 declarations The public finite selector is compared with the scalar frontier using a rounded degree whose squared reciprocal is a fixed dilation of the scalar resolution.
Uniform upper tuning for the matched frontier
The public finite selector is compared with the scalar frontier using a rounded degree whose squared reciprocal is a fixed dilation of the scalar resolution.
Exponentiating the scalar root equation gives the exact balance identity. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Ceiling a number above one loses at most a factor two. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The rounded upper degree has a width between one quarter and one times the requested dilated resolution. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The rounded dilated degree remains in the public finite candidate set. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A dilation by at least (D+1)^2 absorbs the variance-envelope constant in the square-root cost scaling. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The public finite certificate is uniformly bounded by the scalar frontier. The constant depends only on the smoothness exponent (and on the two classical polynomial identities packaged by the cited gates). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.ObservedCellDensity 42 declarations This file derives the treated observed-cell law from the concrete Bernoulli product witness and the independent Gaussian error.
Observed-cell densities for the cancellation witnesses
This file derives the treated observed-cell law from the concrete Bernoulli product witness and the independent Gaussian error. The resulting density is the convolution already used by the marked-likelihood estimates.
Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The negative-score, fair-outcome latent cell, independent of the treated mark. Given the displayed inputs, this definition specifies the stated object.
Common observed density of either untreated outcome cell. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs, this definition specifies the stated object.
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.PopulationBias 7 declarations Positive normalized kernels preserve density and mean bounds, and the mean Hölder condition gives the population ratio bias in FC.2–FC.3.
Population endpoint-kernel bias
Positive normalized kernels preserve density and mean bounds, and the mean Hölder condition gives the population ratio bias in FC.2–FC.3.
A normalized positive endpoint kernel preserves pointwise density bounds (FC.2). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Reflecting either arm sends its unit interval into the full latent score interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Continuous latent versions stay continuous after restriction and arm reflection. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The FC.1 unmarked integral lies between one quarter and three quarters on either arm. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A positive density-weighted kernel average preserves the potential-mean range. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The density and Hölder envelopes imply the six-times-moment population bias (FC.3). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Each FC.1 weighted potential mean is interior and approximates its cutoff trace (FC.3). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.Procedure 35 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
Chebyshev polynomial normalized by its cosine identity. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The polynomial quotient fills the removable singularity at zero. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Normalized cube of the endpoint quotient. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Degree of the positive endpoint kernel. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Iterated ordinary polynomial derivative. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Finite inverse heat transform, with the exact factorial coefficients. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Marked arm average. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Unmarked arm average. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Denominator floor and ordinary projection onto the interior mean range. Given the displayed inputs and assumptions, this definition specifies the stated object.
Marked population mean. Given the displayed inputs and assumptions, this definition specifies the stated object.
Unmarked population mean. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Exact public bias moment. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Exact finite covariance cost. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The observable effect estimate includes the zero-degree fallback. Given the displayed inputs and assumptions, this definition specifies the stated object.
The public bias-aware radius includes the fallback. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Public finite cap. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Minimizers of the public radius over the finite candidate set. Given the displayed inputs and assumptions, this definition specifies the stated object.
A finite nonempty candidate set has a radius minimizer. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Smallest public minimizer, formed structurally from the finite set. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The exactly evaluable certificate. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Clipped lower endpoint. Given the displayed inputs and assumptions, this definition specifies the stated object.
Clipped upper endpoint. Given the displayed inputs and assumptions, this definition specifies the stated object.
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The endpoint quotient is nonnegative, including its removable endpoint. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Normalizing a nonnegative cube preserves nonnegativity even at degree zero. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The bias moment is nonnegative for every real smoothness exponent. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every public radius is nonnegative, including the fallback. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Clipping the two arm ratios keeps the estimated contrast in its target range. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Clipped interval endpoints are measurable and always ordered inside the target range. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The total connected closed interval, including the constant fallback interval. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The selected measurable estimate. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The selected interval procedure; its honesty is proved later. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Public finite selection returns the observable estimate and interval. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Extended worst risk of the selected procedure. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Extended worst expected length of the selected interval. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.Rate 19 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
Piecewise continuous endpoint noise cost. Given the displayed inputs and assumptions, this definition specifies the stated object.
Noiseless endpoint resolution. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
A supremum construction of the root, whose existence and uniqueness are proof obligations. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Endpoint frontier rate. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Rate and selected observable procedures. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Each branch of the public noise cost is nonnegative on its stated domain. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The two nonzero cost branches agree at the compact-support interface. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Gluing the explicit branches gives continuity on the positive resolution domain. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The compact branch decreases as resolution increases below its interface. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The power branch decreases on positive resolutions. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Branchwise comparisons and interface agreement give global monotonicity. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The power expression also holds at the direct-branch endpoint. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The compact expression agrees with the power expression at their interface. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On the power branch the multiplicative cost ratio is a two-thirds power. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
On the compact branch the logarithmic factor grows between zero and the square-root ratio. The bound log r ≤ r - 1 is the integrated upper derivative bound in the roadmap. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Multiplicative branch comparisons compose across an intermediate resolution. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Joining the two explicit branch estimates yields the full ratio bounds. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The lower ratio estimate gives dilation decay until the direct branch is reached. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Continuity, monotonicity and both scalar scaling inequalities. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.ScalarRootCompact 5 declarations Monotonicity, uniqueness, and uniform comparisons for the compact-branch scalar equation.
Compact scalar root analysis
Monotonicity, uniqueness, and uniform comparisons for the compact-branch scalar equation.
The left side of the compact scalar equation. Given the displayed inputs and assumptions, this definition specifies the stated object.
Above the compact interface, the compact scalar left side is strictly increasing. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The compact scalar equation has at most one solution above the compact interface. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A solution of the compact scalar equation is uniformly comparable to its explicit logarithmic proxy. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Raising a positive two-sided compact-scale comparison to the negative Hölder exponent reverses its inequalities and inverts the proxy. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.ScalarRootCore 13 declarations Existence, uniqueness, branch identification, and intermediate-branch bounds for the true-side measurement-error resolution equation.
Scalar root analysis
Existence, uniqueness, branch identification, and intermediate-branch bounds for the true-side measurement-error resolution equation.
Given the smoothness index, sample size, and noise level, the unique-rate-root condition requires the root to lie between the direct resolution and one, the scalar balance equation to hold, and no other point in that interval to solve it.
Definition (Lean source)
The exact intermediate-compact branch criterion. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The intermediate branch scalar equation. Given the displayed inputs and assumptions, this definition specifies the stated object.
The compact branch scalar equation. Given the displayed inputs and assumptions, this definition specifies the stated object.
The direct resolution is positive and at most one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The supremum construction is the unique root, derived from the piecewise noise cost. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Noise below the direct resolution leaves the scalar root at the direct rate. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.TwoPoint 10 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The common submeasure bounds the sum of extended absolute risks by separation times overlap. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Honesty at two targets and total variation at most one fifth force expected length at least three fifths of separation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The independent observed sample is a probability law. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Appending the independent uniform seed preserves probability normalization. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Appending the same independent seed cannot increase total variation. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Interior conditional-mean bounds put the target contrast in the half-unit interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A lower bound on the sum of two extended risks yields half that bound for their maximum. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The constant-zero estimator makes the extended minimax absolute risk finite. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full target interval is honest and makes the extended minimax length finite. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The two-point converse includes the independent random seed and all measurable decisions. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.Witness 46 declarations Helpers/Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Helpers/Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
Legendre block normalizer. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Tapered high-degree Legendre block. Given the displayed inputs and assumptions, this definition specifies the stated object.
Full-interval continuation of the lower perturbation. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The fixed numerical perturbation size. Given the displayed inputs, this definition specifies the stated object.
Definition (Lean source)
The signs index the plus and minus law. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Uniform latent score law. Given the displayed inputs, this definition specifies the stated object.
The uniform score density. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Independent conditional Bernoulli potentials and independent Gaussian perturbation. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Conditional means of the constructed witness law. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Uniform density facts, independent of the mean perturbation. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The uniform score construction has unit total mass. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The uniform score construction is supported on the latent interval. Given the displayed inputs, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A normalized Bernoulli mark preserves the base marginal, including endpoint probabilities. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Both conditional marks and the independent Gaussian leave the score marginal unchanged. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The conditional Bernoulli construction is a probability law. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Constructed scores stay in the latent interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The score marginal has the fixed uniform density. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating the successful Boolean mark over a base event recovers its probability integral. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Forgetting the independent Gaussian coordinate recovers the two-mark schedule law. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The specified Bernoulli probabilities are conditional potential means. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Continuous Bernoulli probability yields continuous conditional means. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Package the explicitly constructed measure and its versions, rather than an arbitrary witness. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Cancellation witness success probability. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The explicit coefficient formula gives the reversed Legendre left endpoint. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The block's positive odd weights sum to its displayed normalization. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Proof (Lean source)
Endpoint normalization follows directly from Mathlib's polynomial coefficients. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The continuation is polynomial evaluation at a clamped argument, including both seams. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the positive continuation width, matching endpoint values make the full continuation continuous across both seams.
Formal statement
Proof (Lean source)
Given the positive continuation width, affine Bernoulli perturbations inherit continuity from the full continuation.
Formal statement
Proof (Lean source)
The block normalizer is strictly positive, including at degree zero. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The cited Legendre unit bound controls the tapered block on the whole unit interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Clamping keeps the continuation within the Legendre block's unit bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The displayed scope makes the cancellation construction a continuous Bernoulli probability. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The actual cancellation alternatives, on their stated parameter domains. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Noise-adapted support width. Given the displayed inputs and assumptions, this definition specifies the stated object.
Noise-adapted endpoint resolution. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The direct local bump. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Direct witness success probability. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The direct extension is a continuous clipped linear function for positive width. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Clipping keeps the full direct extension between zero and one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Direct witness probabilities are valid under their stated parameter scope. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The actual direct alternatives, with the same Bernoulli and error construction. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Unmarked treated convolution density. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Signed marked convolution perturbation. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
Support-to-noise ratio. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.Helpers.WitnessModel 8 declarations The product construction supplies the Gaussian marginal and joint independence.
Model membership of the cancellation witnesses
The product construction supplies the Gaussian marginal and joint independence. The unit and Hölder bounds keep the conditional means inside the benchmark class.
The two-mark schedule law is a probability measure for valid Bernoulli probabilities. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The independent product Gaussian survives the coordinate rearrangement. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The Gaussian is independent of the score and both potentials jointly. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Legal widths and degrees give a positive endpoint resolution at most one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Extract the pointwise modulus from the established full-domain seminorm bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The small perturbation keeps the treated mean in the model's interior interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The perturbation amplitude cancels the resolution factor in its Hölder modulus. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
All five model atoms hold for each constructed cancellation alternative. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.TDirectReduction 9 declarations Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
At zero noise only derivative order zero contributes to the public variance. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Rounding a real degree at least one down loses at most a factor two, even for the small-sample range between one and two. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The direct degree balances the negative kernel-bias exponent and the square-root variance exponent at the same noiseless rate. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The rounded direct degree obeys the endpoint bias bound with a uniform factor four because the public smoothness is at most one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The zero-noise covariance formula and endpoint squared-mass estimate bound the public standard-deviation contribution at any degree below a. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Public minimization inherits the direct-RD noiseless order from the rounded balanced degree, using the positive endpoint kernel bounds. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A finite extended worst-risk bound for the selected estimator also bounds the real minimax risk, since the estimator belongs to the decision class. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
An honest selected interval is an admissible minimax competitor; its finite worst expected length controls the real minimax length. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The direct converse is uniform in all noise, and the selected procedures attain the noiseless order. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.TFiniteCertificate 26 declarations Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The denominator floor cannot increase error from a population denominator at least one quarter. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Projection onto the potential-mean range decreases error from any mean in that range. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The floored, clipped ratio obeys the certificate's samplewise eight/six error bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The abstract ratio inequality applies to the actual arm averages on every sample. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Simultaneous average errors and the two population bias bounds give the public error radius. This is the deterministic assembly of (FC.3)--(FC.4), before any probability bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The two ratio errors and population biases bound the effect error with each empirical error retained separately, so expectation can be taken before applying moment bounds. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Normalization prevents the endpoint kernel's squared integral from vanishing. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The derivative-order-zero term makes the public variance strictly positive at every noise scale, including zero; all remaining derivative terms are nonnegative. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Cauchy–Schwarz converts an empirical centered second-moment bound into an absolute first-moment bound on the normalized experiment (the probabilistic step of FC.6). Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Integrating the floored-ratio inequality and using all four empirical second moments proves FC.6, including samples with an empty treatment arm. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
A target in the parameter range remains covered after intersecting a centered interval with that range. This is the deterministic coverage step of the finite certificate. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Chebyshev at the public forty-times-variance threshold bounds one failure by 1/40. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The union bound for four measurable errors gives simultaneous control with probability 0.9. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The four empirical-average failure bounds and population bias imply finite-sample coverage. This assembles the probability and deterministic steps after FC.1 and FC.5 are established. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Intersecting the centered public interval with the target range can only shorten it. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The sample experiment is normalized, so a pointwise radius bound also bounds expected length. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Deterministic public selection preserves the uniform twice-radius length bound, including index zero. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The selected index minimizes the radius over the finite public candidate set. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The fallback candidate caps the selected certificate at one half. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The constant fallback interval covers every model target on every sample. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The zero estimator has risk at most the fallback radius, including an empty sample. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Public deterministic selection preserves positive-degree honesty and fallback coverage. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Uniform fixed-degree risk bounds imply the selected certificate's worst-case risk bound. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Finite-sample mean, risk and honesty certificates, followed by the uniform guarantees of selection. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.TPublishedClassConverseTransfer 17 declarations Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
A benchmark law has locally continuous potential-mean versions on an open neighborhood of zero. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Zero density outside the latent interval extends the set-integral version identity. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The same law, density and versions on the unrestricted score carrier. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The embedding inherits local density positivity and the observed-outcome error independence by applying the observation function to the latent schedule. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Inclusion preserves the target, observed law, and the whole seeded experiment. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The observation map is measurable, including its cutoff treatment coordinate. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Every larger-class observation experiment, including the seed, has unit mass. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Binary cutoff means put the causal contrast in the declared target interval. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The constant full interval is an admissible connected closed interval procedure. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
The full target interval covers every law of the larger class with probability one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The zero estimator bounds the extended minimax risk by one. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The full interval bounds the extended honest minimax length by two. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Honesty on the larger class implies honesty on the benchmark via the exact embedding. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Minimax absolute risk increases under target-preserving experiment inclusion. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Restricting honest procedures and enlarging the law class increases minimax length. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Scaling the independent standard error gives the three published error/density hypotheses. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Benchmark laws embed preserving the observed experiment and target; minimax values increase on the larger class, which receives only lower bounds. The Pei--Shen comparison is source provenance and has no role in constructing the embedding or proving minimax class monotonicity. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.TUniformFrontier 5 declarations Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
Complete theorem conclusion: constants are outside the sample-size and noise binders. Given the displayed inputs and assumptions, this definition specifies the stated object.
Definition (Lean source)
A comparison with a nonnegative target survives decreasing its lower constant and increasing its positive upper constant. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
The minimax chains permit a common smaller lower and larger upper constant. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
Exact branches and interfaces survive a common widening of their comparison constants. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
All-sample, all-noise endpoint frontier, with exhaustive branches, interfaces and sequence comparisons. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_RdTruesideNoiseFrontier_Research.TUniformFrontierResolution 1 declarations Law-level constructions and the obligations specified by the typed core.
True-side Gaussian measurement-error endpoint frontier
Law-level constructions and the obligations specified by the typed core. Cited logical facts are explicit inputs; bibliographic records have no logical consumers.
The uniform precision question is resolved by the same root, public minimization, and observable procedures. Given the displayed inputs and assumptions, the stated mathematical conclusion holds.