descent

Descentは、遺伝理論のための形式的数学フレームワークを提供するLean 4で書かれたソフトウェアプロジェクトである。主な焦点は多遺伝子スコア（PGS）の移植性にあり、異なる集団間でのその精度と限界に関する3つの中核的な問いに取り組んでいる。 このリポジトリには、`OpenQuestions.lean`で開発された厳密な証明が含まれており、個体損失情報とノイズを分類している。これらの証明は、固定された二次モーメントと遺伝的入力における厳密な到達可能範囲を確立し、有限の進化的または報告上の閉包を特徴づけ、計量順序と決定コストの逆命題を定義している。理論的領域には、情報定理のための任意の二乗可積分損失と、厳密な範囲のための明示的な有限モデルクラスが含まれる。さらに、ガウス損失ノイズはガウス測度から導出される。 統合された公理監査は`CheckThreeQuestions.lean`で提供されている。多遺伝子スコア精度の人口統計学的予測に関する詳細な結果と限界については、ユーザーは`UNIVERSAL_PORTABILITY.md`ドキュメントを参照するよう導かれる。 ### ビルド プロジェクトをビルドするには、以下のコマンドを実行する： ```sh lake exe cache get lake build Descent ValidationShared ``` ### コントリビューション コントリビューションは歓迎される。ただし、厳格な仕様が適用される： - シミュレーションはモデルのフィッティングに決して使用してはならない。それらは既存の導出を検証するためだけに用いられる。 - 許可される公理は3つのみである：`propext`、`Classical.choice`、`Quot.sound`。 ### ライセンス このプロジェクトはApache-2.0の下でライセンスされている。