def definition def or abbrev

`kolmogorovComplexity`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 162def kolmogorovComplexity : String :=

proof body

Definition body.

 163  "Shortest program length to output x"
 164
 165/-- Incompressibility:
 166
 167    Most strings are incompressible!
 168
 169    For strings of length n:
 170    - At most 2^(n-1) can compress to n-1 bits
 171    - Most strings have K(x) ≈ n
 172
 173    Random = incompressible = maximum J-cost-to-entropy ratio -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use