`currentRRF`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.SelfReference
domain: RRF
line: 72 · 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 72.

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

  69  hypothesis_count : ℕ
  70
  71/-- The current RRF formalization. -/
  72def currentRRF : RRFDescription := {
  73  core_witness := IndisputableMonolith.Foundation.φ,
  74  theorem_count := 10, -- Approximate count
  75  model_witness := ⟨IndisputableMonolith.Cost.Jcost⟩,
  76  hypothesis_count := 5
  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-/

papers checked against this theorem

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