Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry

show as:
view Lean formalization →

Registry of how mathematical objects arise in the primitive recognition calculus: each object is tagged by one of seven commitments (forced rationals, forced scale, display, completion, convention, quotient, observable/permitted). Downstream native-analysis and strong-closure modules import this taxonomy. The module is definitional: inductive commitment kinds, an RS-object wrapper, classifiers, and a periodic-table summary.

claimAn RS-object is a mathematical entity paired with a commitment $C$ drawn from a seven-kind taxonomy: forced rationals, forced scale, display, completion, convention, quotient, and observable/permitted. The registry maps each constructed real, amplitude, probability, or quotient selection to its generating commitment and records the resulting objecthood table.

background

Primitive Recognition Calculus builds reals, amplitudes, and probabilities from recognition-native primitives (delta-reals, generable reals, calibrated scales, quotient selection, prime-axis coherence) rather than from classical set-theoretic existence. Not every formal expression is on equal footing: some quantities are forced by the recognition composition law and self-similarity, others are display conventions, completions, or permitted observables.

This module sits after DeltaReal, DeltaRealCalibration, GenerableReal, DeltaProbability, DeltaAmplitude, QuotientSelection, ValidComparison, and CompletionConservativity. Those modules supply the raw constructions; ObjecthoodRegistry only classifies them.

The doc-comment states the point directly: seven commitments produce a mathematical object. Sibling names (Commitment, RSObject, commitmentOf, the classify_* family, objecthood_periodic_table) implement that taxonomy as Lean definitions and classifiers.

proof idea

Definition module, not a theorem package. It introduces an inductive (or enumerated) Commitment type with seven constructors, an RSObject pairing payload with commitment, a commitmentOf projection, and a family of classify_* maps that assign each upstream construction (forced rationals, forced scale, display quantities, completions, conventions, quotients, observables/permitted forms) to its commitment. A summary objecthood_periodic_table aggregates the classification. No deep proof obligations beyond type-checking and trivial wrapping of imported constructions.

why it matters in Recognition Science

Native analysis and strong closure need a clean separation between what recognition forces and what is merely conventional or completed. DeltaNativeAnalysis and DeltaNativeStrongClosure import this module for that separation: they can reason about delta-native structure without treating display units, completion points, or quotient choices as ontic necessities.

In the broader Recognition Science foundation, this is bookkeeping for the forcing chain and RCL-derived quantities. Forced rationals and forced scale sit near T5–T6 uniqueness and self-similarity; completion and convention track conservativity of extensions; quotient and observable tags keep measurement and comparison honest. Without the registry, later closure arguments would blur existence with notation.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.

declarations in this module (14)