Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

show as:
view Lean formalization →

Defines the valid-comparison bridge between a native recognition object, its display presentation, and an observable protocol. The central law is a commuting square: observing the display recovers the native observable. Downstream modules on delta-native analysis, Hilbert display completion, and objecthood registry import this interface. The module is definitional scaffolding plus composition and equivalence lemmas, not a deep existence proof.

claimA valid comparison is a bridge $(N,D,O)$ from a native object $N$ to a display object $D$ and an observable $O$ such that observation of the display agrees with the native observable protocol (the comparison square commutes). Composition of valid bridges remains valid; validity is equivalent to the native comparison condition.

background

In the Primitive Recognition Calculus, physical content is carried by native objects, while experiments and Hilbert-space presentations live on display and observable layers. A mismatch between those layers would make derived spectra or selection rules untrustworthy.

This module packages that agreement as a bridge: native $N$, display $D$, observable $O$, together with a commuting law that observation of the display recovers the native protocol. Sibling names indicate the interface: a Bridge carrier, a validity predicate, an equivalence to a native-only formulation, and a composition operation closed on valid bridges.

The surrounding foundation work (forcing chain, J-cost uniqueness, eight-tick structure) is upstream of this layer. Here the concern is purely structural: when is a displayed comparison a legitimate stand-in for the native one.

proof idea

Definition module with light algebraic closure. It introduces the bridge type and the validity predicate, proves that validity is equivalent to the native comparison condition, and shows that composition of valid bridges is again valid. A short doctrine statement packages the intended use. No deep analytic or measure-theoretic argument lives here; downstream modules supply concrete instances and stronger closure properties.

why it matters in Recognition Science

Valid comparison is the gate that lets display-level constructions (Hilbert presentations, registry entries, delta-native analyses) speak for native recognition objects. Importers include DeltaNativeAnalysis, DeltaNativeStrongClosure, HilbertDisplayCompletion, ObjecthoodRegistry, and ValidComparisonExamples.

Without a commuting bridge, display spectra or objecthood claims could drift from the native protocol. This module therefore sits under the Primitive Recognition Calculus stack as the shared interface those parents rely on when they close strong delta-native properties or complete Hilbert displays. It does not itself force constants or dimensions (T5–T8); it only certifies that a comparison is admissible before those results are read off a display.

scope and limits

used by (5)

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

declarations in this module (6)