SelfReferenceComplete
plain-language theorem explainer
The SelfReferenceComplete structure assembles four components asserting that the RRF framework fully describes its own structure: a MetaRRF pairing subject and code, a DescriptiveFixedPoint for self-similarity, InternalConsistency from axioms, and CompilationAsRecognition linking type-checking to validity. Researchers on formal self-reference in physical theories cite it to close the recognition loop. It is realized by a direct record bundling of sibling structures with no additional lemmas or tactics.
Claim. A structure consisting of a meta-RRF (framework describing itself via subject and Lean code with type-check witness), a descriptive fixed point (self-similar description), internal consistency (derivability from axioms with no contradiction such as $0=1$), and compilation as recognition (successful type-checking counts as a recognition event).
background
The RRF Foundation module treats self-reference as the framework referring to its own formalization, with the Lean code itself an octave of the RRF and type-checking as measurement. MetaRRF pairs an RRFDescription (the subject) with LeanCode (the description) and a TypeCheckResult for compilation success. DescriptiveFixedPoint requires the description to equal itself, capturing self-similarity. InternalConsistency asserts derivability from foundational axioms, absence of obvious falsehoods, and rigorous proofs only. CompilationAsRecognition ties code to a recognition event via successful compilation.
proof idea
This is a structure definition realized by direct record construction. It bundles the four fields using existing sibling definitions: meta_rrf from thisFile, is_fixed_point from rrf_is_fixed_point, is_consistent from rrf_internally_consistent, and compilation_is_recognition from this_is_recognition. No lemmas from upstream results are invoked; the definition carries no computational content or proof obligations.
why it matters
This definition supplies the self-reference closure required by the module, directly feeding self_reference_complete (which constructs the instance) and self_reference_witnessed (which proves nonemptiness). It realizes the Gödel-like structure by asserting internal consistency without claiming a proof from within the system. In the Recognition framework it supports the fixed-point property at the meta level and the recognition composition law, completing the loop needed for the T0-T8 forcing chain and the emergence of spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.