bootstrap_to_real
plain-language theorem explainer
Any conditionally complete linearly ordered field carrying a comparison operator that meets the Aristotelian conditions of identity and non-contradiction together with scale invariance and distinguishability is canonically isomorphic to the reals as an ordered field. Researchers closing the foundational loop in Recognition Science cite the result to justify identifying the ambient domain with ℝ. The proof is a one-line wrapper invoking Mathlib's induced order-ring isomorphism once the typeclass supplies Archimedean and completeness properties.
Claim. Let $K$ be a conditionally complete linearly ordered field. Suppose $K$ admits a comparison operator $C$ satisfying the identity, non-contradiction, scale-invariance and distinguishability axioms together with $0<1$. Then there exists an order-preserving ring isomorphism $K ≃ ℝ$.
background
The DomainBootstrap module supplies the bootstrap step that resolves the circularity between stating the Law of Logic via a comparison operator on ℝ and recovering an isomorphic copy from inside the framework. LogicSupported packages the ordered-field data required to express the four Aristotelian conditions plus scale invariance and distinguishability on such an operator.
proof idea
The proof is a one-line wrapper that applies the Mathlib lemma LinearOrderedField.inducedOrderRingIso K ℝ. The typeclass ConditionallyCompleteLinearOrderedField already encodes the Archimedean and Dedekind-completeness hypotheses needed for the standard uniqueness characterization of the reals.
why it matters
The declaration is invoked verbatim by bootstrap_closure to conclude that the Law of Logic plus Archimedean completeness selects ℝ up to canonical isomorphism. It supplies the missing analytic input that the Law of Logic alone does not provide, thereby closing the chicken-and-egg argument recorded in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.