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)
189def ticksToOctaves (t : ℕ) : ℕ := t / 8
proof body
Definition body.
190
191/-- Phase within an octave (0..7). -/
depends on (7)
Lean names referenced from this declaration's body.
-
octave
in IndisputableMonolith.Aesthetics.MusicalScale
decl_use
-
octave
in IndisputableMonolith.Constants
decl_use
-
octave
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
Phase
in IndisputableMonolith.Information.ChurchTuringPhysicsStructure
decl_use
-
octave
in IndisputableMonolith.Masses.CoherenceExponent
decl_use
-
octave
in IndisputableMonolith.MusicTheory.HarmonicModes
decl_use
-
Phase
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use