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)
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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
Lean names referenced from this declaration's body.
-
octave
in IndisputableMonolith.Aesthetics.MusicalScale
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
octave
in IndisputableMonolith.Constants
decl_use
-
or
in IndisputableMonolith.Constants.EulerMascheroni
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
RRF
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
octave
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
octave
in IndisputableMonolith.Masses.CoherenceExponent
decl_use
-
octave
in IndisputableMonolith.MusicTheory.HarmonicModes
decl_use
-
LeanCode
in IndisputableMonolith.RRF.Foundation.SelfReference
decl_use