Information Kolmogorov Complexity Rs

The recognition cost of data

Kolmogorov complexity is a classical idea from algorithmic information theory: the complexity of a piece of data is the length of the shortest program that produces it. Random data has high complexity because no short program compresses it. The framework's page for this topic proposes a different measure, one tied to its own notion of recognition, a forced cost of registering an event in a discrete ledger. The proposal is that recognition complexity grows as a logarithm of data length, specifically the base-phi logarithm times a constant factor of about 8.47.

That proposal is a research note, not a result. The machine-checked library of formal theorems proves only three general facts about the cost function J, facts that hold for any positive inputs. It proves the cost vanishes when the two inputs are equal, it proves the cost is never negative for positive inputs, and it proves that the golden-ratio constant phi minus 3/2 is positive. The module defines its cost as J applied to a ratio of two real numbers, but it never defines what those numbers mean for Kolmogorov complexity. Without a definition of the data length m and the reference length e in the subject's own terms, the theorems say nothing specific about information.

The module does assemble a certificate structure that bundles these three facts together, and it proves that such a certificate exists. This is a formal wrapper, a way of saying the three general facts are available. It is not a proof about Kolmogorov complexity. The body of the module is shared verbatim with thousands of sibling modules, a template applied to many subjects. The honest summary is that this page records an intended direction, not an established theory.

What a reader can take away is a clear boundary. The framework has a proved cost function with strong properties, and it has a conjecture about how that cost might measure information. The gap between them is exactly the missing definition of what m and e are for a piece of data. Until that definition exists, the log-phi growth claim remains a hypothesis waiting for its grounding.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem cert_inhabited : Nonempty KolmogorovCert := ⟨cert⟩

What this page does not claim

The log-phi growth proposal is not proved; it is a research note. The three proved facts are generic properties of the cost function, not facts about information. No definition connects the cost function's inputs to data length or program length.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/Kolmogorov_Complexity_RS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: