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

lambda_rec_unique

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)

   9def lambda_rec_unique : Prop := ExistsUnique (fun x : ℝ => LawfulNormalizer x)

proof body

Definition body.

  10
  11end URC
  12
  13namespace IndisputableMonolith
  14namespace URCAdapters
  15
  16/-- Prop-level witness: a trivial normalizer at λ=1 satisfies stationarity and scaling invariance
  17    under our current abstract obligations; this stands in for the concrete λ_rec bridge and will be
  18    refined when the ethics alignment hook is exposed. -/

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.