RecognitionGeometry
plain-language theorem explainer
RecognitionGeometry bundles a local configuration space, a recognizer, and the finite resolution property into a single structure over configuration space C and event space E. Researchers citing the Recognition Science integration would reference this definition when invoking the master theorem that assembles RG0-RG7. The declaration is a direct structure definition that packages the three fields with no additional proof steps.
Claim. A recognition geometry over configuration space $C$ and event space $E$ consists of a local configuration space structure on $C$, a recognizer map from $C$ to $E$, and the finite resolution property of the recognizer relative to that locality.
background
Recognition Geometry treats configurations as primitive objects and events as outputs of recognizers, with space emerging as the quotient by the indistinguishability relation. The module states the core axioms RG0-RG7: nonempty configuration space, locality via neighborhood refinement, existence of recognizers, indistinguishability equivalence, finite resolution of events, local regularity of preimages, composition of recognizers, and comparative structure inducing preorders. Upstream modules supply the individual components: LocalConfigSpace from Locality, Recognizer from Recognizer, and HasFiniteResolution from FiniteResolution.
proof idea
The declaration is a structure definition that directly packages the three fields: locality of type LocalConfigSpace C, recognizer of type Recognizer C E, and finite_resolution of type HasFiniteResolution locality recognizer. No lemmas or tactics are invoked; it is a pure bundling definition.
why it matters
This structure supplies the central type for the master theorem asserting completeness of Recognition Geometry under RG0-RG7. It is referenced downstream in the Riemann Hypothesis statement, which is conditional on RecognitionGeometry assumptions, and in the refinement theorem establishing surjectivity of composite quotient maps. The definition closes the integration step that maps RS ledger states to configuration space and measurements to recognizers, while leaving open the derivation of the phi-ladder and spatial dimension from the geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.