bootstrap_to_real
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that LogicSupported implies conditional completeness or the Archimedean property.
- Does not construct a comparison operator from the Law of Logic in isolation.
- Does not apply to non-Archimedean or non-totally-ordered fields.
- Does not address uniqueness beyond order-ring isomorphism.
Lean usage
theorem bootstrap_closure (K : Type*) [ConditionallyCompleteLinearOrderedField K] (h : LogicSupported K) : Nonempty (K ≃+*o ℝ) := bootstrap_to_real K hformal statement (Lean)
114theorem bootstrap_to_real
115 (K : Type*) [ConditionallyCompleteLinearOrderedField K]
116 (_ : LogicSupported K) :
117 Nonempty (K ≃+*o ℝ) :=
proof body
Tactic-mode proof.
118 ⟨LinearOrderedField.inducedOrderRingIso K ℝ⟩
119
120/-- **Idempotence**: `ℝ` itself is a Logic-supported domain (witnessed
121by any of the comparison operators we already have over `ℝ`). The
122bootstrap theorem then says nothing new on `ℝ`, but on any other
123candidate ordered field it forces an isomorphism to `ℝ`. -/