This repository provides a Lean 4 formalization of the Support Drift concept: a geometric bound on how the support of a probability measure can change under constrained transformations.
It is a rigidity component used within the Unified Rigidity Framework (URF).
- A theorem-level bound on admissible drift of support, formulated via the Hausdorff distance between supports of measures.
- Establishes conditions under which support evolution is provably limited.
- Formal definitions of support drift and related notions.
- Lemmas establishing basic properties of the drift bound.
- Proof infrastructure used by downstream URF modules.
- Not a convergence theory.
- Not a continuity theory.
- Not a repository for extending the result beyond the stated assumptions.
Mathematically complete within its declared scope. Stable reference component.