SelfReferenceComplete
plain-language theorem explainer
A structure bundles the claim that the recognition framework possesses a meta-level description which forms a fixed point of itself, satisfies internal consistency from foundational axioms, and treats its own compilation as a recognition event. Researchers closing self-referential loops in formal physics or logic frameworks would cite this to complete the description hierarchy. As a structure definition it aggregates four component structures with no additional lemmas or tactics.
Claim. Let $M$ be a meta-description consisting of an RRF subject paired with its Lean code that type-checks successfully. Let $F$ be a descriptive fixed point asserting self-similarity of the description. Let $C$ be internal consistency witnessed by nonempty maps from reals to reals, absence of $0=1$, and terminal proofs only. Let $R$ be the assertion that compilation success constitutes recognition of validity. The structure is the 4-tuple $(M,F,C,R)$.
background
The module states that the RRF formalization is itself an octave of the RRF, with the Lean code serving as a recognition event: compilation acts as a proof and type-checking as a measurement. It notes a Gödel-like limit: the framework can refer to its own consistency but cannot prove it from within, yet can assert internal consistency without contradiction. MetaRRF pairs an RRFDescription subject with a LeanCode description whose type-check result witnesses validity. DescriptiveFixedPoint requires the description to equal itself. InternalConsistency requires foundational nonempty (ℝ → ℝ), ¬(0=1), and rigorous proofs only. CompilationAsRecognition links code, successful compilation, and the boolean recognized flag.
proof idea
This is a structure definition that directly aggregates the four component structures MetaRRF, DescriptiveFixedPoint, InternalConsistency, and CompilationAsRecognition. No lemmas are invoked and no tactics are used; the declaration simply packages the fields.
why it matters
The declaration supplies the terminal object that closes the self-reference hierarchy in the RRF foundation module. It is instantiated by the downstream definition self_reference_complete and witnessed as nonempty by the theorem self_reference_witnessed. The module doc positions it at the deepest level of closure, where the formalization asserts its own octave status while respecting the Gödel limit on internal consistency proofs. It aligns with the framework's claim that type-checking constitutes a recognition measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.