CALLIOPE · BCOM

We are building {KTAIT}, a Lean~4 + Mathlib formalization whose purpose is narrow and load-bearing: to machine-check that the Kolmogorov-Theory (KT) corollaries follow logically from an explicit algorithmic-information-theory (AIT) interface, and that the KT ontology is typed so that structural errors (e.g.\ comparing a whole pattern to its own part) cannot silently compile. We do not re-prove classical AIT: the standard AIT and probability results (the invariance theorem, the coding theorem, symmetry of information, Kraft's inequality, Bayes' rule, the Solomonoff--Levin universal semimeasure, the recursion theorem, Rice's and Chaitin's theorems, and the Vereshchagin--Vitányi structure-function results) are taken as a clearly delimited axiom layer. Every KT corollary is then proved from that layer with no {sorry}, and a toy model witnesses that the axiom layer is jointly satisfiable (so the corollaries are not vacuously true). This working paper states the methodology, fixes the axiom layer, inventories every theorem/lemma across the KT corpus with its current formalization status, and sets a prioritized roadmap.

A machine-checked sanity layer for Kolmogorov Theory: prove that the new corollaries actually follow from the classical results, and that the ontology is typed tightly enough to catch structural nonsense at compile time.

The core worry this project addresses isn't whether the classical algorithmic information theory (AIT) results are correct — those are well-established. The worry is whether the newer Kolmogorov Theory (KT) corollaries (persistence equations, regulator gaps, self-regulation propositions) are correctly derived from those results, and whether the conceptual objects are being combined in ways that are even meaningful. A typed proof assistant is a good tool for exactly this: it refuses to accept a proof unless every logical step is justified, and it refuses to typecheck a statement that mixes incompatible roles.

The methodology is deliberately narrow. Classical AIT theorems — invariance, symmetry of information, the coding theorem, Solomonoff-Levin semimeasure, and so on — are taken as explicit axioms, not re-proved. The formalization then proves the KT corollaries from that axiom layer with no sorry (Lean's "trust me" escape hatch). A concrete toy model (a degenerate frame where K = 0) witnesses that the axiom set is satisfiable, so the corollaries aren't vacuously true from a hidden contradiction. The #print axioms command then lets you inspect exactly which named axioms each corollary depends on — nothing hidden.

The ontology typing is where the real conceptual work lives. The paper defines distinct Lean types for substrate states, patterns, self-codes, readouts, regulators, and time — not just strings or natural numbers. Crucially, SelfCode carries evidence that it is a sub-pattern of a given Pattern. This makes a specific class of structural error impossible to write silently: the mutual information of a pattern with its own self-code, taken statically, is vacuous (a whole vs. its own part). With the typed ontology, that statement either fails to typecheck or demands a visible coercion. The correct object is always temporal — $I_K(\mathcal{S}_t : \mathcal{S}_{t+\tau})$ — and the type system routes you there.

The source document is a project kickoff and learning guide rather than a completed formalization. It is honest about this: it inventories the milestones (toolchain setup through satisfiability witness), provides illustrative Lean 4 code sketches explicitly labeled as "intent, not final code," and flags that the actual Mathlib API names need to be verified against the installed version. The formalization itself is in progress. What the document firmly establishes is the methodology, the axiom layer, the ontology design, and the definition of done for "Level 1" — with Levels 2 (computability-backed K from a universal prefix machine) and 3 (full ART proof) deferred to future work.