{"backend":"aristotle","engine":"Lean 4 via Harmonic Aristotle","enabled":true,"configured":true,"caps":{"maxInFlight":1,"maxPerDay":8,"breakerThreshold":3,"maxAttempts":2,"maxResultAttempts":3,"maxTaskAgeHours":30},"submissionsLast24h":7,"breaker":{"consecutiveFailures":0,"open":false,"openedAt":null,"trialAt":null,"nextTrialAt":null},"counts":{"eligible":242,"machineChecked":154,"inFlight":0,"notVerified":11},"coverage":{"desks":56,"covered":56,"bare":[],"allCovered":true,"next":{"factId":"depth-dividend-passes-through-as-the-step-times-the-holding","desk":"depth"}},"learning":{"order":["invariant","mandate","theorem","solve","frontier"],"minSettled":10,"measured":["invariant"],"retry":{"carrying":0}},"machineChecked":[{"factId":"pnt","projectId":"77c2fbee-c275-425f-bfab-7ef25134be42","taskId":"bc34f985-0252-420d-b3c6-bc798c696a9e","completedAt":"2026-08-30T22:47:28.188Z","file":"bc34f985-0252-420d-b3c6-bc798c696a9e_aristotle/RequestProject/ChebyshevLimit.lean","bytes":11542,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"basel","projectId":"eafc8e23-8460-4234-94a7-d9b7114c0905","taskId":"865ef240-0e1d-4b71-8ddc-3794715089ad","completedAt":"2026-08-27T22:50:37.479Z","file":"865ef240-0e1d-4b71-8ddc-3794715089ad_aristotle/RequestProject/Basel.lean","bytes":1974,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"bayes","projectId":"c1558b4a-671e-4f4d-a832-ee3331a422ac","taskId":"b3312ee9-15cc-4407-bae8-96203b8cbca1","completedAt":"2026-09-06T23:42:35.633Z","file":"b3312ee9-15cc-4407-bae8-96203b8cbca1_aristotle/RequestProject/Bayes.lean","bytes":1587,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"godel","projectId":"09236bfa-dc2a-4ea6-9e19-808749b49d2c","taskId":"a8551fd0-eddc-4cae-8fa7-6704163e3c6f","completedAt":"2026-09-01T00:49:45.388Z","file":"a8551fd0-eddc-4cae-8fa7-6704163e3c6f_aristotle/RequestProject/Godel.lean","bytes":6247,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"cantor","projectId":"bcbda03f-ef73-4198-867e-f895af1d69ea","taskId":"4ff03cc5-36e0-4d09-a474-cd321ca3ce50","completedAt":"2026-08-31T23:31:21.482Z","file":"4ff03cc5-36e0-4d09-a474-cd321ca3ce50_aristotle/RequestProject/CantorUncountable.lean","bytes":2409,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"golden","projectId":"7bd64500-8805-4680-ba30-8cde0b5403e5","taskId":"652390a0-f9a5-4c53-92f2-4cfb5ebf2848","completedAt":"2026-09-06T01:58:10.125Z","file":"652390a0-f9a5-4c53-92f2-4cfb5ebf2848_aristotle/RequestProject/GoldenRatio.lean","bytes":1373,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"brouwer","projectId":"6a7d2f14-0945-4060-a216-741905f9898c","taskId":"1440f2d8-a79c-4f26-bb4a-7cdc03bb68bd","completedAt":"2026-09-07T23:57:11.486Z","file":"1440f2d8-a79c-4f26-bb4a-7cdc03bb68bd_aristotle/RequestProject/CoffeeCup.lean","bytes":11780,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"taxicab","projectId":"fbfadf50-00d2-4f58-88d0-cff34f8a77b1","taskId":"eb872974-c5c2-46ab-85c3-0039ef5fc3b5","completedAt":"2026-09-05T23:17:38.173Z","file":"eb872974-c5c2-46ab-85c3-0039ef5fc3b5_aristotle/RequestProject/Taxicab.lean","bytes":2353,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"birthday","projectId":"9c0c0099-8677-460a-b991-787e0b68135c","taskId":"e158b4f3-9bbd-4752-92c0-eae960cb60cf","completedAt":"2026-08-31T00:37:24.618Z","file":"e158b4f3-9bbd-4752-92c0-eae960cb60cf_aristotle/RequestProject/Birthday.lean","bytes":2361,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"monty-hall","projectId":"7b123996-29da-4f1e-acf3-3e89fc13069b","taskId":"e08dc6a7-2e5c-4f25-ab12-a4827b658bfc","completedAt":"2026-08-31T22:06:21.375Z","file":"e08dc6a7-2e5c-4f25-ab12-a4827b658bfc_aristotle/RequestProject/MontyHall.lean","bytes":6723,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"point-nine","projectId":"10179863-1b8f-47f9-a90b-578188ffa87e","taskId":"666fbcda-0ef5-4d70-aa4b-beebc76f4c9e","completedAt":"2026-08-31T22:26:21.394Z","file":"666fbcda-0ef5-4d70-aa4b-beebc76f4c9e_aristotle/RequestProject/PointNineRepeating.lean","bytes":1522,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"e-irrational","projectId":"bc771ef2-53f7-4bcd-bbd0-c7d51d589ed4","taskId":"55ad403a-27a3-4951-85a5-fb2354cefe61","completedAt":"2026-09-07T04:39:34.299Z","file":"55ad403a-27a3-4951-85a5-fb2354cefe61_aristotle/RequestProject/EIrrational.lean","bytes":4444,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"burn-monotone","projectId":"adec98a5-ad62-49e5-b589-fb28337420e5","taskId":"81812435-4da5-4120-b3a9-5d80deb3625c","completedAt":"2026-09-01T22:28:47.701Z","file":"81812435-4da5-4120-b3a9-5d80deb3625c_aristotle/RequestProject/Main.lean","bytes":6620,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"buy-then-burn","projectId":"a29aaf89-c7be-4bae-8865-a087dec13711","taskId":"9849ef83-6585-469f-962b-34b8f28fb29c","completedAt":"2026-09-01T22:52:36.594Z","file":"9849ef83-6585-469f-962b-34b8f28fb29c_aristotle/RequestProject/BuyThenBurn.lean","bytes":3064,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"euclid-primes","projectId":"9fc984f4-76ee-47f9-97a6-84d0ee059d59","taskId":"77bbe667-b7ae-4c4a-81eb-669bea5f6ff7","completedAt":"2026-08-28T21:29:38.047Z","file":"77bbe667-b7ae-4c4a-81eb-669bea5f6ff7_aristotle/RequestProject/Euclid.lean","bytes":1141,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"euler-formula","projectId":"4dd77a26-e096-4df4-a8c6-61f8ad0eb19d","taskId":"e2b08ef3-813a-4ef1-9de0-789b3aa0d52f","completedAt":"2026-08-28T22:48:33.655Z","file":"e2b08ef3-813a-4ef1-9de0-789b3aa0d52f_aristotle/RequestProject/EulerFormula.lean","bytes":1031,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"alloc-conserves","projectId":"388c840d-9744-4b89-9ade-bb943565314a","taskId":"f1732eb2-defe-4c11-bf07-949a3161ec4f","completedAt":"2026-08-29T22:20:47.940Z","file":"f1732eb2-defe-4c11-bf07-949a3161ec4f_aristotle/RequestProject/Alloc.lean","bytes":3081,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"index-daily-cap","projectId":"3ad55642-cee7-4c93-bfdf-44ac5fb8995d","taskId":"dca32a7b-505f-43d5-bce5-f47fa8810b1c","completedAt":"2026-09-02T23:33:06.026Z","file":"dca32a7b-505f-43d5-bce5-f47fa8810b1c_aristotle/RequestProject/WindowCap.lean","bytes":3240,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"alloc-burn-floor","projectId":"5775f20c-14b3-42f8-b469-2492f187cc33","taskId":"2f8b9aa9-dd99-43b8-a7cf-4cd50e468108","completedAt":"2026-08-29T22:01:38.190Z","file":"2f8b9aa9-dd99-43b8-a7cf-4cd50e468108_aristotle/RequestProject/Main.lean","bytes":4164,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"alloc-sums-exact","projectId":"9c8afb34-aa8e-47ef-928a-aed1537326be","taskId":"27f5ffcb-e3df-4339-9d54-a97c219d46f4","completedAt":"2026-08-29T21:42:44.836Z","file":"27f5ffcb-e3df-4339-9d54-a97c219d46f4_aristotle/RequestProject/NormalizeWeights.lean","bytes":7078,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"solve-b95a2a.2.1","projectId":"a34354c2-d768-4fd9-8d78-0c7ee03634dc","taskId":"3798f600-5acd-4d33-b36f-00fac911c642","completedAt":"2026-09-11T18:36:22.633Z","file":"3798f600-5acd-4d33-b36f-00fac911c642_aristotle/RequestProject/PowFiveSubSelf.lean","bytes":2942,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"solve-b95a2a.4.1","projectId":"e5a6c9f3-f753-4fd6-8ecb-560caf55b992","taskId":"664f8c99-d099-49aa-b635-f4dbcf91d078","completedAt":"2026-09-12T00:22:59.632Z","file":"664f8c99-d099-49aa-b635-f4dbcf91d078_aristotle/RequestProject/PowFiveSubSelf.lean","bytes":746,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"solve-b95a2a.5.1","projectId":"f8728289-6ded-4fd7-8dbd-2380ee9e15ac","taskId":"98837719-6c83-4fdc-8c3d-2e9049e45b32","completedAt":"2026-09-12T00:57:59.630Z","file":"98837719-6c83-4fdc-8c3d-2e9049e45b32_aristotle/RequestProject/CombinationStep.lean","bytes":2768,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"sqrt2-irrational","projectId":"af410c9a-2283-4fc0-8e85-753708cc0a6c","taskId":"c1c24696-fa46-455b-843d-37bbe77e95b0","completedAt":"2026-08-28T21:57:30.155Z","file":"c1c24696-fa46-455b-843d-37bbe77e95b0_aristotle/RequestProject/Sqrt2Irrational.lean","bytes":2041,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"gaussian-integral","projectId":"dea91d90-b764-490d-959d-3ee9e9c3bd34","taskId":"0c62bf2d-7d31-4cbc-8873-cb8dfc7adcf6","completedAt":"2026-08-28T22:23:09.966Z","file":"0c62bf2d-7d31-4cbc-8873-cb8dfc7adcf6_aristotle/RequestProject/GaussianIntegral.lean","bytes":818,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"harmonic-diverges","projectId":"e752048a-e527-41a3-9b25-99d60de5de48","taskId":"3904407c-7eac-41f6-ba2b-356ca3cf5947","completedAt":"2026-08-27T22:15:37.231Z","file":"3904407c-7eac-41f6-ba2b-356ca3cf5947_aristotle/RequestProject/HarmonicDiverges.lean","bytes":4554,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"no-mint-reachable","projectId":"f0973af2-9fac-4441-84e6-b9b676c94128","taskId":"edc4353a-f5fb-4237-a1cd-ba5230f3bef0","completedAt":"2026-09-01T23:31:52.429Z","file":"edc4353a-f5fb-4237-a1cd-ba5230f3bef0_aristotle/RequestProject/Main.lean","bytes":5768,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"pool-day-caps-hold","projectId":"9e593d18-36d1-47fb-9328-04849a4bd348","taskId":"0f7a1931-60ff-4206-ab1f-37bb6f0c1ce8","completedAt":"2026-09-17T02:23:08.879Z","file":"0f7a1931-60ff-4206-ab1f-37bb6f0c1ce8_aristotle/RequestProject/BountyDesk.lean","bytes":2904,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"desk-size-is-bounded","projectId":"e032ba8a-4907-416c-ab75-2f900e7df1fa","taskId":"1b5fc735-28be-4c00-a399-ec61aeb5104f","completedAt":"2026-09-05T01:33:04.357Z","file":"1b5fc735-28be-4c00-a399-ec61aeb5104f_aristotle/RequestProject/DeskSize.lean","bytes":898,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"edge-floor-only-rises","projectId":"50425bf6-abf5-4999-83d0-5efea73d6e5c","taskId":"c77644dd-b9f4-44ba-b189-b5972d6c6645","completedAt":"2026-09-24T20:29:35.220Z","file":"c77644dd-b9f4-44ba-b189-b5972d6c6645_aristotle/RequestProject/EdgeFloor.lean","bytes":1612,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"frontier-goldbach-5-1","projectId":"bbf3561c-ed6b-4ba3-8e63-1be7866a1a1d","taskId":"70884a10-44e5-4b2d-8746-c18fdbd65a3e","completedAt":"2026-09-27T03:09:50.086Z","file":"70884a10-44e5-4b2d-8746-c18fdbd65a3e_aristotle/RequestProject/Goldbach.lean","bytes":3382,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"mandate-per-trade-cap","projectId":"fccaadd3-9551-4d16-ab26-6dbdb4208795","taskId":"a0ac06a1-cbf9-46f8-b51e-5fe04f774ae7","completedAt":"2026-09-22T03:35:07.713Z","file":"a0ac06a1-cbf9-46f8-b51e-5fe04f774ae7_aristotle/RequestProject/Main.lean","bytes":4059,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"stake-under-every-cap","projectId":"0c166bcd-932c-4923-93d4-ca491ce17394","taskId":"6f78c137-2166-4e00-bf33-ab262f43bbef","completedAt":"2026-10-08T09:03:28.657Z","file":"6f78c137-2166-4e00-bf33-ab262f43bbef_aristotle/RequestProject/KellyStake.lean","bytes":2491,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"supply-non-increasing","projectId":"9e2ad0b5-f271-4cc8-8db6-b87ebde30e97","taskId":"818a493e-5b97-4821-994d-9af2ccab83e2","completedAt":"2026-08-30T21:50:42.800Z","file":"818a493e-5b97-4821-994d-9af2ccab83e2_aristotle/RequestProject/Main.lean","bytes":8730,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"desk-ladder-first-blood","projectId":"6a9665c3-4cff-4721-8c37-3aa57d917aa6","taskId":"d74321fd-73ad-40e5-9151-e699235c0481","completedAt":"2026-09-04T23:07:32.253Z","file":"d74321fd-73ad-40e5-9151-e699235c0481_aristotle/RequestProject/DeskLadder.lean","bytes":2159,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"mining-grid-split-exact","projectId":"a8ad51dc-9e17-4bb0-bcaa-0c84c0962a38","taskId":"da845cf7-9a2c-4591-b6d3-4532cdf617d6","completedAt":"2026-09-14T01:19:04.904Z","file":"da845cf7-9a2c-4591-b6d3-4532cdf617d6_aristotle/RequestProject/MiningGridSplit.lean","bytes":693,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"alloc-drift-favours-burn","projectId":"5fedc020-e04a-47fc-b837-4e82b9e11abe","taskId":"a592d550-9291-4ff1-9fe4-24d731ce5d30","completedAt":"2026-08-29T22:56:43.766Z","file":"a592d550-9291-4ff1-9fe4-24d731ce5d30_aristotle/RequestProject/BurnRounding.lean","bytes":2773,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"index-mint-never-dilutes","projectId":"b09ebdca-ff26-4801-a629-ce476449e53a","taskId":"77f1523b-7a4b-43a0-bb63-b5dffc486141","completedAt":"2026-09-02T22:33:06.213Z","file":"77f1523b-7a4b-43a0-bb63-b5dffc486141_aristotle/RequestProject/MintNeverDilutes.lean","bytes":1537,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"risk-modulation-monotone","projectId":"5bdf2dc5-f91f-4036-92f3-c345b2c8b5ea","taskId":"906bb4ff-357a-4cc3-84d4-4a18b314498a","completedAt":"2026-09-03T22:41:37.404Z","file":"906bb4ff-357a-4cc3-84d4-4a18b314498a_aristotle/RequestProject/Main.lean","bytes":5095,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"learned-veto-only-refuses","projectId":"3c8043bf-29e2-4122-9cad-6734dc8afa11","taskId":"63bb8aea-27ea-42e2-957c-f712cacc3d55","completedAt":"2026-09-10T23:36:58.505Z","file":"63bb8aea-27ea-42e2-957c-f712cacc3d55_aristotle/RequestProject/LearnedVeto.lean","bytes":3458,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"agent-mandate-clauses-hold","projectId":"34659c3a-67d0-4de1-bd1b-16cf55139712","taskId":"bf065f71-11ab-4ce1-8b3e-e3547efc4546","completedAt":"2026-09-20T19:42:10.838Z","file":"bf065f71-11ab-4ce1-8b3e-e3547efc4546_aristotle/RequestProject/Main.lean","bytes":14726,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"desk-nothing-past-the-bond","projectId":"b4e766fd-7ba8-498a-8864-5913266e7aae","taskId":"6a1ce611-54e2-4e19-8174-548ed296cba7","completedAt":"2026-09-17T00:58:08.425Z","file":"6a1ce611-54e2-4e19-8174-548ed296cba7_aristotle/RequestProject/DeskNothingPastTheBond.lean","bytes":1888,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"flywheel-record-only-eases","projectId":"c8be4095-ae48-463c-a4a7-948def656dcf","taskId":"e5f0781c-bee0-4050-b5c8-e38830ad12c6","completedAt":"2026-09-23T03:09:29.535Z","file":"e5f0781c-bee0-4050-b5c8-e38830ad12c6_aristotle/RequestProject/FlywheelRecord.lean","bytes":1622,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"zap-send-covers-the-basket","projectId":"0db95fb2-55ca-47e6-92fb-7ef5566d51e9","taskId":"205bc16f-a2bc-4c99-847c-6fbddb18664b","completedAt":"2026-09-30T05:26:58.520Z","file":"205bc16f-a2bc-4c99-847c-6fbddb18664b_aristotle/RequestProject/ZapSend.lean","bytes":1877,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"agent-badge-never-rounds-up","projectId":"79c405fd-d057-4a3f-b8d9-197b44716ffa","taskId":"ee9d313b-5e6c-4575-91b0-14dd531c0c8c","completedAt":"2026-09-27T04:35:53.647Z","file":"ee9d313b-5e6c-4575-91b0-14dd531c0c8c_aristotle/RequestProject/AgentBadge.lean","bytes":6843,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"depth-no-fill-during-a-halt","projectId":"a5df879a-f72c-4414-ad3f-d9f5cd0977a1","taskId":"503da578-59d4-41d6-b22c-597f43c3d1c6","completedAt":"2026-10-03T04:52:34.524Z","file":"503da578-59d4-41d6-b22c-597f43c3d1c6_aristotle/RequestProject/HaltGate.lean","bytes":5971,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"index-redeem-never-overpays","projectId":"9686cda2-5e8d-4f0a-8bc5-a80262e96f6f","taskId":"a898c193-1e56-46b8-9e16-9ceb1673e58c","completedAt":"2026-09-02T23:08:05.959Z","file":"a898c193-1e56-46b8-9e16-9ceb1673e58c_aristotle/RequestProject/Redeem.lean","bytes":4507,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"wilson-lower-bound-monotone","projectId":"feda696d-aa48-47da-9016-b900cf3b89d6","taskId":"482a21de-af12-483a-9249-4b10324012d4","completedAt":"2026-09-24T03:38:47.622Z","file":"482a21de-af12-483a-9249-4b10324012d4_aristotle/RequestProject/WilsonLowerBound.lean","bytes":5062,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"borrow-cushion-only-tightens","projectId":"a8400dec-df89-474b-aeb8-7ef2ccef2e0b","taskId":"7bcecc03-ddbc-407e-aca8-0b2b46cf0a67","completedAt":"2026-10-10T07:46:18.797Z","file":"7bcecc03-ddbc-407e-aca8-0b2b46cf0a67_aristotle/RequestProject/BorrowCushion.lean","bytes":5260,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"dial-never-leaves-its-bounds","projectId":"d8a8cd7a-c38c-4854-9cb0-0c1347d688c9","taskId":"7e20f411-9769-41d0-9a46-e2468ad64606","completedAt":"2026-10-11T08:20:55.726Z","file":"7e20f411-9769-41d0-9a46-e2468ad64606_aristotle/RequestProject/DialBounds.lean","bytes":948,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"seal-tightening-is-immediate","projectId":"5db6c49c-84fd-4628-9410-f1ad0d5077bf","taskId":"0ef33547-3b2d-4f3a-bbc9-889044f2774a","completedAt":"2026-09-21T03:15:18.096Z","file":"0ef33547-3b2d-4f3a-bbc9-889044f2774a_aristotle/RequestProject/SealTightening.lean","bytes":2740,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"solve-check-needs-two-others","projectId":"edcacc80-31a5-47e9-8112-cffeabbe3db2","taskId":"eb2ff8e2-d726-438a-862b-4b0a94be1caf","completedAt":"2026-09-25T02:37:55.196Z","file":"eb2ff8e2-d726-438a-862b-4b0a94be1caf_aristotle/RequestProject/CheckNeedsTwoOthers.lean","bytes":2666,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"factory-spend-under-every-cap","projectId":"85e3741a-f0ad-467f-a9ed-caee2a32f675","taskId":"3ed0c3ee-5912-4726-b46b-c1f5b3e35cae","completedAt":"2026-09-14T00:48:40.745Z","file":"3ed0c3ee-5912-4726-b46b-c1f5b3e35cae_aristotle/RequestProject/FactorySpend.lean","bytes":2584,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"index-swap-scale-only-shrinks","projectId":"b333cdcf-07fd-41dd-99f0-c8298e2db129","taskId":"120a184d-5592-4e80-aadd-24dc80645d59","completedAt":"2026-09-16T00:46:06.568Z","file":"120a184d-5592-4e80-aadd-24dc80645d59_aristotle/RequestProject/SwapScale.lean","bytes":3166,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"refusals-are-scored-like-buys","projectId":"898ec8b9-78f7-451d-98ac-930c921a1a4c","taskId":"03b9fbcf-af56-43ad-9524-b226de5650f5","completedAt":"2026-10-11T09:41:29.985Z","file":"03b9fbcf-af56-43ad-9524-b226de5650f5_aristotle/RequestProject/RefusalScoring.lean","bytes":1792,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"band-payoff-is-never-one-trade","projectId":"d3973cbf-2b06-4c12-96d9-625fb2b89e5e","taskId":"f8b692d1-eeab-4f60-99b0-b843b5f1b1c7","completedAt":"2026-10-10T06:46:24.504Z","file":"f8b692d1-eeab-4f60-99b0-b843b5f1b1c7_aristotle/RequestProject/BandPayoff.lean","bytes":9396,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"crew-veto-and-proven-exclusive","projectId":"21b85e9a-7dea-4bc9-87d4-47a3fd2114f2","taskId":"9385e128-d5bd-41ab-b5b8-420ece2f3d47","completedAt":"2026-10-02T06:05:42.057Z","file":"9385e128-d5bd-41ab-b5b8-420ece2f3d47_aristotle/RequestProject/CrewVetoProvenExclusive.lean","bytes":985,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"desk-ev-rule-is-the-inequality","projectId":"4cd1c34d-153f-444c-8180-6916408e337a","taskId":"21e70041-1808-45b4-9829-4c497c0dcfa3","completedAt":"2026-09-04T23:32:32.299Z","file":"21e70041-1808-45b4-9829-4c497c0dcfa3_aristotle/RequestProject/DeskEV.lean","bytes":2656,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"mandate-pause-stops-everything","projectId":"0043b8b2-8c98-44f8-bd3a-a147c4a5c120","taskId":"ea94c428-a2af-4c68-9cf6-b83b2f5d5d32","completedAt":"2026-09-29T04:27:26.406Z","file":"ea94c428-a2af-4c68-9cf6-b83b2f5d5d32_aristotle/RequestProject/PauseSeal.lean","bytes":1261,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"scorebook-keeps-every-open-row","projectId":"91edcb38-45b3-44ec-bd41-db1126bdcbfc","taskId":"169b8ee5-755e-4f9c-b3e7-3dd9a9968f5a","completedAt":"2026-09-16T19:12:23.999Z","file":"169b8ee5-755e-4f9c-b3e7-3dd9a9968f5a_aristotle/RequestProject/Scorebook.lean","bytes":6102,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"a-pool-too-thin-is-never-chosen","projectId":"23d785a3-479d-4d85-adf5-90a26983fb27","taskId":"8f05a975-e6e1-4409-8033-e8ccfb7aa096","completedAt":"2026-09-24T02:17:12.654Z","file":"8f05a975-e6e1-4409-8033-e8ccfb7aa096_aristotle/RequestProject/DepthFloor.lean","bytes":4533,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"claim-split-conserves-every-wei","projectId":"0d58d039-5d1d-41b3-b1ea-bf57e04222fa","taskId":"8e201fc7-d07b-495f-95e6-034bee07ee9f","completedAt":"2026-09-13T00:11:04.844Z","file":"8e201fc7-d07b-495f-95e6-034bee07ee9f_aristotle/RequestProject/ClaimSplit.lean","bytes":2346,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"rounding-can-only-reduce-supply","projectId":"6c2f5644-aa75-4d52-ad05-cf128993ef39","taskId":"87665d76-521d-453a-ac6b-f6a65c70adb8","completedAt":"2026-10-10T08:11:19.214Z","file":"87665d76-521d-453a-ac6b-f6a65c70adb8_aristotle/RequestProject/BuybackRemainder.lean","bytes":1775,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"band-refusal-needs-its-own-count","projectId":"9567b538-1547-4c7e-95f0-0b8ec4a2257c","taskId":"27ffe5b6-d95d-4e06-a73e-243b8c13430a","completedAt":"2026-09-15T01:16:01.822Z","file":"27ffe5b6-d95d-4e06-a73e-243b8c13430a_aristotle/RequestProject/BandRefusal.lean","bytes":3014,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"exec-slice-never-exceeds-the-cap","projectId":"7e896ac5-4e5e-4a07-b39a-b39f96ab85fc","taskId":"374992bf-e0ef-411a-9326-51cfbd3961fe","completedAt":"2026-09-21T01:24:49.491Z","file":"374992bf-e0ef-411a-9326-51cfbd3961fe_aristotle/RequestProject/SliceCap.lean","bytes":2216,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"index-self-limit-holds-a-quarter","projectId":"b42d92c4-f72c-4b0f-bc20-9018ed3241ac","taskId":"91cb0a49-72d3-45f9-9830-dc1befb92037","completedAt":"2026-09-23T03:37:55.495Z","file":"91cb0a49-72d3-45f9-9830-dc1befb92037_aristotle/RequestProject/RollingWindow.lean","bytes":2705,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"risk-weights-normalise-to-a-mean","projectId":"967c7459-b83f-4b9d-a776-c165e0a5e606","taskId":"847f885d-3962-4ba7-83c4-42d3984951b3","completedAt":"2026-10-08T07:38:28.287Z","file":"847f885d-3962-4ba7-83c4-42d3984951b3_aristotle/RequestProject/RiskWeights.lean","bytes":4154,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"band-boundaries-never-drop-a-fill","projectId":"90b0dbe4-776b-4977-a118-d608a61be453","taskId":"aa7238ce-56cd-4936-aea0-8a6b7afbcc1f","completedAt":"2026-09-27T21:08:24.817Z","file":"aa7238ce-56cd-4936-aea0-8a6b7afbcc1f_aristotle/RequestProject/Bands.lean","bytes":5161,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"copy-learned-ceiling-never-widens","projectId":"13009b12-bd09-4b5f-bdf3-7fb150ebadc9","taskId":"26e36237-3203-4982-98a0-d295e930c79a","completedAt":"2026-10-08T08:03:29.064Z","file":"26e36237-3203-4982-98a0-d295e930c79a_aristotle/RequestProject/CopyCeiling.lean","bytes":2041,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"early-own-record-only-stands-down","projectId":"dd4fc883-2d52-46c8-a3f1-3415c131e345","taskId":"95605a09-b041-417a-8272-662cdcf1c3c5","completedAt":"2026-09-11T00:16:58.205Z","file":"95605a09-b041-417a-8272-662cdcf1c3c5_aristotle/RequestProject/WilsonMonotone.lean","bytes":7871,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"the-allocator-conserves-every-wei","projectId":"314939e9-2528-43b9-8bbb-fbb55e29b7a9","taskId":"ede8bc7a-56b6-4898-9b91-02ca8134985b","completedAt":"2026-09-23T02:05:58.237Z","file":"ede8bc7a-56b6-4898-9b91-02ca8134985b_aristotle/RequestProject/Allocator.lean","bytes":3012,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"the-burn-floor-cannot-be-breached","projectId":"c2329174-6875-4210-98a5-13b5e665e45c","taskId":"f23d2fe0-c9e8-4149-9411-0b136720eeac","completedAt":"2026-09-29T21:33:49.011Z","file":"f23d2fe0-c9e8-4149-9411-0b136720eeac_aristotle/RequestProject/BurnFloor.lean","bytes":1107,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"borrow-draw-stays-inside-the-limit","projectId":"7cbe9140-fe2c-43b5-bfc8-fa78a22421ba","taskId":"75d2dd0e-c3a1-4f08-b2ef-743b0fc807d0","completedAt":"2026-09-22T01:37:30.256Z","file":"75d2dd0e-c3a1-4f08-b2ef-743b0fc807d0_aristotle/RequestProject/BorrowDrawNeverWorsens.lean","bytes":1502,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"cli-signs-only-the-quote-it-showed","projectId":"d7515ce4-0195-4899-b56f-7210a191fc1d","taskId":"415c216a-8057-4e69-a0de-a9217d237004","completedAt":"2026-09-29T03:34:21.550Z","file":"415c216a-8057-4e69-a0de-a9217d237004_aristotle/RequestProject/QuoteGuard.lean","bytes":9541,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"mining-gas-ceiling-and-wager-scale","projectId":"d7912a64-27fb-4f7a-b64b-0c64bfaa8e86","taskId":"5ff167ab-260b-4333-8502-ef5af401d930","completedAt":"2026-09-21T02:50:18.812Z","file":"5ff167ab-260b-4333-8502-ef5af401d930_aristotle/RequestProject/MiningGasCeilingAndWagerScale.lean","bytes":1879,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"v4-range-ticks-aligned-and-ordered","projectId":"d2926a55-401d-40ea-8211-5d3af51dd04c","taskId":"8a4c6364-f745-4374-8c9e-32e9ebf47fb8","completedAt":"2026-09-03T23:20:37.399Z","file":"8a4c6364-f745-4374-8c9e-32e9ebf47fb8_aristotle/RequestProject/TickRange.lean","bytes":7218,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"world-rank-is-a-count-off-the-desk","projectId":"7a00eddb-7beb-448a-a015-d43d9ea1f81b","taskId":"e7b3291f-c85d-4aeb-9823-c934c1678cab","completedAt":"2026-09-23T20:09:52.987Z","file":"e7b3291f-c85d-4aeb-9823-c934c1678cab_aristotle/RequestProject/DistrictRank.lean","bytes":2991,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"a-failed-read-never-becomes-a-yield","projectId":"113f782b-303a-44f6-9c12-c2d2130491ba","taskId":"2a5f3e4f-821c-432e-af4a-ce917dddb9e6","completedAt":"2026-09-16T01:52:00.151Z","file":"2a5f3e4f-821c-432e-af4a-ce917dddb9e6_aristotle/RequestProject/FailedReadNeverZero.lean","bytes":6151,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"risk-score-is-bounded-weighted-mean","projectId":"85c923f1-96e6-48a6-8038-319d92ad80c3","taskId":"f70aa918-09f8-4257-8667-945d454f8303","completedAt":"2026-09-03T01:08:06.139Z","file":"f70aa918-09f8-4257-8667-945d454f8303_aristotle/RequestProject/Main.lean","bytes":6762,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"usdg-bid-single-sided-with-headroom","projectId":"a773e048-cf42-4abf-804e-ff2ec25312b3","taskId":"2baf071d-8963-4acd-adb8-d1f75a766d1b","completedAt":"2026-09-03T23:48:56.447Z","file":"2baf071d-8963-4acd-adb8-d1f75a766d1b_aristotle/RequestProject/UsdgBid.lean","bytes":5379,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"pairs-bench-needs-ten-reads-each-way","projectId":"335af864-e9b7-47d7-afc5-7dafc3862dd5","taskId":"f46feaad-03dc-483c-9976-89e9083b2f80","completedAt":"2026-10-05T05:53:14.569Z","file":"f46feaad-03dc-483c-9976-89e9083b2f80_aristotle/RequestProject/PairBench.lean","bytes":7885,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"strategy-funds-only-eligible-markets","projectId":"cc7dcf62-ee0e-45cd-9faa-f0f8145af1ff","taskId":"28793382-5cb4-4a8c-beed-429be50ac76d","completedAt":"2026-09-02T01:06:18.800Z","file":"28793382-5cb4-4a8c-beed-429be50ac76d_aristotle/RequestProject/Main.lean","bytes":7807,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"conviction-is-a-bounded-weighted-mean","projectId":"0f49987e-6e8d-4986-9fae-e151ca3f5331","taskId":"3f1748ca-4885-476f-a920-a8dbbaeea764","completedAt":"2026-09-15T00:46:01.860Z","file":"3f1748ca-4885-476f-a920-a8dbbaeea764_aristotle/RequestProject/Conviction.lean","bytes":4734,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"exec-fee-is-a-quarter-percent-at-most","projectId":"e4765676-e6b7-4e2c-bb61-5f5c9cf13e61","taskId":"dc62c27d-f37e-4f8b-aca3-e68aea54c084","completedAt":"2026-09-13T18:47:24.561Z","file":"dc62c27d-f37e-4f8b-aca3-e68aea54c084_aristotle/RequestProject/DeskFee.lean","bytes":1522,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"lean-learned-order-never-drops-a-fact","projectId":"42e31851-5bc9-414a-92e9-2e4e0b4d9870","taskId":"a743aac8-a0ef-4481-829f-ca58cd9ee3be","completedAt":"2026-10-04T05:51:19.753Z","file":"a743aac8-a0ef-4481-829f-ca58cd9ee3be_aristotle/RequestProject/LearnedOrder.lean","bytes":5936,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"mm-move-never-needs-more-than-it-frees","projectId":"4b081dcc-6f44-4a56-8e25-4c8ecca6116f","taskId":"e4c084ff-038a-4da8-a1b3-e66f58d79d58","completedAt":"2026-09-22T20:15:19.128Z","file":"e4c084ff-038a-4da8-a1b3-e66f58d79d58_aristotle/RequestProject/Main.lean","bytes":11086,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"safe-an-unread-balance-is-never-a-zero","projectId":"ba44d948-1869-477a-9a2b-b79b7894448a","taskId":"cf23fb0b-cabd-42c4-b7b2-47e88a52b122","completedAt":"2026-10-11T07:38:54.978Z","file":"cf23fb0b-cabd-42c4-b7b2-47e88a52b122_aristotle/RequestProject/AssayHolding.lean","bytes":2299,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"copy-fee-is-a-share-of-a-win-or-nothing","projectId":"e0b50564-eed2-4675-8f08-c3d1fb4fffd8","taskId":"5ac4bf22-7a28-47b2-ae9b-76e0ed958a3a","completedAt":"2026-09-12T18:40:29.692Z","file":"5ac4bf22-7a28-47b2-ae9b-76e0ed958a3a_aristotle/RequestProject/Fee.lean","bytes":2287,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"earnings-base-rate-bounded-and-monotone","projectId":"16128879-012b-4dc1-bf11-e39eff5097e5","taskId":"7b0e3610-43b1-4671-bd6f-4e3c1d1aec2f","completedAt":"2026-09-30T05:01:43.824Z","file":"7b0e3610-43b1-4671-bd6f-4e3c1d1aec2f_aristotle/RequestProject/EarningsBaseRate.lean","bytes":6578,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"the-entry-floor-never-leaves-its-bounds","projectId":"18823365-7213-4ea3-a94e-dd421b659e25","taskId":"22fd97ef-5106-4162-947a-90f0fe2511a0","completedAt":"2026-09-24T03:13:46.848Z","file":"22fd97ef-5106-4162-947a-90f0fe2511a0_aristotle/RequestProject/EntryFloor.lean","bytes":5046,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"hookrlp-works-only-a-graduated-hookr-key","projectId":"e04e96d1-e7fa-4d36-b3b3-d4aea26b2277","taskId":"4b738ba1-23dd-4b7f-85c7-a10b0a0a8019","completedAt":"2026-10-05T22:45:49.353Z","file":"4b738ba1-23dd-4b7f-85c7-a10b0a0a8019_aristotle/RequestProject/HookrPool.lean","bytes":2807,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"paused-desk-resumes-only-on-proven-skill","projectId":"13645a9f-f2f9-4511-a34a-494619f6e323","taskId":"ba517aa0-ee0f-4679-9565-de3f70233ce7","completedAt":"2026-09-11T00:41:58.285Z","file":"ba517aa0-ee0f-4679-9565-de3f70233ce7_aristotle/RequestProject/Main.lean","bytes":5507,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"brain-tape-fires-only-on-a-dip-or-the-cap","projectId":"2731bf87-a254-40b4-a722-859b19d4e6ee","taskId":"e23d5bfc-7219-4fad-a368-d6e91952050a","completedAt":"2026-10-09T07:45:29.112Z","file":"e23d5bfc-7219-4fad-a368-d6e91952050a_aristotle/RequestProject/PurseTape.lean","bytes":3836,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"deposit-fee-never-charges-a-desk-delivery","projectId":"38f27ff2-e146-4658-b862-ac4d4b04b294","taskId":"018d2e3a-f1aa-475e-807c-e573f0e79361","completedAt":"2026-09-16T01:24:05.425Z","file":"018d2e3a-f1aa-475e-807c-e573f0e79361_aristotle/RequestProject/DepositFee.lean","bytes":2440,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"public-split-is-three-legs-of-one-hundred","projectId":"ed57a94a-3ba6-4ad3-bc20-bc9a05de2024","taskId":"2936830b-5ee7-438e-8c3c-08d72e873d27","completedAt":"2026-09-15T01:46:01.995Z","file":"2936830b-5ee7-438e-8c3c-08d72e873d27_aristotle/RequestProject/PublicSplit.lean","bytes":2554,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"what-truncation-strands-is-swept-not-lost","projectId":"777c3ac3-444f-4fbe-8d1c-aec3195c8cc9","taskId":"d94ef8f5-de8d-4c5e-8792-bfbb3d62104a","completedAt":"2026-09-27T04:04:50.057Z","file":"d94ef8f5-de8d-4c5e-8792-bfbb3d62104a_aristotle/RequestProject/ClaimRound.lean","bytes":2117,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"an-unmeasured-incumbent-is-never-abandoned","projectId":"e3cc2361-224f-4e3e-8684-f6b2621db2fb","taskId":"5d9d0772-2d56-4503-935b-24e42c7b5769","completedAt":"2026-10-11T07:50:53.951Z","file":"5d9d0772-2d56-4503-935b-24e42c7b5769_aristotle/RequestProject/UnmeasuredIncumbent.lean","bytes":2822,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"flywheel-spend-never-exceeds-the-cycle-cap","projectId":"571d4c64-87d4-4e04-8315-c5c23e9ec0b8","taskId":"2e1a7c7e-63f5-409c-8bd3-eb945a77aa4c","completedAt":"2026-09-15T19:01:15.844Z","file":"2e1a7c7e-63f5-409c-8bd3-eb945a77aa4c_aristotle/RequestProject/Flywheel.lean","bytes":3183,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"borrow-draw-never-passes-the-market-ceiling","projectId":"086e5618-f727-4f8b-80b7-e7781f2ce5a7","taskId":"cd66b253-9aa7-4ada-8332-c016df7e7f85","completedAt":"2026-09-28T04:27:35.025Z","file":"cd66b253-9aa7-4ada-8332-c016df7e7f85_aristotle/RequestProject/BorrowCeiling.lean","bytes":1263,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"fund-a-gap-to-nav-is-stated-only-on-one-day","projectId":"f9e4470f-e832-45d4-ad9f-a9eca9f07eee","taskId":"24a844ca-38b0-4e00-a95d-9e2d696f18af","completedAt":"2026-10-09T09:06:45.473Z","file":"24a844ca-38b0-4e00-a95d-9e2d696f18af_aristotle/RequestProject/FundGap.lean","bytes":13183,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"rail-a-session-opens-only-under-its-own-key","projectId":"8dd9cff1-4ac2-4fc6-9f25-08a367b52001","taskId":"98902e46-b9ef-4317-b82b-391c7281473b","completedAt":"2026-10-11T08:56:23.653Z","file":"98902e46-b9ef-4317-b82b-391c7281473b_aristotle/RequestProject/RailSeal.lean","bytes":7314,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"robinhood-places-only-the-order-it-proposed","projectId":"92756eb2-ec68-4f67-806f-436dbaaf0b76","taskId":"49055ce0-8055-439a-8d58-6414cc8944c5","completedAt":"2026-09-30T03:56:43.339Z","file":"49055ce0-8055-439a-8d58-6414cc8944c5_aristotle/RequestProject/OrderGuard.lean","bytes":12613,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"seal-paused-signs-nothing-and-the-cap-holds","projectId":"4d890d47-2fac-4743-8473-7d23d4dd64f2","taskId":"f666d1f9-4ee7-4429-a042-05ad0ed3b02b","completedAt":"2026-09-14T19:03:35.522Z","file":"f666d1f9-4ee7-4429-a042-05ad0ed3b02b_aristotle/RequestProject/Seal.lean","bytes":3398,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"the-router-never-moves-for-a-rounding-error","projectId":"fc420253-6dec-43a3-b30f-e255f7987f65","taskId":"25039604-0b93-4516-913d-22634c376751","completedAt":"2026-10-01T05:20:46.367Z","file":"25039604-0b93-4516-913d-22634c376751_aristotle/RequestProject/Router.lean","bytes":3293,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"a-flapping-alert-waits-longer-and-never-less","projectId":"b9dbf39d-70aa-4025-91c4-9c9a6b9dfc08","taskId":"a3e230fd-7d82-47d5-a7dc-25badc971aa6","completedAt":"2026-10-04T22:42:11.215Z","file":"a3e230fd-7d82-47d5-a7dc-25badc971aa6_aristotle/RequestProject/AlertScale.lean","bytes":2616,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"a-perp-dial-scales-a-read-and-never-turns-it","projectId":"59a02a8c-83c3-4fef-9360-db6b006e84f5","taskId":"dbde5b2f-8739-45cd-b3cc-1e8bd319bd67","completedAt":"2026-10-08T07:03:27.913Z","file":"dbde5b2f-8739-45cd-b3cc-1e8bd319bd67_aristotle/RequestProject/PerpDial.lean","bytes":3497,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"a-round-can-never-promise-more-than-it-holds","projectId":"f680e710-ea10-421d-80be-2a76751c3724","taskId":"53d4c961-0fa7-4c5f-9e72-d0c15720edd8","completedAt":"2026-09-20T00:57:54.831Z","file":"53d4c961-0fa7-4c5f-9e72-d0c15720edd8_aristotle/RequestProject/ClaimRound.lean","bytes":1388,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"blend-stays-between-the-market-and-its-parts","projectId":"3caedfc0-8a13-4f94-a9e7-314bb3b29efb","taskId":"9340a789-777b-4df0-b045-1fd788a4cfcd","completedAt":"2026-09-17T01:58:08.488Z","file":"9340a789-777b-4df0-b045-1fd788a4cfcd_aristotle/RequestProject/Blend.lean","bytes":3988,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"rail-forwards-only-the-equity-order-it-filed","projectId":"4f724a03-91a8-4ace-9ccb-3ed437e38e03","taskId":"a277e25f-5f98-4d51-94ed-599640ece4d8","completedAt":"2026-10-01T21:56:25.403Z","file":"a277e25f-5f98-4d51-94ed-599640ece4d8_aristotle/RequestProject/Rail.lean","bytes":12107,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"world-milestone-needs-the-desk-not-the-world","projectId":"377e1862-4a40-4ae7-94fb-e369ce59d981","taskId":"81ccf99e-7783-42b3-afc2-1b39fec1f96b","completedAt":"2026-10-10T10:11:20.268Z","file":"81ccf99e-7783-42b3-afc2-1b39fec1f96b_aristotle/RequestProject/MilestoneNeedsDesk.lean","bytes":3144,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"bond-a-quote-never-hands-out-a-free-arbitrage","projectId":"2725b56b-58a8-4868-b088-88984784e14d","taskId":"22e5d0f4-baf3-4ff5-a9b8-87a31334b4f8","completedAt":"2026-09-18T02:01:49.012Z","file":"22e5d0f4-baf3-4ff5-a9b8-87a31334b4f8_aristotle/RequestProject/QuoteSpread.lean","bytes":672,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"dca-tranche-bounded-and-budget-never-exceeded","projectId":"31a8e73d-7bc0-42a4-b185-0cccc82b2f81","taskId":"d72ff966-e2c4-4e3b-b277-041a97d4218b","completedAt":"2026-09-14T00:23:40.697Z","file":"d72ff966-e2c4-4e3b-b277-041a97d4218b_aristotle/RequestProject/DCA.lean","bytes":7154,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"index-leg-window-sizes-inside-the-same-bounds","projectId":"9197db71-ed9e-46ae-8c8c-25139ddb9802","taskId":"8a2cd81d-d418-4ce9-8a51-d0753033d2a2","completedAt":"2026-10-10T09:11:19.537Z","file":"8a2cd81d-d418-4ce9-8a51-d0753033d2a2_aristotle/RequestProject/LegScale.lean","bytes":3064,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"registry-a-filing-is-graded-by-the-move-alone","projectId":"75bc6bd9-131d-4244-bbb5-fa239c19ae31","taskId":"d21468b1-9fa8-43b2-a3cc-2d9287dd9419","completedAt":"2026-09-30T21:46:08.475Z","file":"d21468b1-9fa8-43b2-a3cc-2d9287dd9419_aristotle/RequestProject/FilingGrade.lean","bytes":2957,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"world-purse-pays-a-fraction-under-the-day-cap","projectId":"c2f2d8d3-b2ed-4cfc-9ebf-26e49ac78cab","taskId":"b106e63d-a32d-46b6-b99c-a727188d3940","completedAt":"2026-10-01T04:03:57.949Z","file":"b106e63d-a32d-46b6-b99c-a727188d3940_aristotle/RequestProject/Purse.lean","bytes":4451,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"exec-impact-scale-bounded-and-never-past-the-cap","projectId":"d94219d9-d1a9-42f6-9b39-4cb3fca7068b","taskId":"34c7677b-12a9-4236-8e21-22e6a8409741","completedAt":"2026-10-08T08:33:28.433Z","file":"34c7677b-12a9-4236-8e21-22e6a8409741_aristotle/RequestProject/ImpactScale.lean","bytes":2498,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"band-refusal-is-never-cheaper-than-the-band-paying","projectId":"fd423022-580d-41f6-965c-19eb16fd235e","taskId":"702985b8-0975-452a-b63a-df9c962f0e7e","completedAt":"2026-09-21T19:50:36.489Z","file":"702985b8-0975-452a-b63a-df9c962f0e7e_aristotle/RequestProject/BandRule.lean","bytes":5201,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"copy-size-never-exceeds-the-bankroll-or-the-wallet","projectId":"53f90f63-fc14-4a09-bee2-f1b873cd5236","taskId":"e7c35013-5c35-4765-a1a0-eeff1cc4e73f","completedAt":"2026-09-19T19:37:20.246Z","file":"e7c35013-5c35-4765-a1a0-eeff1cc4e73f_aristotle/RequestProject/RiderSlice.lean","bytes":1794,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"depth-a-buyer-pays-at-least-what-a-leaver-receives","projectId":"3deca813-9f9e-4be1-8ef8-cbdbe61f3950","taskId":"2fe5a339-43be-49b5-8a7f-2b144e230e67","completedAt":"2026-09-25T20:39:59.443Z","file":"2fe5a339-43be-49b5-8a7f-2b144e230e67_aristotle/RequestProject/BookShares.lean","bytes":7460,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"mm-hook-refused-exactly-when-it-can-touch-the-exit","projectId":"d030508f-ccf2-4ccd-adc5-46042c41bf2d","taskId":"d798e521-1471-4cd0-9ff9-ccc2ec40a580","completedAt":"2026-09-29T05:22:03.725Z","file":"d798e521-1471-4cd0-9ff9-ccc2ec40a580_aristotle/RequestProject/HookAdmission.lean","bytes":3415,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"launch-default-rules-move-only-on-proven-separation","projectId":"737b4c30-dc4b-4ca2-8ef4-2718b22bcffb","taskId":"65f990fb-fb4c-4e4c-bb75-3acf52e5abe3","completedAt":"2026-10-03T22:31:40.915Z","file":"65f990fb-fb4c-4e4c-bb75-3acf52e5abe3_aristotle/RequestProject/LaunchDefault.lean","bytes":4152,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"robinhood-slip-is-the-signed-distance-from-the-print","projectId":"f08c40d7-6daf-47ca-afbd-9fbd753e406b","taskId":"25e3226b-1de4-4a3a-80a9-db6c5c960051","completedAt":"2026-10-10T08:46:19.460Z","file":"25e3226b-1de4-4a3a-80a9-db6c5c960051_aristotle/RequestProject/Slip.lean","bytes":10448,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"solsniper-the-buy-refuses-every-seat-behind-its-room","projectId":"3c62158a-f644-404c-ae9a-2fec1829acf7","taskId":"d4a9cf08-4f90-45a3-8db7-3945f7137cf5","completedAt":"2026-10-08T06:33:27.713Z","file":"d4a9cf08-4f90-45a3-8db7-3945f7137cf5_aristotle/RequestProject/SniperSeat.lean","bytes":2879,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"solve-calibration-moves-halfway-and-only-on-evidence","projectId":"47a193ef-563f-4844-8aa1-d4518747e381","taskId":"2b558560-7296-4a60-aced-15cd387d0631","completedAt":"2026-10-08T09:38:28.587Z","file":"2b558560-7296-4a60-aced-15cd387d0631_aristotle/RequestProject/Calibration.lean","bytes":4934,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"stock-token-multiplier-never-falls-except-on-a-split","projectId":"6f92c7b2-8990-4f3b-900c-6f834171dbe4","taskId":"1674d26c-c1af-4c72-a1c1-91f40352a360","completedAt":"2026-09-19T03:04:23.672Z","file":"1674d26c-c1af-4c72-a1c1-91f40352a360_aristotle/RequestProject/Main.lean","bytes":10906,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"the-entry-floor-moves-only-on-what-the-record-proved","projectId":"a1a9ffe0-86a9-4cda-8adc-02b683e6be57","taskId":"bc2366d0-6a26-4aa6-9c09-5495f4168631","completedAt":"2026-10-01T05:53:44.591Z","file":"bc2366d0-6a26-4aa6-9c09-5495f4168631_aristotle/RequestProject/EntryFloor.lean","bytes":8487,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"soldesk-a-buy-breaks-even-exactly-at-the-curves-own-odds","projectId":"5e96da66-88d5-481b-b4af-97ab4058e998","taskId":"0a66de84-4f88-48aa-8840-e085b673d68b","completedAt":"2026-10-08T06:08:27.650Z","file":"0a66de84-4f88-48aa-8840-e085b673d68b_aristotle/RequestProject/PumpFun.lean","bytes":3583,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"equityoracle-a-halted-or-unflagged-token-never-reads-open","projectId":"b97af13d-325d-44cc-960e-0d35afa4cf81","taskId":"e0e8ab44-17b9-4e2d-b260-c3b63f962db6","completedAt":"2026-10-02T05:35:42.069Z","file":"e0e8ab44-17b9-4e2d-b260-c3b63f962db6_aristotle/RequestProject/EquityOracle.lean","bytes":3463,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"chart-a-proof-is-settled-only-by-bars-that-closed-after-it","projectId":"12462d0c-0f44-473f-bdb6-257000608b9c","taskId":"65c4e441-0500-44ae-98e2-5949157f733f","completedAt":"2026-09-19T02:28:50.624Z","file":"65c4e441-0500-44ae-98e2-5949157f733f_aristotle/RequestProject/ChartSettledBars.lean","bytes":1826,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"husd-the-maximum-is-the-chain-figure-and-the-scale-is-exact","projectId":"ac5081db-72f2-4f34-b135-a041e08663b5","taskId":"e6ef3f01-a216-4941-b1e1-db2f23351333","completedAt":"2026-09-18T00:56:47.974Z","file":"e6ef3f01-a216-4941-b1e1-db2f23351333_aristotle/RequestProject/HusdScale.lean","bytes":1192,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"a-timeline-subject-weight-is-never-zero-and-one-until-earned","projectId":"d444a1ac-0504-4dea-9c50-f2d6ba428c6d","taskId":"eb08a1ed-5d00-4491-9c66-eb32e2ea106b","completedAt":"2026-10-04T05:15:31.074Z","file":"eb08a1ed-5d00-4491-9c66-eb32e2ea106b_aristotle/RequestProject/TimelineWeight.lean","bytes":3082,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"payout-the-tally-conserves-and-only-counts-the-account-named","projectId":"435a9989-3dec-4fbe-8209-37c3f71d6a6f","taskId":"15b679ba-a9b7-4407-85b8-79be9451a198","completedAt":"2026-09-25T03:38:23.337Z","file":"15b679ba-a9b7-4407-85b8-79be9451a198_aristotle/RequestProject/UnconvertedFees.lean","bytes":864,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"brain-caps-stay-inside-their-bounds-and-the-cycle-fee-is-small","projectId":"fb080083-fda5-490f-a559-775ae683885a","taskId":"292c1c94-5416-4651-a0bd-4968569b0db1","completedAt":"2026-09-26T04:24:45.459Z","file":"292c1c94-5416-4651-a0bd-4968569b0db1_aristotle/RequestProject/CapsAndFee.lean","bytes":1291,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"defidoor-a-build-the-door-hands-out-passes-the-terminals-guard","projectId":"14f20f83-10f2-48a5-8a6c-3aabe7627711","taskId":"c423acee-715c-4f9e-978f-bede7d66b53a","completedAt":"2026-10-02T04:18:19.937Z","file":"c423acee-715c-4f9e-978f-bede7d66b53a_aristotle/RequestProject/DefiDoor.lean","bytes":5188,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"registry-a-seal-opens-only-on-its-own-fields-and-shut-is-wrong","projectId":"4fda7edc-775a-4f0b-814b-67c388dc7f5b","taskId":"a19f4312-1da6-4353-a5d1-806e0b6461ed","completedAt":"2026-10-10T09:46:20.033Z","file":"a19f4312-1da6-4353-a5d1-806e0b6461ed_aristotle/RequestProject/SealedFiling.lean","bytes":14839,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"payout-held-fees-never-exceed-the-credits-and-never-go-negative","projectId":"e1788c45-3933-41f6-a3b8-f494642859b8","taskId":"588e4661-aab1-4c55-baa6-d009970c3cb4","completedAt":"2026-09-17T19:11:03.025Z","file":"588e4661-aab1-4c55-baa6-d009970c3cb4_aristotle/RequestProject/HeldFees.lean","bytes":4195,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"safe-a-wash-cycle-is-a-ring-sell-and-a-ring-buy-each-trade-once","projectId":"d986ab17-aeab-419e-abc9-55687c851dd8","taskId":"3d8ef826-54b1-44a6-be73-4a9667119684","completedAt":"2026-10-11T07:13:54.983Z","file":"3d8ef826-54b1-44a6-be73-4a9667119684_aristotle/RequestProject/WashCycle.lean","bytes":6957,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"chart-the-check-agrees-only-when-both-windows-take-the-same-side","projectId":"d96a5e15-ce6a-4ff0-b7d0-68512cd9de0f","taskId":"86384c62-9c14-4232-9dc5-feeece2ed470","completedAt":"2026-10-09T10:01:45.507Z","file":"86384c62-9c14-4232-9dc5-feeece2ed470_aristotle/RequestProject/StanceAgreement.lean","bytes":1498,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"payout-a-missing-price-is-never-a-zero-and-milestones-only-climb","projectId":"dc01dda8-3681-4817-86ee-37782c02eea7","taskId":"3386dc2c-1064-4b53-a5b5-24b4c614ca06","completedAt":"2026-10-09T06:18:43.292Z","file":"3386dc2c-1064-4b53-a5b5-24b4c614ca06_aristotle/RequestProject/Milestone.lean","bytes":1402,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"brain-every-split-sums-to-ten-thousand-and-the-trade-leg-is-capped","projectId":"89ef21a3-5027-4579-9505-19beb4ae99e5","taskId":"c56d5bcd-cb8a-45c3-8097-7d367fa1c6a4","completedAt":"2026-09-19T00:58:50.319Z","file":"c56d5bcd-cb8a-45c3-8097-7d367fa1c6a4_aristotle/RequestProject/Split.lean","bytes":3955,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"equityoracle-a-quote-older-than-its-session-allows-never-reads-fresh","projectId":"60fb0bc0-151a-466c-be6e-660c4404ab57","taskId":"8a376adb-a948-4bbb-aebc-3e88bb558d87","completedAt":"2026-10-11T09:26:23.891Z","file":"8a376adb-a948-4bbb-aebc-3e88bb558d87_aristotle/RequestProject/QuoteFreshness.lean","bytes":2827,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"haltwatch-gated-only-if-in-the-swap-path-paid-and-carrying-the-oracle","projectId":"f1c2c9cb-d05b-4536-b91c-624fffb3267c","taskId":"1f1b55e9-41fe-40bd-b608-ac0606a980a8","completedAt":"2026-10-05T22:26:00.428Z","file":"1f1b55e9-41fe-40bd-b608-ac0606a980a8_aristotle/RequestProject/HaltwatchGated.lean","bytes":3063,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"oracle-settlement-conserves-the-pot-and-the-house-keeps-only-the-dust","projectId":"de3b1d02-0ed4-44c3-b009-5a2828f12b5c","taskId":"32a0aaca-080b-475f-9603-c210b8504f58","completedAt":"2026-09-28T03:13:16.483Z","file":"32a0aaca-080b-475f-9603-c210b8504f58_aristotle/RequestProject/Settlement.lean","bytes":7431,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"compute-an-inference-job-goes-only-to-a-machine-that-declared-the-kind","projectId":"a8444717-a8ed-4373-961f-dd0c6e8c1ff2","taskId":"f14bc371-f1b4-4e21-9a5f-897fda060ec9","completedAt":"2026-10-02T22:09:16.551Z","file":"f14bc371-f1b4-4e21-9a5f-897fda060ec9_aristotle/RequestProject/Routing.lean","bytes":2808,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"weekendmark-the-mark-is-dollars-over-tokens-between-the-pools-it-keeps","projectId":"4b65aea7-32f3-47f7-9529-376c09c236d2","taskId":"22bdfdf1-ebe0-432d-8871-140acc7049e7","completedAt":"2026-10-05T23:15:49.746Z","file":"22bdfdf1-ebe0-432d-8871-140acc7049e7_aristotle/RequestProject/WeekendMark.lean","bytes":8734,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"bond-shares-round-against-the-buyer-and-liability-is-netted-never-negative","projectId":"402d654d-bbbc-476d-a3f2-fb2d6fef6bf6","taskId":"17fb62d1-2672-4955-9017-559f72b0cda1","completedAt":"2026-09-25T04:08:23.541Z","file":"17fb62d1-2672-4955-9017-559f72b0cda1_aristotle/RequestProject/BondShares.lean","bytes":1252,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"bond-caps-scale-with-the-balance-and-solvency-refuses-what-cannot-be-covered","projectId":"5052f4e4-3cb8-4005-ac83-a39478d831a4","taskId":"29ac3923-5577-44df-95c6-f3de4096504d","completedAt":"2026-10-09T06:45:28.649Z","file":"29ac3923-5577-44df-95c6-f3de4096504d_aristotle/RequestProject/StakeCap.lean","bytes":891,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"credit-an-advance-never-exceeds-the-ltv-the-cap-or-its-share-of-the-expectation","projectId":"3248c574-8a66-47e1-bf5a-25cd75fe26a9","taskId":"f626644d-e9ce-49b0-9f30-1eb6c7f7ef9a","completedAt":"2026-09-18T19:15:03.497Z","file":"f626644d-e9ce-49b0-9f30-1eb6c7f7ef9a_aristotle/RequestProject/LoanAdvance.lean","bytes":1863,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"oracle-every-stake-is-paid-under-exactly-one-outcome-and-a-void-returns-them-all","projectId":"069a8889-368c-402b-a452-84d8ef8457d6","taskId":"f42340fe-8639-47f0-9096-1ee0947354a0","completedAt":"2026-10-10T06:55:24.654Z","file":"f42340fe-8639-47f0-9096-1ee0947354a0_aristotle/RequestProject/Settlement.lean","bytes":3582,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"compute-a-job-is-never-priced-under-its-floor-and-a-spec-hashes-only-what-it-uses","projectId":"8761c827-3d33-476c-9d61-5c6e6da8d76e","taskId":"f4f66435-7f52-4802-a582-d0c7fead1c14","completedAt":"2026-09-18T02:27:19.520Z","file":"f4f66435-7f52-4802-a582-d0c7fead1c14_aristotle/RequestProject/JobPrice.lean","bytes":845,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"tail-cover-scale-is-one-until-thirty-days-and-stays-between-half-and-five-quarters","projectId":"bf107402-e542-43d5-b674-b8d8bbf0ac1e","taskId":"c46f0b6e-73a8-49c8-bff2-f1573deffbbc","completedAt":"2026-10-05T05:32:20.697Z","file":"c46f0b6e-73a8-49c8-bff2-f1573deffbbc_aristotle/RequestProject/TailCoverScale.lean","bytes":3341,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"chart-the-refuting-level-is-always-on-the-far-side-of-price-and-the-sheet-fits-a-post","projectId":"efaf8922-b53d-46fe-b3d8-178349f14de8","taskId":"a8784643-945d-40de-8e65-cbe6881d2073","completedAt":"2026-09-26T20:55:51.112Z","file":"a8784643-945d-40de-8e65-cbe6881d2073_aristotle/RequestProject/RefutingLevel.lean","bytes":3815,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"door-the-default-slippage-moves-only-on-thirty-graded-fills-and-stays-between-twenty-five-and-a-hundred","projectId":"2b61d2e5-ed5a-44e3-b952-f008e1f303f1","taskId":"5b756b39-1641-4e91-9872-d39eec7b0c72","completedAt":"2026-10-05T06:53:14.801Z","file":"5b756b39-1641-4e91-9872-d39eec7b0c72_aristotle/RequestProject/DefaultSlippage.lean","bytes":11406,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}},{"factId":"compute-a-completion-is-bounded-and-priced-at-its-floor-or-above","projectId":"bd586756-d58d-4be1-b12f-39ea707b014b","taskId":"10bb2e49-82f5-498e-8945-042b94eab0d4","completedAt":"2026-10-11T10:26:14.911Z","file":"10bb2e49-82f5-498e-8945-042b94eab0d4_aristotle/RequestProject/Completion.lean","bytes":8316,"toolchain":{"lean":"leanprover/lean4:v4.28.0","mathlib":"8f9d9cff6bd728b17a24e163c9402775d9e6a365"}}],"inFlight":[],"notVerified":[{"factId":"apery","status":"queued","attempts":2},{"factId":"gauss-sum","status":"queued","attempts":2},{"factId":"four-color","status":"queued","attempts":1},{"factId":"euler-identity","status":"queued","attempts":2},{"factId":"mandate-daily-cap","status":"queued","attempts":2},{"factId":"frontier-erdos-straus-4-1","status":"queued","attempts":2},{"factId":"exec-slices-cover-and-bound","status":"queued","attempts":2},{"factId":"exec-slices-cover-the-order","status":"queued","attempts":2},{"factId":"dca-dislocation-dial-bounded-and-caps-stand","status":"queued","attempts":2},{"factId":"chart-a-fitted-window-holds-every-indicator-it-quotes","status":"queued","attempts":2},{"factId":"equityoracle-a-gated-venue-fills-only-on-a-fresh-open-row-it-can-read","status":"queued","attempts":2}],"updatedAt":"2026-10-11T10:26:14.925Z","verified":["pnt","basel","bayes","godel","cantor","golden","brouwer","taxicab","birthday","monty-hall","point-nine","e-irrational","burn-monotone","buy-then-burn","euclid-primes","euler-formula","alloc-conserves","index-daily-cap","alloc-burn-floor","alloc-sums-exact","solve-b95a2a.2.1","solve-b95a2a.4.1","solve-b95a2a.5.1","sqrt2-irrational","gaussian-integral","harmonic-diverges","no-mint-reachable","pool-day-caps-hold","desk-size-is-bounded","edge-floor-only-rises","frontier-goldbach-5-1","mandate-per-trade-cap","stake-under-every-cap","supply-non-increasing","desk-ladder-first-blood","mining-grid-split-exact","alloc-drift-favours-burn","index-mint-never-dilutes","risk-modulation-monotone","learned-veto-only-refuses","agent-mandate-clauses-hold","desk-nothing-past-the-bond","flywheel-record-only-eases","zap-send-covers-the-basket","agent-badge-never-rounds-up","depth-no-fill-during-a-halt","index-redeem-never-overpays","wilson-lower-bound-monotone","borrow-cushion-only-tightens","dial-never-leaves-its-bounds","seal-tightening-is-immediate","solve-check-needs-two-others","factory-spend-under-every-cap","index-swap-scale-only-shrinks","refusals-are-scored-like-buys","band-payoff-is-never-one-trade","crew-veto-and-proven-exclusive","desk-ev-rule-is-the-inequality","mandate-pause-stops-everything","scorebook-keeps-every-open-row","a-pool-too-thin-is-never-chosen","claim-split-conserves-every-wei","rounding-can-only-reduce-supply","band-refusal-needs-its-own-count","exec-slice-never-exceeds-the-cap","index-self-limit-holds-a-quarter","risk-weights-normalise-to-a-mean","band-boundaries-never-drop-a-fill","copy-learned-ceiling-never-widens","early-own-record-only-stands-down","the-allocator-conserves-every-wei","the-burn-floor-cannot-be-breached","borrow-draw-stays-inside-the-limit","cli-signs-only-the-quote-it-showed","mining-gas-ceiling-and-wager-scale","v4-range-ticks-aligned-and-ordered","world-rank-is-a-count-off-the-desk","a-failed-read-never-becomes-a-yield","risk-score-is-bounded-weighted-mean","usdg-bid-single-sided-with-headroom","pairs-bench-needs-ten-reads-each-way","strategy-funds-only-eligible-markets","conviction-is-a-bounded-weighted-mean","exec-fee-is-a-quarter-percent-at-most","lean-learned-order-never-drops-a-fact","mm-move-never-needs-more-than-it-frees","safe-an-unread-balance-is-never-a-zero","copy-fee-is-a-share-of-a-win-or-nothing","earnings-base-rate-bounded-and-monotone","the-entry-floor-never-leaves-its-bounds","hookrlp-works-only-a-graduated-hookr-key","paused-desk-resumes-only-on-proven-skill","brain-tape-fires-only-on-a-dip-or-the-cap","deposit-fee-never-charges-a-desk-delivery","public-split-is-three-legs-of-one-hundred","what-truncation-strands-is-swept-not-lost","an-unmeasured-incumbent-is-never-abandoned","flywheel-spend-never-exceeds-the-cycle-cap","borrow-draw-never-passes-the-market-ceiling","fund-a-gap-to-nav-is-stated-only-on-one-day","rail-a-session-opens-only-under-its-own-key","robinhood-places-only-the-order-it-proposed","seal-paused-signs-nothing-and-the-cap-holds","the-router-never-moves-for-a-rounding-error","a-flapping-alert-waits-longer-and-never-less","a-perp-dial-scales-a-read-and-never-turns-it","a-round-can-never-promise-more-than-it-holds","blend-stays-between-the-market-and-its-parts","rail-forwards-only-the-equity-order-it-filed","world-milestone-needs-the-desk-not-the-world","bond-a-quote-never-hands-out-a-free-arbitrage","dca-tranche-bounded-and-budget-never-exceeded","index-leg-window-sizes-inside-the-same-bounds","registry-a-filing-is-graded-by-the-move-alone","world-purse-pays-a-fraction-under-the-day-cap","exec-impact-scale-bounded-and-never-past-the-cap","band-refusal-is-never-cheaper-than-the-band-paying","copy-size-never-exceeds-the-bankroll-or-the-wallet","depth-a-buyer-pays-at-least-what-a-leaver-receives","mm-hook-refused-exactly-when-it-can-touch-the-exit","launch-default-rules-move-only-on-proven-separation","robinhood-slip-is-the-signed-distance-from-the-print","solsniper-the-buy-refuses-every-seat-behind-its-room","solve-calibration-moves-halfway-and-only-on-evidence","stock-token-multiplier-never-falls-except-on-a-split","the-entry-floor-moves-only-on-what-the-record-proved","soldesk-a-buy-breaks-even-exactly-at-the-curves-own-odds","equityoracle-a-halted-or-unflagged-token-never-reads-open","chart-a-proof-is-settled-only-by-bars-that-closed-after-it","husd-the-maximum-is-the-chain-figure-and-the-scale-is-exact","a-timeline-subject-weight-is-never-zero-and-one-until-earned","payout-the-tally-conserves-and-only-counts-the-account-named","brain-caps-stay-inside-their-bounds-and-the-cycle-fee-is-small","defidoor-a-build-the-door-hands-out-passes-the-terminals-guard","registry-a-seal-opens-only-on-its-own-fields-and-shut-is-wrong","payout-held-fees-never-exceed-the-credits-and-never-go-negative","safe-a-wash-cycle-is-a-ring-sell-and-a-ring-buy-each-trade-once","chart-the-check-agrees-only-when-both-windows-take-the-same-side","payout-a-missing-price-is-never-a-zero-and-milestones-only-climb","brain-every-split-sums-to-ten-thousand-and-the-trade-leg-is-capped","equityoracle-a-quote-older-than-its-session-allows-never-reads-fresh","haltwatch-gated-only-if-in-the-swap-path-paid-and-carrying-the-oracle","oracle-settlement-conserves-the-pot-and-the-house-keeps-only-the-dust","compute-an-inference-job-goes-only-to-a-machine-that-declared-the-kind","weekendmark-the-mark-is-dollars-over-tokens-between-the-pools-it-keeps","bond-shares-round-against-the-buyer-and-liability-is-netted-never-negative","bond-caps-scale-with-the-balance-and-solvency-refuses-what-cannot-be-covered","credit-an-advance-never-exceeds-the-ltv-the-cap-or-its-share-of-the-expectation","oracle-every-stake-is-paid-under-exactly-one-outcome-and-a-void-returns-them-all","compute-a-job-is-never-priced-under-its-floor-and-a-spec-hashes-only-what-it-uses","tail-cover-scale-is-one-until-thirty-days-and-stays-between-half-and-five-quarters","chart-the-refuting-level-is-always-on-the-far-side-of-price-and-the-sheet-fits-a-post","door-the-default-slippage-moves-only-on-thirty-graded-fills-and-stays-between-twenty-five-and-a-hundred","compute-a-completion-is-bounded-and-priced-at-its-floor-or-above"]}