module module

`IndisputableMonolith.RRF.Foundation.SelfReference`

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.RRF.Foundation module_import

declarations in this module (22)

structure LeanCode L30
inductive TypeCheckResult L37
structure SelfReferentialCode L42
def isRecognized L52
structure RRFDescription L60
def currentRRF L72
structure MetaRRF L80
def thisFile L90
structure FormalizationAsOctave L103
def rrfFormalizationOctave L112
structure DescriptiveFixedPoint L122
def rrf_is_fixed_point L129
theorem rrf_fixed_point_exists L135
structure InternalConsistency L145
def rrf_internally_consistent L154
theorem internal_consistency_exists L162
structure CompilationAsRecognition L172
def this_is_recognition L181
theorem recognition_event_exists L189
structure SelfReferenceComplete L195
def self_reference_complete L206
theorem self_reference_witnessed L214