IndisputableMonolith.Foundation.DomainBootstrap

   1import Mathlib
   2import IndisputableMonolith.Foundation.LogicAsFunctionalEquation
   3import IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability
   4
   5/-!
   6  DomainBootstrap.lean
   7
   8  Move 2: bootstrap theorem for the comparison-operator domain.
   9
  10  The Law of Logic, as stated in `Foundation.LogicAsFunctionalEquation`,
  11  uses a comparison operator `C : ℝ → ℝ → ℝ`. The recovered real line
  12  in `Foundation.RealsFromLogic` is itself derived from the same Law of
  13  Logic. That is a chicken-and-egg, not a paradox: we use `ℝ` as the
  14  ambient ordered field, and recover an isomorphic `LogicReal` from
  15  inside the framework. To close the loop, we need a uniqueness
  16  theorem stating that any ordered-field ambient on which the Law of
  17  Logic can be stated is canonically isomorphic to `ℝ`.
  18
  19  The classical fact used here is the standard characterization of the
  20  real numbers as the unique Archimedean Dedekind-complete ordered
  21  field. This is part of the Mathlib analysis library, available via
  22  the order-isomorphism `OrderIso (· < · : K → K → Prop) (· < · : ℝ → ℝ → Prop)`
  23  for an Archimedean conditionally complete linearly ordered field.
  24
  25  The theorem in this module states: a linearly ordered field on which
  26  a Law-of-Logic comparison operator is supported (with the
  27  Archimedean and Dedekind-completeness hypotheses that any continuous
  28  comparison-operator structure forces) is canonically isomorphic to
  29  ℝ as an ordered field. The completeness hypothesis is named
  30  explicitly because the Law of Logic on its own does not single out
  31  Archimedean completeness; that is the residual analytic input.
  32
  33  This makes the chicken-and-egg explicit: the Law of Logic plus the
  34  natural completeness/Archimedean hypothesis on the ambient field
  35  forces that field to be `ℝ`, and the Law of Logic on `ℝ` recovers
  36  the same field as `LogicReal` (this direction is in
  37  `Foundation.RealsFromLogic`).
  38-/
  39
  40namespace IndisputableMonolith
  41namespace Foundation
  42namespace DomainBootstrap
  43
  44/-! ## 1. The ambient-field abstraction
  45
  46We rephrase the comparison-operator structure over a generic linearly
  47ordered field `K` rather than over `ℝ`. The four Aristotelian
  48conditions transcribe directly. The Excluded Middle (continuity)
  49condition requires `K` to carry a topology compatible with the order;
  50the standard choice is the order topology, which `LinearOrderedField`
  51gives via Mathlib's `LinearOrderedField` to `TopologicalSpace`
  52instance.
  53-/
  54
  55/-- A comparison operator on a linearly ordered field. -/
  56abbrev ComparisonOperatorOn (K : Type*) := K → K → K
  57
  58/-- Derived cost from a comparison operator on a generic ordered field. -/
  59@[simp] def derivedCostOn {K : Type*} [One K] (C : ComparisonOperatorOn K) : K → K :=
  60  fun r => C r 1
  61
  62variable {K : Type*}
  63
  64/-- Identity, generic field version. -/
  65def IdentityOn [Zero K] [LT K] (C : ComparisonOperatorOn K) : Prop :=
  66  ∀ x : K, 0 < x → C x x = 0
  67
  68/-- Non-contradiction, generic field version. -/
  69def NonContradictionOn [LT K] [Zero K] (C : ComparisonOperatorOn K) : Prop :=
  70  ∀ x y : K, 0 < x → 0 < y → C x y = C y x
  71
  72/-- Scale invariance, generic field version. -/
  73def ScaleInvariantOn [Zero K] [LT K] [Mul K] (C : ComparisonOperatorOn K) : Prop :=
  74  ∀ x y lam : K, 0 < x → 0 < y → 0 < lam →
  75    C (lam * x) (lam * y) = C x y
  76
  77/-- Distinguishability, generic field version. -/
  78def DistinguishabilityOn [Zero K] [LT K] (C : ComparisonOperatorOn K) : Prop :=
  79  ∃ x y : K, 0 < x ∧ 0 < y ∧ C x y ≠ 0
  80
  81/-! ## 2. The bootstrap theorem
  82
  83The Law of Logic on an ambient field `K` plus Archimedean +
  84Dedekind-completeness implies `K ≃+*o ℝ`. The proof is by reduction
  85to Mathlib's classical characterization of `ℝ`.
  86
  87The completeness hypothesis is the standard analytic input that makes
  88"continuous comparison" non-vacuous; without it, the comparison
  89operator could live on `ℚ` or any incomplete subfield. With it, `K`
  90is forced to be `ℝ`.
  91-/
  92
  93/-- A linearly ordered field is **Logic-supported** when a comparison
  94operator on it satisfies the four Aristotelian conditions plus scale
  95invariance and distinguishability. We package the ordered-field
  96structure required to even *state* these conditions. -/
  97structure LogicSupported (K : Type*) [Mul K] [Zero K] [One K] [LT K] where
  98  zero_lt_one_in_K : (0 : K) < 1
  99  C : ComparisonOperatorOn K
 100  identity : IdentityOn C
 101  non_contradiction : NonContradictionOn C
 102  scale_invariant : ScaleInvariantOn C
 103  distinguishability : DistinguishabilityOn C
 104
 105/-- **Bootstrap theorem (named-hypothesis form)**: a linearly ordered
 106field on which the Law of Logic is supported and which is Archimedean
 107and conditionally complete is canonically isomorphic to `ℝ` as an
 108ordered field. The Archimedean and conditional-completeness
 109hypotheses are the analytic content the Law of Logic does not on its
 110own provide; they are named here as inputs.
 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 ℝ`.
 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. -/
 155theorem bootstrap_closure
 156    (K : Type*) [ConditionallyCompleteLinearOrderedField K]
 157    (h : LogicSupported K) :
 158    Nonempty (K ≃+*o ℝ) :=
 159  bootstrap_to_real K h
 160
 161/-! ## 4. Summary
 162
 163The Law of Logic, on its own, does not literally name the ambient
 164field as `ℝ`; it requires a domain that is at least a linearly
 165ordered field. Adding the analytic content (Archimedean + Dedekind
 166completeness) forces the domain to be `ℝ`. The recovered real line
 167from `Foundation.RealsFromLogic` then matches the ambient `ℝ`, and
 168the chicken-and-egg is closed up to canonical isomorphism.
 169
 170The single residual classical input is the Archimedean
 171completeness of the ambient field. This is named, not hidden. -/
 172
 173end DomainBootstrap
 174end Foundation
 175end IndisputableMonolith
 176