dd4b793a262459cd85ba57dc31b959d278f2f5281a74996ae3ec7ad304335592  .github/workflows/verify.yml
284f81d666c87f6ed3ca3577b1560c8651a15eef9279517dbd1ce01141cf23ff  CHANGES.txt
9131f1f7d2fa66b32e24abe37047068378a35a5a97b500b5483745588ceb904b  CITATION.bib
ff6e64e9809acccb74410e11dcc21c71251221c5b6d1d13cbdc755bb2c735947  PUBLICATION_AUDIT.txt
f97597d0ac423e491d5387c5308743a3fa817534ff86b221fd57704031fab29f  README.txt
147acbbb25687a13b3e12e5019ddd9b6195894835dec11592a4d7b153c826d93  REVIEWER_GUIDE.txt
4b39630a1d1e159e70c79e114c989f9d6e863a96400677e30479349cd773d8cc  formal/tc10/EXACT_STATEMENT.txt
d0b718cb7193238e2dbf7bbfd20967fa2b20ac172c763d0b9fce21ad0587546e  formal/tc10/PROOF_MAP.txt
c6beefb684268f59f05e4297379351cb73e00b2c157afdfe628e59f609f7513d  formal/tc10/README.txt
0d2951bbfcc5e04ae2e28a31916c2248bd61f755682c7667a49fb2450959cf52  formal/tc10/TC10/AdaptedBasis.lean
c6be900f6f27d89f86395ed6a7a370e79b45b76d93c0652b865a776ed6199e95  formal/tc10/TC10/AffineCertificateBounds.lean
7bc83a6f2f7edf881bfb191fedf3d528c54739280664746229e5dc7c7d48feb6  formal/tc10/TC10/AffineRealization.lean
ba139539f018d77a9a1c1ca8cee481ba4d3bf8033a30ca23950374fde33fa6a4  formal/tc10/TC10/ArithmeticCapacity.lean
8c9151763146be434dfbee8be8d05a8e98c811f60ea02ff77f1f50c645960cdb  formal/tc10/TC10/Audit.lean
f8ae452da9e884187f4ea5075be595444f23297d9e3142364fe19e9cca35976f  formal/tc10/TC10/AugmentedDesign.lean
4a5a6d3c3ea63f55fa17956801140edbd5ee9dea1708dc81dc9ee972341d5ab1  formal/tc10/TC10/BerlekampSplitting.lean
f28a49a355b5958d1a3630b65a49d0f34a9ccbb3dd7c44c7fb24384ea151ae04  formal/tc10/TC10/BinaryHitting.lean
471858e696a42829935b8a7c81f52c9bd0dfc5828bdb1572da883f53d6065a18  formal/tc10/TC10/BinaryParameters.lean
00b9ddcce56dde110c99b6116f14d3e85401c9b94dd030747abba63a03a62796  formal/tc10/TC10/BinaryUnitHitting.lean
804dec9ac799dc61aac3659674ee6b64bf86f5c9cb113e538fc107f5b1bd3893  formal/tc10/TC10/BlockDescent.lean
1147e11b8b89742d004831ae4f4b0b20be2c88d9a7d8b5fb7a72abbb7daa3e01  formal/tc10/TC10/BlockDivision.lean
5c3cccb9910c2c33c811fd5685568b2f7a6ad214fc678e82ae4cc0a25f449051  formal/tc10/TC10/BlockMinorWitness.lean
46da521df2cbe5f60cf20295603d2d89c30154563f148be26978343b9647bf91  formal/tc10/TC10/BlockQuotient.lean
8e1fe4cdd234e0544350f011c493109714a5945c8b9916b627bc0e61919f7a39  formal/tc10/TC10/BoundedOrder.lean
85b610503433af81229355720d081f82407debd0631bdd6a9ea63ed6dc923d29  formal/tc10/TC10/BoundedQuotientDesign.lean
87301162ec23e763f6d55352ae4a1524521ec63f73004fd0a01813f17289f0a7  formal/tc10/TC10/BranchingPrograms.lean
5ba1306eb768aea9a5e915851253126d4ea6d8e132e6f05666b92304fb9e5b65  formal/tc10/TC10/CentralPolynomial.lean
e66056b312d83a91784d0dc3a051ec394127da5da51c52b84eb1ae49e6d72ce9  formal/tc10/TC10/CharacteristicTwoAudit.lean
19d39bda687eaefbb293d8c8d77fa46a1e76adcf4470390088770469dc80aca7  formal/tc10/TC10/CharacteristicTwoExample.lean
3561c1eaeeb15d39255b741a1042cc82005650d08891607f348088abeb6db1a9  formal/tc10/TC10/CofactorFormula.lean
dec6704ae21e80cad069788cc3dbc3231c3aae6e2696b971561a4bcac9ba9eea  formal/tc10/TC10/CofactorLift.lean
a61bce17063f37aefb749b340bfb0a285a9d0d4de28d6951c8f05d7377380ec6  formal/tc10/TC10/CofactorOperations.lean
6b24c7d36af32ee1f2b66b15bdbeef777834c9e90a2accad5234403288f8d712  formal/tc10/TC10/CofactorRealization.lean
aa2b1b8118b2bb97dbd244ddd74f3a54e6e707cf77b421e0def4aa5b756ccf79  formal/tc10/TC10/CofactorSampling.lean
62ffcb05c55c89774ba820e4f1e6ced6ff19170064442c6ee2ae7c2118117a04  formal/tc10/TC10/CompanionCurve.lean
b930fb1a143358e308f61a46827f2ebd44c7fb7432b6aaa553598b3261d2a63e  formal/tc10/TC10/CompanionSampling.lean
0648757e2c9861796c13006372fc431f2df681f3e9137fa9533bae53b5405810  formal/tc10/TC10/CompanionSign.lean
aabfe4a17ca4b2d370419d2e8aa2f2eadd91b380241d33733566f5c4c0b4cf84  formal/tc10/TC10/CompanionTransport.lean
b24cb617508fc3d48cf1c428d1baecf01fbb3d76e067f4160f28f2685dad255b  formal/tc10/TC10/ComplementQuotient.lean
0bbb21d25f04a3c9bf7de756b27aed92eb28ff52e7a9fbd80604242885dbf01e  formal/tc10/TC10/ComponentSampling.lean
4e1a78ab7498ac7168bf8474405690d131abb8c9618c244ab80ebf632416ddf2  formal/tc10/TC10/ConjugateCoding.lean
330a09cee37c189d16ca47ca02be050e62e77cf13099f5e3fa84d5cdfc2fdd1f  formal/tc10/TC10/CoordinateContraction.lean
2abd6e713a069e6628a2e62c64aebb9ac7fa03f5fb68c44b080615583fcd0178  formal/tc10/TC10/CoordinateMinor.lean
312d1eeff7fee01c08c0cb052961d1c061b9b40ffce49f200949285183177c97  formal/tc10/TC10/CyclicAssembly.lean
ed2dd778aed5df47564d49d001021cabc2b2f9b9a54d7a33effd277ccae1c045  formal/tc10/TC10/CyclicBounds.lean
33d99b4fe7b3dea3d650697a079c769aaea2c3001e7cfa2103b3108a0fa5db61  formal/tc10/TC10/CyclicCoding.lean
61ba08437d1ec5645980e865c0b7502423c26693923a9f17081d26424bf9519a  formal/tc10/TC10/CyclicConjugates.lean
e80ce6a33ae08124e5f162fb2a52d92bc5ce19af88f41b406226635cc607ff03  formal/tc10/TC10/CyclicMatrix.lean
fa0c27ada2c021e6465d9614e82c01fbd0d1dc21cd5d304d89c90f33bb19037e  formal/tc10/TC10/CyclicWitness.lean
918e76fa5adf07edbc1b2df039ac016290f8f37068a93e7683571559e5c711cc  formal/tc10/TC10/DesignBudget.lean
3a782605c2875155f19b60f7ca2dcb21cbf5a7845f8102537244db3909b46374  formal/tc10/TC10/DesignInterface.lean
1c377ef669a5288ffef06c24666cb326120eb5239d75feb5529cae971465f33e  formal/tc10/TC10/DeterminantCurve.lean
e8e38bd15b3c7d70280da519b74b466210bdaeb717d427c98b583b4deed35788  formal/tc10/TC10/DeterminantMultiplicity.lean
14105577613696317127d952c03573d99dceb688e63a53f82c4b46bc1a9081ce  formal/tc10/TC10/DirectSum.lean
7f446eb52ef8a74d22419449f7be5d3e6ccd9b870bd6fb6b40ad5039a59a9daf  formal/tc10/TC10/DivisionMinor.lean
f509d812654a566c2575f690e3cc081bc9fb2b4e861c50bef04df0451060abbf  formal/tc10/TC10/DivisionRank.lean
8a16c6b58e1e58e618244bee994e507a766f9bb293718d103fd94cc0e14bf471  formal/tc10/TC10/DomainGuards.lean
ede788673c119e9aa8f0d311a0bf2156c1d10c196e59453b0b82e6eefd18c40b  formal/tc10/TC10/DomainInduction.lean
c90138b7426e55816a159c7f86b6d1808fe262fe79f85696bb6d4d275e4dad1a  formal/tc10/TC10/Encoding.lean
90967675204b6e5507dc1b23c753b3bd69b8f98fa6eb57e84fb8825fb3a0c962  formal/tc10/TC10/EncodingBounds.lean
b97c95c6339c062168c98a9ac15d59315792765f09057d55e507352682cca862  formal/tc10/TC10/EnumeratedDesign.lean
2c82978fd6fa4cf30d3e11352eafc8d607f8922dcc6548d07d927c9f04dac5a5  formal/tc10/TC10/EtalePowerBasis.lean
b308d562493221c58cdb3aea1a13587056f1d52df7e40fbe490aa593fb2e0678  formal/tc10/TC10/EtaleRealization.lean
e4a6be4ad6af66c7c3c66c267ea859aed644b9fdda784d14e04973f2d6462943  formal/tc10/TC10/EvaluationLift.lean
b25070ed0d654b4ede80dc2b504a15bcedef1bf37941651f5d3142b39bad7020  formal/tc10/TC10/ExactCodeSize.lean
09bddf94bbb69f1ac0ae54bac74b2612bdd13b6ca87a22cd7f78c2dbe31b3b93  formal/tc10/TC10/FamilyCertificates.lean
e67a8c7bb00a886f25e5745c1f31145566d844154cd5152077e5838751ea2cb9  formal/tc10/TC10/FieldCompanionSampling.lean
7ce27f81d990f7bc445eafc6ab278079d8e884ae1736936c309817356ab12478  formal/tc10/TC10/FilteredNormalization.lean
87a9a71f9f9fef7ae400cf92560921eb302aba64d4e658c7c425e91bcb95ad00  formal/tc10/TC10/FiniteBlockSum.lean
c0f3951887090f31adbd6906303ae395b86f9e25321a65f28f70f246fbaa1140  formal/tc10/TC10/FiniteCompiler.lean
6bfeada27c626c9e1516eb614f6d0344f0d9966f52a1bacc4207381c5a9eece2  formal/tc10/TC10/FiniteCyclicIndex.lean
0edcbb84b6e13415e0a7dc5fd5c6abc8f5bd21547d6a6930f46008d52f4003e8  formal/tc10/TC10/FiniteFieldParameters.lean
0aac44aa9532b444a61bcaa7f32f6c9cad909cd1bfbb1375507d7aa1bd1caf77  formal/tc10/TC10/FiniteHomogeneousHitting.lean
1f0d7c1cb05c46f767e29fefe0c16a3459398fcc223a50898b3d200f3e3cd67c  formal/tc10/TC10/FoldedCorank.lean
190907385a132df598b194c6e142d9b7766d86a1e52f54d7ef8840d3ff9d1d8e  formal/tc10/TC10/FoldedDegree.lean
1de6ad95ac5bc1bc64e55e9a301a574e8c77a8993132d66a0a6574619d29176e  formal/tc10/TC10/FoldedDesign.lean
286b40825773253175e358ea9a8b680f916d43f377f7c0a8120f27a1429680e8  formal/tc10/TC10/FoldedDeterminant.lean
7b249545107e1b24c5a0ca8aed0bb1a675562eca7b56797f2891b01bcefd2819  formal/tc10/TC10/FullWindow.lean
dfbfa662d4c8b0754cece59ca66d304fefc2977b69cde4405b2920af6d7c7b5a  formal/tc10/TC10/GenericEvaluation.lean
8acd014f131ee6f948748bb842dc8693865bc6f50d81aac13f98003d02e208f4  formal/tc10/TC10/GeometricDesign.lean
86898c20b5811dc0ab8a2eae53588ce316670a3a44acd1640cf6e68765549bca  formal/tc10/TC10/GeometricQuotient.lean
5f711ad63b423812240d74f02ece08b66d4848e5a50271c3cea292898591db1b  formal/tc10/TC10/GreedyNames.lean
567ee735690198fec2ef01a6f66d6c31aac962640574021a629f4f3ba7db1b7d  formal/tc10/TC10/GroupCyclic.lean
aeaa29a44b27371f7ee85d854d19ddfdb0e131adf5b59b79be6c642c187a9468  formal/tc10/TC10/GroupDictionary.lean
bafe4ded41f2094023a218d4268e2047e772eb95aa5525b89bf4f414ba7ffdd5  formal/tc10/TC10/HittingReduction.lean
4eb80dc900c2d2a4cae90aa277129964609c608b556cb254321c1fecf50a1d60  formal/tc10/TC10/IndexedSubstitution.lean
71e2683e500c76e2012db0128eda61a542ef716244740bb608bed3996a815907  formal/tc10/TC10/InputAdapter.lean
c6aac99497f65240ac3944c02ecdf7bb313812c1d8058e3dfc49c3fb74720a96  formal/tc10/TC10/IntegerColumnBound.lean
e1d0f53e151a1ae4888e2d2bb2323899095ca7b2f43dd6c5f429c4fccbd3a5b4  formal/tc10/TC10/IntegralCofactorFormula.lean
e42e0c5daab2c9fe462bb9a420dfa469240368d60c9955b65e2c94a26d947cae  formal/tc10/TC10/IntegralCompanionHeight.lean
6185a38e2464b6322d843f6a63d6e3dcf970f6155e5abc396cd0e90fc362fdce  formal/tc10/TC10/IntegralRealization.lean
163adf3158c21ae914eaeaca33456a98500743962fb1e11a4b0fe79166db1955  formal/tc10/TC10/LargePrimeAffineHitting.lean
fe2cbeaae3452f46a01d3db80e51a4334517728ac257271b991b78be7c058e09  formal/tc10/TC10/LargePrimeHomogeneousHitting.lean
de47ec8b5f93d4244c16b88e94aef26765f4166d91cfb056b80bc74cf469b77a  formal/tc10/TC10/LargePrimeRawSampling.lean
7b50038fdf2fb58bb0a57cbe63f419d77ed2443a29d6b8ec6407d4c19a8f7287  formal/tc10/TC10/LiftedCodeHeight.lean
0ea1932663d9b94023fabcebbdb4785a2e988330ce2e2df13e639c3ccc454777  formal/tc10/TC10/LiftedEntryHeight.lean
38b0d14f723604d464d6f2e14907027114d0ae65d4afc297df1dcff8a971ccbf  formal/tc10/TC10/LinearNames.lean
9e4b3a5bb6e184751d920dff6eb3a397eb558aa8132fce7af3b35090c7ac6618  formal/tc10/TC10/LocalSpecialization.lean
665318cd0f32e773bec38414d57894bd0b0e39b6e8c4c99652011f8945478572  formal/tc10/TC10/LogAssembly.lean
d15db6dd73f624ac60b89a86faf21aca9cf2416f5f79d301612bd147e7e8d28f  formal/tc10/TC10/LogNames.lean
09ec0d068a5fcc8b3aaee9321392c37f6a90c2ff8cf73b0bbea007ee232eddf7  formal/tc10/TC10/MainTheorem.lean
9af294b24857018b4c33e35157387c84678c804c754c400afac297f50b0c4cd0  formal/tc10/TC10/MatrixCertificateBounds.lean
f494104e9f0af343cdf5af7cffee19c7f0a185bed74e0fab6fb2934240e6c479  formal/tc10/TC10/MatrixCertificates.lean
cf286f52a435c7f8a83f940bdf53aa6cb372dab418b5b78c8dd3113d8e44dad9  formal/tc10/TC10/MatrixCoding.lean
97a9bff168895c92002a3b285f2b54d855418730741e834ad1383ac40ba4cbe4  formal/tc10/TC10/MatrixDomain.lean
fabb0b6fbd39b4c72fe506d18ad4022cf7779a9eeebfa408e18bcf44f0237105  formal/tc10/TC10/MatrixQuotient.lean
79c30e7224edf6102d309eab100597a57caccb00bc528e0b7c9ee57b5c315709  formal/tc10/TC10/MatrixRealization.lean
ee86aeda265d6163378c2eb37e46cf90b26bb2547a6b714d427e34fd6edaf869  formal/tc10/TC10/MatrixRenaming.lean
9e665b98fab4b6f0ee8fee6fe5cf12e8f29382f3d7d35d393ea549f180a7db65  formal/tc10/TC10/MatrixSemantics.lean
b5e5bb5175bac8f5529baaabb85959b17eacc6c8b2b532898eca03632e2f8e6c  formal/tc10/TC10/MatrixSupport.lean
8ec41ea06bcb8e601b313e614b9559eb419432b35ff1677be206a6c32e03555a  formal/tc10/TC10/MatrixTransport.lean
eb81c051d321ee7c2e0ece8238f008adafa04b72b3e076315ec5cd8808608d6a  formal/tc10/TC10/MonicPresentation.lean
02c277b049f637de07112f867fe810275131062ec5b57d23a423277afb4cf12f  formal/tc10/TC10/NamingResources.lean
647f803a0af5623c342c6085207d6bb2d415a03d1ff998016e2e8098e72113ef  formal/tc10/TC10/NoShrunkSubspace.lean
8d1cd789431c94746ffd3638cf53d3836784e3c48a4f163c52417d9fe5bab5e9  formal/tc10/TC10/NoncommBlocks.lean
98df4e46b933450c7ab99744b53c14a9727ee2e8552567fd1961bc8937ef6042  formal/tc10/TC10/NormalizedQuotient.lean
be186b53a6513847dfd14987bbcc792e9fd3c32f171d8b2219cd4564a1fa3c12  formal/tc10/TC10/OddCyclotomic.lean
51b76824438779039adf4cfe953a761686910ff32746812116689afb8d1e97c3  formal/tc10/TC10/OuterOperands.lean
e9a2eef6c5d33fbdccc20f35b62b84e6fcb520344fe10bd15e719e11dd58e5f2  formal/tc10/TC10/OutputAdapter.lean
31dd9a41217b8108bc678419d3f84b565996007ed864f5f4b23947d3201840e3  formal/tc10/TC10/OutputPolynomialBounds.lean
02a2d535ea33becb42cdc2000ce1d348a3d4b24359689a758ba1f3f37278cbc5  formal/tc10/TC10/PaperContract.lean
a484377be1a599a01eafff19e35bb7664153b5e0a396d79dcfe459dce2b18faa  formal/tc10/TC10/PencilHomogenization.lean
78fe9782cb7e5064597bcd7a4987c9bcd765343beafe1bd18f312fdeb7fe9156  formal/tc10/TC10/PencilNormalization.lean
2b6c8b530b94af33cfd2439e52732e5a2ab4b040b3094de7fd948b3c98da1230  formal/tc10/TC10/PermittedLift.lean
7fad5673ff03c8788ba0d198e9b7b16b84766d62a6c5a32743e2517b97553808  formal/tc10/TC10/PivotExtension.lean
7147cfcfb0007c16fce6f83fccdb8b98d160c7c8354a5f684509000719280b28  formal/tc10/TC10/PivotQuotient.lean
74391fe368ca23967f670b5635a41a2980ddc7827532ed0dfb15b939e0e0d15e  formal/tc10/TC10/PolynomialCompletion.lean
20aff2795e2acd1b62ccd48e226bfbcdf58de923c55ee654017704e1d1338581  formal/tc10/TC10/PolynomialCoordinates.lean
69e9040b3fa4c82a7cccd07064c7eb53661f38f39dbcf4762286cd8075544456  formal/tc10/TC10/PolynomialDeterminant.lean
bfd9b88dc4f000006a1862b6ab233ca8122da879dfce09839139af9ea7e95bd5  formal/tc10/TC10/PolynomialSampling.lean
e745884bd26fa0b5b48fd7f4cdc5301d0aa11c27309fede0e1840899ec0ce14d  formal/tc10/TC10/PositiveAffineHitting.lean
095d04d349ead2df83efb3f2b97a8c670ed6d9ec18c074ba41c5563ec6c6877f  formal/tc10/TC10/PositiveBounds.lean
03f057351f282c3f9d7a1a0d99506ef19d773523f42785d45daed7efc5969645  formal/tc10/TC10/PositiveFixedHitting.lean
b17d17b7866853f1e1c3e50dd46e8ab3f2a1088a08ab5cce9e9037ac2a68618e  formal/tc10/TC10/PositiveFixedParameters.lean
cf835dea508863df2dacac452b55670d6e4ff113258297ad3cde1a68f19c8fd1  formal/tc10/TC10/PositiveHomogeneousHitting.lean
6d687330227490ca9008104b30488f34a69376ebc2089293576cc78ed37f4c48  formal/tc10/TC10/PositiveParameters.lean
5139e51c58dbd9da6ea59640d09609c4db001503c11f8366969f72e6532d31bf  formal/tc10/TC10/PowerBasisSplitting.lean
fd6f91608cff90630ad6d2c1b475562e7a927fb87541395900b8085448ae8440  formal/tc10/TC10/PrimeAffineAssembly.lean
00ac5ed647b8ecdbd6e8f708892d2655de18f30a2c5ca4ac0135092a36dc734a  formal/tc10/TC10/PrimeField.lean
c12ffe24d55852d74adbad548353a2816101b221fd7f0693a485b0a159844963  formal/tc10/TC10/QuantumCurve.lean
afcd495f46b5bb68c06f315543ece7c7f5eae740e38a2fa70df3a627c6ae42a8  formal/tc10/TC10/QuantumDeformation.lean
0c108b2ddeffd54ed909782ee7ef1e38190da4c63d8503c7b4be36a0e787a55a  formal/tc10/TC10/QuantumDomain.lean
d33b64f1a75f74ba6cba036f2331f98c5cdd4b65af678b38a9a154c17e051a84  formal/tc10/TC10/QuantumMatrices.lean
8fd591631f585600032f261472c9c4847fed0a30268c90cff9a6df717d02a7af  formal/tc10/TC10/QuantumSeries.lean
8a78768b57840623b5d650a8776ec66e996f4bc97fe98ac3fadd4ff61a45db99  formal/tc10/TC10/QuantumWitness.lean
3cc3590f57d7eb12572449c6463adb309d984892b89e8bb900643fa89de0b045  formal/tc10/TC10/QuotientReindex.lean
70ec9476e72283bdd266a95d356e010ba59093eadba1ce52abf5b39d2691bd19  formal/tc10/TC10/RankContraction.lean
ce4867160d1886ee11165f6c65237f12a3d0cd4297395b6cbc6e3e3f715e8184  formal/tc10/TC10/RankPadding.lean
e2ae9b014a30b6efcc24117513d07158836ec0d5dd1c3102e17b23be0edd921b  formal/tc10/TC10/RankSpecialization.lean
ce8a82459f0e7015ccfccf562dcb79d2075ab2a714cadfe4157370424990e327  formal/tc10/TC10/RationalAffineAssembly.lean
c3812ad55f15fc7c0162dad7d67a8350d94a7248f4c2d3923be93ee25526a6c3  formal/tc10/TC10/RationalAffineHitting.lean
5b20fbb075cc9087d91c38cb271f84023d99f5377d99bd4c0d78e3cf1b7550a6  formal/tc10/TC10/RationalCharacters.lean
1d4779c5e2606108ec02a0ab7ecee1804df832a81ad7ee8974bc7f9af73718b9  formal/tc10/TC10/RationalHomogeneousHitting.lean
b5f348ff34a745a0a346339aa14edc40cc36eb91dbe5d3860b26be22bc208f61  formal/tc10/TC10/RationalNormalization.lean
ded2ed1f284077d5759ce0627b0ce5818b049de8808e95629267727af5a3c3ae  formal/tc10/TC10/RationalQuotient.lean
c6e9e09f7a302294ee6953a957cf1bd33197017a0e4610cd8e67ad8d193c227b  formal/tc10/TC10/RationalRawSampling.lean
ba57fd0dd456e960730d79363de9d4135b8ac217d22b64e701721c8a7d58e499  formal/tc10/TC10/RationalUnitHitting.lean
163398b12e627f9f19b1202d20443f22539c3b7a21e406c1be43aed2acc662d6  formal/tc10/TC10/RationalWordHeight.lean
30ac65cf81f66b433dc92408d44a7d5ea9db7718c329c314f5f178bd2c4db82f  formal/tc10/TC10/RawCompiler.lean
25804863a2b1d91f548c40be25c00480a58ba1972cef0a5432a4e00bbe62e9ba  formal/tc10/TC10/RealizationAssembly.lean
17a128708b002f7fa0090fed5f7563177631552aafbc1da57d78300171fcf528  formal/tc10/TC10/RectangularDirectSum.lean
a809e9a4d3f7b49bafa67f1b2fc38ef2890afc96996123e926c7e246ddb240f3  formal/tc10/TC10/ReducedCurveSampling.lean
5069f8233ae22c794117f14bdcd2e3ed1689a84f3ca5b01c8cc1051c0cec0647  formal/tc10/TC10/ReducedFourier.lean
a17449913f9e201db52c05e28291fc27c7617d6b820d2332a97fe0228dd3f2ad  formal/tc10/TC10/ReducedRealization.lean
613e7770d8debe47e5c5d5135bfa56a590910c1aed9c902ae89e24eb6f6d43ac  formal/tc10/TC10/Regression.lean
cca7c369066e56a00357c73eb2365f49f6bb433ce6e16f1c6c2480ce205fa062  formal/tc10/TC10/RelativeCyclicCoding.lean
e8990a0f175d77fd58f66984da6e6161e697c2946f27bc21da750eef0cb5506b  formal/tc10/TC10/Replication.lean
f652f091507893912b2c254533f2c386b6868636db79c3d74d9d2b548566fa38  formal/tc10/TC10/RowSubspaces.lean
b96c074eeabd1f703e1469484bac4704854f1b606345cf0d69de09a7a2e5cb58  formal/tc10/TC10/Runtime/BerlekampChoice.lean
e1142c689c5773863557ae4077f5378d2940a345f9e292fe795b3c1136a74bfb  formal/tc10/TC10/Runtime/BerlekampFactor.lean
e264b9d94cc4abacfc9e24d9e8b0d529cfd784ba4c364272592550fda79eadf7  formal/tc10/TC10/Runtime/BerlekampKernel.lean
ea8141f41449a67d76203dd51248d078feceadbcc1160818717ac8da0d352edc  formal/tc10/TC10/Runtime/BerlekampScalar.lean
8d9cd4265a272f44b0db716c9f4d978771660d355dbb842b06d6067c8d8a5adf  formal/tc10/TC10/Runtime/BinaryAddition.lean
bae1bf814918d5e5067f814d6e4c972065b2f3454333d2e27b785a67c9b8f8f3  formal/tc10/TC10/Runtime/BinaryDivision.lean
9db10436f3d5077c34b2a45a251a786c0ce258c24a127f1067942278a30950df  formal/tc10/TC10/Runtime/BinaryExecutedHitting.lean
1a47809df54ccec5b8c13bfefe04fbddae4a95504dada8bb6ec9a14436c05c6c  formal/tc10/TC10/Runtime/BinaryFieldConstruction.lean
448da01d1e09d8b4d425f0b33fd27b212890a6c006905383ea5352fbd85071e8  formal/tc10/TC10/Runtime/BinaryFieldPivot.lean
513fea1fefb2304019e03adcc8b5a9aff9b1fd64ac360682355a019048b0d70d  formal/tc10/TC10/Runtime/BinaryFieldQuotient.lean
7d1d855e72b032b1c8724eaf53003f7c27a295a7bf78f2bd7452a0dfae69033c  formal/tc10/TC10/Runtime/BinaryGcd.lean
6936a8f324bd8805a1cbc940aa940bf428d928d4c417a60617d1c77eface909c  formal/tc10/TC10/Runtime/BinaryGenerator.lean
74885d17f5b995beb2fca4efdbbc41e71ccc0499cc570e64665835db154770c5  formal/tc10/TC10/Runtime/BinaryListAccess.lean
c349e890ab1316f0eda7c25f3240e81141383b58a12aac60fd17a4aa91686c83  formal/tc10/TC10/Runtime/BinaryMatrixCorrectness.lean
adc3dddaece2a0330b59ada54b61ba42bafe331e7d524a632714fd6e8d0de8b9  formal/tc10/TC10/Runtime/BinaryMatrixPower.lean
dc321c1ad7f902a4b2e05cb2417fe133303284dfd523e8aee50ef4a6e7b4f10c  formal/tc10/TC10/Runtime/BinaryMultiply.lean
c60fdae8b7b03abbe9e72d2a051b8d1772f609c766aa77d75d9da51cce1f8aa1  formal/tc10/TC10/Runtime/BinaryPipeline.lean
d539b485ba26a2682d882b3df4605fae8a911c92c743a82b7fb7cae456601508  formal/tc10/TC10/Runtime/BinaryRootConstruction.lean
e2fb2dcd3977c64cd43ec9b5cbbd0c11f8442021f312ace9769795738490f070  formal/tc10/TC10/Runtime/BinarySubtract.lean
d60c563d25ed2d03660d45eda10d4c3e14ce103a058235a1e441501e9c7a0ab6  formal/tc10/TC10/Runtime/BitAccess.lean
95cff06e1695ed8b619eb6456bab8cc005c0d7720be8911de51e82c8503db36f  formal/tc10/TC10/Runtime/BlockArithmetic.lean
bddbfee65731d32087756b27f662b06ba8cffd1107746a92954e9ba3be4857ca  formal/tc10/TC10/Runtime/BlockForms.lean
76f02d310c44d3adac282d7a034c6ac70c3c058bdeef3546236f83160787aae7  formal/tc10/TC10/Runtime/BoundedOrderSearch.lean
e58826917af2576e807039725b2cab8a6580a5887725b4ae1f61b4f578a78cc5  formal/tc10/TC10/Runtime/CachedExtensionQuotient.lean
5547831d09e017d2065878d3d6acb779bd4f4657844392383d8fb81b19b9da22  formal/tc10/TC10/Runtime/CharacteristicPivot.lean
e46466fe39e09d35a4e119f47c2f2f971739cfa9b5e20e84b7c62a9f625381c2  formal/tc10/TC10/Runtime/CharacteristicPivotTime.lean
65a2c4bae16ccd93b0eaba48e51c2747088308c66ae56f3548840d1b066c58c5  formal/tc10/TC10/Runtime/CharacteristicQuotient.lean
f57d2d4fddfe7c66f3ef94047b9f047d36216b26b79b99750c81446a44a076d0  formal/tc10/TC10/Runtime/CleanMultiply.lean
229a3ca22bde87e00d353cc51a223359a53ca10afc2f4a10baa39a31e6acbe98  formal/tc10/TC10/Runtime/CofactorDecode.lean
de1a964b0a4e0fd3abfa564ce3c8ca47fd9cca3d650098d74c224b35bc58f574  formal/tc10/TC10/Runtime/CofactorEvaluation.lean
ab871e5dbdb01e6055c781c1797904af44a72cda4aca1742a23132b261f7f4f6  formal/tc10/TC10/Runtime/CofactorTables.lean
7b9c19ad7ea05547c4f2a7d5b7bb85a4d3fc0637fd2026d40956f3034dc00f3e  formal/tc10/TC10/Runtime/CollisionWeights.lean
bb7b3f1c1f59ad02f294e2b184303c7284846933180bec7ded67983e61679fff  formal/tc10/TC10/Runtime/CompanionConstruction.lean
6d68bb372f1a8be6ba3ea928b2e7dbb8b34859ee5b9b8888d2789f9ee00b35a8  formal/tc10/TC10/Runtime/CompileProcedure.lean
83bb4c3be0f21b5ea7b4bb032e7b4ccf7dbb0042ea21447cd3bf0768d5d0342d  formal/tc10/TC10/Runtime/ComputedDesign.lean
105b7c6d21a800904ef202a54819c5a9a0ce28cd09ba02ae10e2893a8445ae95  formal/tc10/TC10/Runtime/CurveMatrices.lean
34ce270d93c6f57bad3d2673bb285075584414ef58cb5fedaec02d070d081842  formal/tc10/TC10/Runtime/CyclotomicArithmetic.lean
ce52d9b7320e2d087a4871dd51a55dd2efc4b584c26f6ce144b377fa23ae3c8d  formal/tc10/TC10/Runtime/CyclotomicField.lean
cf03fdf172af9e7b3613db6972142b547f9f6c4a67d58c5c58850fe5265799a3  formal/tc10/TC10/Runtime/DenseDeterminant.lean
403426160f64c4a12aa2fcd7fba147b0d212752d5b86df00d0a98f3dd04e5a2d  formal/tc10/TC10/Runtime/DesignOutput.lean
9330612aea216608972785304e96f2a34d7ea3272fb4bed6e3a04bc2d35ede1a  formal/tc10/TC10/Runtime/DeterminantAlgorithm.lean
eb9037b83401b3746b2fa2f3b204f6b81e4eccd3fc39a75751852dbb6bc153bf  formal/tc10/TC10/Runtime/ExecutedCofactor.lean
465948f59719ea4eac77d3fa000cb2d36042647c4ce4cc5df94eac716edfed57  formal/tc10/TC10/Runtime/ExecutedEtaleSampling.lean
d5d445f79b169e39ce02056cb0481f95b124c55e9029f4f82e0ece8cae01c0da  formal/tc10/TC10/Runtime/ExecutedSampling.lean
98d9647f189484eb60ab8bf497458aa4ee3c327651c6eb1f18a7ad56aae298b7  formal/tc10/TC10/Runtime/ExtensionInverse.lean
fa45dd4e32fdf70844019d47fbf61125f64a8f3494f87ded5f164467e44568ca  formal/tc10/TC10/Runtime/ExtensionMinor.lean
d17aead43a9213b9072e8f38e414d9f1b28f8d4b151da1e3fc96e4291684ca7c  formal/tc10/TC10/Runtime/ExtensionOrderSearch.lean
bd757cc9a53bcf36754277fd7ef52aea3f3d90803e1e6e61ec959b457c6f3ed3  formal/tc10/TC10/Runtime/ExtensionPivot.lean
45e0db6807508268ece440369ecc328c28ddb6f77650157cfa3864dc20cdd1cf  formal/tc10/TC10/Runtime/ExtensionPivotTime.lean
d1a58e96090d5472ccb152f38d3d046c5406037ddf41405149d1f3756cc6fbdd  formal/tc10/TC10/Runtime/ExtensionProjection.lean
1620ec34f965438c434d8f2035895e0c2f2fb8e89126d084fc11cff0b6ce7caa  formal/tc10/TC10/Runtime/ExtensionQuotient.lean
b8e222503ae999b1bf1fbc5643f8dea659d74eda4c12ec251aafa0a1d01454b1  formal/tc10/TC10/Runtime/ExtensionQuotientTime.lean
a75532fbed5a3630fe9a718f42237bc1523db01a3c95e214fb5cd1224179dcfc  formal/tc10/TC10/Runtime/Feasibility.lean
0a7ffb1f443c053534daa6271d43239804f2e10b3c473e937c1d56133e897429  formal/tc10/TC10/Runtime/FieldConstruction.lean
1d932ee47a0804cc0656a5dd6d189684d0e8f61a0658231a52f2ea5968614ca5  formal/tc10/TC10/Runtime/FieldDegree.lean
43f52a67964fb61514b91ccc58012c768a28c4acc1628ff5397af5f25792b0ca  formal/tc10/TC10/Runtime/FieldTest.lean
1bca34b47bb18821aaee0d73e84f432540a58f9551fe7984d235d83d84189cbd  formal/tc10/TC10/Runtime/FiniteExtensionArithmetic.lean
d5b4fbb116f450f47bc34d962cb068a628bb18e636de915949f7264afdb47463  formal/tc10/TC10/Runtime/FiniteExtensionEquality.lean
3b1b7143cfe8c66af85f04d98e5d75ec1362aa407387f80697dc3f8c4fafb4f0  formal/tc10/TC10/Runtime/FiniteExtensionMachine.lean
6041e014b5bf60a26022278bbe0f251b11b74ac495a5fb271b4f4400a56eaf63  formal/tc10/TC10/Runtime/FiniteRootConstruction.lean
ce756910df811f3b13cd9b88815e275a074201e6b279d86241cc81abce23e24f  formal/tc10/TC10/Runtime/FixedGenerator.lean
18931559d4d3555409b356ae34b9365bc44ac6b93d62a6cd80b7e388ba7f7bb2  formal/tc10/TC10/Runtime/FractionEuclid.lean
d4c9559a914b2475948ad639b95fa84ab69cbdb5b7e671dbdbe82d8a82288158  formal/tc10/TC10/Runtime/FractionReduction.lean
d258dc6a658a8b490b1da044b70197d6f830e06cb2c680d3b67adfa6aadff0ba  formal/tc10/TC10/Runtime/FrobeniusMatrix.lean
61ae48f724ad2a84624cfcc2a3c0b8849cb8af47b90111f2dd37381f3ff04fd6  formal/tc10/TC10/Runtime/GeneratedFiniteHitting.lean
c602547a830a7d0e22a86f0a2cf21b1cb40ad1cc8f77c30c23f33367a79c2660  formal/tc10/TC10/Runtime/GreedySelector.lean
6e2ad4c61dfa15f0277d3737f72bea1396cc27948015ca804a320c503eeca38d  formal/tc10/TC10/Runtime/GreedySelectorCorrectness.lean
2bfee8a097792a57da7bdde584cc71ad4fc8c85103f8f5bb4714ea46375b8efa  formal/tc10/TC10/Runtime/GridCapacity.lean
ac00b31764d059a3c0f5f470bc42fc6d853983b6917c745a3c12da70d4d28dd9  formal/tc10/TC10/Runtime/GridCoordinates.lean
7d6a2e7f4253df846cddfc99ceb4dfd61090cf72b6f3b49bf27e94dab4972ce7  formal/tc10/TC10/Runtime/HomogeneousDecode.lean
8effe80114b5187ea47877f1a060449c5d573c5e4e924774310c002a48f590a3  formal/tc10/TC10/Runtime/IntegerCofactor.lean
5dfdc678537c3adf7bc1d7bec85bb56b9c1cba2172a75e6c53c4ff280f63a898  formal/tc10/TC10/Runtime/IntegerCurve.lean
e8722072fd1ecf45de635955df0886c8a329551211432450c91891f520da91aa  formal/tc10/TC10/Runtime/IntegerCurveSemantics.lean
ff64b0960aac35295c1d9c3f1c452c6d7010428b91b4cf426eacf7261c6c28fb  formal/tc10/TC10/Runtime/IntegerListProduct.lean
cd861b2d6f6e14652ff51053ea6f46bdf560bb5c1690889aea2c30967f5b5269  formal/tc10/TC10/Runtime/IntegerMatrix.lean
d265a5ae8ecc6b4f6ce0850713ce680335d393f195ff89792cc4646386dca338  formal/tc10/TC10/Runtime/LargePrimeConstruction.lean
b3ad1ddd784a7b6bb744cc6e2ef10bc4e328b5f4f9af362d4a376f3a33ab42b8  formal/tc10/TC10/Runtime/LargePrimeDesign.lean
5a8f6a7d51d0c0b90426882c9b5857c35cc59b37a9a43333b13c3605f0476e79  formal/tc10/TC10/Runtime/LargePrimeHitting.lean
36072a142377db4ff3a3d3a663aa08d07877eb55befc924dab55d62c9c464797  formal/tc10/TC10/Runtime/LargePrimePipeline.lean
a8f3e769decf605d8150131beeab9eaae98360eb584561c50e3b346e23cb7a6b  formal/tc10/TC10/Runtime/ListArgmin.lean
0ac34b0b6c4b3f04bb4bd9d6f17c464394c8b2e41c8b3a8421638b42db550469  formal/tc10/TC10/Runtime/ListOperations.lean
61f15e16e2f695b8fb1d5bb74249373671000f7b46520df059c1a954e90f2700  formal/tc10/TC10/Runtime/ListProcedures.lean
3b5d6aa7b0c105b35abd8a49f22a17693776eb1d988ecfa2bdacaaaf1cb55062  formal/tc10/TC10/Runtime/ListSearch.lean
d2611f78f67a5fde4765597278918c5da21ac06ad2716b0aa7181a11c5dc892b  formal/tc10/TC10/Runtime/LiteralGenerator.lean
693d3fd8cd988fbb0624e86991e968f5cf95e9f3650d396d554bae6e1d607458  formal/tc10/TC10/Runtime/LiteralInput.lean
6dd8eef32562abe8e897cac90067661f6e4b79ff65dc6956476a6ccad7d958ea  formal/tc10/TC10/Runtime/LiteralOutput.lean
f31d15faebc5376bf82b3a24290c0c752b9b2653f7a7a30abca9c03dff27001f  formal/tc10/TC10/Runtime/LiteralWords.lean
025d9bcd9d0465a471dd2c7d25a99a845c2a13776f97a8977a33c75d98b5c352  formal/tc10/TC10/Runtime/MainGenerator.lean
1262e7c65c3971e81fc92cc0dff954e6db3895410018f6887f3eea5207d91ccc  formal/tc10/TC10/Runtime/MatrixListProduct.lean
730112dbc29398bcdffebcff638e03681f0c45c52a9fb9614c95fb1dce37e81d  formal/tc10/TC10/Runtime/MatrixResize.lean
43799a75977884fa1f29af96a56e831a547aa344397f2b908310c1b5b5dcb7ba  formal/tc10/TC10/Runtime/MatrixSum.lean
a2209c6329262817ed9e8808d6e8c1480a4907c11fa8996bcf6a106c3b147f39  formal/tc10/TC10/Runtime/MatrixZero.lean
683e8c04f98aff7acd0f3c13c63fc79bd467eefe3048366057f596668ba99e9f  formal/tc10/TC10/Runtime/ModProcedure.lean
4363111a4af79dd46536db60b877f9b4bc0459a26018ffff2c3b78afca681272  formal/tc10/TC10/Runtime/ModReduction.lean
ba01b899ca4342456247318677e7512f2851012e03900da1c49e65d06c05dc5b  formal/tc10/TC10/Runtime/ModularMatrix.lean
75dd5edabd648577316023cc5c3a8ff81e54fad9864d02703a409aa47fde469f  formal/tc10/TC10/Runtime/ModularMatrixSemantics.lean
330d65d09cecfc2216e5a90e78606b9be47f7140e70e54382f0a0fe95f855c53  formal/tc10/TC10/Runtime/MomentConstruction.lean
e74c98d422d60d55f19efd4b270accd0280756c5aedd8ca78b21a4eb2ebdb7d4  formal/tc10/TC10/Runtime/MomentQuotient.lean
8c2cb4ffb0e228cafc55b36e38ff014d2df0732cc34ac4c74a5f746793b66ea8  formal/tc10/TC10/Runtime/NamingCopy.lean
eb9a7a57f618a4f145aac4e8c623eb5c948f1d895737290faddbde69a1060a69  formal/tc10/TC10/Runtime/OddPrimeGenerator.lean
dc3b71e2cd214a7f9dcd560c3536e67ee378d54f02c71ad4f786df7c02816f01  formal/tc10/TC10/Runtime/OddPrimeHitting.lean
077df58c0fb1bec63cb96fb63badb2ceb24dcff5a4130e115b8850ef97e1571a  formal/tc10/TC10/Runtime/OddPrimePipeline.lean
1d58b713d67b3cd5131f28b51eef03b9c2133f4321111321dbba206e5fa22692  formal/tc10/TC10/Runtime/PROVENANCE.txt
8df6e1c6f63b649a715969e9ec4494a827b5033ca6e39038ebd7e58c6cd2a7dd  formal/tc10/TC10/Runtime/PivotCompression.lean
f96a09532c8b7356a43fe24b227402c3d4c03105a790b6bb672d3dbcda0c9b82  formal/tc10/TC10/Runtime/PivotComputation.lean
8f4874eb6ec05b4c1f10bc8496e627b8a8ef21d176b9f9f222b76970b47339fb  formal/tc10/TC10/Runtime/PivotSelection.lean
7ab8ecb55ea1675720e8bf7f3a72e2f5e67a70bd39987ae1db65ee81717c7f36  formal/tc10/TC10/Runtime/PivotSelectionTime.lean
abd66d56742c7d462850fbe07901726a3f242d69c740e19a4ca8f8a8c1a483c3  formal/tc10/TC10/Runtime/PolynomialGCD.lean
00e179e944c2689c6eea44e5ae99827c9cd53e4320cb8595ce84ebf49bb3be85  formal/tc10/TC10/Runtime/PolynomialMatrix.lean
1a03b629df37d06fe6c5ad2c9c8e907d46b3fe1e31509181752efc6f56c426f1  formal/tc10/TC10/Runtime/PolynomialMonic.lean
8540c4596c26711d6ba3e54b2591226333baeaef8ff0fbcadb0811c00025e526  formal/tc10/TC10/Runtime/PolynomialRemainder.lean
a3133e82dda3fca5f66431f3782b86c664d55f275e00bb3f15c515975a5cf244  formal/tc10/TC10/Runtime/PositiveGenerator.lean
ee31d72419894c6d600c52cbdf44d9b82de3ea706c553f713c243833a6409c6e  formal/tc10/TC10/Runtime/PowerBasisArithmetic.lean
1bf52d01d73e10a30b0931df50f74d4c069b001c35b1aba18ae185c6e316fe3d  formal/tc10/TC10/Runtime/PowerBasisCoordinates.lean
854c58f8d6ae8ddfecacc7e07ec6862d4c2b09c4f1ff08f5a9be383e6d19820d  formal/tc10/TC10/Runtime/PowerBasisPivot.lean
d634876d375cf8c0f3eeca3b2d45b9f4218718a296f6311f416fa0dfc088215b  formal/tc10/TC10/Runtime/PowerBasisQuotient.lean
b91a0b578d92ca71a264e0b19bcc639b5e3d2cd183f4c4372428c44e2809675e  formal/tc10/TC10/Runtime/PrimeCodeBatch.lean
fa352171745bf7c0ae8cd188378e41c852bb392d558782511e2cf2721dbcabc6  formal/tc10/TC10/Runtime/PrimeDecodedAssembly.lean
464c8a81c4fa359e24b77a57b5a0218566eb21097c677684c723d9ad694af2dd  formal/tc10/TC10/Runtime/PrimeMatrixInverse.lean
466e0b1f671610fad97410fcaa97aa8f77358207b99714517e4cb9fcbda7459f  formal/tc10/TC10/Runtime/PrimeNames.lean
3aadb2d5cd82313f551035a4cdc5d858934c7278229a642435e97285b125b10a  formal/tc10/TC10/Runtime/PrimeNamesCorrectness.lean
378be8772a0a109cd59cc8fbd10d9c6f375f64962e79ace8552c532c5032550f  formal/tc10/TC10/Runtime/PrimeNamesInterface.lean
81d7da48e39715bd07f1e23468821343070ea8834ecca0480ea6dade09e24cc2  formal/tc10/TC10/Runtime/PrimeNamingBalance.lean
d377f5e8c377320d55652e935450acd9faff473dbc06ef517d1315fbaad04cdc  formal/tc10/TC10/Runtime/PrimeNamingTable.lean
5341f5cf3fc9ffc7f4dc1ace052f6a6e08778b0b4a6219d2325ff1024fe97ed2  formal/tc10/TC10/Runtime/PrimeOutput.lean
a2fc348d943e18dc36adfe8076f77a6b9a7a29ac9cc2d720cfd56e38b538f1db  formal/tc10/TC10/Runtime/PrimePalette.lean
636357580e7da96fd4e18316031846a32eb6f46878b496079f9513840eb95b87  formal/tc10/TC10/Runtime/PrimePipeline.lean
08172bb2e0a617d5a82037b3d7975e1ccf52f4039c1f2682f36834ca502b1dfe  formal/tc10/TC10/Runtime/PrimitiveRootSearch.lean
a42e714084756934a95719f4cfb48b1e0e70737eded7d2e43b37c878b7d869a0  formal/tc10/TC10/Runtime/ProcedureControl.lean
abdddb733b8c13b0d3650c3ab3f86baea6689fc53d09b159534150b47f685322  formal/tc10/TC10/Runtime/ProcedurePairs.lean
a5654f4733f6877b8abe1fd4d1ec840ab5a27fbc53cec07813b70c564b488d39  formal/tc10/TC10/Runtime/Procedures.lean
6cd7ba868f678059d853943f007e621c7ce3d10f097b9142a008b58a348cc412  formal/tc10/TC10/Runtime/QuotientMachine.lean
5f96977259de25d110219d03876244d4920944cec278d4aa8d0ccf7fd19d4f56  formal/tc10/TC10/Runtime/RationalCodeBatch.lean
41601cd5fa99c0401e4ee3e7dd2579032bc1328b7014276bba5dfc91f855bfe2  formal/tc10/TC10/Runtime/RationalDecodedAssembly.lean
401877fceed02f90f6f7c4f11b8630bc8c85bd350ab037d4939210b98132b403  formal/tc10/TC10/Runtime/RationalDesign.lean
d815e5e6c0d6bba573f0f3084f5ae6fcd6362e923bb32ed5d299da68e438af26  formal/tc10/TC10/Runtime/RationalExecutedHitting.lean
7f31faf43d20cdf1ca4df446ac995a9c944579457d41e40119ad0334ab581433  formal/tc10/TC10/Runtime/RationalGenerator.lean
63865a15e2461741cb430107f84971b8f1039dc90e469fdb02edf806b45e92b9  formal/tc10/TC10/Runtime/RationalLiteral.lean
a49e6c1ef358eb1b19ae525456bfb094d76033b071808f5dfcba4b5fa159d3c0  formal/tc10/TC10/Runtime/RationalMatrix.lean
1b2f3bbd22151702d25f41520341f1caa6f7010d6ded600c3a129bedc475c8f1  formal/tc10/TC10/Runtime/RationalNaming.lean
3a8f3f6e7f87abaa818248133b64ac7b11fb3cc0e4785d53329f8bea73489878  formal/tc10/TC10/Runtime/RationalNormalize.lean
81bfc09429297d82c5f8fb20e478b1d266ddb84b4c854c55c19e360b790245c3  formal/tc10/TC10/Runtime/RationalOutput.lean
f1ea0409a0a875e640be774713db0e70febbc96145338a1ad2de953b401f429f  formal/tc10/TC10/Runtime/RationalPipeline.lean
e238ec56ed13cfcc6f141230a25764fda60463a1029664c00fe63d830efe5955  formal/tc10/TC10/Runtime/RationalShortDecode.lean
717df0676ac82b9e3e7778f406825f42a918f862193de73172ae7b711678f28c  formal/tc10/TC10/Runtime/ResidueGrid.lean
5d16f8b0c037f0963a5e7a4ab4644dd4231fb5184a1ffb1e262f84d1c89aae5e  formal/tc10/TC10/Runtime/ResiduePrefix.lean
fde323ec51f33181d3cd0334ea2514739d3981fe6b0bdce6a5ed709327205392  formal/tc10/TC10/Runtime/ResidueSamples.lean
cafb07b6ded6be991c01c13c88d8c03dfc37d66bad68661f0ea1aeca948a154f  formal/tc10/TC10/Runtime/SampledPrimePipeline.lean
2067a15216dd81f5a6fb0cfb69155c9484ec2d5111d6db6477578dba798d3ea0  formal/tc10/TC10/Runtime/SelectedQuotient.lean
3362742297bfdbc1b370983b90c7dc7d7fda0ef2cd0d6c9f2d6717ca9ec39023  formal/tc10/TC10/Runtime/ShortCodeDecode.lean
46fbae06795c7cb3e7ceedf261daff87e2f0ad38b955a4c5fce13f7f6fadceef  formal/tc10/TC10/Runtime/SignedArithmetic.lean
98bcc3222ada53b9e5a66992a28a1b71d113467fdbf95df3f7567cf2ed93737c  formal/tc10/TC10/Runtime/SignedDifference.lean
695cebd65d6cb3d6a46d76421d1ab93db702b4d3b8f6b33f0c6682c17788123f  formal/tc10/TC10/Runtime/SmallCyclotomic.lean
d6846c8ad28afcc2e506b4775c61f7ad960ab1d1e0016d356375bbca1745a1a2  formal/tc10/TC10/Runtime/SmallFieldStep.lean
265c62e7b7bdcbc9dd1ef5aaee2c499459c2bdf020cab121aeb6630e8de3c036  formal/tc10/TC10/Runtime/SmallPrimeHitting.lean
d475ab0a5a6577711a0884af8717ce36017faf2c73dd9b5edbb29451a3ff4b19  formal/tc10/TC10/Runtime/SmallPrimeParameters.lean
9f93f77ba37b269c7ddc203e303dd4a6b89b327e19191e22dad7e752c2d5df57  formal/tc10/TC10/Runtime/SmallPrimePipeline.lean
d516f9412304d57e77d560f456339e0bbd40045d988d57219dbdcc030993ebc4  formal/tc10/TC10/Runtime/StackWords.lean
f8965ddf75e49e23e78e32ddf882cb208e8f3a921bf86a3179487a6ae54fd71a  formal/tc10/TC10/Runtime/Tabulation.lean
d53c440391bd251682675268b749f005f7a4595d89a194fcd9cf7eaa879ff1b6  formal/tc10/TC10/Runtime/UnaryDivision.lean
d046f455114dd6b424531d18a1965e556705a97d4b64a004ba3498598c2b9791  formal/tc10/TC10/Runtime/UnaryParameters.lean
05196fbab9c3e7311ad2ec4c8c39e549d5c1f63b9c6988cf913789a27af94096  formal/tc10/TC10/Runtime/UniformCoreParameters.lean
2fee5faf2bc90d9a0d4b9418c9e37d9419d300cdabf3447cc67dcdccf32106a0  formal/tc10/TC10/Runtime/WordProduct.lean
ec4a634b73aeecfd8a8690038cfd366dff2e743a03c574b846c2edf1c9abd884  formal/tc10/TC10/Runtime/WordRecords.lean
15e0a8b37a278228efbe1a3df47fbb6d6287b107222fd388f22ceecef13d9264  formal/tc10/TC10/RuntimeReduction.lean
338054a960c67796584a77384edbfbdb203433fb86fc498db379b7347fdd5b64  formal/tc10/TC10/SampledDescent.lean
ac891538abc2c7f4e06f89f354142d90e998ecaaead418b57fe3b06adab4fbb0  formal/tc10/TC10/ScalarCorollary.lean
6e4103ccbb640fc5e3fd1eaad5ad49919ed382cd1565671c13fac16bc56dff1e  formal/tc10/TC10/SchurCertificates.lean
d77572c06e9c4335278ac8a7083f5abfd7c813ea7e9dbfc8b9af714bdafb38e5  formal/tc10/TC10/SeedHeight.lean
fbfdb307583a0868c03906ec97ce3b3ecf9b75fca798b9a4d2955ceb1dbde7c0  formal/tc10/TC10/SeparableDescent.lean
552dceced26c9db8e0e1d9e139b0159779c5a218728524a122cb71a5e5f76b9a  formal/tc10/TC10/SeparableSplitting.lean
473c45f33540ae9b1dc84300c19f5fd0f6136f08ae11ba3904f0fe437d42924d  formal/tc10/TC10/SharpAssembly.lean
431990fe29606759c3cd8e17aadfef687853125afc9f9688493016e73b4a34c6  formal/tc10/TC10/SharpParameters.lean
eba00a4c3d5af1318a662596b5217297cd51cf786b2b505ced25d621a09fb4f0  formal/tc10/TC10/SharpSemantic.lean
761577e5b4ebd86cb21b871f64444db16e30fd511d3e5c45bd824022444aecf2  formal/tc10/TC10/ShortAssembly.lean
654455b863ac0f7ccee1f588d5dc93e1f32118ed42a85316036a1fccbd13754c  formal/tc10/TC10/ShortHonesty.lean
b9a80d179b35488e7a6cd1e62bd833c5bdcda13101579826de728f4ed1632235  formal/tc10/TC10/ShortWords.lean
058fb8b43a13bd1e984c27e0aca56eb81aa9e930d5ff03e859863ff0bcc6c47d  formal/tc10/TC10/SignedPowerBasis.lean
0875bd4cb51741c95fc8ebb8abd73a63dec7e6fc368e350d19d95c90250eacad  formal/tc10/TC10/SimultaneousRank.lean
cd03a8e9249bc9fc4c784c9eff372e9786591dbb3625f9dcbf669c77025243e4  formal/tc10/TC10/SimultaneousWitness.lean
c0f5cc4b09bcf2354a3a9388f29e4ec95fcf01a570cfb85451b403160a1051c1  formal/tc10/TC10/SplitDescent.lean
eacffbe24ca3dbec4fe45f94745b5af371c28fbe6e1a461713b95fc315633979  formal/tc10/TC10/SquareQuotient.lean
0c2b7490e0d12001b978d590866562145347793b409264afff5d7c48d8acf6ff  formal/tc10/TC10/StackLanguage.lean
e8e3d3814503d8d6c684e691b1651611d7f355b66b3f602f215c672c5cf7e932  formal/tc10/TC10/StackSimulation.lean
a4b73f7425c8da98a0cde2673aeb44d00aa7f620561f77cbc21bb8792e00d356  formal/tc10/TC10/StarOverlap.lean
d2719692700b2978ffe0a02097457befab267d1046919743a98ec868c29d8cdd  formal/tc10/TC10/StructuralRank.lean
f827e10533c249dd2280f679688708c5e03099cc2f517b77af8b01e196af6f26  formal/tc10/TC10/SubspaceOverlap.lean
6edd5d224d9c9796bd063070b52790c9a4fa65c3929872a0f3e1309208f2f811  formal/tc10/TC10/SupportAssembly.lean
f0c5702b97bc4d8dca5d368b4633a6df51a3323b877f1208bde11f949547ae85  formal/tc10/TC10/SupportBounds.lean
12c0be6d3a66d2aae038184499ac0415e5510fc34d15b767a02f8be326a059ad  formal/tc10/TC10/SupportRenaming.lean
6cd88889fe791438d2c4ded2ad5ce279877cb8197730ebb504b2c6fe8e1f441d  formal/tc10/TC10/Syntax.lean
9f5449fac8dc059dc943865c7f2c9fd1cab48558ccd6101255ed873dee2f3497  formal/tc10/TC10/TriangularDictionary.lean
2c1f1e2f106a1b4b6a1926cf378b4d908f0c43e1fefb2dbe73a6b57f4fe3063f  formal/tc10/TC10/TriangularPaths.lean
ab0c96e024c7b6f5e688c3912e1d03163516cce10c1fab24907edd8799a210cd  formal/tc10/TC10/UniformLogAssembly.lean
696ee22ab2223b8f105b1183c077543859fa23f63fbace3949e7c2e4a0a15497  formal/tc10/TC10/UniformParameters.lean
f94373e642f8769d1c3c125477ea3d7a3dc58eb5ae765b849b27911ef7a60fac  formal/tc10/TC10/UnitInputFiltering.lean
ac64078f10b5023fbc90db3c98d588f20b18165a1af27bb374f72dad83c00301  formal/tc10/TC10/UnitSubstitution.lean
e3a3c658238f0f700d77952337652e891cde477db2cc59b386fc531ca62419f4  formal/tc10/TC10/UniversalLowerBounds.lean
71114f05111db6f983b6c771986843f5b007987b8d745eef89997329d52f9833  formal/tc10/TC10/UniversalQuotient.lean
e07d5859f67ef45f0b72cd75d509db8cc1b1d89dacd4fb4b4bfd647c73064ccc  formal/tc10/TC10/VanishingBudget.lean
262770478e93e38b589df31cc9208f7bcee01bcef9ad60e72a1b6f89d4984786  formal/tc10/TC10/WeylEvaluation.lean
10f37699dc02d669332531a2cdf307d5ed15b5327a1aaec90903816933b05da8  formal/tc10/TC10/WeylSimilarity.lean
bf3c879328be49db5bbf58c0b9d5b2e536f631a1bed12209ccf3be0566b6a1e8  formal/tc10/TC10/WideAssembly.lean
a56982d0018f4cd2c7c502f0fef10643488df4c86e16ad455b12cf71d3260b88  formal/tc10/TC10/WideGreedy.lean
bc8d5f6b8c23dce46aafc76f0321240650ebbf47a5f94efedc315b139fc788f9  formal/tc10/TC10/WideNames.lean
d1197f92761a16c05bb42b75e3b86d99126533a8f98ca0332588c26ba1dbe76e  formal/tc10/TC10/WindowCounting.lean
fb2315e45179f82686d0fbb46f889fdae72fcff27703680208cc9263a71ec148  formal/tc10/TC10/ZeroBlockRank.lean
fd09a9b6959e46d930de8208a7cfc9b3f9f70c0e2ea58ac27b3ad59478632875  formal/tc10/TC10.lean
bde88fcdb9ea2c36a94c7a71b2682adb13a9a414aac066edd87907d7e0d43442  formal/tc10/THIRD_PARTY_NOTICES.txt
0443782977958f732664a4c82ae907f24876b19a686607274431872e9b4a909c  formal/tc10/lake-manifest.json
815c829ac0f0ee7c82e2520e37f6bac6e0b0db046b2a312b440149e00226ffac  formal/tc10/lakefile.toml
d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b  formal/tc10/lean-toolchain
c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4  formal/tc10/reference/openai/LICENSE
150c2ce4e096ece402853085966ef35a74ee0e8c11b49fa5073a2faf6c805c12  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Affine.lean
3bab2a514ae1501712c98c522edb5fa7ba786336bda0d6c44518cedb91bd7ce3  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinaryAddition.lean
4bff6eb4b88c8f158cd92a894c20e4afef9150af6d28af727501a8df5a353757  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinaryBinomial.lean
04f12c964896a9359ba0cb3856ea5ebbaec8184b8f7747d6142ba7794cb48252  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinaryDivision.lean
1092dcc2511a85fe31be3ea755bb4adffdd9859cbac60ed4f64154932419f080  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinaryFactorial.lean
5e6c815193a9008b64a03d1b731ef732a035ca0ffa6ad42b54f4bf4e0b276213  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinaryGcd.lean
37c41fe0f9ed732e19c70334560fdacb88309a64b1a22795931f7a2baa0c422a  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinaryMultiply.lean
f4bcb69e49f7b0a9e784f4eba6a45e8495f30065cfa9c7708533f6f1aff28a4c  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinarySubtract.lean
c16ceb963d82a84b81b9875973d1ae250c3d21ddf562faf006f61b497149dfa9  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BinomialBounds.lean
f9a44e5b957de26dcaf32d7ad981386937771d2714f4534ef266aad14ae0c224  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/BlockDivision.lean
316add6ab6f1c4be9c49fe63f18777de17e7a57ed4f8482b86532b14a48594c3  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Certificates.lean
781342669cdb1bedb9e906e40ee83717c3e8c1ece03f0355fc7f2f4a3bae0dd5  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Compiler.lean
380e783eef092537c95759d8fd8325eaa301ab1d17ab1395c1ceccff4e43e604  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/CyclotomicGrid.lean
2dbdeac316092ddeff4288add074dc86349e0a2304e1ac21808471c381459518  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Deformation.lean
a3ddfae5de0e2983c676e3c3b36032a305767e32b6b28d4232ee2e96d4d7d26e  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/DenseDeterminant.lean
43b5fa39dd1d986aa9bc2671ecfb05a28dd2fa99c019217e4969e2714ab7b919  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/DenseRecords.lean
a87a8a0d07d64de106fae3775a4bcfff22afd47da1c2a5c2ce1c839de7379e5b  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Determinant.lean
b5305c4cc1163ed96ebad22b426af852410372928ce83d27be7fb327b9efc875  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/EncodingBounds.lean
905252ba46c6581670a343546862a133c9f4afe6e825353f7ee1342e324f4137  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Evaluation.lean
60c2d0f5deac8733b279cec2f7706642d9dd57cb8ed6a3acb13dac09e21a5694  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Executable.lean
870f0eea69931966ddd8bed1569c2bb97bea4236e4b98a002bedfd26a59e647d  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Feasibility.lean
428903f929a24a5a50c6ea9548db73767c6fd7f5348900787d67f325b31f3a23  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/FiniteCompiler.lean
df62a7ca46e3bc62b0972ea58df49f8f2ec05a3fbb240a3da4403e5ab71b150f  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Generator.lean
d4be1543e872ebaa3383905dd0b72df77061b69087c8647937538ca24e940040  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/GridComputation.lean
f52e59c55bbf23cdeceff1e3b2fb49c26a179cd37c20d828de07cee2e252fa9e  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/InputAdapter.lean
8aa5d9a7f70bf38f9ed560c9edd4c534ea0fcd0269dddce681103dc9aa61706b  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/IntegralLift.lean
443d8f665723662fc157be7988ffc7acadeb689d23093dd6abd08fc8a3fed2c0  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/LaurentReduction.lean
9edf4a447c7260fd900a281b6817be6e11b90cf6fcb78b4e92f82761bc334f13  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/LiftComputation.lean
e6b67a5cc9bf0faac2dd64651c937eb7d34c6a23bea8a51b234a538516268a91  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/ListProcedures.lean
1de92103466695d67f6bbdbf44690af033aab4fb7e232228a702d3434e5203cd  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Main.lean
d112f1c17b310224e2f315c520bce895a8bb6a50341ff268320610e5b8775da6  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/MatrixComputation.lean
f771d1586a5f8ef4e32027a8a45e3a2bfdaeb35088b29abdc0cb99b512f4d2c2  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Model.lean
07205d181b0b85989ac62ab4bf9245a97b1fb862122652babac233ad986f84de  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/OutputAdapter.lean
86aa29328c8212103f7c97626f74a3d92715587473bb571c39c8b49c07141ebf  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/OutputComputation.lean
d2db6c61899ec87a477e71be2163bd5b40acec043f554cfe33bdf6e01f820a0e  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/PaddedRank.lean
2f6aa387f328f775cbc8aa58868191803056daba2fbd8944a1558adfe0c2a512  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/ProcedureControl.lean
6bdc1686c5e72e153cc0f1ea1be40d6c48951bc1e113ba1eed70d78b963af90e  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/ProcedurePairs.lean
550723cb370269161a146495411427b6961f89369e2a0dbab42d324f6f5c0bff  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Procedures.lean
650aaf7a5ae98b1f9e86d9aeae33cb7bac6d17911a9e6dc5f02a61cda1a2ba38  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/QuantumMatrices.lean
09ce9f6d7ccac2675f5622d5eff2ceffdcd24854fcc2787ce4a0852db652361d  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/QuantumSeries.lean
d395e01cc11554a2e30b225f5c2aae2db55a1f98d85f051d73e361d0bb95c397  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/RationalArithmetic.lean
ae72c71a4ceea72441fa35453b06f8ed8354c517301e9a0e020806307dfca494  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/RationalBinary.lean
a198e84aacdc75e4e7e4fa2c38a1b771166b97f196087a1c37169a0d3bfd54bb  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Rectangular.lean
6f1c681afd84b0a6a4438d7e26708e6b92ae73d9359c03662e2c61e01998b554  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/SignedArithmetic.lean
4ed008491ec8f4f4ee2f4e68d1a5c0c9ddc092a128e9e57aab60d1084c4ca9d1  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/SignedBinary.lean
cfe5a94f9afe7554c88de8549a58a2933a6254c71c8ca66cedf5fd94bd05c32b  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/SmallExpansion.lean
c134728f8a5bede784a25bc5fc7344de106c5442f8265bb6dea1c33fb6b8c160  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/StackLanguage.lean
852d3fa1d6e38240f77188ceee9dcfdcb0a73671e20cd7e68889610c6b76d1b2  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/StackSimulation.lean
7e7a94aa2b41b8881bf512628912157f4ed4515d2e83b5346ce9b2443044b409  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/StackWords.lean
d8dfdaad7a322b2b036f0ce538b0cdb0135edb4ab5651a20b4ab8dcc45577e1a  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Tabulation.lean
e55c22466ea48852589a05df5f77d73e4d45312e7ebdc0922910cf7f6d135e4a  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/TaylorComputation.lean
9c2781e8b3149a7dad651a3025c3d98468038dca57f6e27aaebfddb51e015d11  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/UnaryArithmetic.lean
b8a40b5768ee306bda6b1b3f64581d1e6346400104a7ba102de10a87f438b7c9  formal/tc10/reference/openai/lean/OAI/Computability/RationalHitting/Wronskian.lean
ac017f7be623fc159034664f84133f5634cd7ab82ca528d0fb4f6145fa99cf56  formal/tc10/reference/openai/provenance.json
ba766833a25fa02905434b5aa380a6f96d08d6e22bf89875309b9bf3cee85687  formal/tc10/scripts/arithmetic_smoke.lean
c68f0490aec00c78611153ab4beab365e2aa3a09f41a9bba1e2577a77bf73f62  formal/tc10/scripts/characteristic_two_example.py
336bc84b3a26ecb17e5566482bd7e981ec00a2f8c5ffa700dc439e61e68849d6  formal/tc10/scripts/check_supplement.py
8af1b523422c86abbb6c137d3a7459d967d28b2e22fb2db5f10fab08ae6476a5  formal/tc10/scripts/diagnostics.py
f7fc24007ebb623d4916bd1319715a941bd1cdb5e42a57344cbcd7a46505cbf7  formal/tc10/scripts/paper_declarations.lean
49bbacc17865ebccc468982f8ad563509661953895e146fa65fbf5ca02b4528a  formal/tc10/scripts/parameters.py
3c05aacc46fc3bff6c2b300bb5d90ded080a779cf16b675206f65c9ef1cf862f  formal/tc10/scripts/test_supplement.py
d170c720c8256b0be82f1bc0c653e998cb1e7d70df448fb84a1ebf091447afbf  formal/tc10/scripts/test_verify.py
aa78a4b4d460b3e16acd5d73789cf00118ea087264c6581c8fd2db2c59bfbe38  formal/tc10/scripts/verify.py
942c7e16e922e30cfe1ee987af291ec4aaea7c5f1a7739920f4687f5c9a6dd3e  formal/tc10/validation/abstract-changes.json
24dc7865f1dd8bd27aedc16b41b8765cacfed0f058af09b733279b0b3f77a670  formal/tc10/validation/acknowledgments-changes.json
970d825fe91f99b87383c5217149434302ad8ebfaab9da42dcfbf902fd856741  formal/tc10/validation/arithmetic-smoke.log
d7f13d93c1bd717b716ec2be6d9472d3d99f36005249c9b4a59a5b1d6298fd26  formal/tc10/validation/audit-parser-tests.log
25300c934aa6e48e35a2cb706631237de0b2e039a212289bca05f6b8824c3b44  formal/tc10/validation/axioms.log
ee19ea0c655fa1865e956b90a3169f578803323123aec46c8e4edcd1dd75a362  formal/tc10/validation/build.log
5e22fb942313a06065b527f8fefdbbdb4e0eb9ad500b17d96ba5a026648d6fe7  formal/tc10/validation/characteristic-two-example.log
202706900a8dc526385a28bfb03fb994bdf3534e0b3f5da2fa27712d0660bff1  formal/tc10/validation/contract.json
ee30760ebf792d415b1f721f7a54b7ef4aad511de29d471ea4cc6bde219563de  formal/tc10/validation/diagnostics.log
034bce3faec26e73f36096d1c7dd22c6d5b37d289c99687e5453f15db1bb201e  formal/tc10/validation/doi-changes.json
96b9ffc2539ab27060a22548c6ab3c50ea2985436927f67161e472c31de71c1f  formal/tc10/validation/exact-size-example-changes.json
2806f1eef11dfea48a796f0b72a56eb94acfbc708ff90147b5d7ee21e91f7e02  formal/tc10/validation/final-submission.json
0f594aa191c21c2b9c003026a0b856164a5759aa5a9655bde0cb301f4bb6750d  formal/tc10/validation/fresh-source-build.json
c48d93fe8a00b85b8d776cb7059b17538ee8ce076de23c04e176a94fa064c648  formal/tc10/validation/fresh-source-build.log
df43eb959b1edd708ee2ab62adad0a18b91ea0834ba42f1e682eb28493713976  formal/tc10/validation/historical-contract.json
24b8fe2ebb60a0efa61337b2fc9918fccf9e259ecea303718912ac5e33aa6510  formal/tc10/validation/improvements-changes.json
34b67937273fda33bacec26ac15aeff46a63ee2243bb6b68ca458ffacb2d0927  formal/tc10/validation/introduction-changes.json
20f42f897511ec814f7616bd9a193ae7504aa2f52fb05299eb752936eb77ca6e  formal/tc10/validation/lean-version.txt
ed4f6bc57738b92caf3af8375b0ea6ad841d8e59c164c78f58d4b53e4f936cfb  formal/tc10/validation/orcid-changes.json
7bd74ab76c03e22e203fe87a76a8d5578234da3226937530b58349d18f2d4569  formal/tc10/validation/paper-declarations.log
34d1dc90cd56f0288312b68c393f69a87107277facb8b6e8cdc5c99b8cb747d4  formal/tc10/validation/paper-map.json
a98f661aacece8bbe0938113125415692b81dd408433e300b1fb49572c67f5f3  formal/tc10/validation/publication-audit-changes.json
8f3a21ede4e165505139569fb27bf4679d8d05f375b19b751e68cfe83515f832  formal/tc10/validation/publication-source-build.json
20d196884043b6cc92269e2f6af2208d195faed74bd519e0ef902a01b5862355  formal/tc10/validation/publication-source-build.log
d8a32d60a3dcb5298ed6dcd9d1f216d985b116ac63c36b4facbef5f73a27e56b  formal/tc10/validation/reference-audit.json
e75d18f4c6237c117ca11ca062c5f2a36e7593349d50927ec28b9d4246ddfe09  formal/tc10/validation/references-changes.json
1dc202ca4055175e1f8d9cc1da64068fd5f7b6894b52ab6a5ad634243551fb53  formal/tc10/validation/remaining-changes.json
83bf60b5aa384a706db88cb6f2d0f16839fc3a070efed9ffcd44833fc93faefc  formal/tc10/validation/round1-changes.json
c475a73d79578ad6f6186a8b5ea52e64cda3c7c6b50d2ae69e25017dab27b162  formal/tc10/validation/round6-changes.json
27febb7d813832c1cb86da10b970d01407a33b4daa4f863118afc726bd62cad6  formal/tc10/validation/source-changes.json
1604127b93016b69df2bf6eb8904e038de02b9468ee25ea065f2c1484f5f61f4  formal/tc10/validation/supplement-excerpts.json
30c91fa18bf5a1cc5a7e176770cda15976b52eeb8f43c6e10b1eb50a1ce6d53e  formal/tc10/validation/supplement-tests.log
df4e2f22c5710ea78221142a3d702a13c04b1cca295cee0c8609c75001989af2  formal/tc10/validation/supplement-visual-audit.json
df5c016c89a68541ab4f4acc45ba7b2edb2893ede4159cf32164989dccc0d026  formal/tc10/validation/verification.json
94fe9a657e5f46e657966e51983b1226f7ac3a556317c401f9bfdb36904ce314  formal/tc10/validation/visual-audit.json
7f82b6974eb8cf82f72edbdc0160ce9bbfe112a1ed5e7da997ebbf074ba0472b  paper/main.pdf
92da3beb3a55c8bdd5d452b7f53b770023fc482f70b914a2f61c5edb54b1506b  paper/main.tex
fad5306a1c7a006915a93101d3e564bcfdc2a3f1dbdb17c8c6fc615cea0296f7  paper/supplement.pdf
5cfadd5f5f4c5accb1e1c4c8c7bead22953639d9292a23a8b6a6c49bf83b7c24  paper/supplement.tex
2ada86db93d0ad0bc97986c55978756235feaaf0482324c8dc93a5c5a697f598  zenodo-reservation.json
