module module high

`IndisputableMonolith.RecogGeom.Examples`

The Examples module supplies concrete finite instances of configuration spaces and recognizers to illustrate the abstract Recognition Geometry framework. It defines Fin n (n ≥ 2) as the configuration space together with discrete, sign, and magnitude recognizers, then derives basic indistinguishability and quotient properties. Researchers testing discrete models of recognition maps would cite these examples to check how resolution cells emerge. The module consists of definitions and short lemmas that instantiate the core axioms without deep case

claimLet $C = {0,1,…,n-1}$ be the finite configuration space for integer $n≥2$. A recognizer $R:C→E$ induces the indistinguishability relation $x∼_R y$ iff $R(x)=R(y)$. The quotient $C_R=C/∼_R$ consists of the resolution cells. Discrete, sign, and magnitude recognizers are exhibited as concrete maps on $C$.

background

Recognition Geometry derives spatial structure from recognition maps rather than taking space as primitive. The Core module supplies the basic types for configurations C and events E. The Recognizer module defines a recognizer as any function R:C→E. The Indistinguishable module introduces the induced equivalence x∼_R y when R(x)=R(y), whose classes are the smallest distinguishable units. The Quotient module collapses C to the recognition quotient C_R=C/∼_R.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the Integration module that assembles the complete Recognition Geometry framework. It supplies explicit models that realize axioms RG2 (recognizers map configurations to events) and RG3 (indistinguishability partitions into resolution cells), confirming that geometric structure can arise from lossy recognition maps on finite sets.

scope and limits

Does not treat continuous or infinite configuration spaces.
Does not derive physical constants, dimensions, or the forcing chain T0-T8.
Does not contain numerical simulations or empirical validation.
Does not address general theorems beyond the listed finite examples.

used by (1)

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

IndisputableMonolith.RecogGeom.Integration module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.RecogGeom.Core module_import
IndisputableMonolith.RecogGeom.Indistinguishable module_import
IndisputableMonolith.RecogGeom.Quotient module_import
IndisputableMonolith.RecogGeom.Recognizer module_import

declarations in this module (21)

instance finConfigSpace L35
def discreteRecognizer L39
theorem discrete_indist_iff_eq L47
theorem discrete_singleton_cells L53
inductive Sign L65
def signOf L75
def signRecognizer L79
theorem sign_indistinguishable L86
theorem neg_indist L91
theorem neg_pos_dist L95
theorem zero_pos_dist L99
def magnitudeRecognizer L105
theorem magnitude_indistinguishable L112
theorem plus_minus_indist L117
theorem diff_magnitude_dist L121
theorem sign_distinguishes_3_neg3 L136
theorem magnitude_indist_3_neg3 L139
theorem sign_indist_3_5 L142
theorem magnitude_distinguishes_3_5 L145
theorem composition_refines L150
def examples_status L176