Formalization: Quotient-law Inference with Latent Treatment-effect Collisions
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs.
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Basic 86 declarations Core carriers, model assumptions, observable summaries, and finite-product sampling laws for the proxy effect-law collision frontier.
Core carriers, model assumptions, observable summaries, and finite-product sampling laws for the proxy effect-law collision frontier.
One full-data record. It uses the supplied parameters.
One observed record. It uses the supplied parameters.
For the supplied parameters, to Coordinates is given by its defining clause.
For the supplied parameters, to Coordinates is given by its defining clause.
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
Standard product Borel structure on the full-data real coordinates and finite coordinates. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
Single full-data records are measurable in the induced product Borel structure. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
Standard product Borel structure on the observed real coordinates and binary treatment. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
Generic probability-law carrier on a measurable space. Model membership is deliberately consumer-local rather than part of this carrier. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting.
Definition (Lean source)
Observed-coordinate map. @realizes (tuple T,X,Z,Y) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Obs map measurable: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed margin of a full-data law. @realizes (pushforward along O) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the supplied parameters, obs Law is Probability Measure is given by its defining clause.
Definition (Lean source)
Finite observed iid product law. @realizes (P_O tensor n) For the supplied parameters, the defined object is given by its defining clause.
For the supplied parameters, sample Law is Probability Measure is given by its defining clause.
Definition (Lean source)
For the supplied parameters, potential is given by its defining clause.
For the supplied parameters, latent Cell is given by its defining clause.
For the supplied parameters, latent Class is given by its defining clause.
For the supplied parameters, conditional Mean is given by its defining clause.
Definition (Lean source)
Latent-class mass. @realizes (P(U=u)) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Conditional potential-outcome mean. @realizes (E[Y(t)|U=u]) For the supplied parameters, the defined object is given by its defining clause.
Latent-class effect. @realizes (mu_1u-mu_0u) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Derived effect-support radius. @realizes (4 L sqrt(dz)/sigma0) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Conditional reference-proxy feature matrix. @realizes (cell conditional Z means) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Conditional target-proxy feature matrix. @realizes (class conditional X means) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
First canonical target-proxy vector. @realizes (first basis vector) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Fixed model-parameter domain used throughout the paper. The individual conjuncts are the load-bearing symbol-space realizations, rather than comments on an unrelated declaration. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Domain of the effect-separation scale used by labeled-coordinate results. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A real-valued function with a finite uniform envelope. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, Reference Proxy Separation is given by its defining clause.
Definition (Lean source)
For the ambient setting, Target Proxy Separation is given by its defining clause.
Definition (Lean source)
For the ambient setting, Causal Consistency is given by its defining clause.
For the ambient setting, Armwise Latent Ignorability is given by its defining clause.
Definition (Lean source)
For the ambient setting, Anchor Normalization is given by its defining clause.
For the ambient setting, Bounded Target Proxy is given by its defining clause.
For the supplied parameters, outer Product is given by its defining clause.
Definition (Lean source)
For the ambient setting, Bounded Proxy Product is given by its defining clause.
Definition (Lean source)
For the ambient setting, Bounded Outcome Proxy Product is given by its defining clause.
Definition (Lean source)
For the ambient setting, Latent Arm Positivity is given by its defining clause.
Definition (Lean source)
For the ambient setting, Proxy Rank Margin is given by its defining clause.
Definition (Lean source)
The uniformly conditioned causal VMW submodel. @realizes (ten model fields) It uses the supplied parameters.
Definition (Lean source)
Smallest positive pairwise effect gap, with ⊤ for a singleton support. @realizes (nearest positive effect gap) For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
For the supplied parameters, Gap Window is given by its defining clause.
For the ambient setting, Distinct Effects is given by its defining clause.
Definition (Lean source)
Gap-localized model membership. @realizes (model plus gap shell) It uses the supplied parameters.
Definition (Lean source)
Five-block observable summary space. It uses the supplied parameters.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
For target- and reference-proxy dimensions, summary coordinates collect the four observable moment matrices and the target-proxy mean vector.
Definition (Lean source)
For the supplied parameters, to Coordinates is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
For the supplied parameters, obs Arm is given by its defining clause.
Population observable moment summary. @realizes (armwise ZX moment) @realizes (armwise YZX moment) @realizes (unconditional X mean) @realizes (five-block tuple) For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
Sum of four operator norms and the Euclidean mean norm. @realizes (summary metric) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The summary loss is symmetric. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The summary loss obeys the triangle inequality. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
D s continuous: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete observable-summary node, bundling the five population moments with the stated continuous summary loss. It uses the supplied parameters.
Definition (Lean source)
For the ambient setting, observable Summary Data is given by its defining clause.
Definition (Lean source)
For the supplied parameters, observed Proxy Moment is given by its defining clause.
Definition (Lean source)
For the supplied parameters, observed Outcome Proxy Moment is given by its defining clause.
Definition (Lean source)
For the supplied parameters, latent Arm Weights is given by its defining clause.
Definition (Lean source)
For the supplied parameters, stacked Proxy Moment is given by its defining clause.
Definition (Lean source)
For the supplied parameters, arm Count is given by its defining clause.
For the supplied parameters, empirical Arm Matrix is given by its defining clause.
Definition (Lean source)
Total empirical summary, including the empty-arm zero branch. @realizes (armCount) @realizes (arm matrix) @realizes (weighted arm matrix) @realizes (sample mean) @realizes (five empirical blocks) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A supplied orthonormal signal basis and its spanning condition. @realizes (basis) It uses the supplied parameters.
Definition (Lean source)
Row space of the vertically stacked proxy moments. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The supplied orthonormal columns span the stacked proxy row space. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Compressed effect operator. @realizes (Penrose compressed contrast) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Left spectral anchor. @realizes (mX transpose V) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Right spectral anchor. @realizes (V transpose e1) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
All three constructions required by the compressed-operator definition, bundled together. It uses the supplied parameters.
Definition (Lean source)
The compressed effect operator and anchors attached to a model law and any orthonormal basis spanning its stacked proxy row space. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The labelled formula before validity is bundled. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Observed iid experiment. @realizes (set of model product laws) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Domain of a nominal confidence-set miscoverage level. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Domain of a generic high-probability tail level. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Domain of the simultaneous-concentration constant. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Simultaneous summary radius. For the supplied parameters, the defined object is given by its defining clause.
Summary radius pos: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summary concentration event. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.AmbientOperatorBridge 17 declarations Paper-local perturbation bounds for the ambient outcome-weighted Moore--Penrose contrast.
Paper-local perturbation bounds for the ambient outcome-weighted Moore--Penrose contrast. The bounds allow both row and column spaces to move and therefore remain valid across unrelated choices of signal coordinates.
The basis-free ambient effect contrast formed from the two observed arm summaries. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A single outcome-weighted Moore--Penrose product is stable under simultaneous movement of the proxy moment and outcome-weighted moment, assuming only equal rank and a singular margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ambient two-arm contrast is Lipschitz in the paper's five-block summary metric. This is the model-local product-triangle bridge from the moving-space Moore--Penrose estimate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mean-coordinate block is dominated by the full five-block summary distance. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a full-column-rank rectangular matrix, its Moore--Penrose inverse is a genuine left inverse. This is the cancellation used when the proxy factorization is restricted to the latent signal coordinates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The Moore--Penrose inverse of a product of two full-column-rank factors is the reverse product of their Moore--Penrose inverses. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cancelling a full-rank proxy factorization identifies the ambient outcome operator as the target-feature conjugation of the latent diagonal outcome means. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The model's basis-free ambient contrast is exactly the target-feature conjugation of the diagonal latent treatment effects. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every model-generated arm moment has exactly the latent rank. This packages the lower-rank consequence of the observed singular margin with the upper-rank consequence of the latent factorization, in the form required by the moving-space Moore--Penrose estimate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Model membership supplies, simultaneously in both arms, all quantitative hypotheses used by the ambient Moore--Penrose perturbation bound. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The model anchor makes the first ambient coordinate the all-ones right anchor in latent coordinates. This is the paper-local identity Bᵀ e₁ = 1 used by the spectral-law representation certificate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The canonical right anchor has Euclidean norm one whenever the ambient dimension is positive. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under positive latent-class mass and model membership, the observable target-proxy mean factors as the target-feature matrix times the latent-class mass vector.
Formal statement
Proof (Lean source)
An explicit functional-calculus formula for the target-feature factorization represents the labelled latent-effect law. This bridge uses only the mean and anchor identities and is insensitive to repeated effect values. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A model-specific diagonalization whose functional calculus has the target-feature formula automatically represents the model's raw quotient law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Once each model supplies its own bounded real diagonalization and representation certificate, the neutral collision-safe estimate and the moving-space Moore--Penrose bound assemble into a summary-metric modulus. The two diagonalizers are unrelated. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Model membership discharges every analytic side condition in the ambient certificate comparison. What remains for the paper-specific spectral step is exactly one independently chosen real diagonalization and representation certificate for each model law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.AtomicLaw 71 declarations Finite atomic probability laws and their finite-transport formulation of one-Wasserstein loss.
Finite atomic probability laws and their finite-transport formulation of one-Wasserstein loss.
A labelled representation of a probability law with at most k atoms in [-radius,radius]. Coincident locations are intentionally allowed; toMeasure aggregates them. It uses the supplied parameters.
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
The canonical Borel structure inherited from the two real coordinate vectors. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
The labelled representation of the unit point mass at zero. For the ambient setting, the defined object is given by its defining clause.
The simplex and support constraints making a representation a probability law. For the ambient setting, the defined object is given by its defining clause.
Atomic-law coordinates give a homeomorphism with the pair of finite real coordinate vectors. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The valid labelled atomic parameter space is compact. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The actual carrier of at-most-k probability laws supported in the stated interval.
Definition (Lean source)
Valid labelled laws inherit compactness from the compact valid coordinate set. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Delta zero valid: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The bundled unit point mass at zero. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
The probability measure represented by a finite atomic law. For the ambient setting, the defined object is given by its defining clause.
The represented measure of a bundled valid atomic probability law. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
A finite atomic law assigns a singleton its aggregate weight at that location. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
To measure is probability: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
Two valid finite representations denote the same law exactly when their represented measures agree. This removes all dependence on zero-mass slots and on how coincident atoms are labelled. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
Equivalent labelled laws have the same aggregate weight at every location. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, probability Law Setoid is given by its defining clause.
Definition (Lean source)
Extensional at-most-k probability laws: valid atomic representations modulo toMeasure. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Send a valid labelled representation to its extensional law. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
Extensional unit point mass at zero. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A finite representative used internally by explicit algorithms. Public equality remains measure equality through the quotient. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
The quotient of the compact valid labelled parameter space is compact in its coinduced topology. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The represented probability measure, independent of the chosen labelled representative. For the ambient setting, the defined object is given by its defining clause.
To measure eq of mk: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the ambient setting, the stated instance is given by its defining clause.
Definition (Lean source)
A finite coupling between two labelled atomic representations. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting.
Equivalent labelled probability laws have a coupling supported on equal locations. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Cost of a finite transport plan for absolute-distance loss. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
The coupling between equivalent representations has zero transport cost. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
One-Wasserstein distance, definitionally the infimum over the finite transport polytope. @realizes (infimum of finite transport costs) For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
Every feasible transport plan upper-bounds the infimal transport cost. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite transport polytope attains the infimum defining wass1. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite-transport Wasserstein loss is nonnegative on valid labelled laws. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Transposing a finite coupling proves symmetry of finite-transport Wasserstein loss. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A valid labelled law has zero finite-transport Wasserstein loss from itself. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite-transport loss vanishes between measure-equivalent valid representations. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A zero marginal forces every entry in the corresponding column of a nonnegative plan to vanish. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Glue two finite couplings through their common intermediate marginal, interpreting every zero-mass intermediate slice as zero. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The glued coupling costs at most the sum of the two input coupling costs. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Finite-transport Wasserstein loss satisfies the triangle inequality on valid laws. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A zero-cost nonnegative coupling has no mass between distinct locations. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A zero-cost coupling identifies the represented probability measures. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Wasserstein loss vanishes exactly between measure-equivalent valid representations. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Wasserstein loss is unchanged when its left labelled representation is replaced by an equivalent one. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Wasserstein loss is unchanged when its right labelled representation is replaced by an equivalent one. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Wasserstein loss is invariant under equivalent labelled representations in both arguments. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Wasserstein loss on extensional laws, computed using their finite representatives. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
Extensional Wasserstein loss is nonnegative. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Extensional Wasserstein loss vanishes on the diagonal. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Extensional Wasserstein loss is symmetric. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Extensional Wasserstein loss satisfies the triangle inequality. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Extensional Wasserstein loss separates quotient laws. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The raw metric structure whose distance is exactly extensional Wasserstein loss. Its induced topology is compared with the pre-existing quotient topology before an instance is installed. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The raw metric distance unfolds to extensional Wasserstein loss. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Couple common coordinate mass diagonally and the two residual marginals by their normalized product. This coupling is used only to compare nearby labelled representatives. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The coordinate coupling gives a continuous upper bound for Wasserstein loss. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Computing quotient Wasserstein loss on quotient constructors recovers the labelled loss. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The quotient projection is continuous from labelled coordinates to the raw Wasserstein metric topology. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The raw Wasserstein metric topology agrees with the original coinduced quotient topology. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The Wasserstein metric installed on quotient laws, with the original quotient topology. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For any two quotient laws, the installed metric distance equals their extensional one-Wasserstein loss.
Formal statement
Proof (Lean source)
Compact quotient laws are complete for their Wasserstein metric. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The (finite) set of locations carrying positive represented mass. For the ambient setting, the defined object is given by its defining clause.
Every distinct represented atom has at least the prescribed aggregate mass. @realizes (atom-floor class) @realizes (generic member of the atom-floor class) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Distance from a point to a finite set. For the supplied parameters, the defined object is given by its defining clause.
Atom-floor transport implication used by the cluster report. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.CitedGates 19 declarations Explicit cited logical gates used by the paper.
Explicit cited logical gates used by the paper.
A nominal handle for the parameter class and recovery regime defined in the published VMW paper. Its fields deliberately carry no local characterization: the cited gates below are the only bridge from these publication-level names to the conditions displayed in this development. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting.
Definition (Lean source)
The nominal published VMW parameter-class membership predicate. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A nominal record of quantitative margins imposed by a published model specification. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting.
The qualitative conditions listed in VMW Assumptions 1--2 and §4.2. In particular, this predicate has no numerical latent-positivity or singular-value margin parameter. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The published qualitative scope fixes neither this paper's latent-arm margin nor its proxy singular-value margin. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The local nearest-point wrapper, with the local top measurable-space instance adapted to the canonical Euclidean Borel instance used by the discharged Causalean theorem. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Brown and Purves (1973), Corollary 1, specialized to a compact Euclidean action space and an arbitrary jointly continuous loss: the argmin correspondence admits a Borel measurable selector. DOI 10.1214/aos/1176342510. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Virk, Mazaheri, and Wu (2026), arXiv:2607.10926v1, Assumptions 1--2 and §4.2. The cited correspondence says that the displayed qualitative proxy independences, consistency, armwise ignorability, full column ranks, and strict latent positivity are the published model scope; the source does not impose this paper's fixed quantitative margins. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The paper's quantitative model membership implies all of the qualitative conditions; the cited gate is used separately to identify those conditions with the published scope. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The qualitative simple-effect separation condition used by the published recovery regime. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The full-column-rank requirement called Assumption 2 in the cited VMW paper. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The strict latent positivity requirement used by the cited VMW recovery theorem. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The nominal proposition called Assumption 4 in the published VMW paper. Its mathematical content remains attached to the publication handle rather than being replaced by an arbitrary proposition chosen by a consumer. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The positive-dimensional domain on which the cited VMW model and recovery statements apply. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The columns form a population top-k right singular basis of the stacked proxy moment. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The law-level content of VMW Assumption 4: admissible positive dimensions, finite positive envelopes for the target proxy and the two proxy products, positive marginal treatment-arm probabilities, and a positive population singular-value margin. Sample-size and confidence-level conditions belong to the recovery theorem, not to this predicate. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The nominal published Theorem 7.2 recovery-regime membership predicate. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The theorem-level part of published VMW Theorem 7.2, kept separate from both population-law predicates. The universal constants are outermost. For the published estimator, the displayed sample-size and radius conditions imply one event of probability at least 1 - eta on which the treatment effects, anchor-normalized feature columns, and simplex-projected mixture weights obey their three simultaneous bounds. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Virk, Mazaheri, and Wu (2026), arXiv:2607.10926v1, Assumption 3 and Theorem 7.2. The cited recovery regime remains inside the standing Assumption 1 proxy-separation, consistency, and armwise-ignorability conditions and the anchor normalization; it additionally requires Assumption 2, strict latent positivity, Assumption 4, and spectral separation. Theorem 7.2 separately quantifies the sample size and confidence level, imposes its displayed sample-size and radius conditions, applies its stated estimator, and gives simultaneous high-probability bounds for the effects, anchor-normalized feature matrix, and simplex-projected mixture proportions. None of those theorem-level data is a field of either population-law predicate below. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ClusterBounds 10 declarations
Cluster effect gap nonneg: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Cluster effect gap le support distance: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster effect gap le external gap: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster effect gap to real pos of external ne top: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster singleton width from external: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster mass mem unit interval: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster mass eq one of support subset: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster mass gap cost: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster candidate mass error: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster deterministic report: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ClusterGeometry 17 declarations
Cluster support nonempty: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster support eq of measure equivalent: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster dist to finset attained: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster dist to finset nonneg: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster dist to finset le of mem: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster linked symmetric: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster component of mem self: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster component of subset support: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster component of eq of connected: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster component of eq of linked: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster component eq component of of mem: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster components partition support: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster association partition: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster extrema contain and width: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster external gap le cross: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster external gap nonneg: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Cluster external gap to real pos: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ClusterTransport 2 declarations
Test mass identity: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Test mass gap: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.Concentration 1 declarations Uniform concentration of the finite-product observable summary.
Uniform concentration of the finite-product observable summary.
The five-block empirical summary concentrates uniformly, including the empty-arm event. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ConcentrationCore 19 declarations Scalar concentration, ratio stability, and deterministic summary bounds.
Scalar concentration, ratio stability, and deterministic summary bounds.
For the proxy and outcome dimensions, the finite coordinate type for an observed summary enumerates matrix, mean, and treatment-probability coordinates.
For the proxy and outcome dimensions, observed-summary coordinates form a finite type.
Definition (Lean source)
For the supplied parameters, summary Coord Stat is given by its defining clause.
Definition (Lean source)
For the supplied parameters, summary Coord Scale is given by its defining clause.
Definition (Lean source)
Product hoeffding: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summary coord stat measurable: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summary coord stat ae bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summary coord stat integral: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summary coord stat arm sample mean: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summary coord stat matrix sample mean: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, population Arm Coord is given by its defining clause.
Definition (Lean source)
Empirical arm matrix entry error: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Emp summary error of small deviations: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Abs fin average le: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Empirical arm matrix entry bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Emp summary error on support: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Measurable set summary coord support: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Sample summary coord support ae: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summary coord deviation probability: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ConditionalMomentAdapters 14 declarations Paper-local adapters from the model's conditional-mean assumptions and almost-sure coordinate bounds to normalized restricted moments.
Paper-local adapters from the model's conditional-mean assumptions and almost-sure coordinate bounds to normalized restricted moments.
Every entry of a rectangular matrix is bounded by its Euclidean operator norm. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Anchor normalization converts the observable outer-product envelopes into coordinatewise bounds for both proxies and the observed outcome--reference-proxy product. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clamp a real value to the interval [-R, R]. For the supplied parameters, the defined object is given by its defining clause.
Measurable clamp real: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Abs clamp real le: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clamp real eq self: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
An a.e.-bounded measurable scalar has a globally bounded measurable clamped representative, and the two representatives have the same integral. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clamping an a.e.-bounded coordinate on a cell does not change its restricted integral. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Clamping an a.e.-bounded coordinate on a positive cell does not change its normalized restricted integral. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Coordinatewise clamping gives a measurable, globally coordinate-bounded vector representative which agrees almost surely with the original vector when all coordinates obey the a.e. bound. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The paper's conditional mean is exactly integration under the promoted normalized restriction on a positive-mass cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reference-proxy separation supplies the promoted bounded-test factorization on each positive latent cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Target-proxy separation supplies the promoted bounded-test factorization on each positive latent class. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Armwise latent ignorability supplies bounded-test factorization of a potential outcome and the treatment indicator under each positive latent-class law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.GapFreeClosureAssembly 6 declarations Dense extension while preserving the paper's explicit dS control function.
Dense extension while preserving the paper's explicit dS control function.
For the supplied parameters, atomic Law Borel Space is given by its defining clause.
Definition (Lean source)
For the supplied parameters, atomic Law Polish Space is given by its defining clause.
Definition (Lean source)
For the supplied parameters, probability Law Polish Space is given by its defining clause.
Definition (Lean source)
For the supplied parameters, law Modulo Opens Measurable Space is given by its defining clause.
Definition (Lean source)
For the supplied parameters, law Modulo Borel Space is given by its defining clause.
Definition (Lean source)
Exists unique extension with control: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.GapFreeModulusBridge 5 declarations Paper-local bridges from the radius-indexed quotient-law carrier to the neutral collision-safe finite-atomic Wasserstein substrate.
Paper-local bridges from the radius-indexed quotient-law carrier to the neutral collision-safe finite-atomic Wasserstein substrate.
Forget the support-radius index while retaining the labelled atomic law. For the supplied parameters, the defined object is given by its defining clause.
Local validity supplies the positivity and normalization required by the neutral carrier. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The paper-local and neutral finite transport formulations compute exactly the same cost. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Quotient Wasserstein distance can be evaluated by the neutral substrate on any chosen representatives. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A Lipschitz map into the complete quotient-law space extends uniquely from a set to its closure. This packages the final completion step of the modulus argument independently of the model-specific operator construction. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.Inference 17 declarations The theoretical and computable confidence sets and the cluster-adaptive report.
The theoretical and computable confidence sets and the cluster-adaptive report.
Both confidence-set constructions at a fixed sample. It uses the supplied parameters.
Definition (Lean source)
The retained sharp summary-inversion image, independent of the computable outer set. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Confidence radius pos: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The original summary-inversion image and the separate computable Wasserstein outer set. @realizes (candidate law in Calg) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The finite transport-plan constraint representation of the computable outer set. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Confidence sets constrained representation: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, linked is given by its defining clause.
Definition (Lean source)
For the supplied parameters, component Of is given by its defining clause.
Definition (Lean source)
For the ambient setting, components is given by its defining clause.
Definition (Lean source)
For the supplied parameters, cluster Mass is given by its defining clause.
For the supplied parameters, associated Support is given by its defining clause.
For the supplied parameters, cluster External Gap is given by its defining clause.
Definition (Lean source)
Feasible objective values in the ordered-support/weight/transport representation of one cluster-mass endpoint. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Cluster endpoint extrema of representation: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
One cluster report at a fixed sample. It uses the supplied parameters.
Definition (Lean source)
Cluster report side conditions: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Computable cluster-adaptive report. @realizes (support and mass report) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.LatticeEstimator 60 declarations Finite-library and no-advice lattice estimator carriers.
Finite-library and no-advice lattice estimator carriers.
Polynomial aggregate spectral projectors and the positive law they determine at one feasible representative. The law is not supplied independently: its atoms and masses are definitionally the displayed projector formula. It uses the supplied parameters.
Definition (Lean source)
For the supplied parameters, effect Law is given by its defining clause.
Definition (Lean source)
Coordinatewise membership in one deterministic half-open summary cube. For the supplied parameters, the defined object is given by its defining clause.
For the supplied parameters, In Half Open Summary Cube is given by its defining clause.
Definition (Lean source)
For the supplied parameters, summary Lex Key is given by its defining clause.
Definition (Lean source)
For the supplied parameters, Summary Lex LE is given by its defining clause.
Definition (Lean source)
A faithfully well-formed class-dependent grid library of feasible representatives. It uses the supplied parameters.
Definition (Lean source)
For a finite representative library, its index type is finite.
Definition (Lean source)
The actual finite list scanned by the advised estimator. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
One exact-real comparison step: keep the closer representative, breaking distance ties by the prescribed lexicographic rank. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Exhaustive smallest-index nearest-library search, implemented by a fold over the actual finite library rather than supplied as an oracle field. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Successful exhaustive fold selection minimizes distance over the whole library and uses the stored lexicographic rank to break every distance tie. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Feasibility of a raw advised summary implies all spectral facts needed by the stored-summary rule. In particular, these are conclusions of the model assumptions, not certificates bundled into the advice. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The operation classes charged by the paper's fixed-dimensional exact-real model. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting. It uses the ambient setting.
Definition (Lean source)
For the supplied parameters, total is given by its defining clause.
Definition (Lean source)
The finite instruction type records arithmetic, comparison, singular-value, and root-isolation operations in the exact-real implementation.
Definition (Lean source)
Equality of primitive net operations is decidable.
Definition (Lean source)
For the supplied parameters, cost is given by its defining clause.
Definition (Lean source)
For the supplied parameters, add is given by its defining clause.
Definition (Lean source)
For the supplied parameters, net Trace Cost is given by its defining clause.
Definition (Lean source)
Result returned by the singular-value primitive at one feasible representative. Its basis, rank certificates, and threshold decision are the data produced by this execution, not separately supplied advice. It uses the supplied parameters.
Definition (Lean source)
Result returned by fixed-degree real-root isolation and projector-mass arithmetic after the singular-value execution. The validity certificate concerns exactly the atoms and projector masses returned by this execution. It uses the supplied parameters.
Definition (Lean source)
One execution of the result-bearing singular-value and root-isolation primitives. It uses the supplied parameters.
Definition (Lean source)
Exact-real primitives at fixed admissible dimensions and constants. The combined primitive threads feasibility into both singular-value thresholding and root isolation, so no root run can be requested at an arbitrary summary. It uses the supplied parameters.
Definition (Lean source)
A uniform provider of fixed-parameter exact-real primitives, requested only on the admissible core parameter domain.
Definition (Lean source)
Feasibility identifies the admissible positive parameter domain carried by its model law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact-real primitive carrier is inhabited: representative spectral data on every admissible summary supplies a combined fixed-parameter run. Under the stated setting, the stated conclusion holds.
Formal statement
Proof (Lean source)
The representative spectral datum computed by an exact-real spectral execution. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The trace is assembled from the two result-bearing primitive executions that produced the spectral output. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Execute the result-bearing singular-value and root-isolation primitives. No choice operator or precomputed spectral selector participates in this definition. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Instructions used to form all coordinates of the empirical summary. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Instructions used by the actual fold over the representative list. Each distance evaluates four fixed-dimensional operator norms, its scalar coordinate arithmetic, and one comparison. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The result and exact primitive trace of the finite-library program. It uses the supplied parameters.
Definition (Lean source)
The operationally linked exact-real program: form the summary, exhaustively scan the finite library, then run singular-value thresholding and fixed-degree root isolation only at the selected representative. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The advised finite-library estimator is the output of the explicit exhaustive-search and spectral program; the only advice is the representative-summary library. @realizes (nearest finite-library law) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The operation count is computed from the trace of the very execution producing the estimate. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A completed primitive run has the fixed five-operation spectral tail. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The operational program trace is definitionally linked to the selected primitive run. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On a successful exhaustive selection, the returned law is exactly the law produced by the result-bearing spectral run at that selected representative. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every result-bearing spectral execution returns a valid representative law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A concrete structured-lattice estimator interface. It uses the supplied parameters.
Definition (Lean source)
The exhaustive-search work count: one pass over the sample and one fixed-dimensional criterion evaluation for every enumerated lattice point. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
One point in the prescribed no-advice product lattice. It uses the supplied parameters.
Definition (Lean source)
For the supplied parameters, lattice Height is given by its defining clause.
Definition (Lean source)
For the supplied parameters, lattice Mesh is given by its defining clause.
Definition (Lean source)
The displayed constant C_lat from the structured-lattice construction. @realizes (explicit positive structured-lattice constant) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the supplied parameters, Threshold Recovers Matrix Dimension is given by its defining clause.
Definition (Lean source)
For the supplied parameters, Threshold Recovers Dimension is given by its defining clause.
Definition (Lean source)
Inverse gram sqrt exists: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The inverse positive square root of the Gram matrix used in the paper's polar factor. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The unique prescribed polar-factor basis G (G^T G)^(-1/2). For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Exact grid, polar-factor, conditioning, simplex-floor, and clipped-support constraints. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, structured Candidate Operator is given by its defining clause.
Definition (Lean source)
For the supplied parameters, empirical Compressed Operator is given by its defining clause.
Definition (Lean source)
For the supplied parameters, structured Lattice Criterion is given by its defining clause.
Definition (Lean source)
For the ambient setting, effect Law is given by its defining clause.
Definition (Lean source)
For the ambient setting, structured Lattice Lex Key is given by its defining clause.
Definition (Lean source)
For the ambient setting, Lex LE is given by its defining clause.
Definition (Lean source)
The estimator is exactly the first minimizer of the displayed H_n/q_n lattice, its candidate count is an actual exhaustive list size, and its runtime accounts for that search. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The explicit lattice-law output. @realizes (no-advice lattice estimate) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ModelRealDiagonalization 8 declarations Uniformly conditioned ambient real diagonalizations built from a model's thin target-feature singular-value decomposition and an orthonormal kernel complement.
Uniformly conditioned ambient real diagonalizations built from a model's thin target-feature singular-value decomposition and an orthonormal kernel complement.
For the supplied parameters, Thin Signal Factorization is the stated data structure.
Definition (Lean source)
For the supplied parameters, thin Signal Factorization is given by its defining clause.
Definition (Lean source)
Transpose mul self: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, forward is given by its defining clause.
Definition (Lean source)
For the supplied parameters, backward is given by its defining clause.
Definition (Lean source)
Forward mul backward: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Backward mul forward: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, linear Equiv is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ModelSpectralCertificate 2 declarations The model-local bounded real-diagonalization certificate used by the gap-free modulus.
The model-local bounded real-diagonalization certificate used by the gap-free modulus.
Target feature entry bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Model real diagonalization certificate: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ModelSpectralConstruction 32 declarations Ambient real diagonalizations and uniform finite-dimensional conditioning bounds built from the model's thin target-feature singular-value factorization.
Ambient real diagonalizations and uniform finite-dimensional conditioning bounds built from the model's thin target-feature singular-value factorization.
For the supplied parameters, Ambient Extension is the stated data structure.
Definition (Lean source)
For the supplied parameters, ambient Extension is given by its defining clause.
Definition (Lean source)
For the supplied parameters, ambient Eigenvalue is given by its defining clause.
Definition (Lean source)
Ambient eigenvalue signal: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Ambient eigenvalue nonsignal: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, eigenbasis is given by its defining clause.
Definition (Lean source)
Forward signal: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, factor Operator is given by its defining clause.
Definition (Lean source)
Factor operator mul signal eigenvectors: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Transpose mul ambient basis nonsignal: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Forward ambient basis nonsignal: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Factor operator eigenbasis: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, real Diagonalization is given by its defining clause.
Definition (Lean source)
Ambient eigenvalue comp: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Real diagonalization apply function: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Moore penrose inverse thin signal factorization: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Factor operator eq moore penrose: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Real diagonalization apply function moore penrose: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Euc norm le card mul bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, entry Norm Constant is given by its defining clause.
Entry norm constant nonneg: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Matrix norm le entry bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Orthonormal basis entry abs le one: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Entry abs le one: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Coord entry bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Forward norm bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Backward norm bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, condition Bound is given by its defining clause.
Definition (Lean source)
Condition bound nonneg: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Diagonalization condition number le: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Singular system right entry abs le one: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Thin signal factorization coord inv entry bound: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.NetLibraryCertificates 18 declarations Derived certificates for the advised finite summary library
Derived certificates for the advised finite summary library
For the proxy and outcome dimensions, the finite coordinate type for a stored summary enumerates its four matrix blocks and its target-feature mean coordinates.
For the proxy and outcome dimensions, equality of summary coordinates is decidable.
Definition (Lean source)
For the proxy and outcome dimensions, summary coordinates form a finite type.
Definition (Lean source)
For the supplied parameters, net Summary Coord is given by its defining clause.
Definition (Lean source)
Net summary coord ext: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Net summary coord card: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The half-open grid certificate bounds every advised library by a fixed polynomial in n. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every signal basis at a model summary supplies latent-effect diagonal coordinates and the corresponding left/right anchor coordinates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Any valid complete projector enumeration gives the same extensional law as the positive diagonal-coordinate law, even when eigenvalues collide and the list contains dummy slots. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
An arbitrary result-bearing primitive run at a feasible summary denotes its model quotient law; no canonical choice of signal basis or root enumeration is assumed. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exhaustive finite fold is Borel measurable, and hence so is the law returned by the result-bearing program. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Net trace cost total eq length: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Exact trace accounting bounds the program work by the summary scan, the exhaustive library scan, and the fixed five-operation spectral tail. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact trace accounting and the grid-cardinality certificate combine into the displayed polynomial work bound with one class-dependent positive constant. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Net program selected eq nearest: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A rank-r comparison with last signal singular value at least s0 remains exactly r-dimensional after thresholding at s0 / 2 under any perturbation strictly below that threshold. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The quantitative model rank certificate gives the perturbation clause required by every stored representative summary. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Nearest-library selection plus the gap-free model modulus gives the deterministic advised estimator bound. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.NetLibraryExistence 4 declarations Construction of the advised finite summary grid.
Construction of the advised finite summary grid.
If the canonical mapped lists agree, the underlying finite-indexed maps agree.
Formal statement
Proof (Lean source)
If the canonical flattened coordinate lists agree, the underlying finite-indexed matrices agree.
Formal statement
Proof (Lean source)
The displayed lexicographic coordinate list determines a summary.
Formal statement
Proof (Lean source)
Given the latent lower bound, feature dimension bound, proxy dimension bound, radius bound, treatment positivity, treatment upper bound, noise positivity, noise upper bound, and positive mesh size, the bounded half-open coordinate grid supplies a finite feasible representative library.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ObservedLawAdapters 18 declarations Measurability and finite-partition adapters for transporting the full-data law to the observed law and decomposing treatment arms into latent cells.
Measurability and finite-partition adapters for transporting the full-data law to the observed law and decomposing treatment arms into latent cells.
The full-data treatment coordinate is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full-data latent coordinate is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed treatment coordinate is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A latent class is a measurable full-data event. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A latent-treatment cell is a measurable full-data event. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A treatment arm is a measurable full-data event. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A treatment arm is a measurable observed-data event. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed-law mass of an arm equals its full-data-law mass. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional means under the observed pushforward equal the corresponding full-data conditional means on the pulled-back event. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed treatment arm pulls back to the matching full-data arm. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
An observed-arm conditional mean can be evaluated directly under the full-data law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A full-data treatment arm is the disjoint union of its finitely many latent cells. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The real mass of an arm is the sum of the real masses of its latent cells. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Joint latent-arm positivity yields the paper's quantitative marginal arm bound. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every latent-treatment cell has strictly positive mass under a positive margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every treatment arm has strictly positive mass under joint latent-arm positivity. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each normalized latent-arm weight retains the original joint-cell positivity margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The diagonal matrix of normalized latent-arm weights is injective. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.ObservedMarginAssembly 13 declarations Assembly lemmas for the observed VMW margin proposition.
Assembly lemmas for the observed VMW margin proposition.
The full-data target-proxy coordinate map is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full-data reference-proxy coordinate map is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The full-data observed-outcome coordinate map is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each binary potential-outcome coordinate map is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed target-proxy coordinate map is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed reference-proxy coordinate map is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed outcome coordinate map is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A conditional mean on a treatment arm is the finite mixture of the conditional means on its latent cells. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reference-proxy separation factors each latent-cell proxy cross moment, using bounded clamped representatives of the proxy coordinates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Target-proxy separation makes the target-proxy conditional mean invariant across treatment arms within a latent class. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed armwise proxy moment has the latent finite-mixture factorization. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Entrywise conditional outer-product moments agree with the Bochner integral of the corresponding continuous-linear maps under the normalized cell law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A matrix of scalar conditional means is the Bochner conditional mean of the corresponding matrix-valued random element. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.OrderedMassStability 5 declarations Ordered masses of locally separated finite atomic laws
Ordered masses of locally separated finite atomic laws
Ordered aggregate masses depend only on the represented probability measure, despite being computed from a chosen finite representative. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Ordered masses descend to a measurable function on extensional atomic laws. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The canonical ordered-weight estimator is measurable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Below the localization radius, ordered atomic weights are Lipschitz in W₁ with the expected inverse support-gap factor. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Gap-stratum membership supplies the positive weights, injectivity, and numerical gap needed by the finite-atomic stability lemma. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.OutcomeFactorization 8 declarations Paper-local conditional-moment identities used in the outcome-weighted proxy factorization.
Paper-local conditional-moment identities used in the outcome-weighted proxy factorization.
Armwise latent ignorability identifies the potential-outcome mean on a positive latent-treatment cell with its latent-class mean. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Consistency replaces the observed outcome by the arm-specific potential outcome inside a latent-treatment cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Consequently the observed outcome mean on each latent-treatment cell equals the latent potential-outcome mean from the roadmap's factorization. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Target-proxy separation remains valid after conditioning on treatment because the separated second random element contains both the outcome and treatment coordinates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The cell target--outcome moment therefore factors into the target feature and the latent potential-outcome mean. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Reference-proxy separation factors the outcome-weighted proxy product on each positive latent-treatment cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Combining the two proxy separations, consistency, and latent ignorability gives the cellwise outcome-weighted factorization in equation (16). Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed armwise outcome-weighted proxy moment has the roadmap's finite-mixture factorization (16). Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.PathCertificates 21 declarations Paper-local finite-sum and model certificates for the factorization-preserving labelled path.
Paper-local finite-sum and model certificates for the factorization-preserving labelled path.
At zero displacement, the labelled path is exactly the collision witness with effect amplitude g / 2. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The base labelled-path measure is the already validated collision witness. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The undisplaced labelled path inherits uniformly conditioned model validity from the collision witness. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every atomic coefficient of the labelled path is nonnegative on the small rational neighborhood used by the lower-bound construction. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing every nuisance coordinate of the labelled path leaves its prescribed latent mass. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restricted event masses under the labelled path reduce to the defining finite sum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed support point indexed by the four visible Bernoulli coordinates. For the supplied parameters, the defined object is given by its defining clause.
Indicator that a visible Bernoulli support point is the requested observed record. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Singletons of the observed carrier are measurable in its induced Borel structure. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mass assigned by the labelled path to an observed singleton.
Every observed-cell mass is the explicit finite sum over the path atoms mapping to that cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite observed-cell formula after summing out the inactive potential outcome and the latent class. For the supplied parameters, the defined object is given by its defining clause.
Exact visible-cell displacement along the labelled path. The control arm is fixed, while each treated-arm cell changes by an explicit multiple of g * h. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform visible-cell displacement bound, with a numerical constant independent of the cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
An observed singleton mass is the sum of the sixteen visible Bernoulli-cell masses selected by that singleton. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform observed-singleton displacement bound along the labelled path. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every one of the sixteen visible cells of the base path has a uniform positive mass. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every represented observed atom of the base path inherits the uniform visible-cell floor. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For a path law, latent class, and integrand, restricting the finite path sum to that latent class selects exactly its atoms.
Formal statement
Proof (Lean source)
The labelled path has exactly the displaced latent masses prescribed in its construction. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ordered-mass target moves by exactly twice the absolute tangent displacement. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.PathFactorization 7 declarations Paper-local conditional-moment factorization certificates for the labelled path.
Paper-local conditional-moment factorization certificates for the labelled path.
Restricting the finite path sum to a latent-arm cell selects exactly that class and arm. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restricted integrals under the labelled path reduce to its defining finite sum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional means on a labelled-path latent-arm cell reduce to the corresponding finite sum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional means on a labelled-path latent class reduce to the corresponding finite sum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The labelled path preserves reference-proxy conditional independence. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The labelled path preserves target-proxy conditional independence. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The labelled path preserves armwise latent ignorability. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.PathKL 13 declarations Finite observed-carrier and chi-square certificates for the labelled path.
Finite observed-carrier and chi-square certificates for the labelled path.
KL divergence is bounded by chi-square divergence. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite sixteen-cell carrier of one observed labelled-path record.
The atomic law of the four visible Bernoulli coordinates. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The atomic law of the four visible Bernoulli coordinates. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Every singleton of the finite visible carrier has its explicit cell mass. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Mapping the finite visible carrier to observation records recovers the observed margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The visible atomic law has total mass one on the path domain. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every base visible cell has a uniform positive mass. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The displaced finite visible law is absolutely continuous with respect to the base law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed labelled-path law is absolutely continuous with respect to its base law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The labelled-path observed log likelihood ratio is integrable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The chi-square divergence of the finite visible path is quadratically bounded. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed one-record KL divergence along the labelled path is quadratic in g*h. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.PathLocalExperiments 8 declarations Gap and local-experiment certificates for the factorization-preserving labelled path.
Gap and local-experiment certificates for the factorization-preserving labelled path.
Multiplying a Bernoulli mass by its Boolean outcome and summing returns its mean. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A Bernoulli nuisance coordinate integrates out even with a trailing constant factor. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Potential-outcome means on the labelled path equal their construction probabilities. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two latent effects on the labelled path are exactly separated by g. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The nearest positive effect gap of the labelled path is exactly g. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both positive-mass effects on the labelled path are distinct. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every small-displacement path law lies in the gap-localized model. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed KL certificate promotes a small labelled path into the local experiment. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.PathModelCertificates 21 declarations Model-class and gap certificates for the factorization-preserving labelled path.
Model-class and gap certificates for the factorization-preserving labelled path.
A property true at every displayed path atom holds almost everywhere under the path law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The constructed reference feature has the normalized constant first coordinate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The path's latent-class conditional target means equal its constructed target feature. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The path's latent-arm conditional reference means equal its constructed reference feature. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The path obeys observed/potential-outcome consistency. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The path preserves the constant first target-proxy coordinate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target proxy remains inside the envelope along the path. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Proxy outer products remain inside the envelope along the path. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Outcome-weighted proxy outer products remain inside the envelope along the path. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The latent-arm cell masses are exactly the constructed arm weights. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every latent-arm cell retains the required one-tenth probability floor. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The operator norm of a two-by-two perturbation supported in the lower-right entry is bounded by the absolute value of that entry. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The operator norm of a two-by-two perturbation supported in the lower-left entry is bounded by the absolute value of that entry. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The undisplaced target feature has enough strict singular-value slack to absorb the small labelled-path perturbation. Under the stated setting, the stated conclusion holds.
Formal statement
Proof (Lean source)
The displaced lower-right target-feature entry remains within one fiftieth of its undisplaced value. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target feature retains the one-tenth singular-value margin throughout the small labelled-path neighborhood. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each undisplaced reference feature has enough strict singular-value slack to absorb the labelled-path perturbation. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The varying lower-left reference-feature entry remains within one fiftieth of its undisplaced value in either treatment arm. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Both reference features retain the one-tenth singular-value margin throughout the small labelled-path neighborhood. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The factorization-preserving path has the full proxy-rank certificate required by the uniformly conditioned model. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every sufficiently small labelled-path displacement remains in the uniformly conditioned model, uniformly over the displayed gap range. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.QuotientFunctionalCalculus 11 declarations Collision-stable finite functional calculus for quotient atomic laws.
Collision-stable finite functional calculus for quotient atomic laws.
The results deliberately use labelled diagonalizing coordinates only as a certificate. Repeated
eigenvalues are allowed: the represented law is passed to LawModulo, so splitting, merging, or
permuting equal-eigenvalue slots has no mathematical effect.
A square real operator together with diagonalizing coordinates. recover records the diagonal entry of basisInv * operator * basis; it is the only part of diagonalization needed by the perturbation bound, while expand is the usual reconstruction identity. It uses the supplied parameters.
The left-right spectral weight occurring in aᵀ f(D) c. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The matrix obtained by applying a scalar function to diagonalized spectral coordinates. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The bilinear anchor evaluation of a square matrix. For the supplied parameters, the defined object is given by its defining clause.
Left-right functional calculus is exactly integration against the labelled spectral weights: aᵀ f(D)c equals the weighted sum of f over the real spectrum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The labelled atomic law extracted from left-right functional calculus. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Positivity and normalization of the spectral weights turn functional-calculus coordinates into a valid atomic probability law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Public quotient-law constructor for a positive normalized left-right functional calculus. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Coordinatewise atom and weight perturbations control quotient Wasserstein loss. This lemma is independent of any eigengap and permits coincident atoms. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Gap-free quotient-law modulus in diagonalized operator coordinates. The right side contains only the recovered operator entries and the left-right anchor weights; no eigenvalue separation or choice of distinct spectral projectors occurs. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
With bounded diagonalizers and anchors, quotient Wasserstein loss has an explicit fixed-k gap-free bound in entrywise operator, anchor, diagonalizer, and inverse perturbations. The formula is uniform over all real spectra in the radius interval, including arbitrary repeated eigenvalues. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.QuotientLaw 2 declarations Validity and bundling of the quotient latent-effect law, after the observed-margin consequences needed for its support bound are available.
Validity and bundling of the quotient latent-effect law, after the observed-margin consequences needed for its support bound are available.
Quotient law raw valid: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Quotient latent-effect probability law, supported at the derived radius; its represented measure automatically aggregates coincident effect values. @realizes (valid probability law at latent effects) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.RealDiagonalizationBridge 9 declarations Paper-local conversion of a real eigenbasis into the matrix certificate used by the collision-safe functional-calculus substrate.
Paper-local conversion of a real eigenbasis into the matrix certificate used by the collision-safe functional-calculus substrate.
The orthonormal target-signal frame extends to an ambient orthonormal basis. This is the paper-local complement construction needed to add the zero eigenspace without choosing an eigengap or a basis inside any repeated signal eigenspace. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ambient orthonormal extension may be indexed by the standard ambient coordinates, with an explicit embedding recording which coordinates are the signal columns. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The matrix whose columns are the vectors of a Euclidean basis. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The inverse coordinate matrix of a Euclidean basis. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A basis matrix followed by its coordinate matrix is the identity. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coordinate matrix followed by its basis matrix is the identity. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A full real eigenbasis yields the substrate's two-sided real diagonalization certificate. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The functional calculus of the eigenbasis certificate is the expected conjugation formula. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A matrix agreeing with the scalar functional calculus on every vector of the eigenbasis is exactly the functional-calculus matrix. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.RepresentativeSpectralCertificate 2 declarations This file extracts from one model law a signal basis, its exact threshold rank, a real diagonalization of the compressed operator, and the two anchor-coordinate identities required by the generic collision-safe spectral
Model certificates for collision-safe representative spectra
This file extracts from one model law a signal basis, its exact threshold rank, a real diagonalization of the compressed operator, and the two anchor-coordinate identities required by the generic collision-safe spectral enumeration theorem.
The model-generated facts needed to turn a compressed operator into collision-safe polynomial projector masses. It uses the supplied parameters.
Definition (Lean source)
Every model law supplies a compressed real diagonalization in latent-effect coordinates, together with an observable signal basis and exact threshold-rank certificates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.Risk 12 declarations Decision rules and finite-sample risks used in upper and lower bounds.
Decision rules and finite-sample risks used in upper and lower bounds.
For the supplied parameters, Law Estimator is the stated data structure.
Definition (Lean source)
Probability-simplex constraint for labelled weight vectors. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the supplied parameters, Weight Estimator is the stated data structure.
Definition (Lean source)
Ordered masses are a Borel function of the labelled atomic coordinates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Ordered masses of a valid nonempty atomic law form a probability-simplex vector. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ℓ¹ diameter of the probability simplex is two. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, expected Law Risk is given by its defining clause.
Definition (Lean source)
For the supplied parameters, expected Weight Risk is given by its defining clause.
Definition (Lean source)
Risk of the specified ordered-mass estimator derived from the common repaired law estimator. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
One-Wasserstein loss between two bundled finite probability laws is nonnegative. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Integrating a Gaussian upper-tail envelope gives the corresponding mean bound. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A square-root logarithmic deviation inequality, uniform over confidence levels, implies a root-sample-size mean bound. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.SpectralSubstrate 16 declarations Rectangular finite-dimensional spectral helpers used by the proxy-effect-law construction.
Rectangular finite-dimensional spectral helpers used by the proxy-effect-law construction.
For a dimension, the Euclidean coordinate space is the real Euclidean space indexed by its d coordinates.
Definition (Lean source)
For numbers of rows and columns, the rectangular matrix space is the space of real matrices of that size.
For the supplied parameters, matrix CLM is given by its defining clause.
Definition (Lean source)
As a matrix varies, the associated continuous linear map varies continuously.
Formal statement
Proof (Lean source)
The singular value with zero-based index j. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The last signal singular value for a rows × k matrix. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Moore--Penrose formula for a full-column-rank rectangular matrix. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
A genuine real thin singular-value decomposition. Besides reconstruction, the right singular vectors are orthonormal and every retained positive singular direction satisfies both singular-vector equations; these conditions prevent the thresholded inverse from using an arbitrary rank-one reconstruction. It uses the supplied parameters.
Definition (Lean source)
Singular system exists: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A fixed real SVD of a rectangular matrix. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The genuine SVD-thresholded Moore--Penrose inverse sum_{sigma_j >= threshold} sigma_j^{-1} v_j u_j^T. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The Moore--Penrose inverse of an arbitrary real rectangular matrix. This local spelling delegates to the paper-independent substrate construction, which satisfies all four Penrose equations without a rank assumption. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Singular value variational lower: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Singular value weyl: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the full-column-rank domain, the canonical Moore--Penrose inverse agrees with the Gram formula used by the perturbation and moment-identity proofs. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Penrose perturbation: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeAnalysis 7 declarations This module collects the paper-local numerical and model consequences used by the explicit structured-lattice estimator.
Quantitative facts for the paper's structured lattice
This module collects the paper-local numerical and model consequences used by the explicit structured-lattice estimator. It is intentionally separate from the reusable collision-safe spectral substrate: the lattice height and its constants belong to this paper's construction.
The displayed lattice constant is strictly positive throughout the core parameter domain. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The prescribed inverse-Gram square root has the two defining square-root properties. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The prescribed polar factor has orthonormal columns whenever its asserted singular margin is positive. This is the algebraic fact used for every rounded grid basis. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
At every model-generated summary, thresholding at half the population margin retains exactly the k signal singular values. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The operator norm of a perturbation of the vertically stacked proxy block is bounded by the two proxy-block terms already present in the summary metric. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The stacked proxy perturbation is controlled without an extra dimension factor by the summary metric used in the theorem. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Any summary lying strictly inside half the population singular margin has exactly the same thresholded signal dimension. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeCardinality 2 declarations Polynomial cardinality of the structured lattice
Polynomial cardinality of the structured lattice
For fixed structural parameters, the exact encoder (and hence every prescribed duplicate-free search) has the paper's n^(D/2) cardinality, where D = dx*k+k^2+2*k-1. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The charged exhaustive-search runtime obeys the matching polynomial bound. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeComparator 1 declarations Assembly of the rounded structured-lattice comparator
Assembly of the rounded structured-lattice comparator
Assemble coordinate, polar, matrix, simplex, and effect rounding into one well-formed lattice point. The conclusion records the four approximation estimates used factorwise in (91). Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeEnumeration 13 declarations The lattice is encoded by its bounded integer grid coordinates and simplex numerators.
Finite enumeration of the prescribed structured lattice
The lattice is encoded by its bounded integer grid coordinates and simplex numerators. This gives the finite coordinate-key set used by exhaustive minimization without introducing a precomputed library of model summaries.
Integer coordinates large enough to encode a mesh-1/H scalar bounded by B.
Definition (Lean source)
For the latent dimension, feature dimension, mesh denominator, and bounds, the finite code type for one structured-lattice point stores its grid, coordinate, mass, and effect entries.
Definition (Lean source)
For the lattice dimensions and bounds, structured lattice codes form a finite type.
Definition (Lean source)
The encoder has exactly the paper's number of free mesh coordinates; the simplex contributes k-1 because its final mass is determined by the sum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The subtype of all well-formed points in the prescribed lattice is finite. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Coordinate keys which are realized by at least one well-formed lattice point. Passing to keys removes harmless duplicate grid bases having the same prescribed visible coordinates. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, structured Lattice Key Linear Order is given by its defining clause.
Definition (Lean source)
For the ambient setting, structured Lattice Key Finite is given by its defining clause.
Definition (Lean source)
For the ambient setting, structured Lattice Key Fintype is given by its defining clause.
Definition (Lean source)
Realized visible-coordinate keys inject into the integer encoder, so their cardinality is bounded by the encoder's exact free-coordinate product. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
There is a duplicate-free exhaustive enumeration of the well-formed lattice, ordered by the displayed lexicographic coordinate key. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Any certified duplicate-free exhaustive lattice search has no more candidates than the exact integer/simplex encoder. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A nonempty finite candidate family has a unique first minimizer: first minimize the displayed real score, then minimize the enumeration index among ties. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeFunctionalCalculus 19 declarations Collision-safe functional calculus for selected structured-lattice tuples
Collision-safe functional calculus for selected structured-lattice tuples
Extending an operator on an orthonormal signal frame by the identity on its orthogonal complement has norm at most the larger of the signal-block norm and one. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ambient diagonalizer induced by a thin signal factorization has condition number at most the product of the sharp signal/complement extension bounds. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Regard a well-conditioned structured tuple as a thin signal factorization of its reconstructed feature matrix. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Ambient diagonalization of the selected candidate operator, including zero on the orthogonal complement of the reconstructed signal space. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Under the paper's parameter domain, every selected structured-lattice diagonalizer has condition number at most the frozen sharp value 4 * sqrt k * L / sigma0. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The corrected right anchor changes the observed anchor only inside the selected signal space and makes the structured feature transpose evaluate exactly to the all-ones vector. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Structured feature transpose corrected anchor: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The corrected-anchor displacement is controlled by the selected anchor residual and the inverse coordinate margin, with no eigengap condition. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The selected labelled atomic law is represented exactly by its ambient collision-safe functional calculus at the reconstructed mean and corrected anchor. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A signal frame and a square coordinate factor with a positive singular margin determine the thin factorization used for the exact population tuple. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Exact ambient real diagonalization of a population signal tuple. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The exact population tuple has condition number at most the same frozen sharp value used for every selected lattice point. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Support membership of the signal atoms bounds the full ambient spectrum, including the zero eigenvalues on the orthogonal complement. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every selected structured-lattice diagonalizer has its full ambient spectrum in the prescribed effect interval. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact population tuple represents its labelled atomic law at the factorized mean and the uncorrected first-coordinate anchor. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The uncorrected first-coordinate anchor costs at most the spectral radius times its Euclidean anchor residual. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Local presentation wrapper for the attaining Kantorovich--Rubinstein potential used by the structured-lattice comparison. It records the normalization and the immediate uniform-bound consequence together with the substrate theorem.
Formal statement
Proof (Lean source)
Exact small-error Wasserstein estimate (paper display (102)) for the selected prescribed structured-lattice law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The small- and large-summary-error branches combine into the deterministic all-sample oracle bound with the frozen displayed lattice constant. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeMeasurability 11 declarations Borel measurability of the hard-threshold lattice criterion
Borel measurability of the hard-threshold lattice criterion
For the row and column dimensions, the measurable-space structure on rectangular matrices is the Borel structure.
Definition (Lean source)
For the row and column dimensions, rectangular matrices form a Borel space.
Formal statement
Proof (Lean source)
For the row and column dimensions, open sets of rectangular matrices are measurable.
Formal statement
Proof (Lean source)
For the row and column dimensions, the topology on rectangular matrices is second countable.
Formal statement
Proof (Lean source)
The genuine SVD hard-thresholded Moore--Penrose inverse is Borel measurable, including at the equality stratum of the convention tau ≤ sigma. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Empirical compressed operator measurable: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Structured lattice criterion measurable: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A finite score family with measurable coordinates has a measurable smallest-index minimizer. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The paper's exhaustive family admits a Borel, lexicographically first criterion minimizer on the five-block summary space. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The total empirical five-block summary is measurable, including the empty-arm branch. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The measurable structured search packages into the estimator interface, with the prescribed atom floor and exact exhaustive-search certificate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeNonempty 2 declarations The exhaustive search is nonempty for every core-domain parameter tuple.
A canonical point in the paper's structured lattice
The exhaustive search is nonempty for every core-domain parameter tuple. The witness uses the
first k coordinate vectors, the identity coordinate matrix, zero effects, and an integer-simplex
weight vector with the required floor.
The core-domain inequalities guarantee that the prescribed structured lattice is nonempty. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The core domain therefore supplies the exact exhaustive, lex-ordered search and its smallest-index empirical minimizer. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeOracle 9 declarations Deterministic oracle interfaces for the structured lattice
Deterministic oracle interfaces for the structured lattice
Exhaustive minimization compares the selected point with every well-formed lattice point, including points represented by a different harmless grid-basis witness. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The three coordinate/operator residual estimates combine to the displayed grid criterion constant, with no hidden multiplicative loss. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each of the three nonnegative residuals is bounded by the full criterion. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Structured lattice criterion mean le: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Structured lattice criterion anchor le: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Once a rounded well-formed comparator has the three frozen residual bounds at the empirical summary, exhaustive minimization transfers their exact c_grid sum to the selected point. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The mesh is no larger than the nominal root-n scale. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two probability laws supported in the same radius interval are at Wasserstein distance at most the interval diameter. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The large-summary-error branch of the deterministic oracle inequality. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticePolar 2 declarations Stability of the prescribed polar factor
Stability of the prescribed polar factor
The prescribed polar factor is Lipschitz at an orthonormal basis. The factor 2 is stronger than the factor 4 used in the frozen comparator estimate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The rounded grid and its prescribed polar factor satisfy the exact cV = 4 * sqrt (dx*k) comparator bound used in the frozen proof. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticePopulation 36 declarations Population tuple and ideal-to-summary residual bridges
Population tuple and ideal-to-summary residual bridges
The first r positive directions of the paper-local singular system, packaged for the neutral retained-SVD substrate. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Matrix obtained by retaining exactly the singular directions at or above a threshold. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Threshold singular truncation eq retained: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
An upper bound on every discarded singular coefficient controls the truncation error. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Discarding singular directions below a positive threshold changes the matrix by at most the threshold in operator norm. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Dimension recovery makes the thresholded singular truncation have exactly the target rank. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Truncation costs at most one cutoff radius in addition to the original perturbation. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Weyl's inequality transfers a last-signal singular margin to a nearby empirical matrix. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
If the comparison matrix has rank r and recovery retains the first r directions, the discarded empirical tail is bounded by the original perturbation radius. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Rank-aware truncation stays within twice the original perturbation radius of the rank-r comparison matrix. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Dimension recovery identifies the paper's thresholded reciprocal expansion with the neutral Moore--Penrose inverse of the retained rank-r SVD matrix. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The thresholded reciprocal expansion inherits any lower bound on the last retained singular coefficient. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
One arm of the empirical thresholded product is stable with the constants used by the frozen structured-lattice modulus. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two empirical arms obey the exact operator coefficient used in the frozen theorem. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each proxy-moment arm is dominated by the full summary distance. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under the dimension-recovery certificate, the custom thresholded SVD retains exactly the first k singular directions. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every direction discarded after the recovered rank is genuinely a zero singular direction of the rank-k comparison matrix. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A rank-r comparison with margin s0, perturbed by less than s0/4, is recovered by thresholding at s0/2. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Model membership specializes the two-arm perturbation certificate, including deriving threshold recovery rather than assuming it. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each latent-class conditional target-feature column retains the model's Euclidean envelope. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A matrix whose columns obey a common Euclidean envelope has the corresponding square-root-of-cardinality operator envelope. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coordinate factor has no larger operator norm than the original matrix because its left factor has orthonormal columns. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The transposed coordinate factor in the thin SVD inherits the certified lower singular margin of every retained direction. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The model supplies one common latent tuple whose mean, anchor, and ambient effect operator have exactly the factorizations used by the structured lattice criterion. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact population tuple admits a well-formed prescribed-grid comparator, retaining both its factorization identities and all four frozen rounding estimates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, population Operator Coefficient is given by its defining clause.
Definition (Lean source)
For the supplied parameters, structured Grid VConstant is given by its defining clause.
Definition (Lean source)
For the supplied parameters, structured Grid Mean Coefficient is given by its defining clause.
Definition (Lean source)
For the supplied parameters, structured Grid Anchor Coefficient is given by its defining clause.
Definition (Lean source)
For the supplied parameters, structured Grid Operator Coefficient is given by its defining clause.
Definition (Lean source)
For the supplied parameters, structured Grid Criterion Coefficient is given by its defining clause.
Definition (Lean source)
Model-specialized oracle inequality for the selected structured-lattice point, with the population perturbation and grid approximation contributions kept additively separate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The single frozen path coefficient used to dominate all three selected population residuals after adding the empirical-to-population bridge. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The selected grid point obeys the common paper-local path envelope against the population operator, population mean, and exact population anchor. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The population mean factorization leaves only the mean block of the summary distance. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Criterion-coordinate form of the exact population anchor residual. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeResiduals 9 declarations Factorwise residual estimates for the rounded comparator
Factorwise residual estimates for the rounded comparator
Matrix clm norm le one: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A positive square signal margin makes the ordinary nonsingular inverse available. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The inverse norm is the reciprocal of any certified lower singular margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The exact inverse perturbation estimate used by the frozen operator coefficient. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A finite probability vector has Euclidean norm at most one. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Factorwise perturbation of the observable mean reconstruction. Substituting cV = 4*sqrt(dx*k) gives exactly the frozen cm coefficient. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Factorwise perturbation of the anchor reconstruction. This is the exact frozen cb coefficient after substituting cV = 4*sqrt(dx*k). Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Factorwise perturbation of the similarity-transformed diagonal operator. The hypotheses expose the three analytic ingredients needed downstream: inverse stability, inverse norm control, and coordinatewise effect rounding. With KD = 4 * sqrt k * L * Ltau / sigma0, the conclusion is the frozen cD coefficient. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Signal-margin form of rounded_operator_factorization_residual_le, discharging all ordinary-inverse hypotheses from the ideal and rounded singular-value certificates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.StructuredLatticeRounding 17 declarations Coordinate rounding for the structured lattice comparator
Coordinate rounding for the structured lattice comparator
The prescribed height is positive on the core domain. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The height contains the reciprocal-mass ceiling required by largest-remainder rounding. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The height's explicit polar term makes the signal-basis mesh at most one quarter. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The height's conditioning term makes square-coordinate rounding preserve half the model singular margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
On the core size and envelope domain, the basic 2k height term also leaves enough norm budget for square-coordinate rounding. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A rectangular matrix whose entries are uniformly bounded by M has Euclidean operator norm at most sqrt (rows * cols) * M. This is the sharp dimension factor needed when rounding the signal basis coordinatewise. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Largest-remainder rounding of a finite probability vector. Each allocated numerator differs from its unrounded value by at most one, and any lower bound already satisfied by every floor is preserved. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under the model's doubled latent-mass floor and H ≥ ceil(pi0⁻¹), largest-remainder rounding lands in the prescribed floor-constrained simplex. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Euclidean form of the largest-remainder error bound used in the frozen estimate (88). Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Rounding toward zero puts a bounded scalar on the clipped 1/H lattice without leaving its support interval. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Coordinatewise clipped rounding for rectangular matrices. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Operator-norm form of coordinatewise matrix rounding, with the exact Frobenius-to-operator dimension factor used by the comparator construction. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every supplied orthonormal signal basis has all of its k column singular values at least one (in fact equal to one). Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Coordinate rounding of an orthonormal signal basis produces a valid grid matrix. Weyl's inequality preserves the asserted singular margin under the frozen quarter-radius condition. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A well-conditioned square coordinate matrix can be rounded to the prescribed clipped lattice while retaining half its singular margin and the doubled norm budget. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Coordinatewise clipped rounding for the effect vector. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Euclidean error form of clipped coordinatewise vector rounding. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.SubspaceAlignment 4 declarations This module isolates the exact algebraic core of Procrustes alignment.
Alignment of orthonormal signal frames
This module isolates the exact algebraic core of Procrustes alignment. Two orthonormal rectangular frames with the same column space differ by an explicitly constructed square orthogonal matrix. The result is stated in the matrix operator norm used by the surrounding proxy-effect-law development.
The Gram matrix of an orthonormal signal frame is the identity.
Formal statement
Proof (Lean source)
If two orthonormal signal frames have the same column space, then projecting either frame through the other recovers it exactly.
Formal statement
Proof (Lean source)
If two orthonormal signal frames span the same subspace, there is a square matrix orthogonal on both sides that aligns the second frame with the first exactly. The alignment is the cross-Gram matrix WᵀV.
Formal statement
Proof (Lean source)
Under a common signal row space, positive margin, and arbitrary matrix perturbation data, the exactly aligned orthonormal frames have zero operator distance, hence obey the requested inverse-margin perturbation bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.SummaryClosure 24 declarations Feasible-summary closure, nearest-summary repair, and ordered mass extraction.
Feasible-summary closure, nearest-summary repair, and ordered mass extraction.
A probability law together with membership in the uniformly conditioned model. It uses the supplied parameters.
Definition (Lean source)
For the supplied parameters, summary is given by its defining clause.
Definition (Lean source)
Admissible summary image. @realizes (S(M)) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Closed feasible-summary space. @realizes (closure of admissible image) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The quotient-law functional on the admissible summary image. @realizes (quotient functional on admissible summaries) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The 2k spectral moments identify the quotient functional on the admissible image. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The model anchor makes the first ambient coordinate the all-ones right anchor in latent coordinates. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observable target-proxy mean is the target-feature matrix applied to the latent masses. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The positive compressed signal singular value implies injectivity for the moment identity. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Injectivity makes the Gram determinant a unit for the moment-identity calculation. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The Gram-form inverse is a left inverse in the injective moment-identity calculation. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Published moment identity holds: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Homogeneity at a common latent effect. @realizes (common value of all latent effects) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The homogeneous-effect specialization included in the closed-summary definition. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Positivity of the last singular value makes a finite rectangular map injective. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Injectivity of a rectangular map makes its Gram determinant a unit. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The Gram-form Penrose inverse is a left inverse on every injective rectangular map. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Homogeneous summary specialization holds: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The complete closed-summary node: its closure, identified quotient functional, spectral moment identity, and homogeneous-effect specialization. It uses the supplied parameters.
Definition (Lean source)
For the supplied parameters, summary Closure Data is given by its defining clause.
Definition (Lean source)
Data supplied by the unique continuous extension and measurable nearest-point construction. The extension is defined only on K, at the paper's fixed effect radius. It uses the supplied parameters.
Definition (Lean source)
The repaired estimator data. @realizes (Fbar(Pi(empSummary))) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the ambient setting, ordered Masses is given by its defining clause.
Total effect-ordered mass estimator, with barycenter fallback. @realizes (ordered true masses) @realizes (ordered estimated masses) @realizes (generic competitor type) For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.SummaryMetric 11 declarations A concrete metric on finite-dimensional summary coordinates and comparison with dS.
A concrete metric on finite-dimensional summary coordinates and comparison with dS.
To coordinates injective: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For target- and reference-proxy dimensions, metric summary coordinates are the Euclidean representation of the four moment matrices and target-proxy mean.
Definition (Lean source)
For the supplied parameters, to Metric Coordinates is given by its defining clause.
Definition (Lean source)
To metric coordinates injective: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, from Metric Coordinates is given by its defining clause.
Definition (Lean source)
To metric coordinates continuous: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
From metric coordinates continuous: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
From to metric coordinates: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the ambient setting, summary Metric Space is given by its defining clause.
Definition (Lean source)
For any observable summary, its summary distance from itself is zero.
Formal statement
Proof (Lean source)
D s le dist mul: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.Witness 58 declarations Explicit finite two-class witness laws and local experiments.
Explicit finite two-class witness laws and local experiments.
For the supplied parameters, bernoulli Mass is given by its defining clause.
Definition (Lean source)
Bernoulli mass nonneg: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Sum bernoulli mass: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Sum mul bernoulli mass: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, vec2 is given by its defining clause.
Definition (Lean source)
For the supplied parameters, bool Real is given by its defining clause.
Definition (Lean source)
For the supplied parameters, det2 is given by its defining clause.
Definition (Lean source)
For the supplied parameters, witness Point is given by its defining clause.
Definition (Lean source)
For the supplied parameters, witness Weight is given by its defining clause.
Definition (Lean source)
Every elementary weight in the admissible witness family is nonnegative. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Latent-arm cylinders are measurable in the witness full-data space. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Latent-class cylinders are measurable in the witness full-data space. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Domain of the collision-witness perturbation. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Explicit two-class Bernoulli collision law. @realizes (finite Dirac law) @realizes (real carrier; range via WitnessPerturbationDomain) For the supplied parameters, the defined object is given by its defining clause.
Witness law is probability measure: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Summing out the four Bernoulli nuisance coordinates leaves the prescribed latent-class and treatment masses. This is the finite-factorization calculation used by the witness-validity proof for its class and arm marginals. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Restricted integrals under the finite witness law reduce to its explicit 128-point sum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Event masses under the finite witness law reduce to its explicit 128-point sum. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional means under the witness law are ratios of two explicit 128-point sums. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, Local Quotient Neighborhood is given by its defining clause.
Definition (Lean source)
For the supplied parameters, Local Weight Neighborhood is given by its defining clause.
Definition (Lean source)
Local quotient-law KL experiment. @realizes (model KL neighborhood) It uses the supplied parameters.
Definition (Lean source)
Local separated labeled-weight experiment. @realizes (gap model KL neighborhood) It uses the supplied parameters.
Definition (Lean source)
A complex spectral point of a real square compressed operator. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the supplied parameters, Matrix Eigenvector is given by its defining clause.
Definition (Lean source)
For the supplied parameters, complexify Matrix is given by its defining clause.
Definition (Lean source)
A polynomial aggregate projector used by the separate structured-lattice algebra. The constructive repair handle below deliberately does not use it: empirical clusters use Riesz contour projectors instead. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
For the supplied parameters, aggregate Mass is given by its defining clause.
For the supplied parameters, moment Discrepancy is given by its defining clause.
The identifying moment vector computed from a compressed operator and its summary anchors. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Full pairwise diameter of the effect cluster specified by the overlap relation. For the supplied parameters, the defined object is given by its defining clause.
The compressed operator computed from the one empirical summary generated by sample. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The complex resolvent appearing in the Kato/Riesz contour projector. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The Kato/Riesz contour integral of the resolvent of a real empirical operator. Contours are parametrized on [0,1]; certification that they close and avoid the spectrum is carried by RepairHandle. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The winding index used to tie the certified interior to its contour. For the supplied parameters, the defined object is given by its defining clause.
One empirical-summary carrier generated from the observed product law of P. Both its law and its summary are pinned, so neither can be chosen independently of the common DGP. It uses the supplied parameters.
Definition (Lean source)
Total empirical spectral mass carried by the eigenvalues enclosed by one cluster contour. For the supplied parameters, the defined object is given by its defining clause.
A positive finite-atomic law is a moment-cone projection of one specified moment vector when it is valid and minimizes the fixed finite-moment discrepancy among valid laws. This relation is used only at the realized empirical summary; it does not choose projections for other inputs.
Definition (Lean source)
A cluster-level constructive repair certificate indexed by one data-generating probability law, its model witness, one sample from its observed product carrier, and the corresponding population signal basis. No population operator, target law, empirical summary, or basis floats free: all clauses refer definitionally to this single package.
Definition (Lean source)
For the supplied parameters, path Target Feature is given by its defining clause.
Definition (Lean source)
For the supplied parameters, path Arm Totals is given by its defining clause.
For the supplied parameters, path Arm Weights is given by its defining clause.
Definition (Lean source)
Path arm weights formula: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Path target transpose inverse formula: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, base Reference Feature is given by its defining clause.
Definition (Lean source)
For the supplied parameters, path Joint Proxy Moment is given by its defining clause.
Definition (Lean source)
For the supplied parameters, path Reference Feature is given by its defining clause.
Definition (Lean source)
Path reference feature second formula: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, path Point is given by its defining clause.
Definition (Lean source)
For the supplied parameters, path Weight is given by its defining clause.
Definition (Lean source)
Exact domain of the generic tangent amplitude used by the labelled path. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The factorization-preserving Bernoulli path of equations (68)--(72). Every theorem and certificate using its second argument carries TangentAmplitudeDomain. For the supplied parameters, the defined object is given by its defining clause.
Path law is probability measure: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A labelled-path certificate for the explicit rational Bernoulli factorization used by the converse. The first four equalities tie every supplied path component to pathLaw and its proxy and weight primitives, so the remaining factorization, displacement, and score fields cannot be realized by an unrelated family of full-data laws. The coordinatewise derivative clause records the score-cancellation equations for Aₜ(h) diag(wₜ(h)) B(h)ᵀ.
Definition (Lean source)
The open constructive object requested by the note. It does not assert existence of a repair algorithm or prove a headline theorem: an inhabitant must supply both the empirical contour/moment certificate tied to P and sample, and the separate factorization-preserving labelled path certificate. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Calibrated positive path displacement. @realizes (a min(1,(sqrt n g)^-1)) For the supplied parameters, the defined object is given by its defining clause.
Calibrated displacement mem: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Range of the universal local-experiment radius. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.WitnessFactorization 7 declarations Conditional-independence verification for the explicit finite witness.
Conditional-independence verification for the explicit finite witness.
Witness sum restrict latent cell: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional mean witness latent cell: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness sum restrict latent class: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional mean witness latent class: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness reference proxy separation: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness target proxy separation: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness armwise latent ignorability: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.WitnessKL 14 declarations Finite-cell KL and quotient-law separation certificates for the collision witness.
Finite-cell KL and quotient-law separation certificates for the collision witness.
The coordinate measurable structure on labelled atomic laws is their Borel structure. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The quotient law's mapped measurable structure contains all open sets of its installed Wasserstein topology. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The collision witness represented on the finite visible Bernoulli carrier. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Mapping the finite collision-witness carrier recovers its observed margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite visible collision-witness law has total mass one. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Each visible cell changes by at most the collision amplitude. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every base collision-witness visible cell has a uniform positive mass. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Every collision-witness visible law is absolutely continuous with respect to the base law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed collision-witness law is absolutely continuous with respect to the base law. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The collision-witness observed log likelihood ratio is integrable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The finite visible collision-witness chi-square divergence is quadratic. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The observed one-record KL divergence of the collision witness is quadratic. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A collision witness whose quadratic KL is within the local radius belongs to the quotient local experiment. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The collision witness quotient laws are separated by exactly the collision amplitude. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.WitnessSpectral 4 declarations A two-dimensional variational certificate for the explicit witness proxy matrices.
A two-dimensional variational certificate for the explicit witness proxy matrices.
A coordinatewise quadratic lower bound certifies the last singular value of a real two-by-two matrix. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The target-proxy matrix of the collision witness has singular-value margin one tenth. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The control-arm reference-proxy matrix has singular-value margin one tenth. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The treated-arm reference-proxy matrix has singular-value margin one tenth. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.Helpers.WitnessValidity 29 declarations Finite-sum, envelope, matrix, and law calculations for the explicit collision witness.
Finite-sum, envelope, matrix, and law calculations for the explicit collision witness.
Measurable set obs arm: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Measurable obs z mul x: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Obs witness arm mass: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness latent mass: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness latent cell mass: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness target feature: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness reference feature: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness latent effect: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional mean obs law witness: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness sum restrict obs arm: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional mean obs arm witness: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness weight sum outcomes mul: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness weight sum outcomes: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Conditional mean obs arm zx: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness observed proxy moment entry: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness observed proxy moment det: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Ae witness law of points: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness consistency: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness anchor: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness outer product norm: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness bounded x: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness bounded proxy product: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness bounded outcome proxy product: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness latent arm positivity: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness proxy rank margin: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness det target feature: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Witness det reference feature: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Two by two injective of signal min singular pos: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The collision witness belongs to the uniformly conditioned model throughout its admissible amplitude interval. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.OpenQuestions 1 declarations The unresolved exact/sharp computation question, recorded as descriptive non-Prop data.
The unresolved exact/sharp computation question, recorded as descriptive non-Prop data.
Can the original sharp summary-inversion image and its support-dependent extrema be evaluated by one fixed-dimensional exact-real algorithm, uniform in the sample size and polynomial in it, without compact nearest-summary optimization or black-box Fbar evaluation? The unresolved alternative also allows a sharp representation rather than direct exact evaluation. This payload is deliberately nonassertive because the note leaves the exact-real operation and forbidden-oracle criteria undefined. For the ambient setting, the defined object is given by its defining clause.
Definition (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TClusterAdaptiveReport 1 declarations
On the summary event, associated true clusters partition the target support, lie in their reported intervals, and obey the atom-floor external-gap mass bounds. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TCollisionUniformRootN 2 declarations
The total empirical five-block summary is Borel measurable, including its empty-arm branches. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The computable lattice and theoretical nearest-summary estimators simultaneously attain the collision-uniform root-n quotient-law rate. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TFiniteNetLawEstimator 1 declarations
The advised class-dependent finite library is total and Borel, has the displayed polynomial size, and obeys the deterministic gap-free modulus bound. Its spectral output and operation count come from the same result-bearing exact-real primitive execution. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TGapFreePositiveMeasureModulus 1 declarations
Gap-free Lipschitz modulus for quotient effect laws and its positive-law continuous extension. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.THonestRootNConfidence 7 declarations
Latent class real eq sum cells: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Latent mass two pi0 le: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Of measure equivalent: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Quotient law atom floor: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
For the supplied parameters, wass Diameter is given by its defining clause.
Summary repair with modulus: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Simultaneous honesty and the two separate root-n diameter bounds, without asserting an equality or inclusion between the confidence sets. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TLabeledWeightUpper 1 declarations
Uniform labeled-coordinate upper bound on the gap stratum; inverse-gap behavior is confined to ordered labels. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TMatchingLocalLowerBounds 9 declarations
A tail event for a nonnegative integrable loss gives a lower bound on its mean. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Distance to a fixed point is integrable for measurable maps into a compact metric space. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Le Cam's inequality, tensorisation, and tail integration give an expected metric-risk lower bound for one member of a two-point experiment. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ℓ¹ loss between two simplex-valued vectors is integrable. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The scalar-coordinate Le Cam bound lower-bounds the full simplex ℓ¹ risk. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Along the separated two-class path, ordering the quotient-law atoms preserves their latent coordinate order. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The ordered mass vector on the separated two-class path belongs to the probability simplex. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Calibrating by the inverse square-root signal bounds the squared product displacement. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Matching local converse witnesses for quotient-law and labeled-weight loss. The existential law form avoids supremum junk values and is equivalent to the displayed minimax lower bounds. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TObservedVMWMarginInclusion 20 declarations
For Euclidean input and output dimensions, the measurable-space structure on continuous linear maps is the Borel structure.
Definition (Lean source)
For Euclidean input and output dimensions, continuous linear maps form a Borel space.
Formal statement
Proof (Lean source)
The diagonal normalized latent-arm weight matrix retains the joint-cell positivity margin at its least signal singular value. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Once the promoted conditional-moment argument supplies the proxy factorization, the three quantitative factor margins yield the required armwise singular-value margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The matrix carried by a SignalBasis is the linear isometric embedding determined by its orthonormal columns. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
Compression by any orthonormal basis spanning the stacked signal rowspace preserves the last signal singular value and its quantitative lower margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Independence transfers an almost-sure product envelope to the second factor whenever the first factor exceeds a positive threshold with positive probability. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A bound holding on a positive-probability event transfers to an independent random variable on the whole probability space. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
A reference-feature singular-value margin supplies a coordinate that is nontrivial with positive probability in every normalized latent cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Proxy separation, a reference-rank margin, the anchor, and the observable outcome--proxy envelope bound the observed outcome on every latent treatment cell. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Consistency and armwise latent ignorability transfer the observed cell envelope to each potential outcome on the whole latent class. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The derived potential-outcome envelope bounds every latent conditional mean. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The two derived latent-mean bounds imply the gap-free support bound for every latent effect. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Given the latent dimension lower bound, feature dimension bound, proxy dimension bound, radius bound, treatment positivity, noise positivity, and model membership, the effect gap is infinite or lies in the declared positive bounded interval.
Formal statement
Proof (Lean source)
The operator norm of a conditional matrix mean is bounded by an almost-sure operator envelope for the matrix-valued random element. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
All five observable summary blocks inherit the common model envelope. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The Euclidean norm of either arm block is at most the norm of the vertically stacked proxy-moment operator. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The vertically stacked proxy moment retains the common quantitative signal margin. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Uniform observed-moment and latent-outcome consequences of model membership, together with the conditional cited-scope transfer to the published VMW model. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The five observable blocks of a model-generated summary obey the common envelope. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TPolynomialLatticeEstimator 1 declarations
Existence and deterministic/high-probability guarantees of the explicit no-advice structured lattice estimator, including its atom floor and polynomial candidate count. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TPublishedVMWConverseTransfer 5 declarations
For the supplied parameters, law Risk is given by its defining clause.
Definition (Lean source)
For the supplied parameters, weight Risk is given by its defining clause.
Definition (Lean source)
Distinct effects in a gap stratum imply the qualitative spectral-separation condition. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Under model membership, the leading right singular vectors of the stacked proxy moment give a signal-spanning basis satisfying the published population equations.
Formal statement
Proof (Lean source)
Relative to one fixed nominal published-scope handle, any comparator classes containing the explicit quotient and separated labeled witness pairs inherit the two Le Cam converses. No upper or confidence result is transferred. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TSameClassLabeledMinimax 1 declarations
The inverse-gap lower and upper bounds hold on the same gap-localized two-class model. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TSameClassQuotientMinimax 1 declarations
Root-n upper and lower bounds hold on the same uniformly conditioned two-class model. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TSummaryClosureCompact 15 declarations
Every matrix entry is bounded by the Euclidean operator norm. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The entrywise closed cube of rectangular matrices. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The entrywise matrix cube is compact in the finite product topology. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The coordinatewise closed cube for the unconditional proxy mean. For the supplied parameters, the defined object is given by its defining clause.
The proxy-mean cube is compact in the finite product topology. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Product cube containing every admissible five-block summary. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The five-block coordinate cube is compact. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The summary record is topologically identical to its five-coordinate product. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The coordinate equivalence respects the induced summary topology. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The summary-space cube corresponding to the coordinate product cube. For the supplied parameters, the defined object is given by its defining clause.
Definition (Lean source)
The summary-space cube is compact. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Observable block envelopes place the admissible image in the finite coordinate cube. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The closure of an admissible image contained in the summary cube is compact. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
Observable block bounds give a uniform bound for the continuous summary loss. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The admissible image is uniformly dS-bounded, its closure is compact, and closure nonemptiness is equivalent to model nonemptiness. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TSummaryRepairTotalBorel 7 declarations
For target- and reference-proxy dimensions, the summary-repair coordinate index labels four matrix blocks and one target-proxy mean block.
For the supplied parameters, summary Repair To Euc is given by its defining clause.
Definition (Lean source)
For the supplied parameters, summary Repair Of Euc is given by its defining clause.
Definition (Lean source)
For the supplied parameters, summary Repair Space Homeomorph is given by its defining clause.
Definition (Lean source)
For the supplied parameters, euclidean Reindex Homeomorph is given by its defining clause.
Definition (Lean source)
Compact loss selector of homeomorph: under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
The nearest-summary repair has a total Borel positive-law realization, with the stated zero-law fallback and a nonempty theoretical confidence set. Under the stated inputs and assumptions, the stated conclusion holds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_ProxyEffectlawEigencollisionFrontier_Research.TTwoClassWitnessValid 1 declarations
The explicit two-class law remains in the uniformly conditioned model through the collision, with unequal latent weights and nonsingular proxy matrices. Under the stated inputs and assumptions, the stated conclusion holds.