derivedCostOn

formal source

  56abbrev ComparisonOperatorOn (K : Type*) := K → K → K
  57
  58/-- Derived cost from a comparison operator on a generic ordered field. -/
  59@[simp] def derivedCostOn {K : Type*} [One K] (C : ComparisonOperatorOn K) : K → K :=
  60  fun r => C r 1
  61
  62variable {K : Type*}
  63
  64/-- Identity, generic field version. -/
  65def IdentityOn [Zero K] [LT K] (C : ComparisonOperatorOn K) : Prop :=
  66  ∀ x : K, 0 < x → C x x = 0
  67
  68/-- Non-contradiction, generic field version. -/
  69def NonContradictionOn [LT K] [Zero K] (C : ComparisonOperatorOn K) : Prop :=
  70  ∀ x y : K, 0 < x → 0 < y → C x y = C y x
  71
  72/-- Scale invariance, generic field version. -/
  73def ScaleInvariantOn [Zero K] [LT K] [Mul K] (C : ComparisonOperatorOn K) : Prop :=
  74  ∀ x y lam : K, 0 < x → 0 < y → 0 < lam →
  75    C (lam * x) (lam * y) = C x y
  76
  77/-- Distinguishability, generic field version. -/
  78def DistinguishabilityOn [Zero K] [LT K] (C : ComparisonOperatorOn K) : Prop :=
  79  ∃ x y : K, 0 < x ∧ 0 < y ∧ C x y ≠ 0
  80
  81/-! ## 2. The bootstrap theorem
  82
  83The Law of Logic on an ambient field `K` plus Archimedean +
  84Dedekind-completeness implies `K ≃+*o ℝ`. The proof is by reduction
  85to Mathlib's classical characterization of `ℝ`.
  86
  87The completeness hypothesis is the standard analytic input that makes
  88"continuous comparison" non-vacuous; without it, the comparison
  89operator could live on `ℚ` or any incomplete subfield. With it, `K`