ABC: source and evidence reader

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

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.