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 proof that Kolmogorov Theory's new corollaries actually follow from the classical results they claim to use.

The core problem this project addresses is subtle but important. Kolmogorov Theory (KT) is a framework that uses algorithmic information theory (AIT) — think Kolmogorov complexity, the length of the shortest program that produces a string — to reason about regulators, persistence, self-models, and agents. The classical AIT results it builds on (the invariance theorem, the coding theorem, symmetry of information, and so on) are well-established and not in doubt. What is in doubt, or at least unverified, is whether the new KT-specific corollaries actually follow logically from those classical results, or whether they sneak in hidden assumptions, type errors, or gaps. KTAIT is a Lean 4 formalization project that machine-checks exactly this dependency structure.

The methodology is clean. Classical AIT results are declared as named axioms — honest placeholders, not gaps. Every KT corollary must then be proved from those axioms with no sorry (Lean's placeholder for an unfinished proof). A toy model witnesses that the axiom layer is jointly satisfiable, so the corollaries aren't vacuously true. The type system does real work here: KT roles like substrate, pattern, self-code, regulator, and time are distinct types, so a structurally nonsensical expression — like computing the information a whole pattern shares with itself as a part — fails to compile rather than silently producing a meaningless number.

The project has already machine-checked a substantial corpus. All five planned roadmap phases are complete. This includes the probabilistic Algorithmic Regulator Theorem (ART), the Bayes-to-Kolmogorov bridge, the temporal self-model proposition, persistence conservation, regulator selection, self-model incompleteness (three independent obstructions), and regulatory coarse-graining uncomputability. The formalization also caught and recorded real errors: a counterexample to a sufficiency claim in WP0186 (non-strict boundary conditions don't guarantee attraction), a retraction of an inference in WP0186 that wasn't licensed by the axioms, and a proof that circular shifts are not valid null models for algorithmic mutual information — a mistake that had caused a real screening effect to be incorrectly withdrawn as noise.

What remains out of scope is also clearly stated. The "model it or pay for it" conjecture — that a regulator sustaining a complexity gap must either carry proportional model content or dissipate proportional thermodynamic work — cannot even be stated in the current framework because the frame has no bath, no temperature, and no physical realization. The Lie-group and differential-geometry layer of the world-models paper is deferred to a separate track. The source is a detailed working paper with a full theorem inventory and formalization status table; it is substantive and the summary above reflects what the paper actually establishes.