IUT Valuation Hulls / Edition README

Komorebi × IUT — Valuation Hulls and Reconstruction, B05

This is a self-contained Lean source continuation of the Hodge Reduct B04 formalization (the four original IUT PDFs are not redistributed). It proves local valuation saturation, optimal ideal enlargement costs, a stronger F17 addition-reconstruction obstruction, and a discrete quantitative witness criterion. It does not prove or disprove IUT III Corollary 3.12 or abc.

Start here

RESEARCH_NOTE_B05.md — mathematical statements, proofs, explicit model limits.
CLAIM_LEDGER_B05.md — verified versus open claims.
verification/b05/verification.json — actual Lean audit results.
SOURCE_PROVENANCE.md — source mapping and hashes.
HANDOFF_B05.md — next source-dependent task.

Source code

New Lean modules (all imported by formalization/lean/KTG.lean):

KTG/ValuationHulls.lean
KTG/ValuationCost.lean
KTG/HodgeAnchors.lean
KTG/HodgeStructural.lean
KTG/IUT312DiscreteWitness.lean

Previous Block03 / B04 modules and source maps are preserved. All formal modules are dependency-free apart from Lean/Std bundled with Lean 4.34.0-rc2.

Reproduce

From formalization/lean, with the appropriate pinned toolchain:

lake build -KwarningAsError=true

For a full independent check of each Lean source and deliberate negative controls:

LEAN_BIN=/absolute/path/to/lean LAKE_BIN=/absolute/path/to/lake \
    python verification/verify_b05.py

Run the last command from the package root. On Windows, replace the Unix-style environment assignment syntax as appropriate for PowerShell. The verifier records a warning-as-error compilation of every source, a preserved-source audit, interface checks, and rejection of three intentionally false claims.

Additional outputs

The reproducible plot is generated by figures/make_b05_figure.py and saved in PNG and SVG formats. It illustrates only the toy ideal and valuation model.

Licence and source provenance

This research handoff is not a legal opinion on the licence of third-party source texts. The IUT source PDFs are not included in the redistributable package. Original paper names, passage locations, and source hashes are listed in SOURCE_PROVENANCE.md. The archive does not purport to grant a licence to any prior proprietary or third-party file.