descent

Descent é um projeto de software escrito em Lean 4 que fornece uma estrutura matemática formal para a teoria genética. Seu foco principal é a portabilidade de Escores Poligênicos (PGS), abordando três questões centrais sobre sua precisão e limitações em diferentes populações. O repositório contém provas rigorosas desenvolvidas em `OpenQuestions.lean` que classificam a informação de perda individual e o ruído. Essas provas estabelecem faixas atingíveis precisas em segundos momentos fixos e entradas genéticas, caracterizam o fechamento evolutivo ou de relato finito e definem conversos de ordenação métrica e custo de decisão. Os domínios teóricos incluem perda arbitrária quadrado-integrável para teoremas de informação e classes de modelos finitos explícitos para faixas precisas. Além disso, o ruído de perda gaussiano é derivado da medida gaussiana. Uma auditoria combinada de axiomas é fornecida em `CheckThreeQuestions.lean`. Para resultados detalhados e limites relativos à predição demográfica da precisão de escores poligênicos, os usuários são direcionados à documentação `UNIVERSAL_PORTABILITY.md`. ### Compilação Para compilar o projeto, execute os seguintes comandos: ```sh lake exe cache get lake build Descent ValidationShared ``` ### Contribuição Contribuições são bem-vindas. No entanto, especificações estritas se aplicam: - Simulações nunca devem ser usadas para ajustar modelos; elas servem exclusivamente para validar derivações existentes. - Apenas três axiomas são permitidos: `propext`, `Classical.choice` e `Quot.sound`. ### Licença O projeto está licenciado sob Apache-2.0.