module module high

`IndisputableMonolith.RecogGeom.Examples`

The module supplies concrete finite configuration spaces on Fin n for n at least 2, together with discrete and sign-based recognizers that induce explicit indistinguishability relations and quotients. Researchers building explicit models of recognition geometry cite these constructions to verify cell resolution and quotient formation before moving to abstract cases. The module proceeds entirely by definitions and direct verifications of basic equivalence properties on the finite sets.

claimLet $C = {0,1,…,n-1}$ be the finite configuration space for integer $n ≥ 2$. A discrete recognizer is a map $R: C → E$ from configurations to events. The induced indistinguishability relation partitions $C$ into resolution cells whose quotient is $C_R = C/∼_R$. Sign recognizers further distinguish positive and negative labels and generate the corresponding equivalence classes.

background

Recognition Geometry treats space as emergent from recognition maps. The Core module introduces the basic types for configurations $C$ and events $E$. The Recognizer module defines maps $R: C → E$ that connect configurations to observable events. Indistinguishable defines the relation $∼_R$ under which two configurations are equivalent precisely when they produce the same event. Quotient then collapses $C$ to the space of resolution cells $C_R = C/∼_R$.

proof idea

This is a definition module containing no proofs. It defines the finite configuration space on Fin n for n ≥ 2, supplies discrete recognizers and sign recognizers, and records direct verifications that indistinguishability coincides with equality for discrete maps and that sign recognizers separate positive and negative classes.

why it matters in Recognition Science

The module supplies the concrete examples required by the Integration module to assemble the full Recognition Geometry framework. It demonstrates how the abstract constructions from Core, Recognizer, Indistinguishable and Quotient operate on finite configuration spaces, thereby grounding the theory in explicit cases before the Integration module provides its comprehensive summary.

scope and limits

Does not treat continuous or infinite configuration spaces.
Does not derive physical constants or mass formulas.
Does not connect to the forcing chain T0-T8 or phi-ladder.
Does not address Berry creation thresholds or Z_cf values.

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