c8bdd828297a335c0ec1adfe889b4d9ee970f485c350530f01b2d447259dc4c5  Erdos143/AbelBounds.lean
2d880c20d96ceaf34c72ddd62efd2b47d0b4568fae9230d0a131130b7b28963e  Erdos143/AbelLayerSelection.lean
fd514a9605086544e11b0ddee4f50776a8897c0a24794df4ec3d46ea1e0b8494  Erdos143/AllResiduesAbel.lean
1ee00b946537e4ba14975d46e151238b5885bd2b70213115310c439b7edfd032  Erdos143/AnalyticInputs.lean
a4368b683a0dd5236bd4a3e3048d8fe74a10d279986438237dc111ef5f9fea01  Erdos143/Arithmetic.lean
0fb425117a237f8bc9494d0ad31aa4fbec8939c1f307d28a6d073f6ee281a95e  Erdos143/BlockExtension.lean
60cf6a8bfaa3d0ff55ceac031c72b09b948d06d246c92931d3aa57fe4641a1ca  Erdos143/BlockParameters.lean
16809c9da0f7cefaf3bf7509873fa510b4a62b2f95410bfa1bd9823e53865d12  Erdos143/BlockWeight.lean
6cbb317405ca6d9ba6a3236bf1bbb65199ae773f6fc9cf78aa647bea2747248f  Erdos143/ConstraintSelection.lean
5206a0cbf77be9c19a65acc0a66f5d4bc298df3a31de7fdf9887d3c53f0826f5  Erdos143/ConstructionState.lean
9f69fe82fd8663ed8b894a784297376ca2ac2a7c0312cf1505b3b281707a2425  Erdos143/CoprimeAbel.lean
15e233e77e3b07fd32d45f14eebc14cea170eef60be872d75d965b6a68cc36e1  Erdos143/CorrectionProducts.lean
b9f6679067ca782cc87f4827b6768921349990177e1e06464c9d0b43e58f3790  Erdos143/Definitions.lean
0a1541dacc0af90e27e48ea570f2a169c7a0293dd2be0eddd05c292d68700e66  Erdos143/EulerFactorBounds.lean
17725a7257613e8ee5d3d366ff7a58d9a5a1b1e58213881d0afa078614909184  Erdos143/FiniteDensity.lean
9d52a604571e5aecaff12d197205b75be2861497f6e2d14234b556a47625ebad  Erdos143/FiniteExtraction.lean
42f5c50367178b9e75eabc8c7a99f7b3c88ebcdac599194907256eba05e3eaf8  Erdos143/GeneratingDomination.lean
cb41fa12b8f3f90bf56c9fa766b6d7e7a349db03e0c0fee5f291f0f8f937eeaf  Erdos143/GeneratingEulerProducts.lean
7ec3323817b614fd156aac1a598fe05e857220fcb4eec334245f433314b614b4  Erdos143/GeneratingIntegrability.lean
2f2526bee9ab1fc31e26126321b670d0f356ef2aae1f8be8e507efe130eae2e0  Erdos143/GeneratingRegularity.lean
9e3ca246670c2d071467be292def09a4269d0cdbb01860c6a1ebdbe83b5b6b75  Erdos143/GeneratingTail.lean
7d79dc78919333e60a07125f84a68ebe5a9650e175b05d4dd4400222cd53ca97  Erdos143/Geometry.lean
6e868c0b403718daad2eb2424b20af9552eb9a5efa2ac25f54a9feb213e05312  Erdos143/ImproperControl.lean
825bb34ee20a37326cf2bc80e443e8c6dcb76ed6af817f3f407dad898effe543  Erdos143/Insertion.lean
80a077b031355588236a6f7c144407ee55b2bd6da08a88c0bc3c0cb9e3ac1a51  Erdos143/InsertionExistence.lean
551268d72a9a7f1227c7399c0d9ff28bc7194fcbce18da8a32c598e3a6c76746  Erdos143/LayerDecomposition.lean
5063ad22700dd655326d64a9c6181520399c2c0649bbfce5bca9051492cfc913  Erdos143/Levels.lean
3ab6ecfd8464182c4e20d5b3857bdb44f62b259aacc34bb6a31767005d7e62a8  Erdos143/LocalFiniteness.lean
f18463157cc8e2f111ed66aa548c8fa0d21c553ae43076e6e8458b96ca360c79  Erdos143/LogShift.lean
0e3b478a20a327e0dff1a3c1c2d77fba63c14dbb05ab59818affcf87809c8892  Erdos143/LogWeights.lean
a268692cddddae64e413eae8283b1018048044417ab05ee45e875e9075da8582  Erdos143/Main.lean
54ff185f4a3045cc0b60696f0342d81bdacdc268da40b7f5027a64f30796c62a  Erdos143/MellinWeight.lean
5e3f3c3b6abea210821f3d24596f26ecef4bb2f2ce7747e5ccfc3c7ea8d5fe22  Erdos143/MomentIntegrability.lean
dc2777705ec2b8c0c18df97839a08828fc92517901fe9df8cc00de0bed859de2  Erdos143/MomentKernel.lean
3e7ff79e43b91034614d8ab24f35adb7644f06b2c6de861c398c17888de2a2db  Erdos143/NestedUnion.lean
794018ae476bc7fb2d909f63a13e155da70c7a07ae20a1c81199b0c5de37c315  Erdos143/NonprincipalAbel.lean
8a1cec53ab23c48253cf92020ddbd2f2d022f5336a31293cee80842bceec10ac  Erdos143/PeriodicMass.lean
fe2fe6c14c91c9ba9bb091729bebbafcbcba54daa3aa29737e8c33ce58ac1bbc  Erdos143/PeriodicSelection.lean
a09f8baf8c48e563bc2f4b8bd5509bb1e499663d360b0f99dcb32000a7236b1f  Erdos143/Perturbation.lean
d8bca4ecc19d2c1e2442781816ff38208104df8a1a546181a2583a808ff7bf81  Erdos143/PositiveEulerBound.lean
ca7bda2c41e2067ebfe46cbbb2730bb5dadd448819ce09d726d8ce4851dcae2b  Erdos143/PositiveInterchange.lean
e903e28d3b379ea572762a3c5aa163a3b85261aefef6c466f11fb684c8d045d0  Erdos143/PrincipalAbel.lean
bdab7fa20ca4ce05c375f5e977612a3a4c2bbd570fb438a005822bf9f0458aac  Erdos143/PrincipalBound.lean
d02c198f5dfed3027fccd88a28b59e14c54052d978fc5fb2c1ff2331ebeb35f3  Erdos143/PrincipalReality.lean
70ab168f42349155dddc33e3998953e9d3dd81da7aa1158f96d173ecb2133431  Erdos143/PrincipalResidue.lean
1fc7219733a7239f7ad60e2e851f542b5f0ef77454c39f3982594d530c99d4b1  Erdos143/ProgressionScaling.lean
b1f223514d9036033dc7cb3dd8c43997999c401eda9d5f78c61da1cb9efa768c  Erdos143/Progressions.lean
f063e56e6672352266c5803130508bf66d29fc2a7b00e22491e564b3e817207c  Erdos143/RealConclusion.lean
41a857ca32366546f9513510d007495eb9c46d1143c5131030378166f9b9d80b  Erdos143/RootResidues.lean
c8bd5b855576d03af5442ed7f6045e99a9c39129134dc3f4f1631b094f9cf2fb  Erdos143/RoundExtension.lean
546a428b2772d5e48a177b598aaaa141b040ceb7f38865c327a3982a8fbd331f  Erdos143/RoundLabels.lean
19f2d183c2d45f82dc6a94f2884ea22f24a845dab146b5bdfd7f35c8e99edf5b  Erdos143/TwistedBound.lean
5458db12ac0ed069c0d87230b1d6c0b473144ce3916dee7cc92f0ceacbe7307b  Erdos143/TwistedIntegral.lean
d93a2042837e10a5ccbbb70b2fbccee4c1b2b76c8adb98b52b90229a9f2b5c47  Erdos143/Weight.lean
44b58728b1f03b19a8cb11cecac5ba2a9dd549e055e2cf01d021daa7cd37440a  Erdos143/WeightedIntegrability.lean
00df6e1d1f40c5613d067eb0f41a96334ede37ff21f9e4f9837ee79780ce2b39  scripts/bootstrap.sh
d4b120d396e83f2a25cdba5bcd1bc5287a9a9344d5afc0c3e86d62949740ae36  scripts/check_axioms.py
85456469fac137e0ec3b992801db1a052fddd0c36b21c141977e741c352a9cb4  scripts/check_sources.py
f633ec8119dbe41366b36310d00145ecdf22f2593068ddb899793d0f03d618fb  scripts/generate_audit.py
6ef96df5b10a9f27b8e33346c91f6a91eacabc21ef3436f6e0d452be46ef5d55  scripts/verify.sh
df9bda238f403c3f684d852a67fdd83c68d7bf6732d14249e65a7440746e3031  Erdos143.lean
d87387f986f359aaf03ca7b21d913a1af7fa6476ce85ee1984783c9f3f907638  AxiomAudit.lean
c5e1be451ab450fa045a49bc242fd268ae15ed82817a4d4d869be26d7e3120a2  StatementAudit.lean
d1593a50716b88910a0479406861fc3f7293fc37440f1a579db44af40d77cd18  README.md
24d2b114e74558721a7192a1fa67c737cc10a3eec77568928d177410da1bd5c2  Abel-periodic-proof.md
66fd48b852c5d90cac277ff4d0f75a30c14b91c713c3abd84fc0ae689427f609  Construction-correspondence.md
681c0a724311fb2733604e17c3806410f274a7ea708bcdc74e35765b6244c2cb  lakefile.toml
55f55e223176da05663a0e3b98abbd9fb481d8827f1e10fad25f2ae3eaa2f527  lake-manifest.json
42779d67b81608af8a12aa4328d2ab47ca201925b3b2bd68369587b5340bb434  lean-toolchain
f73357dbbf4052c79d0cc3fefe209d5d26c227955c0ab9901678fa1665919ac3  .gitignore
