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
proof body
Definition body.
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. -/
depends on (34)
Lean names referenced from this declaration's body.