TypeCheckResult
plain-language theorem explainer
TypeCheckResult is the inductive type classifying type-checking outcomes as either success or failure carrying an error string. It is cited in constructions of self-referential code within the RRF foundation, where Lean compilation counts as a recognition event. The definition is a direct inductive enumeration of the two cases with no further structure or proof obligations.
Claim. The type of type-checking outcomes is the inductive type with constructors $success$ and $failure(e)$ for error message $e$ in the type of strings.
background
The RRF Foundation module treats the Lean formalization itself as an octave of the Recognition framework, with compilation acting as a recognition measurement and type-checking as verification of internal consistency. TypeCheckResult records the binary outcome of that measurement. It depends on the active-edge constant A (defined as 1 in IntegrationGap, Masses.Anchor, and Modal.Actualization) and on the self-closure lemma establishing that phi lies in its own subfield.
proof idea
Inductive definition introducing the two constructors success and failure(error : String) with no recursion or additional fields.
why it matters
The definition supplies the result type for SelfReferentialCode and CompilationAsRecognition, which encode the claim that the RRF formalization recognizes itself. It thereby closes the meta-level loop described in the module documentation, consistent with the T7 eight-tick octave and the Gödel-style internal-consistency statement that the framework can prove its own propositions without proving its own consistency from within.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.