dcae18176436581f16f03a25d21a76443c744c1473291fa3913e5b68bfdf0214  check/AuditCheck.lean
71d76eeb71899d6fee5b2fb9c8237e2b2567e44175696360e9e3fd00648c51fc  check/AuditTarget.lean
8d763314cf6da185aa662c4ca30f11e30127b4eeb416c2ebe85180804e55692c  .gitignore
0bf6638d730e2f89d277d0d771cef7e14aeb49f4607550fccf088cfafdc77844  Hilb3/Foundations/Artinian.lean
8ff1c4b6dfb62505119c21d7022ae4b5594099b1a86359f9fd6b3856f6dbc7a0  Hilb3/Foundations/Dominance.lean
405032fc287084170177dfbf358846040a44ce81c4083a58766dfadeddd81790  Hilb3/Foundations/HilbertFunction.lean
dbaddaa04aa2e7828fcd1f636d46c12f5959e1d7b1aa5314a8d370d2b60cad05  Hilb3/Foundations/LinearChange.lean
1d4b2aa13b9830a5139f3999d20a475446d694ab7b7c15d2d253461951c70b12  Hilb3/Foundations/Local.lean
acc465e9cd68f4551ea7c88b37b9b8bc07146655f6f79c93dc1481574eb28b20  Hilb3/Foundations/Macaulay.lean
49dc98b13716ab87ab7f7bf2d5483f5ec32a117e2e113acdceb06613a2d93b48  Hilb3/Foundations/Zariski.lean
9cb064a1f24b3df6da2a1b4133cedd5ba581798a682bdb07c2fc96acabd88002  Hilb3.lean
3b4144b455a65a87a3f7cd8dc477366667a5eefa463066479341149cd1f272ad  Hilb3/Main/B12.lean
31d385588953277b0b81a9227bb3626c6893d8feb73f91e201561d2e146529af  Hilb3/Main/B14.lean
de678c65a395846bdfda23034098b043b945d8ccaf200d1781e83d8cf8a05063  Hilb3/Rays/Case135311.lean
ea041463ab02aff3ecbbe64ea5bdc1d4d53e8882b172258526311c48e233bdff  Hilb3/Rays/Case13541.lean
73d77064376b7379a540b654cc2217caa141afa802a6c3ec3880c59c9f8acaf2  Hilb3/Rays/Case135k.lean
b4f45cd64f06bfd8d4ae04b7d5e3a85c33c52caeff3803ff6e30e118d5eb5f41  Hilb3/Rays/Case13611.lean
f85d61916818d3d885c445dd27d332c63ec21de05ae282bac8cddd607f49ae88  Hilb3/Rays/Case13621.lean
ad8f27608fea5e8c48bd499d652eff1e8c0fdc08d6a0f03f068b56ee2d1c4211  Hilb3/Rays/Case13622Family.lean
3418d35d5a86e3b59d11abbafba654e8730c9b4e46e61ae9088d83bf05c2fd42  Hilb3/Rays/Case13622.lean
cbfce5620217cc58fc9fe3642d2be5c5b84882f8c5327a3db8f1cedad47e2e9c  Hilb3/Rays/Case13631.lean
286c403be938fd2f3765916c2bff41744392b1a74455c634bf605f62fba5050d  Hilb3/Rays/Cases136.lean
0bf23bf273677d28f1cb50512db98ae1f4dea12cd5516110a44f0aca55805145  Hilb3/Rays/Family.lean
cb19d73849ee49cbb0b507b3d0306b866aba9a0a57b3ec6da27e2647056b4630  Hilb3/Rays/GoodPoint.lean
c9f83aafd5fbb3f90fbd2490568de5f26942c050ed8890c8923e4ae1f9c251a7  Hilb3/Rays/Helpers.lean
8d089946b10dd1028f0e8b9633d3b6f3a79464d245a05cb222e4a0d206afe30a  Hilb3/Rays/PencilAlgebra.lean
c1ae7dc6fc2933182b414e371f055691f1c4d71671c54d397bcdd80be36398f4  Hilb3/Rays/Pencil.lean
8cf92787f632fbc2e5ed58342e7b9ca6937f2db035bdb2e3196401bd695f9645  Hilb3/Rays/Tail.lean
2c7df2771fd08da662763b8c84c05cddb615a680a6c6dacd379f288f25e36c7e  Hilb3/Smoothability/BaseChange.lean
3f5bf6b4fe7640def3c5e93330dc2c93422de57ddea02ed82b0308cfa5163a24  Hilb3/Smoothability/Basic.lean
bc04804ae1f195b8ad35cac94239d003ce3ba51be5d8fdc8af973de42721bb8d  Hilb3/Smoothability/Curvilinear.lean
618915d7a89912df3ce1e18c2d2b0867b4970cf4b5a9a582717cf38f3a031360  Hilb3/Smoothability/Defs.lean
7bf47c2e5b3cf4c684ff6145527a80c7c4a123f00acea84f5d70e9f411a1df7c  Hilb3/Smoothability/Families.lean
f2dbee6bbc74005c2501619d4a6b89099a39f286f48c188bc7cafa2db4de541f  Hilb3/Smoothability/FormalLimit.lean
ac753d51f6be78c59b2ed324080ab07de023a96f19a974a0f1cf91ffcbc66dc9  Hilb3/Smoothability/Pairs.lean
cf2623a878d657990889fec153191991b7408c973fad172787763c2c0d80e878  Hilb3/Smoothability/Products.lean
5ed60c660aca3c7eb54a6c3ecf0eb51504b944aa4da96d14d64657190058be9b  Hilb3/Smoothability/Reduction.lean
0f7e6a181cd9bdd131a9eef9e342cc6c57f3b5f5dff0cd367c67131f497d79dc  Hilb3/Surfaces/ADE.lean
6b7d2e9ce1d65fcc028e112d60263c5738512aba8b550b8c99b75737b95dd702  Hilb3/Surfaces/BinaryForms.lean
0bafa42c6f57fd1f9986991a5f7465fa0eae5a8f71e5f462e732d4a55be078e2  Hilb3/Surfaces/NormalE.lean
5473a83d374d8e90f09a7584eee7ea46aaa35130d97c17bf8082b8c283e9206c  Hilb3/Surfaces/SurfaceCriterion.lean
7c0af448af6933ce277b2036ac1181ff9785217b49626baebc5e6c9325806f0f  Hilb3/Surfaces/TypeA.lean
b38171806274da85c751dd45f6952c3b42dd1e9082c585e65bed7d52b23a6914  Hilb3/Surfaces/TypeDE.lean
6b709bc7ad87f1fcbf043b37fc54cd77ff41b890a46cff19f3769b18af19aec1  Hilb3/Surfaces/TypeEFamily.lean
1778bfc5ad44f0dd529bd5c733d19f133c6ecd717b3b2bcece22248e149fcb93  Hilb3/Truncated/Basic.lean
5ec5d2cd6151d4e9b9cb917c071fc387c06f4b4d8d6c8926bd977d7fae49eca3  Hilb3/Truncated/FactorLift.lean
c7d415f31aa7fdf38d7e3a42aa92f5da8c6c617b521ae9c447bd9a36f1981488  Hilb3/Truncated/Hensel.lean
f82dc200aaed62a3b6cc1f6a0fadb1ea55bb78f68d3886c38eb041b75641e674  Hilb3/Truncated/Splitting.lean
6477433b40cbc31417cee631d379806b69eeeb307eb0c8e0ec1e450a8b0862e0  Hilb3/VeryCompressed/Cert10.lean
5055d6da47acd95094fd3d0f4e8a82d1570903a3f851ca1554b3fe48fbb0faa1  Hilb3/VeryCompressed/Cert3.lean
af0faa6c4c690911787a6e2a8709b914ff3a1795e93e9ad117ac54c0b13194d6  Hilb3/VeryCompressed/Cert4.lean
22933b347d8a7c4cf04373756aa45e15e0fe687eff8cff349c6f854b8b578e7c  Hilb3/VeryCompressed/Cert5.lean
3d81d968b4d9d5bd096e72f0c479079294a13398c2a3e069498cf495fc5c6c84  Hilb3/VeryCompressed/Cert6.lean
fcb617729136900c2af26562ee101139ba98e49053d3d3febea52b30a0bc1f06  Hilb3/VeryCompressed/Cert7.lean
8fbb6f3f9d21f0a50116e03d8d8d6241f07f09ab4875e1d022c448b1e94987df  Hilb3/VeryCompressed/Cert8.lean
5fa1928397fbe406eccf2e7948421f5225c9babcc2b7e6912b980cb62e68b643  Hilb3/VeryCompressed/Cert9.lean
27994dbb86bdc7a4c48ff1745277fdef6138f50772a3587ffc9d5753281b2f04  Hilb3/VeryCompressed/Cert.lean
fc1d8ea06f54532e69df7760a768eb666f6f4736e0028bd0a3e9b38741fcc3eb  Hilb3/VeryCompressed/Chart.lean
e52e60add33c1bc50a4c266e24c061f292cb61fbf83d504416eb4e53b5aa57fa  Hilb3/VeryCompressed/Derivative.lean
51dbba675bc50293ee2b6e8622566b339866229f6af58af875241ae8887c9e8e  Hilb3/VeryCompressed/Functional.lean
c69035a66360e092ef27cb8eae8dfc303bbd0bdaedc8b768097fa3712b04a6e9  Hilb3/VeryCompressed/Main.lean
e79b05211ee33eadf1ef775249fbdd6c8757dfe86ccb3e2ba679ca070951aed9  Hilb3/VeryCompressed/Monomials.lean
5fa59a371ac8c8461b44bde9bf8c2e7d6eccda3a9adc136adc2751a0a344cdf0  Hilb3/VeryCompressed/Points.lean
bd3ce42dd987f35e455c92dbd300d8085721581925c435c5b79664949d4e83c4  Hilb3/Zheng/A/Classification.lean
110f483d1684940a36f3fd9c4b4fb2df0cef135e7023ff766d40835bfa6c8eae  Hilb3/Zheng/A/Family.lean
5535cd906621c8503bb6fdb6ca464116a1fc88f34d33a81a0534c6112e28bb94  Hilb3/Zheng/A/FreeSyz.lean
4ec2efe06f9d133bf224fd4a0087340d2ba483280245aaf2f3608255c0bd3a84  Hilb3/Zheng/A/Main.lean
1a695e93372f0b4d5c558d440736b7179a721b26f6d10fe63169020876500c8c  Hilb3/Zheng/A/Move.lean
0c0c365ab63f478193de1843523f9883aa31b826e7a235cde48c09f8be984882  Hilb3/Zheng/A/Presentation.lean
4b01eb7f46e4ca9eec7248b75393599e387780da512c26be3485d6f7e32c4a7d  Hilb3/Zheng/A/Up.lean
c8b1561d8f3b217c2ef0ae537384c3f13f778a24b4b910da7472a1fd81459e5f  Hilb3/Zheng/A/Weights.lean
82fde540f986e91b81f2d143cbde2df8e65e5457142f37c87362491d531908fe  Hilb3/Zheng/CovariantsA.lean
8291e2a752130dbdbca563b4360fa61b9e4cee6e1a76d8d9fad585ca97f374ce  Hilb3/Zheng/D/Classification.lean
5790b89cd452346dd649af02507188be690600b4f0ca3e91dcfefee11e8a3d34  Hilb3/Zheng/D/Generators.lean
8a5c2a65719f41e44f17b651a4e7166a884f3cd7c66de464cd1a16642c541c29  Hilb3/Zheng/Dichotomy.lean
389a0fcf475b52412fce7ab0a11c09e09aea7fd11fe70b46c9538d100be68d95  Hilb3/Zheng/D/Main.lean
8cabda3b4078ea34ab7ee70a42649030f37b42c4e88a8b29f599715d85b01eeb  Hilb3/Zheng/D/MovesL1.lean
f9910d7a98c216687d783ffdf1fca2ecb8fd9afc68e32fd42c3fc705cb8cbe93  Hilb3/Zheng/D/MovesT1a.lean
dd67ff36ec7b087e3c67685a998eece9c9b2c9b5ab812553bc7e6b8c5c1cf246  Hilb3/Zheng/D/MovesT1b.lean
efc07df6c44942b7c7680e0087c883425a083256f9c753ea64a1bf6056236cef  Hilb3/Zheng/D/NormalForm.lean
6aaed3eed24a6ac15a0706a2e51c49400f28fd70a848d063bdc7863d613c7cad  Hilb3/Zheng/D/Potential.lean
5cba731576af63ca9860e11a9c923920769f160467200830e9c94305882d0305  Hilb3/Zheng/D/PseudoBlock.lean
f01908a9138043c349700cb2411210e102e23f3a2cf630a164b581cf002661e6  Hilb3/Zheng/D/Rep/Basic.lean
f2b54a55bb69ba5895ceb721c29f088e4e8b41fb12c78673bc8e306fbca13261  Hilb3/Zheng/D/Rep.lean
958f5859be21a20854daa4b79408d93905bd2277700a898f901b3366c1ab06c7  Hilb3/Zheng/E6/Classification/Decomp.lean
0c2671e7a7a23b220d4451e922f6e04fb24a258f807218f9ecaf590a97da5f9b  Hilb3/Zheng/E6/Classification/Frame.lean
69c669bd2c3abd3c06c4cd5c15bea3d1f57f112f2b1fe9b6aed2198d8dcab039  Hilb3/Zheng/E6/Classification.lean
651fd6b053983af6818c9de33ed6747aaafc3ab3a960f83e654c41b9d2fb790b  Hilb3/Zheng/E6/Classification/NormalForm.lean
9ff367a94041dd035db1d5e3842403365a04dba4c6b20c512fc2af81560f609a  Hilb3/Zheng/E6/Classification/Residue.lean
2f6e3f59b35bf8c4580e9f56e9fb127d0638ab732b7efdcfba53e951c16b9adf  Hilb3/Zheng/E6/Final.lean
4b80ac423ba5c96a3d45a85b5d3b589b2523255342670d5a7df4fd3179f9a7c5  Hilb3/Zheng/E6/Generators/Basic.lean
c6bf5b6b9c97b4a0c7286d853f3bd4a0bd6a9a61a254d7f0f983c5702d8276ec  Hilb3/Zheng/E6/Generators.lean
602bc4576b755e0f30cfb23609b73767ae1bb7c3ea19aa75febf37795e8bf812  Hilb3/Zheng/E6/Main.lean
7992be3954d08afd2c72b801d56e2186e5c55d3b5c300aa4d06e87f7f936bee5  Hilb3/Zheng/E6/MovesAR1.lean
ae886cbd6cab8ead91a8f56745b2cb51c86304e244095cb6aa81a39d92b44fd3  Hilb3/Zheng/E6/MovesAR2Data.lean
d20f4d9f2c1a8ea3887c4e280d5159f293f16037db47ab66f044a269a40e5515  Hilb3/Zheng/E6/MovesAR2.lean
81a7044a614868e5d9845c794e97d7e216354354c753b689634378466ac00d9c  Hilb3/Zheng/E6/MovesAR5Data.lean
679ca66bf63204d0e14eafb595b994a0ce682342c37e981e682a4ba73e48eece  Hilb3/Zheng/E6/MovesAR5.lean
16960dfdb6aec9b0987ce98ac78cfbf1f9505fad4b1ccbebbd28552a1663e95e  Hilb3/Zheng/E6/MovesAR6.lean
aab7ab2e659d7f93ab4e19ae6ac12288349cbf9d803f977b595ae01ece14dfab  Hilb3/Zheng/E6/MovesARBasic.lean
c582ec4553a363cf3d7ea0514b43ccdf73e468ff8610a766a656a827df01e831  Hilb3/Zheng/E6/MovesL1/Basic.lean
ba6d80c96eb7e67ee6d8d6a33bb9b2151508fd589d01201e4a5c06ef11232b33  Hilb3/Zheng/E6/MovesL1/Gens.lean
3d869ff010470214d06739e2a70545b2ad4d0e6f3912779142cdfc17e47f980a  Hilb3/Zheng/E6/MovesL1/M3Data.lean
1886124884ab422f4e54c571cde2026cef4265bc562c27b9944398ec128e6312  Hilb3/Zheng/E6/MovesL1/M3Dual.lean
4d7d70c7edd6c2875100fc1b53e6df433f53b1fbf5f8e3502fec9855915b9ad8  Hilb3/Zheng/E6/MovesL1M3.lean
b7219f4be691eeae574038d376379d5319bdcc1682fafb1917c9d1a038e8465e  Hilb3/Zheng/E6/MovesL1/M3Push.lean
2d231c02b8736f17c619b2f11d62d8a48a3b6577adcc5658e79085845acdda3b  Hilb3/Zheng/E6/MovesL1/M4Certs.lean
43a51ac4c17c2a1c71f2186778f111df64da8cd8a5eee14d180faa03036833b8  Hilb3/Zheng/E6/MovesL1/M4Data.lean
07b71fde5354bfeb0bf85c41a2393d1b7368ab09102958da268b98839371afa3  Hilb3/Zheng/E6/MovesL1M4.lean
de6e23ce12e5bb773fb88d9275d8ee22c9e77109bbaafb004cd0e4a1f84fc382  Hilb3/Zheng/E6/MovesL1/Reflect.lean
6b8447fb552f88d02e923d4d2ee7663ff150d1a1ce671c9063aaa4c39ebb53e7  Hilb3/Zheng/E6/MovesL1/ReflectMat.lean
0af17aa1169947e05f92d2d45e4a84a75d25288ab8fc6e663a3b14ae3ed81628  Hilb3/Zheng/E6/MovesSyzLad/Basic.lean
d22443104bc6e9cfa123a1b2111dbbcd6d11e61eba0aca8c32364bd439b6708c  Hilb3/Zheng/E6/MovesSyzLad/LadData.lean
7af855b7c243b9af3315bf46ed2d8fd25e1590f47611fcd95c967bf10ca9c322  Hilb3/Zheng/E6/MovesSyzLad/Lad.lean
939cb25657aaf0efcd83adae0b534f35c9b69b4b23ce3c883ce90bc1b648ceb6  Hilb3/Zheng/E6/MovesSyzLad/LadPData.lean
32401b45003036abc62639d4c54d6fe5e5e304ba56dcd8f8dcc2a5e35fa44146  Hilb3/Zheng/E6/MovesSyzLad/LadP.lean
977443af9273397b757b816725a766e3ff0b83684ccc54caed800a97b60fcff5  Hilb3/Zheng/E6/MovesSyzLad.lean
93cb1291fff1bbbdc270d81b9556ea6df86beb2aba199401ea83d85666c0eb85  Hilb3/Zheng/E6/MovesSyzLad/Syz52Data.lean
c516e7aed7fd0be57bfae413f6068c99de01ab1ba763c54d5dc86a6f88003325  Hilb3/Zheng/E6/MovesSyzLad/Syz52Gens1.lean
a736b26d2c457bb310d1bdd6677e67ddb3c6808e7becb0006fc19cddc82eef1f  Hilb3/Zheng/E6/MovesSyzLad/Syz52Gens2.lean
8b1068c862c1c7654cc437e77906d09ae10e545e58eb1f3609f217a5e2337709  Hilb3/Zheng/E6/MovesSyzLad/Syz52.lean
7021a45e1395ade1bc09c1adc3611d8b8f6272ca4f8e1db6cf7ce19205d01698  Hilb3/Zheng/E6/MovesSyzLad/Syz52O4.lean
4d400f2c3a2286059462e9b2fab814efb4f5a5e5e4430b73f4aea4e14429f1d9  Hilb3/Zheng/E6/MovesSyzLad/Syz52O5.lean
4563127234f2ea24ab75425e8350704559b66ace0e66504b7e4641fd14241307  Hilb3/Zheng/E6/MovesSyzLad/Syz61.lean
cb7851a0955074c03b8c3f8de7c61a35de1cb61944805acf49dbdc4fb94db773  Hilb3/Zheng/E6/Potential.lean
781ed1373503877ff6101311922454278802392374f557bd5d6ef346a291d916  Hilb3/Zheng/E6/Rep/Basic.lean
9477309a755f31708274d5470b641dd43b1216a9c858ce6eb4656249ac99c3c3  Hilb3/Zheng/E6/Rep.lean
d87443f82eb4ba01d6514291712e0e756f1555c82cba2765cf145fc41fa4a327  Hilb3/Zheng/E6/Rep/Matrices.lean
cf6974c55d50b552720e5864517746bd4e6b2c7388176733af55aaaf984fa318  Hilb3/Zheng/Family.lean
6f4029cf8421d72cb5476da3b506f9c86637abee272f179d31ef9957b760eaf1  Hilb3/Zheng/FlatLift.lean
6ee7e86e32d0ec7ffd064ba3fb09143c53259227301ec62a02e8c56ea9710ac2  Hilb3/Zheng/FreeSyz.lean
c631b567476ee1e69d0d90e68909506b3b6b99e42f65b473db4416046d9692f7  Hilb3/Zheng/HilbertBurch.lean
1dcbb25e65d5bb6adabe7d60b30720ba8f11d45dea31815809c7e389cd82675b  Hilb3/Zheng/Invariants/ModelA.lean
ed17cc61781142cd39461a2473d3f334f9fcf83f4ae5c1e81c8d416967964c94  Hilb3/Zheng/Invariants/ModelD/Basic.lean
4365541982b05cce2c0b55bc6c89ef008875d7873e6711041549b59d57e94b58  Hilb3/Zheng/Invariants/ModelD.lean
815756d2338cbe584f4d138c3d9e3fe864ed6725b6e8bae9b1ed156f564545b1  Hilb3/Zheng/Invariants/ModelE6/Basic.lean
e7a1da94f4e0bc6b9938c4b6da679d2a199f7d7e17f515633d8f470d5958a269  Hilb3/Zheng/Invariants/ModelE6.lean
d4a651383be211e8f16f09a82a5cad77d364b28a6245c5f62c6455ada0fc9b3e  Hilb3/Zheng/Invariants/Reynolds.lean
ecf0d97825fdc2800580dccbd4cd29ae40d9933a05449a09000a3174d796af77  Hilb3/Zheng/LocalSyzygy.lean
de93c5cf6f076b5e12e5fa76755fa685a586739a103c11811f4009a047a6e73d  Hilb3/Zheng/Minors2.lean
a0b90b70729a68c834d81998178d1a0782dc534c68abe724295a196b9a1a0186  Hilb3/Zheng/Minors.lean
2aa016b248da0697bcc775f295f49d720b2d18d2280c48f96ffd6b61f5cd157a  Hilb3/Zheng/Model.lean
92cfa53093085d6b043f826ee3731d6a0e7288b392c35b07a0a780551457e98e  Hilb3/Zheng/NearPartFibres.lean
9e57d85410490c78e2c87c9707dc49bef54d587f1fc45b208476dfbe83dee158  Hilb3/Zheng/NearPart.lean
d47f1a9a3c48ca7b7416f0b6dffa2db37d06f43fcb71df040e345d7fe14469e6  Hilb3/Zheng/Pres.lean
6cbbdb033d3f9ea09ed2f51300523b4c9fa0715bcaaf3aad0b0ddb3e4756a9a4  Hilb3/Zheng/Reduction.lean
c9dbe830422dc72059957e28bf5e7764e5d18438f2f31ec94a5f4dfca2adf329  Hilb3/Zheng/SubstL1Gen.lean
41467126736737be662ad8a0b8a22afb73e6d3931b6f8a53a5da42c1cc3e602a  Hilb3/Zheng/SubstL1.lean
d7aa3a669a044de3e1725d5493061e10f7f406ae9c9ea93c8e9d73b5aec4b249  Hilb3/Zheng/SubstMove.lean
90fa27644e4d968ab9a5d1eb13854a6e2dc92f75b48371a8879541db44bb43db  Hilb3/Zheng/SubstT1E.lean
82ed82f2135b1965557fa6de68c227b2351cff465a80efe92b4a046d8536ab90  Hilb3/Zheng/SubstT1.lean
706677061fa91cf038336d209b614f4adb5583bd9ce9a00aeb1cd1adea3bd8df  Hilb3/Zheng/Up.lean
23bbc7c78454c57d0e58a2835006c9522b96c4143c14907bccfd8d3c85a1997a  lakefile.toml
5a43f8cfe231742c7a9282383d03aac7ca3db03af186abe046a25a01ae22abe1  lake-manifest.json
8733782dc070a99b312039cda424f601b80f3be6f6f512627da5ba25adc27632  lean-toolchain
091872374d359a3a63f2b619ea9d6f5b281d6e771c9389a60c7de60c749a5231  LICENSE
a8edac211c98f2257531499a50467d99d4c1fa311434f7ab76b43ae46c706b5c  README.md
cb343c13b24853553e23f1664d59cc95fd67f88d94f5fed7896bdfff56aedc62  VERIFY.sh
