IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCompletenessIndependence

   1/-
   2  PrimitiveRecognitionCalculus/PRCCompletenessIndependence.lean
   3
   4  The deepest open frontier of the δ program, resolved: is the continuous completion
   5  (the move to the order-complete field ℝ) FORCED by the δ / cost axioms, or is it an
   6  independent posit?
   7
   8  Prior work established the SEPARATION (the completion has elements the δ-native
   9  carrier lacks) and tagged the completion as a "stronger commitment". What was
  10  missing was an exact INDEPENDENCE statement: a model of the cost/field axioms that
  11  fails order-completeness. This module supplies it.
  12
  13  The witness is the countable exp/log-closed field `T` of `PRCExpLogField`, on which
  14  the canonical cost `Cost.Jcost` is closed (`PRCCostOnField`). We prove:
  15
  16  * `subfield_not_complete`: ANY proper subfield `K ⊊ ℝ` lacks the least-upper-bound
  17    property. Every subfield contains ℚ (which is dense in ℝ), so for any `r ∉ K` the
  18    Dedekind cut `{x ∈ K : x < r}` is nonempty, bounded above in `K`, yet has no least
  19    upper bound inside `K` (its real supremum is `r ∉ K`, and density rules out any
  20    `K`-element being a least upper bound). This is the classical "a cut at an
  21    irrational has no rational supremum" argument, lifted from ℚ to any proper
  22    subfield.
  23
  24  * `completeness_not_forced_by_cost_axioms`: the countable field `T` is closed under
  25    `Cost.Jcost` and is countable, YET lacks the least-upper-bound property, WHILE ℝ
  26    has it (`Real.exists_isLUB`). So order-completeness is true of one cost-closed
  27    field (ℝ) and false of another (`T`): it is NOT a consequence of the cost/field
  28    axioms. The completion to ℝ is a strictly stronger commitment, independent of δ.
  29
  30  This resolves the question the program flagged as its real remaining frontier: the
  31  continuous completion is NOT δ-forced. δ and the cost laws are satisfied by a
  32  countable, incomplete carrier; completeness is an additional, independent axiom.
  33
  34  HONEST BOUNDARY. "Independence" here is semantic/model-theoretic in the precise
  35  sense that the property `has-LUB` is not entailed by `is-a-subfield-of-ℝ-closed-
  36  under-Jcost`: it holds in ℝ and fails in `T`, both of which are such fields. We do
  37  not build a first-order theory and run a formal independence proof; we exhibit the
  38  two models directly, which is the stronger and more transparent statement.
  39
  40  No project-local axioms. No sorry.
  41-/
  42
  43import IndisputableMonolith.Cost
  44import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCostOnField
  45
  46namespace IndisputableMonolith
  47namespace Foundation
  48namespace PrimitiveRecognitionCalculus
  49namespace CompletenessIndependence
  50
  51open ExpLogField
  52
  53/-- `s` is a least upper bound of `S` lying inside the subfield `K`: it is in `K`, it
  54bounds `S`, and it is `≤` every `K`-element that bounds `S`. This is the relativized
  55notion of supremum that order-completeness of `K` would always supply. -/
  56def IsLUBIn (K : Subfield ℝ) (S : Set ℝ) (s : ℝ) : Prop :=
  57  s ∈ K ∧ (∀ x ∈ S, x ≤ s) ∧ ∀ u ∈ K, (∀ x ∈ S, x ≤ u) → s ≤ u
  58
  59/-- **Any proper subfield of ℝ lacks the least-upper-bound property.** Every subfield
  60contains ℚ; ℚ is dense in ℝ; so for any real `r ∉ K`, the cut `{x ∈ K : x < r}` is
  61nonempty and bounded above in `K`, but no `K`-element is its least upper bound: a
  62candidate `s < r` is beaten by a rational in `(s, r)` that still lies in the cut, a
  63candidate `s > r` is not least because a rational in `(r, s)` already bounds the cut,
  64and `s = r` is impossible since `r ∉ K`. -/
  65theorem subfield_not_complete (K : Subfield ℝ) (hK : (K : Set ℝ) ≠ Set.univ) :
  66    ∃ S : Set ℝ,
  67      (∀ x ∈ S, x ∈ K)
  68        ∧ S.Nonempty
  69        ∧ (∃ b ∈ K, ∀ x ∈ S, x ≤ b)
  70        ∧ ¬ ∃ s, IsLUBIn K S s := by
  71  obtain ⟨r, hr⟩ := (Set.ne_univ_iff_exists_notMem _).mp hK
  72  refine ⟨{x | x ∈ K ∧ x < r}, ?_, ?_, ?_, ?_⟩
  73  · intro x hx; exact hx.1
  74  · obtain ⟨q, hq⟩ := exists_rat_lt r
  75    exact ⟨(q : ℝ), SubfieldClass.ratCast_mem K q, hq⟩
  76  · obtain ⟨q, hq⟩ := exists_rat_gt r
  77    exact ⟨(q : ℝ), SubfieldClass.ratCast_mem K q, fun x hx => le_of_lt (lt_trans hx.2 hq)⟩
  78  · rintro ⟨s, hsK, hub, hleast⟩
  79    rcases lt_trichotomy s r with hlt | heq | hgt
  80    · obtain ⟨q, hsq, hqr⟩ := exists_rat_btwn hlt
  81      have hqS : (q : ℝ) ∈ {x | x ∈ K ∧ x < r} := ⟨SubfieldClass.ratCast_mem K q, hqr⟩
  82      exact absurd (hub _ hqS) (not_le.mpr hsq)
  83    · exact hr (heq ▸ hsK)
  84    · obtain ⟨q, hrq, hqs⟩ := exists_rat_btwn hgt
  85      have hqub : ∀ x ∈ {x | x ∈ K ∧ x < r}, x ≤ (q : ℝ) :=
  86        fun x hx => le_of_lt (lt_trans hx.2 hrq)
  87      exact absurd (hleast _ (SubfieldClass.ratCast_mem K q) hqub) (not_le.mpr hqs)
  88
  89/-- **Every countable subfield of ℝ lacks the least-upper-bound property.**
  90Countability forces properness (ℝ is uncountable), and properness forces
  91incompleteness by `subfield_not_complete`. So order-completeness and countability are
  92flatly incompatible for subfields of ℝ: completeness is exactly what uncountability
  93(the continuum) buys. Whatever countable carrier δ uses, it is never order-complete. -/
  94theorem countable_subfield_not_complete (K : Subfield ℝ)
  95    (hc : (K : Set ℝ).Countable) :
  96    ∃ S : Set ℝ,
  97      (∀ x ∈ S, x ∈ K)
  98        ∧ S.Nonempty
  99        ∧ (∃ b ∈ K, ∀ x ∈ S, x ≤ b)
 100        ∧ ¬ ∃ s, IsLUBIn K S s := by
 101  refine subfield_not_complete K ?_
 102  intro h
 103  exact Cardinal.not_countable_real (h ▸ hc)
 104
 105/-- The countable cost-closed field `T` lacks the least-upper-bound property. -/
 106theorem T_not_complete :
 107    ∃ S : Set ℝ,
 108      (∀ x ∈ S, x ∈ T)
 109        ∧ S.Nonempty
 110        ∧ (∃ b ∈ T, ∀ x ∈ S, x ≤ b)
 111        ∧ ¬ ∃ s, IsLUBIn T S s :=
 112  countable_subfield_not_complete T T_countable
 113
 114/-- ℝ has the least-upper-bound property: every nonempty bounded-above set has a least
 115upper bound. -/
 116theorem real_has_lub (S : Set ℝ) (hne : S.Nonempty) (hbdd : ∃ b, ∀ x ∈ S, x ≤ b) :
 117    ∃ s, IsLUB S s := by
 118  obtain ⟨b, hb⟩ := hbdd
 119  exact Real.exists_isLUB hne ⟨b, fun x hx => hb x hx⟩
 120
 121/-- **Independence of order-completeness from the cost/field axioms.** The countable
 122field `T` is closed under the canonical cost `Cost.Jcost` and is countable, yet it
 123lacks the least-upper-bound property; ℝ has it. Order-completeness therefore holds in
 124one cost-closed subfield of ℝ (namely ℝ itself) and fails in another (`T`): it is not
 125entailed by being a `Cost.Jcost`-closed field. The continuous completion is a
 126strictly stronger, independent commitment, not a δ-consequence. -/
 127theorem completeness_not_forced_by_cost_axioms :
 128    (∀ x ∈ T, Cost.Jcost x ∈ T)
 129      ∧ (T : Set ℝ).Countable
 130      ∧ (∃ S : Set ℝ,
 131          (∀ x ∈ S, x ∈ T) ∧ S.Nonempty ∧ (∃ b ∈ T, ∀ x ∈ S, x ≤ b)
 132            ∧ ¬ ∃ s, IsLUBIn T S s)
 133      ∧ (∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s) :=
 134  ⟨fun _ hx => CostOnField.jcost_mem_T hx, T_countable, T_not_complete, real_has_lub⟩
 135
 136/-- The canonical cost `Cost.Jcost` genuinely satisfies the recognition-cost axioms:
 137the unit law `J(1) = 0` and reciprocal symmetry `J(x) = J(x⁻¹)` for positive `x`. So
 138the premise of the independence result is not merely "closed under a function"; it is
 139"a model of the cost laws". -/
 140theorem jcost_isCostRequirements : Cost.CostRequirements Cost.Jcost :=
 141  ⟨fun hx => Cost.Jcost_symm hx, Cost.Jcost_unit0⟩
 142
 143/-- **Completeness independent of the GENUINE cost laws (not just `Jcost`-closure).**
 144This upgrades `completeness_not_forced_by_cost_axioms`: the premise now records that
 145`Cost.Jcost` is a bona fide recognition cost (unit `J(1)=0`, reciprocal symmetry
 146`J(x)=J(x⁻¹)`, nonnegativity `J(x)≥0` on positives), and that `T` is a countable field
 147on which `Jcost` is closed (hence a model of those laws). `T` still fails the
 148least-upper-bound property while ℝ satisfies it. So order-completeness is not entailed
 149by the genuine cost laws plus the field structure; it is an independent commitment.
 150This is the credibility-gating form: a skeptic cannot say the independence rests on a
 151weak "closure" premise rather than the actual cost axioms. -/
 152theorem completeness_not_forced_by_genuine_cost_laws :
 153    (Cost.Jcost 1 = 0)
 154      ∧ (∀ x : ℝ, 0 < x → Cost.Jcost x = Cost.Jcost x⁻¹)
 155      ∧ (∀ x : ℝ, 0 < x → 0 ≤ Cost.Jcost x)
 156      ∧ (∀ x ∈ T, Cost.Jcost x ∈ T)
 157      ∧ (T : Set ℝ).Countable
 158      ∧ (∃ S : Set ℝ,
 159          (∀ x ∈ S, x ∈ T) ∧ S.Nonempty ∧ (∃ b ∈ T, ∀ x ∈ S, x ≤ b)
 160            ∧ ¬ ∃ s, IsLUBIn T S s)
 161      ∧ (∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s) :=
 162  ⟨Cost.Jcost_unit0, fun _ hx => Cost.Jcost_symm hx, fun _ hx => Cost.Jcost_nonneg hx,
 163    fun _ hx => CostOnField.jcost_mem_T hx, T_countable, T_not_complete, real_has_lub⟩
 164
 165/-- **The sharp final form.** Order-completeness is precisely the content the
 166continuum adds: NO countable subfield of ℝ is order-complete, while ℝ is. Since every
 167δ result places the carrier in a countable field (the constants, the φ-ladder, the
 168cost dynamics all live countably), the carrier δ uses is never order-complete,
 169whichever countable field it is. Completeness is an independent axiom whose only model
 170is uncountable. -/
 171theorem completeness_is_exactly_the_continuum :
 172    (∀ K : Subfield ℝ, (K : Set ℝ).Countable →
 173        ∃ S : Set ℝ, (∀ x ∈ S, x ∈ K) ∧ S.Nonempty ∧ (∃ b ∈ K, ∀ x ∈ S, x ≤ b)
 174          ∧ ¬ ∃ s, IsLUBIn K S s)
 175      ∧ (∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s) :=
 176  ⟨countable_subfield_not_complete, real_has_lub⟩
 177
 178end CompletenessIndependence
 179end PrimitiveRecognitionCalculus
 180end Foundation
 181end IndisputableMonolith
 182