`MetaRRF`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.SelfReference
domain: RRF
line: 80 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.SelfReference on GitHub at line 80.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  77}
  78
  79/-- The Meta-RRF: the framework describing itself. -/
  80structure MetaRRF where
  81  /-- The subject (the RRF). -/
  82  subject : RRFDescription
  83  /-- The description (this Lean code). -/
  84  description : LeanCode
  85  /-- The description is valid.
  86      Witnessed by compilation success. -/
  87  description_compiles : TypeCheckResult
  88
  89/-- This file is a MetaRRF. -/
  90def thisFile : MetaRRF := {
  91  subject := currentRRF,
  92  description := { source := "-- RRF Foundation: SelfReference", module := "SelfReference" },
  93  description_compiles := .success
  94}
  95
  96/-! ## Octave Structure of the Formalization -/
  97
  98/-- The formalization is an octave of the RRF.
  99
 100Just as proteins fold in the biological octave,
 101Lean proofs "fold" in the logical octave.
 102-/
 103structure FormalizationAsOctave where
 104  /-- The logical octave. -/
 105  octave_type : String
 106  /-- The strain functional (proof complexity). -/
 107  strain : LeanCode → ℕ  -- Lines of proof, or similar metric
 108  /-- Lower strain = simpler proof = more "elegant". -/
 109  elegance : LeanCode → ℝ
 110

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.