8dc805c75a8f23f4d8c1176d9c57bb10fe183aa6d3cc907d9e1325f5d51c0e39  Odanorm/Ball/Bang.lean
2460fbc9a2a49d2795b4cba032108ed0ecfecae4d08572375f8bae9fcf909aab  Odanorm/Ball/Basic.lean
a4e634f3b9978aba7efb7789a8a1bae48b88ff27fb30f8c3e2856b264156106d  Odanorm/Ball/Symmetrize.lean
711bcb4b9c802e8a273d2224c5bd3e45cc1c919882d4f4e019b2d3106a05a89c  Odanorm/Ball/Theorem.lean
741bcb4b78b01f2cd2a27aa931cd7aa136078e7d3cb688413afd16878e5984d8  Odanorm/Cell_cell0000.lean
caf11aaa706d664e4a2efe460f28de222075ac4a9acd1ad12a5fc10049ac3117  Odanorm/Cell_cell0001.lean
ec194644a8c5773ad645188ea4c00c66761de690115ee529f2c984167fd612b3  Odanorm/Cell_cell1000high.lean
19c2991f42bca0cdf32fd188f0bb3146bda0b77046c427a059cc78d435eb794e  Odanorm/Cell_cell1000low.lean
b6d18333d0e5e609dab4997f8dbcd88e5dece411a8f8445a35b507e17c11c732  Odanorm/Cell_cell1001.lean
335a4474484cd2b56f6ca5396d30802a33bebdfb338c3d78a09aa0ed96a6afe8  Odanorm/Cell_cell101x.lean
5147d7f67d3ac6e22d84ac6abeb4f45f4b8262a0d0f95876e8159ad668e03c4d  Odanorm/CellCore.lean
71f9db5b09d372dd5f67a36abce0d1c35434ef44710f9c970740f67c65d88735  Odanorm/Certificate2.lean
371b8d89c2116ec37500418464d09388fe0a435e4b808001bf0cb19df17001de  Odanorm/Cited.lean
85b332a85d4752e1a243ea6dbc953693501931e437e9cd6b5faca32c4085eb48  Odanorm/Completion.lean
ff5dcbfccb112220bc60b19a4fda874d9c7db0b7c502d71904beb970ca3849d7  Odanorm/ContactPolytope.lean
7f52947833cd215826fba377ac8e3793d7dd0fa39e891147129d7537952155fe  Odanorm/Defs.lean
c7000fe48f1cf8dd1afa3c583fbcb16a03ffb9c8e5c0139f0c660089d72e0474  Odanorm/Enlargement.lean
0050f592d371f294f28375383411df27d8cd292cbace9c2c0fcc7e240a400ba5  Odanorm/FacetDepthCore.lean
9f7d4daa46f2a674bde7b65499584919efe862865c02393dd74512ecf0892040  Odanorm/Farkas.lean
60942c9f727988747998254cfca4164ad0d4ba964874080a3076e17dfbf05764  Odanorm/FarkasRational.lean
c1dd36d4df6162d55f9915bce6ab3bb0c0bbd0920ebcdab9471171c4e7fe6a64  Odanorm/FourStrips.lean
75ef0270cd3af947c64e07850c96e41e0d90dcf568d8878c231d7b3f72e14441  Odanorm/Main.lean
8e4d047207084323337dcee25c79ed5b673648f30c4e838822d96628f81cff3c  Odanorm/MatrixClassify.lean
01dbb17691d77655dd43e7adeec3c8ad3d00ade2afbfff39e638602750fe5eeb  Odanorm/MatrixLemma.lean
30155b39987943998cb146a9f3ba1104335ddb1087c019ebbd236eda2aa264ee  Odanorm/MatrixWitness.lean
5d65c34c60023c1c70348f6e706138bb39b7ca245a321c7550e258167c1630f4  Odanorm/NormalForm.lean
b00af8613a0b2f2acec7ed167e98a070101359e5fd62e2c138e4de60ae43bde3  Odanorm/ParityLens.lean
c825a5db56c3d75ab11913e85ac75a5f11f264c74a0df2d745bb95cd2e951bd1  Odanorm/PickCore.lean
5d4e9d1f73eef1de55133951f3ff6308dd867cbcc5fbfcc2c21340de62d5ced3  Odanorm/S1/Basic.lean
b726219e9b34951d6573d8f10eff73c35e7c70b53f9cb7069a23517eee570b1a  Odanorm/S1/Chord.lean
edbb0ddfbb598c4b22db40d50b07601bc340bb8074d02f5f7ba6d095a191eccc  Odanorm/S1/Doignon.lean
d64fff012c0e58fa165907ebac6206b9b0abab67dea9330e289bd164af26fead  Odanorm/S1/Face.lean
63bc6c6cc8af927b663fcd8ab08ec52363fa6d08aef631f1d85de0d8fa9d4385  Odanorm/S1/Fan.lean
2e05aecad4464b060fdb800b39442e45dab0a7b36ed30cdf1e49a98e0439e781  Odanorm/S1/Main.lean
85caad9a4482336e2b08d1e74a3305f14ac0a734880cba0e8677dbcfa33da526  Odanorm/S2/Det.lean
765054be57c7339341aea6fbe6fd8a7d9f734a1a8ba6c035bf6147a8417b55cc  Odanorm/S2/Hull.lean
1b8a1ba3af40c6f609f084c64c83b884b7a9b77f1254cd6abc457a8f43f20196  Odanorm/S2/Interface.lean
52d1d0c92c044cf04805429ba64860f99a3ec30b1d506770e1343c1f3d8d9349  Odanorm/S2/Kernel.lean
c4e70a08bf06e61dfa3633c8d192ee2e7fc8fe13b6c5b8bc83a24a96884e13d1  Odanorm/S2/Octa.lean
fd9f63b6b29a9392839116b31f647410dfaa4843f9c574a8a7eecc530a8189f1  Odanorm/S2/Parity.lean
ad525a4dbf376171770712862e51136199852044d4a691bc8f09a013ccfafd1d  Odanorm/S2/Small.lean
e51a2651e665b7042ce3702e1884756b52f68bd9865ec7b7bd399fcb89b29e1c  Odanorm/Stabilization.lean
f61c6452540c9dc19e675e102d113b549bb16ce0a2952127e3c9edf27fa803cf  Odanorm/WidthLemmaCore.lean
0db6739734eb621bdbb3ec05180e0d2d80dafb1b48e04eb606f01a4258bce92b  Odanorm.lean
c353397ee1e43deff834239b0efc5ee3e610312522314b6c347ec284a0dd8af2  Reach.lean
cc0c2bc00e8ee446c23282de9d0796f2a2709c6861f63ca118e8222216e93452  Api.lean
8733782dc070a99b312039cda424f601b80f3be6f6f512627da5ba25adc27632  lean-toolchain
eb28a261ef3962ede7e2eac890c5a23f75613ba3d73d7d3fd52576626b19bb40  lake-manifest.json
2a634ee48c406e9fcee0202410068d0ded883418ceffa00acd515bff2da4e340  lakefile.toml
18a4d1040ef959b06a52e04890279ab16259a7334df82a5a7558890a522e54f8  BUILD_LOG.txt
5d9a1dcf9ac9fb986bbed9f2fc8fdbcbf62250e10aa4de8cf94576030c4508ee  VERIFY.sh
18e1093502f6d0951c7e2c3f57ec4468af7e58594b58be4bdc0fddd9fb0e3aa5  README.md
091872374d359a3a63f2b619ea9d6f5b281d6e771c9389a60c7de60c749a5231  LICENSE
