Edition README
IUT Valuation Hulls
README.md
1 # Komorebi × IUT — Valuation Hulls and Reconstruction, B05
2
3 This is a self-contained Lean source continuation of the Hodge Reduct B04
4 formalization (the four original IUT PDFs are not redistributed). It proves
5 local valuation saturation, optimal ideal enlargement costs, a stronger F17
6 addition-reconstruction obstruction, and a discrete quantitative witness
7 criterion. It does **not** prove or disprove IUT III Corollary 3.12 or abc.
8
9 ## Start here
10
11 1. `RESEARCH_NOTE_B05.md` — mathematical statements, proofs, explicit model limits.
12 2. `CLAIM_LEDGER_B05.md` — verified versus open claims.
13 3. `verification/b05/verification.json` — actual Lean audit results.
14 4. `SOURCE_PROVENANCE.md` — source mapping and hashes.
15 5. `HANDOFF_B05.md` — next source-dependent task.
16
17 ## Source code
18
19 New Lean modules (all imported by `formalization/lean/KTG.lean`):
20
21 - `KTG/ValuationHulls.lean`
22 - `KTG/ValuationCost.lean`
23 - `KTG/HodgeAnchors.lean`
24 - `KTG/HodgeStructural.lean`
25 - `KTG/IUT312DiscreteWitness.lean`
26
27 Previous Block03 / B04 modules and source maps are preserved. All formal
28 modules are dependency-free apart from Lean/Std bundled with Lean 4.34.0-rc2.
29
30 ## Reproduce
31
32 From `formalization/lean`, with the appropriate pinned toolchain:
33
34 ```bash
35 lake build -KwarningAsError=true
36 ```
37
38 For a full independent check of each Lean source and deliberate negative controls:
39
40 ```bash
41 LEAN_BIN=/absolute/path/to/lean LAKE_BIN=/absolute/path/to/lake \
42 python verification/verify_b05.py
43 ```
44
45 Run the last command from the package root. On Windows, replace the Unix-style
46 environment assignment syntax as appropriate for PowerShell. The verifier
47 records a warning-as-error compilation of every source, a preserved-source
48 audit, interface checks, and rejection of three intentionally false claims.
49
50 ## Additional outputs
51
52 The reproducible plot is generated by `figures/make_b05_figure.py` and saved
53 in PNG and SVG formats. It illustrates only the toy ideal and valuation model.
54
55 ## Licence and source provenance
56
57 This research handoff is not a legal opinion on the licence of third-party
58 source texts. The IUT source PDFs are **not included** in the redistributable
59 package. Original paper names, passage locations, and source hashes are listed
60 in `SOURCE_PROVENANCE.md`. The archive does not purport to grant a licence to
61 any prior proprietary or third-party file.