d21c5621d78127e2f3328193bb07fc74e20dbeebb3ce6d00eda12e54abec7987  check/AuditCheck.lean
6d5020b2a89f5b639d7d3ea61d1401a410525cba9f0c98a3694a180bc75b5d8d  check/AuditTarget.lean
8d763314cf6da185aa662c4ca30f11e30127b4eeb416c2ebe85180804e55692c  .gitignore
0bf6638d730e2f89d277d0d771cef7e14aeb49f4607550fccf088cfafdc77844  Hilb3/Foundations/Artinian.lean
405032fc287084170177dfbf358846040a44ce81c4083a58766dfadeddd81790  Hilb3/Foundations/HilbertFunction.lean
dbaddaa04aa2e7828fcd1f636d46c12f5959e1d7b1aa5314a8d370d2b60cad05  Hilb3/Foundations/LinearChange.lean
1d4b2aa13b9830a5139f3999d20a475446d694ab7b7c15d2d253461951c70b12  Hilb3/Foundations/Local.lean
49dc98b13716ab87ab7f7bf2d5483f5ec32a117e2e113acdceb06613a2d93b48  Hilb3/Foundations/Zariski.lean
79fa5f4b9a7ef9225517348d4a93f9ba682c9ee6642363fbc054bc2222fcbb4f  Hilb3.lean
3b4144b455a65a87a3f7cd8dc477366667a5eefa463066479341149cd1f272ad  Hilb3/Main/B12.lean
98607b41136f5aa60635edbad390d735817c836316a6a6fa37d98130825be44b  Hilb3/Rays/Case13611.lean
286c403be938fd2f3765916c2bff41744392b1a74455c634bf605f62fba5050d  Hilb3/Rays/Cases136.lean
0bf23bf273677d28f1cb50512db98ae1f4dea12cd5516110a44f0aca55805145  Hilb3/Rays/Family.lean
c9f83aafd5fbb3f90fbd2490568de5f26942c050ed8890c8923e4ae1f9c251a7  Hilb3/Rays/Helpers.lean
4fc4cc3717223f819b7e2150de9fbad764df44a07abe228e85b97d6bf3b41900  Hilb3/Rays/PencilAlgebra.lean
c1ae7dc6fc2933182b414e371f055691f1c4d71671c54d397bcdd80be36398f4  Hilb3/Rays/Pencil.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
bc77dc3c2525fe68c9c2d19acf3d0092856d1ee9a86ee1a3357756fcb249e459  Hilb3/Surfaces/BinaryForms.lean
5473a83d374d8e90f09a7584eee7ea46aaa35130d97c17bf8082b8c283e9206c  Hilb3/Surfaces/SurfaceCriterion.lean
7c0af448af6933ce277b2036ac1181ff9785217b49626baebc5e6c9325806f0f  Hilb3/Surfaces/TypeA.lean
b38171806274da85c751dd45f6952c3b42dd1e9082c585e65bed7d52b23a6914  Hilb3/Surfaces/TypeDE.lean
d6140672f2b1929b3cf19b0c71c8b4515889b1c5b5f9cea44c47f696fbc3e8c1  Hilb3/Truncated/Basic.lean
5ec5d2cd6151d4e9b9cb917c071fc387c06f4b4d8d6c8926bd977d7fae49eca3  Hilb3/Truncated/FactorLift.lean
c7d415f31aa7fdf38d7e3a42aa92f5da8c6c617b521ae9c447bd9a36f1981488  Hilb3/Truncated/Hensel.lean
f82dc200aaed62a3b6cc1f6a0fadb1ea55bb78f68d3886c38eb041b75641e674  Hilb3/Truncated/Splitting.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
6dea52810bbe967c5392237e7adb8deb9ecc1ca6886706e4aa52036a97ddddd3  README.md
e8d9a1f32d3c237f645c9f4abcfb61baca998690e15ee864244e10dc04a10d79  VERIFY.sh
