Foundation Primitive Recognition Calculus Objecthood Registry

The objecthood registry

The objecthood registry is a classification system for the mathematical objects that appear in a physical theory. It answers a simple question about each object: what kind of act brought it into existence? The registry defines seven such acts, called commitments. An object can be forced, meaning uniquely determined by the laws with no freedom; permitted, meaning an admissible free choice; quotient, meaning an identification of states that no measurement can tell apart; completion, meaning a closure that adds limit points and requires its own axiom; display, meaning a rendering or instrument rather than a native ingredient; observable, meaning defined by what can be measured; or convention, meaning a gauge or labeling choice.

The registry assigns each object in the framework one of these tags. The rational numbers are forced, because every field of real numbers must contain them. The classical real numbers are a completion, because they require the least-upper-bound property as an independent axiom. The physical quotient is forced by indistinguishability: two states are identified exactly when no observable can tell them apart. The cost-scale unit is a convention, a free real number fixed only by a continuum-side datum, a gauge in the physicist's sense. The generable carrier is permitted, a free but admissible choice of a countable inventory.

The registry also audits background objects that usually enter a theory untyped: continuum, point, space, set, equality, infinity, function, probability, amplitude. Each receives an explicit commitment tag. Complex numbers, Hilbert spaces, manifolds, and measures are typed as displays or completions. This prevents background objects from quietly assuming a status they have not earned.

In Recognition Science, the registry is a periodic table of objecthood. The assignment is a proved theorem in the framework's machine-checked library of formal theorems: each catalogued object carries its commitment, and the assignment is exactly the evidence above. Objecthood is not flat. Each object is produced by a specific kind of commitment, and the kind is now a typed, proved attribute. The registry's value is that it forces the theory to say what kind of act produced each object it uses, and to say it in a form a machine has checked.

/-- `forced`: the rationals are forced into every carrier; they are the unique
prime subfield. No carrier of the framework can omit them. -/
theorem classify_forced_rationals :
    ∀ (K : Subfield ℝ) (q : ℚ), (q : ℝ) ∈ K :=
  fun K q => SubfieldClass.ratCast_mem K q

/-- `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⟩

/-- `quotient`: the physical quotient identifies two states iff no observable
distinguishes them. The quotient is forced by indistinguishability. -/
theorem classify_quotient :
    ∀ {X C : Type} (F : Set (X → C)) (x y : X),
      QuotientSelection.proj F x = QuotientSelection.proj F y ↔ QuotientSelection.ObsEquiv F x y :=
  fun F x y => QuotientSelection.forced_iff F x y

/-- `convention`: the cost-scale unit is a faithful, transitively-rescaled torsor,
a single free real fixed only by a continuum-side datum. It is a gauge. -/
theorem classify_convention :
    (∀ c d : ℝ, 0 < c → 0 < d →
        (fun t => Real.cosh (c * t) - 1) = (fun t => Real.cosh (d * t) - 1) → c = d)
      ∧ (∀ c d : ℝ, 0 < c → 0 < d →
          ∃ μ : ℝ, 0 < μ ∧
            (fun t => Real.cosh (c * (μ * t)) - 1) = (fun t => Real.cosh (d * t) - 1)) :=
  DeltaRealCalibration.discrete_does_not_force_unit

/-- **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⟩

What this page does not claim

The registry does not prove that the seven commitment types are exhaustive. The registry does not assign commitment types to objects outside the framework's own construction. The registry does not claim that the least-upper-bound property is derivable from the framework's other axioms.

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: