Pith. sign in
module module high

IndisputableMonolith.Foundation.RecognizerInducesLogic

show as:
view Lean formalization →

The module defines a recognizer as a surjection from configuration space onto event space whose many-to-one fibers generate the indistinguishability quotient. Physicists and mathematicians tracing the emergence of logic from recognition geometry cite it when linking recognition to Aristotelian structure. The module supplies the core definition plus a certification theorem whose proof is a direct construction from the imported distinction and mismatch modules.

claimA recognizer is a surjective map $\pi: \mathcal{C} \twoheadrightarrow \mathcal{E}$ whose fibers define an indistinguishability equivalence on configurations; the induced comparison operator $C$ satisfies symmetry $C(x,y)=C(y,x)$ and thereby encodes non-contradiction.

background

The module occupies the Foundation layer and imports PrimitiveDistinction, MagnitudeOfMismatch, and ObserverFromRecognition. MagnitudeOfMismatch encodes the Aristotelian non-contradiction condition (L2) as symmetry of the single-valued comparison operator $Cxy = Cyx$. ObserverFromRecognition shows that non-trivial recognition forces an interface that serves as the primitive observer. The local setting is Recognition Geometry, in which logic is not postulated but extracted from the quotient induced by any many-to-one recognizer.

proof idea

This is a definition module, no proofs. It introduces the Recognizer type as the surjection, records the induced indistinguishability relation, and supplies a certification theorem that the resulting structure satisfies the required logical properties by direct appeal to the symmetry already proved in MagnitudeOfMismatch.

why it matters in Recognition Science

The module supplies the recognizer-to-logic bridge that the root IndisputableMonolith module imports to reach the master forcing-chain theorem. It exposes the RecognizerComposition hypothesis that MultiplicativeRecognizerL4 later discharges to obtain (L4) Composition Consistency. The construction fills the step claimed in the companion paper RS_Recognition_Geometry_Logic_Unification.tex where any compositional recognizer family on a multiplicative event space satisfies the required logical axioms automatically.

scope and limits

used by (2)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)