module module

`IndisputableMonolith.RecogGeom.RSBridge`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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.Comparative module_import
IndisputableMonolith.RecogGeom.Composition module_import
IndisputableMonolith.RecogGeom.FiniteResolution module_import
IndisputableMonolith.RecogGeom.Quotient module_import

declarations in this module (12)

class RSConfigSpace L58
structure RSLocalityFromRHat L77
def toLocalConfigSpace L92
structure RSMeasurement L121
def toRecognizer L128
structure EightTickFiniteResolution L143
theorem eight_tick_implies_RG4 L149
theorem RS_instantiates_RG L163
def physical_space_is_quotient L175
structure JCostComparative L192
def toRecognitionDistance L205
def rsbridge_status L236