`ComparisonOperator`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.LogicAsFunctionalEquation
domain: Foundation
line: 64 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation on GitHub at line 64.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  61returns a real-valued cost of comparing them. The four Aristotelian
  62constraints below are the structural content of comparison being a
  63well-posed operation. -/
  64abbrev ComparisonOperator := ℝ → ℝ → ℝ
  65
  66/-- The cost function derived from a comparison operator by fixing the
  67second argument at the multiplicative identity. Under scale invariance,
  68this is well-defined on the multiplicative group of positive ratios. -/
  69@[simp] def derivedCost (C : ComparisonOperator) : ℝ → ℝ :=
  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. -/
  93def Identity (C : ComparisonOperator) : Prop :=
  94  ∀ x : ℝ, 0 < x → C x x = 0

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.