488b4f14e704195cb1febdb01f26831d820e0fa973e48ebcfd49ef027973fb86  .gitignore
0d869a25889cfd58f2a1366f45c519b5d6951fe033a231f920c71f9bda72b92a  Kourovka/Ambient/Bilinear.lean
73f23ab2673feec114a5b30d9c7603f6f31e645a285b6edad6b11ee1bc01e8a7  Kourovka/Ambient/Checks/Chunk00.lean
184951a848e2935aec9795a8d4c153e049c2149621da280683de7049ff27f0ec  Kourovka/Ambient/Checks/Chunk01.lean
7d206bc12c705f4af3c0067196deb41b2849b37c3d5d29f74da338b2ed8ffd4c  Kourovka/Ambient/Checks/Chunk02.lean
5248e628699c2fd72e7843aed4ef0d752b6905dee8b152745bfa2ff51f6cdf28  Kourovka/Ambient/Checks/Chunk03.lean
e1b62f31bcf910a4cc10fa8f6d4845a87f7cb65bf503f8fae3cb00a278907d27  Kourovka/Ambient/Checks/Chunk04.lean
830a47356a7be572602876bb3e8997d798ff9d421b73aa32e5f4b10d6aa71d3a  Kourovka/Ambient/Checks/Chunk05.lean
a5a8aab2930043f17946584794a996602fe9514371c06e173071853eda21acc2  Kourovka/Ambient/Checks/Chunk06.lean
783866ecf5bc3e8396bd7720b3b61cec8a769da9d765ed34e22fb260cd639ee2  Kourovka/Ambient/Checks/Chunk07.lean
3846e5f82ad42be883d08443b387e47a6b5b22915de8f24662f64c4b55b98ac3  Kourovka/Ambient/Checks/Chunk08.lean
7685c58ab8abb1a8dc98dfbb2aa709a5443ffdc4751184845e6a80bee93c8c2f  Kourovka/Ambient/Checks/Chunk09.lean
d7045fd554bcf342979ba13a8a3e453c4f813f476b7c75f3e450c9ba10ba6227  Kourovka/Ambient/Checks/Chunk10.lean
0fec6ad5c98aaf40559400418d716f4f1a95f2d7799b9e9f8c0e8f0023a8b92f  Kourovka/Ambient/Checks/Chunk11.lean
4c60efba07a25ba3538b0866e7309ca7bed4d3ed11e8c8d77a354c349e9053ef  Kourovka/Ambient/Checks/Chunk12.lean
f9ae14b06971d332079e85278188063a875247eaa448b4094d006dccadc2b7ff  Kourovka/Ambient/Checks/Chunk13.lean
37548f20706986973050153eeecda0cdaa6763b8ea6cef84adfbb694bcc275f2  Kourovka/Ambient/Checks/Chunk14.lean
d60ab27556f78059a68d0577db65d9469d42058575e91d19b64e5c1c1885b629  Kourovka/Ambient/Checks/Chunk15.lean
314e3949324926794fbaacf3a0117316768030526559c61b53658c1776bf978c  Kourovka/Ambient/Checks/Chunk16.lean
60008c3328926e2f7e6ad7fabcc9059e6b2c073320b73128d166941f5ab237c6  Kourovka/Ambient/Checks/Chunk17.lean
8613e21eeb3eb08a44014af0fe044b6197978aa7f76c12ee0fb655e5cbb28d86  Kourovka/Ambient/Checks/Chunk18.lean
9e410d11ca11512927b949581fdf235e6cdc6175db08c45b23ee563839e50813  Kourovka/Ambient/Checks/Chunk19.lean
c7fea65af4f4452ededa6ebb7fc49f32aa1fb7068a32cdac1578bd75d387af52  Kourovka/Ambient/Checks/Chunk20.lean
b1d69a5daae0c99fd3c8cfc8b35a4157c368dfab5a4586864b982f383f85eeaa  Kourovka/Ambient/Checks/Chunk21.lean
4e61337d914516a36fc976ebf664e9d1021b139206bddbafbd8f241ad94f3aa9  Kourovka/Ambient/Checks/Chunk22.lean
ea42dc18806692c1b1a7553844032145f3573d4d1932ca353a6ce266c87e7e86  Kourovka/Ambient/Checks/Chunk23.lean
4bf73dfcd92314bd125731ded89bb353ff4995dbea5db18c5287e957cb8f25e4  Kourovka/Ambient/Checks/Chunk24.lean
1c263bf9a8a31d1ec5acee5bcefa87d532760a49cb47e345b3ca6c8be795defb  Kourovka/Ambient/Checks/Chunk25.lean
221f98b34d0f4357c5b3d35b847d7359380511e017c90b1f2adf26b7b1a91787  Kourovka/Ambient/Checks/Chunk26.lean
8077b450cd5e7c94e36677c684e7a5ff762fc4a27844913c5430ece92ed052a0  Kourovka/Ambient/Checks/Chunk27.lean
06c203e31c03cc4a09593b2a8fa16c65d6e3679df2845b394e8580757606f626  Kourovka/Ambient/Checks/Chunk28.lean
81232e931808948c5fff6c484e3c20fd24df2f99d9410ef101760893c21d72fc  Kourovka/Ambient/Checks/Chunk29.lean
1c9381643f57564b116c5c5559256fb18828c0ca8dd63b10c108ec5e23dfc3b7  Kourovka/Ambient/Checks/Chunk30.lean
8fb2765dae38b5dec03932793463a208b4d3068cdf0a86c2911d10a4e531adf4  Kourovka/Ambient/IntData.lean
53f760284abd276ff16380c61659b64641c7072b2733eb0f08f02048914b0c45  Kourovka/Ambient/Lie.lean
3e86d131455a3831571f576d17ebe93df0c95d4444f491b5a52685f14f391ff7  Kourovka/Analytic/NilpotentUnit.lean
b3b44d02176482401394ab0a85f75a1f71b85746eddfd7d8b4b38c781b5559de  Kourovka/Analytic/TensorAction.lean
a60bb4c3a61d0e972eefa476a10ce8462953f68001994c2a4eb4c66436508b82  Kourovka/BCH/CoefficientSoundness.lean
530f1de2e4eb3db07b9af4388e46ccc634a3d6fd82f205f0e8a8f2b8fc20aabe  Kourovka/BCH/Dynkin.lean
516ddb53cd42a51ed5720c31a683d9e3b0a54f1a1718fbdc58cdcac4b319852b  Kourovka/Bracket.lean
d882b66d44f601d2de6e0ad68c987c62276af70dd0d1ff517fb52c6a8f57f29e  Kourovka/Certificates/DerivationMatrix.lean
364b30ac9329114dcecd53ede936518eecfa2d1e152ce18696528ee48f6fde3d  Kourovka/Certificates/DiagonalKernel.lean
b3c84b3e441e768d4eefb9d242688011b8fc2741c3ad9159122f7c22198d98ae  Kourovka/Certificates/Elementary.lean
5c96e69552950263c0bf321004778ae7a4139142db0b00453735916dca7461a0  Kourovka/Certificates/Indexing.lean
39f3200b26746e8e04aa7efe6a3d072361128a8f7a95aba932f92f5f56515ae1  Kourovka/Certificates/InnerRank.lean
8c3655cdfae6c501ded0dbb91169d60bbef8108dbec8578246dd60e6fa91e848  Kourovka/Certificates/InnerScalarExtension.lean
a7c1faa2273d22ee5921a2197f6d03a63a83572cad48c1757284f5b3b66f4b1c  Kourovka/Certificates/KernelTransport.lean
0182b184e26201c47def3a08fec25c222a9aa2d3e0e6e5979fec46b536516a20  Kourovka/Certificates/ScalarKernel.lean
b4b27437be08565ab97f769af03d27b63b77a4e0933dc796442971d5ef404b68  Kourovka/Challenge.lean
c9bf685449b4da978c70979c702488966867898947b8b50c067eece4088accfb  Kourovka/ExportedData.lean
e17fa305052502efe8cd107e7b877acc61e400a45aacee952861a8c3dc155dac  Kourovka/Finite/AdditiveLinear.lean
ae71091cd38e59a1e6eb883c4fd6e32212cdde5d332c5a91219a38883212b75c  Kourovka/Finite/BracketTrees.lean
1b9ef7c1f66dabf98c87144afa7fbbe08281accd6f4ba955b3831e4a444f9cc8  Kourovka/Finite/Coordinates.lean
aa45b3a8f6b76ae57e71987eb73d70d529cb7218a0d15812d054547e23ac1cbc  Kourovka/Finite/LieAutomorphisms.lean
e1e5ee6613dac6d716769a9e0f9d7880a94fede3755b8250609de21e2ea45614  Kourovka/Finite/Nilpotency.lean
59d5d6a539724c73b9b3fbcb4ce1b467b4b6aaca61978756ed60b01339d2e697  Kourovka/Finite/PadicQuotient.lean
f1969f712a1170d8cf24eb4d79edd01a3a3982075d07fed19c0fed149cd8a5c7  Kourovka/Flag/Concrete.lean
2a2eb84244de1eb161069783b592c3d2429c7840dbcdaea24a2be150b7bebbb9  Kourovka/Flag/Generation.lean
bcd320a89e9e982c4a85a8a77f25762eb32f30e14a1d462389aca029d931f3f5  Kourovka/Flag/Rigidity.lean
ae81d5e5a4078b1b5ce208e010f0f78b712be0fa3c288672c36ab9388d0ebe5f  Kourovka/FlagScalars.lean
861c3eb0edd6f2cfff5a62d949bf28f9a8b59f143d5ee02952e5bde8fcbc61e8  Kourovka/Lattice/AdaptedBasis.lean
5acbe26744e8bfee96737381584d91e8e349ef6a820b304567df5f8ae28fd080  Kourovka/Lattice/Checks/Chunk00.lean
c0e434c867d0653f206ed59a36780ce0a524c5e9f432de0ae9703813dcce80e0  Kourovka/Lattice/Checks/Chunk01.lean
3f4c081fc96dac855e1e4fa81623202f48b96dbb923331c2b23d33f63067750a  Kourovka/Lattice/Checks/Chunk02.lean
0202b34f1945ce2aa6c9666f36b66cea5d9014e1eaa26e33d229a7ccfaca8101  Kourovka/Lattice/Checks/Chunk03.lean
68e243f1e048c0202715c4ee4531e9e3ee0ec366b50fbf74f9e24ea1644b8161  Kourovka/Lattice/Checks/Chunk04.lean
97009a0c8b347e2138efa608ce4763e47d68047d320bd001686a81cfb2a0bae8  Kourovka/Lattice/Checks/Chunk05.lean
a3c62d56a31fc163463295b2023c99cfc686c8208e307ffa8967effad55665b2  Kourovka/Lattice/Checks/Chunk06.lean
7af3933dc1e6fcdf1c08caf119840b9ea9304642bdbd05a62bcb0325fb642b44  Kourovka/Lattice/Checks/Chunk07.lean
c6152e8fde865d65aa269a6e59498a9bd28b2d7d58366f494e2e100f4a05a5cb  Kourovka/Lattice/Checks/Chunk08.lean
cb8a9c1af07023cc725a3c38d7fb34811b9420834d653be86f7fb20ac02f84ed  Kourovka/Lattice/Checks/Chunk09.lean
550350bba6552e452b230d4b298bcb737fb8bbce459b767895df6dae528022e0  Kourovka/Lattice/Checks/Chunk10.lean
fc2021a3f5b079fd89d9a628a1898c4310e938c0315cf073a0abe46c25b0587f  Kourovka/Lattice/Checks/Chunk11.lean
9f7288da89214edec0fcddd33b5a6cbf030f132dd0dce1a66389b62da117252c  Kourovka/Lattice/Checks/Chunk12.lean
02ee14f7f8db7c067dcc7f18d9476d8258d2bc733f84532e2abfb2dbd3cfce76  Kourovka/Lattice/Checks/Chunk13.lean
1e0a5587bfe1488c2c05ee8140cedd992e9293838ccee54686c158687e5f2467  Kourovka/Lattice/Checks/Chunk14.lean
da098ef0a289145248a98992a2db1506401fd91e1934931173f5c00e133c43d3  Kourovka/Lattice/Checks/Chunk15.lean
1a111605e717229f875b6899a83719043c5c3918cb14ce1f059f793f99b5ddbc  Kourovka/Lattice/Checks/Chunk16.lean
555c9b4c51b7c358f6481c1087e13970df5844b50f0c5df41d8ecbd1983d0976  Kourovka/Lattice/Checks/Chunk17.lean
5db48c488075800719eb01d23eb54387c1b06ba06088ae6fbae067ebce9da63c  Kourovka/Lattice/Checks/Chunk18.lean
9ba6f8debc669b2aa87d4d800e3b5a75ee3a5eba41eb7e239c576534bbb46240  Kourovka/Lattice/Checks/Chunk19.lean
4e9478ddf23f703388a9f573ef9b7ac34e2dcb514291533081d23b880caced37  Kourovka/Lattice/Checks/Chunk20.lean
f8e2f1a053204dbb6cc04a90ddd6e9c9a7346a2fe0c89d63d579c1b99aba40d8  Kourovka/Lattice/Checks/Chunk21.lean
a0150742cba96856e3a975fb26847a5637acc09fe545f006f398a940b203feb0  Kourovka/Lattice/Checks/Chunk22.lean
adc626b156039fa8716f5d3c4261b70360d3c0f68ffe25ae73a50252c456893b  Kourovka/Lattice/Checks/Chunk23.lean
72e2fb330f51507ed6a8c5c453521984e3daa19ed373837d756ccad8a9c82eea  Kourovka/Lattice/Checks/Chunk24.lean
baf9b5629438d3d21c860e813567e13674412c7fcfdbb89106cf798bbd3d1f87  Kourovka/Lattice/Checks/Chunk25.lean
e007ced9166cda612d87cf339fdd2a05f8f69e6867711bc7e52766d82de83f61  Kourovka/Lattice/Checks/Chunk26.lean
c896c1d34f73e0178d93d669779cc66e3880001e49045e996ff5bd9d5a93728d  Kourovka/Lattice/Checks/Chunk27.lean
7c6f53aa6bc203189996b84387c5f0f4e0f3e30e529aabd9757f0d6409163a1d  Kourovka/Lattice/Checks/Chunk28.lean
0c47cb207852932360abd67fcd14ac521ae89ce81b69c02ea64a7feba7120fd4  Kourovka/Lattice/Checks/Chunk29.lean
a5a1a7bc6b70034620f34d6b806da7ce2d775ae358f43ccfda29b4e3d6717621  Kourovka/Lattice/Checks/Chunk30.lean
b4f0591f6296cf4a3645f16e1549cac7a2180c4f20020c37d14c0f23a34ea0d4  Kourovka/Lattice/Expressions.lean
b396c9b866ff022b9eca1b218944e7c5527e10069eb2cf471ff77c65e50c892e  Kourovka/Lattice/Integral.lean
27394512d25c440eb0d58ed008f9f611cc3644ecf4d22655d73ff18dccce71aa  Kourovka/Lattice/IntegralGeneration.lean
eb306acbec48da5b98657e753d4e56057acbab02c231c506bc2ef7430690cf09  Kourovka/Lattice/NearIdentity.lean
451a9f686e402493dd10193e6b2b1364825854390fa8a3d6e83961bd21981537  Kourovka/Lattice/Precision.lean
d38b33a8d96c59b75e263480adeeabd09dbb0d2eeb47687ae6efc8f7c025a52a  Kourovka/Lattice/ScaledData.lean
a2aaceda2ac0d83e7ec5f9419f75206a98543f7f043065721f939065f86a0ce1  Kourovka/Lattice/WeightedFlags.lean
84236295ee0d7f8616d0003c14082abfffe326f3cb3d23d684207512f1028fc2  Kourovka/Linear/Basis.lean
96287df1d43c1bddf524b03a62915d728f2cafa58a95a241da23225c02c1fef8  Kourovka/Linear/BilinearOps.lean
61efb2e9dfecacae3e62156654692e63a28cbadaf5df4f496ceedc659240ca37  Kourovka/Linear/EndomorphismCoordinates.lean
b8e78e2bd8fce3379786ec8f21cac1a4dceb6ef1fe74696eb239896fff429938  Kourovka/Parameters.lean
2ea735d6f7e07512a8b08bb4e29b47904c14560b3fab474036bc224eebffcf48  Kourovka/RawCoefficients.lean
ae0f2975fcb6a82ff0e9dea71516f9205351f58d47ae24feca90c3422dbe12f2  Kourovka/TableCertificate.lean
d2c466087cce08db85c6c32bba6b3a13572dc6e24f6e8b24804f818de2e6926f  Kourovka/Words.lean
52c36d608ba7c481609616b3cbccdba0b091fea6fe68e6e0f7cc15639a7aafe3  Kourovka.lean
251c9ccd2c6faadc5fb2a3a01db9270efae6aaf40c40323c2004a97db675dbed  README.md
404f0f4d94d5169f0a270b4ca40eec352078ca52bb4c398799a7a7ed71b0daf7  SESSION_REPORT.md
7b63116b884bf8df7dfbb6c59fb564ac5a6a677413c81e8800d28e984ae6b34c  STATEMENT_CONTRACT.md
8585d46c8087020783396e6692a2eae1ad5e275ccfb43f9008200a313247eaad  data/generation_dag.json
d060acc6eb31c106ab31f64b139c07c9eb1ef978c648cdbbc5d1ee1a9987e22e  data/group_lie_presentation.json
372272a140795ee66bc8a9e849b6f99175c05bda3ed03b8a8b04b6bdecc40851  data/inner_left_inverse.json
db3d230587113604d473036f3493efef0dcbbeef54a61aa15f76e9bff1fece25  data/integral_generation_certificate.json
b07bac9121d4accc4161355f3b4fe56776156a8f30c61905e636290f3e2127aa  data/lie31_brackets.json
679c9615a8b0ea61e22e0a5067b34caaf901b984f0cd900a4e87ceedf3131e12  data/smith_pivot_plan.json
e4ba889f433bb0956b2ae5d6f0e94542d84b4de6ace758fe06f8de3776e5ee6c  data/smith_pivot_plan.txt
5f256540c9ea29945d322463e6ef058d37c6ae43c02eed3f06429d6b0d7e0aad  docs/API_LEDGER.md
858ce6f0751f19e9d069e678428d0f7d72d41eb8630130ccb36b4d07edc0acd5  docs/DECLARATION_MAP.md
c7ca28451b8fdfcfe3ec340433ffe5935f33a2534a0a20289d7ad0808fcc65c0  docs/DEPENDENCIES.md
11b525649263fae3be633b35d3b4d58ec230606e773b7d31c2b745ae2a4889eb  docs/DIRECT_FLAG_RIGIDITY.md
f364f1580e57a323f9e2621404745a47b21fbc0981b393cc18f00744ba2434ed  docs/OFFLINE_GUIDE.md
7d903897f066060c82cfb397904c1a5127daf7840b5a1951a682bdee13b55789  docs/REMAINING_OBLIGATIONS.md
29ec1b206cc9a802b1accadf34aeea27019b48bc6c3a206a76cef545af89b7ae  docs/REVIEWER_GUIDE.md
7b176607f9d55be9fa371688c66652db0d02ade21903175283ed8b80c3fef49d  docs/TRUST_REPORT.md
a145466c9d46a7808e1670d2b72cafdd52ef9381c884783d839f845a1e14c3b4  lake-manifest.json
608ad71fdf3eb59e6fdf8e648860060913e9a9ead652ffdc96d3d87fb55b0adb  lakefile.toml
55e97be96000b5e9e290c9e74482e5e317861499a5540353ce845471bded8cea  lean-toolchain
062afac1b877ad2aba78b96267c3b826981f1b447307e29d55654e4ff639e91a  logs/README.md
64adbebd1378d61ebdac059e3556fe83865fbbf200da21e5f95474deb3fd8da7  logs/connector_setup_failures.json
75acea0b966beb842a807a5658ca07861ca98d2468fa6cd9bc8e5534bcc47aa4  logs/direct_flag.json
cc11be3f7d60cfd10b26a60b864610b94ed9c6624be2e95b8da91dfb6612a38e  logs/direct_flag_final_check.log
152da82264ff30251cc59ae463d9ca80b96a42f46dac2e2709a0bd040054b637  logs/direct_flag_run.log
102a608227ffe28f06d296dc8a1d7123438f2b8b8be5c492a55caacd94932767  logs/direct_flag_stored_check.log
9620445b430da18cf6f254b6095583211582346db1f33ded92fdb66b36800903  logs/environment_probe.json
9620445b430da18cf6f254b6095583211582346db1f33ded92fdb66b36800903  logs/environment_probe_run.log
44885409656d55e27f0e3ef5adc50d68a7d02185250bcfb89755ec4cf740c124  logs/export_literal_check.log
c2191f43f0a2436ba727d6c064ab7eec8840e60ebd60910e18c47285f93a68b1  logs/final_gate.json
c2191f43f0a2436ba727d6c064ab7eec8840e60ebd60910e18c47285f93a68b1  logs/final_gate.log
9a7fde3a301bb503b8e436ff6bd725ea013e5c8f28c50bc20054a33638af848f  logs/fresh_original_verifier.log
c1ae4f27043dd940f90e6b63f8f29ffef0794d392bb494d5f90294e9ed8ddf00  logs/harness_tests.log
0b4c060db9ae12af946ac4f30630c5638fca3e06fe55fed1d3d862c091f8825f  logs/last_check.json
7807ed6733faa976ffeb9777efe9c9d83444c35e0f6d8017c7d528d4f775d2e8  logs/latest_source_check.json
0b4c060db9ae12af946ac4f30630c5638fca3e06fe55fed1d3d862c091f8825f  logs/milestone_gate.json
0b4c060db9ae12af946ac4f30630c5638fca3e06fe55fed1d3d862c091f8825f  logs/milestone_gate.log
35303375482c79285fff082996acd03b38a67b262bd536a119964e8cd9e29390  logs/runs/20260917T142746.228400Z/result.json
9d255ffa02f5a64baf3f9b43617672c5b790222cf53686fbe9255371674ed695  logs/runs/20260917T142758.282633Z/result.json
40c2114bf9c4373579beec163546f14997a445f6a3398dae065e543edd502cf6  logs/runs/20260917T143027.070184Z/result.json
d9a292db786811ce9f55436920ca79ebc1398b24977c79946f534eedad71ecaf  logs/runs/20260917T143031.112724Z/result.json
fc8cdb695ddc6990d602ef972206eef49d42ce93a277bc71d40c0f63f396f846  logs/runs/20260917T143202.609487Z/result.json
cf79352321bb64fcc4d989223fc7ece802f55fc514ff4cc13595641ec6a5c94d  logs/runs/20260917T143456.572140Z/result.json
a7487d51332ee1c03bfc9fd06bd50e8d84a698be8a41276fcefc75fa65f2e6fc  logs/runs/20260917T143629.366650Z/result.json
6ea937e135fb5a53a28011ad2d325449df8481b401b69c2863c477d832c8235f  logs/runs/20260917T144523.019255Z/result.json
cf841009f0a4041bcb853dfe2455427e17a36944ebb5917abf4486397e75cdc1  logs/runs/20260917T144526.436927Z/result.json
7807ed6733faa976ffeb9777efe9c9d83444c35e0f6d8017c7d528d4f775d2e8  logs/runs/20260917T144534.794953Z/result.json
396bca086b83b60424a9c76e236d57c403ba0a69de0d0f25f4b4bead82cd98b3  logs/source_acquisition.json
396bca086b83b60424a9c76e236d57c403ba0a69de0d0f25f4b4bead82cd98b3  logs/source_acquisition_run.log
e1ae11d2073105fd6a23892c8e13ae8c1717a3789febeb1f872b5d51298026b5  logs/source_expansion_2026-09-17/direct_flag.json
9b1bdc9d32f3aad5d378db6087aed20bebec5b6f7fadb224ee9014362b770706  logs/source_expansion_2026-09-17/external_evidence.json
52c76f7060f5cebae300445db163fc51f8e74a5086da7b9e447081efa46e46bf  logs/source_expansion_2026-09-17/final_gate.json
0a044f63925c1e555a2ed8186714450f74bdded1aa6915f8b7352b1638613bab  logs/source_expansion_2026-09-17/original_input_integrity.json
44885409656d55e27f0e3ef5adc50d68a7d02185250bcfb89755ec4cf740c124  logs/source_expansion_2026-09-17/original_literal_check.log
e46dbc669715ff7543e6e206c3515e197abb799a667d8a2def0073e306825d0f  logs/source_expansion_2026-09-17/prepared_inventory.json
6adf6f15c950a63cc15ea0113b278f67158821817b3ef33313dffdf81bf44b28  logs/source_expansion_2026-09-17/runner_controls.json
f21281c8df2e70decda7e41ff0a283e79ed84b0484288ac1e97bb163bf0242e0  logs/source_expansion_2026-09-17/static_scan.json
7efe9297294c2efbe5eeaa9c7395c17d5e95728a9e855fb5307e6ffc2dd2cd33  logs/source_expansion_2026-09-17/witness_regeneration.json
242e9d2c531a37968eea323f36cd7c34a4cbc91ec7cc27ea507f0249b69b1888  logs/static_scan.log
48eff5e789dcad564d84a3fbc5588bbc529cb6bcacfc402fce220d262664566a  progress.json
ad202437992b4657de982b01dc57368b2e6fe7cfbcb802bd58bf71b16ced5acb  reference/assignment.txt
5c6421b650bc87a2427a892a39e5522dc44543ca4ac1bd6e9f08d536c044a752  reference/mathlib_lake_manifest_upstream.json
da744da6f3bb3886dadac2382fe65d97acd8ee4f9afc9fac1b0fb733c2a5273e  reference/original_report_20260914.pdf
c007b1153a492619b69d5f3441799595dc3ea673adc85738b02d8b454d0aeed2  reference/original_report_20260914.tex
7f26df24672cb99158a6d7df1e65005137a06dda411784b874c86f35aa247d31  reference/original_verification_bundle.zip
0b6eb6c285fe24d45cd27e1849fd0ed2c05775ebd01a5f75cbe295211a2ebd13  reference/previous_progress_2026-09-16.json
c66ec188690024220fb5144ef12702104a438208935cf0455894c10c8c82ba9a  reference/provenance.json
d80e6a73ee0b8749d26b13a396d0cc5c5f044392d825ec55f5408a7383ca7818  reference/source_inventory.json
aca88c589ad6d756cc2cd0eb94531193040a0ec36fcc5988e31dbf25c1225b9c  reference/source_only_instruction.txt
5e48ba4b2599e26ded88841c76bc3e79d1d035fb98b9e06b5f39219ea1968805  reference/source_only_session.json
3ffce13054a957d1f36901369b31a256964d96814fda73d7ca29fe667dccdf87  scripts/audit_support.py
f109aeb8e6370ad562d2287b06e929af07770e13e7a84e3658ffa30de0f1bb4f  scripts/check.py
8605f883207a67a0d0d904c4b845f2fe623c56e6fa523e05c3fcf7f1e84b8afc  scripts/direct_flag.py
c0d79ef70930c150c658a8250d9c8bcfa32d6e426a42293ea2f2f9b4c028f158  scripts/environment_probe.py
76ce336a755fa2cb137db008bf96dafadd25759e53773b7948a5ba1d5743de87  scripts/export_lean.py
90ee10cafbed8ddffe3e0ab81d69a0f514f82f834b91b227bcbc7511a56512ef  scripts/fetch_frozen_source.py
2e7904c96147d47b092a8aa973575ced3313c71a9bb41d9a790254ac3d4cf3a7  scripts/generate_certificates.py
367da0eea73eb53dfafe47da090a21d0a92b2c920615644d250c9e13d8c8bfc4  scripts/source_evidence.py
013aea9c22013e3973cc4bf58c56efebde1afd28b705757f3c83197119b452a4  validation/AxiomAudit.lean
7b02bac89e03e0c1296edf83836c5d315fcea156b6638321da548cb5470efee5  validation/Statements.lean
