Formal source guide and replay prerequisites
Strong Artin: source and evidence
README.md
1 # Strong Artin formal source guide
2
3 The latest authoritative mathematical checkpoint is the exact v0.38 effective
4 matrix Hensel archive, SHA-256
5 `d5f065bcb05ee02465082804dfb14800f82b86f43a8838eded2e3d3519abcb9a`.
6 Strong Artin is open.
7
8 `history/v0.38/src/` contains its seven new mathematical modules. These exact
9 bytes match the successful September 12, 2026 extracted-archive replay.
10 `history/v0.38/DECLARATIONS.json` records 60 named declarations: 44 theorems,
11 15 definitions and one abbreviation. Helpers and controls are included. These
12 counts are not independent discoveries or progress percentages.
13
14 `history/v0.9/` through `history/v0.38/` are selected source, build and boundary
15 files from the checkpoint's exact nested ancestry. No sibling branch absent
16 from the original archive has been added. Repeated dependency files have not
17 been merged into one synthetic Lean namespace. Historical result filenames
18 such as `verification/fresh/RESULT.json` retain their original meaning: they
19 describe the run timestamp inside the record, not verification performed for
20 this publication.
21
22 `ANCESTRY_INDEX.json` records each archive identity and its canonical extracted
23 directory. Thirty byte-distinct archives occur in the retained ancestry, with
24 repeated edges. `AUTHENTICATION_2026-10-08.json` records fresh CRC, payload-hash
25 and static-source checks. Authentication is not Lean compilation.
26
27 The current publication attempted to recover the matching portable Lean kit.
28 The seven Library archive parts were found, but downloading their bytes failed
29 with HTTP 403. No kit was materialized and no fresh compiler invocation ran.
30 See `CURRENT_REPLAY_STATUS.json` and `../evidence/LEAN_COVERAGE.md`.
31
32 ## Replay
33
34 Use the exact original v0.38 archive included in the handoff and the external
35 portable kit with these pins:
36
37 * Lean 4.34.0-rc2, commit `6a10ac8c22beadecabdbb0919c2b50214762f91d`
38 * Mathlib `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`
39 * Combined offline runtime archive SHA-256
40 `66dfa8ce4627489bc61e44a77782931d36c1b626a177790a5d4599034b70ec34`
41
42 The isolated wrapper preserves all historical evidence:
43
44 ```bash
45 python3 lean/replay_current.py \
46 --archive /absolute/path/to/Strong_Artin_Lean_v0.38.0_Effective_Matrix_Hensel_Checked.zip \
47 --kit /absolute/path/to/Komorebi_Portable_Lean_4.34.0-rc2 \
48 --work /absolute/path/to/a/new/replay-directory
49 ```
50
51 The original verifier rebuilds every new v0.38 module into a fresh object
52 directory and audits all 60 named constants. It excludes unrelated project
53 object paths, authenticates the v0.37 parent and reuses the pinned Mathlib
54 compiled cache. It does not rebuild the full ancestry, Mathlib or a second
55 Lean kernel. A `BLOCKED`, `PARTIAL`, `FAIL` or timeout is not a pass.
56
57 To reproduce the byte audit, use `authenticate_archives.py` with the original
58 archive, the retained September 12 replay JSON and a new output path.
59
60 ## Current module map
61
62 | Module | Mathematical task |
63 | --- | --- |
64 | `NCPowerEstimates` | Ordered derivative and ultrametric nonlinear remainder estimates |
65 | `NCPowerLocalImage` | Exact small-ball image and uniqueness from a bounded two-sided inverse |
66 | `PadicMatrixNorm` | Entrywise matrix norm, completeness, integral embedding and congruence comparison |
67 | `MatrixInverseCertificate` | Pair-indexed coefficient action and exact inverse identities checked on matrix units |
68 | `EffectiveMatrixRoot` | Existence and uniqueness of integral matrix powers in a deep congruence fibre |
69 | `FiniteMatrixCriterion` | Reduction of the target condition to one finite residue-ring calculation |
70 | `EffectiveMatrixControls` | Singular-residual unipotent example, noncommuting root and rejected target |
71
72 The source documentation explains the older obstruction, syzygy, local-gauge,
73 compactness and scalar-horizon results. The coverage report distinguishes their
74 proved conditional statements from the arithmetic inputs they require.