def definition def or abbrev

`coding_length`

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

formal statement (Lean)

  19noncomputable def coding_length (events : ℕ) : ℝ := Cost.Jcost (events : ℝ)

Definition body.

  20
  21/-- Theorem: φ-prior holds as unique MDL from T5 J-unique. -/

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use