`SelfReferenceComplete`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.SelfReference
domain: RRF
line: 195 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.SelfReference on GitHub at line 195.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 192/-! ## Summary -/
 193
 194/-- The complete self-reference structure. -/
 195structure SelfReferenceComplete where
 196  /-- The Meta-RRF exists. -/
 197  meta_rrf : MetaRRF
 198  /-- It's a fixed point. -/
 199  is_fixed_point : DescriptiveFixedPoint
 200  /-- It's internally consistent. -/
 201  is_consistent : InternalConsistency
 202  /-- Compilation is recognition. -/
 203  compilation_is_recognition : CompilationAsRecognition
 204
 205/-- The self-reference structure is complete. -/
 206def self_reference_complete : SelfReferenceComplete := {
 207  meta_rrf := thisFile,
 208  is_fixed_point := rrf_is_fixed_point,
 209  is_consistent := rrf_internally_consistent,
 210  compilation_is_recognition := this_is_recognition
 211}
 212
 213/-- Self-reference completeness is witnessed. -/
 214theorem self_reference_witnessed : Nonempty SelfReferenceComplete :=
 215  ⟨self_reference_complete⟩
 216
 217end RRF.Foundation.SelfReference
 218end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.