SelfReferentialCode
plain-language theorem explainer
This structure packages a Lean code object with its type-check outcome and a substring check confirming self-reference via the module name in the source. Meta-mathematicians studying formal self-reference or type-theoretic closure would cite it when analyzing the RRF formalization's internal description. The definition is a direct three-field structure with no reduction steps or lemmas.
Claim. A structure consisting of a code object (source string $s$ and module name $m$), a type-check result $r$ (success or failure with error string), and the predicate that $s$ contains $m$ as a substring.
background
The RRF Foundation module formalizes self-reference to capture how the framework describes its own structure. LeanCode is the structure holding source : String and module : String. TypeCheckResult is the inductive type with constructors success and failure (error : String). The module doc states that this Lean code is a recognition event, its compilation a proof, and type-checking a measurement, establishing the deepest level of closure.
proof idea
This is a pure structure definition. The three fields are declared directly: code of type LeanCode, compiles of type TypeCheckResult, and self_referential as the Boolean expression code.source.contains code.module.toSubstring. No tactics or upstream lemmas are invoked.
why it matters
The structure supplies the data type underlying the isRecognized predicate, which returns true precisely on successful compilation. It realizes the module insight that the RRF formalization is itself an octave of the RRF and supports discussion of internal consistency without a self-proof, consistent with the Gödel-like limitation noted in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.