488b4f14e704195cb1febdb01f26831d820e0fa973e48ebcfd49ef027973fb86  .gitignore
47fbea5acf441af553eed43c37e67f84c2796823e8f071d16976e7600f62335b  Kourovka/Ambient/Bilinear.lean
00186ef3f0df5c799fd827b1e0db4bd62ed5718e862ae6450a5f5e465db0ee40  Kourovka/Ambient/Checks/Chunk00.lean
cdfe27b093b16aa67a96138c66fe18a0e39b6ec2be277c3f12ab833ec83aa4e6  Kourovka/Ambient/Checks/Chunk01.lean
243212707811b846360b6c77760e6db6fdf0b273698b74fa92e8195c3fd55e8f  Kourovka/Ambient/Checks/Chunk02.lean
773a61bb5e6981321f2d1d934937ea799989ca5b12c7f9745ccd6ffc1788e48b  Kourovka/Ambient/Checks/Chunk03.lean
ec05b6a250c09946bc8efacab2c9627c3c89caac5eb858119af6d714acd58fe2  Kourovka/Ambient/Checks/Chunk04.lean
f99bae8f6012dbd659c2c9812179e9fa49a105bb32d447cc53754f44dd991a53  Kourovka/Ambient/Checks/Chunk05.lean
25d3871c1efc983938bc343bf6736aaf23cf75d3dc2e123b20e0d7832486d1fc  Kourovka/Ambient/Checks/Chunk06.lean
9dd1223ecf6806e88d9bb23e057254833d939cf1e18131352ff0708345ba3649  Kourovka/Ambient/Checks/Chunk07.lean
a80fb3585209c49f1fe1e2cee446560385fb49ffb866f6fa071a694a02e57899  Kourovka/Ambient/Checks/Chunk08.lean
4f761ca6a973de34f052145ae836f0fcff6093f1852014b4e9cf2157dbbce66b  Kourovka/Ambient/Checks/Chunk09.lean
e9d6f78837964473af27114a0a59fe12754223c5fac6f74a142f88e79b16b47a  Kourovka/Ambient/Checks/Chunk10.lean
e8875f6d18e0a16e0bfadead1fea3459280e20a8a8e84168b3bfe01bf1d336bb  Kourovka/Ambient/Checks/Chunk11.lean
6ed6f16d9babee55d035375c566c289038a5d2bbd39b803cd1b928a52e47c050  Kourovka/Ambient/Checks/Chunk12.lean
2b227668a5b0118188c780ed3fd44646c537c2b6ac029a891778ed4cf60ff0d2  Kourovka/Ambient/Checks/Chunk13.lean
6039588d3cebd474841cdd00ce8823d581ab69eaadddb516190dccf88c4ad06c  Kourovka/Ambient/Checks/Chunk14.lean
122c69002b3b9f29315e7f38962e550878d17bad23e3cb998f4a6043dbff7260  Kourovka/Ambient/Checks/Chunk15.lean
9c47dd3e2dc2d24a1dee2df330d9f9ea1f70e4f397448cf78de5f977bd64a522  Kourovka/Ambient/Checks/Chunk16.lean
a7c010d6cf257028b4abcf908ff81aa959bbf85c209699f63eb9190ce5f8d7d7  Kourovka/Ambient/Checks/Chunk17.lean
9a32ee0b21b069866eff734eac206643aa8d7f0696ffeca2c580aa2ebce23eb1  Kourovka/Ambient/Checks/Chunk18.lean
391198b556be5d38ad56f6c77d4067763d13697bdf90ec8bd8c9fa4c275839a3  Kourovka/Ambient/Checks/Chunk19.lean
4ea28f91079a7f555bb6fd80978f2461c25601447dcd0d1aed1582a5948551f9  Kourovka/Ambient/Checks/Chunk20.lean
ab1044c7827d7524587459ea9ec45b1250fd605995ac64a121d50ebdfd6c36e9  Kourovka/Ambient/Checks/Chunk21.lean
4af4849bec90bf16b3daaf0be4fdd4d0341fefc6ab348ca4c97cdc62ad16bd86  Kourovka/Ambient/Checks/Chunk22.lean
0400c26205a14d7899cf4a8c96971b68e171e0e072df0db1e39c41422f513179  Kourovka/Ambient/Checks/Chunk23.lean
0328b45f7bfc712cb4e7e0566cccd2a5265b7afc0c7b0746170481937cbebc44  Kourovka/Ambient/Checks/Chunk24.lean
f1bb8fa418b439c04cf3341e4472424e54b99757cc1a5aa970c9e4105bea0802  Kourovka/Ambient/Checks/Chunk25.lean
9a1c434f59a8d8a91426d2b74a17892f5dba79a1e3212860f1f47a093bf418a4  Kourovka/Ambient/Checks/Chunk26.lean
7abdf692c0426be59b207722e2021aaa1ab4d6718080390467ff23a92f005ef6  Kourovka/Ambient/Checks/Chunk27.lean
bef886d701a2ea93f6e1b863d8841418c51cfbed5984b4dab35ea5b489dba4b4  Kourovka/Ambient/Checks/Chunk28.lean
168c459270cc3fb483d2169570680bc1ca1a100ed7df87b8647722bfe79ed3d0  Kourovka/Ambient/Checks/Chunk29.lean
9bddb63cd6c5fce8e201994ca719838eaf55c3b7a65027c2f502ce318984f0bd  Kourovka/Ambient/Checks/Chunk30.lean
53d7861d0a22222c75472cef995d88fbf600f6a3a623ce2e8b5fea67a5aa3c4a  Kourovka/Ambient/FastBasis.lean
8fb2765dae38b5dec03932793463a208b4d3068cdf0a86c2911d10a4e531adf4  Kourovka/Ambient/IntData.lean
9ed6faa9b48568a2e5232dc44d71614aed6036e0beb6052e6471ba57c0efa21e  Kourovka/Ambient/Lie.lean
3c86327eb006aa5c3dc4b046f6e56e5e9930278ea9ddb3322799d50d2b37707c  Kourovka/Analytic/NilpotentUnit.lean
002192ad25083e6d7b546ba1ddf985042deb52eb885f5c3745cdf3eff980566a  Kourovka/Analytic/TensorAction.lean
0aa48d13d08fea2a8ffb9638259f9916c710680a98d11bf8b52aff1989f0ef67  Kourovka/BCH/CoefficientSoundness.lean
e6ffb94aa31e0d02ea07b3e79aedb35492e80ab299a41607af6e264d679fff68  Kourovka/BCH/Dynkin.lean
516ddb53cd42a51ed5720c31a683d9e3b0a54f1a1718fbdc58cdcac4b319852b  Kourovka/Bracket.lean
5aa1191844804f7908afbff794865721adf4a41f17f0283d834588dc988be80f  Kourovka/Certificates/DerivationMatrix.lean
ed977eaa465e8f93502c308eda019d975556eef26a75e765e3604a5dd694ba55  Kourovka/Certificates/DiagonalKernel.lean
8dc33a357ffca81aee1d50580a51f51985b739b021a33f3c68a5296616c8a022  Kourovka/Certificates/Elementary.lean
0efdba3e54d6c00aaacd17289c1357cc8f0ccc124cf4bc137f9702ed783ba73d  Kourovka/Certificates/Indexing.lean
e4566d81274151a1f38c5f854b97be400c58d28a5b9b8e6a7a24af6e58cd9438  Kourovka/Certificates/InnerChecks/Row00.lean
faf019de733f0fa229eee77fb5bcc3b455a6d17d59474039042b0801f9f55d42  Kourovka/Certificates/InnerChecks/Row01.lean
08d3664e867c80024f53f14bf646ef269e4eea21068a92c3961fa9cf0aa109b7  Kourovka/Certificates/InnerChecks/Row02.lean
e5e4c7f99e6e1f8b916a89cdda9d27d3198f2bfe09789d13bf0a638e714de8d4  Kourovka/Certificates/InnerChecks/Row03.lean
3569f3bcd6cec35a040b837b7bb130afbfa9c006df33f5b9e1a722315a488da1  Kourovka/Certificates/InnerChecks/Row04.lean
6b3a5d35c564c8a72dd1f0138be9fc0d3021c9881dc02b94527f6cd8e3814ded  Kourovka/Certificates/InnerChecks/Row05.lean
379671351c3cdf32d364b5782a0e5ec5fd4c96443d2d4dc8745d103a98813e96  Kourovka/Certificates/InnerChecks/Row06.lean
20163259e778e5c26679ab005729f27765ceda5c97f3b99b53f8f7b13adcbfd7  Kourovka/Certificates/InnerChecks/Row07.lean
fd1a9d602c42d203bf7ed9064838cf8189a8070566df72f52c857329b3082228  Kourovka/Certificates/InnerChecks/Row08.lean
60bac143f1b398f89c2a85b5b508dd3b4b764bbea5036bdd6c7e962a95183d5a  Kourovka/Certificates/InnerChecks/Row09.lean
e442ee369ad939619f0b464ec2b9d51d854f1aa881f76072dbb9f40a79996e92  Kourovka/Certificates/InnerChecks/Row10.lean
568a16fe8e85cd92e44d5ec5192272b3ca8d90ec286029b79137401e6b182eed  Kourovka/Certificates/InnerChecks/Row11.lean
544299344cdc67745d74d2baab3906199d9d26cf77e072c04fb416ea60f57f8c  Kourovka/Certificates/InnerChecks/Row12.lean
30f23d2d521fcb1fcf2ae04a5e15a68496da7f608e7e46a40c3e650b6615acbe  Kourovka/Certificates/InnerChecks/Row13.lean
417b2c925a8627c9ae1d0e286fb5879430363fd334db97d3f90e65e363dba83a  Kourovka/Certificates/InnerChecks/Row14.lean
4f0276a0f0f489d58535d7015c2c974d03a0a8db8f9ac884cfe1bba3f812776d  Kourovka/Certificates/InnerChecks/Row15.lean
edf83a49198bc437e44ca373219fcb3e16e8adc9e0a2efa860578ed63cadc848  Kourovka/Certificates/InnerChecks/Row16.lean
9ab49c6c241333f754ee1c783c3b70afc4698f9300d824c6ca55ff8aea309739  Kourovka/Certificates/InnerChecks/Row17.lean
b9fbfaf97d3f5ff010154a38691dbc530a0e26eede5fb25b7a67d07836fe9b1b  Kourovka/Certificates/InnerChecks/Row18.lean
0d223fd874ec171ead30ac6a176e5a0d0a11ce6e786354a54a9719b3ceff76b4  Kourovka/Certificates/InnerChecks/Row19.lean
0ca4bb7484d7c4c86b2ec28b4635d3946e6a39ba6f89d08dbe361ac54afe35d2  Kourovka/Certificates/InnerChecks/Row20.lean
6d1e28314204b6e0ca820be96f5aed0f11cbd3dff091f5e95ce4fc064b7b1b39  Kourovka/Certificates/InnerChecks/Row21.lean
2eef0a791c0d34abf9db27e5254e4e2b3337788c906f7e29008d6fc340bd3058  Kourovka/Certificates/InnerChecks/Row22.lean
c4f0c46d49310ea81ffb30d2ba6a15e9f873c72e50b11c597c1eddd5baece3ba  Kourovka/Certificates/InnerChecks/Row23.lean
200287ea10e9a2284ac30c844fee0dbaf7f8a2df7b66edbed13f9653de01ba1e  Kourovka/Certificates/InnerChecks/Row24.lean
34185d371475a2d08341760d22278803d9e384c71f025f0f0f32e615b4c4aabf  Kourovka/Certificates/InnerChecks/Row25.lean
5a3b1a09e212a818c5ffef0083d5d500015fff14722ad7fbf6705d6e53863b52  Kourovka/Certificates/InnerChecks/Row26.lean
160b65be0bd83a1d7c0a077f510e944eb62c151fc47b319d89f30407456e594d  Kourovka/Certificates/InnerChecks/Row27.lean
2ca68cdcddb8ad99b5db510364495fb063b2ced95251f961d01cdcbca7430f54  Kourovka/Certificates/InnerChecks/Row28.lean
b968efb89265ddec4bddb508e808da9b89754bdb5f3e93ca2075b3f9b19be5dd  Kourovka/Certificates/InnerChecks/Row29.lean
1395ee4ed83ee5947011e92af566ad1778c2bda06cb3e83bde6fd87bdd9eb45a  Kourovka/Certificates/InnerRank.lean
771ccdf9e06e356d35db898b25de605a2052a1d1cfb6e3e36a97031072ff4b1c  Kourovka/Certificates/InnerScalarExtension.lean
3a54b465af01983cfabbaf2ec0edf55a1fd8c94f503575a15cebbb8aecca9a0f  Kourovka/Certificates/InnerScalarWitness.lean
c23422f043d10a4cb3a853be8bfa464bf27d949d5c07f2852b5d43b0d5e29cb7  Kourovka/Certificates/InnerWitness.lean
e6413e97fcca3d4c4f70764cd931a5234290669602cff78194a9138bfebe567d  Kourovka/Certificates/InnerWitnessData.lean
eac583ddd480fba5b7b58be174c8c0a65603b159f6a7f491be52e4ebddf31ec8  Kourovka/Certificates/KernelTransport.lean
1d7b926b3ff007722b7d2694cf0cbafc2ac7df593d712b804f954b94b78fa477  Kourovka/Certificates/ScalarKernel.lean
af058420b565f1d9f24448ce36fc9b9a3b7839673e443409bce879db73cb7205  Kourovka/Challenge.lean
c9bf685449b4da978c70979c702488966867898947b8b50c067eece4088accfb  Kourovka/ExportedData.lean
bbf2c376af4b94d4c09c47003c2dfa9952aff84368a992f217491567d69a25ed  Kourovka/Finite/AdditiveLinear.lean
19b6acbe2d36c10650b9a34f5bb506196afb9a9f235ef6609218a64ea4839bfb  Kourovka/Finite/BracketTrees.lean
fc138c37cf67e2ff61de6218596cf7602da30e4333af6b42646aa0a773b83286  Kourovka/Finite/Coordinates.lean
5010b32af93d32e82ac0fcd4e5fea7f31e83bc341f3e53b74cac87cbbb430a23  Kourovka/Finite/LieAutomorphisms.lean
fb4b6a914d41e7da2929e494c97cea938ec372a2d8dd18e3bd22e946a5ed773c  Kourovka/Finite/Nilpotency.lean
33c6059e685c87a5d9dbc332804848277582dcfeafadd3bd7bd33420b56cec0a  Kourovka/Finite/PadicQuotient.lean
bf3bfd86541caa21f939d1c45498d31c91399641ec52ad26e8c0597153d2f412  Kourovka/Flag/Concrete.lean
0c93f7f08191a8490f540143e5795404547e3c34cb01b6ea4b7eb84116011f33  Kourovka/Flag/Generation.lean
2cf97f53a7af3cb20ad8a5f9ab16395886caaf430d70427772fe2926d25c8bd9  Kourovka/Flag/Rigidity.lean
ae81d5e5a4078b1b5ce208e010f0f78b712be0fa3c288672c36ab9388d0ebe5f  Kourovka/FlagScalars.lean
0980999013aea778c055b612e979d95383fa8ef71c8c274f3bef86a6d736945f  Kourovka/Lattice/AdaptedBasis.lean
e9af997db764ab95c5cb4793c2d1bfa7a2effe721287a8ea1b45a254f1118e69  Kourovka/Lattice/Checks/Chunk00.lean
e2ec5b514ec68197dfb314d07720e4cf3c88b65f44762dd92fbbb988ef1ec6fc  Kourovka/Lattice/Checks/Chunk01.lean
bc51c76ca6331e0a0c0908cc70cbfe5ecfde0e2d2a582b7c5ba16dfe158b43ae  Kourovka/Lattice/Checks/Chunk02.lean
9b21f2e04d1da9d9a28ce4b872da044383f2e17383144466457aad4f8e7ae482  Kourovka/Lattice/Checks/Chunk03.lean
c8038fce1cebc90d3a8a079935f6f55de0be501aec2b11d533c54c5fcefad20c  Kourovka/Lattice/Checks/Chunk04.lean
45b01412e8f9b528aea4c66730ee64e5f8b4ff5a93f69eb8e23dd13711c7e2f0  Kourovka/Lattice/Checks/Chunk05.lean
731c6a38bed8c1e1618701366a00f01ff9392bb6c2ef562c36478b272fa9eaee  Kourovka/Lattice/Checks/Chunk06.lean
404f6f946052d2f2c01025c3d9051d10c3447d380d2c1f5097cef6816762457e  Kourovka/Lattice/Checks/Chunk07.lean
59039c6e550fcd1b7aba7f8c7e04824cc811b37780d8a14d15e0cca26f12eb51  Kourovka/Lattice/Checks/Chunk08.lean
40a09d251d5f6ce967c50bc0a5d6fe3e0c4d7132ccb8f1b074deb8ff0c19abca  Kourovka/Lattice/Checks/Chunk09.lean
05772fff6a4692a619f82fd9084587da354a36275f53a8b7eaa59a6ab4431f04  Kourovka/Lattice/Checks/Chunk10.lean
c41d2daef9ee4d7a38eca1b1b44edc7f6cdd583f3b5aca06337902d9e238fd53  Kourovka/Lattice/Checks/Chunk11.lean
dfdf0f55e4324ca80ef45de4a29582fb026e0e686b88873b254fad955abab354  Kourovka/Lattice/Checks/Chunk12.lean
8879d69add4c6edf658192206a6de47fb53b956fc4938872466902f60d270758  Kourovka/Lattice/Checks/Chunk13.lean
30ddfd027f4737c5137ab46eb540a208b77609576aaa3cd08a880f5c24f2354c  Kourovka/Lattice/Checks/Chunk14.lean
7efc1634491bdae3c5655783b48b8e42176dcf84c84cc59a73542483cccd4d9c  Kourovka/Lattice/Checks/Chunk15.lean
bafbbe833113d26a7d9873b0973475d81c2c2bc64b79ef7cd389a6cc3163435b  Kourovka/Lattice/Checks/Chunk16.lean
6255d58ec42ff3ca55d57e5ecaf8ef246f2e2c9fe09e8caa749644ca9ff06b8a  Kourovka/Lattice/Checks/Chunk17.lean
846337d0d2897c3352e1c139993ef7d813bb1f5e6d4d3105c566d134bab0445b  Kourovka/Lattice/Checks/Chunk18.lean
c1df7e6e5ffd854c676ef3f8c6fa9b2fcf174b1c58832013e9d5d8c89d3c6809  Kourovka/Lattice/Checks/Chunk19.lean
11e3290165b341b3b050fba1c6e3c69ca0c47c195e1f673ff8514e25075351d1  Kourovka/Lattice/Checks/Chunk20.lean
e0716e84734d374e67d5f5080a6c3ccea78bd1bda97bfcb5931323384c0d4e01  Kourovka/Lattice/Checks/Chunk21.lean
1c61fa4e45de4d8e0f23f0c226285b77612e3f580ca16860b763c798d84a4372  Kourovka/Lattice/Checks/Chunk22.lean
0fa991a73a33fc6b90e65ff044c4627bb3782404677b128e37d6be4119493fe6  Kourovka/Lattice/Checks/Chunk23.lean
e51e38365a52e6a6c8eca6cf3c9db2d6885cea9f4e0aa53e318d757b43206521  Kourovka/Lattice/Checks/Chunk24.lean
64bea5d5d3e9fe8794e61b45394d87bf2750611ef5eb830799aebd46291b4dab  Kourovka/Lattice/Checks/Chunk25.lean
d71dde0777a9126e51454e13adbf5db04020fc50b05acdbb635fab13c61280fc  Kourovka/Lattice/Checks/Chunk26.lean
3edd46bc1f932df6adc70a47c78757bce32fed7f6c32cddd886d4810d4f12a93  Kourovka/Lattice/Checks/Chunk27.lean
02ebadb5adf234ed0cdc4871be65681040ee405a7e92a06c6d07bcdb7b34565f  Kourovka/Lattice/Checks/Chunk28.lean
e3f80378a30700dcf86502da94f3c78aba88650144698eed40f049f06932b088  Kourovka/Lattice/Checks/Chunk29.lean
0f0d03a561e40e7a1e12706da221c8ee101a5fd0db444be31a9e1675d57fe575  Kourovka/Lattice/Checks/Chunk30.lean
02e548e5388801464272360d8026c1da65dee28c2ef23255cb3a17e7ef9dede9  Kourovka/Lattice/EmbeddingBasis.lean
b4f0591f6296cf4a3645f16e1549cac7a2180c4f20020c37d14c0f23a34ea0d4  Kourovka/Lattice/Expressions.lean
e5364a2f46b3d1f7143bc02b71af4f459cf815bc3132f4b53c19c19c62e5df9c  Kourovka/Lattice/Integral.lean
4e9956ac4a30c035f85ea52b6ef84537041b2d89988d8e9a51a5df45810f1369  Kourovka/Lattice/IntegralGeneration.lean
0d47eede2fc8fd4696316c21727846be301ebb9a71b4975555fc3605f6c56a7e  Kourovka/Lattice/IntegralWords.lean
caa687377883ee45b732747ea3cfe0ec1202b9dcb299783edeb9ec1893dca2af  Kourovka/Lattice/NearIdentity.lean
1ceda4ef725b4ce206d5559037cb469595612a211a71c32e7956413fe6d8a91a  Kourovka/Lattice/Precision.lean
2188b4f2578b3c27c3db41aaec2f0a98edacadadcbfce17fefe638fd9b4bfa2d  Kourovka/Lattice/ScaledData.lean
454c025ebc5cfeff5a051fee2fa72b48f527e6324d7077ddce3910ba3fb087a8  Kourovka/Lattice/WeightedFlags.lean
f6af96af75c023fc2ac96d9370449d82272e2289ceddd9c8e000ec37d5258132  Kourovka/Linear/Basis.lean
d42861a1a481584cbef7ed9d0bbf90736917b579fab3c4193775c7d4e806fd1f  Kourovka/Linear/BilinearOps.lean
61efb2e9dfecacae3e62156654692e63a28cbadaf5df4f496ceedc659240ca37  Kourovka/Linear/EndomorphismCoordinates.lean
51233f49d2214b12b5118ce4defcf295a9485fb67cd3a6e1fc85ee796911f3da  Kourovka/Parameters.lean
2ea735d6f7e07512a8b08bb4e29b47904c14560b3fab474036bc224eebffcf48  Kourovka/RawCoefficients.lean
0aba7577cb2fe64771195799050fca6bfabc008bf2b9c5d9c756a4633d541d4b  Kourovka/TableCertificate.lean
d2c466087cce08db85c6c32bba6b3a13572dc6e24f6e8b24804f818de2e6926f  Kourovka/Words.lean
2f7750afb6f82c46d6e1e7e3bc91c2e5abfffdf429928f1cc42aa49004d60906  Kourovka.lean
359b63b790619b4034bf92ab4efec16b1281d772127a859242554eb663e64a25  README.md
ac4f518d9370883c2d30a065798130921d18768e171bc5fbd5ec1ef9be806654  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
1c5db3303c42c6a457e5155ca4eb846a97d70e698d354ca864ab5ee7d545c184  docs/DECLARATION_MAP.md
02ddf5dd0982651ab1a97868c0b9d56614273bb442456de27cdf094c81965623  docs/DEPENDENCIES.md
11b525649263fae3be633b35d3b4d58ec230606e773b7d31c2b745ae2a4889eb  docs/DIRECT_FLAG_RIGIDITY.md
a50b718fc9f3d3af5bb8f7746ecfa67039ba35acc46dc11ebf5daa0f36760fd3  docs/OFFLINE_GUIDE.md
bc97fd630fd3af9ec95ee567328a810aae50e5e04bd7edfc979dc24a2fa24693  docs/REMAINING_OBLIGATIONS.md
29ec1b206cc9a802b1accadf34aeea27019b48bc6c3a206a76cef545af89b7ae  docs/REVIEWER_GUIDE.md
4fe2913bc4df831567ccdb416dd717142347973add94d8cffde0ff2ce709a478  docs/TRUST_REPORT.md
a145466c9d46a7808e1670d2b72cafdd52ef9381c884783d839f845a1e14c3b4  lake-manifest.json
608ad71fdf3eb59e6fdf8e648860060913e9a9ead652ffdc96d3d87fb55b0adb  lakefile.toml
55e97be96000b5e9e290c9e74482e5e317861499a5540353ce845471bded8cea  lean-toolchain
3021bf83587872b1ab19ad3f7b2a1a80529d2e53ee2762ef836491559214a89c  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
cbc1d02a6349c2b2ab009705110a1f08e825224bf5b1be96038f6de5e6075b83  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
95244c91f2534f9d30db36adaa143bca1731989805c85fdfdbc83491c7c5c643  logs/runs/20260919T045135.558392Z/result.json
b31794f71f1a4380cd6e730d9c0a05fefeefa62ebfb5cc9c6a53157ab40d2dc1  logs/runs/20260919T045141.724341Z/001_lean_version.log
dfb48df091ee0aa057f9ebc8344343a95e791b3f50fd50c65306396ba0bf845d  logs/runs/20260919T045141.724341Z/002_existing_pin_plausible.log
0a5bb31b673b8a92c0da31ed6a4b80c87d9135463858b6e0c5a37e1ad75c3670  logs/runs/20260919T045141.724341Z/003_clean_plausible.log
e9ec5f6de44aa6f951463a2b8f25498cbd362c035c9a5c3d70b2084fc7075c09  logs/runs/20260919T045141.724341Z/004_source_shadow_plausible.log
240a2f393c46fb9b48fb0c98d657adb95b19a2746905eb03c5f9780923b66a7b  logs/runs/20260919T045141.724341Z/005_existing_pin_LeanSearchClient.log
53f0ef17a56be22ffea0db36ce7d71aa3431d52f733cf295f67dac88dc4bcf22  logs/runs/20260919T045141.724341Z/006_clean_LeanSearchClient.log
0f4ebc4b16c65f37b4b0d2b95f5390058a652eafa8cea626e466f6747148e652  logs/runs/20260919T045141.724341Z/007_source_shadow_LeanSearchClient.log
3d4c0f4bc7c92a8f47a2af9a380096090f0f0dab5c3348c51c97193428a742bb  logs/runs/20260919T045141.724341Z/008_existing_pin_importGraph.log
0ae9d0607995dbbf82cefd642827f1921c621eeb4bdedea3bba7b249009e6f76  logs/runs/20260919T045141.724341Z/009_clean_importGraph.log
61e8aa60dea669d00650d486ef79a08b237541a27c446318ee914acf01180fb7  logs/runs/20260919T045141.724341Z/010_source_shadow_importGraph.log
11534c4c09d094687671c8e09f8feac1e135bc2cb2d78261860f9d91fce31fd2  logs/runs/20260919T045141.724341Z/011_existing_pin_proofwidgets.log
532982655f68835271d7ed78e91095a2c31bf888ce4750ec9fad90712da3f092  logs/runs/20260919T045141.724341Z/012_clean_proofwidgets.log
31f9f947d49a3b3f584164cdaf74b3b78c4179032da046adc6a0671c4e4c1a1f  logs/runs/20260919T045141.724341Z/013_source_shadow_proofwidgets.log
94dc5c33719f25b8dcad2f135d7dcc41f2b586bb99d5c8f6980ad26484b3da8b  logs/runs/20260919T045141.724341Z/014_existing_pin_aesop.log
dd576e2f7892c6881a4a092d896fd97478cc257bda9d3510ad930db8557f7728  logs/runs/20260919T045141.724341Z/015_clean_aesop.log
48c134e8d54436dc57c3bac6381eb6e7d85e6a25c1c062bb743dadaea65b2725  logs/runs/20260919T045141.724341Z/016_source_shadow_aesop.log
b3d2e48bd67149fb426671aa2fdca0cff3de32e4c0bf2469dd998b9f7b776d88  logs/runs/20260919T045141.724341Z/017_existing_pin_Qq.log
b7ff9a290d1889ed99c20a066bee39a0d0330307192dfb6bfa49e876610fb5fb  logs/runs/20260919T045141.724341Z/018_clean_Qq.log
a977da4247390812c78d126344a19a74b276bb54d427cb621dd2d53986734775  logs/runs/20260919T045141.724341Z/019_source_shadow_Qq.log
d7e0ccefe24e37a61d9471afafc3ecc1a5e045cc0194cc1ea4b4361e9962b131  logs/runs/20260919T045141.724341Z/020_existing_pin_batteries.log
810fe04f46006e9672f417c3b7eeb41bb0446f9d828655e7022b0f8020357d33  logs/runs/20260919T045141.724341Z/021_clean_batteries.log
71001f58f27826a179a9d95bbc9d1522b05509c0d7bf5e3efeeccdbea27d0cc9  logs/runs/20260919T045141.724341Z/022_source_shadow_batteries.log
1cdfbf0aa1462435bdbd1980e7f4e7e9dd128bb520a043cbc09adbf8fdddc966  logs/runs/20260919T045141.724341Z/023_existing_pin_Cli.log
73eac2f9d5dbbc38165190b87fcbfd3e26c1a828125012fa08199cc57163382e  logs/runs/20260919T045141.724341Z/024_clean_Cli.log
93f0a1982f4ee3cbe940b4a019893c98f4571ced4aeb125fa1f91dc2d82ad030  logs/runs/20260919T045141.724341Z/025_source_shadow_Cli.log
53fa3293a778e0f3cf108fb5eac336bd5b84919042d9010199c0b6054ebb4cf8  logs/runs/20260919T045141.724341Z/026_existing_pin_mathlib.log
d39d3e006c4cfad4979e3327c1794a170ccbecb81a1d8d96daa0a6542ab992c0  logs/runs/20260919T045141.724341Z/027_clean_mathlib.log
cf1793baee927329696f998743e49894b5ec5eaedb9fa72d5a24502d6876efcd  logs/runs/20260919T045141.724341Z/028_source_shadow_mathlib.log
40990455c9684cc7a8383d0f1f87842c4fdbbec9726c50582f6d29b89b69fd9c  logs/runs/20260919T045141.724341Z/029_accepted_object_axioms.log
ab67bdd1e10b5860c66a8e34c8269315f4a78ee07b79abd30700487907d4a7b1  logs/runs/20260919T045141.724341Z/030_accepted_object_statements.log
46e64a7dca532e44e4981a97e87eaf824b8b3e6871463461a603b57a772a33ee  logs/runs/20260919T045141.724341Z/031_existing_pin_plausible.log
a71168156a144507c64e36ed326a7121366ed0985621b5f2a87452a4261c98fc  logs/runs/20260919T045141.724341Z/032_clean_plausible.log
4fd656e02e72fe68220a1daf2d3910de9d22940b2d92b074934c4df59da25148  logs/runs/20260919T045141.724341Z/033_source_shadow_plausible.log
3cc3ce728bc3236ad93f3ce92414a6a49cf719f45933d9214e66238aeb25d02a  logs/runs/20260919T045141.724341Z/034_existing_pin_LeanSearchClient.log
856e5023b4129c81dab8aa6c6e81e954bb5cfe26968e3ca8927a925dcce3e2a6  logs/runs/20260919T045141.724341Z/035_clean_LeanSearchClient.log
17e6904c22bf39306f5a8ff1a6ff2cf10113eae439964d353e9ba573e2d8ee64  logs/runs/20260919T045141.724341Z/036_source_shadow_LeanSearchClient.log
d99dc7b947a85fdf48008882ff037e4ac4c55baed88266129ec42245189fc2f9  logs/runs/20260919T045141.724341Z/037_existing_pin_importGraph.log
05c5e3512cd706922752219aec6db9bb5e46da01a54f80787c0cb3320641330e  logs/runs/20260919T045141.724341Z/038_clean_importGraph.log
0e1eafc304ac40e23eda1db7abb53583ebdcf3c9624f44f0a9cbd45990a58ce5  logs/runs/20260919T045141.724341Z/039_source_shadow_importGraph.log
da76248776fe8d28e157b9ebb4971e1a85101b1ee14ef8c396fd553ae42f8f1b  logs/runs/20260919T045141.724341Z/040_existing_pin_proofwidgets.log
1d855fafe3a91977fc8aa9719ffb13dbda029b198bced27a5dc5382a6500983a  logs/runs/20260919T045141.724341Z/041_clean_proofwidgets.log
43a3642c98c51fa02721be1d0be439fcafa27e89ec52108526fc7aa7f14593a3  logs/runs/20260919T045141.724341Z/042_source_shadow_proofwidgets.log
e9c2929a37f0d783398d2bb5607af509e155e84d0fc5c9967235c5c6005b3b80  logs/runs/20260919T045141.724341Z/043_existing_pin_aesop.log
ecc0de899291366d4a46ef4f6a598dab64e6dc4e9233dd85ecc423d73ff7cb12  logs/runs/20260919T045141.724341Z/044_clean_aesop.log
37c432bfc4df795c9d0254d9bce5adfa55f31e3edc11b212f1a5f123e00f1dd1  logs/runs/20260919T045141.724341Z/045_source_shadow_aesop.log
6655bc6f93bc12b79c23109d68e6b7c33ab585db68da3cabc483fe55680d3cbc  logs/runs/20260919T045141.724341Z/046_existing_pin_Qq.log
b32253c113d9e65272287469d4328e83c6b31b7e2bf560754a1a6c4bb25737d5  logs/runs/20260919T045141.724341Z/047_clean_Qq.log
c885e8100685328770c8840ded55459db3bb519d89de206d6b131a818c29310f  logs/runs/20260919T045141.724341Z/048_source_shadow_Qq.log
3bf84b2d78bc60804b20013ce92b8a6462539eea36df5a8e7c2c82ea291d8c33  logs/runs/20260919T045141.724341Z/049_existing_pin_batteries.log
4a427715d5b14761bc92e7542ad637c3dccc73ab4edd2112c24985703249374c  logs/runs/20260919T045141.724341Z/050_clean_batteries.log
032434280ac5c0f9223288982c1cfcf491922c9cf9680f890ea7ec6c9b9cdb63  logs/runs/20260919T045141.724341Z/051_source_shadow_batteries.log
663dc65372b70a07d5feced8c182e49715299043072514e70160eb0a32ccb4cd  logs/runs/20260919T045141.724341Z/052_existing_pin_Cli.log
0b6ee1a3c710d6cc74d29e45fe2f5e75cce2df5467dcf26bfcc88ba1a34a68c3  logs/runs/20260919T045141.724341Z/053_clean_Cli.log
9e90e377569cb43b60abe35b2957da2da0fd999ba3f3aace6aeef284dfd7c919  logs/runs/20260919T045141.724341Z/054_source_shadow_Cli.log
cf816c735f86f3c717a8f6d7ffe6cf5d9736ab069f6edf6a7f3425f45f16a2c4  logs/runs/20260919T045141.724341Z/055_existing_pin_mathlib.log
38700e7a79e7415440b192ca75777b21f2bd0b7346b120c6a8f9b2107958b13b  logs/runs/20260919T045141.724341Z/056_clean_mathlib.log
e4fc37b0f3b807744f8d0a93bea373e1ec13db3d66d0376f34a0a223ba35c540  logs/runs/20260919T045141.724341Z/057_source_shadow_mathlib.log
cbc1d02a6349c2b2ab009705110a1f08e825224bf5b1be96038f6de5e6075b83  logs/runs/20260919T045431.429075Z/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
be8ce32b2df3d2c09ab2a74d8cb108a7a21b7859e9e580266694bc1d315985f6  progress.json
251c9ccd2c6faadc5fb2a3a01db9270efae6aaf40c40323c2004a97db675dbed  reference/README_original_2026-09-17.md
ad202437992b4657de982b01dc57368b2e6fe7cfbcb802bd58bf71b16ced5acb  reference/assignment.txt
5c6421b650bc87a2427a892a39e5522dc44543ca4ac1bd6e9f08d536c044a752  reference/mathlib_lake_manifest_upstream.json
404f0f4d94d5169f0a270b4ca40eec352078ca52bb4c398799a7a7ed71b0daf7  reference/original_SESSION_REPORT_2026-09-17.md
ee578c84fbcbe8c57c5c75923b13f145ccf1527347a0adabd5769b7dfa3cb65a  reference/original_SHA256SUMS_2026-09-17
858ce6f0751f19e9d069e678428d0f7d72d41eb8630130ccb36b4d07edc0acd5  reference/original_docs_DECLARATION_MAP_2026-09-17.md
c7ca28451b8fdfcfe3ec340433ffe5935f33a2534a0a20289d7ad0808fcc65c0  reference/original_docs_DEPENDENCIES_2026-09-17.md
7d903897f066060c82cfb397904c1a5127daf7840b5a1951a682bdee13b55789  reference/original_docs_REMAINING_OBLIGATIONS_2026-09-17.md
062afac1b877ad2aba78b96267c3b826981f1b447307e29d55654e4ff639e91a  reference/original_logs_README_2026-09-17.md
48eff5e789dcad564d84a3fbc5588bbc529cb6bcacfc402fce220d262664566a  reference/original_progress_2026-09-17.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
9fbbd9dc3fa73749cfd2972cc63a4fac840390fb1cafef39e55a88d474b34986  reference/source_inventory.json
aca88c589ad6d756cc2cd0eb94531193040a0ec36fcc5988e31dbf25c1225b9c  reference/source_only_instruction.txt
5e48ba4b2599e26ded88841c76bc3e79d1d035fb98b9e06b5f39219ea1968805  reference/source_only_session.json
a07b2c05cf93b8a8ad6c1bc9b846e2d7f0a2186c6efd2deab8886bb828409b1d  scripts/audit_support.py
7bac6b9c58c56e39bb013b1d63ebaa4be3f8ec43b8a993589568a1979ca2d2e6  scripts/build_serial.py
9d8903352cfd876b863dec50a93e80f9aef346e019f440d6ba48091682574a60  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
c145be6822284b69d4c136a718007cb2e448b65aa154930d6e4d2ec22a24bcac  scripts/source_evidence.py
60050cc779d98165dcfc35d92699e9fffdba87c2676940f4143c9aeeb1c939f4  validation/AxiomAudit.lean
64e36f87dc67b7daf8fd6d881539114c2ca549170683aa787411bed9276b70d9  validation/Statements.lean
