Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ValidComparison

show as:
view Lean formalization →

Defines a valid comparison as a bridge from a native object N through a display D to an observable O, with a commuting law that observation of the display matches the native protocol. Anyone formalizing display-versus-native agreement in the primitive recognition calculus cites this. The module packages the bridge structure, validity predicate, composition, and a short doctrine statement rather than a deep proof.

claimA bridge is a triple of maps linking a native object $N$, a display object $D$, and an observable $O$. The bridge is a valid comparison when the diagram commutes: observing the display agrees with the native observable protocol. Validity is preserved under composition of bridges, and is equivalent to the corresponding native comparison condition.

background

In the primitive recognition calculus, physical content is carried by native objects, while instruments and formalisms present display objects that must be read by an observable protocol. A comparison is trustworthy only when those layers agree.

This module introduces the bridge data packing $N$, $D$, and $O$ together with the maps between them, and the predicate that the display-then-observe path equals the native observe path. That commuting law is the mathematical content of "valid comparison."

Sibling material includes an iff linking validity to a native formulation, a compose operation on bridges, a lemma that composition preserves validity, and a short doctrine statement packaging the intended use of the notion.

proof idea

This is largely a definition module. It introduces the bridge structure and the validity predicate, then records elementary consequences: equivalence with the native comparison condition, composition of bridges, and closure of validity under that composition. The doctrine item is a packaging statement, not a multi-step derivation. Downstream modules import these definitions rather than reprove the commuting law.

why it matters in Recognition Science

Valid comparison is the interface that lets later foundation modules treat display constructions as faithful to native recognition data. It is imported by DeltaNativeAnalysis and DeltaNativeStrongClosure (native delta analysis and strong closure), HilbertDisplayCompletion (completing Hilbert-style displays), ObjecthoodRegistry (registering what counts as an object), and ValidComparisonExamples (concrete instances).

Without a commuting bridge, display-level identities cannot be promoted to native claims. In the Recognition Science stack this sits under the foundation layer that feeds the forcing chain and cost calculus: displays must not invent structure that the native J-cost and recognition protocol do not support.

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)