octave — Recognition explainer

formal statement (Lean)

  14def octave : ℝ := 8 * tick

proof body

Definition body.

  15
  16/-- Golden ratio φ as a concrete real. -/

used by (40)

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

octave in IndisputableMonolith.Aesthetics.MusicalScale decl_use
layerSysPlus_comp in IndisputableMonolith.Algebra.RecognitionCategory decl_use
OctaveAlgHom in IndisputableMonolith.Algebra.RecognitionCategory decl_use
OctaveLoop in IndisputableMonolith.Applied.CoherenceTechnology decl_use
rs_device in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
tick in IndisputableMonolith.Constants decl_use
breathCycle in IndisputableMonolith.Constants.RSNativeUnits decl_use
octavePhase in IndisputableMonolith.Constants.RSNativeUnits decl_use
phiRung_neg in IndisputableMonolith.Constants.RSNativeUnits decl_use
ticksToOctaves in IndisputableMonolith.Constants.RSNativeUnits decl_use
businessCyclePeriod in IndisputableMonolith.Econ.LedgerEconomics decl_use
businessCyclePeriod_lower in IndisputableMonolith.Econ.LedgerEconomics decl_use
businessCyclePeriod_pos in IndisputableMonolith.Econ.LedgerEconomics decl_use
businessCyclePeriod_upper in IndisputableMonolith.Econ.LedgerEconomics decl_use
economicPhases in IndisputableMonolith.Econ.LedgerEconomics decl_use
eight_economic_phases in IndisputableMonolith.Econ.LedgerEconomics decl_use
ledgerConservation_eq_one in IndisputableMonolith.Econ.LedgerEconomics decl_use
octaveGrowthMultiplier in IndisputableMonolith.Econ.LedgerEconomics decl_use
flipAt512 in IndisputableMonolith.Foundation.Breath1024 decl_use
Gap45Region in IndisputableMonolith.Foundation.Gap45Degeneracy decl_use
J_at_phi_approx in IndisputableMonolith.Foundation.PhiEmergence decl_use
framework_self_consistent in IndisputableMonolith.Foundation.SpectralEmergence decl_use
octave in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music decl_use
perfectFourth in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music decl_use
strictMusicRealization in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music decl_use
impulse_after_octaves_mono_decay in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
impulse_at_saturation in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
impulse_per_octave in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
impulse_tambora_eq_zero in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use
octavePeriod_eq_eight in IndisputableMonolith.Geology.VolcanicForcingAsJCostImpulse decl_use

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.

octave in IndisputableMonolith.Aesthetics.MusicalScale decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
octave in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music decl_use
octave in IndisputableMonolith.Masses.CoherenceExponent decl_use
octave in IndisputableMonolith.MusicTheory.HarmonicModes decl_use