b4ed7a975a6dd954633cc85e0bc7d503783692ed1ed0b59a84c6aecd3d4a66be  README.txt
b3248202894c6fa1e5ad7980e9c9ec955f6f5e27424bd99db485af824ea5baee  anc/BUILD_NOTES.md
4489c6d66e9ad2e3bb9207ea9981e409cc92f08c50568bd2e928180ea4c84938  anc/CITATION.bib
fecdc44a46d2ca0d20f7a66cc33b8f3594f0a4884de8473a7bf2951de6a1a2b3  anc/LEAN_FORMALIZATION.md
f7bd00d871f913346ac77062ec5a35b8792451ba542d2c7958249e57e5aef7e0  anc/LICENSE.md
97192e40c819e5c15f1538911d718a38d6b3e739438fb416acf5f574a3cb955d  anc/LICENSES/CC-BY-4.0.txt
ad7dd18077f920e2326157dd543ef44e36abb82c1b57f5f9719a3779132b93a9  anc/LICENSES/MIT.txt
a2bcc29379e22bc90ea98ff4169af923e2c1f12ae043eabda74d6a5b28a57697  anc/PROOF_GUIDE.md
ad103f7741474b1218fcfe03c6582bb9c98fdc66c4543c590b5bc60d80746f1f  anc/README.md
a5c5568097b6be5c1240ee48293024e944ad2ece2a89c039a7f6cde54e807f7a  anc/REFERENCES_REVIEW.md
01d50a1bb015218d8cfbb3a5bc5fc9437788afc734e8f896a797a6fae60f2fe2  anc/VERIFICATION.md
66c77905b752184f33dd794faca03a3f9062f2987e543d4859289e1a8ec8dac5  anc/ZENODO_PREPARATION.md
95d726c361a6b107fae165c6290874d6baf13fb9705ac5f4d4a52575f4a4e236  anc/certificate.json
69e72093facbba391f52895b4d608766d5f5f1c39e34c7c446c381cd127fc1e9  anc/crosscheck.py
f7bd00d871f913346ac77062ec5a35b8792451ba542d2c7958249e57e5aef7e0  anc/lean/LICENSE.md
97192e40c819e5c15f1538911d718a38d6b3e739438fb416acf5f574a3cb955d  anc/lean/LICENSES/CC-BY-4.0.txt
ad7dd18077f920e2326157dd543ef44e36abb82c1b57f5f9719a3779132b93a9  anc/lean/LICENSES/MIT.txt
e5f30a228afc5a6e5bf0c098dd98b56ec02849a65bdf2820386596cf3bb39336  anc/lean/README.md
2e8e317e841c29af823bf655a4498af5ca615153e4afa325c1d3412ddeadac92  anc/lean/SHA256SUMS
daa47f6f4218dad3585f3ae84c2f6893d3c1505131a90bfb3e4d95e20b4a3c1f  anc/lean/formal/Audit.lean
7de9058225e665581b0530ff9beaf3fc2244a374aaadcb7c26225267b6b24a40  anc/lean/formal/AuditRank8.lean
7095d4245d3308c032d7785424ff62ddb2393f683c7160a5193842f490b66484  anc/lean/formal/AuditThreePrime.lean
55a05fe830dec46f4d2f7dacdbad06445e6da388bb0f00d0bc40b61609485514  anc/lean/formal/Erdos7.lean
0cf2e7e8642141d6cf8c7bcc9906c7df0d99ab266d62c86ac9cb5ea870e20624  anc/lean/formal/Erdos7/ArithmeticReduction.lean
31649f8a199ccbd1a9ce46b1c99e2384ca614260756cf4ffa93af0d768bcbcb1  anc/lean/formal/Erdos7/CappedGain.lean
9f844aa0e8f88eada6d8b7107ddb7f2e3aa3063237db2df3bb08693b742309b0  anc/lean/formal/Erdos7/CappedGainBlock.lean
542d4d55f3bc37dae0c44f5815d4b66fee191a3770f2c03b79e93d2589ddece9  anc/lean/formal/Erdos7/CappedGainCovering.lean
b7275bc24f020748554a5f2010c4a9e8268a4363fd6691ecc41b2338f0fbb881  anc/lean/formal/Erdos7/CappedGainDepth.lean
a1ab3d503e97b10b4524391df4585102584eab47a26aa4447ffcd21540b5b9c1  anc/lean/formal/Erdos7/CappedGainDistortion.lean
9cc127d1f7a4014de2689aef8641676d392e7258627a4cfc723b0896797f96d3  anc/lean/formal/Erdos7/CappedGainEnvelope.lean
1f7010df6738a87cda4e45ccee1062561aa983cb346a223067ad05eab3f6c489  anc/lean/formal/Erdos7/CappedGainFunctional.lean
78362463df2c3997e6a7fdbf7d345e1409d908d5ca42a51d8762fde1cc998e88  anc/lean/formal/Erdos7/CappedGainGeometric.lean
7f4541df6ec9f2ac5edaa6f3f6054b1d59a7c2ac47090a9fff121cc18973bc9c  anc/lean/formal/Erdos7/CappedGainLattice.lean
cdcbb84f1f17aa62d639796ec4f405e186f9f287b9abe6273d09fccab3953166  anc/lean/formal/Erdos7/CappedGainLift.lean
50a75c3df518a51d2ffce353fa5168a8ea3a815d03b4c31008f6f81b6da917da  anc/lean/formal/Erdos7/CappedGainProbability.lean
f6d3565ae629318ca6347851ddcf092b9c6db9e89dc3acb0326a583011e14dac  anc/lean/formal/Erdos7/CappedGainRearrangement.lean
dc66abdfd02a97eadafce0a43779fac7f4b325e59bd0ef6b31f3c643565540d3  anc/lean/formal/Erdos7/CappedGainScalar.lean
9fa9954a53a70e7625b1c9d1142b5423e4f9778329a2dd5dbfbc186f006015f2  anc/lean/formal/Erdos7/CappedGainTrees.lean
c61eb5217c124ed7461e5ea7893759e95267f034930ad6017cacce8bb909a5bf  anc/lean/formal/Erdos7/CappedGainTypes.lean
8821f4a1e642a005cd33e48cce345e4a8c8e31e77dc7a7d7e3f2b0a0fb0f44ce  anc/lean/formal/Erdos7/Causal.lean
33973ceb1db69eda1e1738093fddd31a20e1652c6372a3381a060dad542dd193  anc/lean/formal/Erdos7/Certificate.lean
a07d9778f81740dedcddb92a9517979deb48a2c4f24ea3636056706e8b2a9d87  anc/lean/formal/Erdos7/Cylinders.lean
3214449a0e7983a1d21ab721c3beb3865fa66542ea82971837b5539334254da4  anc/lean/formal/Erdos7/Distortion.lean
f7404a193f1bf6ef2b3cd6741453e469966e594ff60e9192cb6363fa124b6195  anc/lean/formal/Erdos7/DistortionChain.lean
ad3e8702a076eb81fa1cfd5da10e0f0b5b95dce12a4052ebcb0f2208d0074637  anc/lean/formal/Erdos7/FiniteProbability.lean
727757b25f792dace30db388f1b66f3d2d8a0749830639f0030e91541ff3cced  anc/lean/formal/Erdos7/GateModel.lean
051268de09179fb09c32a2626945d13854a4f74b836374b4b6d0f6ab98f219fe  anc/lean/formal/Erdos7/Hybrid.lean
7382df9ab68ecd8baf040d08089f68501700cb091b168cdb1dbb603c48da7516  anc/lean/formal/Erdos7/OpenRuns.lean
dbf76b83f8bf58fea875efa044f5c791bc7cb655a9e8620e1a8a0d6204c340ae  anc/lean/formal/Erdos7/ProductGates.lean
1feb45c300488d2d89e2cef9c7bb9a915d39046070eaf3084513364128addac5  anc/lean/formal/Erdos7/ProxyCertificate.lean
97b22ffc264df036bd43510fb0ad460a7907f2753ae4305764b065e31c389fa8  anc/lean/formal/Erdos7/Rank8Arithmetic.lean
308f99b3132ca45e0312816633809d04184bbd7c4f2bdf5d08ca5f297a5e228f  anc/lean/formal/Erdos7/Rank8Certificate.lean
e81b8017541eaa0f548176a458346d69432440391e830221d4427992bb100b42  anc/lean/formal/Erdos7/Rank8Cylinders.lean
993185e32b6df8315e5f0219d4e060e4feae990cafaf7cb9869f2ccf25ff96a2  anc/lean/formal/Erdos7/RankedRearrangement.lean
850f191707b1044be1c6c64d1abe2f2a2f6a5dc6f9cbeae11b299a4f15e7a0e2  anc/lean/formal/Erdos7/RunDominance.lean
66f35dfe1741580137d58888910fe48f8088e5a354d986a6412e3268ed8ef871  anc/lean/formal/Erdos7/Runs.lean
1ac462e39fbf96839685d5242b24d26d10f6bb075adc66ebdb02c14ec6de2906  anc/lean/formal/Erdos7/SixBlockCharge.lean
d027c8a2bf06803312b5b05e2f941a7c92f06f4ca2aff02df434dd8caca44980  anc/lean/formal/Erdos7/SixBlockExpectations.lean
9550513c2c948c6e2e8eedf94c410245a715afad593ce44eb22a13121c1a3d37  anc/lean/formal/Erdos7/SixBlockGates.lean
a2f56f41bb02b30f2a36619e486fee9099d323f8732e6688a1c25448eab0c1fb  anc/lean/formal/Erdos7/SixBlockModel.lean
0006bc11fa89d185abf0762afcb1f908b26a1774a5037de04a62bce02da64e0a  anc/lean/formal/Erdos7/SixBlockNoncover.lean
40913b61d6966c480eaec017e50d23638bc5c924010bae886e9c50df21776bd3  anc/lean/formal/Erdos7/SixBlockReduction.lean
28d13560f1a13cea1e06dff58563443b41c2c36b4d541950af0e15144fcc6ecb  anc/lean/formal/Erdos7/SixBlockTotal.lean
54eeadae8666c949dba0ff1b3bee564baf10b9aed874b805bf5285efda396da3  anc/lean/formal/Erdos7/Supermodular.lean
6e91fb555e0a6ba2f5093a2221569bc213b27589179586de0677087c90850cb4  anc/lean/formal/Erdos7/ThreePrime.lean
79c6d2e5f4ceacf6b59eee6aad20bc398990d6532a1d32119d499a2345dd3424  anc/lean/formal/Erdos7/ThreePrime/Arithmetic.lean
30e58bc426524a85c39f3fcf1b840982383e044808c30192b7e42f3cc2997cee  anc/lean/formal/Erdos7/ThreePrime/Binomial.lean
f438f65b695b76749fb1613a1b1640ed8ea4d90e4a1f13df00b6f49e7ca75f07  anc/lean/formal/Erdos7/ThreePrime/CertificateData.lean
71800fcc8bd11894f0dad38c35bdb828f94dab0b48121b40a854bf05dcd91975  anc/lean/formal/Erdos7/ThreePrime/ChargeInterface.lean
9a24d07120f5225389606628961742d023ae7b09c0ff6a03554403a12436b2c0  anc/lean/formal/Erdos7/ThreePrime/Charges.lean
5c6b528f2d341c7f1172604999296483332200325aa996e87bdc9d6ebc1d222f  anc/lean/formal/Erdos7/ThreePrime/Cofactors.lean
ddbbfda608f1c600e6544e0cbb6f79bf641db3a4b1dcbf7f43ac4d7556c4b677  anc/lean/formal/Erdos7/ThreePrime/Comparison.lean
d7cbbf11e469c25bdd48628a2c3f3ed928a41d19967f9f7dfba9cb8ef3270b6c  anc/lean/formal/Erdos7/ThreePrime/Counts.lean
bb8e751513046e494c8aa3bebca176ae120b299302d5b867ef524d174de44e61  anc/lean/formal/Erdos7/ThreePrime/CylinderModel.lean
37c43712fdbfb4ea695e6ddd0329750e969ddc919f559692f9d4fd74291efd57  anc/lean/formal/Erdos7/ThreePrime/DistortionChain.lean
95b3dc5d24b49f7684a9f7486aa18f0ea5d0cef45e72bc1bc870a5b2dc21039c  anc/lean/formal/Erdos7/ThreePrime/EarlyBounds.lean
d03c25f5cb6bfc4ae79e1b9424189fbf925cbac0837f34b6ac7625b94053a1ba  anc/lean/formal/Erdos7/ThreePrime/EarlyCertificate.lean
1744fd779a416e814eba7405fe371aab3117200d90732b19954dd92aece438da  anc/lean/formal/Erdos7/ThreePrime/FiniteChargeBounds.lean
335f582ac4f72f2ae92f905c02161c5bc2526c9ff9b0207ba31ee412771c3d39  anc/lean/formal/Erdos7/ThreePrime/FullSchedule.lean
f0a2f517cdfa4cfe2f52063e8477cec9f8f59ad81a7d216df6cf07690b2b8018  anc/lean/formal/Erdos7/ThreePrime/Geometric.lean
eec28126d98565668cc966cc0aea5c548466d31882079b21889d079ee282e094  anc/lean/formal/Erdos7/ThreePrime/HeadCertificate.lean
039333ed942be34b8c578cab042218e06001f6f42b9f43c6b69698065f3a7d31  anc/lean/formal/Erdos7/ThreePrime/HeadMoments.lean
0d4e082d52ef48f90c98d6e1907ef9f581377d33897ae7ef542bd225bedbc067  anc/lean/formal/Erdos7/ThreePrime/HingeCertificate.lean
c3b66ea9a08ae897d927e7fe059a9526d16f2214d2a18ed82584b4a0e43dc450  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0071.lean
c370e68e04be1f652d8e0d7b6619f6cc17ee32eeab489e3f723fc95ed452348a  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0073.lean
8e74fb8dd9e39bdbd567c385c70011f1881ddeb913880460ea4cf55c07ffa843  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0079.lean
99133a3247a76b43eca799c97c449b7a4eb09b18e4e0ec26ac116621e1c97257  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0083.lean
ef7446b13aa3e1b94fe60a1540c5869698b87107b9c849b7124603db92c7d40a  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0089.lean
2423b8beb4205354f3a9bd6f9a2d7adf3a4db9f3152b917dba9ca90c05c5ffe2  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0097.lean
e993f2a2859bf2335e54be8cdc8c6eb5ceb5706a9afa5c8878ba7fa3825ca2b9  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0101.lean
dfcc56f28fe39d9ce8488aafeb9ad3c0ab625ccf473cffde7a3f1b1ccbbf0397  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0103.lean
85a4a7c13f190f0f7d3247880e42c690f32fa31d67189c75f792251116ac1f2d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0107.lean
59747e1a5fbd439c8ff61c9a33ab04e8d3002fbdb96c934c4cc2fccbfb4abfc3  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0109.lean
9c2c5a61c638dba66a60c1077f3fff1e552ee38a0eb17de9d0b9d1b9f892027f  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0113.lean
ba1f3a6f623de7321182ac720350ca4f867540a1364c16023868c31471e4e970  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0127.lean
5ee454464d2d0916fada5b48a7ed6d5050c9794703ebf4ae63e508f2947b6882  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0131.lean
c3eeb0f9fba1cd751602247676d67123e946d29d54040ad89cb5d9dc44682e81  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0137.lean
c4efc154f85c183e5f14510d8b4a925e108213ffadc2f05716cfe366ad05bddc  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0139.lean
483b825a2ce32d96e8fda5e8d556cb6c00de8649fb69741da5b144e732f32b5c  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0149.lean
5428229dd7aa7bf5fb65336b37a95915bf4938d62c0fa092d3436c9f019f9460  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0151.lean
20ad9654eeaef7b3f7ed1786ab18b12434c810d3a3ca20043e3bf54996ba935b  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0157.lean
5caea74ce7528803c9aeba341179b18027659342c938cd46b304620ec6970c17  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0163.lean
a0d7a5e25cc4b1fcd04275cf25d339ac8284d542b5e962250fa32723cdcc7ad9  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0167.lean
fe477e33fabd5da4c908efdc5bdfd4849ef72678eb05fc069389931dce07a445  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0173.lean
6c68012467d46d21ccb58fc64b14b1dc9c6e767e6eded4a2e15cad5fc10d013d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0179.lean
b08dfba9c75f20dcedbf0e72814052a5b0297985ff7bc3c894c6d4fe5a9156cf  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0181.lean
1325a27bb38b1f9d0ac3036a3e9ca27fe51400d014e3bf42382450d74c96ee15  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0191.lean
10922f188e8f4a23ca517acc428c830f7530ef21830d547866ef5c84c397ee1c  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0193.lean
30e931eae2b5746f71a439142268f4c739b544b5c8463834b450ba5058207813  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0197.lean
a727355d3ccdaea39258ef9eaf2446a562cf6d45ff82933e369e0a691098944d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0199.lean
38bc12f7358009e87fd5065da7bf04e69640e39a8806c1387d7e25fc9900f0c5  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0211.lean
fc8a066d7693c24cf7b53b52fc9a728da1305455dda205cd9cc01103ed96bda0  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0223.lean
34aef071b0ed23c35bf89ce1aa9ad7555df27f561e89869a820ad349ad0eb7b7  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0227.lean
2f726fa0fd107b78fa701f97aaedc549a386514e828a83d8b5be959fd0f56b6f  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0229.lean
d58a1f768a7ae51776dc474f3e029725adc933a22f24ff856b666b005fa83373  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0233.lean
dc0549cea6930648d26c3080e1f27b242b52c52197e34c32eb33ec101a33d903  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0239.lean
5eb675e636b49023c9f9efaa3577c8eaab1ed84450a2635b8bac59c5ed0b71b8  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0241.lean
ed310deb21c614ed15a14a7f6d042bbf731b5491b953e3ed466391c11902c052  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0251.lean
e620ac23c99ebf7fe9ce8ced0dad7a1b3cae32f735be5298a5b3a3d29d2331d3  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0257.lean
9736d45e2c6711281c10f5ddee31bd655845e8da2e6f366418a1c16e03dae714  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0263.lean
533dfca32af8c6442f0823daf17e2043120e52563f3ca36c6e4887d58d0296cc  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0269.lean
4d475d5b2a9dc878bef69cd40f19153956500df984d8b1e26e007c0b026db4a0  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0271.lean
e577064fb20a2284cd6c8ab4d4092d7a92ecaf9321c88c45251191aaecb0ef61  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0277.lean
99e7dc22047315f5b675183c609a30648d7030532fbedab9ae9984c28180022b  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0281.lean
3b3e2829ba8c925a8df2207c9743d8af40c669825cb533e8c4a8de3456b9df2b  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0283.lean
50ed45aeae933502cf926e91a28436c0dfa17edf21cb2847a432c6edddddeb29  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0293.lean
b1326ea3abea0899a538826191c209459629cc3e591c53157b750eb71558a86c  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0307.lean
e1ec85d7de71e27f0465006af92c57179244096131a1ea344bbba0a01dade8b4  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0311.lean
07fa7c909749452b48ecdf269f4a07dbe595b23bdf0840260bbd3a4188f717e6  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0313.lean
fe8656f0768d27db968c7488b00665fd2bed205f4ec44cdcdecb0e7608b165f9  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0317.lean
8ca09ec9e9d2dc585c0d2f396e8c90b10820283266b23d609ff32d58182490bc  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0331.lean
2b320618bd46368daa0bbe6ad538f7404fafea550c7a391f242fc16dcfc3508d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0337.lean
42cb7ab539e58116321dae4346094edad928e331a0420af3b30eeb39d43a20c3  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0347.lean
b3966e4f373515d8695658ff55caf8017b0eb86e73cabef9b075675daec557c8  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0349.lean
4c3a5295eb7eaa8d89d8c2e2434c0de6564bc4ebfad02c9c497e7751c48ab7f9  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0353.lean
548169cc600529ca61045a70edb450fd15a0eb73f37f4d6af5bbf0fb72e6c980  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0359.lean
9a260959733649eb940c70e81657ba271452f9fe3399527952d71379a6770224  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0367.lean
d43f608b24251bf9d53d14b4e0b6d2b1043d9929ef1bcd4eb77893212a952d93  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0373.lean
218b4bec3f97073287fedba126a31588663340edd2d8643084b87dd562f39b13  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0379.lean
11850bd83fc8d26d7c59d9d088f8ab4a0b9ee4cea499c672592fd955a419cf42  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0383.lean
da304286ce95285d9c5e793d5e1161bbf108eb2d57b9aebc9b96f1e7b98774b0  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0389.lean
0a176db9d0c13b956075625e9eec3af718ba19edd01282c71591f75a0e910f24  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0397.lean
c4428c2694778e1090fb11c1f91d7ca20ea14b2d3202492176bdec94ec4f0c41  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0401.lean
eee08f07d2c934edba512048f781253d2568c416f7395d952cc476e58c8f7b5e  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0409.lean
c321d923f5008ad390d2edda2e04b6887d744a771e3567078e784c26c50d6eff  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0419.lean
7479103d0550114710b76782446e87cfd995d435eff291d3689d33093df137ad  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0421.lean
83d9b409a1d68ef604e80d9ef4a23af358b958a89fe6d57490779f93dfc84731  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0431.lean
76060e9060904fc9450e216b5118dc077d086e1c73cdccdbbf09b2a8163843ab  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0433.lean
a97e2b4dd7d11a9cdab8542c6c20a138679c07be67812d9d074a439c88a0f5f7  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0439.lean
f72ac14fb3074d60d4b83a5b114386839a3f85724a5488bb936472e962d55eb4  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0443.lean
971733eba8c0c7d447c890a3cdc77bed4e47665702d5271d17259fb1509025f2  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0449.lean
52b639d1fcfadbae18e68bca63b515603241d9504248913bb20efd109e564e0a  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0457.lean
ff8b8075506a2870a949b96b20f1c9fe47546e48d6db854c2eea343d455ead7d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0461.lean
fa2814adfdfac0465da14e1c8c6b719443f562b3c72cbded2d319b6f7973e738  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0463.lean
0ef88d35eaf0e145c86b6c51a380937e18c16daf0d403f4672dbf7f819bc1fee  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0467.lean
efc1abe85dbcf3bc6a93d171456e8c1ad24686f926fc3678c49a6545354ba99e  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0479.lean
4f6973cb55fe7883148742b8a5499bdc149cd5b74c25aa66180ec22676f6fd20  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0487.lean
6010c8c21db1c2fe5e05a409806b0e57845877c7a3ce559cd456533f14759a3d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0491.lean
e9730bb59454db6ae1df2a827b71ffdc4c73e28696fcf50b75bd951ca5b31d05  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0499.lean
7c05802f703af28bca26dcc046c01bee06c8863564160994b06a6ab3d24aee95  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0503.lean
82b3a4970ec5fd1f3971ba781386f6f614f0015ea577057f655d7c62fd0e4be0  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0509.lean
ae117c6fca91d78494c5fa37a5f7b636097b141f3e85454ffbaf28d7afbb40e7  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0521.lean
c66e270f6a1150c2e08f46e21e5f03795d1b19281c88a77542a499e2642dea23  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0523.lean
a894c931f9327de0b3c8a410c2d71343dc1964a154c121ce45e022400d02b977  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0541.lean
1d3ecb08a7a80773e42ad4d1c0f8e4966e44ecbb71f03dc9c1613fa1235245fc  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0547.lean
d31bd95df8b88da35454d1b2593dc3e5f122efcdab0a40b62eff8adaed42951e  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0557.lean
80139eb21424dbecc4da66dbce1a52592aa9fcfb5df22a2e45a0d7b966904530  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0563.lean
c3e356d462b53e4f6033f155b7f80e38708c59a95da9a9f70dd135ae2b6ed6ac  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0569.lean
c5613e2f0cdd3b4fa606f729d13c384276a913f75006ca93c450fabc82edb7a8  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0571.lean
71bb4c057a07b8a0ae97452c6c5110c2262f20c17fb854aad8d89c9c9bf8399e  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0577.lean
5b86c79d638d6f025a048174182fe89b3ed3674c3736e8e1f7d6bc296b2fb54d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0587.lean
ad419a7f96cbfc5c9725942d190f1a93d8161d963dcd0f5d451fd262317abac6  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0593.lean
3cddc194b200ce808cc93f293f618ec56a922681304983e307d937da103b12a7  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0599.lean
9ee7b9df602d35abb1ad61706307d22af1a9eed2173e06d111f8987fac7c3674  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0601.lean
44cc021078d381043573da642c7229235016379f315e203954389c7c73d726eb  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0607.lean
c23441bf1c4bb8fcc417f1c4770ae91894c4cdd1df0bc605ec9b0c2cb269c28e  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0613.lean
a6fe12c31e143253b8ef931d8a956c56e88d541a5241ddeb28bfb5cd1cc6caf2  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0617.lean
a19feec0ca1c0826f58cf596d9437435cd0236b89ac8cf3bf75e1f5e6546cc03  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0619.lean
cb86944db7bb07789ebba68b1278fa28630703d3aa82781f3cbd7c9c1f84e875  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0631.lean
17cb0255e94a31b451936d70ba4789db498eca9531cfa0c07e9d26b09c412018  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0641.lean
fbc3fdf4ec1579eb8a44841512deec2c077d684e30e4fa715687d87a1a23ddb5  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0643.lean
0617d8a81299857e40e16e2f180241a49188c09c2adf47a02e241ccb23e63b91  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0647.lean
b892cc731c89f3333f731f2d7987670b9883e9623eebd3a3b52260f9e61e9ec3  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0653.lean
27e222fc3026d7594e6fc9d230c335666ac5a0458209705f5de6a1a012d3cab9  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0659.lean
f0018a434a5face9f2d453d95cbf246652e7a4ad9498fba39670939271e927c5  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0661.lean
263a494744ffcd6d78ed10d5fd69f445090c2a46a452d149fd620eb1301f5503  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0673.lean
a7bef0259613b5e46881f659d5378dbed14ac4b413a42d3bbdf9bb9b6eadb4e4  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0677.lean
6864651ef868b64d4edca57b847e4dd4efab41416d626aeafb34df47c59bd06b  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0683.lean
6c2bcf43578b5c8514b174f78b63c2b3a089b15193011757635daa1697bdcf12  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0691.lean
b863ab8b730eaf06e3a50774bae3ad504ca1cd5be263e4042052cb5c9dd16cda  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0701.lean
c669f3a4a1f907e43f02ee52d2a2055e589028abf356774a09624c3799b9f96f  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0709.lean
a5f172b7edd0325ec150c1ffbaf33c752b450e34d18690785cd1f05cac87dada  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0719.lean
bcdc44cc78587da52780f759e2fd27a8b1c8775e96f8fffe2dd1a3779f287493  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0727.lean
6108842ae56b2a858a0818729bd05ee8a340729acd42c7d3c0d24148b6c85c4a  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0733.lean
e7fbb1f83e408f97edce14c0fe2986243f0ccce717fd260f95048f84469d0e55  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0739.lean
50759c261b447f522853ea44a859c41087c64614bc25adbaf97150e311b9b161  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0743.lean
a6ab85e1441988603023e4804b3745428c2b1ede1cc64ade8ed6403138b2a36f  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0751.lean
8f382db2a250e96341c5c87c38e74b82f57162e41b25c299705989ec9c4d3903  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0757.lean
81487a05f26f12aafc53508f95533f3c39c250b71fc369fbfe4f41fb7db4b02a  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0761.lean
5add7e93d6c8a60cf2e967d9d4ecc359770b93f0d0bc7e3858d75d1646013f0c  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0769.lean
854a3b584997acbcfbffce91bb2ec26bdb1a297acbd102afe6c59a1414abb022  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0773.lean
5a61bd55bc8e468e73a8cad052dbd20e5a46e24ffa5882cb5492475692b6cde1  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0787.lean
d38419bbb3e3576fcd3b38d19a940ec000628957df6802cb3e289eae6148ec67  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0797.lean
340abb7a56844462fdbe359c66f8f72a6ccc64e448fbef20838031351769dc5c  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0809.lean
c4cf81b347f13112e4b77522d8d02c407d602d20f125d9217a3045dae1fec64e  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0811.lean
0d7e96686559f11cfe90eb11d1ea41905fcee08292dbbb381212bc5840728359  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0821.lean
95d61f3e0c595fcd4f5aed9094305a78f08545dd69b3c4d86a64afcc74aed9c4  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0823.lean
7b0b3084ea8f9895ae79d93ef9b5aab23c44573227d68345b9fd952c8575392a  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0827.lean
25d981d7ea58e7e199ae5632f4b0f6d427e8fe6518bba7a5fe23eb3ba085820e  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0829.lean
b286c461d61cb5769c258d76af95e74e24a2fde1cd912f72f3ceb1ffc090259f  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0839.lean
870765a76d307ee367bb7c978da97cc284b6d90b51908819a0049a8e4d67f154  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0853.lean
c735d559756dcf1233f16757cdfc331b1dc235645f2aed61eaa2895acc524afe  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0857.lean
dd177567c3980511837d51d3b3f996c871c51310bd7cd7f80cf7b0df35b46195  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0859.lean
c123b93388e8a1e7b318005140add732fced2240ebba0a3af67538ac85b5d1cb  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0863.lean
91441360883d0ff23317be13cc44e7b8a4b1dd3a1fad9efd53b51610bf89fb49  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0877.lean
12aed6f11925e89c50049cd9666eec8356a8c702651f195d63f1bdcdd6122fe1  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0881.lean
e4c83b82066a453f050105419f5667b12d456c620fabce132bd9bb1f4da65fd1  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0883.lean
576bb0936a9453746e6082587c8d83869af2800be5cb3c3ae620c9ac956b7c98  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0887.lean
a7ed6e7ab08ef094d066b21544d772a89b9687fc8f0f8aa952078f43a846070b  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0907.lean
014434facc5d4744f062de11bd84d1bf9083c3d4ab53ccda9d47f23cbbf302cc  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0911.lean
4465226528f975f0ff3ca4b913d541b28248c151c9904e605df22482f289ec85  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0919.lean
d598d98e372b28ec5222c5f9910d740700f0516ead609d46b7a3a8bdf6ac6a98  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0929.lean
82dae3893981b1dd5745bf804c258b04d599f54e36b62057ac42b709d39b2e28  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0937.lean
0e3dba733ea2d85c2dd0472c2d17fbbde83d036a3be65d4a10c53b5a311049eb  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0941.lean
3a602179859db000ad7c29074b2feaa7318dd8e4133334779b3162ed9c6a5caa  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0947.lean
375ebf30364621a6d35fc80a78c6e489e5e00531cb470aeadbbc65f05846277d  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0953.lean
65440253df73f5148f047ab2e6be8f3a0e087993aea068feb0a445f84eac5682  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0967.lean
0ffab751e0b3833f08291578073821ebde9f56bcdc956e745fef4956eac059df  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0971.lean
4af0b5151ab9133cb0e27fbfec19f5f7c8df4c0cf9dbba6ebdc4f7a825defd75  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0977.lean
61a17dae93a267cf9c9777c8dd554c690336af888572d8551cb155b0e2bab3c0  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0983.lean
622d7cb5ea9b7c7b08da5cf420177e9f01e3cc6589f623731ef5e3d7d24752d1  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0991.lean
705e04b537905d7aaa4566bcbfa74c39e02483edd3e11d71cae8f76d938d52a0  anc/lean/formal/Erdos7/ThreePrime/LateCertificate/P0997.lean
747a233d1daa4c882a3071e847f3026f0c080bef319c6ed1009e7369e8ed00cc  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0003.lean
a7ec76db88cb48eac0e6992aee33462de29b4244059174ad48b409a9b67688c0  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0005.lean
fcd6e0f004241026df731158e5c2ccc81326528bfc29cdbd359812e2ffc8d8e4  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0007.lean
a88aa16c308f9b48b8034c893a2b9c478d1cdfb2032cff2b5cf3e658ee8b6c8a  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0011.lean
239b185d19f83c86bdd399d2a12ed30253521513eac0fa11512f6402d51a7197  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0013.lean
af3e691a34809207467b788a4dd9bbd3cc2b90e173110a747fb6ec41259dbf1a  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0017.lean
45ce0996cbac1c2f063f0beabf2d8e1a00daf2ed2b15bd06aa7aea21c4db2c91  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0019.lean
f686bd41ef8378eead638e6c36b8b8bb829ecb97f350199baed64c0dca07e497  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0023.lean
a14b700c8110dac3f0227c1e9ad5ace668b5f92ae9070f6e8c3bc569eeda624a  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0029.lean
559ef4ed77711144f155b84780e1225de4d8b677920408f6a85cbb33747ca6af  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0031.lean
9ace44b4b63aa6af50baa76481b9dceb85724525cd80d4c98b346cada47eb8ef  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0037.lean
825d2cc04a152a4db26659c4132aa6be96045ff6bc78be54e5efb0370037867c  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0041.lean
b7ba24fdcf4ddd52204a8c1a6331e42a7927017cceb656778de0fe19c8fea19f  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0043.lean
1c0634afc4cc0cce23f33168a5c5077d4ac3a5affcc4cb6b1d69139284704eed  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0047.lean
e8b85046e23b17315abdc68b84564cd1779269341eb32ed17007dbc52601ee8f  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0053.lean
3f9213ef7c643216fd8d53a4b47a3d10d719428bd3c6b9dcd97a9e6113c90c16  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0059.lean
8da631f600d3d767ec52524255f619a27242dd1796a283c5ca4454d2aabded08  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0061.lean
fc9e2785d2fc1b8661c284c5657ed5935f938a7851766a1ba284f38ca73ebdfb  anc/lean/formal/Erdos7/ThreePrime/LowCertificate/P0067.lean
ca70f6fd100daaea96a759a470d517c6f837acc5c30cf0ed7d1a31e859d788f1  anc/lean/formal/Erdos7/ThreePrime/LowCertificateData.lean
d0224f844a46784b066e1f20943b65ea73d555d21ccdc82b67182b4aa05e230b  anc/lean/formal/Erdos7/ThreePrime/LowGeometry.lean
5082de4c689e770825b720337917338688141b8533c0650ef87c8732436f17f7  anc/lean/formal/Erdos7/ThreePrime/LowInteger.lean
8fbe23dc473d586523c2feaa6a4a9a3f044ef5541d3847ba85d2fb3de395843a  anc/lean/formal/Erdos7/ThreePrime/LowStates.lean
dff4e90e62a25dc4fa488331520c95996413f27d39a20150f3b42ea7579296e7  anc/lean/formal/Erdos7/ThreePrime/Model.lean
8c328a70eace949411612078c71a5cd30c30afc0403f8c41c8469bb32d3637ec  anc/lean/formal/Erdos7/ThreePrime/ModelCharges.lean
b0068149bf642fd33137b7894d855424e3e695ac1c3d5fa8d6b14a8084ebcd01  anc/lean/formal/Erdos7/ThreePrime/ModelMetadata.lean
ae8e08d65d84b9873e2227a0f2ae677523e9d9d038b3ca397d3381381086597a  anc/lean/formal/Erdos7/ThreePrime/ModelSemantics.lean
d6338aede24b87b0bd07281246d77bb0f9e7b0fcf489128d6dd6dd34e58eea57  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0003.lean
58f6e6f6d420b50b7a0939de8e75f1d3db7d7c09c4a69e130fcefdd993ddd389  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0005.lean
add42c93e9974b1bfaed819206adbb31212148376ae8dcd91b2a95d568c939ee  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0007.lean
3cf4efea6ba207946036841074009459ddfd78d3f02cc98f8f872c99a58707f7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0011.lean
cd08433695a3b83d7bdcbb3619bc103f27b248066d65e036391069505fa93bb3  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0013.lean
6049d5ad39a2b93199707d5f0bf0b03392704324acd339d1c1bf04a4886b4173  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0017.lean
453a5e8d70f4211c649762df2a47ba594b2451e4d4a86eb5238e34029ea1e3de  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0019.lean
8aef31357fd2e0533f2b72f4d79bdd255bf5f63f68f38b8880224070deeadc38  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0023.lean
621e8e28e16ba5bb60684c2a878b436f613235cdbabc0aa7922e284a1659cedd  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0029.lean
87db9ecabf37d076cb239710c66d6fc8fe6c15e0a52254dfd807cbfa60507e73  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0031.lean
b3ad35b32c304d5e3162d8e2df2ce678dcd29f02d15752f97506b2602767fdbb  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0037.lean
cfffd33a764f49b9c82c4cf69dcf783a62ad0868d5d1f18e21441adc430132be  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0041.lean
32e5f6f96c7872484717c4dcd715e69069989169bc4005b79e8ff5dd5965e419  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0043.lean
6e1798fa115a17e7da8d3d3509fb2bf52b77b2c4828cf3147d8cdbed7f140db4  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0047.lean
c96bd5cac2a046264cbc95bd8efb9f1ee95c51c6ad3683e00d2652ca53317543  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0053.lean
f9a3de608dfc4100e2f4fbb997ab3ccbc801f8cefeec66f1afdc655d17441249  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0059.lean
9cd6dd43a0e27183f95b91b078bb717107f1d3c7f78b250eaf5cff24f94337a0  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0061.lean
2fe57eeb163662253ed8dbc113cca6beaf8b55feecc486f4c282c074bb7faa45  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0067.lean
a88f6d8f205d9f3a530c2a4e8bd8f8a7d69db2450438682ac4f510f228f6581d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0071.lean
a5512bb63804fed73438c9e7cd1d3459a28da3e32a8632188a04b98dd00523f2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0073.lean
bd3ef41fcb71c8d69e0aa51390fe4498ab2b263dd7b42ce25c04820e7b965175  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0079.lean
e2fe546defd2db90bf67fd105434ba652110774d311eb4ef86c6dfe4f8ac3d92  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0083.lean
070f3baf4ea7366512fd6c9172de8a5e1521e33e5a387b4120f49b92340201c3  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0089.lean
9def35916d734785acb3d1f525e9efd3d109c98ab8b46d476d477d670a1b8f44  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0097.lean
b3c441412b0cb01d4a041050f3991e83fb3deb053efb73cf6ee5c03fa0df52c2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0101.lean
e9cec8d1866cda689c35b19d91f304aa4d4ac1e0f0c002f968c7f12be60178dc  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0103.lean
d8564a9692e6c7249abb565c696e63f270a21ab2da4e7f155b2ab015a7d37510  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0107.lean
c0a22515a979e1900c4a9f9593d29893bb2a876999c4045370eb83aff2e57bdf  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0109.lean
10e7eb3803119d4c1f95e7591e09c307bef7ea647cdc0cf584da29f50b12f3b4  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0113.lean
8b797f9ee7c22f3904c0f54c680bf4252d23036fe889c9543c7d7e89c4a6651a  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0127.lean
f36ae1187b81c504b28880da2ecbc66a60daeef7a74651bbbddaaaed2838506e  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0131.lean
f5f8be79ff17c3884eebd52054091099ba25278a9120b3e342133e3f43bde8c2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0137.lean
b5f21914c37ada969e8db39917c6f1a7eb290039fc67c294129f6fe0fe7ceb19  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0139.lean
59ea2fab207c124723da58475273fe1b17be39862f7f08fac5edc186fc24dea6  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0149.lean
7fb4b77aef2b30a0d43ea3627e86771d9f53fa5d1ef35a94c78512716c560524  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0151.lean
98f1918b865b8899d8d8c3141cea7b6617aa82f8e1cefa636a49ae8d5f702654  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0157.lean
ca8dafdc7382f1221a5f15e34c486ddc37668f3ba62ce85f4f84df821ebf9b90  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0163.lean
783cbf61cebabdc4ae709cf3c572cc1b8e398821ccdb35886b1fcb761bbb5eae  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0167.lean
91a0f9c50c6e920bf11b4586167f87b30f755963f6dd31e5c3a995a0abd42734  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0173.lean
fecb1a9792c65fab05ea6a167d5e53c8d479015b9a6cbf06d91cbc2d84cfc7f8  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0179.lean
8e82ff17f57fd9d540406f8c7e97aaa1baf1f2d4c6276666f255c7ad9982be34  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0181.lean
6125104466d8a2c668ee0796f39492bec6bc02ac26d230a1340fa467a0d0431b  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0191.lean
8bff9e104f03e70a8e5424d9058ba0d144376e3d8a437b9361487f099684bf75  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0193.lean
d7ee5d6eddc48302d967b27133a3be99ed0400121938c21b3cf23fad1f67c3e1  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0197.lean
c5db3ca6d0bd8b8a441958180bda93ec9c73f3794d8cd76ac828ac2091238bd8  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0199.lean
cd4a526953bc3c590d4f5834203134498ce0fd13476128bc339b575874ec6ac2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0211.lean
d0801d399afbfee6b87ec902f8ff5a7a6bda1cb448608d436ac536da0cb2ce5c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0223.lean
bbc4495cffcb4d269dc6b598d3ed63cc282ec1e07f8f929ab1a4356361c6adf0  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0227.lean
22957411b13c37a7bcbc4109358e69530d5fa3490436c6992c64b9cbe63d6a72  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0229.lean
daf1c5b1ab0ffb92f3e532353260e5b6bc7294277eba08a9534cfd1d3c7d503c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0233.lean
cabfcff1761275306ce1ad9d9f5f7ba33a91f4ec712da991c7a73c5e3b8c0be9  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0239.lean
e62f81ba9958dfcb41e5fb1e7e89b05b5d01c1d22eb92dce577fabecce9ccbb2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0241.lean
28dff3a70e3ef9a008b13e452921818cfa4d0bfc506b7cfc111f405e8d2a73f5  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0251.lean
f5472dba43ed37db884c4246375f2196581b74ba7b8eb382336c16b4bb835430  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0257.lean
f7ce8f59d8548b0cff6f3c58da62f19c63c3c0e8ca5b4c79a6af827b1cc3dc22  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0263.lean
7fe3c96e8f173825e9185321c15ad731a45ea67951a0229e96552e80d685ece7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0269.lean
9a0a3972c8afa0e7fac59cc83637d714cc54b0c6ab953cdfd1f27f70f403b9fe  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0271.lean
3bfa55e6212c945e62bb3e4e636782cad4a9441b5c606f7b715e19dc7adc412c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0277.lean
6166e209626f149c53d064e1959472b6d2ecdf10863bc23e14cead04329d9a57  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0281.lean
5925dc7ec127fe1ba9c8ba88b57c1a1917411b28e75d64bac188839d3b693977  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0283.lean
d149968a6a8f3b021707155d73f87522b6fb8b4a52bd1efec47c51a0f850643a  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0293.lean
c6123b5a227535d7f6e2798edc9f4d98dfb97eaea2890bd4f1260ad66a0d4a5d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0307.lean
9a621bb21a8288b09f061c7d0244c117a2c3ffefedceb302731023b8c513acc9  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0311.lean
c7825bc3f009b1c0c0d5e267438009f9e18375c746ba3969c664093dd2a16518  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0313.lean
382309ebc9076c4961eddd98a9a29149d7cbed309f3f2dab9333a98e63403acf  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0317.lean
c1d26d1d882d158e547d5070ad58cadf02ba84810dc77ea980dded3201d832c7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0331.lean
3b64cbc87f7b52595c9a481495ccd25a167a721d6d6bcc0183db0408f959b6c7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0337.lean
754e4b4379b68051a0f2f2189e95a470fa4e119b154080778423aceb1cfe998c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0347.lean
956ee3fa75b93cece1c9ed1e93e36dab7a1a26d47c9777cf49d915009203fdd3  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0349.lean
9ed9a688d3e8800fa61a6ceb696ad7a7da8cdbce2a5a02788ae1b4f5aaac0cfe  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0353.lean
93de8c80552366128ae53da7dd822c69029f10682e30f9ff374e7199899360b2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0359.lean
12dbe0470d62d9a1407639196719440a3933c6bd7ed5c7f55202a914f66af8e3  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0367.lean
1692a66d2c977fe9e12bc3e63d7d81c145aff2d48311a946d2d357e4569a408e  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0373.lean
fdfa8e404a9c4d68b862b06cc0d0225fa869ff5ae0ac928083e757dac3e1351c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0379.lean
f41a8f00595908b2cee78e0ce05346317c2dbf1abcd27fafbcf81f71c0e1c81a  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0383.lean
ed3c332651f1b1eb7a30b97250a7fbf2387b732efc5aa2c25714f3c12c972f2c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0389.lean
e6346236ef7983b49951a43968f1edfe33666d1153f0579c9531dae2e1a06466  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0397.lean
6fbd85e0c37c35ee481d64714ea9b109cb06baba8a840f907b72b7c957b22557  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0401.lean
2fab59e38e72788635e2a31524388d5d47dae10f7ab52999ab0e1ce1265f911a  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0409.lean
0e8d421e3d9c90a683e9d9d0e6c396cb674ef8d496f63a06875e0c35ec71b217  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0419.lean
e7ff4dc10caa7da42c0c6061fa5f585694b4ebccdea4e2dcfd11ba4d2e704001  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0421.lean
b13dfd918791e22184cd4cb72ce6e8dce9dba0b16575d9b75b6bf82bd87de852  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0431.lean
663b95a218ff44f9245eebe21f006d07b140eb11d7ad66df5d2c267f65c9e196  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0433.lean
374760701b8dc31d672f42233675e243dba523a00d8ec5fc86e207a5662bfbbd  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0439.lean
0dc23e97335106c774cfc5a2964f125316e561d091622b6b89396e6f078c912d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0443.lean
ead152a1eb30e05976d58e8b46723ec78c404ed09db7ffa11db7cf51223442a8  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0449.lean
fce21406d71b12488eee5acaae253b435642d45f635d3330906abb17762cf017  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0457.lean
248b7baee2ccf09be9ee435bf5064f9033370c236d40d88d724ab92e359a9b9d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0461.lean
86df117842cda144d89aa27b63c47944190da335bcbb63b2257ccd75f49adee3  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0463.lean
37664564e58ede421def00bfd14286b7cbc7565df2f8acdc944e27aa9099c026  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0467.lean
cf157102576f7355f4785b01c44937f402e77d3c33ed58a4b06404c41ff40a1f  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0479.lean
fff08bda6c5b5bce01c227cfea539dea9cc263fea88c7087b304048759573b12  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0487.lean
352cddbaec1293341f3ca3367efd93990251f13902288f640625ee17e2e3c208  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0491.lean
5d324ed51b414a34c32b587286adfe06a7c12b39cb859dbb872c2138858acfd0  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0499.lean
6bb1bd8c9826b65f4d442332b3da7e2e51016a7303955dbad847b961358125aa  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0503.lean
8e98f082c48b8f42c14b335e637fc7ce4d3f706d31f247ee3f1115d604ecbd46  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0509.lean
bede1514e0c2e380259b4fa6b642d95f83b1d942bfb1c378b582b22e4c1b5c4d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0521.lean
12e9bef47cc8bd12960eced96bca32171e51b4ab065bd9636ff890ff8d379781  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0523.lean
9f37103847bece03b6cd23f020aa4bfa1f158773a86b90d1bf72bcd3b218acfc  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0541.lean
6585fe2a36b554931beb8860581b9316acbffce05e1398819a3a4a5a8e2b9255  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0547.lean
739729a8e7b0072f957370bb6a3bf4642bc9ac15de2d18e4db8398576b7e459b  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0557.lean
ece579e4a703958bb50eb1a2739eb6cc782f9863a857deb129f3c201fb8faa5c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0563.lean
a1e0d44e80a759cd9832e9a9ea03c85799ab1867a0c83944e6b096bc9f6b1700  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0569.lean
b2a20c48f2219922ad7079a1250ce389fb32f4069d0ced05f09b492cbf5ee2f2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0571.lean
95456e94664dfb26051fcd4b0ea5eb20e1f37208132d880f7cb50f7b3fa2fa20  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0577.lean
f1ab9d7c225f6aff514da13168f9d6b97f2b14789c9fbcc3fb4970c830e644d4  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0587.lean
e0a7fc615439f083407ab914d3dd76374d1ffd6ea9cf9ce829973e020275b2ef  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0593.lean
452304a23474edfafaa586a9a58a41bbe32f9ea8639f4538cdb99bfff22a2510  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0599.lean
2e804c281f6bf6469dfc67468a043f2a5ad634d621f4bd31c50a51f9fa9818cc  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0601.lean
7ad9e2a24a090e1afd94ed4f933e63ff864ff1d02f5262efc30d704564b92290  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0607.lean
16c38cd188a2d83fdb7fa101e37b458c313707e113e000ae937f487ee5df64c7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0613.lean
e1d9325625de053ba12ff6e68e4c8618356b484440effcaf7584244664aecd6b  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0617.lean
df0969bc8505694990af7fcea8c37af6f19ba594ef1c1e235a71165d87b6ec34  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0619.lean
88ad5bf855da835c6ab8736cdf2fce26b8cb8d9fdf8e209b3dd4a5256c8107ba  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0631.lean
2afcf54993455f3d831ab99e833a7f3595b67f35de1f2c223dafa51f16e9a6cd  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0641.lean
e6cec503b69381ec00eb2c2ad89348c2ebfb600c3dab7ae45476a835551d6114  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0643.lean
226f83e379b7d8024b7c013f62c62b82c5a8b455bbdd827333d4406316bea19f  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0647.lean
91c208613679ec4ddfbe1ccf8c6398a80ca904eb14c5b29abf74d3f4b7bc509c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0653.lean
e19aa8c1b0228fd3096306d17ae98135400d8377244ebbd765bb5d23c1c4627e  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0659.lean
07f89a533d8d11ddcbdcc0c6bedd1d33b869b24a8cde42ae7eb1601ff365ff89  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0661.lean
9fc076ef3dc367c41326ddaba69b41c349529a690be6f35b04f08b7b2c7025b5  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0673.lean
3cb12bee047f43aff01748d6ddea3cebef15bdb868932601463cbc71d67023ec  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0677.lean
19e91c80321fbe0fb36c5d4bbe76bc1b282653c85865d849f60fac3bf494608b  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0683.lean
c40dea15a1c1874a67fb9ba83cf4493d3f6cb475e9df1af6aaaf69c381cb89ea  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0691.lean
ffc7e7460395363caa97f05e361c76fa6c8841fa79b92cd6c5410743f4215ec2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0701.lean
a3aefc77a8dd5f0674aaca48cc53084fdf1f465397d0c01bedb7148010c65cd7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0709.lean
b0cf8eb17aa13fa9be17092e80e4e89a8ca5a1d63f57f1667e6625b0aba1af7d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0719.lean
12c9ce075b36a85a4a12d568d0d8bba143e213cb86f7880598d05fe38a5cf09d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0727.lean
f0b6d1aa831f16942e0050fe1febbaa3c37251d0b169520c38857e5cd815676c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0733.lean
d65fcf82c7778a6e263184f31400e453cab13e0434cf5534e6d624b6f7f2276d  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0739.lean
bfb53bd0729c3ac526ec13f5bdcc95a0fa40e71793d3871f04f00eecd1eb5b77  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0743.lean
8de3fbbda731453894e1ce3cc6c3756fc1b4e7427de421ba0a153df902bdd953  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0751.lean
8253ff88a40bef93c29ab36683e7a15e0caf0f15b06752c5a803a66010918a94  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0757.lean
cad57611b3e7562bf7185813624d1a4db1c464bd6dc486b71915d9c8ee1d36fc  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0761.lean
ab142440e89c1a3b498cf8331d4bc6e79e07252bde0e929a76f29adc2651994f  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0769.lean
f6722a9509e411e47c704f2033524f43e7132649d06e3571a43b8f585eb39a6e  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0773.lean
18c513186974b8e00d4e37d5a77586155f6501a0391ab25130f3278473f0df63  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0787.lean
c3f574cae9ccd7379f01d3c07f0f4a6d55d67c73a8736b579e863322e28c2efa  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0797.lean
8d1d9c2a26393fc485e28a18598fdc3a53a6842f3db9920940d7a56034ff1323  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0809.lean
b761590f5f34c6b06428fc51ad6889bd08f3c77032c48c88129492e39b5c53c5  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0811.lean
649f3bffcd0c4f331df121d5891e6acacac50fa5874408335ce8a9884ec18aaf  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0821.lean
6a2aba991c1c8078bea04e3606cf26e7e0e1a33fce37b4f41db77373166d2f6e  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0823.lean
0a5a608b7d4282a85dd84fd122255d3c40c561717e327eb378b0d663eee7ca2f  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0827.lean
3c82624957c070cfb6d2e27b21adb45c4f6860e3606f079a441fb87bf71abcb7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0829.lean
9b5a19fd6abd5dc831b7ec42218975657fd145e87a15d4a92bf8cfd8568e0b60  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0839.lean
8262d98624ffc89e21eabf9876348ffbae2f439bbbd907d304d3fa1c32fefbfa  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0853.lean
3836481a2be8d036ff4a087e3cc2ccad77af88bbc332d600f36b059039a8c80c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0857.lean
83508d6d6d02c5b7713a80e9a80548dae113656e34ed82dd834d152782766d09  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0859.lean
70982e1e00a594ada001f7ee6a9e52880891c2dc39c996ca29f8d3ccb0f48dd5  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0863.lean
581f17b302c2d7173ff20ab24bba1836342aad85722da71c1d6e8c5196575db2  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0877.lean
b905780146bd2ec332a41f36f6c14317e69f67178f3e728f0b449a8d3a644820  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0881.lean
86df694017bb83c03d98a0698000c68c7f42f11e4c17a0d28e47c565197649b4  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0883.lean
36ee125afb3f2c6416ab1de46ccf67bef001ad0c5a26334359e8c5ea78ce0dd8  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0887.lean
57f4275ecf59830bdf3d34be849ab94eb6ac286bdfbbcfb72dee29e9902b54e4  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0907.lean
d29be0b27cfb47640887b7ae5d819c2893ae9e9c65f0c21e7830ec47f19819d4  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0911.lean
1de428c71a2a555717afa9970ab90cd7212ba4f23f06f320b9143f35e067b797  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0919.lean
a44facfd1902ec925e5531231e5a4f840bb5363a49291c4a4759935c1f74cb68  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0929.lean
ee4cbbb5e8889bfd27a13694cc1d4c501a4a0480db420cf73a9c6ad4a2e8d378  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0937.lean
7c187cea89cc5be3b0a49514ee170f94f5cc7720d4b7c84b23378aa6a2c0ed5c  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0941.lean
36a10b016e06913ef284d6179901614c143c29586659cf3f8ebe11ebe33974c6  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0947.lean
85ce338402529e35f39806b231130237fa48fbae13bbb0dee6ab18249e0970bd  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0953.lean
8f10952252074d705f2bb97e692f2aa05edc730479dc1afa19c9a9c6376e1a3e  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0967.lean
f540e2bc82eea56ba99d86b6f8f67262f551b6e73d64bff793b2b4ffb81185b9  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0971.lean
6d6ea82f5eacf0db9724b76b09bcdd339ae722baed576eff930fc3031abaedf8  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0977.lean
ff72234b80d10aa11c9b5b83efe1587f411ee39403ba43b7b94dcb0de6766326  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0983.lean
f73a43b6b65673a296caac4afcfc1f6ba7c79b9b9eea30ba0cdc0b05c3cac181  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0991.lean
909dc630b827f7f62902da0ea1b77bbc0d89da7721d15e9edd9425820e6d5ba7  anc/lean/formal/Erdos7/ThreePrime/MomentCertificate/P0997.lean
7065dcd7ae8c10f7847c0772531df258749b3f4494f90f41eaf3f7d69a36c2ab  anc/lean/formal/Erdos7/ThreePrime/MomentIdentities.lean
c54d5084f110329dd73fb716b3c66b70d4c1ded8782eb1db880fb7628efb49b1  anc/lean/formal/Erdos7/ThreePrime/Moments.lean
b600d9d76d2760b1da91091a129032fe0103c474b88bbb4905283d0de17a8b6c  anc/lean/formal/Erdos7/ThreePrime/Obstruction.lean
c4205754453128cf29eabae0c9becec4ae37fcb072654aae5073877483b38142  anc/lean/formal/Erdos7/ThreePrime/Probability.lean
d58d6aa5688e1ce77ae67a51d0e455105b5e024fb9be55c7628ce063d9428b6d  anc/lean/formal/Erdos7/ThreePrime/ReindexModel.lean
b1b490e31beb6048e8f6013604ba949c244af8a135103d9ad3db0bffbeee23ac  anc/lean/formal/Erdos7/ThreePrime/Schedule.lean
5c782e003f821f60a3097742bfb39f58aab32aa194538cbf45a45bb11230cf5b  anc/lean/formal/Erdos7/ThreePrime/TailBounds.lean
41bfe70fa5f2167d59ff220c31c247024a8c79bdbf52d0e925bf712c26f7ae08  anc/lean/formal/Erdos7/ThreePrime/TailIdentities.lean
55c4892f85d6ee2dc0075aa34a58086a73502838109ffe661a173b4248327ea1  anc/lean/formal/Erdos7/ThreePrime/TailMoments.lean
e979bbd4d783c10244fad766ed7cdf60b60ef064e927a6f4fdba67e534935842  anc/lean/formal/Erdos7/ThreePrime/TailPotential.lean
14818401f722b8dd3a5dfab3fd4225dd7cfbe6bdda989511523f9e26e4111aa6  anc/lean/formal/Erdos7/TreeSelection.lean
9402bb43bdfcd158a7fa39c1fcc72078ef2ef1bee35c4d244992a6dc35392474  anc/lean/formal/README.md
0792de98f9f9c4c41d33e2268119d9204549f6dcb18a7433fecbb51eb067110b  anc/lean/formal/THREE_PRIME_STATUS.md
da9c68f428363c74d80f328be15f2e83c64867a1429b2193abdcaa950a373bd4  anc/lean/formal/build_three_prime.py
0de34e67ab3e75e006a020ea2d35336d880864d34c19b02a92deff21bc0a37e1  anc/lean/formal/lake-manifest.json
9407135c55bc1e2edae348d8c7f7e603fb4cac82a8f3f865a29e749c57b34c72  anc/lean/formal/lakefile.toml
72681913b978b3f7c2f48229836771f736f6e97d833917726b2263afbc6108ed  anc/lean/formal/lean-toolchain
b3248202894c6fa1e5ad7980e9c9ec955f6f5e27424bd99db485af824ea5baee  anc/lean/publication/three_factors/BUILD_NOTES.md
4489c6d66e9ad2e3bb9207ea9981e409cc92f08c50568bd2e928180ea4c84938  anc/lean/publication/three_factors/CITATION.bib
fecdc44a46d2ca0d20f7a66cc33b8f3594f0a4884de8473a7bf2951de6a1a2b3  anc/lean/publication/three_factors/LEAN_FORMALIZATION.md
f7bd00d871f913346ac77062ec5a35b8792451ba542d2c7958249e57e5aef7e0  anc/lean/publication/three_factors/LICENSE.md
97192e40c819e5c15f1538911d718a38d6b3e739438fb416acf5f574a3cb955d  anc/lean/publication/three_factors/LICENSES/CC-BY-4.0.txt
ad7dd18077f920e2326157dd543ef44e36abb82c1b57f5f9719a3779132b93a9  anc/lean/publication/three_factors/LICENSES/MIT.txt
a2bcc29379e22bc90ea98ff4169af923e2c1f12ae043eabda74d6a5b28a57697  anc/lean/publication/three_factors/PROOF_GUIDE.md
ad103f7741474b1218fcfe03c6582bb9c98fdc66c4543c590b5bc60d80746f1f  anc/lean/publication/three_factors/README.md
a5c5568097b6be5c1240ee48293024e944ad2ece2a89c039a7f6cde54e807f7a  anc/lean/publication/three_factors/REFERENCES_REVIEW.md
01d50a1bb015218d8cfbb3a5bc5fc9437788afc734e8f896a797a6fae60f2fe2  anc/lean/publication/three_factors/VERIFICATION.md
66c77905b752184f33dd794faca03a3f9062f2987e543d4859289e1a8ec8dac5  anc/lean/publication/three_factors/ZENODO_PREPARATION.md
95d726c361a6b107fae165c6290874d6baf13fb9705ac5f4d4a52575f4a4e236  anc/lean/publication/three_factors/certificate.json
69e72093facbba391f52895b4d608766d5f5f1c39e34c7c446c381cd127fc1e9  anc/lean/publication/three_factors/crosscheck.py
1507a89638c50c3a225bb6f861175ec18151b256d0a4dc0bdc16e8d6d270702e  anc/lean/publication/three_factors/lean_generate_certificate.py
8732083de29b17ccc141d911d3733a8f94bddf98fee70b60e3c8158f2e5f9a38  anc/lean/publication/three_factors/lean_generate_charge_assembly.py
0a0dd71ada1d30ff6bbb06b706b55bf63da26adabfc62e496fbe9cd363823232  anc/lean/publication/three_factors/lean_generate_head.py
42c0494d67e63195ab6083d0bb18e1f38fd2e905a0f49a6d5cff535896d7f167  anc/lean/publication/three_factors/lean_generate_low.py
a8a85eb6e6ef764eda2abf7ca3a62c04ac1a3f79e594aaa47635aa38df9fd32a  anc/lean/publication/three_factors/lean_generate_moments.py
c4caf74f04d7e8ae21048f3c118f7b5a9976cbecee085142c50701e28a91a7c8  anc/lean/publication/three_factors/lean_generate_tail.py
4f618566fe3a4dbdf46e4d20d02ccfafb12bf8cad5f699d3a80e030dc05db30e  anc/lean/publication/three_factors/package_release.py
291020863f5fbb4f2d98aa0a1d5ac63349bd8c565d4ab07422aee83d23825451  anc/lean/publication/three_factors/paper/main.tex
215a48672cd4d795125edd9c9b7913be2fddb88e1db6459b8976650ac4126dbf  anc/lean/publication/three_factors/verification/appendix_clean_build.log
2685485df8e3e347ba25327df8984d5b7bf156e605a5df015c064b8c28088d19  anc/lean/publication/three_factors/verification/appendix_crosscheck.log
c056e8edfbb7afd222ac24180bb79b1a693e770a06de03697fda6f3ec08b7b94  anc/lean/publication/three_factors/verification/appendix_lean_audit.log
5d3191416ae1900045176eaa1b28f6904dab4860aee8252f5723c3354a1be5df  anc/lean/publication/three_factors/verification/appendix_manuscript_build.log
12d8d4356f576ffb0799b07644991c590d927619bf133fd45cb2502edad374a9  anc/lean/publication/three_factors/verification/appendix_pdf_checks.log
97ee4372aaff45520464f69180193d82f789c9a13e221355ba3701d615f6eb65  anc/lean/publication/three_factors/verification/appendix_portability.log
7d18c30f2fc43ccc1c152d1c5ca5e791d6531bfea92f545a9c337ecc11e83e5b  anc/lean/publication/three_factors/verification/appendix_verify.log
eb865df1ffb318a38498e4c1f6d4bd799dbad4e102629f01f0d4afb9ec6461a6  anc/lean/publication/three_factors/verification/clean_build.log
2685485df8e3e347ba25327df8984d5b7bf156e605a5df015c064b8c28088d19  anc/lean/publication/three_factors/verification/crosscheck.log
898fd76aa25acb3278f4d7bd28f1f320cde597e1fe330f0d7de772704e9e44c8  anc/lean/publication/three_factors/verification/formal_appendix.log
db6aa2851f5ed2c05eb8c6a5ff68c0d7d89842ff73378f605edeb9b33ec3c738  anc/lean/publication/three_factors/verification/lean_axiom_audit.log
d2c167bd4f7d17ef5d21e00041bc7dacc4c3875e6ee2e036b667cd446c0335c6  anc/lean/publication/three_factors/verification/lean_build_summary.log
e6b3abf1c44cb5cfd2484d17f399f6b15e34ef450abf255c45d750a528ecd917  anc/lean/publication/three_factors/verification/lean_manuscript_build.log
3380624ce1afc3c536c6f982aa05dfc572d0425072cfc6fdff69b72b243e36e6  anc/lean/publication/three_factors/verification/lean_pdf_checks.log
81de4ce61d947d6a72de50a9f28194b91e5c564a4e6984a750dab20d8178f9cb  anc/lean/publication/three_factors/verification/lean_regeneration.log
1b2c0344b54a407bda3ed81241d9b9d77e435df80a37887e700a664b2f9b8604  anc/lean/publication/three_factors/verification/lean_root_build.log
a849f526b2c0ff27177ed2168c6fc476cd87e060a77c57df9fd7d575c79aa397  anc/lean/publication/three_factors/verification/lean_source_scan.log
9fe574e19132c5f9e113e19c760c39addc6bf167ba508a0fc039d97f32c91203  anc/lean/publication/three_factors/verification/lean_trust_zero.log
ee2cf58424c2f040caa9b16e2637b89af7eaa43bc2518635eb1dcce08e28034a  anc/lean/publication/three_factors/verification/references_2026-09-15/clean_build.log
2685485df8e3e347ba25327df8984d5b7bf156e605a5df015c064b8c28088d19  anc/lean/publication/three_factors/verification/references_2026-09-15/crosscheck.log
7fd2eca19cb367668d0fee9d12fde2d44878dadb06be33066cc134be56f7ee5f  anc/lean/publication/three_factors/verification/references_2026-09-15/manuscript_build.log
05f23c9b17b62f54696e3c63a14c50c01f1f969e86d4f8db9cb09590d4670c3f  anc/lean/publication/three_factors/verification/references_2026-09-15/pdf_checks.json
a9bbc841452d8b133cc7ea9ecc61d7e64836450877f2c9e2ca60ded14265f0ac  anc/lean/publication/three_factors/verification/references_2026-09-15/proof_source_identity.json
72dbe07a91bc141dd8603bc8c1ab166a775a05fa96fbf82c7ed5b39903711467  anc/lean/publication/three_factors/verification/references_2026-09-15/rank_doi_verification.json
7d18c30f2fc43ccc1c152d1c5ca5e791d6531bfea92f545a9c337ecc11e83e5b  anc/lean/publication/three_factors/verification/references_2026-09-15/verify.log
898fd76aa25acb3278f4d7bd28f1f320cde597e1fe330f0d7de772704e9e44c8  anc/lean/publication/three_factors/verification/references_2026-09-15/verify_formal_appendix.log
56b7c5fe0dd641c38a393056603f5324bad01442b375d9128c0e68b4bfff565f  anc/lean/publication/three_factors/verification/references_2026-09-15/visual_review.log
cf230fb91e5e4bd2d4aea6ba8a3a1a0fa709f6a2a0dcf27227e88401c202c79a  anc/lean/publication/three_factors/verification/release_checks.log
7d18c30f2fc43ccc1c152d1c5ca5e791d6531bfea92f545a9c337ecc11e83e5b  anc/lean/publication/three_factors/verification/verify.log
d9e13e6c5209d4220e0ee0ff3469400ffe9c2df37cd1fc6f1771a86b1d90157f  anc/lean/publication/three_factors/verification/zenodo_2026-09-15/clean_build.log
071ed7237f4af5333a0b90458e32374b0eb1e3d0615693638914dda74a19fc08  anc/lean/publication/three_factors/verification/zenodo_2026-09-15/doi_reservation.json
d9e13e6c5209d4220e0ee0ff3469400ffe9c2df37cd1fc6f1771a86b1d90157f  anc/lean/publication/three_factors/verification/zenodo_2026-09-15/manuscript_build.log
a43eb2f749e44aac2ccba45dafe906cf9bbcf1f41af64c073e9ca123b73607a9  anc/lean/publication/three_factors/verification/zenodo_2026-09-15/manuscript_changes.diff
7b766052f8a3e53ba6b7c4fd3be9f52a85396aa8603400ae02af524fd909ba77  anc/lean/publication/three_factors/verification/zenodo_2026-09-15/pdf_checks.json
5e29126f294b18838f61dd6bee790817e07bf7ec94aec3e7bb407bd132f6fe25  anc/lean/publication/three_factors/verification/zenodo_2026-09-15/version_1_0_checks.json
f3b0850af425cf1babc2f74398eb6317c00975d1ce6bbdf8dab9a0e1e2004882  anc/lean/publication/three_factors/verification/zenodo_2026-09-15/visual_review.log
b72ecced21b156fff925882541fedd03c517c2a63986a0e9adf79b3eb4f9f20c  anc/lean/publication/three_factors/verify.py
c4f582adb57d6192c5fb8b063d46993e3e91bbed706669cee92daba30f710ccd  anc/lean/publication/three_factors/verify_formal_appendix.py
671b74eb45c55f71562ea20b6b14ea82d750d3fbd8c0eab39eb630a588e5cf99  anc/lean/publication/three_factors/zenodo_metadata.json
4f618566fe3a4dbdf46e4d20d02ccfafb12bf8cad5f699d3a80e030dc05db30e  anc/package_release.py
215a48672cd4d795125edd9c9b7913be2fddb88e1db6459b8976650ac4126dbf  anc/verification/appendix_clean_build.log
2685485df8e3e347ba25327df8984d5b7bf156e605a5df015c064b8c28088d19  anc/verification/appendix_crosscheck.log
c056e8edfbb7afd222ac24180bb79b1a693e770a06de03697fda6f3ec08b7b94  anc/verification/appendix_lean_audit.log
5d3191416ae1900045176eaa1b28f6904dab4860aee8252f5723c3354a1be5df  anc/verification/appendix_manuscript_build.log
12d8d4356f576ffb0799b07644991c590d927619bf133fd45cb2502edad374a9  anc/verification/appendix_pdf_checks.log
97ee4372aaff45520464f69180193d82f789c9a13e221355ba3701d615f6eb65  anc/verification/appendix_portability.log
7d18c30f2fc43ccc1c152d1c5ca5e791d6531bfea92f545a9c337ecc11e83e5b  anc/verification/appendix_verify.log
eb865df1ffb318a38498e4c1f6d4bd799dbad4e102629f01f0d4afb9ec6461a6  anc/verification/clean_build.log
2685485df8e3e347ba25327df8984d5b7bf156e605a5df015c064b8c28088d19  anc/verification/crosscheck.log
898fd76aa25acb3278f4d7bd28f1f320cde597e1fe330f0d7de772704e9e44c8  anc/verification/formal_appendix.log
db6aa2851f5ed2c05eb8c6a5ff68c0d7d89842ff73378f605edeb9b33ec3c738  anc/verification/lean_axiom_audit.log
d2c167bd4f7d17ef5d21e00041bc7dacc4c3875e6ee2e036b667cd446c0335c6  anc/verification/lean_build_summary.log
e6b3abf1c44cb5cfd2484d17f399f6b15e34ef450abf255c45d750a528ecd917  anc/verification/lean_manuscript_build.log
3380624ce1afc3c536c6f982aa05dfc572d0425072cfc6fdff69b72b243e36e6  anc/verification/lean_pdf_checks.log
81de4ce61d947d6a72de50a9f28194b91e5c564a4e6984a750dab20d8178f9cb  anc/verification/lean_regeneration.log
1b2c0344b54a407bda3ed81241d9b9d77e435df80a37887e700a664b2f9b8604  anc/verification/lean_root_build.log
a849f526b2c0ff27177ed2168c6fc476cd87e060a77c57df9fd7d575c79aa397  anc/verification/lean_source_scan.log
9fe574e19132c5f9e113e19c760c39addc6bf167ba508a0fc039d97f32c91203  anc/verification/lean_trust_zero.log
ee2cf58424c2f040caa9b16e2637b89af7eaa43bc2518635eb1dcce08e28034a  anc/verification/references_2026-09-15/clean_build.log
2685485df8e3e347ba25327df8984d5b7bf156e605a5df015c064b8c28088d19  anc/verification/references_2026-09-15/crosscheck.log
7fd2eca19cb367668d0fee9d12fde2d44878dadb06be33066cc134be56f7ee5f  anc/verification/references_2026-09-15/manuscript_build.log
05f23c9b17b62f54696e3c63a14c50c01f1f969e86d4f8db9cb09590d4670c3f  anc/verification/references_2026-09-15/pdf_checks.json
a9bbc841452d8b133cc7ea9ecc61d7e64836450877f2c9e2ca60ded14265f0ac  anc/verification/references_2026-09-15/proof_source_identity.json
72dbe07a91bc141dd8603bc8c1ab166a775a05fa96fbf82c7ed5b39903711467  anc/verification/references_2026-09-15/rank_doi_verification.json
7d18c30f2fc43ccc1c152d1c5ca5e791d6531bfea92f545a9c337ecc11e83e5b  anc/verification/references_2026-09-15/verify.log
898fd76aa25acb3278f4d7bd28f1f320cde597e1fe330f0d7de772704e9e44c8  anc/verification/references_2026-09-15/verify_formal_appendix.log
56b7c5fe0dd641c38a393056603f5324bad01442b375d9128c0e68b4bfff565f  anc/verification/references_2026-09-15/visual_review.log
cf230fb91e5e4bd2d4aea6ba8a3a1a0fa709f6a2a0dcf27227e88401c202c79a  anc/verification/release_checks.log
7d18c30f2fc43ccc1c152d1c5ca5e791d6531bfea92f545a9c337ecc11e83e5b  anc/verification/verify.log
d9e13e6c5209d4220e0ee0ff3469400ffe9c2df37cd1fc6f1771a86b1d90157f  anc/verification/zenodo_2026-09-15/clean_build.log
071ed7237f4af5333a0b90458e32374b0eb1e3d0615693638914dda74a19fc08  anc/verification/zenodo_2026-09-15/doi_reservation.json
d9e13e6c5209d4220e0ee0ff3469400ffe9c2df37cd1fc6f1771a86b1d90157f  anc/verification/zenodo_2026-09-15/manuscript_build.log
a43eb2f749e44aac2ccba45dafe906cf9bbcf1f41af64c073e9ca123b73607a9  anc/verification/zenodo_2026-09-15/manuscript_changes.diff
7b766052f8a3e53ba6b7c4fd3be9f52a85396aa8603400ae02af524fd909ba77  anc/verification/zenodo_2026-09-15/pdf_checks.json
5e29126f294b18838f61dd6bee790817e07bf7ec94aec3e7bb407bd132f6fe25  anc/verification/zenodo_2026-09-15/version_1_0_checks.json
f3b0850af425cf1babc2f74398eb6317c00975d1ce6bbdf8dab9a0e1e2004882  anc/verification/zenodo_2026-09-15/visual_review.log
b72ecced21b156fff925882541fedd03c517c2a63986a0e9adf79b3eb4f9f20c  anc/verify.py
c4f582adb57d6192c5fb8b063d46993e3e91bbed706669cee92daba30f710ccd  anc/verify_formal_appendix.py
671b74eb45c55f71562ea20b6b14ea82d750d3fbd8c0eab39eb630a588e5cf99  anc/zenodo_metadata.json
291020863f5fbb4f2d98aa0a1d5ac63349bd8c565d4ab07422aee83d23825451  main.tex
