descent

Descent is a software project written in Lean 4 that provides a formal mathematical framework for genetic theory. Its primary focus is on the portability of Polygenic Scores (PGS), addressing three core questions regarding their accuracy and limitations across different populations. The repository contains rigorous proofs developed in `OpenQuestions.lean` that classify individual-loss information and noise. These proofs establish sharp attainable ranges at fixed second moments and genetic inputs, characterize finite evolutionary or reporting closure, and define metric-ordering and decision-cost converses. The theoretical domains include arbitrary square-integrable loss for information theorems and explicit finite model classes for sharp ranges. Additionally, Gaussian loss noise is derived from the Gaussian measure. A combined axiom audit is provided in `CheckThreeQuestions.lean`. For detailed results and limits concerning demographic prediction of polygenic score accuracy, users are directed to the `UNIVERSAL_PORTABILITY.md` documentation. ### Building To build the project, run the following commands: ```sh lake exe cache get lake build Descent ValidationShared ``` ### Contributing Contributions are welcome. However, strict specifications apply: - Simulations must never be used to fit models; they are exclusively for validating existing derivations. - Only three axioms are permitted: `propext`, `Classical.choice`, and `Quot.sound`. ### License The project is licensed under Apache-2.0.