module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealCauchy`

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 (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Kernel module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealNullSetoid module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RationalField module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.TraceClosure module_import

declarations in this module (21)

def lt L31
theorem lt_iff_toRat_lt L34
theorem zero_lt_of_positive L45
def PRCSquareGap L56
theorem PRCSquareGap_toRat L59
def PRCJCostDistance L68
theorem PRCJCostDistance_self_zero L71
theorem PRCJCostDistance_symmetric L78
structure PRCCauchySeq L90
def constant L100
theorem constant_term L109
def PRCNullEquivalent L118
def PRCNullDistanceTransitiveTarget L142
def PRCNullDistanceSetoidTarget L151
def PRCSameTerm L158
def PRCSameTermSetoid L172
def PRCReal L178
def ofRat L184
def realCauchyClaim L190
structure PRCRealCauchyCertificate L199
theorem real_cauchy_certificate L219