Foundation Primitive Recognition Calculus Objecthood Registry Classify Completio

Completing the real numbers

The real numbers are the number system that fills every gap. Given any nonempty set of real numbers with an upper bound, the system guarantees a least upper bound: the smallest number that is greater than or equal to every member of the set. This property, called completeness, is what makes calculus work, since limits and continuous functions depend on having no missing points. The classical statement is a theorem about the real line itself, independent of any framework.

In the Recognition Science framework, the declaration classify_completion assigns this property a precise role. The framework's objecthood registry classifies every mathematical object by the kind of commitment that produces it. The real numbers are tagged as a completion: an independent axiom that adds limit points to a smaller system. The theorem proves that any nonempty bounded set of reals has a least upper bound, which is exactly the classical completeness property. The framework's library, a machine-checked collection of formal theorems, verifies this classification.

The classification matters because it separates what is forced from what is chosen. The rational numbers, for example, are forced into every carrier of the framework; no carrier can omit them. But the reals are not forced in the same way. The framework proves that no countable cost-closed carrier has the completeness property, so completeness is an independent axiom rather than a consequence of the earlier structure. The theorem classify_completion records this independence: the real numbers appear only when the completion axiom is added.

What the declaration does not claim is equally important. It does not prove that the real numbers are the only possible complete ordered field; the classical uniqueness theorem for complete ordered fields is not part of this declaration. It does not show that completeness follows from the framework's earlier principles; the framework explicitly treats it as an independent axiom. And it does not say that the real numbers are physically real or that the universe must use them; it only classifies the mathematical object within the framework's registry.

The practical consequence is a clean ledger of mathematical commitments. When the framework uses the real numbers, it knows exactly what it is assuming: a completion axiom, not a forced consequence. This lets the framework distinguish between objects that are uniquely determined by its laws and objects that require a separate choice. The classification turns an implicit background assumption into an explicit, typed attribute.

/-- `completion`: ℝ has the least-upper-bound property. (That no countable
cost-closed carrier has it, so completeness is an independent axiom, is
`PRCCompletenessIndependence.completeness_is_exactly_the_continuum`.) -/
theorem classify_completion :
    ∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s := by
  intro S hne hbdd
  obtain ⟨b, hb⟩ := hbdd
  exact Real.exists_isLUB hne ⟨b, fun x hx => hb x hx⟩

/-- **Phase 8 headline: the periodic table of objecthood.** Each catalogued object
carries its commitment, and the assignment is exactly the evidence above:
distinction-forced (rationals, the coherence scale), display (ℝδ value map),
completion (ℝ), convention (cost unit), quotient and observable (the gauge
quotient and its probes), permitted (the generable inventory). Objecthood is not
flat: each object is produced by a specific kind of commitment, and the kind is
now a typed, proved attribute. -/
theorem objecthood_periodic_table :
    commitmentOf RSObject.deltaRationals = Commitment.forced
      ∧ commitmentOf RSObject.protocolReals = Commitment.display
      ∧ commitmentOf RSObject.classicalReals = Commitment.completion
      ∧ commitmentOf RSObject.calibrationUnit = Commitment.convention
      ∧ commitmentOf RSObject.physicalQuotient = Commitment.quotient
      ∧ commitmentOf RSObject.observableFamily = Commitment.observable
      ∧ commitmentOf RSObject.generableCarrier = Commitment.permitted
      ∧ commitmentOf RSObject.primeScale = Commitment.forced :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩

/-- `completion`: ℝ has the least-upper-bound property. (That no countable
cost-closed carrier has it, so completeness is an independent axiom, is
`PRCCompletenessIndependence.completeness_is_exactly_the_continuum`.) -/
theorem classify_completion :
    ∀ S : Set ℝ, S.Nonempty → (∃ b, ∀ x ∈ S, x ≤ b) → ∃ s, IsLUB S s := by
  intro S hne hbdd
  obtain ⟨b, hb⟩ := hbdd
  exact Real.exists_isLUB hne ⟨b, fun x hx => hb x hx⟩

What this page does not claim

The declaration does not prove the classical uniqueness theorem for complete ordered fields. The declaration does not show that completeness follows from the framework's earlier principles. The declaration does not claim that the real numbers are physically real or that the universe must use them.

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/ObjecthoodRegistry.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: