module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCompletenessIndependence`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCostOnField module_import

declarations in this module (9)

def IsLUBIn L56
theorem subfield_not_complete L65
theorem countable_subfield_not_complete L94
theorem T_not_complete L106
theorem real_has_lub L116
theorem completeness_not_forced_by_cost_axioms L127
theorem jcost_isCostRequirements L140
theorem completeness_not_forced_by_genuine_cost_laws L152
theorem completeness_is_exactly_the_continuum L171