Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry

show as:
view Lean formalization →

Registry of the seven commitments that turn a formal construction into a Recognition-Science mathematical object. It classifies each construction as forced rational, forced scale, display, completion, convention, quotient, or observable/permitted, and packages the result as an RSObject with an explicit commitment. Downstream native-analysis and strong-closure modules cite the periodic table of objecthood to keep analytic claims inside the permitted class.

claimA finite registry of seven commitments $C$ such that a construction $X$ is an RS-object only when it carries a well-typed commitment $C(X)\in\{\text{forced rationals},\text{forced scale},\text{display},\text{completion},\text{convention},\text{quotient},\text{observable/permitted}\}$. The module supplies the classification maps and the resulting objecthood periodic table.

background

Primitive Recognition Calculus builds real quantities from discrete recognition data (Delta-reals, generable reals, amplitudes, probabilities) and then must say which of those constructions count as genuine mathematical objects rather than scaffolding or display conventions. Upstream modules supply the raw carriers: calibrated Delta-reals, quotient selection, prime-axis coherence, generable reals, Delta-probabilities and amplitudes, valid comparisons, and completion conservativity.

This module introduces the commitment type and the RS-object wrapper. Each commitment records why a quantity is allowed to appear in a theorem: it may be forced by the rational or scale structure, be a mere display choice, arise by conservative completion, be a conventional normalization, be a quotient identification, or be an observable/permitted quantity. The classification functions assign every construction one of these seven labels.

The local setting is foundational bookkeeping inside the forcing chain: before native analysis or strong closure can treat a real as physical, its objecthood commitment must be registered.

proof idea

This is a definition-and-classification module, not a deep proof module. It declares the inductive (or enumerated) type of commitments, the RS-object structure pairing a carrier with its commitment, the projection that recovers the commitment, and a family of classifiers (forced rationals, forced scale, display, completion, convention, quotient, observable, permitted). The objecthood periodic table assembles those classifiers into a single lookup. Any lemmas are thin wrappers that restate the classifiers or the table; there is no substantial tactic development.

why it matters in Recognition Science

Without an explicit objecthood registry, later analytic claims risk treating display conventions or non-conservative completions as physical reals. DeltaNativeAnalysis and DeltaNativeStrongClosure import this module so that native limits, closures, and strong-closure arguments only fire on constructions whose commitment is permitted or observable. The seven-commitment table is the gate between the primitive calculus (Delta-reals, generable reals, amplitudes) and the parts of the framework that feed mass ladders, constants, and the T0–T8 forcing chain. It keeps the Recognition Composition Law and J-cost calculus from being applied to quantities that were never forced.

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)