def
definition
thisFile
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Foundation.SelfReference on GitHub at line 90.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
octave -
of -
Structure -
octave -
of -
RRF -
is -
of -
as -
is -
of -
octave -
is -
of -
octave -
is -
octave -
Octave -
currentRRF -
MetaRRF
used by
formal source
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
111/-- The RRF formalization as an octave. -/
112def rrfFormalizationOctave : FormalizationAsOctave := {
113 octave_type := "logical",
114 strain := fun c => c.source.length, -- Simplistic: length as complexity
115 elegance := fun c => 1.0 / (c.source.length : ℝ)
116}
117
118
119/-! ## Fixed Point Structure -/
120