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

currentRRF

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  72def currentRRF : RRFDescription := {

proof body

Definition body.

  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. -/

used by (2)

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

depends on (3)

Lean names referenced from this declaration's body.