pith. machine review for the scientific record. sign in
def

Identity

definition
show as:
view math explainer →
module
IndisputableMonolith.Foundation.LogicAsFunctionalEquation
domain
Foundation
line
93 · github
papers citing
1 paper (below)

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.LogicAsFunctionalEquation on GitHub at line 93.

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

  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
  95
  96/-- **Non-contradiction (reciprocal symmetry)**: the cost of comparing x to y
  97equals the cost of comparing y to x. The mathematical counterpart of the
  98Aristotelian law ¬(A ∧ ¬A): if comparison were not single-valued under
  99reordering, the same comparison would simultaneously hold and not hold. -/
 100def NonContradiction (C : ComparisonOperator) : Prop :=
 101  ∀ x y : ℝ, 0 < x → 0 < y → C x y = C y x
 102
 103/-- **Excluded middle (totality and continuity)**: every comparison returns a
 104definite real value and small perturbations of inputs give small
 105perturbations of cost. The mathematical counterpart of the Aristotelian
 106law A ∨ ¬A applied to continuous comparisons: there is no "neither" outcome
 107on the comparison's domain. -/
 108def ExcludedMiddle (C : ComparisonOperator) : Prop :=
 109  ContinuousOn (Function.uncurry C) (Set.Ioi (0 : ℝ) ×ˢ Set.Ioi (0 : ℝ))
 110
 111/-- **Scale invariance**: the cost of a comparison depends only on the
 112ratio of the two quantities. This is the structural bridge from a
 113two-argument comparison operator to a one-argument cost on positive ratios.
 114It is what allows the four laws of logic, which make no reference to absolute
 115scale, to be expressed as constraints on the multiplicative group ℝ₊. -/
 116def ScaleInvariant (C : ComparisonOperator) : Prop :=
 117  ∀ x y lam : ℝ, 0 < x → 0 < y → 0 < lam →
 118    C (lam * x) (lam * y) = C x y
 119
 120/-- **Route-independence (the d'Alembert form)**: the cost of any composite
 121comparison, taken in its symmetric forward-and-backward form on positive
 122ratios, is a polynomial function of the constituent ratio costs.
 123Concretely: assembling a comparison of ratio xy with a comparison of ratio

papers checked against this theorem (showing 1 of 1)