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.
docs/SCOPE_INTEGRITY_NOTE_2026_04.md— conditional note specifying the weakest downstream-scope audit compatible with the repository's complete-within-scope status.
Mathematically complete within its declared scope. Stable reference component.
This repository is governed by docs/status/EXTERNAL_STATUS_LOCK.md. Build success, CI success, dashboards, ledgers, axioms, admits, sorry, or placeholder witnesses do not constitute theorem-level closure.
This repository is governed by docs/status/LEAN_PROOF_PORTFOLIO_CLASSIFICATION.md. Its role in the portfolio is explicitly classified as proof-facing, conditional frontier, infrastructure/documentation, or legacy/scaffold.