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

H_UniquenessVerified

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)

  29def H_UniquenessVerified : Prop :=

proof body

Definition body.

  30  ∀ (F : ℝ → ℝ), InformationCost F → (∀ x > 0, F x = Cost.Jcost x)
  31
  32-- Legacy axiom eliminated. See CostUniqueness.T5_uniqueness_complete.
  33
  34/-- **HYPOTHESIS**: Thermodynamic Bound.
  35    Recognition cost satisfies the Landauer bound for information erasure.
  36
  37    STATUS: SCAFFOLD — Bound derived in `Information.Thermodynamics`.
  38    TODO: Complete the Taylor expansion proof in `Thermodynamics.lean`. -/

depends on (9)

Lean names referenced from this declaration's body.