real_supports_logic

formal source

 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 ℝ`.
 145
 146Composition: starting from `ℝ` as the ambient field, we recover
 147`LogicReal ≃+*o ℝ`; conversely, any other ambient field that supports
 148the Law of Logic with the same analytic completeness is `≃+*o ℝ`. The
 149choice of `ℝ` as the comparison-operator domain is therefore a
 150canonical choice up to isomorphism, not a contingent one. -/
 151
 152/-- **Bootstrap closure**: the Law of Logic plus Archimedean
 153completeness uniquely picks out `ℝ` as the ambient ordered field, up
 154to canonical isomorphism. -/