module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ObjecthoodRegistry`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (2)

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

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeAnalysis module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaNativeStrongClosure module_import

depends on (9)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CompletionConservativity module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaAmplitude module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaReal module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.GenerableReal module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PrimeAxisCoherence module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison module_import

declarations in this module (14)

inductive Commitment L48
inductive RSObject L59
def commitmentOf L88
theorem classify_forced_rationals L119
theorem classify_forced_scale L125
theorem classify_display L133
theorem classify_completion L143
theorem classify_convention L151
theorem classify_quotient L161
theorem classify_observable L168
theorem classify_permitted L176
theorem objecthood_periodic_table L189
theorem background_object_audit L205
theorem display_object_extension L230