module module high

`IndisputableMonolith.RRF.Foundation.SelfReference`

The SelfReference module supplies definitions for type-checkable Lean code and self-referential structures inside the RRF Foundation. It introduces predicates such as isRecognized to capture code that refers to itself while remaining formally verifiable. Researchers formalizing the MetaPrinciple axiom cite it when grounding self-reference as the starting point for deriving constants from phi. The module contains only definitions and no proof obligations.

claimDefinitions for LeanCode (type-checkable code), SelfReferentialCode, isRecognized (recognition predicate), RRFDescription, currentRRF, MetaRRF, thisFile, FormalizationAsOctave, and rrf_is_fixed_point.

background

The module forms part of the foundational layer of the Reality Recognition Framework. It imports only Mathlib.Data.Real.Basic and introduces sibling definitions that formalize self-reference: LeanCode as verifiable Lean expressions, SelfReferentialCode as structures that name themselves, and isRecognized as the predicate asserting successful recognition. The parent RRF.Foundation module collects these pieces to state the single MetaPrinciple axiom together with constants derived from phi and a double-entry ledger.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the self-referential scaffolding required by the RRF.Foundation module, which states the MetaPrinciple as the single foundational axiom and derives physical constants from phi. It supports the Recognition Science chain by providing the formal objects that later steps use to reach the eight-tick octave and D=3.

scope and limits

Does not contain any theorem statements or proofs.
Does not derive physical constants or the ledger.
Does not state the MetaPrinciple axiom itself.
Does not import other RRF modules or physics-specific libraries.

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