CompilationAsRecognition
plain-language theorem explainer
The structure models compilation of Lean code as a recognition event that verifies propositions against type theory. Researchers formalizing self-referential systems in Recognition Science cite it to close the loop between code and measurement. The definition simply records a LeanCode object, its TypeCheckResult, and a boolean flag for successful recognition.
Claim. A record consisting of a Lean code object (source string and module name), a type-check outcome (success or failure with error string), and a boolean indicating that the propositions are recognized as valid.
background
The RRF Foundation module establishes self-reference by treating the Lean formalization itself as an instance of the Recognition framework. LeanCode is the structure holding source text and module identifier for any type-checkable code fragment. TypeCheckResult is the inductive type with constructors success and failure(error), capturing whether compilation succeeds. The module doc notes that type-checking acts as a measurement and that the formalization forms an octave of the RRF, allowing internal consistency without proving external consistency from within.
proof idea
This is a structure definition that directly assembles the three fields: code of type LeanCode, compiles of type TypeCheckResult, and recognized of type Bool. No lemmas or tactics are applied; the declaration itself supplies the record constructor.
why it matters
It supplies the concrete witness used by recognition_event_exists and SelfReferenceComplete to establish that a recognition event occurs inside the formalization. The construction fills the self-reference step in the RRF foundation, linking compilation to the recognition process described in the module doc. It touches the open question of internal consistency without claiming a full Gödel-proof of consistency from within the system.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.