IndisputableMonolith.RRF.Foundation.SelfReference
The SelfReference module defines Lean structures for self-referential code that can be type-checked inside the Reality Recognition Framework. It supplies the types and predicates needed to represent the framework's own formalization. Researchers building meta-consistent foundations for physics would cite these definitions when constructing the RRF axiom system. The module consists entirely of definitions with no theorems or proofs.
claimDefinitions of self-referential structures: $\mathsf{LeanCode}$, $\mathsf{SelfReferentialCode}$, $\mathsf{isRecognized} : \mathsf{SelfReferentialCode} \to \mathsf{Prop}$, and related fixed-point predicates in the RRF.
background
This module belongs to the foundational layer of the Reality Recognition Framework. The parent module RRF.Foundation contains the single MetaPrinciple axiom (MP), constants derived from $\phi$, and a double-entry ledger for conservation. SelfReference adds the machinery for self-reference so that the formal system can describe its own code, consistent with the Recognition Science emphasis on fixed points and self-similar structures.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
These definitions feed the RRF.Foundation module that houses the MetaPrinciple, $\phi$-derived constants, and ledger. The self-reference layer supports the framework's claim to describe its own formalization as a fixed point, directly enabling the meta-principle that anchors the entire RRF construction.
scope and limits
- Does not contain theorems or proofs.
- Does not derive physical constants or the ledger.
- Does not implement the MetaPrinciple axiom.
used by (1)
declarations in this module (22)
-
structure
LeanCode -
inductive
TypeCheckResult -
structure
SelfReferentialCode -
def
isRecognized -
structure
RRFDescription -
def
currentRRF -
structure
MetaRRF -
def
thisFile -
structure
FormalizationAsOctave -
def
rrfFormalizationOctave -
structure
DescriptiveFixedPoint -
def
rrf_is_fixed_point -
theorem
rrf_fixed_point_exists -
structure
InternalConsistency -
def
rrf_internally_consistent -
theorem
internal_consistency_exists -
structure
CompilationAsRecognition -
def
this_is_recognition -
theorem
recognition_event_exists -
structure
SelfReferenceComplete -
def
self_reference_complete -
theorem
self_reference_witnessed