# Project Status

**Release:** Komorebi IUT–KTG v0.3.0, Block 03  
**Date:** 2026-09-17

## Verified state

- **IUT source corpus:** four user-supplied principal papers preserved.
- **Block 02 abstract KTG framework:** preserved and reverified.
- **Source-faithful Step (xi-e) interface:** compiler-verified.
- **Typed IPL/SHE/APT certificate:** compiler-verified.
- **Nine obstruction channels:** typed with separate control obligations.
- **Two-stage normalization and grade bridge:** compiler-verified.
- **IUT IV `j²` attachment:** explicitly represented and compiler-verified.
- **Source-specific logical countermodel:** compiler-verified.
- **Positive source-shaped finite example:** compiler-verified.
- **Clean Lean build:** PASS, 24 jobs.
- **Per-source warning-as-error audit:** PASS, 22 files.
- **Placeholder and axiom scan:** PASS.
- **Block 02 core preservation:** PASS, 14 module sources unchanged.
- **IUT III Corollary 3.12:** neither proved nor disproved.

## Strongest checked source-faithful theorem interface

```text
Concrete IPL/SHE/APT realization
+ controlled Ind1–Ind3 and live obstruction channels
+ determinant/procession normalization witness
+ SourceWitnessTheorem
+ monotone observable
⇒ scalar log-volume order.
```

The source witness theorem is a separate premise. It is not synthesized from
linkage, common representation, compatibility, or normalization.

## Principal Block 03 formal advances

- `IUT312.TypedData`
- `IUT312.QPilotHullContainment`
- `IUT312.ObstructionSemantics`
- `IUT312.ObstructionControl`
- `IUT312.SourceRealizationCertificate`
- `IUT312.NormalizationData`
- `IUT312.normalizationGradeBridge`
- `IUT312.directNormalization`
- `IUT312.StepXiEWitnessPreservation`
- `IUT312.SourceWitnessTheorem`
- `IUT312.witnessBridgeOfSourceTheorem`
- `IUT312.SourceCountermodel.no_sourceWitnessTheorem`
- `IUT312.cor312ScalarBoundOfSourceWitness`

## Current frontier

The formal shape is no longer the main uncertainty. The next frontier is
source instantiation. The decisive task is to construct actual IUT terms for
O1–O4 and either locate or prove the O5 q-pilot hull-containment theorem with
its full dependency chain. O6 then becomes a concrete monotonicity theorem for
the log-volume observable.