3a4502b215f486d4c2dd718cfec247befe424a47ce354a21ccb3168953cb40d1  DEPENDENCIES.md
a1da438398d4df276d5abd441c8baa654ff98312ece80e9211a6db05a40cd048  PROOFS.md
0b350943d4b1fd4532f02177de414f7406be8fb75372d10cf3e8677d85c77211  Project.toml
71de22038e8c4ebe9bb391d7e4b995adf4061b1494e4d075f629c73bd0746c78  README.md
2659313e6df58b03e6a1181fd786015d02e0091ef300110cf78685a8f9a0195b  REPRODUCTION.md
8b27cf29d5c9c738fa00eea721168ca7409ad2ce97417123e5263fdb7abc4c35  THEOREMS.toml
7a609115531637ecd1ef04b2b125e2f5e795875fad20b4dab1cd45ee6d966c70  THEOREM_GUIDE.md
9b6c232e062806665a3223f90edad4e838988f188b36bfb95a147d39245eadb7  TRANSLATION.md
eb5fdeaf1aeef4d3fa13f880fcbd19300974093bad98beb2bf3f84e7cafc033f  evidence/O0/gap_blocks.csv
63d3c849d626e3b808f35d376969f084c273ea61774f5538b9163006fbdea8f2  evidence/O0/polynomial_certificates.tsv
7e2c0313ff402b628cdd1ad809dc9539a4e594af2be556aa77353756cf59b5e3  evidence/O0/precision_sweep.csv
7fd085ae638ef4ff8a3e0486d371d30ee4897bc4dc737584e54a9c7c1895d64b  evidence/O0/rational_enclosures.tsv
28fc2001eaa7d9591b769f37d097f145c60dd37442241060d24fae5a9ae5aa20  evidence/O0/results.toml
b4269d3a331b2f2da0b4d55e9b012fde64a7f8e7b02a947d5e90cf607ccde466  evidence/O0/state_certificate.csv
93db690c00cc4ef19270895bd5a78fd497b67a27c58f871692d03575d3564df4  evidence/O0.log
eb5fdeaf1aeef4d3fa13f880fcbd19300974093bad98beb2bf3f84e7cafc033f  evidence/O3/gap_blocks.csv
63d3c849d626e3b808f35d376969f084c273ea61774f5538b9163006fbdea8f2  evidence/O3/polynomial_certificates.tsv
7e2c0313ff402b628cdd1ad809dc9539a4e594af2be556aa77353756cf59b5e3  evidence/O3/precision_sweep.csv
7fd085ae638ef4ff8a3e0486d371d30ee4897bc4dc737584e54a9c7c1895d64b  evidence/O3/rational_enclosures.tsv
28fc2001eaa7d9591b769f37d097f145c60dd37442241060d24fae5a9ae5aa20  evidence/O3/results.toml
b4269d3a331b2f2da0b4d55e9b012fde64a7f8e7b02a947d5e90cf607ccde466  evidence/O3/state_certificate.csv
93db690c00cc4ef19270895bd5a78fd497b67a27c58f871692d03575d3564df4  evidence/O3.log
6ba9b6c2f381fb21bbc907bed68eeb597ebfecd84ed38815ef1ef7ff3ac34457  evidence/optimization_comparison.tsv
ee7e51cbfb88cd8c18713119d9a1e083ef2d3bfb3afa40f5d2774944f15f1138  evidence/run_manifest.toml
3bcdc38005d5953dd77b10ab299a78c983b09a41230b7f779bc2b0a29ffa5e8d  evidence/source_and_environment.json
045d1f82645dd14fa2bdc114288cefdad44c922c06d76d61f299469f1a7ae139  examples/reconstruction.jl
0ee46b684ed08be98c69d1631b632b5a5607c638cd1b8cce2e4bdb9443b7d0b3  julia-version
bf8c5e04ee15ad4b1ec14cae878fdaf572d374e635f31191d750ab0c90de0121  reference/Lean/Omega/Affine.lean
4a0bdc5680cfb7123d6a0a206bb96bdedd6c3c5a49cc15a3d6835efe302efe07  reference/Lean/Omega/AxiomAudit.lean
a622442855d7d565b8a2ddf9364980f4919638c456229be4f2f4887a3eeea3fa  reference/Lean/Omega/Constants.lean
8f44a603b1448576055ffba4edaf62ca6a83773767962792fe785ea53f24b32f  reference/Lean/Omega/Dimension.lean
7305e893875398c5baa585d435eed4e9425cb0dcfa6b76d5d81f514317e2ca0c  reference/Lean/Omega/Extinction.lean
02bba826557c5206cc168a0eeef6dbd380b69e1892b4b2028e05bdfe6bd53a2d  reference/Lean/Omega/Finite.lean
774298bfb89beb990b8bdb6ef0cd95e1cedc7114b2aabf6b1949e91b33a652fb  reference/Lean/Omega/Floor.lean
1cb6284afc2eca467a90de27888d3157aa72cf39ebd788aac505bc256d24638b  reference/Lean/Omega/Geometry.lean
0a61e038b6c7a8cd42273aacaad53615be8fff13cc43ee61cf798d86ea392ae6  reference/Lean/Omega/Interface.lean
c4c833bd29e349e2550a4c2bfd67d6abe6b76a84a78041d81092f73e6e7d095c  reference/Lean/Omega/Ledger.lean
882556911c03bc06059a80a08a58bc87982dace224591e6368a0ffcad3b06bf8  reference/Lean/Omega/Main.lean
7715cf5d450e3d166858991f44c75a88ba67a8d3826789d9392cb0e7c32d7b0f  reference/Lean/Omega/Metrics.lean
6f4d106c949af1f9f12fe25f1a6cfe8a3691af58e3b2ecc26c0782d155690cb2  reference/Lean/Omega/Placement.lean
75e6164d192d8f659be9b73da00cb847017e9909631c93596b40d7ee4fad2010  reference/Lean/Omega.lean
c2accf70d8b425f6e660724c5df93f1f3521299158566f77fbc585aa1f71e51d  reference/Lean/PROOF_GUIDE.md
1396da8c8cd39227588d260b4086f1f7ae3aeec2f319251cb8e7879802986643  reference/Lean/README.md
23006d03bbb3b5ef00ed807d165904010c84b1061b65329a988dc6238616d828  reference/Lean/REPRODUCTION.md
f8208d18f6ac80dfbd4a7b73eec7bb865820e1c703717ee47bf1704ed0258e81  reference/Lean/SHA256SUMS
35122d4222988b074ab80e46316c050ab1b17d2047248396bbcce3489819ffd7  reference/Lean/SOURCE_MAPPING.md
82dae0644b5ce591c3e4af7bf9fdbfa6aeec11591560cb785ab0727a65d8eda1  reference/Lean/evidence/axioms.log
b34aef23107d7eb168cf4b1b3642791ab8a49bc7b5848843481e3a01e3be1ae6  reference/Lean/evidence/build.log
62555658e57af67df06d8ddb4fc1507ed6b8e6f43f63a289aefd1ee4f7e70768  reference/Lean/evidence/setup_lake_update.log
2d90f26571b91180cb175c34f8339ce30a4958bfdc573acd278f17ce2b538a3e  reference/Lean/lake-manifest.json
30e552cd01e0b82081a26f9446cab1960f1f157f9c120a86740fa3656eb56e5c  reference/Lean/lakefile.lean
55e97be96000b5e9e290c9e74482e5e317861499a5540353ce845471bded8cea  reference/Lean/lean-toolchain
f57f46411b7245ec715eb13e4546d82d273eb9a8bbfe186c9f4fbf07fe78f5c2  reference/Lean/scripts/check_axioms.py
0124bc35127d5d64c5f3b97a21c6705ba944c071f2d2e28abb3a4a6ae35d3adb  reference/Lean/scripts/lean_local.sh
b0318dff24ea404bf6f983697599e34947f49ef505a5a196fc64e2b30a8c810c  reference/Lean/scripts/self_exe.c
4131c9c3b40bad2320a5059f1e8daaf3cd0a78f4e30270b20ae0c3093def2b8c  reference/Lean/scripts/verify.sh
16a035f69fb06623d85260a9bde03d05d97bd0a0772d88636922d5cb2fe0ae1a  run_proofs.jl
10970faeffe0804073ffab73555cc0a5cb3dfd19892fa559e4ada68c454eb94e  scripts/check_inventory.jl
121953ec5044660dabefd0d811346c1c9ec6d1a94f17bb4c4d6ef551bd2ae489  scripts/export_guides.jl
ec08951e3c28cd8b2b299839ec5499c42aa0d2b233514b4a8e259af952bd3969  scripts/reproduce.jl
06a3a54b17c550736ed7d1daff907ec8cb15a2fce00a5cd857f9b0ebadcfdad9  src/Dynamics.jl
dcadae591fd616aca154c834a584109c038fc0bd27b38e2a1a2244a62af6b380  src/ExactArithmetic.jl
4a79980d4487c8de1e8f9dbe06a52163b06e5511d0e26ac35d31118d104c66af  src/Geometry.jl
f6cc1965c16635fed2956f81ffb9f9c81f39da11f15f4da0024f4b92b09dea27  src/OmegaNaughtProofs.jl
01bc9164c584fb87adef800cfa10ccc8c0cafea3e5241c663b1bf95bdf4aa91d  src/PolynomialCertificates.jl
4e98dd719a6f792b2490eccc27fe66966a2de8020bd9c2dd61929a4780f95af8  src/ProofGuide.jl
972dd8e9b4aee7f0101c8010935898a3b8e7fd316e99f3a863b30926049308b5  src/Verification.jl