IndisputableMonolith.RecogGeom.Connectivity
This module defines recognition-connected sets in Recognition Geometry: a set S is recognition-connected for recognizer r precisely when all its points are mutually indistinguishable under the indistinguishability relation. It supplies the core predicates IsRecognitionConnected, IsLocallyRegular, and SatisfiesRG5 together with elementary lemmas for empty sets, singletons, and resolution cells. Researchers building geometric models of recognition processes cite these definitions when they need uniform event visibility across a subset. The module
claimA subset $S$ of configuration space $C$ is recognition-connected for recognizer $r$ when $x$ and $y$ are indistinguishable for every pair $x,y$ in $S$, i.e., $x$ and $y$ lie in the same equivalence class of the relation $C/$.
background
Recognition Geometry begins with the recognition quotient $C_R = C/$, where the equivalence relation identifies configurations that no recognizer can distinguish. The Connectivity module works inside this quotient by introducing the predicate IsRecognitionConnected, which requires that an entire set $S$ collapses to a single point in $C_R$. Related definitions include IsLocallyRegular (local uniformity of the recognizer) and SatisfiesRG5 (global regularity condition). These notions rest on the indistinguishability relation already constructed in the Quotient module.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the connectivity predicates required by the Integration module, which assembles all Recognition Geometry components into a single framework summary. It directly supports the claim that recognition geometry organizes configurations by mutual indistinguishability and feeds the higher-level statements about complete integration of the theory.
scope and limits
- Does not define the indistinguishability relation or construct the quotient space.
- Does not prove global connectivity or integration theorems.
- Does not treat continuous or infinite-dimensional configuration spaces.
- Limits basic lemmas to empty sets, singletons, and resolution cells.
used by (1)
depends on (1)
declarations in this module (11)
-
def
IsRecognitionConnected -
theorem
isRecognitionConnected_empty -
theorem
isRecognitionConnected_singleton -
theorem
isRecognitionConnected_resolutionCell -
theorem
isRecognitionConnected_subset -
def
IsLocallyRegular -
def
IsRegular -
structure
SatisfiesRG5 -
theorem
locally_regular_cell_connected -
theorem
constant_recognizer_regular -
def
connectivity_status