# 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

1. `RESEARCH_NOTE_B05.md` — mathematical statements, proofs, explicit model limits.
2. `CLAIM_LEDGER_B05.md` — verified versus open claims.
3. `verification/b05/verification.json` — actual Lean audit results.
4. `SOURCE_PROVENANCE.md` — source mapping and hashes.
5. `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:

```bash
lake build -KwarningAsError=true
```

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

```bash
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.