Strong Artin: source and evidence

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 {
2   "generated_utc": "2026-10-08T18:10:07.028379+00:00",
3   "status": "BLOCKED",
4   "fresh_lean_compiler_invocations": 0,
5   "historical_replay_relabelled_as_fresh": false,
6   "lean_path": null,
7   "lake_path": null,
8   "elan_path": null,
9   "python": "3.12.14",
10   "platform": "Linux-6.18.44-x86_64-with-glibc2.39",
11   "local_kit_absent": true,
12   "required_lean_commit": "6a10ac8c22beadecabdbb0919c2b50214762f91d",
13   "required_mathlib_commit": "aeb72f1e9981b6d35b426b16dca7759be3e7ba06",
14   "matching_kit_parts_found": 7,
15   "kit_download_attempt": {
16     "status": "FAIL",
17     "process_returncode": 1,
18     "error": "library download request failed: download failed with HTTP status 403",
19     "files_materialized": 0,
20     "failure_kind": "dependency byte access failure, not Lean proof failure"
21   },
22   "bounded_wrapper_attempt": {
23     "started_utc": "2026-10-08T18:10:06.689514+00:00",
24     "scope": "Seven new v0.38 modules plus all-named-constant axiom audit; pinned Mathlib cache reused",
25     "parent_freshly_replayed": false,
26     "archive": "/workspace/scratch/fd5253a691e7/strong_artin_sources/Strong_Artin_Lean_v0.38.0_Effective_Matrix_Hensel_Checked.zip",
27     "kit": "/mnt/data/lean_runtime/Komorebi_Portable_Lean_4.34.0-rc2",
28     "status": "BLOCKED",
29     "archive_sha256": "d5f065bcb05ee02465082804dfb14800f82b86f43a8838eded2e3d3519abcb9a",
30     "failure": "Matching Lean binary is absent",
31     "fresh_lean_replay": false,
32     "finished_utc": "2026-10-08T18:10:06.729487+00:00",
33     "runtime_seconds": 0.04037749700000859
34   },
35   "authentication_status": "PASS",
36   "authenticated_unique_archives": 30,
37   "current_v038_payload_hashes_verified": 126,
38   "historical_manifest_entries_verified": 3004,
39   "current_historical_replay_source_match": true,
40   "static_forbidden_source_markers": 0,
41   "development_failures": [
42     {
43       "action": "First archive authentication",
44       "failure": "Parser treated normalized relative paths beginning ./ and historical absolute paths as missing ZIP members, producing 512 false missing-file findings",
45       "repair": "Normalize relative paths and resolve historical absolute paths against each manifest directory; preserved original output and reran successfully"
46     },
47     {
48       "action": "Second archive authentication",
49       "failure": "Traversal initially omitted the standalone embedded v0.9 archive outside a base directory, yielding 29 rather than30 unique nodes",
50       "repair": "Traverse all embedded ZIP archive children, deduplicate by SHA256; final count30 with all hashes valid"
51     }
52   ],
53   "non_claims": [
54     "No fresh Lean compile",
55     "No full combined historical-source replay",
56     "No new Strong Artin proof"
57   ]
58 }

Back to source controls

Back to Strong Artin: source and evidence