LeanCode
plain-language theorem explainer
LeanCode records Lean source together with its module identifier as a structure that can be type-checked. Self-reference researchers in Recognition Science cite the definition when closing the loop from formalization back to the RRF itself. The declaration introduces the record directly with two String fields.
Claim. A record type with a source string field and a module string field, denoting Lean code that admits type-checking.
background
The module sets the RRF formalization as self-referential closure: this Lean code is a recognition event, its compilation a proof, and its type-checking a measurement. The framework can refer to its own consistency but cannot prove it internally, consistent with Gödel. Upstream structures supply the supporting physics: J-cost minimization is convex with unique minimum at x=1 (PhysicsComplexityStructure.of); Q3 forces SU(3)×SU(2)×U(1) plus three generations (SpectralEmergence.of); nuclear densities occupy discrete φ-tiers (NucleosynthesisTiers.of).
proof idea
Direct structure definition introducing the record type with two fields; no lemmas or tactics are applied.
why it matters
The definition supplies the base object for CompilationAsRecognition (type-checking as recognition) and MetaRRF (framework describing itself). It realizes the module claim that the formalization is an octave of the RRF, closing the self-reference loop at the level of T7 eight-tick octave and the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.