  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`
  90is forced to be `ℝ`.
  91-/
  92
  93/-- A linearly ordered field is **Logic-supported** when a comparison
  94operator on it satisfies the four Aristotelian conditions plus scale
  95invariance and distinguishability. We package the ordered-field
  96structure required to even *state* these conditions. -/
  97structure LogicSupported (K : Type*) [Mul K] [Zero K] [One K] [LT K] where
  98  zero_lt_one_in_K : (0 : K) < 1
  99  C : ComparisonOperatorOn K

papers checked against this theorem

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