590f525bd29921d9a9c3e56af630ee0f58571bf72c6042f67cc5519daddcb4cd  Odanorm/Ball/Bang.lean
1814f9724219fc5a57d882a16a0c392063767eaee4ffaa9394e19832458c5b1c  Odanorm/Ball/Basic.lean
be387393340aa5152b04ef3aece2a7abb445f153fdb7e2a2fbb1b5bd1417b807  Odanorm/Ball/Symmetrize.lean
3b93357835d0f54c4a3ebadbbbcf0b956df7dcbb6214675b3a8dac71f68abd29  Odanorm/Ball/Theorem.lean
e7cd06d7dda1ed7f6fb485105afd70ab36d6484c65a450425e6199436c56b122  Odanorm/CellCore.lean
0eb4079dfde682dc21b5522b42edaa83f2ecae09f9f42f64e83a979e8794ce57  Odanorm/Cell_cell0000.lean
64d6f6cd0da6ac6a2df967a6533c55696f39d125f5eea38d560b59781dc50271  Odanorm/Cell_cell0001.lean
65bcfb6fe1e522d0335bb4d0b5eb0aedbe10c1de4d2ac2ac548573f99a8c191b  Odanorm/Cell_cell1000high.lean
a170e17864ff10834e071be610f35e352ff653f5a34abd74ca40435fbc30e677  Odanorm/Cell_cell1000low.lean
17eb6546c0d7a5bd22b61982eb9db88b6a60b1126d61618e0139d26f0b24de89  Odanorm/Cell_cell1001.lean
f419621c95154013cd618f39d3b2ec70dc6cdbd43be2cba639604b3d7a600090  Odanorm/Cell_cell101x.lean
df46edafc826ee68bf6530941565dce5aacef2d39a1473bafc42df8a2094c19e  Odanorm/Certificate.lean
ad1e17863eca4b61d0c6267a5494cd4b418fee355aaac031c59023789042b5ae  Odanorm/Certificate2.lean
80d6f074b4402226622055758f5cf76fc945a44d6304420c0b6927deab4d8622  Odanorm/Cited.lean
fae755fff3d0d7eb1ba86c9a92fc95200150e7f4e2eddd0fbe059d84c14faad5  Odanorm/Completion.lean
984a33434723c366ec079467c62b3b4fc1f8858502ec0407ffe20a416970edf0  Odanorm/ContactPolytope.lean
40385f2452535b72a0d2c214877e626169ada7e9561a9e7f01231c03df6f1a75  Odanorm/Defs.lean
4d13a7d6934cd7a73f7dee88745be7c1ab322094269f16e6ceff83a4aa7fad86  Odanorm/Enlargement.lean
f79b893ba7c7b5c0093ff8ff388388ea276959e5b5dac155a0c9fe42f4a1543e  Odanorm/FacetDepthCore.lean
9c9f3d0f389494747687778952cc43299b5b390529aa05a3635d8d1eabfdb2fb  Odanorm/Farkas.lean
de23703f62e99f1e6b686ba43abf778ffa2cda4878fd3f6e5251b18cdc979c56  Odanorm/FarkasRational.lean
0f057e324d0099b992cf2713913a4e23ae63c0bc1dcf26c5132275eccbf3755d  Odanorm/FourStrips.lean
1db0732afd0fff074bbe85b4100048b972470f1e0e24ee7e94f070bc76106ee0  Odanorm/Main.lean
85d430a707f832445ea67e385d5591a3b21d396234b996e3eec3c52cfa611939  Odanorm/MatrixBridge.lean
0af9c399b7953f96362d3c040ac612e3dd6687fa661379d1cb2deebd9c9879f5  Odanorm/MatrixClassify.lean
52cd17cf8dd9db1efc3112b980cb5cfd7a6b058ca5a6eee73acce985e455bb60  Odanorm/MatrixLemma.lean
012715d5d760594b6b41ad66f630c6884ea380d9f2548bd7450c49136d164a1a  Odanorm/MatrixWitness.lean
d1431248ef2455b969f91b39e84647717632af777d73efb21fdc3294d57b6078  Odanorm/NormalForm.lean
e77a3440a62a09cf13fa561aef64cf4425cbff3f89e858b9fec580e5fcb3257d  Odanorm/ParityLens.lean
47dbece321014f5b75f598c61dcd21af5ed0acf626a192e662a1a4217785ead1  Odanorm/PickCore.lean
cf874cad66590599a5530ca42df4a8ec33da397b3fb34df5fcde3176bc8e412b  Odanorm/Projection.lean
64d644fec0f29c1947086b810b789630e83d1559249b75070a2393779274f5fb  Odanorm/S1/Basic.lean
5fc65febf4e5237d529afe5a25f9d7a47258ee15cb6ebb00507fff688dc7fd2c  Odanorm/S1/Chord.lean
15e075c3faf8a987583e48c9eb4220948ca13899be0a7de7051badb3d07f1714  Odanorm/S1/Doignon.lean
7e03720f4d679a26c729578e755e0ab2f20135e5849d635456be1d4a85f034de  Odanorm/S1/Face.lean
5b85249df83ed17af55ef8aa2a339e933311eb4ab9695ce29357aabed18c52bc  Odanorm/S1/Fan.lean
033f4e5b855d67cda57607789c6e362f56b1f4c4cd5c8778de569344fb47e07e  Odanorm/S1/HDesc.lean
b24a6f2428b30927a15b00378e225ddd4bdd34d29578e89bc1bc65255a49b77a  Odanorm/S1/HFull.lean
2df8cec04248e030b81b16fea11c3512861fa6f69ca203e3b906c90c608f28ff  Odanorm/S1/Main.lean
fd90d99cce2d13d62bee08f6a5ac4e2e1239f085c62d8702a6412c5e94cca3d5  Odanorm/S2/Det.lean
07ac6a7d5935f0934408680f5e3ce9ee0abb2e4ac529870e97489a4ebec3baa6  Odanorm/S2/Hull.lean
6d8669855894a07b48db6157e1c3f20e61210aaf68844f7fc4592bed0868e202  Odanorm/S2/Interface.lean
5716da2a1fc35767983b120fdc2c09088e97e8b3eaebeb3ee3e0627c03397415  Odanorm/S2/Kernel.lean
b0abe4b7200ed6d442a2414833df3ecf8789bf729573ca82c1386c9eb9239821  Odanorm/S2/Octa.lean
25b633baeee053d32dadf53c832737877b2898281a68e4575b203cf622517156  Odanorm/S2/Parity.lean
410569a438c304001dffe4f937153566ce335973da299b55265e25d0a1c3225a  Odanorm/S2/Small.lean
a077927ffe4a05c02b81d8613226accf916f5430da9b12da187dff685a0f895b  Odanorm/Stabilization.lean
a60509813fea4a0ea38d21cef33efd813ccb8e2e33e755bc89be30a28df071fe  Odanorm/WidthLemmaCore.lean
43dbe63449896466b67ef91173cc1c9215a0e06352b47f61bfdabab452894e41  Odanorm.lean
c353397ee1e43deff834239b0efc5ee3e610312522314b6c347ec284a0dd8af2  Reach.lean
cc0c2bc00e8ee446c23282de9d0796f2a2709c6861f63ca118e8222216e93452  Api.lean
8733782dc070a99b312039cda424f601b80f3be6f6f512627da5ba25adc27632  lean-toolchain
eb28a261ef3962ede7e2eac890c5a23f75613ba3d73d7d3fd52576626b19bb40  lake-manifest.json
2a634ee48c406e9fcee0202410068d0ded883418ceffa00acd515bff2da4e340  lakefile.toml
771f1f1eb4db8c1fbf306041a5c4ba215db7e31969663df01169156d77239dae  BUILD_LOG.txt
4fd85c74a21feb4b2fec826d2d31f5c5be3a13690e2b267a0f9ca328dec15c74  VERIFY.sh
a248c19a7ce7ad215e8f97fd6a8e5b85835ebf337458bf2568d91cff72a28dbe  README.md
091872374d359a3a63f2b619ea9d6f5b281d6e771c9389a60c7de60c749a5231  LICENSE
