isRecognized
plain-language theorem explainer
A self-referential code structure is marked recognized exactly when its type-check result indicates success. Workers on formal closure in Recognition Science cite this definition to complete the loop from formalization back to validation. The body reduces directly to a case distinction on the compilation outcome.
Claim. Let $s$ be a structure containing Lean source, a type-check result, and a self-reference indicator. Define isRecognized$(s)$ to be true if and only if the type-check result of $s$ is success.
background
The RRF Foundation module treats the Lean formalization as an instance of the recognition field. A self-referential code structure packages source code, its compilation status, and a predicate that the source mentions its own module name. This operationalizes the module insight that compilation serves as a proof and type-checking as a measurement. Upstream results include the local recognition field defined as maps from four indices to reals and structures for nuclear tiers and crystal lattices that populate the broader framework.
proof idea
The definition is realized by a direct match on the compilation field of the input structure, yielding true for success and false for any failure case.
why it matters
This definition realizes the self-description property of the Recognition Science framework at its foundational level. It supports the claim that the formalization constitutes an octave of itself, consistent with the eight-tick structure. No downstream theorems depend on it yet, leaving open the question of lifting this recognition to physical predictions such as the fine-structure constant bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.