2169449bb3f69bc799183c1830c5ab93f21c054878bc9adef058fe601ec1d653  .gitignore
407089696c1b94b86fb143a0d8664bea7913bb489710aac25551be702be57f03  LEAN_VERIFICATION_REPORT.md
225b0cead6b1b89932b5a5dc7ad6b891c26aae886b17657d04704182ac597f82  LICENSE
c14bcc56e1ed86972aff6cc3b62248a7a5d67a0e501938df4271d3926611d7c9  PROGRESS_LEDGER_v0.1.0.md
1cff05ed0fd4db3947e7b2425c361ad1fbf4d0e006e53be127806539aa362091  README.md
d009dfb679fc35c419c24cf32c1189ba9b3e270459210a77cb1ae424f697d90e  RealizationBoundaries/Ambient.lean
a1f15a06278486bc9874dd1b0cd7153776c948cef97cf16c9ded4c103bd0e038  RealizationBoundaries/Cocycle.lean
bcbaec5c016b15990b892ee0a1f443425ad394c525ab27ed5c279aa850b31483  RealizationBoundaries/Extensions.lean
4c48fffef4ed0db07ff506afe0aea5338cc646431114ce8c9acf8d4ab032df8e  RealizationBoundaries/FiniteQuotients.lean
f971b3a747e798ecf68a2545d0b663b97c5cc07fea0f3b6802a91ae62f6f7d27  RealizationBoundaries/NormalForms.lean
e1bd2087ee046750aa4a8df4055180492581987afb895be12985abcfccaf5c17  RealizationBoundaries/PairedPrimes.lean
258f910de6583f6a40a26547b616fd2316e13fbbb2ccaf140a2f5e7a0249fa3a  RealizationBoundaries/Preimages.lean
aaa9438390a872d47b29f0b64d24254fac85f3571d0100f1dedd896a7cae753d  RealizationBoundaries/Quotient.lean
59f264c6fb1ad6acea65047f285e6931be0d0424afaf5ed5a78f8d04caa79584  RealizationBoundaries/Sections.lean
2ffc39e740c4e98c8eb27eda7cdc8203052c5b324c1f8062c218fdb1d09d3a4c  RealizationBoundaries.lean
45e49baacd5fb5da40a4f444697303ad98a64d3436ddd7d51a19344a6da9b18c  docs/MONOGRAPH_COVERAGE.json
438f881681fadeec6b6a26b54bf99a9a047fabc1b9ea213cf4e707c32c3f849f  docs/MONOGRAPH_COVERAGE.md
08ee0b0d67ad5437d77ddda51fa4d9e8e530770f3d4738daa100a5ff092ff4d3  docs/NAMED_THEOREMS.json
36ec3a339770f42ac4f14f3994f833042120935d92aed3fb4189bf7c302188ca  lake-manifest.json
3bf184ff9cfc881b2a483c39b1a143aefc7b1f746c0aab7c55b09a7d2fd29ad8  lakefile.toml
8190e75a201741065fe508b28955dd64dd72d090babe5f70ce6848879d68ae88  lean-toolchain
96c26c420d6cd4c89fd0292066ce4ace8094a60e646b97fe25fcaad4ac940556  provenance/Realization_Boundaries_Final_Package.zip
7cc4d809402fcb81176ed2467d735bcc03d2dd4e0704c3776009507baa69e619  provenance/runtime_restoration.json
a33739eec9f11a1c8c6e94c30301963d9ed1386ea2ede04041bbaa644b046ecc  publication/Realization_Boundaries_Final.pdf
f9b23e7cb0ed0a21bc337e924a86c71c51a7174fc96053988158d6b59f1196dd  scripts/check.py
e459fad4589c442bdc6b32b9f1539160d4c79cee90a934a49f258bdd913c5e18  scripts/verify.py
0643d7e6144d9da52ad3edfd6d3e8b0c5f4b00e3e1d5ef0e3a6d0921cb0cc843  tests/Audit.lean
75237cf1f9a6ec5f274595eab5cfcc89df4303de115b5f619d64d287b1248118  tests/Contracts.lean
6f75cfb6fd1ffeb0fc869dbdc57dfc9541cc3c086a69ec90bd5c1f67994837b4  tests/CoreSmoke.lean
dd702d42399847c706b67dc9be9a4c09cf31b5d0022e60d2758f401608ae9eaa  tests/controls.json
a6c9db59223400d5a8289a66f9a1c7f8d9b8355e9ca1efbc9756bde03f91b62c  tests/negative/AutoImplicit.lean
fc034bf9a47106138bc455574033ec106fefd6cf98af0aafe7283d4bafee23b8  tests/negative/ChosenRoot.lean
4c665a64a3e12410b7ea039c7b99c067b6eb6f7748bfefc86f3f1d18267eb0ba  tests/negative/CompositeCoordinate.lean
630c78db7238ad9e8ced46d636ba5e5b29aa62c8aae9582b98f487c325425ae8  tests/negative/DenominatorUnit.lean
3d330f06e8b4db4f4dcdad276cc4263f2238ee9389860807cb4d594abee2a1a9  tests/negative/EmptySelector.lean
16a267a3f494346597c51d22d40870561a438739332f5782227eef92ea265d45  tests/negative/EraseCocycle.lean
b8fd8870e8d0aa426ad67149d342b5de220128fdbe3f22d9d54582d570647505  tests/negative/ExtraAxiom.lean
801bd6688c5e347545d74730199241f2a4816794aaa3923cab41ed79bbd4280e  tests/negative/NoPositivity.lean
f872b88fdc3f1cec4278bbe52716de4eb659c70a95d26fd72b6cb529ec7749b6  tests/negative/SorryAudit.lean
7b353894aabb5bc2aaee9609c3b7cef3dc47eccc9ea506a0d15686d8b5264ae7  tests/negative/UnsafeAudit.lean
d5c47a4980dbb8f59fec00e4855a2d9c905710de2929b0a6722aa4996ced518d  verification/DELIVERY_SUMMARY.json
e8ad50a7828b82be36345aee1edb3020ab9b70c95d9144ad6d8c93d65edcc6b2  verification/accepted/declarations.json
33ee01cae8120e09ea5859122d34de84852c8a7faddb56a375e416c0de7560db  verification/accepted/dependency_after.json
33ee01cae8120e09ea5859122d34de84852c8a7faddb56a375e416c0de7560db  verification/accepted/dependency_before.json
5a53acd8171eed9b9dcc2ce6ae696b3ce02394fb26612ed131499353cdfe0cc6  verification/accepted/imported_modules.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_Ambient.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_Cocycle.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_Extensions.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_FiniteQuotients.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_NormalForms.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_PairedPrimes.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_Preimages.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_Quotient.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_Sections.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/build_entrypoint.log
544b4920040fb4a18fbbf04c48a65f06739ab3268fc7d3c756bc1b64e823a094  verification/accepted/logs/compiler_version.log
b41c84ddc7f0adc769576c17db43f120eed7af110884381e657ca178a481e11a  verification/accepted/logs/negative_AutoImplicit.log
df0c408aac3ef04420c159f9392870bf6308395fcd4e55f67f06ec50bc9b27ea  verification/accepted/logs/negative_ChosenRoot.log
7b8c4cce0888db7d7a0dc558612d1540426ca3d0acdee475fd7fdb03b54b3f62  verification/accepted/logs/negative_CompositeCoordinate.log
270f79b354e3fd0b1b2f95bc6eb4b21c42734ad7639380343445eb2f7d6cefcb  verification/accepted/logs/negative_DenominatorUnit.log
7f08d6ebf8469e2c7d806deb4e86d10b540a25609c63025fc8ba0803b3a2c9b0  verification/accepted/logs/negative_EmptySelector.log
3bd39236026bf759b14f1ab0465e52a13eff175da0c2c5cb1726530d113d86f5  verification/accepted/logs/negative_EraseCocycle.log
f439c6580a72cc4805d4c08f27b004986bfc587b5f77d57326c64d71977e5b07  verification/accepted/logs/negative_ExtraAxiom.log
472e5cc26e6778d9bbadd0201e29c06cb60c88a10f74dd885fc4c99f711114fa  verification/accepted/logs/negative_NoPositivity.log
46e19e16cb10f3ff5efe9820b61645e82934388bcc02b0fc855f9726a2212e83  verification/accepted/logs/negative_SorryAudit.log
5013cf04a5287d832c634178b11b6d1b430f88429c502a68d5925ef59ec4cd8c  verification/accepted/logs/negative_UnsafeAudit.log
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/accepted/logs/positive_contracts.log
669acf82d2e6a7ed317efc7470ce2555eaf2a0028064f96b8e6715dfd873c232  verification/accepted/logs/preflight_audit.log
669acf82d2e6a7ed317efc7470ce2555eaf2a0028064f96b8e6715dfd873c232  verification/accepted/logs/production_audit.log
a3f04f48353d8cb6fdc7f47dc47f2dfe234299de4dca6672561b9d8cdbe93c7c  verification/accepted/logs/replay_Ambient.log
e502cc2c5a9aae3f3d403f8d5c728dc7bac4baac7d68ee6fe763ff654935c010  verification/accepted/logs/replay_Cocycle.log
a8684052b03ef8d9b335f159fe8372f836b726c0842042bb8c1c54fd3ba4ce3d  verification/accepted/logs/replay_Extensions.log
7ea69713dff61b5c571149f695a761625b9c0536ec226093b4689d98862cc8df  verification/accepted/logs/replay_FiniteQuotients.log
8a4dce8f6ab256439435de3583932589f59922a022f73234314b2d0117e71b99  verification/accepted/logs/replay_NormalForms.log
ab792fd75f217f1938f631cad85376082683e00d89ebe1e3f9c44306db27269a  verification/accepted/logs/replay_PairedPrimes.log
ba66bdeb797d110f1fd14cd222f7fe1bbd41645dca0097a3cd5209855c5cc1cb  verification/accepted/logs/replay_Preimages.log
3cf564e8a711ea0f6ff7db4d7e05e4fd7aaf81a53d9df0c05f4a52b26783fa15  verification/accepted/logs/replay_Quotient.log
4dfa44d9b47a97aea13713942c91cd3d9a1368238fc1391b863fb0ab13001960  verification/accepted/logs/replay_Sections.log
c1165e62d23f474e80d874b1764df76bb68a00e9c11711948cda58652dfba3d3  verification/accepted/run.json
914ba676502df87f591b6b2f10d1f248ea72a4594b7bb5d4722129591c62e99f  verification/accepted/source_after.json
914ba676502df87f591b6b2f10d1f248ea72a4594b7bb5d4722129591c62e99f  verification/accepted/source_before.json
b47bb93508b7c3167275e9809e407d348f076df217ab8b5260f9e1d2a6398912  verification/accepted_progress.log
72bb40f15e5a1b63c426ea5d409c44945c935302b4428a7174d5b4cbd243ee60  verification/audit_first_stdout.log
2688ede3eb490890482c95352b333f9c2a1c83c74568796d4693af664005d239  verification/development/Ambient_001.json
f767caa2514d33a61fd29bc9a54beaacdf0c7ebe6ebd5229c805610afe261878  verification/development/Ambient_001.log
5767082849744285edd273c642d17b31f2ffda40982860460f6c7db8edc81e3e  verification/development/Ambient_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/Ambient_002.log
cafbfe6bb2aa077742883245220d6110d4ed99ff7d0decbcbe467b9b03f1ced7  verification/development/Audit_001.json
bad5fc9bb4945d18129c7f2dae7ba52dd67743a6c60b6856d71b29ec6c2e36ea  verification/development/Audit_001.log
7dd4ab52c8fff191a056be20c44276d93606cd50bd9467220d340a1a0fb7371e  verification/development/Audit_002.json
ab38d24a8a14f8f95b0c34da5547b006f4450fbfa1c047ae5b4c2c54d5dd1542  verification/development/Audit_002.log
b4d51b96ddc48ee6daa655531522d587d145743e6807b531f2dcef03100beea9  verification/development/CheckNames.lean.txt
58fc6ea7e813061e502f8c25333e7a84fe300a1fc7d552144a29c8fa1c16e947  verification/development/CheckNames_001.json
db74a230b3cd307f222e0f433e7cc262bb24972e5db42a10ac8729ecc5dc7daa  verification/development/CheckNames_001.log
3379e7114c8364d963a66febed09ccaae79738ffb9bc2f41c118c7a75a0119f0  verification/development/Cocycle_001.json
21473239b94a26fb77fb5e188981986b0d467d5b44892da59c620bf2d912abc2  verification/development/Cocycle_001.log
79dafd09f43e7447b4ed4a66021b4477ccf9fdf4a1b744ab4eab3f5b130106c2  verification/development/Cocycle_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/Cocycle_002.log
f2eb3b8fa7583d402d45ff47119ae27671d6d97de476c6cf26f250baff2d91f1  verification/development/Contracts_001.json
afda55f90b5c15f74d5a8a600c9dcb13a39d9ad70a8281b3a288ab535a11f58e  verification/development/Contracts_001.log
d45635e436a68becc9febd984ff10dd072b1d1a4301f09e22249bd33cc3ceebf  verification/development/Contracts_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/Contracts_002.log
51dcdc47eb67355e7566c44eb516f8aa3fbb74839081ec017aee2ccf8018af51  verification/development/Extensions_001.json
fb0400514bcea98d1ce73e1d91248b8446acfada94dad3d0552accd79f1fb5ca  verification/development/Extensions_001.log
93c132bdbca6fb4b114e0ea4b6e04eea96204c15c2a7f73f01acdf25a9a6ca18  verification/development/Extensions_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/Extensions_002.log
2d0f53d80ee2e90a98179cba22a179c4b63a851c0683abc01448a27d2a0be709  verification/development/FiniteQuotients_001.json
14deb5cebcb147e46adaa0a2d6f458b6fd7dfbd2e5e1b2c321815d3bcaee3a03  verification/development/FiniteQuotients_001.log
b975a44a7d5e928986992982db549c85b28f7cfe077832a56f9029f519e49725  verification/development/FiniteQuotients_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/FiniteQuotients_002.log
40bcc15f093465f6820fe5057dafa8b68f04b982b406cd3153ead64963d98d9b  verification/development/FiniteQuotients_003.json
0fae5dccf1bb67ce92998331311366204693368f81a320104a52ccbd653268e4  verification/development/FiniteQuotients_003.log
507d32f8c1ffe8db16c5a560ad03cc97e786d5c43d0b6ffa0b8c48f521a3b771  verification/development/FiniteQuotients_004.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/FiniteQuotients_004.log
f90c49c15420b11ddbfad2dcc4942e0d108e4092b9194b74ace067b15a89f68a  verification/development/INCIDENTS.md
4ce84c199703e242bdf13a018a8fd3aa33174957c19c60d9e5b44440fec205e8  verification/development/NormalForms_001.json
f352913135ee5ef4cfd0d0e1796baa6db64d82ca5ffda755a272a56f5ef85404  verification/development/NormalForms_001.log
649b6d2903d51aa6760e2aac184e5b67503c9e578d61970708c75932b8a1256a  verification/development/NormalForms_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/NormalForms_002.log
3781ea125f0befd843c8ed30c46587b864c1724ca503a8b8d547f0d6675f4b0c  verification/development/PairedPrimes_001.json
a278d99f87a2c7f4abb45a5bb6b7ca7eb73b152b6d7dcbba17a4ddf15eaa8d09  verification/development/PairedPrimes_001.log
3ea7ce75ab0d14022c38c0e7f8a319edd853f694ec748cdc70a7dba0ab0ebb74  verification/development/PairedPrimes_002.json
8c1dd65915c64c67ee222ff6b9a2fa7193350ecc17bdc6e6e571049a04f97118  verification/development/PairedPrimes_002.log
5217145691b1acf45c0347df6e1c365cb5069febf4f86a210095d4326cd55657  verification/development/PairedPrimes_003.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/PairedPrimes_003.log
065edccb8fbd097f4265adc3e200006523e14d7c59fc8b30f863a3871773ecfa  verification/development/Preimages_001.json
eb2f37bb57bc7a0f3622e6a006f0276e483060d6f44ef80ba93f49a4ec724156  verification/development/Preimages_001.log
11a8f8f7203d3015ac11a70d2b37dce150e9d0226fb729a4874b8db3cddcd85a  verification/development/Preimages_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/Preimages_002.log
8d11b20358c19420913681d9be66e2b618a360daa249a9cb8f191f2b15790280  verification/development/Quotient_001.json
930c8070fdcea1c2cd2c30a98110eaf4125b1697356d38ebfb70c188e4807704  verification/development/Quotient_001.log
0aa2a560243e33bbf9e0ad55ee1c3a87de25d345446eba28bae4cb9b7d5cf52f  verification/development/Quotient_002.json
5707425a95176d19b9387b60847147e5f528a3b11ea23cee22556c0b526ea084  verification/development/Quotient_002.log
3b8e3d38f8813deb8c479a5f8c59929574b4a4f7c7cf6cb57849003a5cd0066d  verification/development/Quotient_003.json
9246b922c51ab84a2e07b6a2a90cb59b45d8b4c5cad61853aeafbd4b5041251f  verification/development/Quotient_003.log
2e72ca67fc2e9b17fc5654ee5e4f56d617b9433c0523b88b373a4083fd796059  verification/development/Quotient_004.json
aaf16cd376742c7f191771b2040abb9341eff2abc090b9bb03f69fa56d01434e  verification/development/Quotient_004.log
d311f6df9cae80d506bc15202cf293fabd47ff390cd467e3eb282fcfe754dfa0  verification/development/Quotient_005.json
8ca30943e2fb505941d7d20fc854d9fc0b3baa780f8fa2560a257b1822a94bc3  verification/development/Quotient_005.log
8554e87591af7c7ee7d387a2d008787f50f91a5875812176b158b13f67bba760  verification/development/Quotient_006.json
8ca30943e2fb505941d7d20fc854d9fc0b3baa780f8fa2560a257b1822a94bc3  verification/development/Quotient_006.log
4d601c87af29384bbca2978a0c54653397f74b8842a748d96a34687419407e79  verification/development/Quotient_007.json
e9f986d675815bbe17e01c6fb5b93cf1b631d39ac16252690ec28040650593c6  verification/development/Quotient_007.log
c19c5ae52c84fb1621611e9bbcf5a0bf74c054f08af35584c0c6b8577106b69a  verification/development/Quotient_008.json
dc26843cf39c1a1d27c239821d7a1462aca98551e3f9eb223815e2e8c7f3226c  verification/development/Quotient_008.log
97ad55f686c3ded06b24252b1cdb91237642839a51e1fd199d701c11d231dee0  verification/development/Quotient_009.json
d8a313958472b50eda1356f3ab080cef3d278a7a0fbac670fb9696cc749aac71  verification/development/Quotient_009.log
bf1ce63db5b3d1e12b185bf2785a6787c2bde312295cf21c19a7e8341275fd0e  verification/development/Quotient_010.json
057f33e5943588544ee2568a7960bc3316c6d7919dee8292778af072c955797d  verification/development/Quotient_010.log
1aedf15f5e29578787a1398e4c55e1ea8801b3d84999b99144e9c8e87db7ee0d  verification/development/Quotient_011.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/Quotient_011.log
47fcbcc7a51f62643f2b7f9cff0ab97b4e306b99acda03f5e60bcdcd7a976707  verification/development/Quotient_diamond.lean.txt
0c34658f92b52700d14f181b85da9bafb90900f079b2009c01423a6b53cc6a7b  verification/development/RealizationBoundaries_001.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/RealizationBoundaries_001.log
3d3f4123c3edf8a15f307a2d6fa428939e96cbe74b64fe9eb4153e73612abcaa  verification/development/RealizationBoundaries_002.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/RealizationBoundaries_002.log
3ab7efa82fdba49f2f920a1e1b79acaae224dae7fadc7d2624481af33bd09d88  verification/development/Sections_001.json
709a8466c19a2499ac556312013e06f7cd4daaabdec9fbc014cd6eb91ada870c  verification/development/Sections_001.log
d9eb83ba96c9cebc7ea020bbea9f77b482921f7e44614a7b2afc2268ef3e56b0  verification/development/Sections_002.json
990817cc8715af81d9e43cc34ed653b9cf9b71fd6ecc12f75a56317b03cd2efa  verification/development/Sections_002.log
bb2626ee0100bb7b6e0ee6c136ab7465fcbc9cb4240bfbe94c9f936e15cea862  verification/development/Sections_003.json
e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855  verification/development/Sections_003.log
f67c91b24faafd83441c1a85cc2e71de0ffd79342facae19b39047fda743059a  verification/development/ambient_01.log
b10c183100539cd4490c8498ecff2f41932b2c95c2e35e884b8526da2821387d  verification/development/ambient_02.log
045624d90c9733c8848f8a65bff2394cc215f1aad1a60d1453246cd389459c3b  verification/development/ambient_03.log
