Information Algorithmic Prob3 From Jcost

The cost of a message

Algorithmic probability asks how likely a message is to be produced by a computer program. The classic answer is the Solomonoff prior: the probability of a string x is the sum over all programs p that output x of 2 raised to the negative length of p. Shorter programs get more weight. This is a standard idea in information theory, and it connects compression to prediction.

The Recognition Science framework (RS) has its own account of cost. Its central object is a cost function, a measure of how expensive it is to recognize one thing as another. RS proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The module named information algorithmic prob3 from jcost defines a cost on a pair of real numbers m and e as J(m/e). It then proves three facts: the cost is zero when m equals e, the cost is never negative for positive inputs, and the number phi - 3/2 is positive, where phi is the golden ratio.

In plain language, the module shows that a cost function built from J has a sensible minimum at equality and never goes below zero. The third fact, that phi - 3/2 is positive, is a small arithmetic consequence of the golden ratio being larger than 1.5. These are general properties of the cost function, not results about algorithmic probability itself.

What the module does not do is connect J to actual programs or to the Solomonoff prior. The docstring records an intention: at an RS-optimal encoding, the shortest program length would be J(phi) times the length of the message. But the Lean code defines domainCost as J(m/e) without any reference to a specific subject. To make this a theorem about algorithmic probability, one would need to define m and e in terms of programs and outputs. That step is missing.

The module therefore establishes a narrow but solid fact: a certain cost function has the expected properties. It is a building block, not a bridge. The bridge to algorithmic probability remains open.

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]

What this page does not claim

The module does not prove a connection between J and the Solomonoff prior. The module does not establish that J(phi) is the optimal compression rate. The module does not define m and e in terms of programs or outputs.

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/AlgorithmicProb3FromJCost.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: