module module

`IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer`

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 module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.ArithmeticFromLogic module_import
IndisputableMonolith.Foundation.ObserverFromRecognition module_import

declarations in this module (22)

def interfaceSetoid L48
def RecognitionLattice L54
def cellOf L58
theorem cell_eq_iff_kernel L64
def cellLabel L72
theorem cellLabel_cellOf L78
def neighborhood L82
theorem cell_mem_own_neighborhood L87
theorem every_cell_has_label L92
theorem nontrivial_recognition_forces_lattice L101
def pointLattice L109
def SameKernel L116
def latticeEquivOfSameKernel L121
theorem latticeEquivOfSameKernel_cell L143
def iteratedCarrier L150
def logicNatToLattice L155
theorem logicNatToLattice_zero L159
theorem logicNatToLattice_step L163
theorem logicNat_interprets_into_lattice L170
structure RecognitionLatticeCert L180
def recognitionLatticeCert L198
theorem recognitionLatticeCert_inhabited L205