pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

TypeCheckResult

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  37inductive TypeCheckResult
  38  | success : TypeCheckResult
  39  | failure (error : String) : TypeCheckResult
  40
  41/-- A self-referential code structure. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.