PROJECT_STATUS.md
ABC: source and evidence reader
PROJECT_STATUS.md
1 # Project Status
2
3 **Release:** Komorebi IUT–KTG v0.3.0, Block 03
4 **Date:** 2026-09-17
5
6 ## Verified state
7
8 - **IUT source corpus:** four user-supplied principal papers preserved.
9 - **Block 02 abstract KTG framework:** preserved and reverified.
10 - **Source-faithful Step (xi-e) interface:** compiler-verified.
11 - **Typed IPL/SHE/APT certificate:** compiler-verified.
12 - **Nine obstruction channels:** typed with separate control obligations.
13 - **Two-stage normalization and grade bridge:** compiler-verified.
14 - **IUT IV `j²` attachment:** explicitly represented and compiler-verified.
15 - **Source-specific logical countermodel:** compiler-verified.
16 - **Positive source-shaped finite example:** compiler-verified.
17 - **Clean Lean build:** PASS, 24 jobs.
18 - **Per-source warning-as-error audit:** PASS, 22 files.
19 - **Placeholder and axiom scan:** PASS.
20 - **Block 02 core preservation:** PASS, 14 module sources unchanged.
21 - **IUT III Corollary 3.12:** neither proved nor disproved.
22
23 ## Strongest checked source-faithful theorem interface
24
25 ```text
26 Concrete IPL/SHE/APT realization
27 + controlled Ind1–Ind3 and live obstruction channels
28 + determinant/procession normalization witness
29 + SourceWitnessTheorem
30 + monotone observable
31 ⇒ scalar log-volume order.
32 ```
33
34 The source witness theorem is a separate premise. It is not synthesized from
35 linkage, common representation, compatibility, or normalization.
36
37 ## Principal Block 03 formal advances
38
39 - `IUT312.TypedData`
40 - `IUT312.QPilotHullContainment`
41 - `IUT312.ObstructionSemantics`
42 - `IUT312.ObstructionControl`
43 - `IUT312.SourceRealizationCertificate`
44 - `IUT312.NormalizationData`
45 - `IUT312.normalizationGradeBridge`
46 - `IUT312.directNormalization`
47 - `IUT312.StepXiEWitnessPreservation`
48 - `IUT312.SourceWitnessTheorem`
49 - `IUT312.witnessBridgeOfSourceTheorem`
50 - `IUT312.SourceCountermodel.no_sourceWitnessTheorem`
51 - `IUT312.cor312ScalarBoundOfSourceWitness`
52
53 ## Current frontier
54
55 The formal shape is no longer the main uncertainty. The next frontier is
56 source instantiation. The decisive task is to construct actual IUT terms for
57 O1–O4 and either locate or prove the O5 q-pilot hull-containment theorem with
58 its full dependency chain. O6 then becomes a concrete monotonicity theorem for
59 the log-volume observable.