pith. machine review for the scientific record. sign in
def definition def or abbrev

identity_config

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  74def identity_config (t : ℕ) : Config := ⟨1, one_pos, t, by simp [Real.log_one]⟩

proof body

Definition body.

  75
  76/-! ## Cost Functions for Modal Logic -/
  77
  78/-- The fundamental cost J(x) = ½(x + 1/x) - 1.
  79
  80    This is the unique cost satisfying d'Alembert + normalization + calibration (T5). -/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.