bootstrap_to_real

formal source

 111
 112The conclusion is the existence of an order-preserving ring
 113isomorphism with `ℝ`. -/
 114theorem bootstrap_to_real
 115    (K : Type*) [ConditionallyCompleteLinearOrderedField K]
 116    (_ : LogicSupported K) :
 117    Nonempty (K ≃+*o ℝ) :=
 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 `ℝ`. -/
 124def real_supports_logic
 125    (C : LogicAsFunctionalEquation.ComparisonOperator)
 126    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C) :
 127    LogicSupported ℝ where
 128  zero_lt_one_in_K := by norm_num
 129  C := C
 130  identity := h.identity
 131  non_contradiction := h.non_contradiction
 132  scale_invariant := h.scale_invariant
 133  distinguishability :=
 134    LogicAsFunctionalEquation.distinguishability_of_nonTrivial C h.non_trivial
 135
 136/-! ## 3. Closing the chicken-and-egg
 137
 138The chain is now explicitly idempotent.
 139
 140Forward direction (`Foundation.RealsFromLogic`): the Law of Logic on
 141`ℝ` recovers a `LogicReal` carrier with `LogicReal ≃+*o ℝ`.
 142
 143Backward direction (this module): a Law-of-Logic-supported ambient
 144ordered field `K` (Archimedean + conditionally complete) is `≃+*o ℝ`.