Foundation Primitive Recognition Calculus Prccompleteness Independence Real Has

The real numbers' defining property

The real numbers, denoted ℝ, are the standard continuum of mathematics: the number line with no gaps. Their defining structural property is the least-upper-bound property: every nonempty set of real numbers that is bounded above has a least upper bound, also called the supremum. For example, the set of all numbers whose square is less than 2 has a supremum, namely √2, even though √2 is not in the set. This property is what distinguishes the real numbers from the rationals, where such a supremum can fail to exist.

The theorem real_has_lub in the framework's machine-checked library of formal theorems states this classical fact in full generality: for any nonempty set S of real numbers that has an upper bound, there exists a real number s that is the least upper bound of S. The proof is a direct formalization of the standard construction, relying on the library's existing theorem Real.exists_isLUB. This is a theorem about the real numbers themselves, independent of any framework-specific assumptions.

In Recognition Science, the significance of real_has_lub is not the fact itself, which is classical, but what it does not follow from. The framework's cost function J(x) = (x + 1/x)/2 - 1 and its associated field structure can be realized on a countable subfield T of the real numbers. This countable field T is closed under the cost function and satisfies the cost laws, yet it lacks the least-upper-bound property. The theorem completeness_not_forced_by_genuine_cost_laws proves that order-completeness is not entailed by the genuine cost laws plus the field structure.

The sharp final form, completeness_is_exactly_the_continuum, states the dichotomy: no countable subfield of ℝ is order-complete, while ℝ itself is. Since every result in the framework's δ-calculus places its carrier in a countable field, the carrier is never order-complete. Order-completeness is therefore an independent axiom whose only model is uncountable. The real numbers' defining property is precisely the content that the continuum adds, and the framework treats it as such: a separate commitment, not a derived consequence.

/-- ℝ has the least-upper-bound property: every nonempty bounded-above set has a least
upper bound. -/
theorem real_has_lub (S : Set ℝ) (hne : S.Nonempty) (hbdd : ∃ b, ∀ x ∈ S, x ≤ b) :
    ∃ s, IsLUB S s := by
  obtain ⟨b, hb⟩ := hbdd
  exact Real.exists_isLUB hne ⟨b, fun x hx => hb x hx⟩

/-- The countable cost-closed field `T` lacks the least-upper-bound property. -/
theorem T_not_complete :
    ∃ S : Set ℝ,
      (∀ x ∈ S, x ∈ T)
        ∧ S.Nonempty
        ∧ (∃ b ∈ T, ∀ x ∈ S, x ≤ b)
        ∧ ¬ ∃ s, IsLUBIn T S s :=
  countable_subfield_not_complete T T_countable

/-- **Completeness independent of the GENUINE cost laws (not just `Jcost`-closure).**
This upgrades `completeness_not_forced_by_cost_axioms`: the premise now records that
`Cost.Jcost` is a bona fide recognition cost (unit `J(1)=0`, reciprocal symmetry
`J(x)=J(x⁻¹)`, nonnegativity `J(x)≥0` on positives), and that `T` is a countable field
on which `Jcost` is closed (hence a model of those laws). `T` still fails the
least-upper-bound property while ℝ satisfies it. So order-completeness is not entailed
by the genuine cost laws plus the field structure; it is an independent commitment.
This is the credibility-gating form: a skeptic cannot say the independence rests on a
weak "closure" premise rather than the actual cost axioms. -/
theorem completeness_not_forced_by_genuine_cost_laws :
    (Cost.Jcost 1 = 0)
      ∧ (∀ x : ℝ, 0 < x → Cost.Jcost x = Cost.Jcost x⁻¹)
      ∧ (∀ x : ℝ, 0 < x → 0 ≤ Cost.Jcost x)
      ∧ (∀ x ∈ T, Cost.Jcost x ∈ T)
      ∧ (T : Set ℝ).Countable
      ∧ (∃ S : Set ℝ,
          (∀ x ∈ S, x ∈ T) ∧ S.Nonempty ∧ (∃ b ∈ T, ∀ x ∈ S, x ≤ b)
            ∧ ¬ ∃ s, IsLUBIn T S s)
      ∧ (∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s) :=
  ⟨Cost.Jcost_unit0, fun _ hx => Cost.Jcost_symm hx, fun _ hx => Cost.Jcost_nonneg hx,
    fun _ hx => CostOnField.jcost_mem_T hx, T_countable, T_not_complete, real_has_lub⟩

/-- **The sharp final form.** Order-completeness is precisely the content the
continuum adds: NO countable subfield of ℝ is order-complete, while ℝ is. Since every
δ result places the carrier in a countable field (the constants, the φ-ladder, the
cost dynamics all live countably), the carrier δ uses is never order-complete,
whichever countable field it is. Completeness is an independent axiom whose only model
is uncountable. -/
theorem completeness_is_exactly_the_continuum :
    (∀ K : Subfield ℝ, (K : Set ℝ).Countable →
        ∃ S : Set ℝ, (∀ x ∈ S, x ∈ K) ∧ S.Nonempty ∧ (∃ b ∈ K, ∀ x ∈ S, x ≤ b)
          ∧ ¬ ∃ s, IsLUBIn K S s)
      ∧ (∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s) :=
  ⟨countable_subfield_not_complete, real_has_lub⟩

What this page does not claim

The real numbers are the only ordered field with the least-upper-bound property; the theorem does not address uniqueness among all ordered fields. The framework derives the existence of the real numbers from the cost axioms; it only shows that order-completeness is independent of them. The countable field T is a model of the cost laws in the sense of satisfying the unit law and reciprocal symmetry, but it is not a model of the full real-number structure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PRCCompletenessIndependence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: