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
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.