module module high

`IndisputableMonolith.RecogGeom.Examples`

This module supplies concrete examples of configuration spaces in Recognition Geometry, taking the form of finite sets Fin n for n ≥ 2. Researchers constructing discrete recognizers or testing indistinguishability relations would cite these examples to instantiate the abstract framework. The module consists of definitions and small lemmas that apply the imported core, recognizer, indistinguishability, and quotient constructions to the finite case.

claimConfiguration space $C$ is the finite set $C = $ Fin $n$ for integer $n$ with $n$ ≥ 2, equipped with a recognizer $R: C → E$ and the induced indistinguishability relation whose quotient yields the recognition cells.

background

Recognition Geometry treats space as emergent from recognition maps rather than primitive. The Core module supplies the basic types for configurations and events. The Recognizer module defines a recognition map $R: C → E$ that sends configurations to observable events. The Indistinguishable module introduces the equivalence relation of indistinguishability, whose classes are the resolution cells. The Quotient module forms the recognition quotient $C_R = C / {∼}$. The Examples module instantiates these objects on the finite set Fin n with n ≥ 2 distinct configurations.

proof idea

This is a definition module, no proofs. It assembles the imported modules into explicit finite examples and records a handful of elementary lemmas that verify the expected relations hold on Fin n.

why it matters in Recognition Science

The module supplies the discrete test cases required by the Integration module, which assembles all Recognition Geometry components into a complete framework summary. It directly supports the finite-configuration illustrations needed to connect the abstract axioms RG2 and RG3 to concrete models.

scope and limits

Does not treat continuous or infinite configuration spaces.
Does not derive new general theorems beyond the imported modules.
Does not address the forcing chain or Recognition Science constants.
Does not provide numerical simulations or physical interpretations.

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