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

derivedCost

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)

  69@[simp] def derivedCost (C : ComparisonOperator) : ℝ → ℝ :=

proof body

Definition body.

  70  fun r => C r 1
  71
  72/-! ## The Four Aristotelian Constraints
  73
  74We encode the classical laws of logic as structural constraints on a
  75comparison operator. The mapping from Aristotle's propositional
  76formulations to functional constraints on C is:
  77
  78  Identity (A = A)             ↦  C(x, x) = 0
  79                                  comparison of a thing with itself is trivial
  80  Non-contradiction (¬(A ∧ ¬A))↦  C(x, y) = C(y, x)
  81                                  the cost is single-valued under reordering
  82                                  (with scale invariance, this gives reciprocity
  83                                   F(x) = F(1/x))
  84  Excluded middle (A ∨ ¬A)     ↦  C is continuous and total on its domain
  85                                  every comparison returns a definite value
  86  Composition consistency      ↦  Route-independence (the d'Alembert form)
  87                                  comparisons assembled forward and backward
  88                                  must compose by a fixed combining rule
  89-/
  90
  91/-- **Identity**: comparing a thing with itself costs zero. The mathematical
  92counterpart of the Aristotelian law A = A. -/

used by (40)

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

… and 10 more

depends on (30)

Lean names referenced from this declaration's body.