KTG build instructions and claim boundary
IUT Valuation Hulls
README.md
1 # Komorebi Transport Geometry Lean Project
2
3 **Version:** 0.3.0
4 **Toolchain:** `leanprover/lean4:v4.34.0-rc2`
5
6 This project is dependency-free apart from Lean's bundled `Std` library.
7
8 ## Build
9
10 ```bash
11 lake build
12 ```
13
14 ## Full Block 03 verification
15
16 From the bundle root:
17
18 ```bash
19 python verification/verify_block03.py --clean
20 ```
21
22 When Lean and Lake are not on `PATH`, set their exact executable paths:
23
24 ```bash
25 LEAN_BIN=/path/to/lean \
26 LAKE_BIN=/path/to/lake \
27 python verification/verify_block03.py --clean
28 ```
29
30 The verifier performs a clean Lake build, elaborates every Lean source with
31 warnings treated as errors, scans for prohibited proof placeholders and axiom
32 declarations, checks the required Block 03 interface, compares the preserved
33 Block 02 core hashes, and writes
34 `verification/block03_final/verification.json`.
35
36 ## Core modules
37
38 - `KTG.Basic`: typed contexts and dependency-free `KPreorder`.
39 - `KTG.Transport`: common-carrier transport and structural relatedness.
40 - `KTG.Certification`: realization certificates and obstruction control.
41 - `KTG.Coricity`: invariance predicates.
42 - `KTG.Hull`: closure and enclosure operators.
43 - `KTG.Observable`: monotone scalar observables.
44 - `KTG.Witness`: measurement witnesses and hull witnesses.
45 - `KTG.Normalization`: typed normalization and grade-space bridges.
46 - `KTG.CertifiedBound`: witness bridge and generic certified bound.
47 - `KTG.Countermodels`: finite logical non-implication models.
48 - `KTG.Examples`: positive generic full-pipeline model.
49 - `KTG.Curvature`: relational path flatness and curvature witnesses.
50 - `KTG.SafeAbstraction`: safe factorization through public abstractions.
51 - `KTG.IUT312Model`: non-circular Block 02 interface for the audited hinge.
52
53 ## Block 03 source-faithful modules
54
55 - `KTG.IUT312Types`: distinct IUT-shaped object and measurement types.
56 - `KTG.IUT312Certificates`: IPL, SHE, APT, and obstruction-control interfaces.
57 - `KTG.IUT312Normalization`: determinant/procession grades and grade bridge.
58 - `KTG.IUT312WitnessObligation`: exact open Step (xi-e) witness theorem.
59 - `KTG.IUT312SourceCountermodel`: all pre-witness fields without containment.
60 - `KTG.IUT312Cor312Bridge`: refinement of the abstract Corollary 3.12 interface.
61 - `KTG.IUT312SourceExample`: positive finite equality-model realization.
62
63 ## Claim boundary
64
65 The project verifies the formal interface, countermodel, and finite positive
66 example. It does not formalize all of IUT and does not prove or disprove IUT III
67 Corollary 3.12. The IUT-specific inhabitant of
68 `IUT312.SourceWitnessTheorem` remains open.