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)
106structure OctaveLoop (State : Type) where
107 steps : Fin 8 → State
108 closure : steps 0 = steps 7 -- Conceptual closure
109
110/-- **THEOREM: Octave Loop Neutrality**
111 A complete octave loop has zero net recognition flux (σ = 0). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (15)
Lean names referenced from this declaration's body.
-
octave
in IndisputableMonolith.Aesthetics.MusicalScale
decl_use
-
State
in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
decl_use
-
complete
in IndisputableMonolith.Complexity.SAT.Backprop
decl_use
-
octave
in IndisputableMonolith.Constants
decl_use
-
has
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
octave
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
octave
in IndisputableMonolith.Masses.CoherenceExponent
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
octave
in IndisputableMonolith.MusicTheory.HarmonicModes
decl_use
-
State
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
Octave
in IndisputableMonolith.RRF.Core.Octave
decl_use
-
net
in IndisputableMonolith.RRF.Core.Strain
decl_use
-
net
in IndisputableMonolith.RRF.Foundation.Ledger
decl_use